fix todo on enforcing premises

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

src/math/polysat/conflict.cpp

@@ -146,22 +146,35 @@ namespace polysat {
             m_constraints.push_back(c);
     }
 
-    void conflict::insert(signed_constraint c, vector<signed_constraint> premises) {
+    void conflict::insert(signed_constraint c, vector<signed_constraint> const& premises) {
         insert(c);
-        m_saturation_premises.insert(c, std::move(premises));  // TODO: map doesn't have move-insertion, so this still copies the vector.
+        // NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c?
+        clause_builder c_lemma(s);
+        for (auto premise : premises) {
+            LOG_H3("premise: " << premise);
+            keep(premise);
+            SASSERT(premise->has_bvar());
+            SASSERT(premise.bvalue(s) == l_true);         
+            // otherwise the propagation doesn't make sense
+            c_lemma.push(~premise.blit());
+        }
+        c_lemma.push(c.blit());
+        clause_ref lemma = c_lemma.build();
+        cm().store(lemma.get(), s);
+        if (s.m_bvars.value(c.blit()) == l_undef)
+            s.assign_bool(s.level(*lemma), c.blit(), lemma.get(), nullptr);
     }
 
     void conflict::remove(signed_constraint c) {
+        SASSERT(!c->has_bvar() || std::count(m_constraints.begin(), m_constraints.end(), c) == 0);
         unset_mark(c);       
-        if (c->has_bvar()) {
+        if (c->has_bvar())             
-            SASSERT(std::count(m_constraints.begin(), m_constraints.end(), c) == 0);
+            remove_literal(c.blit());        
-            remove_literal(c.blit());
-        }
         else
             m_constraints.erase(c);
     }
 
-    void conflict::replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> c_new_premises) {
+    void conflict::replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> const& c_new_premises) {
         remove(c_old);
         insert(c_new, c_new_premises);
     }
@@ -185,10 +198,8 @@ namespace polysat {
         SASSERT(!contains_literal(~lit));
         SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0);
         
-        remove_literal(lit);
+        remove_literal(lit);        
-        
+        unset_mark(m.lookup(lit));        
-        unset_mark(m.lookup(lit));
-        
         for (sat::literal lit2 : cl)
             if (lit2 != lit)
                 insert(m.lookup(~lit2));
@@ -205,25 +216,6 @@ namespace polysat {
             insert(c);
         }
         LOG_H3("keeping: " << c);
-        // NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c?
-        auto it = m_saturation_premises.find_iterator(c);
-        if (it == m_saturation_premises.end())
-            return;
-        auto& premises = it->m_value;
-        clause_builder c_lemma(s);
-        for (auto premise : premises) {
-            LOG_H3("premise: " << premise);
-            keep(premise);
-            SASSERT(premise->has_bvar());
-            SASSERT(premise.is_currently_true(s) || premise.bvalue(s) == l_true);
-            // otherwise the propagation doesn't make sense
-            c_lemma.push(~premise.blit());
-        }
-        c_lemma.push(c.blit());
-        clause_ref lemma = c_lemma.build();
-        cm().store(lemma.get(), s);
-        if (s.m_bvars.value(c.blit()) == l_undef)
-            s.assign_bool(s.level(*lemma), c.blit(), lemma.get(), nullptr);
     }
 
     clause_builder conflict::build_lemma() {

src/math/polysat/conflict.h

@@ -86,9 +86,9 @@ namespace polysat {
         void set(clause const& cl);
 
         void insert(signed_constraint c);
-        void insert(signed_constraint c, vector<signed_constraint> premises);
+        void insert(signed_constraint c, vector<signed_constraint> const& premises);
         void remove(signed_constraint c);
-        void replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> c_new_premises);
+        void replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> const& c_new_premises);
 
         void keep(signed_constraint c);
 

src/math/polysat/explain.cpp

@@ -46,48 +46,65 @@ namespace polysat {
 
     // c2 ... constraint that is currently false
     // Try to replace it with a new false constraint (derived from superposition with a true constraint)
-    signed_constraint ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict& core) {
+    lbool ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict& core) {
+        vector<signed_constraint> premises;
         for (auto c1 : core) {
             if (!is_positive_equality_over(v, c1))
                 continue;
             if (!c1.is_currently_true(s()))
                 continue;
-
             signed_constraint c = resolve1(v, c1, c2);
             if (!c)
                 continue;
-            vector<signed_constraint> premises;
+            if (!c->has_bvar())
-            premises.push_back(c1);
+                s().m_constraints.ensure_bvar(c.get());
-            premises.push_back(c2);
+
-            core.replace(c2, c, std::move(premises));
+            switch (c.bvalue(s())) {
-            return c;
+            case l_false:
+                // new conflict state based on propagation and theory conflict
+                core.reset();
+                core.insert(c1);
+                core.insert(c2);
+                core.insert(~c);
+                return l_true;
+            case l_undef:
+                // Ensure that c is assigned and justified                    
+                premises.push_back(c1);
+                premises.push_back(c2);
+                core.replace(c2, c, premises);
+                SASSERT(l_true == c.bvalue(s()));
+                SASSERT(c.is_currently_false(s()));
+                break;
+            default:
+                break;
+            }
+
+            // NOTE: more variables than just 'v' might have been removed here (see polysat::test_p3).
+            // c alone (+ variables) is now enough to represent the conflict.
+            core.reset();
+            core.set(c);
+            return c->contains_var(v) ? l_undef : l_true;
         }
-        return {};
+        return l_false;
     }
 
     // TODO(later): check superposition into disequality again (see notes)
     // true = done, false = abort, undef = continue
+    // TODO: can try multiple replacements at once; then the c2 loop needs to be done only once... (requires some reorganization for storing the premises)
     lbool ex_polynomial_superposition::try_explain1(pvar v, conflict& core) {
         for (auto c2 : core) {
             if (!is_positive_equality_over(v, c2))
                 continue;
             if (!c2.is_currently_false(s()))
                 continue;
-
+            switch (find_replacement(c2, v, core)) {
-            // TODO: can try multiple replacements at once; then the c2 loop needs to be done only once... (requires some reorganization for storing the premises)
+            case l_undef:
-            signed_constraint c = find_replacement(c2, v, core);
-            if (!c)
-                continue;
-            if (c->contains_var(v))
                 return l_undef;
-            if (!c->has_bvar() || l_undef == c.bvalue(s()))
+            case l_true:
-                core.keep(c);  // adds propagation of c to the search stack
+                return l_true;
-
+            case l_false:
-            // NOTE: more variables than just 'v' might have been removed here (see polysat::test_p3).
+                continue;
-            // c alone (+ variables) is now enough to represent the conflict.
+            }
-            core.reset();
-            core.set(c);
-            return l_true;
         }
         return l_false;
     }

src/math/polysat/explain.h

@@ -36,7 +36,7 @@ namespace polysat {
     private:
         bool is_positive_equality_over(pvar v, signed_constraint const& c);
         signed_constraint resolve1(pvar v, signed_constraint c1, signed_constraint c2);
-        signed_constraint find_replacement(signed_constraint c2, pvar v, conflict& core);
+        lbool find_replacement(signed_constraint c2, pvar v, conflict& core);
         void reduce_by(pvar v, conflict& core);
         bool reduce_by(pvar, signed_constraint c, conflict& core);
         lbool try_explain1(pvar v, conflict& core);