From 516ca06c28c6b5838ccdb147f2506c99eb420050 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 10 Sep 2021 15:40:25 +0200
Subject: [PATCH] levels take 1

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/clause.cpp              |  2 +-
 src/math/polysat/clause_builder.cpp      |  3 +-
 src/math/polysat/conflict_core.cpp       |  4 +-
 src/math/polysat/constraint.cpp          | 94 +++++-------------------
 src/math/polysat/constraint.h            | 29 +++-----
 src/math/polysat/eq_constraint.h         |  4 +-
 src/math/polysat/explain.cpp             |  3 +-
 src/math/polysat/forbidden_intervals.cpp | 11 +--
 src/math/polysat/saturation.cpp          | 47 ++++++------
 src/math/polysat/saturation.h            |  8 +-
 src/math/polysat/solver.cpp              | 77 ++++++++-----------
 src/math/polysat/solver.h                |  3 -
 src/math/polysat/ule_constraint.h        |  4 +-
 13 files changed, 99 insertions(+), 190 deletions(-)

diff --git a/src/math/polysat/clause.cpp b/src/math/polysat/clause.cpp
index 9ac839df5..9a33459d9 100644
--- a/src/math/polysat/clause.cpp
+++ b/src/math/polysat/clause.cpp
@@ -19,7 +19,7 @@ namespace polysat {
 
     clause_ref clause::from_unit(signed_constraint c, p_dependency_ref d) {
         SASSERT(c->has_bvar());
-        unsigned const lvl = c->level();
+        unsigned const lvl = 0; // level from literal?
         sat::literal_vector lits;
         lits.push_back(c.blit());
         return clause::from_literals(lvl, std::move(d), std::move(lits));
diff --git a/src/math/polysat/clause_builder.cpp b/src/math/polysat/clause_builder.cpp
index 390ab87b7..e2be4e362 100644
--- a/src/math/polysat/clause_builder.cpp
+++ b/src/math/polysat/clause_builder.cpp
@@ -54,8 +54,7 @@ namespace polysat {
         if (c->unit_clause()) {
             add_dependency(c->unit_dep());
             return;
-        }
-        m_level = std::max(m_level, c->level());
+        }       
         m_literals.push_back(c.blit());
     }
 
diff --git a/src/math/polysat/conflict_core.cpp b/src/math/polysat/conflict_core.cpp
index 7b388d43a..f9531c218 100644
--- a/src/math/polysat/conflict_core.cpp
+++ b/src/math/polysat/conflict_core.cpp
@@ -186,7 +186,7 @@ namespace polysat {
             LOG_V("Adding: " << item);
             if (item.is_assignment()) {
                 pvar v = item.var();
-                auto c = ~cm().eq(0, m_solver->var(v) - m_solver->m_value[v]);
+                auto c = ~cm().eq(m_solver->var(v) - m_solver->m_value[v]);
                 cm().ensure_bvar(c.get());
                 lemma.push(c.blit());
             } else {
@@ -226,7 +226,7 @@ namespace polysat {
                     continue;
                 if (m_solver->m_justification[v].level() > model_level)
                     continue;
-                auto diseq = ~cm().eq(lemma.level(), m_solver->var(v) - m_solver->m_value[v]);
+                auto diseq = ~cm().eq(m_solver->var(v) - m_solver->m_value[v]);
                 cm().ensure_bvar(diseq.get());
                 lemma.push(diseq);
             }
diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp
index 8bac1f0cc..c10d4031a 100644
--- a/src/math/polysat/constraint.cpp
+++ b/src/math/polysat/constraint.cpp
@@ -53,32 +53,9 @@ namespace polysat {
     /** Add constraint to per-level storage */
     void constraint_manager::store(constraint* c) {
         LOG_V("Store constraint: " << show_deref(c));
-        while (m_constraints.size() <= c->level())
-            m_constraints.push_back({});
-        m_constraints[c->level()].push_back(c);
+        m_constraints.push_back(c);
     }
 
-    /** Remove the given constraint from the per-level storage (without deallocating it) */
-    void constraint_manager::erase(constraint* c) {
-        LOG_V("Erase constraint: " << show_deref(c));
-        auto& vec = m_constraints[c->level()];
-        for (unsigned i = vec.size(); i-- > 0; )
-            if (vec[i] == c) {
-                vec.swap(i, vec.size() - 1);
-                constraint* c0 = vec.detach_back();
-                SASSERT(c0 == c);
-                vec.pop_back();
-                return;
-            }
-        UNREACHABLE();
-    }
-
-    /** Change level of the given constraint, adjusting its storage position */
-    void constraint_manager::set_level(constraint* c, unsigned new_lvl) {
-        erase(c);
-        c->m_level = new_lvl;
-        store(c);
-    }
 
     clause* constraint_manager::store(clause_ref cl_ref) {
         clause* cl = cl_ref.get();
@@ -99,20 +76,6 @@ namespace polysat {
 
     // Release constraints at the given level and above.
     void constraint_manager::release_level(unsigned lvl) {
-        for (unsigned l = m_constraints.size(); l-- > lvl; ) {
-            for (auto* c : m_constraints[l]) {
-                LOG_V("Destroying constraint: " << show_deref(c));
-                auto* d = c->unit_dep();
-                if (d && d->is_leaf()) {
-                    unsigned const dep = d->leaf_value();
-                    SASSERT(m_external_constraints.contains(dep));
-                    m_external_constraints.remove(dep);
-                }
-                m_constraint_table.erase(c);
-                erase_bvar(c);
-            }
-            m_constraints[l].reset();
-        }
         for (unsigned l = m_clauses.size(); l-- > lvl; ) {
             for (auto const& cl : m_clauses[l]) {
                 SASSERT_EQ(cl->m_ref_count, 1);  // otherwise there is a leftover reference somewhere
@@ -137,37 +100,20 @@ namespace polysat {
 
     /** Look up constraint among stored constraints. */
     constraint* constraint_manager::dedup(constraint* c1) {
-        auto it = m_constraint_table.find(c1);
-        if (it == m_constraint_table.end()) {
-            store(c1);
+        constraint* c2 = nullptr;
+        if (m_constraint_table.find(c1, c2)) {
+            dealloc(c1);
+            return c2;
+        }
+        else {
             m_constraint_table.insert(c1);
             return c1;
         }
-        constraint* c0 = *it;
-        if (c1->level() < c0->level())
-            set_level(c0, c1->level());
-        dealloc(c1);
-        return c0;
     }
 
     void constraint_manager::gc() {
-        for (auto& vec : m_constraints)
-            for (int i = vec.size(); i-- > 0; ) {
-                constraint* c = vec[i];
-                if (!c->has_bvar()) {
-                    LOG_V("Destroying constraint: " << show_deref(c));
-                    m_constraint_table.erase(c);
-                    vec.swap(i, vec.size() - 1);
-                    vec.pop_back();
-                }
-            }
-        DEBUG_CODE({
-            for (auto const& vec : m_constraints)
-                for (auto* c : vec) {
-                    SASSERT(c->has_bvar());
-                    SASSERT(m_constraint_table.contains(c));
-                }
-        });
+        // collect used literals from lemmas and stack
+        // walk constraints to remove unused.
     }
 
     bool constraint_manager::should_gc() {
@@ -176,17 +122,17 @@ namespace polysat {
         return true;
     }
 
-    signed_constraint constraint_manager::eq(unsigned lvl, pdd const& p) {
-        return {dedup(alloc(eq_constraint, *this, lvl, p)), true};
+    signed_constraint constraint_manager::eq(pdd const& p) {
+        return {dedup(alloc(eq_constraint, *this, p)), true};
     }
 
-    signed_constraint constraint_manager::ule(unsigned lvl, pdd const& a, pdd const& b) {
-        return {dedup(alloc(ule_constraint, *this, lvl, a, b)), true};
+    signed_constraint constraint_manager::ule(pdd const& a, pdd const& b) {
+        return {dedup(alloc(ule_constraint, *this, a, b)), true};
     }
 
-    signed_constraint constraint_manager::ult(unsigned lvl, pdd const& a, pdd const& b) {
+    signed_constraint constraint_manager::ult(pdd const& a, pdd const& b) {
         // a < b  <=>  !(b <= a)
-        return ~ule(lvl, b, a);
+        return ~ule(b, a);
     }
 
     // To do signed comparison of bitvectors, flip the msb and do unsigned comparison:
@@ -205,14 +151,14 @@ namespace polysat {
     //
     // Argument: flipping the msb swaps the negative and non-negative blocks
     //
-    signed_constraint constraint_manager::sle(unsigned lvl, pdd const& a, pdd const& b) {
+    signed_constraint constraint_manager::sle(pdd const& a, pdd const& b) {
         auto shift = rational::power_of_two(a.power_of_2() - 1);
-        return ule(lvl, a + shift, b + shift);
+        return ule(a + shift, b + shift);
     }
 
-    signed_constraint constraint_manager::slt(unsigned lvl, pdd const& a, pdd const& b) {
+    signed_constraint constraint_manager::slt(pdd const& a, pdd const& b) {
         auto shift = rational::power_of_two(a.power_of_2() - 1);
-        return ult(lvl, a + shift, b + shift);
+        return ult(a + shift, b + shift);
     }
 
     signed_constraint inequality::as_signed_constraint() const {
@@ -236,7 +182,7 @@ namespace polysat {
     }
 
     std::ostream& constraint::display_extra(std::ostream& out, lbool status) const {
-        out << " @" << level() << " (b";
+        out << " (b";
         if (has_bvar()) { out << bvar(); } else { out << "_"; }
         out << ")";
         (void)status;
diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index 58fd91c8f..1e0706405 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -40,10 +40,9 @@ namespace polysat {
         ptr_vector<constraint> m_bv2constraint;
         // Constraints that have a boolean variable, for deduplication
         constraint_table m_constraint_table;
+        scoped_ptr_vector<constraint> m_constraints;
 
-        // Constraint storage per level
-
-        vector<scoped_ptr_vector<constraint>> m_constraints;
+        // Clause storage per level
         vector<vector<clause_ref>> m_clauses;
 
         // Association to external dependency values (i.e., external names for constraints)
@@ -56,7 +55,6 @@ namespace polysat {
 
         void store(constraint* c);
         void erase(constraint* c);
-        void set_level(constraint* c, unsigned new_lvl);
 
         constraint* dedup(constraint* c);
 
@@ -84,11 +82,14 @@ namespace polysat {
         signed_constraint lookup(sat::literal lit) const;
         constraint* lookup_external(unsigned dep) const { return m_external_constraints.get(dep, nullptr); }
 
-        signed_constraint eq(unsigned lvl, pdd const& p);
-        signed_constraint ule(unsigned lvl, pdd const& a, pdd const& b);
-        signed_constraint ult(unsigned lvl, pdd const& a, pdd const& b);
-        signed_constraint sle(unsigned lvl, pdd const& a, pdd const& b);
-        signed_constraint slt(unsigned lvl, pdd const& a, pdd const& b);
+        signed_constraint eq(pdd const& p);
+        signed_constraint ule(pdd const& a, pdd const& b);
+        signed_constraint ult(pdd const& a, pdd const& b);
+        signed_constraint sle(pdd const& a, pdd const& b);
+        signed_constraint slt(pdd const& a, pdd const& b);
+
+        constraint *const* begin() const { return m_constraints.data(); }
+        constraint *const* end() const { return m_constraints.data() + m_constraints.size(); }
     };
 
 
@@ -114,7 +115,6 @@ namespace polysat {
 
         // constraint_manager* m_manager;
         clause*             m_unit_clause = nullptr;  ///< If this constraint was asserted by a unit clause, we store that clause here.
-        unsigned            m_level;  ///< Controls lifetime of the constraint object. Always a base level.
         ckind_t             m_kind;
         unsigned_vector     m_vars;
         /** The boolean variable associated to this constraint, if any.
@@ -126,8 +126,8 @@ namespace polysat {
         // TODO: replace parameter 'is_positive' everywhere by 'sign'? (also in signed_constraint)
         sat::bool_var       m_bvar = sat::null_bool_var;
 
-        constraint(constraint_manager& m, unsigned lvl, ckind_t k):
-            /*m_manager(&m),*/ m_level(lvl), m_kind(k) {}
+        constraint(constraint_manager& m, ckind_t k):
+            /*m_manager(&m),*/ m_kind(k) {}
 
     protected:
         std::ostream& display_extra(std::ostream& out, lbool status) const;
@@ -160,16 +160,12 @@ namespace polysat {
         unsigned_vector const& vars() const { return m_vars; }
         unsigned var(unsigned idx) const { return m_vars[idx]; }
         bool contains_var(pvar v) const { return m_vars.contains(v); }
-        unsigned level() const { return m_level; }
         bool has_bvar() const { return m_bvar != sat::null_bool_var; }
         sat::bool_var bvar() const { return m_bvar; }
 
         clause* unit_clause() const { return m_unit_clause; }
         void set_unit_clause(clause* cl);
         p_dependency* unit_dep() const { return m_unit_clause ? m_unit_clause->dep() : nullptr; }
-
-
-
     };
 
     inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
@@ -209,7 +205,6 @@ namespace polysat {
 
         sat::bool_var bvar() const { return m_constraint->bvar(); }
         sat::literal blit() const { return sat::literal(bvar(), is_negative()); }
-        unsigned level() const { return m_constraint->level(); }
         constraint* get() const { return m_constraint; }
 
         explicit operator bool() const { return !!m_constraint; }
diff --git a/src/math/polysat/eq_constraint.h b/src/math/polysat/eq_constraint.h
index b34c8ca5c..b8de5c8d3 100644
--- a/src/math/polysat/eq_constraint.h
+++ b/src/math/polysat/eq_constraint.h
@@ -22,8 +22,8 @@ namespace polysat {
 
         pdd m_poly;
 
-        eq_constraint(constraint_manager& m, unsigned lvl, pdd const& p):
-            constraint(m, lvl, ckind_t::eq_t), m_poly(p) {
+        eq_constraint(constraint_manager& m, pdd const& p):
+            constraint(m, ckind_t::eq_t), m_poly(p) {
             m_vars.append(p.free_vars());
         }
 
diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp
index 89b4ad587..0660b8ab4 100644
--- a/src/math/polysat/explain.cpp
+++ b/src/math/polysat/explain.cpp
@@ -35,8 +35,7 @@ namespace polysat {
             // (this condition might be too strict, but we use it for now to prevent looping)
             if (b.degree(v) <= r.degree(v))
                 return {};
-            unsigned const lvl = std::max(c1->level(), c2->level());
-            signed_constraint c = cm().eq(lvl, r);
+            signed_constraint c = cm().eq(r);
             LOG("resolved: " << c << "        currently false? " << c.is_currently_false(s()));
             if (!c.is_currently_false(s()))
                 return {};
diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp
index c16757576..a6e7a222a 100644
--- a/src/math/polysat/forbidden_intervals.cpp
+++ b/src/math/polysat/forbidden_intervals.cpp
@@ -131,11 +131,8 @@ namespace polysat {
         LOG("seq: " << seq);
         SASSERT(seq.size() >= 2);  // otherwise has_full should have been true
 
+        // TODO lemma level depends on clauses used to derive it, not on levels of constraints
         unsigned lemma_lvl = 0;
-        for (unsigned i : seq) {
-            signed_constraint const& c = records[i].src;
-            lemma_lvl = std::max(lemma_lvl, c->level());
-        }
 
         // Update the conflict state
         // Idea:
@@ -159,7 +156,7 @@ namespace polysat {
             // NB: do we really have to pass in the level to this new literal?
             // seems separating the level from the constraint is what we want
             // the level of a literal is when it was assigned. Lemmas could have unassigned literals.
-            signed_constraint c = s.m_constraints.ult(lemma_lvl, lhs, rhs);
+            signed_constraint c = s.m_constraints.ult(lhs, rhs);
             LOG("constraint: " << c);
             lemma.push(~c);
             // Side conditions
@@ -315,9 +312,9 @@ namespace polysat {
             out_neg_cond = nullptr;
         }
         else if (is_trivial)
-            out_neg_cond = ~s.m_constraints.eq(0, condition_body);
+            out_neg_cond = ~s.m_constraints.eq(condition_body);
         else
-            out_neg_cond = s.m_constraints.eq(0, condition_body);
+            out_neg_cond = s.m_constraints.eq(condition_body);
 
         if (is_trivial) {
             if (!ineq.is_strict)
diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index fa2c2e7e6..4c461420e 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -25,9 +25,8 @@ TODO: when we check that 'x' is "unary":
    (extension to arbitrary monomials for 'x' should be fairly easy too)
 
 TODO: 
-- resolve away the "problematic" premise (non-linear inequality etc) that is reduced by a saturation rule.
-  - it would work by adding the explanations for the resolved premises to the reason clause 
-  - and removing the literal from the core
+- remove the "problematic" literal from the core itself such that reference counts on variable assignments are decreased.
+
 --*/
 #include "math/polysat/saturation.h"
 #include "math/polysat/solver.h"
@@ -52,11 +51,11 @@ namespace polysat {
         return false;
     }
 
-    signed_constraint inf_saturate::ineq(unsigned lvl, bool is_strict, pdd const& lhs, pdd const& rhs) {
+    signed_constraint inf_saturate::ineq(bool is_strict, pdd const& lhs, pdd const& rhs) {
         if (is_strict)
-            return cm().ult(lvl, lhs, rhs);
+            return cm().ult(lhs, rhs);
         else
-            return cm().ule(lvl, lhs, rhs);
+            return cm().ule(lhs, rhs);
     }
 
     /**
@@ -72,13 +71,13 @@ namespace polysat {
         return true;
     }
 
-    bool inf_saturate::propagate(conflict_core& core, unsigned lvl, bool is_strict, pdd const& lhs, pdd const& rhs, clause_builder& reason) {
-        signed_constraint c = ineq(lvl, is_strict, lhs, rhs);
+    bool inf_saturate::propagate(conflict_core& core, bool is_strict, pdd const& lhs, pdd const& rhs, clause_builder& reason) {
+        signed_constraint c = ineq(is_strict, lhs, rhs);
         return propagate(core, c, reason);
     }
 
     /// Add premises for Ω*(x, y)
-    void inf_saturate::push_omega_bisect(clause_builder& reason, unsigned level, pdd const& x, rational x_max, pdd const& y, rational y_max) {
+    void inf_saturate::push_omega_bisect(clause_builder& reason, pdd const& x, rational x_max, pdd const& y, rational y_max) {
         rational x_val, y_val;
         auto& pddm = x.manager();
         unsigned bit_size = pddm.power_of_2();
@@ -128,15 +127,15 @@ namespace polysat {
         // conflict resolution should be able to pick up this as a valid justification.
         // or we resort to the same extension as in the original mul_overflow code
         // where we add explicit equality propagations from the current assignment.
-        auto c1 = cm().ule(level, x, pddm.mk_val(x_lo));
-        auto c2 = cm().ule(level, y, pddm.mk_val(y_lo));
+        auto c1 = cm().ule(x, pddm.mk_val(x_lo));
+        auto c2 = cm().ule(y, pddm.mk_val(y_lo));
         reason.push(~c1);
         reason.push(~c2);
     }
 
     // determine worst case upper bounds for x, y
     // then extract premises for a non-worst-case bound.
-    void inf_saturate::push_omega(clause_builder& reason, unsigned level, pdd const& x, pdd const& y) {     
+    void inf_saturate::push_omega(clause_builder& reason, pdd const& x, pdd const& y) {     
         auto& pddm = x.manager();
         unsigned bit_size = pddm.power_of_2();
         rational bound = rational::power_of_two(bit_size);
@@ -149,7 +148,7 @@ namespace polysat {
             y_max = s().m_viable.max_viable(y.var());        
 
         if (x_max * y_max  >= bound)            
-            push_omega_bisect(reason, level, x, x_max, y, y_max);
+            push_omega_bisect(reason, x, x_max, y, y_max);
         else {
             for (auto c : s().m_cjust[y.var()])
                 reason.push(~c);
@@ -263,13 +262,12 @@ namespace polysat {
         if (!c.is_strict && s().get_value(v).is_zero())
             return false;
 
-        unsigned const lvl = c.src->level();
         clause_builder reason(s());   
         if (!c.is_strict)
-            reason.push(cm().eq(lvl, x - x.manager().mk_val(rational(0))));
+            reason.push(cm().eq(x - x.manager().mk_val(rational(0))));
         reason.push(~c.as_signed_constraint());
-        push_omega(reason, lvl, x, y);        
-        return propagate(core, lvl, c.is_strict, y, z, reason);
+        push_omega(reason, x, y);        
+        return propagate(core, c.is_strict, y, z, reason);
     }
 
     /// [y] z' <= y /\ zx > yx  ==>  Ω*(x,y) \/ zx > z'x
@@ -282,15 +280,14 @@ namespace polysat {
         if (!is_non_overflow(x, y))
             return false;
           
-        unsigned const lvl = std::max(yx_l_zx.src->level(), le_y.src->level());
         pdd const& z_prime = le_y.lhs;
 
         clause_builder reason(s());
         reason.push(~le_y.as_signed_constraint());
         reason.push(~yx_l_zx.as_signed_constraint());
-        push_omega(reason, lvl, x, y);
+        push_omega(reason, x, y);
         // z'x <= zx
-        return propagate(core, lvl, yx_l_zx.is_strict || le_y.is_strict, z_prime * x, z * x, reason);
+        return propagate(core, yx_l_zx.is_strict || le_y.is_strict, z_prime * x, z * x, reason);
     }
 
     bool inf_saturate::try_ugt_y(pvar v, conflict_core& core, inequality const& c) {
@@ -329,12 +326,11 @@ namespace polysat {
         pdd z = x_l_z.rhs;
         if (!is_non_overflow(a, z))
             return false;
-        unsigned const lvl = std::max(x_l_z.src->level(), y_l_ax.src->level());
         clause_builder reason(s());
         reason.push(~x_l_z.as_signed_constraint());
         reason.push(~y_l_ax.as_signed_constraint());
-        push_omega(reason, lvl, a, z);
-        return propagate(core, lvl, x_l_z.is_strict || y_l_ax.is_strict, y, a * z, reason);
+        push_omega(reason, a, z);
+        return propagate(core, x_l_z.is_strict || y_l_ax.is_strict, y, a * z, reason);
     }
 
 
@@ -356,16 +352,15 @@ namespace polysat {
     bool inf_saturate::try_ugt_z(pvar z, conflict_core& core, inequality const& c, inequality const& d, pdd const& x, pdd const& y) {
         SASSERT(is_g_v(z, c));
         SASSERT(verify_YX_l_zX(z, d, x, y));
-        unsigned const lvl = std::max(c.src->level(), d.src->level());
         pdd const& y_prime = c.rhs;
         if (!is_non_overflow(x, y_prime))
             return false;
         clause_builder reason(s());
         reason.push(~c.as_signed_constraint());
         reason.push(~d.as_signed_constraint());
-        push_omega(reason, lvl, x, y_prime);
+        push_omega(reason, x, y_prime);
         // yx <= y'x
-        return propagate(core, lvl, c.is_strict || d.is_strict, y * x, y_prime * x, reason);
+        return propagate(core, c.is_strict || d.is_strict, y * x, y_prime * x, reason);
     }
 
 
diff --git a/src/math/polysat/saturation.h b/src/math/polysat/saturation.h
index 9a521b997..2a6605db3 100644
--- a/src/math/polysat/saturation.h
+++ b/src/math/polysat/saturation.h
@@ -38,11 +38,11 @@ namespace polysat {
     class inf_saturate : public inference_engine {
         bool find_upper_bound(pvar x, signed_constraint& c, rational& bound);
 
-        void push_omega(clause_builder& reason, unsigned level, pdd const& x, pdd const& y);
-        void push_omega_bisect(clause_builder& reason, unsigned level, pdd const& x, rational x_max, pdd const& y, rational y_max);
-        signed_constraint ineq(unsigned level, bool strict, pdd const& lhs, pdd const& rhs);
+        void push_omega(clause_builder& reason, pdd const& x, pdd const& y);
+        void push_omega_bisect(clause_builder& reason, pdd const& x, rational x_max, pdd const& y, rational y_max);
+        signed_constraint ineq(bool strict, pdd const& lhs, pdd const& rhs);
         bool propagate(conflict_core& core, signed_constraint& c, clause_builder& reason);
-        bool propagate(conflict_core& core, unsigned level, bool strict, pdd const& lhs, pdd const& rhs, clause_builder& reason);
+        bool propagate(conflict_core& core, bool strict, pdd const& lhs, pdd const& rhs, clause_builder& reason);
 
         bool try_ugt_x(pvar v, conflict_core& core, inequality const& c);
 
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 0135c2513..ddfe037ad 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -117,27 +117,27 @@ namespace polysat {
     }
 
     signed_constraint solver::mk_eq(pdd const& p) {
-        return m_constraints.eq(m_level, p);
+        return m_constraints.eq(p);
     }
 
     signed_constraint solver::mk_diseq(pdd const& p) {
-        return ~m_constraints.eq(m_level, p);
+        return ~m_constraints.eq(p);
     }
 
     signed_constraint solver::mk_ule(pdd const& p, pdd const& q) {
-        return m_constraints.ule(m_level, p, q);
+        return m_constraints.ule(p, q);
     }
 
     signed_constraint solver::mk_ult(pdd const& p, pdd const& q) {
-        return m_constraints.ult(m_level, p, q);
+        return m_constraints.ult(p, q);
     }
 
     signed_constraint solver::mk_sle(pdd const& p, pdd const& q) {
-        return m_constraints.sle(m_level, p, q);
+        return m_constraints.sle(p, q);
     }
 
     signed_constraint solver::mk_slt(pdd const& p, pdd const& q) {
-        return m_constraints.slt(m_level, p, q);
+        return m_constraints.slt(p, q);
     }
 
     void solver::new_constraint(signed_constraint c, unsigned dep, bool activate) {
@@ -150,7 +150,7 @@ namespace polysat {
         if (dep != null_dependency)
             m_constraints.register_external(c.get());
         LOG("New constraint: " << c);
-        m_original.push_back(c);
+
 #if ENABLE_LINEAR_SOLVER
         m_linear_solver.new_constraint(*c.get());
 #endif
@@ -308,8 +308,6 @@ namespace polysat {
             }
             m_trail.pop_back();
         }
-        pop_constraints(m_original);
-        pop_constraints(m_redundant);
         m_constraints.release_level(m_level + 1);
         SASSERT(m_level == target_level);
         for (unsigned j = replay.size(); j-- > 0; ) {
@@ -319,13 +317,6 @@ namespace polysat {
         }
     }
 
-    void solver::pop_constraints(signed_constraints& cs) {
-        VERIFY(invariant(cs));
-        while (!cs.empty() && cs.back()->level() > m_level) {
-            deactivate_constraint(cs.back());
-            cs.pop_back();
-        }        
-    }
 
     void solver::add_watch(signed_constraint c) {
         SASSERT(c);
@@ -796,7 +787,6 @@ namespace polysat {
         if (cl->size() == 1) {
             signed_constraint c = m_constraints.lookup((*cl)[0]);
             c->set_unit_clause(cl);
-            insert_constraint(m_redundant, c);
         }
     }
 
@@ -804,13 +794,6 @@ namespace polysat {
         SASSERT(c);
         LOG_V("INSERTING: " << c);
         cs.push_back(c);
-        for (unsigned i = cs.size() - 1; i-- > 0; ) {
-            auto c1 = cs[i + 1];
-            auto c2 = cs[i];
-            if (c1->level() >= c2->level())
-                break;
-            std::swap(cs[i], cs[i+1]);
-        }
         SASSERT(invariant(cs)); 
     }
     
@@ -864,11 +847,8 @@ namespace polysat {
             // out << m_viable[v] << "\n";
         }
         out << "Boolean assignment:\n\t" << m_bvars << "\n";
-        out << "Original:\n";
-        for (auto c : m_original)
-            out << "\t" << c << "\n";
-        out << "Redundant:\n";
-        for (auto c : m_redundant)
+        out << "Constraints:\n";
+        for (auto c : m_constraints)
             out << "\t" << c << "\n";
         out << "Redundant clauses:\n";
         for (auto* cl : m_redundant_clauses) {
@@ -906,18 +886,13 @@ namespace polysat {
     }
 
     bool solver::invariant() {
-        invariant(m_original);
-        invariant(m_redundant);
         return true;
     }
 
     /**
-     * constraints are sorted by levels so they can be removed when levels are popped.
+     * levels are gone
      */
     bool solver::invariant(signed_constraints const& cs) {
-        unsigned sz = cs.size();
-        for (unsigned i = 0; i + 1 < sz; ++i) 
-            VERIFY(cs[i]->level() <= cs[i + 1]->level());
         return true;
     }
 
@@ -925,21 +900,25 @@ namespace polysat {
      * Check that two variables of each constraint are watched.
      */
     bool solver::wlist_invariant() {
-        signed_constraints cs;
-        cs.append(m_original.size(), m_original.data());
-        cs.append(m_redundant.size(), m_redundant.data());
-        // Skip boolean literals that aren't active yet
+        // Skip boolean variables that aren't active yet
         uint_set skip;
         for (unsigned i = m_qhead; i < m_search.size(); ++i)
             if (m_search[i].is_boolean())
-                skip.insert(m_search[i].lit().to_uint());
-        for (auto c : cs) {
-            SASSERT(c->has_bvar());
-            if (skip.contains(c.blit().to_uint()))
+                skip.insert(m_search[i].lit().var());
+        for (auto c : m_constraints) {
+            if (!c->has_bvar())
                 continue;
+            if (skip.contains(c->bvar()))
+                continue;
+
+            lbool value = m_bvars.value(c->bvar());
+            if (value == l_undef)
+                continue;
+            bool is_positive = value == l_true;
             int64_t num_watches = 0;
+            signed_constraint sc(c, is_positive);
             for (auto const& wlist : m_watch) {
-                auto n = std::count(wlist.begin(), wlist.end(), c);
+                auto n = std::count(wlist.begin(), wlist.end(), sc);
                 VERIFY(n <= 1);  // no duplicates in the watchlist
                 num_watches += n;
             }
@@ -968,10 +947,12 @@ namespace polysat {
         LOG_H1("Checking current model...");
         LOG("Assignment: " << assignments_pp(*this));
         bool all_ok = true;
-        for (auto c : m_original) {
-            bool ok = c.is_currently_true(*this);
-            LOG((ok ? "PASS" : "FAIL") << ": " << c);
-            all_ok = all_ok && ok;
+        for (auto s : m_search) {
+            if (s.is_boolean()) {
+                bool ok = m_bvars.value(s.lit()) == l_true;
+                LOG((ok ? "PASS" : "FAIL") << ": " << s.lit());
+                all_ok = all_ok && ok;
+            }
         }
         if (all_ok) LOG("All good!");
         return true;
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index fdf9a3098..77b0e3ced 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -89,8 +89,6 @@ namespace polysat {
 
         // Per constraint state
         constraint_manager       m_constraints;
-        signed_constraints       m_original;
-        signed_constraints       m_redundant;
         ptr_vector<clause>       m_redundant_clauses;
 
         svector<sat::bool_var>   m_disjunctive_lemma;
@@ -154,7 +152,6 @@ namespace polysat {
 
         void push_level();
         void pop_levels(unsigned num_levels);
-        void pop_constraints(signed_constraints& cs);
 
         void assign_bool(unsigned level, sat::literal lit, clause* reason, clause* lemma);
         void activate_constraint(signed_constraint c);
diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h
index 57951710f..d2003ded4 100644
--- a/src/math/polysat/ule_constraint.h
+++ b/src/math/polysat/ule_constraint.h
@@ -23,8 +23,8 @@ namespace polysat {
         pdd m_lhs;
         pdd m_rhs;
 
-        ule_constraint(constraint_manager& m, unsigned lvl, pdd const& l, pdd const& r):
-            constraint(m, lvl, ckind_t::ule_t), m_lhs(l), m_rhs(r) {
+        ule_constraint(constraint_manager& m, pdd const& l, pdd const& r):
+            constraint(m, ckind_t::ule_t), m_lhs(l), m_rhs(r) {
             m_vars.append(l.free_vars());
             for (auto v : r.free_vars())
                 if (!m_vars.contains(v))