Merge pull request #28 from pysmt/eager_model_contains

Bugfix: Implemented EagerModel.__contains__
pysmt · Mar 3, 2015 · e3d7d16 · e3d7d16
2 parents 1f50d94 + 238c96f
commit e3d7d16
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 0 deletions.
diff --git a/pysmt/solvers/eager.py b/pysmt/solvers/eager.py
@@ -67,3 +67,7 @@ def __iter__(self):
         include more variables.
         """
         return iter(self.assignment.items())
+
+    def __contains__(self, x):
+        """Returns whether the model contains a value for 'x'."""
+        return x in self.assignment
diff --git a/pysmt/test/test_eager_model.py b/pysmt/test/test_eager_model.py
@@ -74,6 +74,13 @@ def test_complete_model(self):
         self.assertTrue(model.get_value(p).is_constant(INT))
         self.assertTrue(model.get_value(r).is_constant(REAL))
 
+    def test_contains(self):
+        x, y, z = [FreshSymbol() for _ in xrange(3)]
+        d = {x: TRUE(), y: FALSE()}
+        model = EagerModel(assignment=d,
+                           environment=get_env())
+        self.assertTrue(x in model)
+        self.assertFalse(z in model)
 
 if __name__ == '__main__':
     import unittest