Merge pull request #68 from pysmt/unsat_cores

Added unsat cores support 

Currently only for MathSAT and Z3

docs/CHANGES.rst

@@ -14,6 +14,11 @@ General:
   (msat_lw) uses Loos-Weisspfenning elimination (aka Virtual
   Substitution)
 
+* Added support for unsat core extraction using the MathSAT and the Z3
+  solvers. Dedicated shortcuts (get_unsat_core and UnsatCoreSolver)
+  have been added.
+
+
 
 0.2.4: 2015-03-15  -- PicoSAT
 -----------------------------

pysmt/exceptions.py

@@ -53,3 +53,17 @@ class SolverRedefinitionError(Exception):
     """Exception representing errors caused by multiple defintion of solvers
        having the same name."""
     pass
+
+class SolverNotConfiguredForUnsatCoresError(Exception):
+    """
+    Exception raised if a solver not configured for generating unsat
+    cores is required to produce a core.
+    """
+    pass
+
+class SolverStatusError(Exception):
+    """
+    Exception raised if a method requiring a specific solver status is
+    incorrectly called in the wrong status.
+    """
+    pass

pysmt/factory.py

@@ -32,6 +32,8 @@
 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
@@ -43,6 +45,7 @@ def __init__(self, environment,
                  qelim_preference_list=None):
         self.environment = environment
         self._all_solvers = None
+        self._unsat_core_solvers = None
         self._all_qelims = None
         self._generic_solvers = {}
 
@@ -82,7 +85,7 @@ def get_solver(self, quantified=False, name=None, logic=None):
                 closer_logic = get_closer_logic(SolverClass.LOGICS, logic)
                 return SolverClass(environment=self.environment,
                                    logic=closer_logic,
-                                   options=None)
+                                   user_options={"generate_models":True})
             else:
                 raise NoSolverAvailableError("Solver %s is not available" % name)
 
@@ -97,12 +100,60 @@ def get_solver(self, quantified=False, name=None, logic=None):
             closer_logic = get_closer_logic(SolverClass.LOGICS, logic)
             return SolverClass(environment=self.environment,
                                logic=closer_logic,
-                               options=None)
+                               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,
+                              logic=None, unsat_cores_mode="all"):
+        assert quantified is False or logic is None, \
+            "Cannot specify both quantified and logic."
+
+        if quantified is True:
+            logic = self.default_logic.get_quantified_version
+
+        if name is not None:
+            if name in self._unsat_core_solvers:
+                if logic is None:
+                    SolverClass = self._unsat_core_solvers[name]
+                    logic = most_generic_logic(SolverClass.LOGICS)
+                else:
+                    if name in self.all_unsat_core_solvers(logic=logic):
+                        SolverClass = self._unsat_core_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,
+                                        "unsat_cores_mode" : unsat_cores_mode})
+            else:
+                raise NoSolverAvailableError("Solver %s has no support for " \
+                                             "unsat cores" % name)
+
+        if logic is None:
+            logic = self.default_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_solver(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)
+
+
 
     def get_quantifier_eliminator(self, name=None):
         if len(self._all_qelims) == 0:
@@ -134,13 +185,14 @@ def pick_favorite_qelim(self, qelims):
                                      "eliminator in the preference list")
 
 
-    def add_generic_solver(self, name, args, logics):
+    def add_generic_solver(self, name, args, logics, unsat_core_support=False):
         from pysmt.smtlib.solver import SmtLibSolver
         if name in self._all_solvers:
             raise SolverRedefinitionError("Solver %s already defined" % name)
         self._generic_solvers[name] = (args, logics)
         solver = partial(SmtLibSolver, args)
         solver.LOGICS = logics
+        solver.UNSAT_CORE_SUPPORT = unsat_core_support
         self._all_solvers[name] = solver
 
     def is_generic_solver(self, name):
@@ -151,6 +203,7 @@ def get_generic_solver_info(self, name):
 
     def _get_available_solvers(self):
         self._all_solvers = {}
+        self._unsat_core_solvers = {}
 
         try:
             from pysmt.solvers.z3 import Z3Solver
@@ -196,6 +249,13 @@ def _get_available_solvers(self):
             pass
 
 
+        for k,s in iteritems(self._all_solvers):
+            try:
+                if s.UNSAT_CORE_SUPPORT:
+                    self._unsat_core_solvers[k] = s
+            except AttributeError:
+                pass
+
 
     def _get_available_qe(self):
         self._all_qelims = {}
@@ -259,6 +319,31 @@ def all_solvers(self, logic=None):
 
         return solvers
 
+    def all_unsat_core_solvers(self, logic=None):
+        """
+        Returns a dict <solver_name, solver_class> including all and only
+        the solvers supporting unsat core extraction and 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
+
+        """
+        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
 
@@ -270,6 +355,14 @@ def Solver(self, quantified=False, name=None, logic=None):
                                name=name,
                                logic=logic)
 
+    def UnsatCoreSolver(self, quantified=False, name=None, logic=None,
+                        unsat_cores_mode="all"):
+        return self.get_unsat_core_solver(quantified=quantified,
+                                          name=name,
+                                          logic=logic,
+                                          unsat_cores_mode=unsat_cores_mode)
+
+
     def QuantifierEliminator(self, name=None):
         return self.get_quantifier_eliminator(name=name)
 
@@ -292,6 +385,21 @@ def get_model(self, formula, solver_name=None, logic=None):
                 retval = solver.get_model()
             return retval
 
+    def get_unsat_core(self, clauses, solver_name=None, logic=None):
+        if logic == AUTO_LOGIC:
+            logic = get_logic(self.environment.formula_manager.And(clauses),
+                              self.environment)
+
+        with self.UnsatCoreSolver(name=solver_name, logic=logic) \
+             as solver:
+            for c in clauses:
+                solver.add_assertion(c)
+            check = solver.solve()
+            if check:
+                return None
+
+            return solver.get_unsat_core()
+
     def is_valid(self, formula, solver_name=None, logic=None):
         if logic == AUTO_LOGIC:
             logic = get_logic(formula, self.environment)

pysmt/shortcuts.py

@@ -226,6 +226,14 @@ def Solver(quantified=False, name=None, logic=None):
                                     name=name,
                                     logic=logic)
 
+def UnsatCoreSolver(quantified=False, name=None, logic=None,
+                    unsat_cores_mode="all"):
+    """Returns a solver supporting unsat core extraction."""
+    return get_env().factory.UnsatCoreSolver(quantified=quantified,
+                                             name=name,
+                                             logic=logic,
+                                             unsat_cores_mode=unsat_cores_mode)
+
 def QuantifierEliminator(name=None):
     """Returns a quantifier eliminator"""
     return get_env().factory.QuantifierEliminator(name=name)
@@ -261,6 +269,18 @@ def get_model(formula, solver_name=None, logic=None):
                                  solver_name=solver_name,
                                  logic=logic)
 
+def get_unsat_core(clauses, solver_name=None, logic=None):
+    """Similar to :py:func:`get_model` but returns the unsat core of the
+    conjunction of the input clauses"""
+    env = get_env()
+    if any(c not in env.formula_manager for c in clauses):
+        warnings.warn("Warning: Contextualizing formula during get_model")
+        clauses = [env.formula_manager.normalize(c) for c in clauses]
+
+    return env.factory.get_unsat_core(clauses,
+                                      solver_name=solver_name,
+                                      logic=logic)
+
 def is_valid(formula, solver_name=None, logic=None):
     """Similar to :py:func:`is_sat` but checks validity."""
     env = get_env()

pysmt/smtlib/solver.py

@@ -18,8 +18,11 @@ class SmtLibSolver(Solver):
     the executable. Interaction with the solver occurs via pipe.
     """
 
-    def __init__(self, args, environment, logic, options=None):
-        Solver.__init__(self, environment, logic=logic, options=options)
+    def __init__(self, args, environment, logic, user_options=None):
+        Solver.__init__(self,
+                        environment,
+                        logic=logic,
+                        user_options=user_options)
 
         self.args = args
         self.declared_vars = set()
@@ -37,11 +40,18 @@ def __init__(self, args, environment, logic, options=None):
         # Initialize solver
         self._send_command(SmtLibCommand(smtcmd.SET_OPTION, [":print-success", "false"]))
         self._send_command(SmtLibCommand(smtcmd.SET_OPTION, [":produce-models", "true"]))
-        if options is not None:
-            for o,v in iteritems(options):
+
+        if self.options is not None:
+            for o,v in iteritems(self.options):
                 self._send_command(SmtLibCommand(smtcmd.SET_OPTION, [o, v]))
         self._send_command(SmtLibCommand(smtcmd.SET_LOGIC, [logic]))
 
+    def get_default_options(self, logic=None, user_options=None):
+        res = {}
+        for o,v in iteritems(user_options):
+            if o not in ["generate_models", "unsat_cores_mode"]:
+                res[o] = v
+        return res
 
     def _send_command(self, cmd):
         if self.dbg: print("Sending: " + cmd.serialize_to_string())

pysmt/solvers/bdd.py

@@ -65,11 +65,11 @@ def __exit__(self, type, value, traceback):
 class BddSolver(Solver):
     LOGICS = [ pysmt.logics.QF_BOOL, pysmt.logics.BOOL ]
 
-    def __init__(self, environment, logic, options=None):
+    def __init__(self, environment, logic, user_options):
         Solver.__init__(self,
                         environment=environment,
                         logic=logic,
-                        options=options)
+                        user_options=user_options)
 
         self.mgr = environment.formula_manager
         self.ddmanager = pycudd.DdManager()

pysmt/solvers/cvc4.py

@@ -29,11 +29,11 @@
 class CVC4Solver(Solver, SmtLibBasicSolver, SmtLibIgnoreMixin):
     LOGICS = pysmt.logics.PYSMT_QF_LOGICS
 
-    def __init__(self, environment, logic, options=None):
+    def __init__(self, environment, logic, user_options):
         Solver.__init__(self,
                         environment=environment,
                         logic=logic,
-                        options=options)
+                        user_options=user_options)
         self.em = CVC4.ExprManager()
         self.cvc4 = CVC4.SmtEngine(self.em)
         self.cvc4.setOption("produce-models", CVC4.SExpr("true"))