Merge pull request #41 from pysmt/factory_get_logic_clean

Using get_logic oracle in shortcuts and defining default for Factory

docs/CHANGES.rst

@@ -8,6 +8,16 @@ General:
 
 * install.py: script to automate the installation of supported
   solvers.
+* get_logic() Oracle: Detects the logic used in a formula. This is now
+  automatically used in _is_sat()_, _is_unsat()_, _is_valid()_, and
+  _get_model()_.
+
+Backwards Incompatible Changes:
+
+* The default logic for Factory.get_solver() is now the most generic
+  *quantifier free* logic supported by pySMT (currently,
+  QF_UFLIRA). Previously it was UFLIRA, but this was due to a bug in
+  the logic of get_solver().
 
 * Expressions: Added Min/Max operators.
 

pysmt/factory.py

@@ -23,15 +23,17 @@
 particular solver.
 """
 
-import warnings
 from functools import partial
 
 from pysmt.exceptions import NoSolverAvailableError, SolverRedefinitionError
-from pysmt.logics import PYSMT_LOGICS, most_generic_logic, get_closer_logic
+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
 
 DEFAULT_SOLVER_PREFERENCE_LIST = ['msat', 'z3', 'cvc4', 'yices', 'bdd']
 DEFAULT_QELIM_PREFERENCE_LIST = ['z3']
-
+DEFAULT_LOGIC = QF_UFLIRA
 
 class Factory(object):
 
@@ -50,21 +52,18 @@ def __init__(self, environment,
         if qelim_preference_list is None:
             qelim_preference_list = DEFAULT_QELIM_PREFERENCE_LIST
         self.qelim_preference_list = qelim_preference_list
+        self._default_logic = DEFAULT_LOGIC
 
         self._get_available_solvers()
         self._get_available_qe()
 
 
     def get_solver(self, quantified=False, name=None, logic=None):
         assert quantified is False or logic is None, \
-            "Cannot specify both quantified and logic"
+            "Cannot specify both quantified and logic."
 
         if quantified is True:
-            warnings.warn("Keyword 'quantified' in get_solver is deprecated" \
-                          ", use 'logic=UFLIRA' instead",
-                          DeprecationWarning)
-            quantified = False
-            logic = most_generic_logic(PYSMT_LOGICS)
+            logic = self.default_logic.get_quantified_version
 
         if name is not None:
             if name in self._all_solvers:
@@ -87,7 +86,7 @@ def get_solver(self, quantified=False, name=None, logic=None):
                 raise NoSolverAvailableError("Solver %s is not available" % name)
 
         if logic is None:
-            logic = most_generic_logic(PYSMT_LOGICS)
+            logic = self.default_logic
 
         solvers = self.all_solvers(logic=logic)
 
@@ -257,13 +256,17 @@ def Solver(self, quantified=False, name=None, logic=None):
     def QuantifierEliminator(self, name=None):
         return self.get_quantifier_eliminator(name=name)
 
-    def is_sat(self, formula, quantified=None, solver_name=None, logic=None):
-        with self.Solver(quantified=quantified, name=solver_name, logic=logic) \
+    def is_sat(self, formula, solver_name=None, logic=None):
+        if logic == AUTO_LOGIC:
+            logic = get_logic(formula, self.environment)
+        with self.Solver(name=solver_name, logic=logic) \
              as solver:
             return solver.is_sat(formula)
 
-    def get_model(self, formula, quantified=None, solver_name=None, logic=None):
-        with self.Solver(quantified=quantified, name=solver_name, logic=logic) \
+    def get_model(self, formula, solver_name=None, logic=None):
+        if logic == AUTO_LOGIC:
+            logic = get_logic(formula, self.environment)
+        with self.Solver(name=solver_name, logic=logic) \
              as solver:
             solver.add_assertion(formula)
             check = solver.solve()
@@ -272,16 +275,28 @@ def get_model(self, formula, quantified=None, solver_name=None, logic=None):
                 retval = solver.get_model()
             return retval
 
-    def is_valid(self, formula, quantified=False, solver_name=None, logic=None):
-        with self.Solver(quantified=quantified, name=solver_name, logic=logic) \
+    def is_valid(self, formula, solver_name=None, logic=None):
+        if logic == AUTO_LOGIC:
+            logic = get_logic(formula, self.environment)
+        with self.Solver(name=solver_name, logic=logic) \
              as solver:
             return solver.is_valid(formula)
 
-    def is_unsat(self, formula, quantified=False, solver_name=None, logic=None):
-        with self.Solver(quantified=quantified, name=solver_name, logic=logic) \
+    def is_unsat(self, formula, solver_name=None, logic=None):
+        if logic == AUTO_LOGIC:
+            logic = get_logic(formula, self.environment)
+        with self.Solver(name=solver_name, logic=logic) \
              as solver:
             return solver.is_unsat(formula)
 
     def qelim(self, formula, solver_name=None):
         with self.QuantifierEliminator(name=solver_name) as qe:
             return qe.eliminate_quantifiers(formula)
+
+    @property
+    def default_logic(self):
+        return self._default_logic
+
+    @default_logic.setter
+    def default_logic(self, value):
+        self._default_logic = value

pysmt/logics.py

@@ -206,7 +206,14 @@ def __init__(self, name, description,
 
         return
 
-
+    def get_quantified_version(self):
+        """Returns the quantified version of logic."""
+        if self.quantifier_free:
+            return self
+        target_logic = Logic(name="", description="",
+                             quantifier_free=False,
+                             theory=self.theory)
+        return get_closer_pysmt_logic(target_logic)
 
     def __str__(self):
         return self.name
@@ -527,6 +534,8 @@ def __gt__(self, other):
               linear=False,
               uninterpreted=True)
 
+AUTO = Logic(name="Auto",
+             description="Special logic used to indicate that the logic to be used depends on the formula.")
 
 SMTLIB2_LOGICS = [ AUFLIA,
                    AUFLIRA,

pysmt/oracles.py

@@ -172,8 +172,9 @@ def get_theory(self, formula):
 # EOC TheoryOracle
 
 
-def get_logic(formula):
-    env = pysmt.shortcuts.get_env()
+def get_logic(formula, env=None):
+    if env is None:
+        env = pysmt.shortcuts.get_env()
     # Get Quantifier Information
     qf = env.qfo.is_qf(formula)
     theory = env.theoryo.get_theory(formula)

pysmt/shortcuts.py

@@ -226,14 +226,11 @@ def QuantifierEliminator(name=None):
     """Returns a quantifier eliminator"""
     return get_env().factory.QuantifierEliminator(name=name)
 
-def is_sat(formula, quantified=False, solver_name=None, logic=None):
+def is_sat(formula, solver_name=None, logic=None):
     """ Returns whether a formula is satisfiable.
 
     :param formula: The formula to check satisfiability
     :type  formula: FNode
-    :param quantified: A boolean indicating whether the formula is
-                       quantified (this will influence the choice of
-                       the solver.
     :param solver_name: Specify the name of the solver to be used.
     :param logic: Specify the logic that is going to be used.
     :returns: Whether the formula is SAT or UNSAT.
@@ -245,11 +242,10 @@ def is_sat(formula, quantified=False, solver_name=None, logic=None):
         formula = env.formula_manager.normalize(formula)
 
     return env.factory.is_sat(formula,
-                              quantified=quantified,
                               solver_name=solver_name,
                               logic=logic)
 
-def get_model(formula, quantified=False, solver_name=None, logic=None):
+def get_model(formula, solver_name=None, logic=None):
     """ Similar to :py:func:`is_sat` but returns a model if the formula is
     satisfiable, otherwise None."""
     env = get_env()
@@ -258,31 +254,28 @@ def get_model(formula, quantified=False, solver_name=None, logic=None):
         formula = env.formula_manager.normalize(formula)
 
     return env.factory.get_model(formula,
-                                 quantified=quantified,
                                  solver_name=solver_name,
                                  logic=logic)
 
-def is_valid(formula, quantified=False, solver_name=None, logic=None):
+def is_valid(formula, solver_name=None, logic=None):
     """Similar to :py:func:`is_sat` but checks validity."""
     env = get_env()
     if formula not in env.formula_manager:
         warnings.warn("Warning: Contextualizing formula during is_valid")
         formula = env.formula_manager.normalize(formula)
 
     return env.factory.is_valid(formula,
-                                quantified=quantified,
                                 solver_name=solver_name,
                                 logic=logic)
 
-def is_unsat(formula, quantified=False, solver_name=None, logic=None):
+def is_unsat(formula, solver_name=None, logic=None):
     """Similar to :py:func:`is_sat` but checks unsatisfiability."""
     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.is_unsat(formula,
-                                quantified=quantified,
                                 solver_name=solver_name,
                                 logic=logic)
 

pysmt/test/test_solving.py

@@ -21,11 +21,12 @@
 from pysmt.shortcuts import Bool, TRUE, Real, LE, FALSE, Or, Equals
 from pysmt.shortcuts import Solver
 from pysmt.shortcuts import is_sat, is_valid, get_env, get_model
+from pysmt.shortcuts import get_env
 from pysmt.typing import BOOL, REAL, FunctionType
 from pysmt.test import TestCase, skipIfSolverNotAvailable, skipIfNoSolverForLogic
 from pysmt.test.examples import get_example_formulae
 from pysmt.exceptions import SolverReturnedUnknownResultError, InternalSolverError
-from pysmt.logics import QF_UFLIRA, QF_BOOL, QF_LRA
+from pysmt.logics import QF_UFLIRA, QF_BOOL, QF_LRA, AUTO
 
 class TestBasic(TestCase):
 
@@ -62,6 +63,31 @@ def test_is_sat(self):
             res = is_sat(g, solver_name=solver)
             self.assertFalse(res, "Formula was expected to be UNSAT")
 
+    # This test works only if is_sat requests QF_BOOL as logic, since
+    # that is the only logic handled by BDDs
+    @skipIfSolverNotAvailable("bdd")
+    def test_get_logic_in_is_sat(self):
+        varA = Symbol("A", BOOL)
+        varB = Symbol("B", BOOL)
+
+        f = And(varA, Not(varB))
+        res = is_sat(f, logic=AUTO)
+        self.assertTrue(res)
+
+    @skipIfSolverNotAvailable("bdd")
+    def test_default_logic_in_is_sat(self):
+        factory = get_env().factory
+        factory.default_logic = QF_BOOL
+
+        self.assertEquals(factory.default_logic, QF_BOOL)
+        varA = Symbol("A", BOOL)
+        varB = Symbol("B", BOOL)
+
+        f = And(varA, Not(varB))
+        res = is_sat(f)
+        self.assertTrue(res)
+
+
     @skipIfNoSolverForLogic(QF_BOOL)
     def test_get_model_unsat(self):
         varA = Symbol("A", BOOL)