Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat

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

@@ -16,6 +16,7 @@ Author:
 #include "math/polysat/solver.h"
 #include "math/polysat/log.h"
 #include "math/polysat/log_helper.h"
+#include "math/polysat/explain.h"
 #include "math/polysat/saturation.h"
 #include "math/polysat/variable_elimination.h"
 #include <algorithm>
@@ -24,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);
     }
@@ -79,6 +83,31 @@ namespace polysat {
         m_saturation_premises.insert(c, std::move(premises));  // TODO: map doesn't have move-insertion, so this still copies the vector. Maybe we want a clause_ref (but this doesn't work either since c doesn't have a boolean variable yet).
     }
 
+    void conflict_core::remove(signed_constraint c) {
+        m_constraints.erase(c);
+    }
+
+    void conflict_core::replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> c_new_premises) {
+        remove(c_old);
+        insert(c_new, c_new_premises);
+    }
+
+    void conflict_core::remove_var(pvar v) {
+        unsigned j = 0;
+        for (unsigned i = 0; i < m_constraints.size(); ++i)
+            if (m_constraints[i]->contains_var(v))
+                m_constraints[j++] = m_constraints[i];
+        m_constraints.shrink(j);
+    }
+
+    void conflict_core::keep(signed_constraint c) {
+        SASSERT(!c->has_bvar());
+        cm().ensure_bvar(c.get());
+        LOG("new constraint: " << c);
+        // Insert the temporary constraint from saturation into \Gamma.
+        handle_saturation_premises(c);
+    }
+
     void conflict_core::resolve(constraint_manager const& m, sat::bool_var var, clause const& cl) {
         // Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z
         //       clause: x \/ u \/ v
@@ -118,17 +147,14 @@ namespace polysat {
         auto& premises = it->m_value;
         clause_builder c_lemma(*m_solver);
         for (auto premise : premises) {
-            handle_saturation_premises(c);
+            handle_saturation_premises(premise);
             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).
+        m_solver->assign_bool(c.blit(), cl, nullptr);
-        // => add at the end and update pop_levels to replay appropriately
-        m_solver->assign_bool_backtrackable(c.blit(), cl, nullptr);
-        m_solver->activate_constraint(c);
     }
 
     /** Create fallback lemma that excludes the current search state */
@@ -169,13 +195,8 @@ namespace polysat {
         // TODO: try a final core reduction step?
 
         for (auto c : m_constraints) {
-            if (!c->has_bvar()) {
+            if (!c->has_bvar())
-                // temporary constraint -> keep it
+                keep(c);
-                cm().ensure_bvar(c.get());
-                LOG("new constraint: " << c);
-                // Insert the temporary constraint from saturation into \Gamma.
-                handle_saturation_premises(c);
-            }
             lemma.push(c);
         }
 
@@ -211,14 +232,26 @@ namespace polysat {
         // NOTE:
         // In the "standard" case where "v = val" is on the stack:
         //      - cjust_v contains true constraints
-        //      - core contains both false and true constraints... (originally only false ones, but additional true ones may come from saturation).
+        //      - 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?
+        //      - for now, we just pick a value. TODO: revise later
+        /*
+        if (conflict_var() == v) {
+            // Temporary assignment
+            // (actually we shouldn't just pick any value, but one that makes at least one constraint true...)
+            LOG_H1("WARNING: temporary assignment of conflict_var");
+            m_solver->assign_core(v, m_solver->m_value[v], justification::propagation(m_solver->m_level));
+        }
+        */
 
         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/conflict_core.h

@@ -18,6 +18,7 @@ Author:
 namespace polysat {
 
     class solver;
+    class explainer;
     class inference_engine;
     class variable_elimination_engine;
 
@@ -40,6 +41,7 @@ namespace polysat {
 
         solver* m_solver = nullptr;
         constraint_manager& cm();
+        scoped_ptr_vector<explainer> ex_engines;
         scoped_ptr_vector<variable_elimination_engine> ve_engines;
         scoped_ptr_vector<inference_engine> inf_engines;
 
@@ -77,7 +79,13 @@ namespace polysat {
 
         void insert(signed_constraint c);
         void insert(signed_constraint c, vector<signed_constraint> premises);
-        void remove(signed_constraint c) { NOT_IMPLEMENTED_YET(); }
+        void remove(signed_constraint c);
+        void replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> c_new_premises);
+
+        /** remove all constraints that contain the variable v */
+        void remove_var(pvar v);
+
+        void keep(signed_constraint c);
 
         /** Perform boolean resolution with the clause upon variable 'var'.
          * Precondition: core/clause contain complementary 'var'-literals.

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; }
 
+    signed_constraint ex_polynomial_superposition::resolve1(pvar v, signed_constraint c1, signed_constraint c2) {
+            // 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))
+                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)
-    bool ex_polynomial_superposition::try_explain(pvar v, /* vector<signed_constraint> const& cjust_v, */ conflict_core& core) {
+    // true = done, false = abort, undef = continue
-        // TODO: core saturation premises are from \Gamma (i.e., has_bvar)... but here we further restrict to the core; might need to revise
+    lbool ex_polynomial_superposition::try_explain1(pvar v, conflict_core& core) {
-        //       -- 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())
+            if (!is_positive_equality_over(v, c1))
-                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())
+                if (!is_positive_equality_over(v, c2))
-                    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.
+                signed_constraint c = resolve1(v, c1, c2);
-                // c1 is true, c2 is false
+                if (!c)
-                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;
-                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()))
                     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)
-//         DEBUG_CODE({
+            result = try_explain1(v, core);
-//             if (lemma) {
+        LOG("success? " << result);
-//                 LOG("New lemma: " << *lemma);
+        return result;
-//                 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;
     };
 
 

src/math/polysat/solver.cpp

@@ -155,7 +155,7 @@ namespace polysat {
         m_linear_solver.new_constraint(*c.get());
 #endif
         if (activate && !is_conflict())
-            activate_constraint_base(c);
+            propagate_bool(c.blit(), unit);
     }
 
     void solver::assign_eh(unsigned dep, bool is_true) {
@@ -191,6 +191,8 @@ namespace polysat {
         }
         linear_propagate();
         SASSERT(wlist_invariant());
+        if (!is_conflict())
+            SASSERT(assignment_invariant());
     }
 
     void solver::linear_propagate() {
@@ -208,9 +210,8 @@ namespace polysat {
     void solver::propagate(sat::literal lit) {
         LOG_H2("Propagate boolean literal " << lit);
         signed_constraint c = m_constraints.lookup(lit);
-        (void)c;
         SASSERT(c);
-        // c->narrow(*this);
+        activate_constraint(c);
     }
 
     void solver::propagate(pvar v) {
@@ -576,22 +577,10 @@ namespace polysat {
         if (!lemma)
             return;
         SASSERT(lemma->size() > 0);
-        SASSERT(m_conflict_level <= m_justification[v].level());  // ???
         lemma->set_justified_var(v);
-        clause* cl = lemma.get();
+        add_lemma(lemma);
-        add_lemma(std::move(lemma));
+        sat::literal lit = decide_bool(*lemma);
-        if (cl->size() == 1) {
+        SASSERT(lit != sat::null_literal);
-            sat::literal lit = (*cl)[0];
-            signed_constraint c = m_constraints.lookup(lit);
-            c->set_unit_clause(cl);
-            push_cjust(v, c);
-            activate_constraint_base(c);
-        }
-        else {
-            sat::literal lit = decide_bool(*cl);
-            SASSERT(lit != sat::null_literal);
-            signed_constraint c = m_constraints.lookup(lit);
-        }
     }
 
     // Guess a literal from the given clause; returns the guessed constraint
@@ -747,53 +736,23 @@ namespace polysat {
     void solver::decide_bool(sat::literal lit, clause& lemma) {
         push_level();
         LOG_H2("Decide boolean literal " << lit << " @ " << m_level);
-        assign_bool_backtrackable(lit, nullptr, &lemma);
+        assign_bool(lit, nullptr, &lemma);
     }
 
     void solver::propagate_bool(sat::literal lit, clause* reason) {
         LOG("Propagate boolean literal " << lit << " @ " << m_level << " by " << show_deref(reason));
         SASSERT(reason);
-        if (reason->size() == 1) {
+        assign_bool(lit, reason, nullptr);
-            SASSERT((*reason)[0] == lit);
-            signed_constraint c = m_constraints.lookup(lit);
-            // m_redundant.push_back(c);
-            activate_constraint_base(c);
-        }
-        else
-            assign_bool_backtrackable(lit, reason, nullptr);
     }
 
     /// Assign a boolean literal and put it on the search stack,
     /// and activate the corresponding constraint.
-    void solver::assign_bool_backtrackable(sat::literal lit, clause* reason, clause* lemma) {
+    void solver::assign_bool(sat::literal lit, clause* reason, clause* lemma) {
-        assign_bool_core(lit, reason, lemma);
+        LOG("Assigning boolean literal: " << lit);
+        m_bvars.assign(lit, m_level, reason, lemma);
 
         m_trail.push_back(trail_instr_t::assign_bool_i);
         m_search.push_boolean(lit);
-
-        signed_constraint c = m_constraints.lookup(lit);
-        activate_constraint(c);
-    }
-
-    /// Activate a constraint at the base level.
-    /// Used for external unit constraints and unit consequences.
-    void solver::activate_constraint_base(signed_constraint c) {
-        SASSERT(c);
-        LOG("\n" << *this);
-        // c must be in m_original or m_redundant so it can be deactivated properly when popping the base level
-        SASSERT_EQ(std::count(m_original.begin(), m_original.end(), c) + std::count(m_redundant.begin(), m_redundant.end(), c), 1);
-        // TODO: how is the boolean assignment for this undone? when we remove the constraint by popping a solver level.
-        //       if the constraint is deleted by popping it, then it's fine because we will remove the boolean variable.
-        //       however, we now dedup constraints so it might have been promoted to a lower level and thus live longer.
-        //       so this bool assignment needs to be backtrackable too...
-        assign_bool_core(c.blit(), nullptr, nullptr);
-        activate_constraint(c);
-    }
-
-    /// Assign a boolean literal
-    void solver::assign_bool_core(sat::literal lit, clause* reason, clause* lemma) {
-        LOG("Assigning boolean literal: " << lit);
-        m_bvars.assign(lit, m_level, reason, lemma);
     }
 
     /** 
@@ -817,7 +776,7 @@ namespace polysat {
     void solver::deactivate_constraint(signed_constraint c) {
         LOG("Deactivating constraint: " << c);
         erase_watch(c);
-        c->set_unit_clause(nullptr);
+        // c->set_unit_clause(nullptr);
     }
 
     void solver::backjump(unsigned new_level) {
@@ -846,6 +805,7 @@ namespace polysat {
         m_redundant_clauses.push_back(cl);
         if (cl->size() == 1) {
             signed_constraint c = m_constraints.lookup((*cl)[0]);
+            c->set_unit_clause(cl);
             insert_constraint(m_redundant, c);
         }
     }
@@ -994,6 +954,18 @@ namespace polysat {
         return true;
     }
 
+    /** Check that boolean assignment and constraint evaluation are consistent */
+    bool solver::assignment_invariant() {
+        for (sat::bool_var v = m_bvars.size(); v-- > 0; ) {
+            sat::literal lit(v);
+            if (m_bvars.value(lit) == l_true)
+                SASSERT(!m_constraints.lookup(lit).is_currently_false(*this));
+            if (m_bvars.value(lit) == l_false)
+                SASSERT(!m_constraints.lookup(lit).is_currently_true(*this));
+        }
+        return true;
+    }
+
     /// Check that all original constraints are satisfied by the current model.
     bool solver::verify_sat() {
         LOG_H1("Checking current model...");

src/math/polysat/solver.h

@@ -113,8 +113,6 @@ namespace polysat {
         svector<trail_instr_t>   m_trail;
         unsigned_vector          m_qhead_trail;
         unsigned_vector          m_cjust_trail;
-        ptr_vector<constraint>   m_activate_trail;
-
 
         unsigned_vector          m_base_levels;  // External clients can push/pop scope. 
 
@@ -158,10 +156,7 @@ namespace polysat {
         void pop_levels(unsigned num_levels);
         void pop_constraints(signed_constraints& cs);
 
-        void assign_bool_backtrackable(sat::literal lit, clause* reason, clause* lemma);
+        void assign_bool(sat::literal lit, clause* reason, clause* lemma);
-        void activate_constraint_base(signed_constraint c);
-        void assign_bool_core(sat::literal lit, clause* reason, clause* lemma);
-        // void assign_bool_base(sat::literal lit);
         void activate_constraint(signed_constraint c);
         void deactivate_constraint(signed_constraint c);
         sat::literal decide_bool(clause& lemma);
@@ -195,8 +190,6 @@ namespace polysat {
         void set_marks(conflict_core const& cc);
         void set_marks(constraint const& c);
 
-        unsigned                 m_conflict_level { 0 };
-
         bool can_decide() const { return !m_free_vars.empty(); }
         void decide();
         void decide(pvar v);
@@ -237,6 +230,7 @@ namespace polysat {
         bool invariant();
         static bool invariant(signed_constraints const& cs);
         bool wlist_invariant();
+        bool assignment_invariant();
         bool verify_sat();
 
     public: