Repository: pysmt/pysmt
Pull request #74 (2015-04-16 12:59:32)

Added support for picosat assumptions
This solves #69 


Patch:
diff --git a/docs/CHANGES.rst b/docs/CHANGES.rst
index 0ec94d8..82ed419 100644
--- a/docs/CHANGES.rst
+++ b/docs/CHANGES.rst
@@ -18,11 +18,6 @@ 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 894ca53..2f92d1d 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,
-                              NoLogicAvailableError)
-from pysmt.logics import QF_UFLIRA, LRA
+from pysmt.exceptions import NoSolverAvailableError, SolverRedefinitionError
+from pysmt.logics import QF_UFLIRA
 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._all_unsat_core_solvers = None
+        self._unsat_core_solvers = None
         self._all_qelims = None
         self._generic_solvers = {}
 
@@ -57,7 +57,6 @@ 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()
@@ -70,17 +69,41 @@ 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_solvers,
-                                  solver_type="Solver",
-                                  preference_list=self.solver_preference_list,
-                                  default_logic=self.default_logic,
-                                  name=name,
-                                  logic=logic)
+        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)
 
-        return SolverClass(environment=self.environment,
-                           logic=closer_logic,
-                           user_options={"generate_models" : True})
+        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)
 
 
     def get_unsat_core_solver(self, quantified=False, name=None,
@@ -91,84 +114,75 @@ 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 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:
+            if name in self._unsat_core_solvers:
+                if logic is None:
+                    SolverClass = self._unsat_core_solvers[name]
                     logic = most_generic_logic(SolverClass.LOGICS)
-                except NoLogicAvailableError:
-                    if default_logic in SolverClass.LOGICS:
-                        logic = default_logic
+                else:
+                    if name in self.all_unsat_core_solvers(logic=logic):
+                        SolverClass = self._unsat_core_solvers[name]
                     else:
-                        raise NoLogicAvailableError("Cannot automatically select a logic")
-
-            closer_logic = get_closer_logic(SolverClass.LOGICS, logic)
-
-            return SolverClass, closer_logic
+                        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)
 
         if logic is None:
-            logic = default_logic
+            logic = self.default_logic
 
-        solvers = self._filter_solvers(solver_list, logic=logic)
+        solvers = self.all_unsat_core_solvers(logic=logic)
 
         if solvers is not None and len(solvers) > 0:
             # Pick the first solver based on preference list
-            SolverClass = self._pick_favorite(preference_list, solver_list, solvers)
+            SolverClass = self.pick_favorite_solver(solvers)
             closer_logic = get_closer_logic(SolverClass.LOGICS, logic)
-            return SolverClass, closer_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)
+
 
+
+    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 %s is available for logic %s" %
-                                         (solver_type, logic))
+            raise NoSolverAvailableError("No quantifier eliminator %s" % name)
 
+        return QElimClass(self.environment)
 
-    def _pick_favorite(self, preference_list, solver_list, solvers):
-        for candidate in preference_list:
+
+    def pick_favorite_solver(self, solvers):
+        for candidate in self.solver_preference_list:
             if candidate in solvers:
-                return solver_list[candidate]
+                return self._all_solvers[candidate]
         raise NoSolverAvailableError(
-            "Cannot find a matching solver in the preference list: %s " % solvers)
+            "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")
 
 
     def add_generic_solver(self, name, args, logics, unsat_core_support=False):
@@ -189,7 +203,7 @@ class Factory(object):
 
     def _get_available_solvers(self):
         self._all_solvers = {}
-        self._all_unsat_core_solvers = {}
+        self._unsat_core_solvers = {}
 
         try:
             from pysmt.solvers.z3 import Z3Solver
@@ -238,7 +252,7 @@ class Factory(object):
         for k,s in iteritems(self._all_solvers):
             try:
                 if s.UNSAT_CORE_SUPPORT:
-                    self._all_unsat_core_solvers[k] = s
+                    self._unsat_core_solvers[k] = s
             except AttributeError:
                 pass
 
@@ -281,7 +295,8 @@ class Factory(object):
         assert len(preference_list) > 0
         self.qelim_preference_list = preference_list
 
-    def _filter_solvers(self, solver_list, logic=None):
+
+    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.
@@ -293,45 +308,17 @@ class Factory(object):
         """
         res = {}
         if logic is not None:
-            for s, v in iteritems(solver_list):
+            for s, v in iteritems(self._all_solvers):
                 for l in v.LOGICS:
                     if logic <= l:
                         res[s] = v
                         break
             return res
         else:
-            solvers = solver_list
+            solvers = self._all_solvers
 
         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
@@ -342,10 +329,23 @@ class Factory(object):
         declared in the LOGICS class field.
 
         If logic is None, the map will contain all the known solvers
+
         """
-        return self._filter_solvers(self._all_unsat_core_solvers, logic=logic)
+        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 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, logic=None):
-        return self.get_quantifier_eliminator(name=name, logic=logic)
+    def QuantifierEliminator(self, name=None):
+        return self.get_quantifier_eliminator(name=name)
 
     def is_sat(self, formula, solver_name=None, logic=None):
         if logic == AUTO_LOGIC:
@@ -414,11 +414,8 @@ class Factory(object):
              as solver:
             return solver.is_unsat(formula)
 
-    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:
+    def qelim(self, formula, solver_name=None):
+        with self.QuantifierEliminator(name=solver_name) as qe:
             return qe.eliminate_quantifiers(formula)
 
     @property
@@ -428,11 +425,3 @@ 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 1257b6d..ba75210 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 14874aa..e57f4ea 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, logic=None):
+def QuantifierEliminator(name=None):
     """Returns a quantifier eliminator"""
-    return get_env().factory.QuantifierEliminator(name=name, logic=logic)
+    return get_env().factory.QuantifierEliminator(name=name)
 
 def is_sat(formula, solver_name=None, logic=None):
     """ Returns whether a formula is satisfiable.
@@ -303,17 +303,10 @@ def is_unsat(formula, solver_name=None, logic=None):
                                 solver_name=solver_name,
                                 logic=logic)
 
-def qelim(formula, solver_name=None, logic=None):
+def qelim(formula, solver_name=None):
     """Performs quantifier elimination of the given 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)
-
+    _qelim = get_env().factory.QuantifierEliminator(name=solver_name)
+    return _qelim.eliminate_quantifiers(formula)
 
 
 def read_configuration(config_filename, environment=None):
diff --git a/pysmt/solvers/msat.py b/pysmt/solvers/msat.py
index 1e3d221..50571a6 100644
--- a/pysmt/solvers/msat.py
+++ b/pysmt/solvers/msat.py
@@ -683,9 +683,7 @@ class MSatConverter(Converter, DagWalker):
 if hasattr(mathsat, "MSAT_EXIST_ELIM_ALLSMT_FM"):
     class MSatQuantifierEliminator(QuantifierEliminator, IdentityDagWalker):
 
-        LOGICS = [LRA]
-
-        def __init__(self, environment, logic=None, algorithm='fm'):
+        def __init__(self, environment, algorithm='fm'):
             """Algorithm can be either 'fm' (for Fourier-Motzkin) or 'lw' (for
                Loos-Weisspfenning)"""
 
@@ -696,7 +694,6 @@ 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
@@ -747,12 +744,10 @@ if hasattr(mathsat, "MSAT_EXIST_ELIM_ALLSMT_FM"):
 
 
     class MSatFMQuantifierEliminator(MSatQuantifierEliminator):
-        def __init__(self, environment, logic=None):
-            MSatQuantifierEliminator.__init__(self, environment,
-                                              logic=logic, algorithm='fm')
+        def __init__(self, env):
+            MSatQuantifierEliminator.__init__(self, env, 'fm')
 
 
     class MSatLWQuantifierEliminator(MSatQuantifierEliminator):
-        def __init__(self, environment, logic=None):
-            MSatQuantifierEliminator.__init__(self, environment,
-                                              logic=logic, algorithm='lw')
+        def __init__(self, env):
+            MSatQuantifierEliminator.__init__(self, env, 'lw')
diff --git a/pysmt/solvers/pico.py b/pysmt/solvers/pico.py
index 8bc3a1e..c082b9e 100644
--- a/pysmt/solvers/pico.py
+++ b/pysmt/solvers/pico.py
@@ -69,27 +69,48 @@ class PicosatSolver(Solver):
         # no need to declare variables
         pass
 
+    def _get_pico_lit(self, lit):
+        mult = 1
+        var = lit
+        if lit.is_not():
+            mult = -1
+            var = lit.arg(0)
+
+        vid = self._get_var_id(var)
+        return vid * mult
+
+
     @clear_pending_pop
     def add_assertion(self, formula, named=None):
         cnf = self.cnfizer.convert(formula)
+        self._add_cnf_assertion(cnf)
+
+    def _add_cnf_assertion(self, cnf):
         for clause in cnf:
             for lit in clause:
-                mult = 1
-                var = lit
-                if lit.is_not():
-                    mult = -1
-                    var = lit.arg(0)
-
-                vid = self._get_var_id(var)
-                picosat.picosat_add(self.pico, mult * vid)
+                v = self._get_pico_lit(lit)
+                picosat.picosat_add(self.pico, v)
             picosat.picosat_add(self.pico, 0)
 
     @clear_pending_pop
     def solve(self, assumptions=None):
         if assumptions is not None:
-            self.push()
-            self.add_assertion(self.mgr.And(assumptions))
-            self.pending_pop = True
+            cnf = []
+            for a in assumptions:
+                cnf += self.cnfizer.convert(a)
+
+            missing = []
+            for clause in cnf:
+                if len(clause) == 1:
+                    v = self._get_pico_lit(next(iter(clause)))
+                    picosat.picosat_assume(self.pico, v)
+                else:
+                    missing.append(clause)
+
+            if len(missing) > 0:
+                self.push()
+                self._add_cnf_assertion(missing)
+                self.pending_pop = True
 
         res = picosat.picosat_sat(self.pico, -1)
         if res == picosat.PICOSAT_SATISFIABLE:
diff --git a/pysmt/solvers/z3.py b/pysmt/solvers/z3.py
index 96c2c32..3f8ba48 100644
--- a/pysmt/solvers/z3.py
+++ b/pysmt/solvers/z3.py
@@ -431,11 +431,8 @@ class Z3Converter(Converter, DagWalker):
 
 class Z3QuantifierEliminator(QuantifierEliminator):
 
-    LOGICS = [LIA, LRA]
-
-    def __init__(self, environment, logic=None):
+    def __init__(self, environment):
         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 4e42e79..04b930d 100644
--- a/pysmt/test/__init__.py
+++ b/pysmt/test/__init__.py
@@ -88,21 +88,6 @@ 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."""
@@ -134,19 +119,3 @@ 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 a1b0d58..b634860 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_quantifier_eliminators():
+        for qelim_name in factory.all_qelims():
             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_quantifier_eliminators()[qelim_name]))
+            self.assertTrue(isinstance(qelim, factory.all_qelims()[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 a081e0b..48e5e36 100644
--- a/pysmt/test/test_qe.py
+++ b/pysmt/test/test_qe.py
@@ -19,19 +19,18 @@ import unittest
 
 from pysmt.shortcuts import *
 from pysmt.typing import REAL, BOOL, INT
-from pysmt.test import (TestCase, skipIfNoSolverForLogic, skipIfNoQEForLogic,
-                        skipIfQENotAvailable)
-from pysmt.exceptions import (SolverReturnedUnknownResultError, \
-                              NoSolverAvailableError)
-from pysmt.logics import LRA, LIA, UFLIRA
+from pysmt.test import TestCase, skipIfNoSolverForLogic
+from pysmt.exceptions import SolverReturnedUnknownResultError
+from pysmt.logics import LRA, QF_LIA
 
 
 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(logic=LRA)
+        qe = QuantifierEliminator()
 
         varA = Symbol("A", BOOL)
         varB = Symbol("B", BOOL)
@@ -51,22 +50,9 @@ class TestQE(TestCase):
         except SolverReturnedUnknownResultError:
             pass
 
-    def test_selection(self):
-        with self.assertRaises(NoSolverAvailableError):
-            QuantifierEliminator(logic=UFLIRA)
 
-        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')
+    @unittest.skipIf('z3' not in get_env().factory.all_qelims(),
+                     "Z3 is not available.")
     def test_qe_z3(self):
         qe = QuantifierEliminator(name='z3')
         self._bool_example(qe)
@@ -84,8 +70,8 @@ class TestQE(TestCase):
         with self.assertRaises(NotImplementedError):
             qe.eliminate_quantifiers(f).simplify()
 
-
-    @skipIfQENotAvailable('msat_fm')
+    @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)
@@ -109,7 +95,8 @@ class TestQE(TestCase):
             qe.eliminate_quantifiers(f).simplify()
 
 
-    @skipIfQENotAvailable('msat_lw')
+    @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)