update

src/math/polysat/conflict_core.cpp

@@ -108,7 +108,29 @@ namespace polysat {
                 m_constraints.push_back(m.lookup(~lit));
     }
 
-    clause_ref conflict_core::build_lemma() {
+    /** If the constraint c is a temporary constraint derived by core saturation, insert it (and recursively, its premises) into \Gamma */
+    void conflict_core::handle_saturation_premises(signed_constraint 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(*m_solver);
+        for (auto premise : premises) {
+            handle_saturation_premises(c);
+            c_lemma.push_literal(~premise.blit());
+        }
+        c_lemma.push_literal(c.blit());
+        clause* cl = cm().store(c_lemma.build());
+        if (cl->size() == 1)
+            c->set_unit_clause(cl);
+        // TODO: this should be backtrackable (unless clause is unit).
+        // => add at the end and update pop_levels to replay appropriately
+        m_solver->assign_bool_core(c.blit(), cl, nullptr);
+        m_solver->activate_constraint(c);
+    }
+
+    clause_ref conflict_core::build_lemma(unsigned model_level) {
         LOG_H3("build lemma from core");
         sat::literal_vector literals;
         p_dependency_ref dep = m_solver->mk_dep_ref(null_dependency);
@@ -122,22 +144,7 @@ namespace polysat {
                 cm().ensure_bvar(c.get());
                 LOG("new constraint: " << c);
                 // Insert the temporary constraint from saturation into \Gamma.
-                auto it = m_saturation_premises.find_iterator(c);
+                handle_saturation_premises(c);
-                if (it != m_saturation_premises.end()) {
-                    auto& premises = it->m_value;
-                    clause_builder c_lemma(*m_solver);
-                    for (auto premise : premises)
-                        c_lemma.push_literal(~premise.blit());
-                    c_lemma.push_literal(c.blit());
-                    clause* cl = cm().store(c_lemma.build());
-                    if (cl->size() == 1)
-                        c->set_unit_clause(cl);
-                    // TODO: actually, this should be backtrackable (unless clause is unit). But currently we cannot insert in the middle of the stack!
-                    //      (or do it like MCSAT... they keep "theory-propagated" literals also at the end and restore them on backtracking)
-                    // => add at the end and update pop_levels to replay appropriately
-                    m_solver->assign_bool_core(c.blit(), cl, nullptr);
-                    m_solver->activate_constraint(c);
-                }
             }
             if (c->unit_clause()) {
                 dep = m_solver->m_dm.mk_join(dep, c->unit_dep());
@@ -156,6 +163,9 @@ namespace polysat {
                     vars.insert(v);
             // Add v != val for each variable
             for (pvar v : vars) {
+                // SASSERT(!m_solver->m_justification[v].is_unassigned());  // TODO: why does this trigger????
+                if (m_solver->m_justification[v].level() > model_level)
+                    continue;
                 auto diseq = ~cm().eq(lvl, m_solver->var(v) - m_solver->m_value[v]);
                 cm().ensure_bvar(diseq.get());
                 literals.push_back(diseq.blit());
@@ -166,20 +176,19 @@ namespace polysat {
     }
 
     bool conflict_core::resolve_value(pvar v, vector<signed_constraint> const& cjust_v) {
-        // TODO: maybe don't do this automatically, because cjust-constraints are true and core constraints are false.
+        // NOTE:
-        //       issue: what if viable(v) is empty? then we only have cjust constraints and none of them is evaluable (at least not immediately because no value is set for this variable.)
+        // In the "standard" case where "v = val" is on the stack:
-        //                  => think about what we want to do in this case (choose a value and evaluate? try all possible superpositions without caring about the value of the premises?)
+        //      - cjust_v contains true constraints
-        // the last value_resolution method can then be the one that adds the cjusts and calls saturation and more general VE.
+        //      - core contains both false and true constraints... (originally only false ones, but additional true ones may come from saturation).
+        // In the case where no assignment to v is on the stack, i.e., conflict_var == v and viable(v) = \emptyset:
+        //      - the constraints in cjust_v cannot be evaluated.
+        //      - TODO: what to do here? pick some value?
 
-        // No value resolution method was successful => fall back to saturation and variable elimination
         for (auto c : cjust_v)
             insert(c);
 
-        // Variable elimination
+        // No value resolution method was successful => fall back to saturation and variable elimination
         while (true) {  // TODO: limit?
-            // TODO: maybe we shouldn't try to split up VE/Saturation in the implementation.
-            //       it might be better to just have more general "core inferences" that may combine elimination/saturation steps that fit together...
-            //       or even keep the whole "value resolution + VE/Saturation" as a single step. we might want to know which constraints come from the current cjusts?
             // TODO: as a last resort, substitute v by m_value[v]?
             if (!try_saturate(v))
                 break;

src/math/polysat/conflict_core.h

@@ -44,6 +44,7 @@ namespace polysat {
 
         // ptr_addr_map<constraint, vector<signed_constraint>> m_saturation_premises;
         map<signed_constraint, vector<signed_constraint>, obj_hash<signed_constraint>, default_eq<signed_constraint>> m_saturation_premises;
+        void handle_saturation_premises(signed_constraint c);
     public:
         conflict_core(solver& s);
         ~conflict_core();
@@ -88,7 +89,7 @@ namespace polysat {
         bool resolve_value(pvar v, vector<signed_constraint> const& cjust_v);
 
         /** Convert the core into a lemma to be learned. */
-        clause_ref build_lemma();
+        clause_ref build_lemma(unsigned model_level);
 
         bool try_eliminate(pvar v);
         bool try_saturate(pvar v);

src/math/polysat/explain.cpp

@@ -19,31 +19,44 @@ namespace polysat {
 
     constraint_manager& explainer::cm() { return s().m_constraints; }
 
-    bool ex_polynomial_superposition::try_explain(pvar v, vector<signed_constraint> const& cjust_v, conflict_core& core) {
+    // TODO(later): check superposition into disequality again (see notes)
-        // TODO: check superposition into disequality again (see notes)
+    bool ex_polynomial_superposition::try_explain(pvar v, /* vector<signed_constraint> const& cjust_v, */ conflict_core& core) {
-
-        // TODO: use indexing/marking for this instead of allocating a temporary vector
         // TODO: core saturation premises are from \Gamma (i.e., has_bvar)... but here we further restrict to the core; might need to revise
         //       -- especially: should take into account results from previous saturations (they will be in \Gamma, but only if we use the constraint or one of its descendants for the lemma)
         //       actually: we want to take one from the current cjust (currently true) and one from the conflict (currently false)
-        vector<signed_constraint> candidates;
-        for (auto c : core)
-            if (c->has_bvar() && c.is_positive() && c->is_eq() && c->contains_var(v))
-                candidates.push_back(c);
 
-        // TODO: c1 should a currently true constraint, while c2 should take a currently false constraint.
+        // TODO: resolve multiple times... a single time might not be enough to eliminate the variable.
-        //       remove candidates vector (premature optimization)
-        //      we may want to apply this multiple times (a single resolve might not eliminate the variable).
 
         LOG_H3("Trying polynomial superposition...");
-        for (auto it1 = candidates.begin(); it1 != candidates.end(); ++it1) {
+        for (auto it1 = core.begin(); it1 != core.end(); ++it1) {
-            for (auto it2 = it1 + 1; it2 != candidates.end(); ++it2) {
             signed_constraint c1 = *it1;
+            if (!c1->has_bvar())
+                continue;
+            if (!c1.is_positive())
+                continue;
+            if (!c1->is_eq())
+                continue;
+            if (!c1->contains_var(v))
+                continue;
+            if (!c1.is_currently_true(s()))
+                continue;
+
+            for (auto it2 = core.begin(); it2 != core.end(); ++it2) {
                 signed_constraint c2 = *it2;
-                SASSERT(c1 != c2);
+                if (!c2->has_bvar())
+                    continue;
+                if (!c2.is_positive())
+                    continue;
+                if (!c2->is_eq())
+                    continue;
+                if (!c2->contains_var(v))
+                    continue;
+                if (!c2.is_currently_false(s()))
+                    continue;
+
+                // c1 is true, c2 is false
                 LOG("c1: " << c1);
                 LOG("c2: " << c2);
-
                 pdd a = c1->to_eq().p();
                 pdd b = c2->to_eq().p();
                 pdd r = a;
@@ -57,20 +70,26 @@ namespace polysat {
                 vector<signed_constraint> premises;
                 premises.push_back(c1);
                 premises.push_back(c2);
+                if (!c->contains_var(v)) {
+                    core.reset();
                     core.insert(c, std::move(premises));
                     return true;
-
+                } else {
-//             clause_builder clause(m_solver);
+                    core.insert(c, std::move(premises));
-//             clause.push_literal(~c1->blit());
+                }
-//             clause.push_literal(~c2->blit());
-//             clause.push_new_constraint(m_solver.m_constraints.eq(lvl, r));
-//             return clause.build();
             }
         }
 
         return false;
     }
 
+
+
+
+
+
+
+
 //         LOG_H3("Attempting to explain conflict for v" << v);
 //         m_var = v;
 //         m_cjust_v = cjust;

src/math/polysat/explain.h

@@ -31,11 +31,11 @@ namespace polysat {
         constraint_manager& cm();
     public:
         virtual ~explainer() {}
-        virtual bool try_explain(pvar v, vector<signed_constraint> const& cjust_v, conflict_core& core) = 0;
+        virtual bool try_explain(pvar v, /* vector<signed_constraint> const& cjust_v, */ conflict_core& core) = 0;
     };
 
     class ex_polynomial_superposition : public explainer {
-        bool try_explain(pvar v, vector<signed_constraint> const& cjust_v, conflict_core& core) override;
+        bool try_explain(pvar v, /* vector<signed_constraint> const& cjust_v, */ conflict_core& core) override;
     };
 
 

src/math/polysat/justification.h

@@ -36,7 +36,7 @@ namespace polysat {
         bool is_unassigned() const { return m_kind == justification_k::unassigned; }
         bool is_propagation() const { return m_kind == justification_k::propagation; }
         justification_k kind() const { return m_kind; }
-        unsigned level() const { return m_level; }
+        unsigned level() const { /* SASSERT(!is_unassigned()); */ return m_level; }   // TODO: check why this assertion triggers...
         std::ostream& display(std::ostream& out) const;
     };
 

src/math/polysat/solver.cpp

@@ -634,15 +634,17 @@ namespace polysat {
         rational val = m_value[v];
         LOG_H3("Reverting decision: pvar " << v << " := " << val);
         SASSERT(m_justification[v].is_decision());
+        unsigned const lvl = m_justification[v].level();
 
         clause_ref lemma;
         if (m_conflict.is_bailout())
-            lemma = mk_fallback_lemma(m_justification[v].level());
+            lemma = mk_fallback_lemma(lvl);  // must call this before backjump
         else
-            lemma = m_conflict.build_lemma();
+            lemma = m_conflict.build_lemma(lvl - 1);
         m_conflict.reset();
 
-        backjump(m_justification[v].level()-1);
+        backjump(lvl - 1);
+
         // TODO: we need to decide_bool on the clause (learn_lemma takes care of this).
         //       if the lemma was asserting, then this will propagate the last literal. otherwise we do the enumerative guessing as normal.
         //       we need to exclude the current value of v. narrowing of the guessed constraint *should* take care of it but we cannot count on that.
@@ -724,12 +726,13 @@ namespace polysat {
         // - propagation of L' from L
         //      (L')^{L' \/ ¬L \/ ...}
         //      again L is in core, unless we core-reduced it away
+        unsigned const lvl = m_bvars.level(var);
 
         clause_ref reason;
         if (m_conflict.is_bailout())
-            reason = mk_fallback_lemma(m_bvars.level(var));
+            reason = mk_fallback_lemma(lvl);
         else
-            reason = m_conflict.build_lemma();
+            reason = m_conflict.build_lemma(lvl - 1);
         m_conflict.reset();
 
         bool contains_lit = std::any_of(reason->begin(), reason->end(), [lit](auto reason_lit) { return reason_lit == ~lit; });
@@ -754,7 +757,7 @@ namespace polysat {
         clause* lemma = m_bvars.lemma(var);  // need to grab this while 'lit' is still assigned
         SASSERT(lemma);
 
-        backjump(m_bvars.level(var) - 1);
+        backjump(lvl - 1);
 
         add_lemma(reason);
         propagate_bool(~lit, reason.get());