Repository: pysmt/pysmt

Issue:
Solver.get_model should not try to assign a value to each variable in the environment
Implementation of get_model in the solvers using EagerModel, extracts one value for each symbol defined in the environment. This has a few problems:

1. In same cases we are doing much more work than needed
2. We cannot extract "partial models"
3. Symbols of type not supported by the solver (e.g., BV) will cause the solver to fail in the model creation.

Ideally, we should use iteration functions from the native solver API to extract models (if these are available).

Discussion:

Patch:
diff --git a/pysmt/native_nodes/__init__.py b/pysmt/native_nodes/__init__.py
new file mode 100644
index 0000000..8b13789
--- /dev/null
+++ b/pysmt/native_nodes/__init__.py
@@ -0,0 +1,1 @@
+
diff --git a/pysmt/solvers/eager.py b/pysmt/solvers/eager.py
index da3fbc7..9f43040 100644
--- a/pysmt/solvers/eager.py
+++ b/pysmt/solvers/eager.py
@@ -16,7 +16,7 @@
 #   limitations under the License.
 #
 from pysmt.solvers.solver import Model
-from pysmt.shortcuts import get_env, Real, Bool, Int
+from pysmt.shortcuts import get_env
 from pysmt.typing import REAL, BOOL, INT
 
 class EagerModel(Model):
@@ -34,37 +34,54 @@ class EagerModel(Model):
         Model.__init__(self, environment)
         self.environment = environment
         self.assignment = assignment
+        # Create a copy of the assignments to memoize completions
+        self.completed_assignment = dict(self.assignment)
+
+    def get_value(self, formula, model_completion=True):
+        if model_completion:
+            syms = formula.get_free_variables()
+            self._complete_model(syms)
+            r = formula.substitute(self.completed_assignment)
+        else:
+            r = formula.substitute(self.assignment)
 
-    def get_value(self, formula):
-        r = formula.substitute(self.assignment)
         res = r.simplify()
         if not res.is_constant():
             raise TypeError("Was expecting a constant but got %s" % res)
         return res
 
-    def complete_model(self, symbols):
-        undefined_symbols = (s for s in symbols if s not in self.assignment)
+
+    def _complete_model(self, symbols):
+        undefined_symbols = (s for s in symbols
+                             if s not in self.completed_assignment)
+        mgr = self.environment.formula_manager
 
         for s in undefined_symbols:
             if not s.is_symbol():
                 raise TypeError("Was expecting a symbol but got %s" %s)
 
-            if s.is_symbol(BOOL):
-                value = Bool(False)
-            elif s.is_symbol(REAL):
-                value = Real(0)
-            elif s.is_symbol(INT):
-                value = Int(0)
+            if s.symbol_type().is_bool_type():
+                value = mgr.Bool(False)
+            elif s.symbol_type().is_real_type():
+                value = mgr.Real(0)
+            elif s.symbol_type().is_int_type():
+                value = mgr.Int(0)
+            elif s.symbol_type().is_bv_type():
+                value = mgr.BVZero(s.bv_width())
             else:
                 raise TypeError("Unhandled type for %s: %s" %
                                 (s, s.symbol_type()))
 
-            self.assignment[s] = value
+            self.completed_assignment[s] = value
+
+
+    def iterator_over(self, language):
+        for x in language:
+            yield x, self.get_value(x, model_completion=True)
 
     def __iter__(self):
         """Overloading of iterator from Model.  We iterate only on the
-        variables defined in the assignment. Call complete_model to
-        include more variables.
+        variables defined in the assignment.
         """
         return iter(self.assignment.items())
 
diff --git a/pysmt/solvers/msat.py b/pysmt/solvers/msat.py
index 5770a86..da38c0a 100644
--- a/pysmt/solvers/msat.py
+++ b/pysmt/solvers/msat.py
@@ -288,10 +288,16 @@ class MathSAT5Solver(IncrementalTrackingSolver, UnsatCoreSolver,
 
     def get_model(self):
         assignment = {}
-        for s in self.environment.formula_manager.get_all_symbols():
-            if s.is_term():
-                v = self.get_value(s)
-                assignment[s] = v
+        msat_iterator = mathsat.msat_create_model_iterator(self.msat_env)
+        while mathsat.msat_model_iterator_has_next(msat_iterator):
+            term, value = mathsat.msat_model_iterator_next(msat_iterator)
+            pysmt_term = self.converter.back(term)
+            pysmt_value = self.converter.back(value)
+            if self.environment.stc.get_type(pysmt_term).is_real_type() and \
+               pysmt_value.is_int_constant():
+                pysmt_value = self.mgr.Real(pysmt_value.constant_value())
+            assignment[pysmt_term] = pysmt_value
+        mathsat.msat_destroy_model_iterator(msat_iterator)
         return EagerModel(assignment=assignment, environment=self.environment)
 
 
diff --git a/pysmt/solvers/solver.py b/pysmt/solvers/solver.py
index 3ac613e..f0cf4a0 100644
--- a/pysmt/solvers/solver.py
+++ b/pysmt/solvers/solver.py
@@ -369,43 +369,46 @@ class Model(object):
         self.environment = environment
         self._converter = None
 
-    def get_value(self, formula):
+    def get_value(self, formula, model_completion=True):
         """ Returns the value of formula in the current model (if one exists).
 
+        If model_completion is True, then variables not appearing in the
+        assignment are given a default value, otherwise an error is generated.
+
         This is a simplified version of the SMT-LIB funtion get_values .
         """
         raise NotImplementedError
 
-    def get_values(self, formulae):
+    def get_values(self, formulae, model_completion=True):
         """Evaluates the values of the formulae in the current model returning
            a dictionary.
         """
         res = {}
         for f in formulae:
-            v = self.get_value(f)
+            v = self.get_value(f, model_completion=model_completion)
             res[f] = v
         return res
 
 
-    def get_py_value(self, formula):
+    def get_py_value(self, formula, model_completion=True):
         """ Returns the value of formula as a python type.
 
         E.g., Bool(True) is translated into True.
         This simplifies writing code that branches on values in the model.
         """
-        res = self.get_value(formula)
+        res = self.get_value(formula, model_completion=model_completion)
         assert res.is_constant()
         return res.constant_value()
 
 
-    def get_py_values(self, formulae):
+    def get_py_values(self, formulae, model_completion=True):
         """Evaluates the values of the formulae as python types in the current
            model returning a dictionary.
         """
 
         res = {}
         for f in formulae:
-            v = self.get_py_value(f)
+            v = self.get_py_value(f, model_completion=model_completion)
             res[f] = v
         return res
 
@@ -419,12 +422,7 @@ class Model(object):
         self._converter = value
 
     def __getitem__(self, idx):
-        return self.get_value(idx)
-
-
-    def __iter__(self):
-        for var in self.environment.formula_manager.get_all_symbols():
-            yield var, self.get_value(var)
+        return self.get_value(idx, model_completion=True)
 
     def __str__(self):
         return "\n".join([ "%s := %s" % (var, value) for (var, value) in self])
diff --git a/pysmt/solvers/z3.py b/pysmt/solvers/z3.py
index ec11e8b..8800911 100644
--- a/pysmt/solvers/z3.py
+++ b/pysmt/solvers/z3.py
@@ -64,11 +64,29 @@ class Z3Model(Model):
         self.z3_model = z3_model
         self.converter = Z3Converter(environment)
 
-    def get_value(self, formula):
+    def get_value(self, formula, model_completion=True):
         titem = self.converter.convert(formula)
-        z3_res = self.z3_model.eval(titem, model_completion=True)
+        z3_res = self.z3_model.eval(titem, model_completion=model_completion)
         return self.converter.back(z3_res)
 
+    def iterator_over(self, language):
+        for x in language:
+            yield x, self.get_value(x, model_completion=True)
+
+    def __iter__(self):
+        """Overloading of iterator from Model.  We iterate only on the
+        variables defined in the assignment.
+        """
+        for d in self.z3_model.decls():
+            pysmt_d = self.converter.back(d)
+            yield pysmt_d, self.get_value(pysmt_d)
+
+    def __contains__(self, x):
+        """Returns whether the model contains a value for 'x'."""
+        z3_x = self.converter.convert(x)
+        return z3_x in self.z3_model.decls()
+
+
 
 class Z3Solver(IncrementalTrackingSolver, UnsatCoreSolver,
                SmtLibBasicSolver, SmtLibIgnoreMixin):


Test patch:
diff --git a/pysmt/test/test_eager_model.py b/pysmt/test/test_eager_model.py
index aed7433..610908a 100644
--- a/pysmt/test/test_eager_model.py
+++ b/pysmt/test/test_eager_model.py
@@ -54,7 +54,7 @@ class TestEagerModel(TestCase):
 
         model = EagerModel(assignment=d)
         with self.assertRaises(TypeError):
-            model.get_value(And(x,y))
+            model.get_value(And(x,y), model_completion=False)
 
         d2 = {x:TRUE(), y:x}
         model = EagerModel(assignment=d2)
@@ -69,13 +69,21 @@ class TestEagerModel(TestCase):
         d = {x:TRUE()}
 
         model = EagerModel(assignment=d)
-        model.complete_model([x,y,r,p])
 
         self.assertEqual(model.get_value(x), TRUE())
         self.assertEqual(model.get_value(Or(x,y)), TRUE())
         self.assertTrue(model.get_value(p).is_constant(INT))
         self.assertTrue(model.get_value(r).is_constant(REAL))
 
+        self.assertEqual(model.get_value(x, model_completion=False), TRUE())
+        with self.assertRaises(TypeError):
+            model.get_value(And(x,y), model_completion=False)
+        with self.assertRaises(TypeError):
+            model.get_value(p, model_completion=False)
+        with self.assertRaises(TypeError):
+            model.get_value(r, model_completion=False)
+
+
     def test_contains(self):
         x, y, z = [FreshSymbol() for _ in xrange(3)]
         d = {x: TRUE(), y: FALSE()}
diff --git a/pysmt/test/test_regressions.py b/pysmt/test/test_regressions.py
index 2ce5a75..ce69638 100644
--- a/pysmt/test/test_regressions.py
+++ b/pysmt/test/test_regressions.py
@@ -180,6 +180,19 @@ class TestRegressions(TestCase):
             # The modulus operator must be there
             self.assertIn("%2", str(ex.expression))
 
+    @skipIfSolverNotAvailable("msat")
+    def test_msat_partial_model(self):
+        msat = Solver(name="msat")
+        x, y = Symbol("x"), Symbol("y")
+        msat.add_assertion(x)
+        c = msat.solve()
+        self.assertTrue(c)
+
+        model = msat.get_model()
+        self.assertNotIn(y, model)
+        self.assertIn(x, model)
+        msat.exit()
+
 
 if __name__ == "__main__":
     import unittest