MathSAT: Preferred variables with polarity (#526)

Add option to specify polarity in mathsat add_preferred_variable method.

pysmt/solvers/msat.py

@@ -351,9 +351,12 @@ def _var2term(self, var):
         titem = mathsat.msat_make_term(self.msat_env(), decl, [])
         return titem
 
-    def set_preferred_var(self, var):
+    def set_preferred_var(self, var, val=None):
         tvar = self.converter.convert(var)
-        mathsat.msat_add_preferred_for_branching(self.msat_env(), tvar)
+        mval = mathsat.MSAT_UNDEF
+        if val is not None:
+            mval = mathsat.MSAT_TRUE if val==True else mathsat.MSAT_FALSE
+        mathsat.msat_add_preferred_for_branching(self.msat_env(), tvar, mval)
         return
 
     def print_model(self, name_filter=None):

pysmt/test/test_solving.py

@@ -498,6 +498,32 @@ def walk_plus(formula, args):
         with self.assertRaises(InternalSolverError):
             new_converter.convert(f2)
 
+    @skipIfSolverNotAvailable("msat")
+    def test_msat_preferred_variable(self):
+        a, b, c = [Symbol(x) for x in "abc"]
+        na, nb, nc = [Not(Symbol(x)) for x in "abc"]
+
+        f = And(Implies(a, And(b,c)),
+                Implies(na, And(nb,nc)))
+
+        s1 = Solver("msat")
+        s1.add_assertion(f)
+        s1.set_preferred_var(a, True)
+        self.assertTrue(s1.solve())
+        self.assertTrue(s1.get_value(a).is_true())
+
+        s2 = Solver("msat")
+        s2.add_assertion(f)
+        s2.set_preferred_var(a, False)
+        self.assertTrue(s2.solve())
+        self.assertTrue(s2.get_value(a).is_false())
+
+        # Show that calling without polarity still works
+        # This case is harder to test, because we only say
+        # that the split will occur on that variable first.
+        s1.set_preferred_var(a)
+
+
     @skipIfNoSolverForLogic(QF_BOOL)
     def test_conversion_error(self):
         from pysmt.type_checker import SimpleTypeChecker