Repository: pysmt/pysmt
Pull request #73 (2015-04-14 16:12:06)

Z3 lia qe error
This PR implements error rising in Z3 quantifier eliminator when a formula containing an unsupported operator is found. This solves #47. 

marcogario: When you fix the typo, try to make a single commit out of these 3.

Patch:
diff --git a/pysmt/exceptions.py b/pysmt/exceptions.py
index 43f32e3..3e754be 100644
--- a/pysmt/exceptions.py
+++ b/pysmt/exceptions.py
@@ -67,3 +67,18 @@ class SolverStatusError(Exception):
     incorrectly called in the wrong status.
     """
     pass
+
+class ConvertExpressionError(Exception):
+    """
+    Exception raised if the converter cannot convert an expression
+    due to limited expressiveness in pySMT.
+    """
+
+    def __init__(self, message=None, expression=None):
+        if message is not None:
+            Exception.__init__(self, message)
+        else:
+            Exception.__init__(self)
+        self.expression=expression
+
+    pass
diff --git a/pysmt/solvers/msat.py b/pysmt/solvers/msat.py
index 1e3d221..b9e584c 100644
--- a/pysmt/solvers/msat.py
+++ b/pysmt/solvers/msat.py
@@ -704,6 +704,7 @@ if hasattr(mathsat, "MSAT_EXIST_ELIM_ALLSMT_FM"):
             self.msat_config = mathsat.msat_create_default_config("QF_LRA")
             self.msat_env = mathsat.msat_create_env(self.msat_config)
             self.converter = MSatConverter(environment, self.msat_env)
+            self._destroyed = False
 
 
         def eliminate_quantifiers(self, formula):
@@ -745,6 +746,12 @@ if hasattr(mathsat, "MSAT_EXIST_ELIM_ALLSMT_FM"):
             subf = formula.arg(0)
             return self.exist_elim(variables, subf)
 
+        def __del__(self):
+            if not self._destroyed:
+                self._destroyed = True
+                mathsat.msat_destroy_env(self.msat_env)
+                mathsat.msat_destroy_config(self.msat_config)
+
 
     class MSatFMQuantifierEliminator(MSatQuantifierEliminator):
         def __init__(self, environment, logic=None):
diff --git a/pysmt/solvers/qelim.py b/pysmt/solvers/qelim.py
index f802463..8897591 100644
--- a/pysmt/solvers/qelim.py
+++ b/pysmt/solvers/qelim.py
@@ -29,3 +29,16 @@ class QuantifierEliminator(object):
         separately.
         """
         raise NotImplementedError
+
+    def __enter__(self):
+        """ Manage entering a Context (i.e., with statement) """
+        return self
+
+
+    def __exit__(self, exc_type, exc_val, exc_tb):
+        """ Manage exiting from Context (i.e., with statement)
+
+        The default behaviour is to explicitely destroy the qelim to free
+        the associated resources.
+        """
+        del self
diff --git a/pysmt/solvers/z3.py b/pysmt/solvers/z3.py
index 96c2c32..88f6b44 100644
--- a/pysmt/solvers/z3.py
+++ b/pysmt/solvers/z3.py
@@ -32,7 +32,8 @@ from pysmt.walkers import DagWalker
 from pysmt.exceptions import (SolverReturnedUnknownResultError,
                               SolverNotConfiguredForUnsatCoresError,
                               SolverStatusError,
-                              InternalSolverError)
+                              InternalSolverError,
+                              ConvertExpressionError)
 from pysmt.decorators import clear_pending_pop
 
 from pysmt.logics import LRA, LIA, PYSMT_LOGICS
@@ -246,6 +247,7 @@ class Z3Converter(Converter, DagWalker):
                 "Quantified back conversion is currently not supported")
 
         args = [self.back(x) for x in expr.children()]
+
         res = None
         if z3.is_and(expr):
             res = self.mgr.And(args)
@@ -316,11 +318,11 @@ class Z3Converter(Converter, DagWalker):
         elif z3.is_ite(expr):
             res = self.mgr.Ite(args[0], args[1], args[2])
 
-        else:
-            raise TypeError("Unsupported expression:", expr)
 
         if res is None:
-            raise TypeError("Unsupported expression:", expr)
+            raise ConvertExpressionError(message=("Unsupported expression: %s" %
+                                                   str(expr)),
+                                          expression=expr)
 
         self.backconversion[askey(expr)] = res
 
@@ -455,4 +457,19 @@ class Z3QuantifierEliminator(QuantifierEliminator):
                        pull_cheap_ite=True,
                        ite_extra_rules=True).as_expr()
         res = eliminator(s, eliminate_variables_as_block=True).as_expr()
-        return self.converter.back(res)
+
+        pysmt_res = None
+        try:
+            pysmt_res = self.converter.back(res)
+        except ConvertExpressionError:
+            if logic <= LRA:
+                raise
+            raise ConvertExpressionError(message=("Unable to represent" \
+                "expression %s in pySMT: the quantifier elimination for " \
+                "LIA is incomplete as it requires the modulus. You can " \
+                "find the Z3 expression representing the quantifier " \
+                "elimination as the attribute 'expression' of this " \
+                "exception object" % str(res)),
+                                          expression=res)
+
+        return pysmt_res


Test patch:
diff --git a/pysmt/test/test_regressions.py b/pysmt/test/test_regressions.py
index 3c50431..2ce5a75 100644
--- a/pysmt/test/test_regressions.py
+++ b/pysmt/test/test_regressions.py
@@ -18,11 +18,12 @@
 from fractions import Fraction
 
 from pysmt.shortcuts import (Real, Plus, Symbol, Equals, And, Bool, Or,
-                             Div, LT, LE, Int, ToReal, Iff)
-from pysmt.shortcuts import Solver, get_env
+                             Div, LT, LE, Int, ToReal, Iff, Exists, Times)
+from pysmt.shortcuts import Solver, get_env, qelim
 from pysmt.typing import REAL, BOOL, INT, FunctionType
 from pysmt.test import TestCase, skipIfSolverNotAvailable, skipIfNoSolverForLogic
-from pysmt.logics import QF_UFLIRA, QF_BOOL
+from pysmt.logics import QF_UFLIRA, QF_BOOL, LIA
+from pysmt.exceptions import ConvertExpressionError
 
 
 class TestRegressions(TestCase):
@@ -165,6 +166,20 @@ class TestRegressions(TestCase):
             s.exit()
             self.assertTrue(True)
 
+    @skipIfNoSolverForLogic(LIA)
+    def test_lia_qe_requiring_modulus(self):
+        x = Symbol("x", INT)
+        y = Symbol("y", INT)
+        f = Exists([x], Equals(y, Times(x, Int(2))))
+        with self.assertRaises(ConvertExpressionError):
+            qelim(f)
+
+        try:
+            qelim(f)
+        except ConvertExpressionError as ex:
+            # The modulus operator must be there
+            self.assertIn("%2", str(ex.expression))
+
 
 if __name__ == "__main__":
     import unittest