reorganize variable tracking for lemmas

this is going to break a bunch

src/math/polysat/conflict_core.cpp

@@ -20,6 +20,16 @@ Notes:
  TODO: maybe implement by marking literals instead (like SAT solvers are doing); if we need to iterate, keep an indexed_uint_set (from util/uint_set.h)
        (i.e., instead of keeping an explicit list of constraints as core, we just mark them.)
        (we still need the list though, for new/temporary constraints.)
+       The approach would be as follows:
+       m_vars - set of variables used in conflict
+       m_constraints - set of new constraints used in conflict
+       indexed_uint_set - for Boolean variables that are in the conflict
+       When iterating over the core acessing the uint_set would require some support
+
+TODO: fallback lemma is redundant:
+      The core lemma uses m_vars and m_conflict directly instead of walking the stack.
+      It should be an invariant that the core is false (the negation of the core is valid modulo assertions).
+      The fallback lemma prunes at least the last value assignment.
 
 --*/
 
@@ -48,34 +58,44 @@ namespace polysat {
 
     conflict_core::~conflict_core() {}
 
-    constraint_manager& conflict_core::cm() { return m_solver->m_constraints; }
+    constraint_manager& conflict_core::cm() { return s().m_constraints; }
 
     std::ostream& conflict_core::display(std::ostream& out) const {
         bool first = true;
-        for (auto c : m_constraints) {
-            if (first)
-                first = false;
-            else
-                out << "  ;  ";
-            out << c;
-        }
-        if (m_needs_model)
-            out << "  ;  + current model";
+        for (auto c : m_constraints) 
+            out << (first ? "" : " ; ") << c, first = false;        
+        if (!m_vars.empty())
+            out << " vars";
+        for (auto v : m_vars)
+            out << "  " << v;
         return out;
     }
 
+    /**
+    * The constraint is false under the current assignment of variables.
+    * The core is then the conjuction of this constraint and assigned variables.
+    */
     void conflict_core::set(signed_constraint c) {
         LOG("Conflict: " << c);
         SASSERT(empty());
-        m_needs_model = true;
         insert(c);
+        for (auto v : c->vars())
+            if (s().is_assigned(v))
+                m_vars.insert(v);
     }
 
+    /**
+    * The variable v cannot be assigned.
+    * The conflict is the set of justifications accumulated for the viable values for v.
+    * These constraints are (in the current form) not added to the core, but passed directly 
+    * to the forbidden interval module.
+    * A consistent approach could be to add these constraints to the core and then also include the
+    * variable assignments.
+    */
     void conflict_core::set(pvar v) {
         LOG("Conflict: v" << v);
         SASSERT(empty());
         m_conflict_var = v;
-        m_needs_model = true;
     }
 
     void conflict_core::insert(signed_constraint c) {
@@ -86,6 +106,9 @@ namespace polysat {
         if (c.is_always_true())
             return;
         SASSERT(!c.is_always_false());
+        if (c->is_marked())
+            return;
+        set_mark(c.get());
         m_constraints.push_back(c);
     }
 
@@ -95,6 +118,7 @@ namespace polysat {
     }
 
     void conflict_core::remove(signed_constraint c) {
+        unset_mark(c.get());       
         m_constraints.erase(c);
     }
 
@@ -106,8 +130,11 @@ namespace polysat {
     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];
+            if (m_constraints[i]->contains_var(v))
+                unset_mark(m_constraints[i].get());
+            else
+                m_constraints[j++] = m_constraints[i];           
+                
         m_constraints.shrink(j);
     }
 
@@ -136,14 +163,17 @@ namespace polysat {
         });
 
         int j = 0;
-        for (auto c : m_constraints)
+        for (auto c : m_constraints) {
             if (c->bvar() != var)
                 m_constraints[j++] = c;
+            else
+                unset_mark(c.get());
+        }
         m_constraints.shrink(j);
 
         for (sat::literal lit : cl)
             if (lit.var() != var)
-                m_constraints.push_back(m.lookup(~lit));
+                insert(m.lookup(~lit));
     }
 
     /** If the constraint c is a temporary constraint derived by core saturation, insert it (and recursively, its premises) into \Gamma */
@@ -154,20 +184,20 @@ namespace polysat {
             return;
         unsigned active_level = 0;
         auto& premises = it->m_value;
-        clause_builder c_lemma(*m_solver);
+        clause_builder c_lemma(s());
         for (auto premise : premises) {
             cm().ensure_bvar(premise.get());
             // keep(premise);
             handle_saturation_premises(premise);
             SASSERT(premise->has_bvar());
             c_lemma.push(~premise.blit());
-            active_level = std::max(active_level, m_solver->m_bvars.level(premise.blit()));
+            active_level = std::max(active_level, s().m_bvars.level(premise.blit()));
         }
         c_lemma.push(c.blit());
         clause* cl = cm().store(c_lemma.build());
         if (cl->size() == 1)
             c->set_unit_clause(cl);
-        m_solver->propagate_bool_at(active_level, c.blit(), cl);
+        s().propagate_bool_at(active_level, c.blit(), cl);
     }
 
     /** Create fallback lemma that excludes the current search state */
@@ -178,18 +208,18 @@ namespace polysat {
     */
     clause_builder conflict_core::build_fallback_lemma(unsigned lvl) {
         LOG_H3("Creating fallback lemma for level " << lvl);
-        LOG_V("m_search: " << m_solver->m_search);
+        LOG_V("m_search: " << s().m_search);
         clause_builder lemma(*m_solver);
         unsigned todo = lvl;
         unsigned i = 0;
         while (todo > 0) {
-            auto const& item = m_solver->m_search[i++];
-            if (!m_solver->is_decision(item))
+            auto const& item = s().m_search[i++];
+            if (!s().is_decision(item))
                 continue;
             LOG_V("Adding: " << item);
             if (item.is_assignment()) {
                 pvar v = item.var();
-                auto c = ~cm().eq(m_solver->var(v) - m_solver->m_value[v]);
+                auto c = ~cm().eq(s().var(v) - s().m_value[v]);
                 cm().ensure_bvar(c.get());
                 lemma.push(c.blit());
             } else {
@@ -213,27 +243,18 @@ namespace polysat {
             lemma.push(~c);
         }
 
-
-        // TODO: need to revisit this for when there are literals obtained by semantic propagation 
-        if (m_needs_model) {
-            // TODO: add equalities corresponding to current model.
-            //       until we properly track variables (use marks from solver?), we just use all of them (reverted decision and the following ones should have been popped from the stack)
-            uint_set vars;
-            for (auto c : m_constraints)
-                for (pvar v : c->vars())
-                    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].is_unassigned())
-                    continue;
-                if (m_solver->m_justification[v].level() > model_level)
-                    continue;
-                auto diseq = ~cm().eq(m_solver->var(v) - m_solver->m_value[v]);
-                cm().ensure_bvar(diseq.get());
-                lemma.push(diseq);
-            }
-        }
+        for (unsigned v : m_vars) {
+            if (!is_pmarked(v))
+                continue;
+            // SASSERT(!s().is_assigned());  // TODO: why does this trigger????
+            if (!s().is_assigned())
+                continue;
+            if (s().m_justification[v].level() > model_level)
+                continue;
+            auto diseq = ~cm().eq(s().var(v) - s().m_value[v]);
+            cm().ensure_bvar(diseq.get());
+            lemma.push(diseq);
+        }        
 
         return lemma;
     }
@@ -252,29 +273,21 @@ namespace polysat {
         // 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?).
-        // 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.
-        //      - 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));
-        }
-        */
+
         if (conflict_var() == v) {
             clause_builder lemma(s());
             forbidden_intervals fi;
-            if (fi.perform(s(), v, *this, lemma)) {
+            if (fi.perform(s(), v, cjust_v, lemma)) {
                 set_bailout();
                 m_bailout_lemma = std::move(lemma);
                 return true;
             }
         }
 
-        for (auto c : cjust_v)
-            insert(c);
+        m_vars.remove(v);
+
+        for (auto c : cjust_v) 
+            insert(c);        
 
         for (auto* engine : ex_engines)
             if (engine->try_explain(v, *this))
@@ -288,6 +301,7 @@ namespace polysat {
             if (try_eliminate(v))
                 return true;
         }
+        m_vars.insert(v);
         return false;
     }
 
@@ -298,7 +312,7 @@ namespace polysat {
         if (!has_v)
             return true;
         for (auto* engine : ve_engines)
-            if (engine->perform(*m_solver, v, *this))
+            if (engine->perform(s(), v, *this))
                 return true;
         return false;
     }
@@ -309,4 +323,62 @@ namespace polysat {
                 return true;
         return false;
     }
+
+    void conflict_core::set_mark(constraint* c) {
+        if (c->is_marked())
+            return;
+        bool bool_propagated = c->has_bvar() && s().m_bvars.is_assigned(c->bvar());
+        c->set_mark();
+        if (c->has_bvar())
+            set_bmark(c->bvar());    
+        if (bool_propagated)
+            c->set_bool_propagated();
+        else 
+            for (auto v : c->vars())
+                inc_pref(v);
+    }
+
+    void conflict_core::unset_mark(constraint* c) {
+        if (!c->is_marked())
+            return;
+        c->unset_mark();
+        if (c->has_bvar())
+            unset_bmark(c->bvar());
+        if (c->is_bool_propagated())
+            c->unset_bool_propagated();
+        else
+            for (auto v : c->vars())
+                dec_pref(v);
+    }
+
+    void conflict_core::inc_pref(pvar v) {
+        if (v >= m_pvar2count.size())
+            m_pvar2count.resize(v + 1);
+        m_pvar2count[v]++;
+    }
+
+    void conflict_core::dec_pref(pvar v) {
+        SASSERT(m_pvar2count[v] > 0);
+        m_pvar2count[v]--;
+    }
+
+    bool conflict_core::is_pmarked(pvar v) const {
+        return m_pvar2count.get(v, 0) > 0;
+    }
+
+    void conflict_core::set_bmark(sat::bool_var b) {
+        if (b >= m_bvar2mark.size())
+            m_bvar2mark.resize(b + 1);
+        SASSERT(!m_bvar2mark[b]);
+        m_bvar2mark[b] = true;
+    }
+
+    void conflict_core::unset_bmark(sat::bool_var b) {
+        SASSERT(m_bvar2mark[b]);
+        m_bvar2mark[b] = false;
+    }
+
+    bool conflict_core::is_bmarked(sat::bool_var b) const {
+        return m_bvar2mark.get(b, false);
+    }
 }

src/math/polysat/conflict_core.h

@@ -25,18 +25,29 @@ namespace polysat {
 
     /** Conflict state, represented as core (~negation of clause). */
     class conflict_core {
-        vector<signed_constraint> m_constraints;
+        vector<signed_constraint> m_constraints;  // constraints used as premises
+        uint_set m_vars;                          // variable assignments used as premises
 
         // If this is not null_var, the conflict was due to empty viable set for this variable.
         // Can be treated like "v = x" for any value x.
         pvar m_conflict_var = null_var;
 
-        /** True iff the conflict depends on the current variable assignment. (If so, additional constraints must be added to the final learned clause.) */
-        bool m_needs_model = false;
         // NOTE: for now we keep this simple implementation.
         //       The drawback is that we may get weaker lemmas in some cases (but they are still correct).
         //       For example: if we have 4x+y=2 and y=0, then we have a conflict no matter the value of x, so we should drop x=? from the core.
 
+        unsigned_vector m_pvar2count;             // reference count of variables
+        void inc_pref(pvar v);
+        void dec_pref(pvar v);
+
+        bool_vector m_bvar2mark;                  // mark of Boolean variables
+        void set_bmark(sat::bool_var b);
+        void unset_bmark(sat::bool_var b);
+
+        void set_mark(constraint* c);
+        void unset_mark(constraint* c);
+
+
         /** Whether we are in a bailout state. We enter a bailout state when we give up on proper conflict resolution.  */
         bool m_bailout = false;
         std::optional<clause_builder> m_bailout_lemma;
@@ -56,19 +67,20 @@ namespace polysat {
         ~conflict_core();
 
         vector<signed_constraint> const& constraints() const { return m_constraints; }
-        bool needs_model() const { return m_needs_model; }
         pvar conflict_var() const { return m_conflict_var; }
 
         bool is_bailout() const { return m_bailout; }
         void set_bailout() { SASSERT(!is_bailout()); m_bailout = true; }
 
         bool empty() const {
-            return m_constraints.empty() && !m_needs_model && m_conflict_var == null_var;
+            return m_constraints.empty() && m_vars.empty() && conflict_var() == null_var;
         }
 
         void reset() {
+            for (auto c : m_constraints)
+                unset_mark(c.get());
             m_constraints.reset();
-            m_needs_model = false;
+            m_vars.reset();
             m_conflict_var = null_var;
             m_saturation_premises.reset();
             m_bailout = false;
@@ -76,6 +88,9 @@ namespace polysat {
             SASSERT(empty());
         }
 
+        bool is_pmarked(pvar v) const;
+        bool is_bmarked(sat::bool_var b) const;
+
         /** conflict because the constraint c is false under current variable assignment */
         void set(signed_constraint c);
         /** conflict because there is no viable value for the variable v */

src/math/polysat/constraint.h

@@ -121,6 +121,8 @@ namespace polysat {
         ckind_t             m_kind;
         unsigned_vector     m_vars;
         bool                m_is_external = false;
+        bool                m_is_marked = false;
+        bool                m_is_bool_propagated = false;
         /** The boolean variable associated to this constraint, if any.
          *  If this is not null_bool_var, then the constraint corresponds to a literal on the assignment stack.
          *  Convention: the plain constraint corresponds the positive sat::literal.
@@ -169,6 +171,14 @@ namespace polysat {
         void set_external() { m_is_external = true; }
         void unset_external() { m_is_external = false; }
         bool is_external() const { return m_is_external; }
+
+        void set_mark() { m_is_marked = true; }
+        void unset_mark() { m_is_marked = false; }
+        bool is_marked() const { return m_is_marked; }
+
+        void set_bool_propagated() { m_is_bool_propagated = true; }
+        void unset_bool_propagated() { m_is_bool_propagated = false; }
+        bool is_bool_propagated() { return m_is_bool_propagated;  }
     };
 
     inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }

src/math/polysat/explain.cpp

@@ -20,26 +20,26 @@ 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_H3("Resolving upon v" << v);
-            LOG("c1: " << c1);
-            LOG("c2: " << c2);
-            pdd a = c1->to_ule().p();
-            pdd b = c2->to_ule().p();
-            pdd r = a;
-            if (!a.resolve(v, b, r) && !b.resolve(v, a, r))
-                return {};
-            // Only keep result if the degree in c2 was reduced.
-            // (this condition might be too strict, but we use it for now to prevent looping)
-            if (b.degree(v) <= r.degree(v))
-                return {};
-            signed_constraint c = cm().eq(r);
-            LOG("resolved: " << c << "        currently false? " << c.is_currently_false(s()));
-            if (!c.is_currently_false(s()))
-                return {};
-            return c;
+        // c1 is true, c2 is false
+        SASSERT(c1.is_currently_true(s()));
+        SASSERT(c2.is_currently_false(s()));
+        LOG_H3("Resolving upon v" << v);
+        LOG("c1: " << c1);
+        LOG("c2: " << c2);
+        pdd a = c1->to_ule().p();
+        pdd b = c2->to_ule().p();
+        pdd r = a;
+        if (!a.resolve(v, b, r) && !b.resolve(v, a, r))
+            return {};
+        // Only keep result if the degree in c2 was reduced.
+        // (this condition might be too strict, but we use it for now to prevent looping)
+        if (b.degree(v) <= r.degree(v))
+            return {};
+        signed_constraint c = cm().eq(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) {

src/math/polysat/forbidden_intervals.cpp

@@ -79,13 +79,13 @@ namespace polysat {
         lemma.push(~src);
     }
 
-    bool forbidden_intervals::perform(solver& s, pvar v, conflict_core& core, clause_builder& lemma) {
+    bool forbidden_intervals::perform(solver& s, pvar v, vector<signed_constraint> const& just, clause_builder& lemma) {
 
         // Extract forbidden intervals from conflicting constraints
         vector<fi_record> records;
         rational longest_len;
         unsigned longest_i = UINT_MAX;
-        for (signed_constraint c : core) {
+        for (signed_constraint c : just) {
             LOG_H3("Computing forbidden interval for: " << c);
             eval_interval interval = eval_interval::full();
             signed_constraint neg_cond;

src/math/polysat/forbidden_intervals.h

@@ -23,6 +23,6 @@ namespace polysat {
         void full_interval_conflict(signed_constraint c, signed_constraint neg_cond, clause_builder& lemma);
         bool get_interval(solver& s, signed_constraint const& c, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond);
     public:
-        bool perform(solver& s, pvar v, conflict_core& core, clause_builder& lemma);
+        bool perform(solver& s, pvar v, vector<signed_constraint> const& just, clause_builder& lemma);
     };
 }

src/math/polysat/saturation.cpp

@@ -61,9 +61,9 @@ namespace polysat {
         if (crit.as_signed_constraint().is_currently_false(s()) && c.is_currently_true(s()))
             return false;
         core.insert(c);
-        reason.push(c);
-        core.remove(crit.as_signed_constraint());
+        reason.push(c);        
         s().propagate_bool(c.blit(), reason.build().get());
+        core.remove(crit.as_signed_constraint()); // needs to be after propagation so we know it is propagated
         return true;
     }
 

src/math/polysat/solver.cpp

@@ -418,21 +418,6 @@ namespace polysat {
         m_conflict.set(v);
     }
 
-    void solver::set_marks(conflict_core const& cc) {
-        if (cc.conflict_var() != null_var)
-            set_mark(cc.conflict_var());
-        for (auto c : cc.constraints())
-            if (c)
-                set_marks(*c);
-    }
-
-    void solver::set_marks(constraint const& c) {
-        if (c.has_bvar())
-            m_bvars.set_mark(c.bvar());
-        for (auto v : c.vars())
-            set_mark(v);
-    }
-
     /**
      * Conflict resolution.
      * - m_conflict are constraints that are infeasible in the current assignment.
@@ -460,15 +445,11 @@ namespace polysat {
 
         SASSERT(is_conflict());
 
-        reset_marks();
-        set_marks(m_conflict);
         // TODO: subsequent changes to the conflict should update the marks incrementally
 
         if (m_conflict.conflict_var() != null_var) {
             // This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack.
             resolve_value(m_conflict.conflict_var());
-            reset_marks();
-            set_marks(m_conflict);
         }
 
         search_iterator search_it(m_search);
@@ -479,7 +460,7 @@ namespace polysat {
                 // Resolve over variable assignment
                 pvar v = item.var();
                 LOG_H2("Working on pvar v" << v);
-                if (!is_marked(v))
+                if (!m_conflict.is_pmarked(v))
                     continue;
                 justification& j = m_justification[v];
                 LOG("Justification: " << j);
@@ -491,8 +472,6 @@ namespace polysat {
                 }
                 SASSERT(j.is_propagation());
                 resolve_value(v);
-                reset_marks();
-                set_marks(m_conflict);
             }
             else {
                 // Resolve over boolean literal
@@ -500,7 +479,7 @@ namespace polysat {
                 sat::literal const lit = item.lit();
                 LOG_H2("Working on blit " << lit);
                 sat::bool_var const var = lit.var();
-                if (!m_bvars.is_marked(var))
+                if (!m_conflict.is_bmarked(var))
                     continue;
                 if (m_bvars.level(var) <= base_level())
                     break;
@@ -508,10 +487,9 @@ namespace polysat {
                     revert_bool_decision(lit);
                     return;
                 }
+                
                 SASSERT(m_bvars.is_propagation(var));
                 resolve_bool(lit);
-                reset_marks();
-                set_marks(m_conflict);
             }
         }
         report_unsat();
@@ -803,18 +781,7 @@ namespace polysat {
         LOG_V("INSERTING: " << c);
         cs.push_back(c);
         SASSERT(invariant(cs)); 
-    }
-    
-    void solver::reset_marks() {
-        m_bvars.reset_marks();
-        LOG_V("-------------------------- (reset variable marks)");
-        m_marks.reserve(m_vars.size());
-        m_clock++;
-        if (m_clock != 0)
-            return;
-        m_clock++;
-        m_marks.fill(0);        
-    }
+    }   
 
     void solver::push() {
         LOG("Push user scope");

src/math/polysat/solver.h

@@ -180,15 +180,6 @@ namespace polysat {
         void set_conflict(signed_constraint c);
         void set_conflict(pvar v);
 
-        unsigned_vector m_marks;
-        unsigned        m_clock { 0 };
-        void reset_marks();
-        bool is_marked(pvar v) const { return m_clock == m_marks[v]; }
-        void set_mark(pvar v) { LOG_V("Marking: v" << v); m_marks[v] = m_clock; }
-
-        void set_marks(conflict_core const& cc);
-        void set_marks(constraint const& c);
-
         bool can_decide() const { return !m_free_vars.empty(); }
         void decide();
         void decide(pvar v);