update var dependency tracking

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/polysat/conflict_core.cpp

@@ -78,12 +78,8 @@ namespace polysat {
     void conflict_core::set(signed_constraint c) {
         LOG("Conflict: " << c);
         SASSERT(empty());
-        insert(c);
-        for (auto v : c->vars()) {
-            if (s().is_assigned(v))
-                m_vars.insert(v);
-            // inc_pref(v);  // hack to be able to test the rest of the conflict resolution loop, TODO: proper fix
-        }
+        c->set_var_dependent();
+        insert(c);       
         SASSERT(!empty());
     }
 
@@ -100,10 +96,8 @@ namespace polysat {
         SASSERT(empty());
         m_conflict_var = v;
         for (auto c : s().m_cjust[v]) {
+            c->set_var_dependent();
             insert(c);
-            for (auto v : c->vars())
-                if (s().is_assigned(v))
-                    m_vars.insert(v);
         }
         SASSERT(!empty());
     }
@@ -305,15 +299,16 @@ namespace polysat {
     void conflict_core::set_mark(signed_constraint c) {
         if (c->is_marked())
             return;
-        bool bool_propagated = c->has_bvar() && c.bvalue(s()) == l_true;
         c->set_mark();
         if (c->has_bvar())
             set_bmark(c->bvar());    
-        if (bool_propagated)
-            c->set_bool_propagated();
-        else 
-            for (auto v : c->vars())
+        if (c->is_var_dependent()) {
+            for (auto v : c->vars()) {
+                if (s().is_assigned(v))
+                    m_vars.insert(v);
                 inc_pref(v);
+            }
+        }
     }
 
     void conflict_core::unset_mark(signed_constraint c) {
@@ -322,11 +317,11 @@ namespace polysat {
         c->unset_mark();
         if (c->has_bvar())
             unset_bmark(c->bvar());
-        if (c->is_bool_propagated())
-            c->unset_bool_propagated();
-        else
+        if (c->is_var_dependent()) {
+            c->unset_var_dependent();
             for (auto v : c->vars())
                 dec_pref(v);
+        }
     }
 
     void conflict_core::inc_pref(pvar v) {

src/math/polysat/constraint.h

@@ -138,7 +138,7 @@ namespace polysat {
         unsigned_vector     m_vars;
         lbool               m_external_sign = l_undef;
         bool                m_is_marked = false;
-        bool                m_is_bool_propagated = false;
+        bool                m_is_var_dependent = false;
         /** The boolean variable associated to this constraint, if any.
          *  If this is not null_bool_var, then the constraint corresponds to a literal on the assignment stack.
          *  Convention: the plain constraint corresponds the positive sat::literal.
@@ -193,9 +193,9 @@ namespace polysat {
         void unset_mark() { m_is_marked = false; }
         bool is_marked() const { return m_is_marked; }
 
-        void set_bool_propagated() { m_is_bool_propagated = true; }
-        void unset_bool_propagated() { m_is_bool_propagated = false; }
-        bool is_bool_propagated() { return m_is_bool_propagated;  }
+        void set_var_dependent() { m_is_var_dependent = true; }
+        void unset_var_dependent() { m_is_var_dependent = false; }
+        bool is_var_dependent() { return m_is_var_dependent;  }
     };
 
     inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }

src/math/polysat/solver.cpp

@@ -497,6 +497,8 @@ namespace polysat {
                 resolve_bool(lit);
             }
         }
+        // here we build conflict clause if it has free variables.
+        // the last decision is reverted.
         report_unsat();
     }
 

src/test/polysat.cpp

@@ -493,7 +493,6 @@ namespace polysat {
         s.expect_unsat();
         s.pop();
 
-        NOT_IMPLEMENTED_YET();  // this is just a note to continue here once we get the above expect_unsat to pass.
 
         // s.push();
         // s.add_ult(quot3 + em, a);
@@ -868,14 +867,25 @@ namespace polysat {
 
 
 void tst_polysat() {
-    polysat::test_subst();
-    // polysat::test_monot_bounds(8);
+    // not working
+    // polysat::test_fixed_point_arith_div_mul_inverse();
+    // polysat::test_cjust();
+    polysat::test_ineq_basic5();
+    // polysat::test_ineq_basic6();
+    // polysat::test_monot_bounds_full();
     // polysat::test_monot_bounds_simple(8);
+    // working
     return;
 
+    polysat::test_fixed_point_arith_mul_div_inverse();
+
+
+        
+    polysat::test_subst();
+    polysat::test_monot_bounds(8);
+
     polysat::test_add_conflicts();
     polysat::test_wlist();
-    polysat::test_cjust();
     polysat::test_l1();
     polysat::test_l2();
     polysat::test_l3();
@@ -888,12 +898,8 @@ void tst_polysat() {
     polysat::test_ineq_basic2();
     polysat::test_ineq_basic3();
     polysat::test_ineq_basic4();
-    polysat::test_ineq_basic5();
-    polysat::test_ineq_basic6();
-    polysat::test_fixed_point_arith_div_mul_inverse();
     polysat::test_monot_bounds(2);
-    polysat::test_monot_bounds_full();
-    polysat::test_fixed_point_arith_mul_div_inverse();
+
 #if 0
     // worry about this later
     polysat::test_ineq1();