From be0d0d5b9b53e613dbd4acd65bc6c45cee571b41 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 6 Mar 2023 21:39:43 +0100
Subject: [PATCH 1/5] Use checked division

---
 src/math/polysat/saturation.cpp | 22 ++++++++++++----------
 1 file changed, 12 insertions(+), 10 deletions(-)

diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index c612577db..c0845bb8e 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -785,22 +785,31 @@ namespace polysat {
     bool saturation::try_mul_eq_bound(pvar x, conflict& core, inequality const& axb_l_y) {
         set_rule("[x] 2^k*x = 2^k*y & x < 2^N-k => y = x or y >= 2^{N-k}");
         auto& m = s.var2pdd(x);
-        unsigned N = m.power_of_2();
+        unsigned const N = m.power_of_2();
         pdd y = m.zero();
         pdd a = y, b = y, a2 = y;
-        pdd X = s.var(x);
+        pdd const X = s.var(x);
+        // Match ax + b <= y with eval(y) = 0
         if (!is_AxB_eq_0(x, axb_l_y, a, b, y))
             return false;
         if (!a.is_val())
             return false;
         if (!a.val().is_power_of_two())
             return false;
-        unsigned k = a.val().trailing_zeros();
+        unsigned const k = a.val().trailing_zeros();
         if (k == 0)
             return false;
+        // x*2^k = b, x <= a2 < 2^{N-k}
+        rational const bound = rational::power_of_two(N - k);
         b = -b;
         if (b.leading_coefficient() != a.val())
             return false;
+        pdd Y = m.zero();
+        if (!b.try_div(b.leading_coefficient(), Y))
+            return false;
+        rational Y_val;
+        if (!s.try_eval(Y, Y_val) || Y_val >= bound)
+            return false;
         for (auto c : core) {
             if (!c->is_ule())
                 continue;
@@ -809,15 +818,9 @@ namespace polysat {
                 continue;
             if (!a2.is_val())
                 continue;
-            // x*2^k = b, x <= a2 < 2^{N-k}
-            rational bound = rational::power_of_two(N - k);
             if (i.is_strict() && a2.val() >= bound)
                 continue;
             if (!i.is_strict() && a2.val() > bound)
-                continue;            
-            pdd Y = b.div(b.leading_coefficient());
-            rational Y_val;
-            if (!s.try_eval(Y, Y_val) || Y_val >= bound)
                 continue;
             signed_constraint le = s.ule(Y, bound - 1);
             m_lemma.reset();
@@ -827,7 +830,6 @@ namespace polysat {
             if (propagate(x, core, axb_l_y, s.eq(X, Y)))
                 return true;
         }
-
         return false;
     }
 

From 6c00d4051340aa0d34edfc3e34a3a509f08ce3be Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Mar 2023 17:35:39 -0800
Subject: [PATCH 2/5] polysat fixes

1. ensure that force_push is invoked before polysat updates state.
2. extract conflicts based on dependencies of both new literal that was conflicting with existing literal that had its value assigned based on dependencies.
---
 src/math/polysat/conflict.cpp | 11 ++++++++++-
 src/math/polysat/conflict.h   |  3 +++
 src/math/polysat/solver.cpp   |  3 +++
 src/math/polysat/solver.h     |  1 +
 src/sat/smt/bv_polysat.cpp    |  9 +++++++++
 src/sat/smt/bv_solver.cpp     |  9 ++++++++-
 6 files changed, 34 insertions(+), 2 deletions(-)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index d68d3236e..37347b7da 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -167,6 +167,7 @@ namespace polysat {
     void conflict::reset() {
         m_literals.reset();
         m_vars.reset();
+        m_dep_literal = sat::null_literal;
         m_var_occurrences.reset();
         m_vars_occurring.reset();
         m_lemmas.reset();
@@ -184,16 +185,21 @@ namespace polysat {
         return contains(lit) || contains(~lit);
     }
 
-    void conflict::init_at_base_level(dependency dep) {
+    void conflict::init_at_base_level(dependency dep, sat::literal lit) {
         SASSERT(empty());
         SASSERT(s.at_base_level());
         m_level = s.m_level;
         m_dep = dep;
+        m_dep_literal = lit;
         SASSERT(!empty());
         // TODO: logger().begin_conflict???
         // TODO: check uses of logger().begin_conflict(). sometimes we call it before adding constraints, sometimes after...
     }
 
+    void conflict::init_at_base_level(dependency dep) {
+        init_at_base_level(dep, sat::null_literal);
+    }
+
     void conflict::init(signed_constraint c) {
         LOG("Conflict: constraint " << lit_pp(s, c));
         SASSERT(empty());
@@ -585,6 +591,9 @@ namespace polysat {
             }
         }
 
+        if (m_dep_literal != sat::null_literal)
+            enqueue_lit(m_dep_literal);
+        
         for (unsigned d : deps)
             out_deps.push_back(dependency(d));
         if (!m_dep.is_null() && !deps.contains(m_dep.val()))
diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h
index 4960aa9b0..6cd509c0b 100644
--- a/src/math/polysat/conflict.h
+++ b/src/math/polysat/conflict.h
@@ -102,6 +102,7 @@ namespace polysat {
         // Level at which the conflict was discovered
         unsigned m_level = UINT_MAX;
         dependency m_dep = null_dependency;
+        sat::literal m_dep_literal = sat::null_literal;
 
     public:
         conflict(solver& s);
@@ -128,6 +129,8 @@ namespace polysat {
 
         /** conflict due to obvious input inconsistency */
         void init_at_base_level(dependency dep);
+        /** conflict due to obvious input inconsistency with literal */
+        void init_at_base_level(dependency dep, sat::literal lit);
         /** conflict because the constraint c is false under current variable assignment */
         void init(signed_constraint c);
         /** boolean conflict with the given clause */
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index c4b016d2c..b4187dda4 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -599,6 +599,7 @@ namespace polysat {
 #if 0
         m_fixed_bits.push();
 #endif
+        display(verbose_stream() << "push\n");
     }
 
     void solver::pop_levels(unsigned num_levels) {
@@ -710,6 +711,8 @@ namespace polysat {
             m_trail.push_back(trail_instr_t::assign_bool_i);
             LOG("Replay: " << lit);
         }
+
+        display(verbose_stream());
     }
 
     bool solver::can_decide() const {
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 1f690de7a..39f046f93 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -263,6 +263,7 @@ namespace polysat {
         void propagate_clause(clause& cl);
 
         void set_conflict_at_base_level(dependency dep) { m_conflict.init_at_base_level(dep); }
+        void set_conflict_at_base_level(dependency dep, sat::literal lit) { m_conflict.init_at_base_level(dep, lit); }
         void set_conflict(signed_constraint c) { m_conflict.init(c); }
         void set_conflict(clause& cl) { m_conflict.init(cl); }
         void set_conflict_by_viable_interval(pvar v) { m_conflict.init_by_viable_interval(v); }
diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp
index d7a2012e2..a5375f7dc 100644
--- a/src/sat/smt/bv_polysat.cpp
+++ b/src/sat/smt/bv_polysat.cpp
@@ -205,6 +205,7 @@ namespace bv {
         polysat::signed_constraint sc = a->m_sc;
         if (!sc)
             return;
+        force_push();
         SASSERT(s().value(a->m_bv) != l_undef);
         bool sign = l_false == s().value(a->m_bv);
         sat::literal lit(a->m_bv, sign);
@@ -216,6 +217,7 @@ namespace bv {
     bool solver::polysat_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {
         if (!use_polysat())
             return false;
+        force_push();
         pdd p = var2pdd(r1);
         pdd q = var2pdd(r2);
         auto sc = m_polysat.eq(p, q);
@@ -229,11 +231,13 @@ namespace bv {
     bool solver::polysat_diseq_eh(euf::th_eq const& ne) {
         if (!use_polysat())
             return false;
+        force_push();
         euf::theory_var v1 = ne.v1(), v2 = ne.v2();
         pdd p = var2pdd(v1);
         pdd q = var2pdd(v2);
         auto sc = ~m_polysat.eq(p, q);
         sat::literal neq = ~expr2literal(ne.eq());
+        TRACE("bv", tout << neq << " := " << s().value(neq) << " @" << s().scope_lvl() << "\n");
         m_polysat.assign_eh(sc, polysat::dependency(1 + 2 * neq.index()));
         return true;
     }
@@ -241,6 +245,7 @@ namespace bv {
     void solver::polysat_propagate() {
         if (!use_polysat())
             return;
+        force_push();
         lbool r = m_polysat.unit_propagate();
         if (r == l_false)
             polysat_core();
@@ -249,6 +254,7 @@ namespace bv {
     lbool solver::polysat_final() {
         if (!use_polysat())
             return l_true;
+        force_push();
         lbool r = m_polysat.check_sat();
         if (r == l_false) 
             polysat_core();
@@ -268,6 +274,9 @@ namespace bv {
                 eqs.push_back(euf::enode_pair(var2enode(v1), var2enode(v2)));
             }
         }
+        for (auto lit : core) {
+            VERIFY(s().value(lit) == l_true);
+        }
         auto ex = mk_bv2ext_justification(core, eqs);
         ctx.set_conflict(ex);
     }
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index 9a177c0cc..c5795de0c 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -247,10 +247,10 @@ namespace bv {
             return;
         if (s().is_probing())
             return;
+        TRACE("bv", tout << "diff: " << v1 << " != " << v2 << " @" << s().scope_lvl() << "\n";);
         if (polysat_diseq_eh(ne))
             return;
         
-        TRACE("bv", tout << "diff: " << v1 << " != " << v2 << " @" << s().scope_lvl() << "\n";);
         unsigned sz = m_bits[v1].size();
         if (sz == 1)
             return;
@@ -801,6 +801,13 @@ namespace bv {
             return out << "bv <- " << m_bits[v1] << " != " << m_bits[v2] << " @" << cidx;
         case bv_justification::kind_t::bv2int:
             return out << "bv <- v" << v1 << " == v" << v2 << " <== " << ctx.bpp(c.a) << " == " << ctx.bpp(c.b) << " == " << ctx.bpp(c.c);
+        case bv_justification::kind_t::bvext: {
+            for (unsigned i = 0; i < c.m_num_literals; ++i)
+                out << c.m_literals[i] << " ";
+            for (unsigned i = 0; i < c.m_num_eqs; ++i)
+                out << ctx.bpp(c.m_eqs[i].first) << " == " << ctx.bpp(c.m_eqs[i].second) << " ";
+            return out << "\n";
+        }            
         default:
             UNREACHABLE();
             break;

From 5c7506306b60b3132d10c4cfb29984540d7a38d6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Mar 2023 17:35:49 -0800
Subject: [PATCH 3/5] missing

---
 src/math/polysat/solver.cpp | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index b4187dda4..6cc43b557 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -180,8 +180,7 @@ namespace polysat {
         if (m_bvars.is_false(lit)) {
             // Input literal contradicts current boolean state (e.g., opposite literals in the input)
             // => conflict only flags the inconsistency
-            set_conflict_at_base_level(dep);
-            m_conflict.insert(~c);  // ~c is true in the solver, need to track its original dependencies
+            set_conflict_at_base_level(dep, ~lit);
             return;
         }
         m_bvars.assumption(lit, m_level, dep);

From b84f9694cd20c232c364b7c8b81d75fc5b3e9983 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Mar 2023 21:39:46 -0800
Subject: [PATCH 4/5] undo unnecessary change

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/conflict.cpp | 11 +----------
 src/math/polysat/conflict.h   |  3 ---
 src/math/polysat/solver.cpp   |  3 ++-
 src/math/polysat/solver.h     |  1 -
 4 files changed, 3 insertions(+), 15 deletions(-)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 37347b7da..8116283df 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -167,7 +167,6 @@ namespace polysat {
     void conflict::reset() {
         m_literals.reset();
         m_vars.reset();
-        m_dep_literal = sat::null_literal;
         m_var_occurrences.reset();
         m_vars_occurring.reset();
         m_lemmas.reset();
@@ -185,21 +184,16 @@ namespace polysat {
         return contains(lit) || contains(~lit);
     }
 
-    void conflict::init_at_base_level(dependency dep, sat::literal lit) {
+    void conflict::init_at_base_level(dependency dep) {
         SASSERT(empty());
         SASSERT(s.at_base_level());
         m_level = s.m_level;
         m_dep = dep;
-        m_dep_literal = lit;
         SASSERT(!empty());
         // TODO: logger().begin_conflict???
         // TODO: check uses of logger().begin_conflict(). sometimes we call it before adding constraints, sometimes after...
     }
 
-    void conflict::init_at_base_level(dependency dep) {
-        init_at_base_level(dep, sat::null_literal);
-    }
-
     void conflict::init(signed_constraint c) {
         LOG("Conflict: constraint " << lit_pp(s, c));
         SASSERT(empty());
@@ -590,9 +584,6 @@ namespace polysat {
                 }
             }
         }
-
-        if (m_dep_literal != sat::null_literal)
-            enqueue_lit(m_dep_literal);
         
         for (unsigned d : deps)
             out_deps.push_back(dependency(d));
diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h
index 6cd509c0b..4960aa9b0 100644
--- a/src/math/polysat/conflict.h
+++ b/src/math/polysat/conflict.h
@@ -102,7 +102,6 @@ namespace polysat {
         // Level at which the conflict was discovered
         unsigned m_level = UINT_MAX;
         dependency m_dep = null_dependency;
-        sat::literal m_dep_literal = sat::null_literal;
 
     public:
         conflict(solver& s);
@@ -129,8 +128,6 @@ namespace polysat {
 
         /** conflict due to obvious input inconsistency */
         void init_at_base_level(dependency dep);
-        /** conflict due to obvious input inconsistency with literal */
-        void init_at_base_level(dependency dep, sat::literal lit);
         /** conflict because the constraint c is false under current variable assignment */
         void init(signed_constraint c);
         /** boolean conflict with the given clause */
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 6cc43b557..7415748c0 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -180,7 +180,8 @@ namespace polysat {
         if (m_bvars.is_false(lit)) {
             // Input literal contradicts current boolean state (e.g., opposite literals in the input)
             // => conflict only flags the inconsistency
-            set_conflict_at_base_level(dep, ~lit);
+            set_conflict_at_base_level(dep);
+            m_conflict.insert(~c);
             return;
         }
         m_bvars.assumption(lit, m_level, dep);
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 39f046f93..1f690de7a 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -263,7 +263,6 @@ namespace polysat {
         void propagate_clause(clause& cl);
 
         void set_conflict_at_base_level(dependency dep) { m_conflict.init_at_base_level(dep); }
-        void set_conflict_at_base_level(dependency dep, sat::literal lit) { m_conflict.init_at_base_level(dep, lit); }
         void set_conflict(signed_constraint c) { m_conflict.init(c); }
         void set_conflict(clause& cl) { m_conflict.init(cl); }
         void set_conflict_by_viable_interval(pvar v) { m_conflict.init_by_viable_interval(v); }

From 57d1506a0af1e26055104a17446cadfd6b42088b Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 7 Mar 2023 10:35:33 +0100
Subject: [PATCH 5/5] remove debug output

---
 src/math/polysat/solver.cpp | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 7415748c0..52ce95648 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -599,7 +599,6 @@ namespace polysat {
 #if 0
         m_fixed_bits.push();
 #endif
-        display(verbose_stream() << "push\n");
     }
 
     void solver::pop_levels(unsigned num_levels) {
@@ -711,8 +710,6 @@ namespace polysat {
             m_trail.push_back(trail_instr_t::assign_bool_i);
             LOG("Replay: " << lit);
         }
-
-        display(verbose_stream());
     }
 
     bool solver::can_decide() const {