na

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

src/math/polysat/conflict.cpp

@@ -304,10 +304,9 @@ namespace polysat {
         
         m_vars.remove(v);
 
-        if (!j.is_decision()) {
+        if (j.is_propagation()) 
             for (auto const& c : s.m_viable.get_constraints(v))
-                insert(c);
-        }
+                insert(c);        
 
         for (auto* engine : ex_engines)
             if (engine->try_explain(v, *this))

src/math/polysat/explain.cpp

@@ -48,7 +48,21 @@ namespace polysat {
     // Try to replace it with a new false constraint (derived from superposition with a true constraint)
     lbool ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict& core) {
         vector<signed_constraint> premises;
+
+        // TBD: replacement can be obtained from stack not just core.
+        // see test_l5. Exposes unsoundness bug: a new consequence is derived 
+        // after some variable decision was already processed. Then the 
+        // behavior of evaluating literals "is_currently_true" and bvalue
+        // uses the full search stack
+#if 0
+        for (auto si : s.m_search) {
+            if (!si.is_boolean())
+                continue;
+            auto c1 = s.lit2cnstr(si.lit());
+        
+#else
         for (auto c1 : core) {
+#endif
             if (!is_positive_equality_over(v, c1))
                 continue;
             if (!c1.is_currently_true(s))

src/math/polysat/solver.cpp

@@ -473,6 +473,8 @@ namespace polysat {
         if (m_conflict.conflict_var() != null_var) {
             // This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack.
             VERIFY(m_viable.resolve(m_conflict.conflict_var(), m_conflict));
+            // TBD: make sure last value decision is blocked by this conflict.
+            // A conflict in test_l5 reverts v1 = 2 more than once.
         }
 
         search_iterator search_it(m_search);

src/math/polysat/viable.cpp

@@ -341,7 +341,7 @@ namespace polysat {
             return out;
         entry* first = e;
         do {
-            out << "v" << v << ": " << e->interval << " " << e->side_cond << " " << e->src << "\n";
+            out << e->interval << " " << e->side_cond << " " << e->src << " ";
             e = e->next();
         }         
         while (e != first);
@@ -350,7 +350,7 @@ namespace polysat {
 
     std::ostream& viable::display(std::ostream& out) const {
         for (pvar v = 0; v < m_viable.size(); ++v)
-            display(out, v);
+            display(out << "v" << v << ": ", v);
         return out;
     }