disable new code paths for commit

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

src/math/polysat/conflict.cpp

@@ -74,7 +74,7 @@ namespace polysat {
         // If they create propagations or conflict lemmas we select the 
         // tightest propagation as part of backjumping.
         // 
-        void try_resolve_value(pvar v, conflict& core) {
+        void infer_lemmas_for_value(pvar v, conflict& core) {
             if (m_poly_sup.perform(v, core)) 
                 return;
             if (m_saturation.perform(v, core))
@@ -257,10 +257,8 @@ namespace polysat {
             logger().begin_conflict(header_with_var("forbidden interval lemma for v", v));
             VERIFY(s.m_viable.resolve(v, *this));
         }
-        // NSB review:
+
-        // Saturation is not invoked on forbidden interval conflicts.
+        // NSB TODO - disabled: revert_decision(v);
-        // We miss propagations.
-        // m_resolver->try_resolve_value(v, *this);
         SASSERT(!empty());
     }
 
@@ -401,6 +399,10 @@ namespace polysat {
         logger().log(inf_resolve_with_assignment(s, lit, c));
     }
 
+    void conflict::revert_decision(pvar v) {
+        m_resolver->infer_lemmas_for_value(v, *this);
+    }
+
     void conflict::resolve_value(pvar v) {
         SASSERT(contains_pvar(v));
         SASSERT(s.m_justification[v].is_propagation());
@@ -416,12 +418,7 @@ namespace polysat {
         }
         logger().log(inf_resolve_value(s, v));
         
-        //
+        revert_decision(v);
-        // NSB review: if try_resolve_value returns true, it adds propagations or conflict lemmas.
-        // the return value should not influence resolution. Indeed the code in solver.cpp
-        // just ignores the return value. It seems this function should not have a return value.
-        // 
-        m_resolver->try_resolve_value(v, *this);
     }
 
     clause_ref conflict::build_lemma() {

src/math/polysat/conflict.h

@@ -183,6 +183,9 @@ namespace polysat {
         /** Perform resolution with "v = value <- ..." */
         void resolve_value(pvar v);
 
+        /** Revert decision, add auxiliary lemmas for the decision variable **/
+        void revert_decision(pvar v);
+
         /** Convert the core into a lemma to be learned. */
         clause_ref build_lemma();
 

src/math/polysat/saturation.cpp

@@ -88,13 +88,16 @@ namespace polysat {
         //
 
         m_lemma.insert(~crit.as_signed_constraint());
-        SASSERT(all_of(m_lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) == l_false; }));
+
+        IF_VERBOSE(10, verbose_stream() << "propagate " << m_rule << " ";
+                   for (auto lit : m_lemma) verbose_stream() << s.lit2cnstr(lit) << " ";
+                   verbose_stream() << c << "\n";
+                   );
+
+        SASSERT(all_of(m_lemma, [this](sat::literal lit) { return is_forced_false(s.lit2cnstr(lit)); }));
 
         // NSB review question: insert_eval: Is this right?
         m_lemma.insert_eval(c);
-        IF_VERBOSE(0, verbose_stream() << "propagate " << m_rule << " ";
-                   for (auto& lit : m_lemma) verbose_stream() << s.lit2cnstr(lit) << " ";
-                   verbose_stream() << "\n");
         core.add_lemma(m_rule, m_lemma.build());
         return true;
     }
@@ -640,28 +643,33 @@ namespace polysat {
         pdd a = m.zero();
         pdd b = m.zero();
         pdd X = s.var(x);
-        signed_constraint a_is_odd, x_is_odd, b_is_odd;
         if (!is_AxB_eq_0(x, axb_l_y, a, b, y))
             return false;
-        if (!is_forced_odd(b, b_is_odd)) {
+        signed_constraint b_is_odd = s.odd(b);
-            if (!is_forced_odd(a, a_is_odd))
+        signed_constraint a_is_odd = s.odd(a);
+        signed_constraint x_is_odd = s.odd(X);
+        if (!b_is_odd.is_currently_true(s)) {
+            if (!a_is_odd.is_currently_true(s))
                 return false;
-            if (!is_forced_odd(X, x_is_odd))
+            if (!x_is_odd.is_currently_true(s))
                 return false;
             m_lemma.reset();
             m_lemma.insert(~s.eq(y));
             m_lemma.insert(~a_is_odd);
             m_lemma.insert(~x_is_odd);
-            if (propagate(core, axb_l_y, s.odd(b)))
+            if (propagate(core, axb_l_y, b_is_odd))
                 return true;
             return false;
         }
         m_lemma.reset();
         m_lemma.insert(~s.eq(y));
         m_lemma.insert(~b_is_odd);
-        if (propagate(core, axb_l_y, s.odd(a)))
+        if (propagate(core, axb_l_y, a_is_odd))
             return true;
-        if (propagate(core, axb_l_y, s.odd(X)))
+        m_lemma.reset();
+        m_lemma.insert(~s.eq(y));
+        m_lemma.insert(~b_is_odd);
+        if (propagate(core, axb_l_y, x_is_odd))
             return true;
         return false;        
     }

src/math/polysat/solver.cpp

@@ -770,6 +770,7 @@ namespace polysat {
                     continue;
                 }
                 if (j.is_decision()) {
+                    // NSB TODO - disabled m_conflict.revert_decision(v);
                     revert_decision(v);
                     return;
                 }

src/math/polysat/ule_constraint.cpp

@@ -184,9 +184,6 @@ namespace polysat {
 
         signed_constraint sc(this, is_positive);
 
-        if (sc.bvar() == 31) {
-            IF_VERBOSE(0, verbose_stream() << "Narrow " << sc << " with " << p << " " << q << "\n");
-        }
         LOG_H3("Narrowing " << sc);
         LOG_V("Assignment: " << assignments_pp(s));
         LOG_V("Substituted LHS: " << lhs() << " := " << p);