From 4af6238f1c006d917cbc5691976d44dd3ebccf4f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Dec 2023 10:35:13 -0800 Subject: [PATCH] weed out some bugs, add more bv op support in intblast and polysat solvers Signed-off-by: Nikolaj Bjorner --- src/sat/smt/intblast_solver.cpp | 57 ++++++++++---- src/sat/smt/polysat/core.cpp | 13 ++-- src/sat/smt/polysat/types.h | 18 ----- src/sat/smt/polysat/viable.h | 20 +++++ src/sat/smt/polysat_internalize.cpp | 110 +++++++++++++++++++++++++--- src/sat/smt/polysat_solver.cpp | 28 +------ src/sat/smt/polysat_solver.h | 6 ++ 7 files changed, 175 insertions(+), 77 deletions(-) diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index 5d9608163..592c8c0f4 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -543,16 +543,17 @@ namespace intblast { auto rotate_left = [&](unsigned n) { auto sz = bv.get_bv_size(e); + n = n % sz; expr* r = arg(0); if (n != 0 && sz != 1) { // r[sz - n - 1 : 0] ++ r[sz - 1 : sz - n] - // r * 2^(sz - n) + (r / 2^(sz - n)) mod n??? - NOT_IMPLEMENTED_YET(); + // r * 2^(sz - n) + (r div 2^n) mod 2^(sz - n)??? + // r * A + (r div B) mod A auto N = bv_size(e); auto A = rational::power_of_two(sz - n); auto B = rational::power_of_two(n); - auto hi = a.mk_mul(r, a.mk_int(B)); - auto lo = a.mk_idiv(a.mk_mod(r, a.mk_int(B)), a.mk_int(A)); + auto hi = a.mk_mul(r, a.mk_int(A)); + auto lo = a.mk_mod(a.mk_idiv(umod(e, 0), a.mk_int(B)), a.mk_int(A)); r = a.mk_add(hi, lo); } return r; @@ -607,7 +608,7 @@ namespace intblast { break; case OP_CONCAT: { unsigned sz = 0; - for (unsigned i = args.size(); i-- > 0; ++i) { + for (unsigned i = args.size(); i-- > 0;) { expr* old_arg = e->get_arg(i); expr* new_arg = umod(old_arg, i); if (sz > 0) { @@ -809,20 +810,48 @@ namespace intblast { break; } case OP_ROTATE_RIGHT: { - auto n = e->get_parameter(0).get_int(); unsigned sz = bv.get_bv_size(e); - n = n % sz; + auto n = e->get_parameter(0).get_int(); r = rotate_left(sz - n); break; } - case OP_EXT_ROTATE_LEFT: - case OP_EXT_ROTATE_RIGHT: - case OP_REPEAT: - case OP_BREDOR: - case OP_BREDAND: - verbose_stream() << mk_pp(e, m) << "\n"; - NOT_IMPLEMENTED_YET(); + case OP_EXT_ROTATE_LEFT: { + unsigned sz = bv.get_bv_size(e); + expr* y = umod(e, 1); + r = a.mk_int(0); + for (unsigned i = 0; i < sz; ++i) + r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(i), r); break; + } + case OP_EXT_ROTATE_RIGHT: { + unsigned sz = bv.get_bv_size(e); + expr* y = umod(e, 1); + r = a.mk_int(0); + for (unsigned i = 0; i < sz; ++i) + r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(sz - i), r); + break; + } + case OP_REPEAT: { + unsigned n = e->get_parameter(0).get_int(); + expr* x = umod(e->get_arg(0), 0); + r = x; + rational N = bv_size(e->get_arg(0)); + rational N0 = N; + for (unsigned i = 1; i < n; ++i) + r = a.mk_add(a.mk_mul(a.mk_int(N), x), r), N *= N0; + break; + } + case OP_BREDOR: { + r = umod(e->get_arg(0), 0); + r = m.mk_not(m.mk_eq(r, a.mk_int(0))); + break; + } + case OP_BREDAND: { + rational N = bv_size(e->get_arg(0)); + r = umod(e->get_arg(0), 0); + r = m.mk_not(m.mk_eq(r, a.mk_int(N - 1))); + break; + } default: verbose_stream() << mk_pp(e, m) << "\n"; NOT_IMPLEMENTED_YET(); diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index c0b56a3d8..b3f8474b7 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -140,14 +140,14 @@ namespace polysat { for (; i < sz && j < 2; ++i) if (!is_assigned(vars[i])) std::swap(vars[i], vars[j++]); - sc.set_num_watch(i); - if (i > 0) + sc.set_num_watch(j); + if (j > 0) add_watch(idx, vars[0]); - if (i > 1) + if (j > 1) add_watch(idx, vars[1]); IF_VERBOSE(10, verbose_stream() << "add watch " << sc << " " << vars << " "; - if (vars.size() > 0) verbose_stream() << "( " << idx << " : " << m_watch[vars[0]] << ") "; - if (vars.size() > 1) verbose_stream() << "( " << idx << " : " << m_watch[vars[1]] << ") "; + if (j > 0) verbose_stream() << "( " << idx << " : " << m_watch[vars[0]] << ") "; + if (j > 1) verbose_stream() << "( " << idx << " : " << m_watch[vars[1]] << ") "; verbose_stream() << "\n"); s.trail().push(mk_add_watch(*this)); return idx; @@ -227,7 +227,6 @@ namespace polysat { m_assignment.push(v , value); s.trail().push(mk_assign_var(v, *this)); - return; // update the watch lists for pvars // remove constraints from m_watch[v] that have more than 2 free variables. // for entries where there is only one free variable left add to viable set @@ -242,7 +241,7 @@ namespace polysat { bool swapped = false; for (unsigned i = vars.size(); i-- > 2; ) { if (!is_assigned(vars[i])) { - verbose_stream() << "watch instead " << idx << " " << vars[i] << "instead of " << vars[0] << "\n"; + verbose_stream() << "watch instead " << vars[i] << " instead of " << vars[0] << " for " << idx << "\n"; add_watch(idx, vars[i]); std::swap(vars[i], vars[0]); swapped = true; diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h index e7beb3eb1..d0b5f7bca 100644 --- a/src/sat/smt/polysat/types.h +++ b/src/sat/smt/polysat/types.h @@ -59,24 +59,6 @@ namespace polysat { return out << "v" << d.eq().first << " == v" << d.eq().second << "@" << d.level(); } - struct trailing_bits { - unsigned length; - rational bits; - bool positive; - unsigned src_idx; - }; - - struct leading_bits { - unsigned length; - bool positive; // either all 0 or all 1 - unsigned src_idx; - }; - - struct single_bit { - bool positive; - unsigned position; - unsigned src_idx; - }; struct fixed_bits { unsigned hi = 0; diff --git a/src/sat/smt/polysat/viable.h b/src/sat/smt/polysat/viable.h index 5f5af7616..64a8d3194 100644 --- a/src/sat/smt/polysat/viable.h +++ b/src/sat/smt/polysat/viable.h @@ -33,6 +33,26 @@ namespace polysat { resource_out, }; + struct trailing_bits { + unsigned length; + rational bits; + bool positive; + unsigned src_idx; + }; + + struct leading_bits { + unsigned length; + bool positive; // either all 0 or all 1 + unsigned src_idx; + }; + + struct single_bit { + bool positive; + unsigned position; + unsigned src_idx; + }; + + class core; class constraints; diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index ef469fe6f..0ba59de0a 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -139,20 +139,21 @@ namespace polysat { case OP_ZERO_EXT: internalize_zero_extend(a); break; case OP_SIGN_EXT: internalize_sign_extend(a); break; - // polysat::solver should also support at least: + case OP_BSREM: + case OP_BSREM_I: + case OP_BSMOD: + case OP_BSMOD_I: + case OP_BSDIV: + case OP_BSDIV_I: + expr2pdd(a); + m_delayed_axioms.push_back(a); + ctx.push(push_back_vector(m_delayed_axioms)); + break; + case OP_BREDAND: // x == 2^K - 1 unary, return single bit, 1 if all input bits are set. case OP_BREDOR: // x > 0 unary, return single bit, 1 if at least one input bit is set. case OP_BCOMP: // x == y binary, return single bit, 1 if the arguments are equal. - case OP_BSDIV: - case OP_BSREM: - case OP_BSMOD: - case OP_BSDIV_I: - case OP_BSREM_I: - case OP_BSMOD_I: - IF_VERBOSE(0, verbose_stream() << mk_pp(a, m) << "\n"); - NOT_IMPLEMENTED_YET(); - return; default: IF_VERBOSE(0, verbose_stream() << mk_pp(a, m) << "\n"); NOT_IMPLEMENTED_YET(); @@ -263,7 +264,94 @@ namespace polysat { expr* x, * y; VERIFY(bv.is_bv_shl(n, x, y)); m_core.shl(expr2pdd(x), expr2pdd(y), expr2pdd(n)); - } + } + + bool solver::propagate_delayed_axioms() { + if (m_delayed_axioms_qhead == m_delayed_axioms.size()) + return false; + ctx.push(value_trail(m_delayed_axioms_qhead)); + for (; m_delayed_axioms_qhead < m_delayed_axioms.size() && !inconsistent(); ++m_delayed_axioms_qhead) { + app* e = m_delayed_axioms[m_delayed_axioms_qhead]; + expr* x, *y; + if (bv.is_bv_sdiv(e, x, y)) + axiomatize_sdiv(e, x, y); + else if (bv.is_bv_sdivi(e, x, y)) + axiomatize_sdiv(e, x, y); + else if (bv.is_bv_srem(e, x, y)) + axiomatize_srem(e, x, y); + else if (bv.is_bv_sremi(e, x, y)) + axiomatize_srem(e, x, y); + else if (bv.is_bv_smod(e, x, y)) + axiomatize_smod(e, x, y); + else if (bv.is_bv_smodi(e, x, y)) + axiomatize_smod(e, x, y); + else + UNREACHABLE(); + } + return true; + } + + // y = 0 -> x + // else x - sdiv(x, y) * y + void solver::axiomatize_srem(app* e, expr* x, expr* y) { + unsigned sz = bv.get_bv_size(x); + sat::literal y_eq0 = eq_internalize(y, bv.mk_zero(sz)); + add_clause(~y_eq0, eq_internalize(e, x)); + add_clause(y_eq0, eq_internalize(e, bv.mk_bv_mul(bv.mk_bv_sdiv(x, y), y))); + } + + // u := umod(x, y) + // u = 0 -> 0 + // y = 0 -> x + // x < 0, y < 0 -> -u + // x < 0, y >= 0 -> y - u + // x >= 0, y < 0 -> y + u + // x >= 0, y >= 0 -> u + void solver::axiomatize_smod(app* e, expr* x, expr* y) { + unsigned sz = bv.get_bv_size(x); + expr* u = bv.mk_bv_urem(x, y); + rational N = rational::power_of_two(bv.get_bv_size(x)); + expr* signx = bv.mk_ule(bv.mk_numeral(N / 2, sz), x); + expr* signy = bv.mk_ule(bv.mk_numeral(N / 2, sz), y); + sat::literal lsignx = mk_literal(signx); + sat::literal lsigny = mk_literal(signy); + sat::literal u_eq0 = eq_internalize(u, bv.mk_zero(sz)); + sat::literal y_eq0 = eq_internalize(y, bv.mk_zero(sz)); + add_clause(~u_eq0, eq_internalize(e, bv.mk_zero(sz))); + add_clause(u_eq0, ~y_eq0, eq_internalize(e, x)); + add_clause(~lsignx, ~lsigny, eq_internalize(e, bv.mk_bv_neg(u))); + add_clause(y_eq0, ~lsignx, lsigny, eq_internalize(e, bv.mk_bv_sub(y, u))); + add_clause(y_eq0, lsignx, ~lsigny, eq_internalize(e, bv.mk_bv_add(y, u))); + add_clause(y_eq0, lsignx, lsigny, eq_internalize(e, u)); + } + + + // d = udiv(abs(x), abs(y)) + // y = 0, x > 0 -> 1 + // y = 0, x <= 0 -> -1 + // x = 0, y != 0 -> 0 + // x > 0, y < 0 -> -d + // x < 0, y > 0 -> -d + // x > 0, y > 0 -> d + // x < 0, y < 0 -> d + void solver::axiomatize_sdiv(app* e, expr* x, expr* y) { + unsigned sz = bv.get_bv_size(x); + rational N = rational::power_of_two(bv.get_bv_size(x)); + expr* signx = bv.mk_ule(bv.mk_numeral(N/2, sz), x); + expr* signy = bv.mk_ule(bv.mk_numeral(N/2, sz), y); + expr* absx = m.mk_ite(signx, bv.mk_bv_sub(bv.mk_numeral(N-1, sz), x), x); + expr* absy = m.mk_ite(signy, bv.mk_bv_sub(bv.mk_numeral(N-1, sz), y), y); + expr* d = bv.mk_bv_udiv(absx, absy); + sat::literal lsignx = mk_literal(signx); + sat::literal lsigny = mk_literal(signy); + sat::literal y_eq0 = eq_internalize(y, bv.mk_zero(sz)); + add_clause(~y_eq0, ~lsignx, eq_internalize(e, bv.mk_numeral(1, sz))); + add_clause(~y_eq0, lsignx, eq_internalize(e, bv.mk_numeral(N-1, sz))); + add_clause(y_eq0, lsignx, ~lsigny, eq_internalize(e, bv.mk_bv_neg(d))); + add_clause(y_eq0, ~lsignx, lsigny, eq_internalize(e, bv.mk_bv_neg(d))); + add_clause(y_eq0, lsignx, lsigny, eq_internalize(e, d)); + add_clause(y_eq0, ~lsignx, ~lsigny, eq_internalize(e, d)); + } void solver::internalize_urem_i(app* rem) { expr* x, *y; diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index 271b6986e..0fa4ab8e6 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -52,7 +52,7 @@ namespace polysat { } bool solver::unit_propagate() { - return m_core.propagate(); + return m_core.propagate() || propagate_delayed_axioms(); } sat::check_result solver::check() { @@ -266,32 +266,6 @@ 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(e)) { - sc = *std::get_if(&e); - constraint_count++; - } - } - if (constraint_count == 1) { - auto lit = ctx.mk_literal(constraint2expr(sc)); - svector eqs; - for (auto e : cs) { - if (std::holds_alternative(e)) { - auto d = *std::get_if(&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(e)) { auto d = *std::get_if(&e); diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h index e88eafdd2..c8d9e314d 100644 --- a/src/sat/smt/polysat_solver.h +++ b/src/sat/smt/polysat_solver.h @@ -130,6 +130,12 @@ namespace polysat { void internalize_udiv_i(app* e); void internalize_urem_i(app* e); void internalize_div_rem(app* e, bool is_div); + void axiomatize_srem(app* e, expr* x, expr* y); + void axiomatize_smod(app* e, expr* x, expr* y); + void axiomatize_sdiv(app* e, expr* x, expr* y); + unsigned m_delayed_axioms_qhead = 0; + ptr_vector m_delayed_axioms; + bool propagate_delayed_axioms(); void internalize_polysat(app* a); void assert_bv2int_axiom(app * n); void assert_int2bv_axiom(app* n);