assign_verify: separate lemma production and activation

src/math/polysat/solver.cpp

@@ -633,31 +633,36 @@ namespace polysat {
     /// Verify the value we're trying to assign against the univariate solver
     void solver::assign_verify(pvar v, rational val, justification j) {
         SASSERT(j.is_decision() || j.is_propagation());
+#ifndef NDEBUG
+        unsigned const old_size = m_search.size();
+#endif
         signed_constraint c;
+        clause_ref lemma;
         {
             // Fake the assignment v := val so we can check the constraints using the new value.
-            m_value[v] = val;
+            // NOTE: we modify the global state here because cloning the assignment is expensive.
             m_search.push_assignment(v, val);
-            m_justification[v] = j;
+            assignment_t const& a = m_search.assignment();
             on_scope_exit _undo([&](){
                 m_search.pop();
-                m_justification[v] = justification::unassigned();
             });
 
             // Check evaluation of the currently-univariate constraints.
-            c = m_viable_fallback.find_violated_constraint(v);
+            c = m_viable_fallback.find_violated_constraint(a, v);
 
             if (c) {
                 LOG("Violated constraint: " << c);
-                // op_constraints produce lemmas rather than forbidden intervals, so give it an opportunity to
-                // produce a lemma before invoking the fallback solver.
-                if (c->is_op()) {
-                    c.narrow(*this, false);
-                    if (is_conflict())
-                        return;
-                }
+                lemma = c.produce_lemma(*this, a);
             }
         }
+        SASSERT(m_search.size() == old_size);
+        SASSERT(!m_search.assignment().contains(v));
+        if (lemma) {
+            add_clause(*lemma);
+            SASSERT(!is_conflict());  // if we have a conflict here, we could have produced this lemma already earlier
+            if (can_propagate())
+                return;
+        }
         if (c) {
             LOG_H2("Chosen assignment " << assignment_pp(*this, v, val) << " is not actually viable!");
             ++m_stats.m_num_viable_fallback;
@@ -699,7 +704,7 @@ namespace polysat {
         // Decision should satisfy all univariate constraints.
         // Propagation might violate some other constraint; but we will notice that in the propagation loop when v is propagated.
         // TODO: on the other hand, checking constraints here would have us discover some conflicts earlier.
-        SASSERT(!j.is_decision() || m_viable_fallback.check_constraints(v));
+        SASSERT(!j.is_decision() || m_viable_fallback.check_constraints(assignment(), v));
 #if ENABLE_LINEAR_SOLVER
         // TODO: convert justification into a format that can be tracked in a dependency core.
         m_linear_solver.set_value(v, val, UINT_MAX);

src/math/polysat/viable.cpp

@@ -837,15 +837,15 @@ namespace polysat {
         m_constraints[v].pop_back();
     }
 
-    signed_constraint viable_fallback::find_violated_constraint(pvar v) {
+    signed_constraint viable_fallback::find_violated_constraint(assignment const& a, pvar v) {
         for (signed_constraint const c : m_constraints[v]) {
             // for this check, all variables need to be assigned
-            DEBUG_CODE(for (pvar w : c->vars()) { SASSERT(s.is_assigned(w)); });
-            if (c.is_currently_false(s)) {
-                LOG(assignment_pp(s, v, s.get_value(v)) << " violates constraint " << lit_pp(s, c));
+            DEBUG_CODE(for (pvar w : c->vars()) { SASSERT(a.contains(w)); });
+            if (c.is_currently_false(a)) {
+                LOG(assignment_pp(s, v, a.value(v)) << " violates constraint " << lit_pp(s, c));
                 return c;
             }
-            SASSERT(c.is_currently_true(s));
+            SASSERT(c.is_currently_true(a));
         }
         return {};
     }

src/math/polysat/viable.h

@@ -250,8 +250,8 @@ namespace polysat {
 
         // Check whether all constraints for 'v' are satisfied;
         // or find an arbitrary violated constraint.
-        bool check_constraints(pvar v) { return !find_violated_constraint(v); }
-        signed_constraint find_violated_constraint(pvar v);
+        bool check_constraints(assignment const& a, pvar v) { return !find_violated_constraint(a, v); }
+        signed_constraint find_violated_constraint(assignment const& a, pvar v);
 
         dd::find_t find_viable(pvar v, rational& out_val);
         signed_constraints unsat_core(pvar v);

src/test/polysat.cpp

@@ -6,6 +6,8 @@
 #include <vector>
 #include <signal.h>
 
+// TODO: collect stats on how often each inference rule is used, so we can see which ones are useful or if any are useless/untested
+
 namespace {
     using namespace dd;
 
@@ -262,6 +264,7 @@ namespace polysat {
             SASSERT(rec->m_expected == l_undef);
             SASSERT(rec->m_result == test_result::undefined);
             SASSERT(rec->m_error_message == "");
+            SASSERT(!rec->m_finished);
             {
                 rec->m_start = test_record::clock_t::now();
                 on_scope_exit end_timer([rec]() {
@@ -1471,6 +1474,8 @@ namespace polysat {
                         VERIFY(false);
                     }
                 }
+                // TODO: now try to extend lo/hi one by one to find out how "bad" our interval really is.
+                //              (probably slow so maybe add a flag to enable/disable that.)
                 e = e->next();
             }
             while (e != first);
@@ -1543,8 +1548,9 @@ static void STD_CALL polysat_on_ctrl_c(int) {
 void tst_polysat() {
     using namespace polysat;
 
-#if 0  // Enable this block to run a single unit test with detailed output.
+#if 1  // Enable this block to run a single unit test with detailed output.
     collect_test_records = false;
+    test_polysat::test_band1();
     // test_polysat::test_ineq_axiom1(32, 1);
     // test_polysat::test_pop_conflict();
     // test_polysat::test_l2();