update polynomial superposition

src/math/polysat/boolean.h

@@ -30,10 +30,10 @@ namespace polysat {
         unsigned_vector         m_marks;
         unsigned                m_clock { 0 };
 
+    public:
         // allocated size (not the number of active variables)
         unsigned size() const { return m_level.size(); }
 
-    public:
         sat::bool_var new_var();
         void del_var(sat::bool_var var);
 

src/math/polysat/conflict_core.cpp

@@ -25,9 +25,12 @@ namespace polysat {
 
     conflict_core::conflict_core(solver& s) {
         m_solver = &s;
+        ex_engines.push_back(alloc(ex_polynomial_superposition));
+        for (auto* engine : ex_engines)
+            engine->set_solver(s);
         ve_engines.push_back(alloc(ve_reduction));
         // ve_engines.push_back(alloc(ve_forbidden_intervals));
-        inf_engines.push_back(alloc(inf_polynomial_superposition));
+        // inf_engines.push_back(alloc(inf_polynomial_superposition));
         for (auto* engine : inf_engines)
             engine->set_solver(s);
     }
@@ -245,6 +248,10 @@ namespace polysat {
         for (auto c : cjust_v)
             insert(c);
 
+        for (auto* engine : ex_engines)
+            if (engine->try_explain(v, *this))
+                return true;
+
         // No value resolution method was successful => fall back to saturation and variable elimination
         while (true) {  // TODO: limit?
             // TODO: as a last resort, substitute v by m_value[v]?

src/math/polysat/constraint.h

@@ -99,7 +99,7 @@ namespace polysat {
         pdd lhs;
         pdd rhs;
         bool is_strict;
-        constraint const* src;
+        constraint const* src;  // TODO: should be signed_constraint now
         inequality(pdd const & lhs, pdd const & rhs, bool is_strict, constraint const* src):
             lhs(lhs), rhs(rhs), is_strict(is_strict), src(src) {}
     };

src/math/polysat/explain.cpp

@@ -19,108 +19,71 @@ namespace polysat {
 
     constraint_manager& explainer::cm() { return s().m_constraints; }
 
-    // TODO(later): check superposition into disequality again (see notes)
+    signed_constraint ex_polynomial_superposition::resolve1(pvar v, signed_constraint c1, signed_constraint c2) {
-    bool ex_polynomial_superposition::try_explain(pvar v, /* vector<signed_constraint> const& cjust_v, */ conflict_core& core) {
-        // 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)
-
-        // TODO: resolve multiple times... a single time might not be enough to eliminate the variable.
-
-        LOG_H3("Trying polynomial superposition...");
-        for (auto it1 = core.begin(); it1 != core.end(); ++it1) {
-            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;
-                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;
-
-                // TODO: separate method for this; then try_explain1 and try_explain* for multi-steps; replace the false constraint in the core.
             // c1 is true, c2 is false
+            SASSERT(c1.is_currently_true(s()));
+            SASSERT(c2.is_currently_false(s()));
             LOG("c1: " << c1);
             LOG("c2: " << c2);
             pdd a = c1->to_eq().p();
             pdd b = c2->to_eq().p();
             pdd r = a;
             if (!a.resolve(v, b, r) && !b.resolve(v, a, r))
-                    continue;
+                return {};
             unsigned const lvl = std::max(c1->level(), c2->level());
             signed_constraint c = cm().eq(lvl, r);
             LOG("resolved: " << c << "        currently false? " << c.is_currently_false(s()));
             if (!c.is_currently_false(s()))
+                return {};
+            return c;
+    }
+
+    bool ex_polynomial_superposition::is_positive_equality_over(pvar v, signed_constraint const& c) {
+        return c.is_positive() && c->is_eq() && c->contains_var(v);
+    }
+
+    // TODO(later): check superposition into disequality again (see notes)
+    // true = done, false = abort, undef = continue
+    lbool ex_polynomial_superposition::try_explain1(pvar v, conflict_core& core) {
+        for (auto it1 = core.begin(); it1 != core.end(); ++it1) {
+            signed_constraint c1 = *it1;
+            if (!is_positive_equality_over(v, c1))
+                continue;
+            if (!c1.is_currently_true(s()))
+                continue;
+
+            for (auto it2 = core.begin(); it2 != core.end(); ++it2) {
+                signed_constraint c2 = *it2;
+                if (!is_positive_equality_over(v, c2))
+                    continue;
+                if (!c2.is_currently_false(s()))
+                    continue;
+
+                signed_constraint c = resolve1(v, c1, c2);
+                if (!c)
                     continue;
                 vector<signed_constraint> premises;
                 premises.push_back(c1);
                 premises.push_back(c2);
+                core.replace(c2, c, std::move(premises));
                 if (!c->contains_var(v)) {
-                    core.reset(); // TODO: doesn't work; this removes the premises as well... / instead: remove the false one.
+                    core.keep(c);
-                    core.insert(c, std::move(premises));
+                    core.remove_var(v);
-                    return true;
+                    return l_true;
-                } else {
+                } else
-                    core.insert(c, std::move(premises));
+                    return l_undef;
             }
         }
+        return l_false;
     }
 
-        return false;
+    bool ex_polynomial_superposition::try_explain(pvar v, conflict_core& core) {
+        LOG_H3("Trying polynomial superposition...");
+        lbool result = l_undef;
+        while (result == l_undef)
+            result = try_explain1(v, core);
+        LOG("success? " << result);
+        return result;
     }
 
-
-
-
-
-//         DEBUG_CODE({
-//             if (lemma) {
-//                 LOG("New lemma: " << *lemma);
-//                 for (auto* c : lemma->new_constraints()) {
-//                     LOG("New constraint: " << show_deref(c));
-//                 }
-//                 // All constraints in the lemma must be false in the conflict state
-//                 for (auto lit : lemma->literals()) {
-//                     if (m_solver.m_bvars.value(lit) == l_false)
-//                         continue;
-//                     SASSERT(m_solver.m_bvars.value(lit) != l_true);
-//                     constraint* c = m_solver.m_constraints.lookup(lit.var());
-//                     SASSERT(c);
-//                     tmp_assign _t(c, lit);
-//                     // if (c->is_currently_true(m_solver)) {
-//                     //     LOG("ERROR: constraint is true: " << show_deref(c));
-//                     //     SASSERT(false);
-//                     // }
-//                     // SASSERT(!c->is_currently_true(m_solver));
-//                     // SASSERT(c->is_currently_false(m_solver));   // TODO: pvar v may not have a value at this point...
-//                 }
-//             }
-//             else {
-//                 LOG("No lemma");
-//             }
-//         });
-
-//         m_var = null_var;
-//         m_cjust_v.reset();
-//         return lemma;
-//     }
-
-
-
-
 }

src/math/polysat/explain.h

@@ -35,7 +35,12 @@ namespace polysat {
     };
 
     class ex_polynomial_superposition : public explainer {
-        bool try_explain(pvar v, /* vector<signed_constraint> const& cjust_v, */ conflict_core& core) override;
+    private:
+        bool is_positive_equality_over(pvar v, signed_constraint const& c);
+        signed_constraint resolve1(pvar v, signed_constraint c1, signed_constraint c2);
+        lbool try_explain1(pvar v, conflict_core& core);
+    public:
+        bool try_explain(pvar v, conflict_core& core) override;
     };