Track existing constraints with indexed_uint_set

src/math/polysat/conflict_core.cpp

@@ -16,21 +16,14 @@ Notes:
 
  TODO: try a final core reduction step or other core minimization
 
-
- 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.
 
+TODO: If we have e.g. 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.
+      (works currently if x is unassigned; for other cases we would need extra info from constraint::is_currently_false)
+
 --*/
 
 #include "math/polysat/conflict_core.h"
@@ -58,7 +51,7 @@ namespace polysat {
 
     conflict_core::~conflict_core() {}
 
-    constraint_manager& conflict_core::cm() { return s().m_constraints; }
+    constraint_manager& conflict_core::cm() const { return s().m_constraints; }
 
     std::ostream& conflict_core::display(std::ostream& out) const {
         char const* sep = "";
@@ -71,6 +64,19 @@ namespace polysat {
         return out;
     }
 
+    void conflict_core::reset() {
+        for (auto c : *this)
+            unset_mark(c.get());
+        m_constraints.reset();
+        m_literals.reset();
+        m_vars.reset();
+        m_conflict_var = null_var;
+        m_saturation_premises.reset();
+        m_bailout = false;
+        m_bailout_lemma.reset();
+        SASSERT(empty());
+    }
+
     /**
     * The constraint is false under the current assignment of variables.
     * The core is then the conjuction of this constraint and assigned variables.
@@ -108,17 +114,25 @@ namespace polysat {
         if (c->is_marked())
             return;
         set_mark(c.get());
-        m_constraints.push_back(c);
+        if (c->has_bvar())
+            insert_literal(c.blit());
+        else
+            m_constraints.push_back(c);
     }
 
     void conflict_core::insert(signed_constraint c, vector<signed_constraint> premises) {
         insert(c);
-        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).
+        m_saturation_premises.insert(c, std::move(premises));  // TODO: map doesn't have move-insertion, so this still copies the vector.
     }
 
     void conflict_core::remove(signed_constraint c) {
         unset_mark(c.get());       
-        m_constraints.erase(c);
+        if (c->has_bvar()) {
+            SASSERT(std::count(m_constraints.begin(), m_constraints.end(), c) == 0);
+            remove_literal(c.blit());
+        }
+        else
+            m_constraints.erase(c);
     }
 
     void conflict_core::replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> c_new_premises) {
@@ -169,7 +183,11 @@ namespace polysat {
 
     /** If the constraint c is a temporary constraint derived by core saturation, insert it (and recursively, its premises) into \Gamma */
     void conflict_core::keep(signed_constraint c) {
-        cm().ensure_bvar(c.get());
+        if (!c->has_bvar()) {
+            m_constraints.erase(c);
+            cm().ensure_bvar(c.get());
+            insert_literal(c.blit());
+        }
         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);
@@ -372,4 +390,13 @@ namespace polysat {
     bool conflict_core::is_bmarked(sat::bool_var b) const {
         return m_bvar2mark.get(b, false);
     }
+
+    void conflict_core::insert_literal(sat::literal lit) {
+        m_literals.insert(lit.to_uint());
+    }
+
+    void conflict_core::remove_literal(sat::literal lit) {
+        m_literals.remove(lit.to_uint());
+    }
+
 }

src/math/polysat/conflict_core.h

@@ -22,20 +22,18 @@ namespace polysat {
     class explainer;
     class inference_engine;
     class variable_elimination_engine;
+    class conflict_core_iterator;
 
     /** Conflict state, represented as core (~negation of clause). */
     class conflict_core {
-        vector<signed_constraint> m_constraints;  // constraints used as premises
+        signed_constraints m_constraints;   // new constraints used as premises
-        uint_set m_vars;                          // variable assignments used as premises
+        indexed_uint_set m_literals;        // set of boolean literals in the conflict
+        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;
 
-        // 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);
@@ -47,14 +45,16 @@ namespace polysat {
         void set_mark(constraint* c);
         void unset_mark(constraint* c);
 
+        void insert_literal(sat::literal lit);
+        void remove_literal(sat::literal lit);
 
         /** 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;
 
         solver* m_solver = nullptr;
-        solver& s() { return *m_solver; }
+        solver& s() const { return *m_solver; }
-        constraint_manager& cm();
+        constraint_manager& cm() const;
         scoped_ptr_vector<explainer> ex_engines;
         scoped_ptr_vector<variable_elimination_engine> ve_engines;
         scoped_ptr_vector<inference_engine> inf_engines;
@@ -65,27 +65,16 @@ namespace polysat {
         conflict_core(solver& s);
         ~conflict_core();
 
-        vector<signed_constraint> const& constraints() const { return m_constraints; }
         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_vars.empty() && conflict_var() == null_var;
+            return m_constraints.empty() && m_vars.empty() && m_literals.empty() && m_conflict_var == null_var;
         }
 
-        void reset() {
+        void reset();
-            for (auto c : m_constraints)
-                unset_mark(c.get());
-            m_constraints.reset();
-            m_vars.reset();
-            m_conflict_var = null_var;
-            m_saturation_premises.reset();
-            m_bailout = false;
-            m_bailout_lemma.reset();
-            SASSERT(empty());
-        }
 
         bool is_pmarked(pvar v) const;
         bool is_bmarked(sat::bool_var b) const;
@@ -123,13 +112,68 @@ namespace polysat {
         bool try_eliminate(pvar v);
         bool try_saturate(pvar v);
 
-        using const_iterator = decltype(m_constraints)::const_iterator;
+        using const_iterator = conflict_core_iterator;
-        const_iterator begin() { return constraints().begin(); }
+        const_iterator begin() const;
-        const_iterator end() { return constraints().end(); }
+        const_iterator end() const;
 
         std::ostream& display(std::ostream& out) const;
     };
 
     inline std::ostream& operator<<(std::ostream& out, conflict_core const& c) { return c.display(out); }
 
+
+    class conflict_core_iterator {
+        friend class conflict_core;
+
+        using it1_t = signed_constraints::const_iterator;
+        using it2_t = indexed_uint_set::iterator;
+
+        constraint_manager* m_cm;
+        it1_t m_it1;
+        it1_t m_end1;
+        it2_t m_it2;
+
+        conflict_core_iterator(constraint_manager& cm, it1_t it1, it1_t end1, it2_t it2):
+            m_cm(&cm), m_it1(it1), m_end1(end1), m_it2(it2) {}
+
+        static conflict_core_iterator begin(constraint_manager& cm, signed_constraints cs, indexed_uint_set lits) {
+            return {cm, cs.begin(), cs.end(), lits.begin()};
+        }
+
+        static conflict_core_iterator end(constraint_manager& cm, signed_constraints cs, indexed_uint_set lits) {
+            return {cm, cs.end(), cs.end(), lits.end()};
+        }
+
+    public:
+        using value_type = signed_constraint;
+        using difference_type = unsigned;
+        using pointer = signed_constraint const*;
+        using reference = signed_constraint const&;
+        using iterator_category = std::input_iterator_tag;
+
+        conflict_core_iterator& operator++() {
+            if (m_it1 != m_end1)
+                ++m_it1;
+            else
+                ++m_it2;
+            return *this;
+        }
+
+        signed_constraint operator*() const {
+            if (m_it1 != m_end1)
+                return *m_it1;
+            else
+                return m_cm->lookup(sat::to_literal(*m_it2));
+        }
+
+        bool operator==(conflict_core_iterator const& other) const {
+            return m_it1 == other.m_it1 && m_it2 == other.m_it2;
+        }
+
+        bool operator!=(conflict_core_iterator const& other) const { return !operator==(other); }
+    };
+
+
+    inline conflict_core::const_iterator conflict_core::begin() const { return conflict_core_iterator::begin(cm(), m_constraints, m_literals); }
+    inline conflict_core::const_iterator conflict_core::end() const { return conflict_core_iterator::end(cm(), m_constraints, m_literals); }
 }

src/math/polysat/constraint.h

@@ -29,6 +29,9 @@ namespace polysat {
     using constraint_eq = deref_eq<constraint>;
     using constraint_table = ptr_hashtable<constraint, constraint_hash, constraint_eq>;
 
+    using constraints = ptr_vector<constraint>;
+    using signed_constraints = vector<signed_constraint>;
+
     // Manage constraint lifetime, deduplication, and connection to boolean variables/literals.
     class constraint_manager {
         friend class constraint;

src/math/polysat/solver.h

@@ -66,9 +66,6 @@ namespace polysat {
         friend class inf_saturate;
         friend class constraint_manager;
 
-        typedef ptr_vector<constraint> constraints;
-        typedef vector<signed_constraint> signed_constraints;
-
         reslimit&                m_lim;
         params_ref               m_params;
         viable                   m_viable;   // viable sets per variable