From e0effa3775d3827fa0c15abc3a8b879ce9fad34b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 12 Dec 2023 14:41:31 -0800
Subject: [PATCH] n/a

---
 src/sat/smt/intblast_solver.cpp              |  8 +++---
 src/sat/smt/intblast_solver.h                | 25 +++++++++----------
 src/sat/smt/polysat/umul_ovfl_constraint.cpp |  2 ++
 src/sat/smt/polysat_solver.cpp               | 26 ++++++++++++++++++++
 4 files changed, 44 insertions(+), 17 deletions(-)

diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp
index da3526bb4..9f0541122 100644
--- a/src/sat/smt/intblast_solver.cpp
+++ b/src/sat/smt/intblast_solver.cpp
@@ -233,8 +233,8 @@ namespace intblast {
         }
 
         m_core.reset();
-        m_vars.reset();
         m_translate.reset();
+        m_is_plugin = false;
         m_solver = mk_smt2_solver(m, s.params(), symbol::null);
 
         expr_ref_vector es(m);
@@ -243,8 +243,9 @@ namespace intblast {
 
         translate(es);
 
-        for (auto const& [src, vi] : m_vars) {
-            auto const& [v, b] = vi;
+        for (auto e : m_vars) {
+            auto v = translated(e);
+            auto b = rational::power_of_two(bv.get_bv_size(e));
             m_solver->assert_expr(a.mk_le(a.mk_int(0), v));
             m_solver->assert_expr(a.mk_lt(v, a.mk_int(b)));
         }
@@ -679,6 +680,7 @@ namespace intblast {
                 }
             }
             break;
+        }
         case OP_BOR: {
             // p | q := (p + q) - band(p, q)
             IF_VERBOSE(2, verbose_stream() << "bor " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h
index 35790c6aa..e9b2527a6 100644
--- a/src/sat/smt/intblast_solver.h
+++ b/src/sat/smt/intblast_solver.h
@@ -46,14 +46,6 @@ namespace euf {
 namespace intblast {
 
     class solver : public euf::th_euf_solver {
-<<<<<<< HEAD
-=======
-        struct var_info {
-            expr* dst;
-            rational sz;
-        };
-
->>>>>>> 4cadf6d9f (preparing intblaster as self-contained solver.)
         euf::solver& ctx;
         sat::solver& s;
         ast_manager& m;
@@ -62,7 +54,6 @@ namespace intblast {
         scoped_ptr<::solver> m_solver;
         obj_map<func_decl, func_decl*> m_new_funs;
         expr_ref_vector m_translate, m_args;
-        ast_ref_vector m_pinned;
         sat::literal_vector m_core;
         ptr_vector<app> m_bv2int, m_int2bv;
         statistics m_stats;
@@ -103,14 +94,13 @@ namespace intblast {
         void add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values);
         void add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values);
 
-        expr* translated(expr* e) { expr* r = m_translate.get(e->get_id(), nullptr); SASSERT(r); return r; }
+        expr* translated(expr* e) const { expr* r = m_translate.get(e->get_id(), nullptr); SASSERT(r); return r; }
         void set_translated(expr* e, expr* r) { m_translate.setx(e->get_id(), r); }
         expr* arg(unsigned i) { return m_args.get(i); }
 
-        expr* mk_mod(expr* x);
-        expr* mk_smod(expr* x);
-        expr* bv_expr = nullptr;
-        rational bv_size();
+        expr* umod(expr* bv_expr, unsigned i);
+        expr* smod(expr* bv_expr, unsigned i);
+        rational bv_size(expr* bv_expr);
 
         void translate_expr(expr* e);
         void translate_bv(app* e);
@@ -122,8 +112,15 @@ namespace intblast {
         void ensure_args(app* e);
         void internalize_bv(app* e);
 
+        unsigned m_vars_qhead = 0;
+        ptr_vector<expr> m_vars;
+        void add_bound_axioms();
+
         euf::theory_var mk_var(euf::enode* n) override;
 
+        void add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values);
+        void add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values);
+
     public:
         solver(euf::solver& ctx);
         
diff --git a/src/sat/smt/polysat/umul_ovfl_constraint.cpp b/src/sat/smt/polysat/umul_ovfl_constraint.cpp
index 5d185e7ee..445169c2f 100644
--- a/src/sat/smt/polysat/umul_ovfl_constraint.cpp
+++ b/src/sat/smt/polysat/umul_ovfl_constraint.cpp
@@ -77,6 +77,8 @@ namespace polysat {
     }
 
     void umul_ovfl_constraint::propagate(core& c, lbool value, dependency const& dep) {
+        if (value == l_undef)
+            return;
         auto& C = c.cs();
         auto p1 = c.subst(p());
         auto q1 = c.subst(q());
diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp
index 690548aaa..c14ca1d14 100644
--- a/src/sat/smt/polysat_solver.cpp
+++ b/src/sat/smt/polysat_solver.cpp
@@ -256,6 +256,32 @@ namespace polysat {
 
     void solver::add_polysat_clause(char const* name, core_vector cs, bool is_redundant) {
         sat::literal_vector lits;
+        signed_constraint sc;
+        unsigned constraint_count = 0;
+        for (auto e : cs) {
+            if (std::holds_alternative<signed_constraint>(e)) {
+                sc = *std::get_if<signed_constraint>(&e);
+                constraint_count++;
+            }
+        }
+        if (constraint_count == 1) {
+            auto lit = ctx.mk_literal(constraint2expr(sc));
+            svector<euf::enode_pair> eqs;
+            for (auto e : cs) {
+                if (std::holds_alternative<dependency>(e)) {
+                    auto d = *std::get_if<dependency>(&e);
+                    if (d.is_literal())
+                        lits.push_back(d.literal());
+                    else if (d.is_eq()) {
+                        auto [v1, v2] = d.eq();
+                        eqs.push_back({ var2enode(v1), var2enode(v2) });
+                    }
+                }
+            }
+            ctx.propagate(lit, euf::th_explain::propagate(*this, lits, eqs, lit, nullptr));
+            return;
+        }
+
         for (auto e : cs) {
             if (std::holds_alternative<dependency>(e)) {
                 auto d = *std::get_if<dependency>(&e);