From 63031548cbf09a60ee0c1aefd4547c00d8978ef4 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 11 Apr 2022 15:00:06 +0200
Subject: [PATCH] Store only literals in the conflict state

---
 src/math/polysat/clause_builder.cpp           |   2 -
 src/math/polysat/conflict.cpp                 | 121 ++++++------------
 src/math/polysat/conflict.h                   |  57 +++------
 src/math/polysat/constraint.cpp               |   2 +
 src/math/polysat/constraint.h                 |  16 +--
 src/math/polysat/explain.cpp                  |   2 -
 src/math/polysat/search_state.cpp             |   1 -
 src/math/polysat/simplify.cpp                 |   4 +-
 src/math/polysat/solver.cpp                   |  10 +-
 .../polysat/univariate/univariate_solver.cpp  |   3 +
 10 files changed, 73 insertions(+), 145 deletions(-)

diff --git a/src/math/polysat/clause_builder.cpp b/src/math/polysat/clause_builder.cpp
index cc8770f05..a6a4f4f44 100644
--- a/src/math/polysat/clause_builder.cpp
+++ b/src/math/polysat/clause_builder.cpp
@@ -77,8 +77,6 @@ namespace polysat {
     void clause_builder::push_new(signed_constraint c) {
         if (c.is_always_false())  // filter out trivial constraints such as "4 < 2" (may come in from forbidden intervals)
             return;
-        if (!c->has_bvar())
-            m_solver->m_constraints.ensure_bvar(c.get());
         push(c);
     }
 }
diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index a261b4024..e142fe47c 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -60,10 +60,16 @@ namespace polysat {
         return out;
     }
 
+    bool conflict::empty() const {
+        return m_literals.empty()
+            && m_vars.empty()
+            && m_bail_vars.empty()
+            && m_conflict_var == null_var;
+    }
+
     void conflict::reset() {
         for (auto c : *this)
             unset_mark(c);
-        m_constraints.reset();
         m_literals.reset();
         m_vars.reset();
         m_bail_vars.reset();
@@ -135,19 +141,15 @@ namespace polysat {
     void conflict::insert(signed_constraint c) {
         if (c.is_always_true())
             return;        
-        if (c->is_marked())
+        if (is_marked(c))
             return;
         LOG("inserting: " << c);
         SASSERT(!c->vars().empty());
         set_mark(c);
-        if (c->has_bvar())
-            insert_literal(c.blit());
-        else
-            m_constraints.push_back(c);
+        m_literals.insert(c.blit().index());
     }
 
     void conflict::propagate(signed_constraint c) {
-        cm().ensure_bvar(c.get());
         switch (c.bvalue(s)) {
         case l_undef:
             s.assign_eval(c.blit());
@@ -175,13 +177,11 @@ namespace polysat {
      * Ensure that c is assigned and justified
      */
     void conflict::insert(signed_constraint c, vector<signed_constraint> const& premises) {
-        keep(c);
-
+        // keep(c);
         clause_builder c_lemma(s);
         for (auto premise : premises) {
             LOG_H3("premise: " << premise);
-            keep(premise);
-            SASSERT(premise->has_bvar());
+            // keep(premise);
             SASSERT(premise.bvalue(s) != l_false);         
             c_lemma.push(~premise.blit());
         }
@@ -194,12 +194,8 @@ namespace polysat {
     }
 
     void conflict::remove(signed_constraint c) {
-        SASSERT(!c->has_bvar() || std::count(m_constraints.begin(), m_constraints.end(), c) == 0);
         unset_mark(c);       
-        if (c->has_bvar())             
-            remove_literal(c.blit());        
-        else
-            m_constraints.erase(c);
+        m_literals.remove(c.blit().index());
     }
 
     void conflict::replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> const& c_new_premises) {
@@ -207,12 +203,12 @@ namespace polysat {
         insert(c_new, c_new_premises);
     }
 
+    bool conflict::contains(signed_constraint c) const {
+        return m_literals.contains(c.blit().index());
+    }
 
-    bool conflict::contains(signed_constraint c) {
-        if (c->has_bvar())
-            return m_literals.contains(c.blit().index());
-        else
-            return m_constraints.contains(c);
+    bool conflict::contains(sat::literal lit) const {
+        return m_literals.contains(lit.index());
     }
 
     void conflict::set_bailout() {
@@ -228,14 +224,12 @@ namespace polysat {
 
         SASSERT(lit != sat::null_literal);
         SASSERT(~lit != sat::null_literal);
-        SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](signed_constraint const& c){ return !c->has_bvar(); }));
-        SASSERT(contains_literal(lit));
+        SASSERT(contains(lit));
         SASSERT(std::count(cl.begin(), cl.end(), lit) > 0);
-        SASSERT(!contains_literal(~lit));
+        SASSERT(!contains(~lit));
         SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0);
         
-        remove_literal(lit);        
-        unset_mark(s.lit2cnstr(lit));         
+        remove(s.lit2cnstr(lit));
         for (sat::literal lit2 : cl)
             if (lit2 != lit)
                 insert(s.lit2cnstr(~lit2));
@@ -247,9 +241,8 @@ namespace polysat {
 
         SASSERT(lit != sat::null_literal);
         SASSERT(~lit != sat::null_literal);
-        SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](signed_constraint const& c){ return !c->has_bvar(); }));
-        SASSERT(contains_literal(lit));
-        SASSERT(!contains_literal(~lit));
+        SASSERT(contains(lit));
+        SASSERT(!contains(~lit));
 
         signed_constraint c = s.lit2cnstr(lit);
         bool has_decision = false;
@@ -260,35 +253,19 @@ namespace polysat {
         if (!has_decision) {
             remove(c);
             for (pvar v : c->vars()) 
-                if (s.is_assigned(v)) 
+                if (s.is_assigned(v)) {
+                    // TODO: 'lit' was propagated at level 'lvl'; can we here ignore variables above that?
+                    SASSERT(s.get_level(v) <= lvl);
                     m_vars.insert(v);            
+                }
         }
     }
 
-    /** 
-     * If the constraint c is a temporary constraint derived by core saturation, 
-     * insert it (and recursively, its premises) into \Gamma 
-     */
-    void conflict::keep(signed_constraint c) {
-        if (c->has_bvar())
-            return;
-        LOG_H3("keeping: " << c);
-        remove(c);
-        cm().ensure_bvar(c.get());
-        insert(c);        
-    }
-
     clause_builder conflict::build_lemma() {
-        // SASSERT(std::all_of(m_vars.begin(), m_vars.end(), [&](pvar v) { return s.is_assigned(v); }));
-        SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](signed_constraint const& c) { return !c->has_bvar(); }));
-
         LOG_H3("Build lemma from core");
         LOG("core: " << *this);
         clause_builder lemma(s);
 
-        while (!m_constraints.empty()) 
-            keep(m_constraints.back());
-
         for (auto c : *this)
             minimize_vars(c);
 
@@ -297,7 +274,6 @@ namespace polysat {
 
         for (unsigned v : m_vars) {
             auto eq = s.eq(s.var(v), s.get_value(v));
-            cm().ensure_bvar(eq.get());
             if (eq.bvalue(s) == l_undef) 
                 s.assign_eval(eq.blit());            
             lemma.push(~eq);
@@ -410,50 +386,27 @@ namespace polysat {
     }
 
     void conflict::set_mark(signed_constraint c) {
-        if (c->is_marked())
-            return;
-        c->set_mark();
-        if (c->has_bvar())
-            set_bmark(c->bvar());    
-    }
-
-    /**
-     * unset marking on the constraint, but keep variable dependencies.
-     */
-    void conflict::unset_mark(signed_constraint c) {
-        if (!c->is_marked())
-            return;
-        c->unset_mark();
-        if (c->has_bvar())
-            unset_bmark(c->bvar());
-    }
-
-    void conflict::set_bmark(sat::bool_var b) {
+        sat::bool_var b = c->bvar();
         if (b >= m_bvar2mark.size())
             m_bvar2mark.resize(b + 1);
         SASSERT(!m_bvar2mark[b]);
         m_bvar2mark[b] = true;
     }
 
-    void conflict::unset_bmark(sat::bool_var b) {
+    /**
+     * unset marking on the constraint, but keep variable dependencies.
+     */
+    void conflict::unset_mark(signed_constraint c) {
+        sat::bool_var b = c->bvar();
         SASSERT(m_bvar2mark[b]);
         m_bvar2mark[b] = false;
     }
 
-    bool conflict::is_bmarked(sat::bool_var b) const {
+    bool conflict::is_marked(signed_constraint c) const {
+        return is_marked(c->bvar());
+    }
+
+    bool conflict::is_marked(sat::bool_var b) const {
         return m_bvar2mark.get(b, false);
     }
-
-    bool conflict::contains_literal(sat::literal lit) const {
-        return m_literals.contains(lit.to_uint());
-    }
-
-    void conflict::insert_literal(sat::literal lit) {
-        m_literals.insert(lit.to_uint());
-    }
-
-    void conflict::remove_literal(sat::literal lit) {
-        m_literals.remove(lit.to_uint());
-    }
-
 }
diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h
index 7fc013686..c31d56382 100644
--- a/src/math/polysat/conflict.h
+++ b/src/math/polysat/conflict.h
@@ -85,7 +85,7 @@ namespace polysat {
     /** Conflict state, represented as core (~negation of clause). */
     class conflict {
         solver& s;
-        signed_constraints m_constraints;   // new constraints used as premises
+        // signed_constraints m_constraints;   // new constraints used as premises
         indexed_uint_set m_literals;        // set of boolean literals in the conflict
         uint_set m_vars;                    // variable assignments used as premises
         uint_set m_bail_vars;
@@ -95,16 +95,9 @@ namespace polysat {
         pvar m_conflict_var = null_var;
 
         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(signed_constraint c);
         void unset_mark(signed_constraint c);
-        void unset_bmark(signed_constraint c);
-
-        bool contains_literal(sat::literal lit) const;
-        void insert_literal(sat::literal lit);
-        void remove_literal(sat::literal lit);
 
         void minimize_vars(signed_constraint c);
 
@@ -126,14 +119,12 @@ namespace polysat {
 
         void set_bailout();
 
-        bool empty() const {
-            return m_constraints.empty() && m_vars.empty() && m_literals.empty() && m_conflict_var == null_var;
-        }
-
+        bool empty() const;
         void reset();
 
         bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); }
-        bool is_bmarked(sat::bool_var b) const;
+        bool is_marked(signed_constraint c) const;
+        bool is_marked(sat::bool_var b) const;
 
         /** conflict because the constraint c is false under current variable assignment */
         void set(signed_constraint c);
@@ -149,9 +140,8 @@ namespace polysat {
         void remove(signed_constraint c);
         void replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> const& c_new_premises);
 
-        void keep(signed_constraint c);
-
-        bool contains(signed_constraint c);
+        bool contains(signed_constraint c) const;
+        bool contains(sat::literal lit) const;
 
         /** Perform boolean resolution with the clause upon variable 'var'.
          * Precondition: core/clause contain complementary 'var'-literals.
@@ -187,23 +177,20 @@ namespace polysat {
     class conflict_iterator {
         friend class conflict;
 
-        using it1_t = signed_constraints::const_iterator;
-        using it2_t = indexed_uint_set::iterator;
+        using inner_t = indexed_uint_set::iterator;
 
         constraint_manager* m_cm;
-        it1_t m_it1;
-        it1_t m_end1;
-        it2_t m_it2;
+        inner_t m_inner;
 
-        conflict_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) {}
+        conflict_iterator(constraint_manager& cm, inner_t inner):
+            m_cm(&cm), m_inner(inner) {}
 
-        static conflict_iterator begin(constraint_manager& cm, signed_constraints const& cs, indexed_uint_set const& lits) {
-            return {cm, cs.begin(), cs.end(), lits.begin()};
+        static conflict_iterator begin(constraint_manager& cm, indexed_uint_set const& lits) {
+            return {cm, lits.begin()};
         }
 
-        static conflict_iterator end(constraint_manager& cm, signed_constraints const& cs, indexed_uint_set const& lits) {
-            return {cm, cs.end(), cs.end(), lits.end()};
+        static conflict_iterator end(constraint_manager& cm, indexed_uint_set const& lits) {
+            return {cm, lits.end()};
         }
 
     public:
@@ -214,28 +201,22 @@ namespace polysat {
         using iterator_category = std::input_iterator_tag;
 
         conflict_iterator& operator++() {
-            if (m_it1 != m_end1)
-                ++m_it1;
-            else
-                ++m_it2;
+            ++m_inner;
             return *this;
         }
 
         signed_constraint operator*() const {
-            if (m_it1 != m_end1)
-                return *m_it1;
-            else
-                return m_cm->lookup(sat::to_literal(*m_it2));
+            return m_cm->lookup(sat::to_literal(*m_inner));
         }
 
         bool operator==(conflict_iterator const& other) const {
-            return m_it1 == other.m_it1 && m_it2 == other.m_it2;
+            return m_inner == other.m_inner;
         }
 
         bool operator!=(conflict_iterator const& other) const { return !operator==(other); }
     };
 
 
-    inline conflict::const_iterator conflict::begin() const { return conflict_iterator::begin(cm(), m_constraints, m_literals); }
-    inline conflict::const_iterator conflict::end() const { return conflict_iterator::end(cm(), m_constraints, m_literals); }
+    inline conflict::const_iterator conflict::begin() const { return conflict_iterator::begin(cm(), m_literals); }
+    inline conflict::const_iterator conflict::end() const { return conflict_iterator::end(cm(), m_literals); }
 }
diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp
index a400982bb..b4252b885 100644
--- a/src/math/polysat/constraint.cpp
+++ b/src/math/polysat/constraint.cpp
@@ -151,6 +151,8 @@ namespace polysat {
             return c2;
         }
         else {
+            SASSERT(!c1->has_bvar());
+            ensure_bvar(c1);
             m_constraint_table.insert(c1);
             store(c1);
             return c1;
diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index 391c1f976..c0082dd41 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -74,14 +74,13 @@ namespace polysat {
 
         void register_clause(clause* cl, solver& s);
 
+        void ensure_bvar(constraint* c);
+        void erase_bvar(constraint* c);
+
     public:
         constraint_manager(bool_var_manager& bvars): m_bvars(bvars) {}
         ~constraint_manager();
 
-        void ensure_bvar(constraint* c);
-        void erase_bvar(constraint* c);
-        // sat::literal get_or_assign_blit(signed_constraint& c);
-
         void store(clause* cl, solver& s, bool value_propagate);
 
         /// Release clauses at the given level and above.
@@ -146,11 +145,9 @@ namespace polysat {
         friend class smul_fl_constraint;
         friend class op_constraint;
 
-        // constraint_manager* m_manager;
         ckind_t             m_kind;
         unsigned_vector     m_vars;
         lbool               m_external_sign = l_undef;
-        bool                m_is_marked = false;
         bool                m_is_active = 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.
@@ -159,7 +156,6 @@ namespace polysat {
         sat::bool_var       m_bvar = sat::null_bool_var;
 
         constraint(constraint_manager& m, ckind_t k): m_kind(k) {}
-        
 
     public:
         virtual ~constraint() {}
@@ -199,7 +195,7 @@ namespace polysat {
         unsigned var(unsigned idx) const { return m_vars[idx]; }
         bool contains_var(pvar v) const { return m_vars.contains(v); }
         bool has_bvar() const { return m_bvar != sat::null_bool_var; }
-        sat::bool_var bvar() const { return m_bvar; }
+        sat::bool_var bvar() const { SASSERT(has_bvar()); return m_bvar; }
         std::string bvar2string() const;
         unsigned level(solver& s) const;
 
@@ -208,10 +204,6 @@ namespace polysat {
         bool is_external() const { return m_external_sign != l_undef; }
         bool external_sign() const { SASSERT(is_external()); return m_external_sign == l_true; }
 
-        void set_mark() { m_is_marked = true; }
-        void unset_mark() { m_is_marked = false; }
-        bool is_marked() const { return m_is_marked; }
-
         bool is_active() const { return m_is_active; }
         void set_active(bool f) { m_is_active = f; }
 
diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp
index 961ee6839..d08b33a9f 100644
--- a/src/math/polysat/explain.cpp
+++ b/src/math/polysat/explain.cpp
@@ -61,8 +61,6 @@ namespace polysat {
             signed_constraint c = resolve1(v, c1, c2);
             if (!c)
                 continue;
-            if (!c->has_bvar())
-                s.m_constraints.ensure_bvar(c.get());
 
             switch (c.bvalue(s)) {
             case l_false:
diff --git a/src/math/polysat/search_state.cpp b/src/math/polysat/search_state.cpp
index 3d884d0e3..d49a89921 100644
--- a/src/math/polysat/search_state.cpp
+++ b/src/math/polysat/search_state.cpp
@@ -50,7 +50,6 @@ namespace polysat {
     void search_state::push_assignment(pvar p, rational const& r) {
         m_items.push_back(search_item::assignment(p));
         m_assignment.push_back({p, r});
-        auto& m = s.var2pdd(p);
         unsigned sz = s.size(p);
         pdd& s = assignment(sz);
         m_subst_trail.push_back(s);
diff --git a/src/math/polysat/simplify.cpp b/src/math/polysat/simplify.cpp
index 377b9fe83..fe6662175 100644
--- a/src/math/polysat/simplify.cpp
+++ b/src/math/polysat/simplify.cpp
@@ -48,6 +48,8 @@ namespace polysat {
         return false; 
     }
 
-    void simplify::operator()() {}
+    void simplify::operator()() {
+      (void)s; // silence warning
+    }
 
 }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index ada5bc4c2..f8fc32e9b 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -186,7 +186,6 @@ namespace polysat {
         SASSERT(c);
         if (is_conflict())
             return;  // no need to do anything if we already have a conflict at base level
-        m_constraints.ensure_bvar(c.get());
         sat::literal lit = c.blit();
         LOG("New constraint: " << c);
         switch (m_bvars.value(lit)) {
@@ -624,7 +623,7 @@ namespace polysat {
                 SASSERT(item.is_boolean());
                 sat::literal const lit = item.lit();
                 sat::bool_var const var = lit.var();
-                if (!m_conflict.is_bmarked(var))
+                if (!m_conflict.is_marked(var))
                     continue;
 
                 LOG_H2("Working on " << search_item_pp(m_search, item));
@@ -639,8 +638,10 @@ namespace polysat {
                 }
                 else if (m_bvars.is_bool_propagation(var))
                     m_conflict.resolve(lit, *m_bvars.reason(lit));
-                else
+                else {
+                    SASSERT(m_bvars.is_value_propagation(var));
                     m_conflict.resolve_with_assignment(lit, m_bvars.level(lit));
+                }
             }
         }
         // here we build conflict clause if it has free variables.
@@ -938,7 +939,6 @@ namespace polysat {
             signed_constraint c = cs[i];
             if (c.is_always_false())
                 continue;
-            m_constraints.ensure_bvar(c.get());
             cb.push(c);
         }
         clause_ref clause = cb.build();
@@ -1114,7 +1114,7 @@ namespace polysat {
     pdd solver::subst(assignment_t const& sub, pdd const& p) const {
         unsigned sz = p.manager().power_of_2();
         pdd s = p.manager().mk_val(1);
-        for (auto const [var, val] : sub) 
+        for (auto const& [var, val] : sub)
             if (size(var) == sz)
                 s = p.manager().subst_add(s, var, val);
         return p.subst_val(s);
diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp
index 4e629fafc..7c0a6a36a 100644
--- a/src/math/polysat/univariate/univariate_solver.cpp
+++ b/src/math/polysat/univariate/univariate_solver.cpp
@@ -17,6 +17,7 @@ Author:
 --*/
 
 #include "math/polysat/univariate/univariate_solver.h"
+#include "math/polysat/log.h"
 #include "sat/sat_solver/inc_sat_solver.h"
 #include "solver/solver.h"
 #include "util/util.h"
@@ -54,7 +55,9 @@ namespace polysat {
         ~univariate_bitblast_solver() override = default;
 
         void push() override {
+            // LOG("univariate push...");
             s->push();
+            // LOG("univariate push done");
         }
 
         void pop(unsigned n) override {