Repository: pysmt/pysmt
Pull request #72 (2015-04-14 12:25:00)

Quantifiler Elimination selector
In this PR we introduce a logic-based selection of the quantifier eliminators, analogously to the Solver case. In addition the factory code has been re-factored.

This addresses issues #16 and #71.  


Patch:
diff --git a/docs/CHANGES.rst b/docs/CHANGES.rst
index 82ed419..0ec94d8 100644
--- a/docs/CHANGES.rst
+++ b/docs/CHANGES.rst
@@ -18,6 +18,11 @@ General:
   solvers. Dedicated shortcuts (get_unsat_core and UnsatCoreSolver)
   have been added.
 
+* QuantifierEliminator and qelim shortcuts, as well as the respective
+  factory methods can now accept a 'logic' parameter that allows to
+  select a quantifier eliminator instance supporting a given logic
+  (analogously to what happens for solvers).
+
 
 
 0.2.4: 2015-03-15  -- PicoSAT
diff --git a/pysmt/factory.py b/pysmt/factory.py
index 2f92d1d..894ca53 100644
--- a/pysmt/factory.py
+++ b/pysmt/factory.py
@@ -26,17 +26,17 @@ particular solver.
 from functools import partial
 from six import iteritems
 
-from pysmt.exceptions import NoSolverAvailableError, SolverRedefinitionError
-from pysmt.logics import QF_UFLIRA
+from pysmt.exceptions import (NoSolverAvailableError, SolverRedefinitionError,
+                              NoLogicAvailableError)
+from pysmt.logics import QF_UFLIRA, LRA
 from pysmt.logics import AUTO as AUTO_LOGIC
 from pysmt.logics import most_generic_logic, get_closer_logic
 from pysmt.oracles import get_logic
 
-import pysmt.solvers.solver
-
 DEFAULT_SOLVER_PREFERENCE_LIST = ['msat', 'z3', 'cvc4', 'yices', 'picosat', 'bdd']
 DEFAULT_QELIM_PREFERENCE_LIST = ['z3', 'msat_fm', 'msat_lw']
 DEFAULT_LOGIC = QF_UFLIRA
+DEFAULT_QE_LOGIC = LRA
 
 class Factory(object):
 
@@ -45,7 +45,7 @@ class Factory(object):
                  qelim_preference_list=None):
         self.environment = environment
         self._all_solvers = None
-        self._unsat_core_solvers = None
+        self._all_unsat_core_solvers = None
         self._all_qelims = None
         self._generic_solvers = {}
 
@@ -57,6 +57,7 @@ class Factory(object):
             qelim_preference_list = DEFAULT_QELIM_PREFERENCE_LIST
         self.qelim_preference_list = qelim_preference_list
         self._default_logic = DEFAULT_LOGIC
+        self._default_qe_logic = DEFAULT_QE_LOGIC
 
         self._get_available_solvers()
         self._get_available_qe()
@@ -69,41 +70,17 @@ class Factory(object):
         if quantified is True:
             logic = self.default_logic.get_quantified_version
 
-        if name is not None:
-            if name in self._all_solvers:
-                if logic is None:
-                    SolverClass = self._all_solvers[name]
-                    logic = most_generic_logic(SolverClass.LOGICS)
-                else:
-                    if name in self.all_solvers(logic=logic):
-                        SolverClass = self._all_solvers[name]
-                    else:
-                        raise NoSolverAvailableError("Solver '%s' does not" \
-                                                     " support logic %s" %
-                                                     (name, logic))
-
-                closer_logic = get_closer_logic(SolverClass.LOGICS, logic)
-                return SolverClass(environment=self.environment,
-                                   logic=closer_logic,
-                                   user_options={"generate_models":True})
-            else:
-                raise NoSolverAvailableError("Solver %s is not available" % name)
-
-        if logic is None:
-            logic = self.default_logic
-
-        solvers = self.all_solvers(logic=logic)
+        SolverClass, closer_logic = \
+           self._get_solver_class(solver_list=self._all_solvers,
+                                  solver_type="Solver",
+                                  preference_list=self.solver_preference_list,
+                                  default_logic=self.default_logic,
+                                  name=name,
+                                  logic=logic)
 
-        if solvers is not None and len(solvers) > 0:
-            # Pick the first solver based on preference list
-            SolverClass = self.pick_favorite_solver(solvers)
-            closer_logic = get_closer_logic(SolverClass.LOGICS, logic)
-            return SolverClass(environment=self.environment,
-                               logic=closer_logic,
-                               user_options={"generate_models":True})
-        else:
-            raise NoSolverAvailableError("No solver is available for logic %s" %\
-                                         logic)
+        return SolverClass(environment=self.environment,
+                           logic=closer_logic,
+                           user_options={"generate_models" : True})
 
 
     def get_unsat_core_solver(self, quantified=False, name=None,
@@ -114,75 +91,84 @@ class Factory(object):
         if quantified is True:
             logic = self.default_logic.get_quantified_version
 
+        SolverClass, closer_logic = \
+           self._get_solver_class(solver_list=self._all_unsat_core_solvers,
+                                  solver_type="Solver supporting Unsat Cores",
+                                  preference_list=self.solver_preference_list,
+                                  default_logic=self.default_logic,
+                                  name=name,
+                                  logic=logic)
+
+        return SolverClass(environment=self.environment,
+                           logic=closer_logic,
+                           user_options={"generate_models" : True,
+                                         "unsat_cores_mode" : unsat_cores_mode})
+
+
+    def get_quantifier_eliminator(self, name=None, logic=None):
+        SolverClass, closer_logic = \
+           self._get_solver_class(solver_list=self._all_qelims,
+                                  solver_type="Quantifier Eliminator",
+                                  preference_list=self.qelim_preference_list,
+                                  default_logic=self.default_qe_logic,
+                                  name=name,
+                                  logic=logic)
+
+        return SolverClass(environment=self.environment,
+                           logic=closer_logic)
+
+
+    def _get_solver_class(self, solver_list, solver_type, preference_list,
+                          default_logic, name=None, logic=None):
+        if len(solver_list) == 0:
+            raise NoSolverAvailableError("No %s is available" % solver_type)
+
         if name is not None:
-            if name in self._unsat_core_solvers:
-                if logic is None:
-                    SolverClass = self._unsat_core_solvers[name]
+            if name not in solver_list:
+                raise NoSolverAvailableError("%s '%s' is not available" % \
+                                             (solver_type, name))
+
+            if logic is not None and \
+               name not in self._filter_solvers(solver_list, logic=logic):
+                raise NoSolverAvailableError("%s '%s' does not support logic %s"%
+                                             (solver_type, name, logic))
+
+            SolverClass = solver_list[name]
+            if logic is None:
+                try:
                     logic = most_generic_logic(SolverClass.LOGICS)
-                else:
-                    if name in self.all_unsat_core_solvers(logic=logic):
-                        SolverClass = self._unsat_core_solvers[name]
+                except NoLogicAvailableError:
+                    if default_logic in SolverClass.LOGICS:
+                        logic = default_logic
                     else:
-                        raise NoSolverAvailableError("Solver '%s' does not" \
-                                                     " support logic %s" %
-                                                     (name, logic))
-
-                closer_logic = get_closer_logic(SolverClass.LOGICS, logic)
-                return SolverClass(environment=self.environment,
-                                   logic=closer_logic,
-                                   user_options={"generate_models" : True,
-                                        "unsat_cores_mode" : unsat_cores_mode})
-            else:
-                raise NoSolverAvailableError("Solver %s has no support for " \
-                                             "unsat cores" % name)
+                        raise NoLogicAvailableError("Cannot automatically select a logic")
+
+            closer_logic = get_closer_logic(SolverClass.LOGICS, logic)
+
+            return SolverClass, closer_logic
 
         if logic is None:
-            logic = self.default_logic
+            logic = default_logic
 
-        solvers = self.all_unsat_core_solvers(logic=logic)
+        solvers = self._filter_solvers(solver_list, logic=logic)
 
         if solvers is not None and len(solvers) > 0:
             # Pick the first solver based on preference list
-            SolverClass = self.pick_favorite_solver(solvers)
+            SolverClass = self._pick_favorite(preference_list, solver_list, solvers)
             closer_logic = get_closer_logic(SolverClass.LOGICS, logic)
-            return SolverClass(environment=self.environment,
-                               logic=closer_logic,
-                               user_options={"generate_models" : True,
-                                        "unsat_cores_mode" : unsat_cores_mode})
-        else:
-            raise NoSolverAvailableError("No solver supporting unsat cores is" \
-                                         " available for logic %s" % logic)
-
+            return SolverClass, closer_logic
 
-
-    def get_quantifier_eliminator(self, name=None):
-        if len(self._all_qelims) == 0:
-            raise NoSolverAvailableError("No quantifier eliminator is available")
-
-        if name is None:
-            QElimClass = self.pick_favorite_qelim(self._all_qelims)
-        elif name in self._all_qelims:
-            QElimClass = self._all_qelims[name]
         else:
-            raise NoSolverAvailableError("No quantifier eliminator %s" % name)
+            raise NoSolverAvailableError("No %s is available for logic %s" %
+                                         (solver_type, logic))
 
-        return QElimClass(self.environment)
 
-
-    def pick_favorite_solver(self, solvers):
-        for candidate in self.solver_preference_list:
+    def _pick_favorite(self, preference_list, solver_list, solvers):
+        for candidate in preference_list:
             if candidate in solvers:
-                return self._all_solvers[candidate]
+                return solver_list[candidate]
         raise NoSolverAvailableError(
-            "Cannot find a matching solver in the preference list: %s "% solvers)
-
-
-    def pick_favorite_qelim(self, qelims):
-        for candidate in self.qelim_preference_list:
-            if candidate in qelims:
-                return self._all_qelims[candidate]
-        raise NoSolverAvailableError("Cannot find a matching quantifier " \
-                                     "eliminator in the preference list")
+            "Cannot find a matching solver in the preference list: %s " % solvers)
 
 
     def add_generic_solver(self, name, args, logics, unsat_core_support=False):
@@ -203,7 +189,7 @@ class Factory(object):
 
     def _get_available_solvers(self):
         self._all_solvers = {}
-        self._unsat_core_solvers = {}
+        self._all_unsat_core_solvers = {}
 
         try:
             from pysmt.solvers.z3 import Z3Solver
@@ -252,7 +238,7 @@ class Factory(object):
         for k,s in iteritems(self._all_solvers):
             try:
                 if s.UNSAT_CORE_SUPPORT:
-                    self._unsat_core_solvers[k] = s
+                    self._all_unsat_core_solvers[k] = s
             except AttributeError:
                 pass
 
@@ -295,8 +281,7 @@ class Factory(object):
         assert len(preference_list) > 0
         self.qelim_preference_list = preference_list
 
-
-    def all_solvers(self, logic=None):
+    def _filter_solvers(self, solver_list, logic=None):
         """
         Returns a dict <solver_name, solver_class> including all and only
         the solvers directly or indirectly supporting the given logic.
@@ -308,17 +293,45 @@ class Factory(object):
         """
         res = {}
         if logic is not None:
-            for s, v in iteritems(self._all_solvers):
+            for s, v in iteritems(solver_list):
                 for l in v.LOGICS:
                     if logic <= l:
                         res[s] = v
                         break
             return res
         else:
-            solvers = self._all_solvers
+            solvers = solver_list
 
         return solvers
 
+
+    def all_solvers(self, logic=None):
+        """
+        Returns a dict <solver_name, solver_class> including all and only
+        the solvers directly or indirectly supporting the given logic.
+        A solver supports a logic if either the given logic is
+        declared in the LOGICS class field or if a logic subsuming the
+        given logic is declared in the LOGICS class field.
+
+        If logic is None, the map will contain all the known solvers
+        """
+        return self._filter_solvers(self._all_solvers, logic=logic)
+
+
+    def all_quantifier_eliminators(self, logic=None):
+        """Returns a dict <qelim_name, qelim_class> including all and only the
+        quantifier eliminators directly or indirectly supporting the
+        given logic.  A qelim supports a logic if either the given
+        logic is declared in the LOGICS class field or if a logic
+        subsuming the given logic is declared in the LOGICS class
+        field.
+
+        If logic is None, the map will contain all the known
+        quantifier eliminators
+        """
+        return self._filter_solvers(self._all_qelims, logic=logic)
+
+
     def all_unsat_core_solvers(self, logic=None):
         """
         Returns a dict <solver_name, solver_class> including all and only
@@ -329,23 +342,10 @@ class Factory(object):
         declared in the LOGICS class field.
 
         If logic is None, the map will contain all the known solvers
-
         """
-        res = {}
-        if logic is not None:
-            for s, v in iteritems(self._unsat_core_solvers):
-                for l in v.LOGICS:
-                    if logic <= l:
-                        res[s] = v
-                        break
-            return res
-        else:
-            solvers = self._unsat_core_solvers
+        return self._filter_solvers(self._all_unsat_core_solvers, logic=logic)
 
-        return solvers
 
-    def all_qelims(self):
-        return self._all_qelims
 
     ##
     ## Wrappers: These functions are exported in shortcuts
@@ -363,8 +363,8 @@ class Factory(object):
                                           unsat_cores_mode=unsat_cores_mode)
 
 
-    def QuantifierEliminator(self, name=None):
-        return self.get_quantifier_eliminator(name=name)
+    def QuantifierEliminator(self, name=None, logic=None):
+        return self.get_quantifier_eliminator(name=name, logic=logic)
 
     def is_sat(self, formula, solver_name=None, logic=None):
         if logic == AUTO_LOGIC:
@@ -414,8 +414,11 @@ class Factory(object):
              as solver:
             return solver.is_unsat(formula)
 
-    def qelim(self, formula, solver_name=None):
-        with self.QuantifierEliminator(name=solver_name) as qe:
+    def qelim(self, formula, solver_name=None, logic=None):
+        if logic == AUTO_LOGIC:
+            logic = get_logic(formula, self.environment)
+
+        with self.QuantifierEliminator(name=solver_name, logic=logic) as qe:
             return qe.eliminate_quantifiers(formula)
 
     @property
@@ -425,3 +428,11 @@ class Factory(object):
     @default_logic.setter
     def default_logic(self, value):
         self._default_logic = value
+
+    @property
+    def default_qe_logic(self):
+        return self._default_qe_logic
+
+    @default_qe_logic.setter
+    def default_qe_logic(self, value):
+        self._default_qe_logic = value
diff --git a/pysmt/logics.py b/pysmt/logics.py
index ba75210..1257b6d 100644
--- a/pysmt/logics.py
+++ b/pysmt/logics.py
@@ -652,7 +652,7 @@ def most_generic_logic(logics):
     res = [ l for l in logics if all(l >= x for x in logics)]
 
     if len(res) != 1:
-        raise NoLogicAvailableError("Could not find the most generic"
+        raise NoLogicAvailableError("Could not find the most generic "
                                     "logic for %s." % str(logics))
     return res[0]
 
diff --git a/pysmt/shortcuts.py b/pysmt/shortcuts.py
index e57f4ea..14874aa 100644
--- a/pysmt/shortcuts.py
+++ b/pysmt/shortcuts.py
@@ -234,9 +234,9 @@ def UnsatCoreSolver(quantified=False, name=None, logic=None,
                                              logic=logic,
                                              unsat_cores_mode=unsat_cores_mode)
 
-def QuantifierEliminator(name=None):
+def QuantifierEliminator(name=None, logic=None):
     """Returns a quantifier eliminator"""
-    return get_env().factory.QuantifierEliminator(name=name)
+    return get_env().factory.QuantifierEliminator(name=name, logic=logic)
 
 def is_sat(formula, solver_name=None, logic=None):
     """ Returns whether a formula is satisfiable.
@@ -303,10 +303,17 @@ def is_unsat(formula, solver_name=None, logic=None):
                                 solver_name=solver_name,
                                 logic=logic)
 
-def qelim(formula, solver_name=None):
+def qelim(formula, solver_name=None, logic=None):
     """Performs quantifier elimination of the given formula."""
-    _qelim = get_env().factory.QuantifierEliminator(name=solver_name)
-    return _qelim.eliminate_quantifiers(formula)
+    env = get_env()
+    if formula not in env.formula_manager:
+        warnings.warn("Warning: Contextualizing formula during is_unsat")
+        formula = env.formula_manager.normalize(formula)
+
+    return env.factory.qelim(formula,
+                             solver_name=solver_name,
+                             logic=logic)
+
 
 
 def read_configuration(config_filename, environment=None):
diff --git a/pysmt/solvers/msat.py b/pysmt/solvers/msat.py
index 50571a6..1e3d221 100644
--- a/pysmt/solvers/msat.py
+++ b/pysmt/solvers/msat.py
@@ -683,7 +683,9 @@ class MSatConverter(Converter, DagWalker):
 if hasattr(mathsat, "MSAT_EXIST_ELIM_ALLSMT_FM"):
     class MSatQuantifierEliminator(QuantifierEliminator, IdentityDagWalker):
 
-        def __init__(self, environment, algorithm='fm'):
+        LOGICS = [LRA]
+
+        def __init__(self, environment, logic=None, algorithm='fm'):
             """Algorithm can be either 'fm' (for Fourier-Motzkin) or 'lw' (for
                Loos-Weisspfenning)"""
 
@@ -694,6 +696,7 @@ if hasattr(mathsat, "MSAT_EXIST_ELIM_ALLSMT_FM"):
             self.functions[op.BOOL_CONSTANT] = self.walk_identity
             self.functions[op.INT_CONSTANT] = self.walk_identity
 
+            self.logic = logic
 
             assert algorithm in ['fm', 'lw']
             self.algorithm = algorithm
@@ -744,10 +747,12 @@ if hasattr(mathsat, "MSAT_EXIST_ELIM_ALLSMT_FM"):
 
 
     class MSatFMQuantifierEliminator(MSatQuantifierEliminator):
-        def __init__(self, env):
-            MSatQuantifierEliminator.__init__(self, env, 'fm')
+        def __init__(self, environment, logic=None):
+            MSatQuantifierEliminator.__init__(self, environment,
+                                              logic=logic, algorithm='fm')
 
 
     class MSatLWQuantifierEliminator(MSatQuantifierEliminator):
-        def __init__(self, env):
-            MSatQuantifierEliminator.__init__(self, env, 'lw')
+        def __init__(self, environment, logic=None):
+            MSatQuantifierEliminator.__init__(self, environment,
+                                              logic=logic, algorithm='lw')
diff --git a/pysmt/solvers/z3.py b/pysmt/solvers/z3.py
index 3f8ba48..96c2c32 100644
--- a/pysmt/solvers/z3.py
+++ b/pysmt/solvers/z3.py
@@ -431,8 +431,11 @@ class Z3Converter(Converter, DagWalker):
 
 class Z3QuantifierEliminator(QuantifierEliminator):
 
-    def __init__(self, environment):
+    LOGICS = [LIA, LRA]
+
+    def __init__(self, environment, logic=None):
         self.environment = environment
+        self.logic = logic
         self.converter = Z3Converter(environment)
 
 


Test patch:
diff --git a/pysmt/test/__init__.py b/pysmt/test/__init__.py
index 04b930d..4e42e79 100644
--- a/pysmt/test/__init__.py
+++ b/pysmt/test/__init__.py
@@ -88,6 +88,21 @@ class skipIfSolverNotAvailable(object):
             return test_fun(*args, **kwargs)
         return wrapper
 
+class skipIfQENotAvailable(object):
+    """Skip a test if the given solver is not available."""
+
+    def __init__(self, qe):
+        self.qe = qe
+
+    def __call__(self, test_fun):
+        msg = "Quantifier Eliminator %s not available" % self.qe
+        cond = self.qe not in get_env().factory.all_quantifier_eliminators()
+        @unittest.skipIf(cond, msg)
+        @wraps(test_fun)
+        def wrapper(*args, **kwargs):
+            return test_fun(*args, **kwargs)
+        return wrapper
+
 
 class skipIfNoSolverForLogic(object):
     """Skip a test if there is no solver for the given logic."""
@@ -119,3 +134,19 @@ class skipIfNoUnsatCoreSolverForLogic(object):
         def wrapper(*args, **kwargs):
             return test_fun(*args, **kwargs)
         return wrapper
+
+
+class skipIfNoQEForLogic(object):
+    """Skip a test if there is no quantifier eliminator for the given logic."""
+
+    def __init__(self, logic):
+        self.logic = logic
+
+    def __call__(self, test_fun):
+        msg = "Quantifier Eliminator for %s not available" % self.logic
+        cond = len(get_env().factory.all_quantifier_eliminators(logic=self.logic)) == 0
+        @unittest.skipIf(cond, msg)
+        @wraps(test_fun)
+        def wrapper(*args, **kwargs):
+            return test_fun(*args, **kwargs)
+        return wrapper
diff --git a/pysmt/test/test_env.py b/pysmt/test/test_env.py
index b634860..a1b0d58 100644
--- a/pysmt/test/test_env.py
+++ b/pysmt/test/test_env.py
@@ -101,11 +101,11 @@ class TestEnvironment(TestCase):
         with self.assertRaises(NoSolverAvailableError):
             factory.get_solver()
 
-        for qelim_name in factory.all_qelims():
+        for qelim_name in factory.all_quantifier_eliminators():
             factory.set_qelim_preference_list([qelim_name])
             self.assertEqual(factory.qelim_preference_list, [qelim_name])
             qelim = factory.get_quantifier_eliminator()
-            self.assertTrue(isinstance(qelim, factory.all_qelims()[qelim_name]))
+            self.assertTrue(isinstance(qelim, factory.all_quantifier_eliminators()[qelim_name]))
 
         factory.set_qelim_preference_list(['nosolver'])
         with self.assertRaises(NoSolverAvailableError):
diff --git a/pysmt/test/test_qe.py b/pysmt/test/test_qe.py
index 48e5e36..a081e0b 100644
--- a/pysmt/test/test_qe.py
+++ b/pysmt/test/test_qe.py
@@ -19,18 +19,19 @@ import unittest
 
 from pysmt.shortcuts import *
 from pysmt.typing import REAL, BOOL, INT
-from pysmt.test import TestCase, skipIfNoSolverForLogic
-from pysmt.exceptions import SolverReturnedUnknownResultError
-from pysmt.logics import LRA, QF_LIA
+from pysmt.test import (TestCase, skipIfNoSolverForLogic, skipIfNoQEForLogic,
+                        skipIfQENotAvailable)
+from pysmt.exceptions import (SolverReturnedUnknownResultError, \
+                              NoSolverAvailableError)
+from pysmt.logics import LRA, LIA, UFLIRA
 
 
 class TestQE(TestCase):
 
-    @unittest.skipIf(len(get_env().factory.all_qelims()) == 0,
-                     "No QE available.")
     @skipIfNoSolverForLogic(LRA)
+    @skipIfNoQEForLogic(LRA)
     def test_qe_eq(self):
-        qe = QuantifierEliminator()
+        qe = QuantifierEliminator(logic=LRA)
 
         varA = Symbol("A", BOOL)
         varB = Symbol("B", BOOL)
@@ -50,9 +51,22 @@ class TestQE(TestCase):
         except SolverReturnedUnknownResultError:
             pass
 
+    def test_selection(self):
+        with self.assertRaises(NoSolverAvailableError):
+            QuantifierEliminator(logic=UFLIRA)
 
-    @unittest.skipIf('z3' not in get_env().factory.all_qelims(),
-                     "Z3 is not available.")
+        with self.assertRaises(NoSolverAvailableError):
+            QuantifierEliminator(name="nonexistent")
+
+        # MathSAT QE does not support LIA
+        with self.assertRaises(NoSolverAvailableError):
+            QuantifierEliminator(name="msat", logic=LIA)
+
+    @skipIfNoQEForLogic(LRA)
+    def test_selection_lra(self):
+        QuantifierEliminator(logic=LRA)
+
+    @skipIfQENotAvailable('z3')
     def test_qe_z3(self):
         qe = QuantifierEliminator(name='z3')
         self._bool_example(qe)
@@ -70,8 +84,8 @@ class TestQE(TestCase):
         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.")
+
+    @skipIfQENotAvailable('msat_fm')
     def test_qe_msat_fm(self):
         qe = QuantifierEliminator(name='msat_fm')
         self._bool_example(qe)
@@ -95,8 +109,7 @@ class TestQE(TestCase):
             qe.eliminate_quantifiers(f).simplify()
 
 
-    @unittest.skipIf('msat_lw' not in get_env().factory.all_qelims(),
-                     "MathSAT quantifier elimination is not available.")
+    @skipIfQENotAvailable('msat_lw')
     def test_qe_msat_lw(self):
         qe = QuantifierEliminator(name='msat_lw')
         self._bool_example(qe)