Fix: #39 by relying on the same sympy satisfiability strategy

src/predi/comparator.py

@@ -278,7 +278,7 @@ def _implies(self, expr1, expr2, level=0):
                 else:
                     printer(f"Implies {expr1} to {expr2}: True", level=0)
                     return True
-            if all(isinstance(arg, (sp.Float, sp.Integer, sp.Symbol)) for arg in [expr1.lhs, expr1.rhs, expr2.lhs, expr2.rhs]):
+            elif all(isinstance(arg, (sp.Float, sp.Integer, sp.Symbol)) for arg in [expr1.lhs, expr1.rhs, expr2.lhs, expr2.rhs]):
                 printer(f'Inside!... expr1: {expr1}, expr2: {expr2}', level)
                 # Check if the negation of the implication is not satisfiable
                 try:
@@ -290,4 +290,15 @@ def _implies(self, expr1, expr2, level=0):
                 except Exception as e:
                     printer(f"Error (satisfiability error): {e}", level)
                     return False
+            else:
+                printer(f'Not all arguments are numbers, floats, or symbols in expr1 and expr2, however, we still try to use the same sympy satisfiability check', level)
+                try:
+                    negation = sp.And(expr1, Not(expr2))
+                    printer(f"Negation of the implication {expr1} -> {expr2}: {satisfiable(negation)}; type of {type(satisfiable(negation))}", level)
+                    result = not satisfiable(negation, use_lra_theory=True)
+                    printer(f"Implication {expr1} -> {expr2} using satisfiable: {result}", level)
+                    return result
+                except Exception as e:
+                    printer(f"Error (satisfiability error): {e}", level)
+                    return False
         return False

tests/test_comparator.py

@@ -12,7 +12,8 @@
     ],
     'The second predicate is stronger.': [
         ("msg.sender == msg.origin || a < b", "a < b"),
-        ("a > 12", "a > 13")
+        ("a > 12", "a > 13"),
+        ("a + 1 <= b", "a + 1 < b"),
     ],
     'The predicates are equivalent.': [
         ("msg.sender == msg.origin", "msg.origin == msg.sender"),