Merge pull request #58 from pysmt/msat_exist_elim_integration

Integrated MathSAT ExistElim API

docs/CHANGES.rst

@@ -9,6 +9,11 @@ General:
 * Added support for Python 3. The library works with both Python 2 and
   Python 3.
 
+* Added two new quantifier eliminators for LRA based on the MathSAT
+  api. One (msat_fm) used Fourier-Motzkin algorithm, the other
+  (msat_lw) uses Loos-Weisspfenning elimination (aka Virtual
+  Substitution)
+
 
 0.2.4: 2015-03-15  -- PicoSAT
 -----------------------------

pysmt/cmd/install.py

@@ -155,7 +155,7 @@ def download(url, file_name):
 def install_msat(options):
     """Installer for the MathSAT5 solver python interafce"""
 
-    base_name =  "mathsat-5.2.12-linux-%s" % get_architecture()
+    base_name =  "mathsat-5.3.4-linux-%s" % get_architecture()
     archive_name = "%s.tar.gz" % base_name
     archive = os.path.join(BASE_DIR, archive_name)
     dir_path = os.path.join(BASE_DIR, base_name)
@@ -415,7 +415,7 @@ def install_picosat(options):
 def check_install():
     """Checks which solvers are visible to pySMT."""
 
-    from pysmt.shortcuts import Solver
+    from pysmt.shortcuts import Solver, QuantifierEliminator
     from pysmt.exceptions import NoSolverAvailableError
 
     required_solver = os.environ.get("PYSMT_SOLVER")
@@ -425,15 +425,28 @@ def check_install():
         # Special case for bdd
         required_solver = "bdd"
 
-
+    print("Solvers:")
     for solver in ['msat', 'z3', 'cvc4', 'yices', 'bdd', 'picosat']:
         is_installed = False
         try:
             Solver(name=solver)
             is_installed = True
         except NoSolverAvailableError:
             is_installed = False
-        print("%s%s" % (solver.ljust(10), is_installed))
+        print("  %s%s" % (solver.ljust(10), is_installed))
+
+        if solver == required_solver and not is_installed:
+            raise Exception("Was expecting to find %s installed" % required_solver)
+
+    print("\nQuantifier Eliminators:")
+    for solver in ['msat_fm', 'msat_lw', 'z3']:
+        is_installed = False
+        try:
+            QuantifierEliminator(name=solver)
+            is_installed = True
+        except NoSolverAvailableError:
+            is_installed = False
+        print("  %s%s" % (solver.ljust(10), is_installed))
 
         if solver == required_solver and not is_installed:
             raise Exception("Was expecting to find %s installed" % required_solver)

pysmt/factory.py

@@ -33,7 +33,7 @@
 from pysmt.oracles import get_logic
 
 DEFAULT_SOLVER_PREFERENCE_LIST = ['msat', 'z3', 'cvc4', 'yices', 'picosat', 'bdd']
-DEFAULT_QELIM_PREFERENCE_LIST = ['z3']
+DEFAULT_QELIM_PREFERENCE_LIST = ['z3', 'msat_fm', 'msat_lw']
 DEFAULT_LOGIC = QF_UFLIRA
 
 class Factory(object):
@@ -206,6 +206,14 @@ def _get_available_qe(self):
         except ImportError:
             pass
 
+        try:
+            from pysmt.solvers.msat import (MSatFMQuantifierEliminator,
+                                            MSatLWQuantifierEliminator)
+            self._all_qelims['msat_fm'] = MSatFMQuantifierEliminator
+            self._all_qelims['msat_lw'] = MSatLWQuantifierEliminator
+        except ImportError:
+            pass
+
 
     def set_solver_preference_list(self, preference_list):
         """Defines the order in which to pick the solvers.

pysmt/solvers/msat.py

@@ -21,20 +21,26 @@
 
 import mathsat
 
-import pysmt.logics
+from pysmt.logics import LRA, PYSMT_QF_LOGICS
+from pysmt.oracles import get_logic
+
+import pysmt.operators as op
 from pysmt import typing as types
+
 from pysmt.solvers.solver import Solver, Converter
 from pysmt.solvers.smtlib import SmtLibBasicSolver, SmtLibIgnoreMixin
 from pysmt.solvers.eager import EagerModel
 from pysmt.walkers import DagWalker
 from pysmt.exceptions import SolverReturnedUnknownResultError
 from pysmt.exceptions import InternalSolverError
 from pysmt.decorators import clear_pending_pop
+from pysmt.solvers.qelim import QuantifierEliminator
+from pysmt.walkers.identitydag import IdentityDagWalker
 
 
 class MathSAT5Solver(Solver, SmtLibBasicSolver, SmtLibIgnoreMixin):
 
-    LOGICS = pysmt.logics.PYSMT_QF_LOGICS
+    LOGICS = PYSMT_QF_LOGICS
 
     def __init__(self, environment, logic, options=None, debugFile=None):
         Solver.__init__(self,
@@ -574,3 +580,77 @@ def declare_variable(self, var):
                                                  tp)
             self.symbol_to_decl[var] = decl
             self.decl_to_symbol[mathsat.msat_decl_id(decl)] = var
+
+
+# Check if we are working on a version MathSAT supporting quantifier elimination
+if hasattr(mathsat, "MSAT_EXIST_ELIM_ALLSMT_FM"):
+    class MSatQuantifierEliminator(QuantifierEliminator, IdentityDagWalker):
+
+        def __init__(self, environment, algorithm='fm'):
+            """Algorithm can be either 'fm' (for Fourier-Motzkin) or 'lw' (for
+               Loos-Weisspfenning)"""
+
+            IdentityDagWalker.__init__(self, env=environment)
+
+            self.functions[op.SYMBOL] = self.walk_identity
+            self.functions[op.REAL_CONSTANT] = self.walk_identity
+            self.functions[op.BOOL_CONSTANT] = self.walk_identity
+            self.functions[op.INT_CONSTANT] = self.walk_identity
+
+
+            assert algorithm in ['fm', 'lw']
+            self.algorithm = algorithm
+
+            self.config = mathsat.msat_create_default_config("QF_LRA")
+            self.msat_env = mathsat.msat_create_env(self.config)
+            self.converter = MSatConverter(environment, self.msat_env)
+
+
+        def eliminate_quantifiers(self, formula):
+            """
+            Returns a quantifier-free equivalent formula of the given
+            formula
+            """
+            return self.walk(formula)
+
+
+        def exist_elim(self, variables, formula):
+            logic = get_logic(formula, self.env)
+            if not logic <= LRA:
+                raise NotImplementedError("MathSAT quantifier elimination only"\
+                                          " supports LRA (detected logic " \
+                                          "is: %s)" % str(logic))
+
+            fterm = self.converter.convert(formula)
+            tvars = [self.converter.convert(x) for x in variables]
+
+            algo = mathsat.MSAT_EXIST_ELIM_ALLSMT_FM
+            if self.algorithm == 'lw':
+                algo = mathsat.MSAT_EXIST_ELIM_VTS
+
+            res = mathsat.msat_exist_elim(self.msat_env, fterm, tvars, algo)
+
+            return self.converter.back(res)
+
+
+        def walk_forall(self, formula, args):
+            nf = self.env.formula_manager.Not(args[0])
+            ex = self.env.formula_manager.Exists(formula.quantifier_vars(), nf)
+            return self.walk(self.env.formula_manager.Not(ex))
+
+        def walk_exists(self, formula, args):
+            # Monolithic quantifier elimination
+            assert formula.is_exists()
+            variables = formula.quantifier_vars()
+            subf = formula.arg(0)
+            return self.exist_elim(variables, subf)
+
+
+    class MSatFMQuantifierEliminator(MSatQuantifierEliminator):
+        def __init__(self, env):
+            MSatQuantifierEliminator.__init__(self, env, 'fm')
+
+
+    class MSatLWQuantifierEliminator(MSatQuantifierEliminator):
+        def __init__(self, env):
+            MSatQuantifierEliminator.__init__(self, env, 'lw')

pysmt/solvers/z3.py

@@ -31,7 +31,9 @@
 from pysmt.exceptions import SolverReturnedUnknownResultError
 from pysmt.decorators import clear_pending_pop
 
-import pysmt.logics
+from pysmt.logics import LRA, LIA, PYSMT_LOGICS
+from pysmt.oracles import get_logic
+
 
 # patch z3api
 z3.is_ite = lambda x: z3.is_app_of(x, z3.Z3_OP_ITE)
@@ -65,7 +67,7 @@ def get_value(self, formula):
 
 class Z3Solver(Solver, SmtLibBasicSolver, SmtLibIgnoreMixin):
 
-    LOGICS = pysmt.logics.PYSMT_LOGICS
+    LOGICS = PYSMT_LOGICS
 
     def __init__(self, environment, logic, options=None):
         Solver.__init__(self,
@@ -380,6 +382,12 @@ def __init__(self, environment):
 
 
     def eliminate_quantifiers(self, formula):
+        logic = get_logic(formula, self.environment)
+        if not logic <= LRA and not logic <= LIA:
+            raise NotImplementedError("Z3 quantifier elimination only "\
+                                      "supports LRA or LIA without combination."\
+                                      "(detected logic is: %s)" % str(logic))
+
         simplifier = z3.Tactic('simplify')
         eliminator = z3.Tactic('qe')
 

pysmt/test/test_qe.py

@@ -19,14 +19,16 @@
 
 from pysmt.shortcuts import *
 from pysmt.typing import REAL, BOOL, INT
-from pysmt.test import TestCase
+from pysmt.test import TestCase, skipIfNoSolverForLogic
 from pysmt.exceptions import SolverReturnedUnknownResultError
-from pysmt.logics import LRA
+from pysmt.logics import LRA, QF_LIA
+
 
 class TestQE(TestCase):
 
     @unittest.skipIf(len(get_env().factory.all_qelims()) == 0,
                      "No QE available.")
+    @skipIfNoSolverForLogic(LRA)
     def test_qe_eq(self):
         qe = QuantifierEliminator()
 
@@ -68,6 +70,55 @@ def test_qe_z3(self):
         with self.assertRaises(NotImplementedError):
             qe.eliminate_quantifiers(f).simplify()
 
+    @unittest.skipIf('msat_fm' not in get_env().factory.all_qelims(),
+                     "MathSAT quantifier elimination is not available.")
+    def test_qe_msat_fm(self):
+        qe = QuantifierEliminator(name='msat_fm')
+        self._bool_example(qe)
+        self._real_example(qe)
+        self._alternation_bool_example(qe)
+        self._alternation_real_example(qe)
+
+        with self.assertRaises(NotImplementedError):
+            self._int_example(qe)
+
+        with self.assertRaises(NotImplementedError):
+            self._alternation_int_example(qe)
+
+        # Additional test for raising error on back conversion of
+        # quantified formulae
+        p, q = Symbol("p", INT), Symbol("q", INT)
+
+        f = ForAll([p], Exists([q], Equals(ToReal(p),
+                                           Plus(ToReal(q), ToReal(Int(1))))))
+        with self.assertRaises(NotImplementedError):
+            qe.eliminate_quantifiers(f).simplify()
+
+
+    @unittest.skipIf('msat_lw' not in get_env().factory.all_qelims(),
+                     "MathSAT quantifier elimination is not available.")
+    def test_qe_msat_lw(self):
+        qe = QuantifierEliminator(name='msat_lw')
+        self._bool_example(qe)
+        self._real_example(qe)
+        self._alternation_bool_example(qe)
+        self._alternation_real_example(qe)
+
+        with self.assertRaises(NotImplementedError):
+            self._int_example(qe)
+
+        with self.assertRaises(NotImplementedError):
+            self._alternation_int_example(qe)
+
+        # Additional test for raising error on back conversion of
+        # quantified formulae
+        p, q = Symbol("p", INT), Symbol("q", INT)
+
+        f = ForAll([p], Exists([q], Equals(ToReal(p),
+                                           Plus(ToReal(q), ToReal(Int(1))))))
+        with self.assertRaises(NotImplementedError):
+            qe.eliminate_quantifiers(f).simplify()
+
 
     def _bool_example(self, qe):
         # Bool Example

shippable.yml

@@ -68,6 +68,7 @@ before_script:
   - mkdir -p shippable/testresults
   - mkdir -p shippable/codecoverage
   - export PYTHONPATH="$PYTHONPATH:$TRAVIS_BUILD_DIR/.smt_solvers/mathsat-5.2.12-linux-x86_64/python:$TRAVIS_BUILD_DIR/.smt_solvers/mathsat-5.2.12-linux-x86_64/python/build/lib.linux-x86_64-$TRAVIS_PYTHON_VERSION"
+  - export PYTHONPATH="$PYTHONPATH:$TRAVIS_BUILD_DIR/.smt_solvers/mathsat-5.3.4-linux-x86_64/python:$TRAVIS_BUILD_DIR/.smt_solvers/mathsat-5.3.4-linux-x86_64/python/build/lib.linux-x86_64-$TRAVIS_PYTHON_VERSION"
   - export PYTHONPATH="$PYTHONPATH:$TRAVIS_BUILD_DIR/.smt_solvers/z3_bin/lib/python2.7/dist-packages"
   # We have 2 different paths for CVC4 1) if we compile 2) if we download the binary
   - export PYTHONPATH="$PYTHONPATH:$TRAVIS_BUILD_DIR/.smt_solvers/CVC4-68f22235a62f5276b206e9a6692a85001beb8d42/builds/src/bindings/python"