Merge pull request #29 from pysmt/converter_interface

Issure #23: Added interface for Converter and enforced property Solver.converter

pysmt/solvers/bdd.py

@@ -22,7 +22,7 @@
 import pysmt.logics
 
 from pysmt import typing as types
-from pysmt.solvers.solver import Solver
+from pysmt.solvers.solver import Solver, Converter
 from pysmt.solvers.eager import EagerModel
 from pysmt.walkers import DagWalker
 from pysmt.decorators import clear_pending_pop
@@ -166,7 +166,7 @@ def exit(self):
             del self.ddmanager
 
 
-class BddConverter(DagWalker):
+class BddConverter(Converter, DagWalker):
 
     def __init__(self, environment, ddmanager):
         DagWalker.__init__(self)

pysmt/solvers/cvc4.py

@@ -20,7 +20,7 @@
 import CVC4
 
 import pysmt
-from pysmt.solvers.solver import Solver
+from pysmt.solvers.solver import Solver, Converter
 from pysmt.exceptions import SolverReturnedUnknownResultError
 from pysmt.walkers import DagWalker
 from pysmt.solvers.smtlib import SmtLibBasicSolver, SmtLibIgnoreMixin
@@ -123,7 +123,7 @@ def exit(self):
             del self.cvc4
 
 
-class CVC4Converter(DagWalker):
+class CVC4Converter(Converter, DagWalker):
 
     def __init__(self, environment, cvc4_exprMgr):
         DagWalker.__init__(self, environment)

pysmt/solvers/msat.py

@@ -22,7 +22,7 @@
 
 import pysmt.logics
 from pysmt import typing as types
-from pysmt.solvers.solver import Solver
+from pysmt.solvers.solver import Solver, Converter
 from pysmt.solvers.smtlib import SmtLibBasicSolver, SmtLibIgnoreMixin
 from pysmt.solvers.eager import EagerModel
 from pysmt.walkers import DagWalker
@@ -197,7 +197,7 @@ def exit(self):
             mathsat.msat_destroy_config(self.config)
 
 
-class MSatConverter(DagWalker):
+class MSatConverter(Converter, DagWalker):
 
     def __init__(self, environment, msat_env):
         DagWalker.__init__(self, environment)

pysmt/solvers/solver.py

@@ -222,6 +222,7 @@ class Model(object):
 
     def __init__(self, environment):
         self.environment = environment
+        self._converter = None
 
     def get_value(self, formula):
         """ Returns the value of formula in the current model (if one exists).
@@ -263,6 +264,15 @@ def get_py_values(self, formulae):
             res[f] = v
         return res
 
+    @property
+    def converter(self):
+        """Get the Converter associated with the Solver."""
+        return self._converter
+
+    @converter.setter
+    def converter(self, value):
+        self._converter = value
+
     def __getitem__(self, idx):
         return self.get_value(idx)
 
@@ -273,3 +283,20 @@ def __iter__(self):
 
     def __str__(self):
         return "\n".join([ "%s := %s" % (var, value) for (var, value) in self])
+
+
+class Converter(object):
+    """A Converter implements functionalities to convert expressions.
+
+    There are two key methods: convert() and back().
+    The first performs the forward conversion (pySMT -> Solver API),
+    the second performs the backwards conversion (Solver API -> pySMT)
+    """
+
+    def convert(self, formula):
+        """Convert a PySMT formula into a Solver term."""
+        raise NotImplementedError
+
+    def back(self, expr):
+        """Convert an expression of the Solver into a PySMT term."""
+        raise NotImplementedError

pysmt/solvers/yices.py

@@ -27,7 +27,7 @@
 from pyices.yices_lib import String
 
 from pysmt.solvers.eager import EagerModel
-from pysmt.solvers.solver import Solver
+from pysmt.solvers.solver import Solver, Converter
 from pysmt.solvers.smtlib import SmtLibBasicSolver, SmtLibIgnoreMixin
 
 from pysmt.walkers import DagWalker
@@ -188,7 +188,7 @@ def _get_yices_value(self, term, term_type, getter_func):
 
 
 
-class YicesConverter(DagWalker):
+class YicesConverter(Converter, DagWalker):
 
     def __init__(self, environment):
         DagWalker.__init__(self, environment)

pysmt/solvers/z3.py

@@ -22,7 +22,7 @@
 from fractions import Fraction
 
 from pysmt import typing as types
-from pysmt.solvers.solver import Solver, Model
+from pysmt.solvers.solver import Solver, Model, Converter
 from pysmt.solvers.smtlib import SmtLibBasicSolver, SmtLibIgnoreMixin
 from pysmt.solvers.qelim import QuantifierEliminator
 
@@ -164,7 +164,7 @@ def exit(self):
 
 
 
-class Z3Converter(DagWalker):
+class Z3Converter(Converter, DagWalker):
 
     def __init__(self, environment):
         DagWalker.__init__(self, environment)