Rename revert_decision -> revert_pvar, and enable it.

Also rename resolve_with_assignment to resolve_evaluated

src/math/polysat/conflict.cpp

@@ -104,11 +104,11 @@ namespace polysat {
         }
     };
 
-    struct inf_resolve_with_assignment : public inference {
+    struct inf_resolve_evaluated : public inference {
         solver& s;
         sat::literal lit;
         signed_constraint c;
-        inf_resolve_with_assignment(solver& s, sat::literal lit, signed_constraint c) : s(s), lit(lit), c(c) {}
+        inf_resolve_evaluated(solver& s, sat::literal lit, signed_constraint c) : s(s), lit(lit), c(c) {}
         std::ostream& display(std::ostream& out) const override {
             out << "Resolve upon " << lit << " with assignment:";
             for (pvar v : c->vars())
@@ -251,15 +251,13 @@ namespace polysat {
                 insert_vars(c);
             }
             SASSERT(!m_vars.contains(v));
-            // TODO: apply conflict resolution plugins here too?
         }
         else {
             logger().begin_conflict(header_with_var("forbidden interval lemma for v", v));
             VERIFY(s.m_viable.resolve(v, *this));
         }
-
-        // NSB TODO - disabled: revert_decision(v);
         SASSERT(!empty());
+        revert_pvar(v);  // at this point, v is not assigned
     }
 
     bool conflict::contains(sat::literal lit) const {
@@ -368,7 +366,7 @@ namespace polysat {
         logger().log(inf_resolve_bool(lit, cl));
     }
 
-    void conflict::resolve_with_assignment(sat::literal lit) {
+    void conflict::resolve_evaluated(sat::literal lit) {
         // The reason for lit is conceptually:
         //    x1 = v1 /\ ... /\ xn = vn ==> lit
 
@@ -400,10 +398,10 @@ namespace polysat {
         SASSERT(!contains(lit));
         SASSERT(!contains(~lit));
 
-        logger().log(inf_resolve_with_assignment(s, lit, c));
+        logger().log(inf_resolve_evaluated(s, lit, c));
     }
 
-    void conflict::revert_decision(pvar v) {
+    void conflict::revert_pvar(pvar v) {
         m_resolver->infer_lemmas_for_value(v, *this);
     }
 
@@ -422,7 +420,7 @@ namespace polysat {
         }
         logger().log(inf_resolve_value(s, v));
         
-        revert_decision(v);
+        revert_pvar(v);
     }
 
     clause_ref conflict::build_lemma() {

src/math/polysat/conflict.h

@@ -177,14 +177,14 @@ namespace polysat {
         /** Perform boolean resolution with the clause upon the given literal. */
         void resolve_bool(sat::literal lit, clause const& cl);
 
-        /** lit was fully evaluated under the assignment.  */
+        /** lit was evaluated under the assignment. */
-        void resolve_with_assignment(sat::literal lit);
+        void resolve_evaluated(sat::literal lit);
 
         /** Perform resolution with "v = value <- ..." */
         void resolve_value(pvar v);
 
-        /** Revert decision, add auxiliary lemmas for the decision variable **/
+        /** Revert variable assignment, add auxiliary lemmas for the reverted variable */
-        void revert_decision(pvar v);
+        void revert_pvar(pvar v);
 
         /** Convert the core into a lemma to be learned. */
         clause_ref build_lemma();

src/math/polysat/solver.cpp

@@ -770,7 +770,7 @@ namespace polysat {
                     continue;
                 }
                 if (j.is_decision()) {
-                    // NSB TODO - disabled m_conflict.revert_decision(v);
+                    m_conflict.revert_pvar(v);
                     revert_decision(v);
                     return;
                 }
@@ -806,7 +806,7 @@ namespace polysat {
                     //       do we really want to resolve these eagerly?
                     m_conflict.resolve_bool(lit, *m_bvars.reason(lit));
                 else
-                    m_conflict.resolve_with_assignment(lit);
+                    m_conflict.resolve_evaluated(lit);
             }
         }
         LOG("End of resolve_conflict loop");
@@ -929,6 +929,11 @@ namespace polysat {
             default:
                 UNREACHABLE();
             }
+            if (is_conflict()) {
+                // TODO: the remainder of the narrow_queue as well as the lemmas are forgotten.
+                //       should we just insert them into the new conflict to carry them along?
+                return;
+            }
         }
 
         for (clause* lemma : lemmas) {
@@ -943,7 +948,6 @@ namespace polysat {
                 // TODO: we could also insert the remaining lemmas into the conflict and keep them for later.
                 return;
             }
-            SASSERT(!is_conflict());
         }
 
         if (best_score.branching_factor() > 1) {

src/math/polysat/solver.h

@@ -137,7 +137,7 @@ namespace polysat {
         friend class scoped_solverv;
         friend class test_polysat;
         friend class test_fi;
-        friend struct inf_resolve_with_assignment;
+        friend struct inf_resolve_evaluated;
 
         reslimit&                m_lim;
         params_ref               m_params;