Repository: pysmt/pysmt
Pull request #733 (2022-07-31 09:47:51)

Deterministic get_closer_logic
In https://github.com/pysmt/pysmt/issues/731#issuecomment-1200380943, we discussed how having a non-deterministic answer in `get_logic` can lead to problems.

We do not expect the logic detection in `get_logic` to pick "the best" logic, but we want at least to fail consistently so that users are aware that a logic needs to be specified.

This PR does two things:
1. Adds QF_LIRA to the set of `PYSMT_LOGICS`, this was the trigger for the work, but only adding this logic does not solve the problem.
2. Adds a test for showing that `get_closer_logic` is deterministic independently of the the order of the input argument `supported_logics`.

**Alternatives Considered**
There was another way to fix the same that would have been to make both `PYSMT_LOGICS` and `SMTLIB_LOGICS` an ordered set. I considered and discarded this option because in general we do not need the ordering, and the solution seemed fragile.
Overall, I believe the root cause is `get_closer_logic` not properly accounting for multiple logics being "close" (as we do instead for `most_generic_logic`).

/cc @enmag 


Patch:
diff --git a/pysmt/logics.py b/pysmt/logics.py
index 9f4ee14..e10a231 100644
--- a/pysmt/logics.py
+++ b/pysmt/logics.py
@@ -480,6 +480,14 @@ variables.""",
                quantifier_free=True,
                real_arithmetic=True)
 
+QF_LIRA = Logic(name="QF_LIRA",
+                description=\
+"""Unquantified linear integer and real arithmetic""",
+                integer_arithmetic=True,
+                real_arithmetic=True,
+                linear=True,
+                quantifier_free=True)
+
 QF_NIA = Logic(name="QF_NIA",
                description=\
 """Quantifier-free integer arithmetic.""",
@@ -667,7 +675,7 @@ QF_LOGICS = frozenset(_l for _l in LOGICS if _l.quantifier_free)
 # This is the set of logics supported by the current version of pySMT
 #
 PYSMT_LOGICS = frozenset([QF_BOOL, QF_IDL, QF_LIA, QF_LRA, QF_RDL, QF_UF, QF_UFIDL,
-                          QF_UFLIA, QF_UFLRA, QF_UFLIRA,
+                          QF_UFLIA, QF_UFLRA, QF_UFLIRA, QF_LIRA,
                           BOOL, LRA, LIA, UFLIRA, UFLRA,
                           QF_BV, QF_UFBV,
                           QF_SLIA,
@@ -795,10 +803,17 @@ def get_closer_logic(supported_logics, logic):
     does not support the given logic.
 
     """
-    res = [l for l in supported_logics if logic <= l]
-    if len(res) == 0:
+    candidates = [l for l in supported_logics if logic <= l]
+    if len(candidates) == 0:
         raise NoLogicAvailableError("Logic %s is not supported" % logic)
-    return min(res)
+
+    # We remove from the candidates, the logics that subsume another candidate
+    # (i.e. that are more general) because we are looking for the closer logic
+    res = [l for l in candidates if not any(l != k and k <= l for k in candidates)]
+
+    # There might be multiple incomparable logics that are closer, we
+    # deterministically select the one having a lexicographically smaller name
+    return sorted(res, key=lambda x:str(x))[0]
 
 
 def get_closer_pysmt_logic(target_logic):


Test patch:
diff --git a/pysmt/test/test_logics.py b/pysmt/test/test_logics.py
index e3dbc83..c4e4da1 100644
--- a/pysmt/test/test_logics.py
+++ b/pysmt/test/test_logics.py
@@ -16,9 +16,9 @@
 #   limitations under the License.
 #
 import pysmt.logics
-from pysmt.logics import get_logic_by_name, get_logic, most_generic_logic
+from pysmt.logics import get_closer_logic, get_logic_by_name, get_logic, most_generic_logic
 from pysmt.logics import PYSMT_LOGICS
-from pysmt.logics import QF_LIA, LIA, UFLIRA, LRA, QF_UFLIRA, QF_BV, NRA, QF_IDL, QF_BOOL
+from pysmt.logics import QF_LIA, LIA, UFLIRA, LRA, QF_UFLIRA, QF_BV, NRA, QF_IDL, QF_BOOL, QF_NIRA, QF_LIRA
 from pysmt.logics import Theory
 from pysmt.exceptions import (UndefinedLogicError, NoSolverAvailableError,
                               NoLogicAvailableError)
@@ -142,5 +142,10 @@ class TestLogic(TestCase):
                    integer_arithmetic=True)
         self.assertIsNotNone(t)
 
+    def test_get_closer_logic_is_deterministic(self):
+        l1 = get_closer_logic([QF_UFLIRA, QF_NIRA], QF_LIRA)
+        l2 = get_closer_logic([QF_NIRA, QF_UFLIRA], QF_LIRA)
+        self.assertEqual(l1, l2)
+
 if __name__ == "__main__":
     main()