Repository: pysmt/pysmt
Pull request #104 (2015-05-08 12:13:33)

Interpolation Support
This is just a clean branch for PR #103.

All the credits go to @agriggio


Patch:
diff --git a/pysmt/factory.py b/pysmt/factory.py
index 4c8704a..a6cb4d9 100644
--- a/pysmt/factory.py
+++ b/pysmt/factory.py
@@ -28,25 +28,29 @@ from six import iteritems
 
 from pysmt.exceptions import (NoSolverAvailableError, SolverRedefinitionError,
                               NoLogicAvailableError)
-from pysmt.logics import QF_UFLIRA, LRA
+from pysmt.logics import QF_UFLIRA, LRA, QF_UFLRA
 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', 'picosat', 'bdd']
 DEFAULT_QELIM_PREFERENCE_LIST = ['z3', 'msat_fm', 'msat_lw']
+DEFAULT_INTERPOLATION_PREFERENCE_LIST = ['msat', 'z3']
 DEFAULT_LOGIC = QF_UFLIRA
 DEFAULT_QE_LOGIC = LRA
+DEFAULT_INTERPOLATION_LOGIC = QF_UFLRA
 
 class Factory(object):
 
     def __init__(self, environment,
                  solver_preference_list=None,
-                 qelim_preference_list=None):
+                 qelim_preference_list=None,
+                 interpolation_preference_list=None):
         self.environment = environment
         self._all_solvers = None
         self._all_unsat_core_solvers = None
         self._all_qelims = None
+        self._all_interpolators = None
         self._generic_solvers = {}
 
         if solver_preference_list is None:
@@ -55,12 +59,19 @@ class Factory(object):
 
         if qelim_preference_list is None:
             qelim_preference_list = DEFAULT_QELIM_PREFERENCE_LIST
+
+        if interpolation_preference_list is None:
+            interpolation_preference_list = \
+                                          DEFAULT_INTERPOLATION_PREFERENCE_LIST
         self.qelim_preference_list = qelim_preference_list
+        self.interpolation_preference_list = interpolation_preference_list
         self._default_logic = DEFAULT_LOGIC
         self._default_qe_logic = DEFAULT_QE_LOGIC
+        self._default_interpolation_logic = DEFAULT_INTERPOLATION_LOGIC
 
         self._get_available_solvers()
         self._get_available_qe()
+        self._get_available_interpolators()
 
 
     def get_solver(self, quantified=False, name=None, logic=None):
@@ -117,6 +128,18 @@ class Factory(object):
         return SolverClass(environment=self.environment,
                            logic=closer_logic)
 
+    def get_interpolator(self, name=None, logic=None):
+        SolverClass, closer_logic = self._get_solver_class(
+            solver_list=self._all_interpolators,
+            solver_type="Interpolator",
+            preference_list=self.interpolation_preference_list,
+            default_logic=self._default_interpolation_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):
@@ -267,6 +290,21 @@ class Factory(object):
             pass
 
 
+    def _get_available_interpolators(self):
+        self._all_interpolators = {}
+
+        try:
+            from pysmt.solvers.z3 import Z3Interpolator
+            self._all_interpolators['z3'] = Z3Interpolator
+        except ImportError:
+            pass
+
+        try:
+            from pysmt.solvers.msat import MSatInterpolator
+            self._all_interpolators['msat'] = MSatInterpolator
+        except ImportError:
+            pass
+
 
     def set_solver_preference_list(self, preference_list):
         """Defines the order in which to pick the solvers.
@@ -288,6 +326,14 @@ class Factory(object):
         assert len(preference_list) > 0
         self.qelim_preference_list = preference_list
 
+
+    def set_interpolation_preference_list(self, preference_list):
+        """Defines the order in which to pick the solvers."""
+        assert preference_list is not None
+        assert len(preference_list) > 0
+        self.interpolation_preference_list = preference_list
+        
+
     def _filter_solvers(self, solver_list, logic=None):
         """
         Returns a dict <solver_name, solver_class> including all and only
@@ -373,6 +419,9 @@ class Factory(object):
     def QuantifierEliminator(self, name=None, logic=None):
         return self.get_quantifier_eliminator(name=name, logic=logic)
 
+    def Interpolator(self, name=None, logic=None):
+        return self.get_interpolator(name=name, logic=logic)
+
     def is_sat(self, formula, solver_name=None, logic=None):
         if logic == AUTO_LOGIC:
             logic = get_logic(formula, self.environment)
@@ -428,6 +477,26 @@ class Factory(object):
         with self.QuantifierEliminator(name=solver_name, logic=logic) as qe:
             return qe.eliminate_quantifiers(formula)
 
+
+    def binary_interpolant(self, formula_a, formula_b,
+                           solver_name=None, logic=None):
+        if logic == AUTO_LOGIC:
+            logic = get_logic(
+                self.environment.formula_manager.And(formula_a, formula_b))
+
+        with self.Interpolator(name=solver_name, logic=logic) as itp:
+            return itp.binary_interpolant(formula_a, formula_b)
+
+
+    def sequence_interpolant(self, formulas, solver_name=None, logic=None):
+        if logic == AUTO_LOGIC:
+            logic = get_logic(
+                self.environment.formula_manager.And(formulas))
+
+        with self.Interpolator(name=solver_name, logic=logic) as itp:
+            return itp.sequence_interpolant(formulas)
+        
+
     @property
     def default_logic(self):
         return self._default_logic
diff --git a/pysmt/shortcuts.py b/pysmt/shortcuts.py
index 12436e5..341f984 100644
--- a/pysmt/shortcuts.py
+++ b/pysmt/shortcuts.py
@@ -360,6 +360,12 @@ def QuantifierEliminator(name=None, logic=None):
     """Returns a quantifier eliminator"""
     return get_env().factory.QuantifierEliminator(name=name, logic=logic)
 
+
+def Interpolator(name=None, logic=None):
+    """Returns an interpolator"""
+    return get_env().factory.Interpolator(name=name, logic=logic)
+
+
 def is_sat(formula, solver_name=None, logic=None):
     """ Returns whether a formula is satisfiable.
 
@@ -437,6 +443,38 @@ def qelim(formula, solver_name=None, logic=None):
                              logic=logic)
 
 
+def binary_interpolant(formula_a, formula_b, solver_name=None, logic=None):
+    """Computes an interpolant of (formula_a, formula_b). Returns None
+    if the conjunction is satisfiable"""
+    env = get_env()
+    formulas = [formula_a, formula_b]
+    for i, f in enumerate(formulas):
+        if f not in env.formula_manager:
+            warnings.warn("Warning: Contextualizing formula during "
+                          "binary_interpolant")
+            formulas[i] = env.formula_manager.normalize(f)
+
+    return env.factory.binary_interpolant(formulas[0], formulas[1],
+                                          solver_name=solver_name,
+                                          logic=logic)
+
+
+def sequence_interpolant(formulas, solver_name=None, logic=None):
+    """Computes a sequence interpolant of the formulas. Returns None
+    if the conjunction is satisfiable"""
+    env = get_env()
+    formulas = list(formulas)
+    for i, f in enumerate(formulas):
+        if f not in env.formula_manager:
+            warnings.warn("Warning: Contextualizing formula during "
+                          "sequence_interpolant")
+            formulas[i] = env.formula_manager.normalize(f)
+
+    return env.factory.sequence_interpolant(formulas,
+                                            solver_name=solver_name,
+                                            logic=logic)
+
+
 
 def read_configuration(config_filename, environment=None):
     """
diff --git a/pysmt/solvers/interpolation.py b/pysmt/solvers/interpolation.py
new file mode 100644
index 0000000..c3662e6
--- /dev/null
+++ b/pysmt/solvers/interpolation.py
@@ -0,0 +1,48 @@
+#
+# This file is part of pySMT.
+#
+#   Copyright 2014 Andrea Micheli and Marco Gario
+#
+#   Licensed under the Apache License, Version 2.0 (the "License");
+#   you may not use this file except in compliance with the License.
+#   You may obtain a copy of the License at
+#
+#       http://www.apache.org/licenses/LICENSE-2.0
+#
+#   Unless required by applicable law or agreed to in writing, software
+#   distributed under the License is distributed on an "AS IS" BASIS,
+#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#   See the License for the specific language governing permissions and
+#   limitations under the License.
+#
+
+class Interpolator(object):
+
+    def binary_interpolant(self, a, b):
+        """
+        Returns a binary interpolant for the pair (a, b), if And(a, b) is
+        unsatisfaiable, or None if And(a, b) is satisfiable.
+        """
+        raise NotImplementedError
+
+
+    def sequence_interpolant(self, formulas):
+        """
+        Returns a sequence interpolant for the conjunction of formulas,
+        or None if the problem is satisfiable.
+        """
+        raise NotImplementedError
+
+
+    def __enter__(self):
+        """ Manage entering a Context (i.e., with statement) """
+        return self
+
+
+    def __exit__(self, exc_type, exc_val, exc_tb):
+        """ Manage exiting from Context (i.e., with statement)
+
+        The default behaviour is to explicitely destroy the interpolator to
+        free the associated resources.
+        """
+        del self
diff --git a/pysmt/solvers/msat.py b/pysmt/solvers/msat.py
index 62bf765..606cd72 100644
--- a/pysmt/solvers/msat.py
+++ b/pysmt/solvers/msat.py
@@ -21,7 +21,7 @@ from six.moves import xrange
 
 import mathsat
 
-from pysmt.logics import LRA, PYSMT_QF_LOGICS
+from pysmt.logics import LRA, QF_UFLIA, QF_UFLRA, QF_BV, PYSMT_QF_LOGICS
 from pysmt.oracles import get_logic
 
 import pysmt.operators as op
@@ -37,6 +37,7 @@ from pysmt.exceptions import (SolverReturnedUnknownResultError,
                               InternalSolverError)
 from pysmt.decorators import clear_pending_pop
 from pysmt.solvers.qelim import QuantifierEliminator
+from pysmt.solvers.interpolation import Interpolator
 from pysmt.walkers.identitydag import IdentityDagWalker
 
 
@@ -904,3 +905,80 @@ if hasattr(mathsat, "MSAT_EXIST_ELIM_ALLSMT_FM"):
         def __init__(self, environment, logic=None):
             MSatQuantifierEliminator.__init__(self, environment,
                                               logic=logic, algorithm='lw')
+
+
+class MSatInterpolator(Interpolator):
+
+    LOGICS = [QF_UFLIA, QF_UFLRA, QF_BV]
+
+    def __init__(self, environment, logic=None):
+        self.msat_env = mathsat.msat_create_env()
+        self.converter = MSatConverter(environment, self.msat_env)
+        self.environment = environment
+        self.logic = logic
+
+
+    def __del__(self):
+        mathsat.msat_destroy_env(self.msat_env)
+
+
+    def _check_logic(self, formulas):
+        for f in formulas:
+            logic = get_logic(f, self.environment)
+            ok = any(logic <= l for l in self.LOGICS)
+            if not ok:
+                raise NotImplementedError(
+                    "Logic not supported by MathSAT inteprolation."
+                    "(detected logic is: %s)" % str(logic))
+
+
+    def binary_interpolant(self, a, b):
+        res = self.sequence_interpolant([a, b])
+        if res is not None:
+            res = res[0]
+        return res
+
+
+    def sequence_interpolant(self, formulas):
+        cfg, env = None, None
+        try:
+            self._check_logic(formulas)
+
+            if len(formulas) < 2:
+                raise Exception("interpolation needs at least 2 formulae")
+
+            cfg = mathsat.msat_create_config()
+            mathsat.msat_set_option(cfg, "interpolation", "true")
+            if self.logic == QF_BV:
+                mathsat.msat_set_option(cfg, "theory.bv.eager", "false")
+                mathsat.msat_set_option(cfg, "theory.eq_propagaion", "false")
+            env = mathsat.msat_create_env(cfg, self.msat_env)
+
+            groups = []
+            for f in formulas:
+                f = self.converter.convert(f)
+                g = mathsat.msat_create_itp_group(env)
+                mathsat.msat_set_itp_group(env, g)
+                groups.append(g)
+                mathsat.msat_assert_formula(env, f)
+
+            res = mathsat.msat_solve(env)
+            if res == mathsat.MSAT_UNKNOWN:
+                raise Exception("error in mathsat interpolation: %s" %
+                                mathsat.msat_last_error_message(env))
+
+            if res == mathsat.MSAT_SAT:
+                return None
+
+            pysmt_ret = []
+            for i in xrange(1, len(groups)):
+                itp = mathsat.msat_get_interpolant(env, groups[:i])
+                f = self.converter.back(itp)
+                pysmt_ret.append(f)
+
+            return pysmt_ret
+        finally:
+            if cfg:
+                mathsat.msat_destroy_config(cfg)
+            if env:
+                mathsat.msat_destroy_env(env)
diff --git a/pysmt/solvers/z3.py b/pysmt/solvers/z3.py
index 441d9ed..1310e6b 100644
--- a/pysmt/solvers/z3.py
+++ b/pysmt/solvers/z3.py
@@ -27,6 +27,7 @@ from pysmt.solvers.solver import (IncrementalTrackingSolver, UnsatCoreSolver,
                                   Model, Converter)
 from pysmt.solvers.smtlib import SmtLibBasicSolver, SmtLibIgnoreMixin
 from pysmt.solvers.qelim import QuantifierEliminator
+from pysmt.solvers.interpolation import Interpolator
 
 from pysmt.walkers import DagWalker
 from pysmt.exceptions import (SolverReturnedUnknownResultError,
@@ -36,7 +37,7 @@ from pysmt.exceptions import (SolverReturnedUnknownResultError,
                               ConvertExpressionError)
 from pysmt.decorators import clear_pending_pop
 
-from pysmt.logics import LRA, LIA, PYSMT_LOGICS, BV_LOGICS
+from pysmt.logics import LRA, LIA, QF_UFLIA, QF_UFLRA, PYSMT_LOGICS, BV_LOGICS
 from pysmt.oracles import get_logic
 
 
@@ -491,3 +492,52 @@ class Z3QuantifierEliminator(QuantifierEliminator):
                                           expression=res)
 
         return pysmt_res
+
+
+class Z3Interpolator(Interpolator):
+
+    LOGICS = [QF_UFLIA, QF_UFLRA]
+
+    def __init__(self, environment, logic=None):
+        self.environment = environment
+        self.logic = logic
+        self.converter = Z3Converter(environment)
+
+
+    def _check_logic(self, formulas):
+        for f in formulas:
+            logic = get_logic(f, self.environment)
+            ok = any(logic <= l for l in self.LOGICS)
+            if not ok:
+                raise NotImplementedError(
+                    "Logic not supported by Z3 inteprolation."
+                    "(detected logic is: %s)" % str(logic))
+
+
+    def binary_interpolant(self, a, b):
+        self._check_logic([a, b])
+            
+        a = self.converter.convert(a)
+        b = self.converter.convert(b)
+
+        try:
+            itp = z3.binary_interpolant(a, b)
+            pysmt_res = self.converter.back(itp)
+        except z3.ModelRef:
+            pysmt_res = None
+            
+        return pysmt_res
+
+
+    def sequence_interpolant(self, formulas):
+        self._check_logic(formulas)
+
+        zf = [self.converter.convert(f) for f in formulas]
+
+        try:
+            itp = z3.sequence_interpolant(zf)
+            pysmt_res = [self.converter.back(f) for f in itp]
+        except z3.ModelRef:
+            pysmt_res = None
+            
+        return pysmt_res


Test patch:
diff --git a/pysmt/test/test_interpolation.py b/pysmt/test/test_interpolation.py
new file mode 100644
index 0000000..fa78176
--- /dev/null
+++ b/pysmt/test/test_interpolation.py
@@ -0,0 +1,141 @@
+#
+# This file is part of pySMT.
+#
+#   Copyright 2014 Andrea Micheli and Marco Gario
+#
+#   Licensed under the Apache License, Version 2.0 (the "License");
+#   you may not use this file except in compliance with the License.
+#   You may obtain a copy of the License at
+#
+#       http://www.apache.org/licenses/LICENSE-2.0
+#
+#   Unless required by applicable law or agreed to in writing, software
+#   distributed under the License is distributed on an "AS IS" BASIS,
+#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#   See the License for the specific language governing permissions and
+#   limitations under the License.
+#
+import unittest
+
+from pysmt.shortcuts import *
+from pysmt.typing import REAL, BOOL, INT
+from pysmt.test import (TestCase, skipIfSolverNotAvailable)
+from pysmt.exceptions import (SolverReturnedUnknownResultError, \
+                              NoSolverAvailableError)
+from pysmt.logics import LRA, LIA, UFLIRA
+
+
+class TestInterpolation(TestCase):
+    def test_selection(self):
+        with self.assertRaises(NoSolverAvailableError):
+            Interpolator(logic=UFLIRA)
+
+        with self.assertRaises(NoSolverAvailableError):
+            Interpolator(name="nonexistent")
+
+
+    @skipIfSolverNotAvailable('z3')
+    def test_binary_interpolant_z3(self):
+        self._test_binary_interpolant('z3')
+
+
+    @skipIfSolverNotAvailable('msat')
+    def test_binary_interpolant_msat(self):
+        self._test_binary_interpolant('msat')
+
+
+    @skipIfSolverNotAvailable('z3')
+    def test_sequence_interpolant_z3(self):
+        self._test_sequence_interpolant('z3')
+
+
+    @skipIfSolverNotAvailable('msat')
+    def test_sequence_interpolant_msat(self):
+        self._test_sequence_interpolant('msat')
+
+
+    def _test_binary_interpolant(self, name):
+        itp = Interpolator(name=name)
+        self._bool_example(itp, True)
+        self._real_example(itp, True)
+        self._int_example(itp, True)
+
+
+    def _test_sequence_interpolant(self, name):
+        itp = Interpolator(name=name)
+        self._bool_example(itp, False)
+        self._real_example(itp, False)
+        self._int_example(itp, False)
+
+
+    def _bool_example(self, itp, binary):
+        # Bool Example
+        x, y, z = Symbol("bx"), Symbol("by"), Symbol("bz")
+
+        a = And(x, Not(y))
+        b = And(Implies(z, y), z)
+
+        if binary:
+            i = itp.binary_interpolant(a, b)
+        else:
+            i = itp.sequence_interpolant([a, b])
+
+        self.assertTrue(i is not None)
+        if not binary:
+            self.assertTrue(hasattr(i, '__len__'))
+            self.assertTrue(len(i) == 1)
+            i = i[0]
+
+        self.assertTrue(i.get_free_variables() == set([y]))
+        self.assertValid(Implies(a, i))
+        self.assertUnsat(And(i, b))
+
+
+    def _real_example(self, itp, binary):
+        # Real Example
+        x, y, z = Symbol("rx", REAL), Symbol("ry", REAL), Symbol("rz", REAL)
+
+        a = And(LE(x, Real(0)), LE(y, x))
+        b = And(GE(y, z), Equals(z, Real(1)))
+
+        if binary:
+            i = itp.binary_interpolant(a, b)
+        else:
+            i = itp.sequence_interpolant([a, b])
+            
+        self.assertTrue(i is not None)
+        if not binary:
+            self.assertTrue(hasattr(i, '__len__'))
+            self.assertTrue(len(i) == 1)
+            i = i[0]
+
+        self.assertTrue(i.get_free_variables() == set([y]))
+        self.assertValid(Implies(a, i))
+        self.assertUnsat(And(i, b))
+
+
+    def _int_example(self, itp, binary):
+        # Int Example
+        x, y, z = Symbol("ix", INT), Symbol("iy", INT), Symbol("iz", INT)
+
+        a = And(LE(x, Int(1)), LT(y, x))
+        b = And(GE(y, z), GT(z, Int(0)))
+
+        if binary:
+            i = itp.binary_interpolant(a, b)
+        else:
+            i = itp.sequence_interpolant([a, b])
+            
+        self.assertTrue(i is not None)
+        if not binary:
+            self.assertTrue(hasattr(i, '__len__'))
+            self.assertTrue(len(i) == 1)
+            i = i[0]
+
+        self.assertTrue(i.get_free_variables() == set([y]))
+        self.assertValid(Implies(a, i))
+        self.assertUnsat(And(i, b))
+        
+
+if __name__ == '__main__':
+    unittest.main()