From ff93c039726a7d4470977ee1eec4ead2b8f3c9ab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 26 Jan 2022 20:20:45 +0100 Subject: [PATCH] integrate polysat into bv solver Signed-off-by: Nikolaj Bjorner --- src/math/polysat/boolean.cpp | 4 +- src/math/polysat/boolean.h | 8 +- src/math/polysat/solver.cpp | 11 +- src/math/polysat/solver.h | 59 ++--- src/math/polysat/types.h | 4 +- src/sat/smt/CMakeLists.txt | 2 + src/sat/smt/bv_delay_internalize.cpp | 24 +- src/sat/smt/bv_internalize.cpp | 17 +- src/sat/smt/bv_polysat.cpp | 324 +++++++++++++++++++++++++++ src/sat/smt/bv_solver.cpp | 37 ++- src/sat/smt/bv_solver.h | 38 +++- src/sat/smt/euf_solver.h | 1 + src/smt/params/smt_params_helper.pyg | 2 +- src/smt/params/theory_bv_params.h | 2 +- 14 files changed, 459 insertions(+), 74 deletions(-) create mode 100644 src/sat/smt/bv_polysat.cpp diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp index 253be8fad..55241f878 100644 --- a/src/math/polysat/boolean.cpp +++ b/src/math/polysat/boolean.cpp @@ -78,13 +78,13 @@ namespace polysat { SASSERT(is_propagation(lit)); } - void bool_var_manager::asserted(sat::literal lit, unsigned lvl, unsigned dep) { + void bool_var_manager::asserted(sat::literal lit, unsigned lvl, dep_t dep) { LOG("Asserted " << lit << " @ " << lvl); assign(kind_t::decision, lit, lvl, nullptr, dep); SASSERT(is_decision(lit)); } - void bool_var_manager::assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, unsigned dep) { + void bool_var_manager::assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dep_t dep) { SASSERT(!is_assigned(lit)); SASSERT(k != kind_t::unassigned); m_value[lit.index()] = l_true; diff --git a/src/math/polysat/boolean.h b/src/math/polysat/boolean.h index 7cb7de457..405722c43 100644 --- a/src/math/polysat/boolean.h +++ b/src/math/polysat/boolean.h @@ -29,7 +29,7 @@ namespace polysat { svector m_unused; // previously deleted variables that can be reused by new_var(); svector m_value; // current value (indexed by literal) unsigned_vector m_level; // level of assignment (indexed by variable) - unsigned_vector m_deps; // dependencies of external asserts + svector m_deps; // dependencies of external asserts unsigned_vector m_activity; // svector m_kind; // decision or propagation? // Clause associated with the assignment (indexed by variable): @@ -40,7 +40,7 @@ namespace polysat { var_queue m_free_vars; // free Boolean variables vector> m_watch; // watch list for literals into clauses - void assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, unsigned dep = null_dependency); + void assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dep_t dep = null_dependency); public: @@ -66,7 +66,7 @@ namespace polysat { unsigned level(sat::literal lit) const { return level(lit.var()); } clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); return is_propagation(var) ? m_clause[var] : nullptr; } clause* reason(sat::literal lit) const { return reason(lit.var()); } - unsigned dep(sat::literal lit) const { return lit == sat::null_literal ? null_dependency : m_deps[lit.var()]; } + dep_t dep(sat::literal lit) const { return lit == sat::null_literal ? null_dependency : m_deps[lit.var()]; } clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_clause[var]; } @@ -83,7 +83,7 @@ namespace polysat { void propagate(sat::literal lit, unsigned lvl, clause& reason); void decide(sat::literal lit, unsigned lvl, clause& lemma); void eval(sat::literal lit, unsigned lvl); - void asserted(sat::literal lit, unsigned lvl, unsigned dep); + void asserted(sat::literal lit, unsigned lvl, dep_t dep); void unassign(sat::literal lit); std::ostream& display(std::ostream& out) const; diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index e3d351d64..d22965b4c 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -83,6 +83,12 @@ namespace polysat { return l_undef; } + lbool solver::unit_propagate() { + flet _max_d(m_max_decisions, m_stats.m_num_decisions + 1); + return check_sat(); + } + + dd::pdd_manager& solver::sz2pdd(unsigned sz) const { m_pdd.reserve(sz + 1); if (!m_pdd[sz]) @@ -164,7 +170,7 @@ namespace polysat { } - void solver::assign_eh(signed_constraint c, unsigned dep) { + void solver::assign_eh(signed_constraint c, dep_t dep) { SASSERT(at_base_level()); SASSERT(c); if (is_conflict()) @@ -195,6 +201,7 @@ namespace polysat { m_linear_solver.new_constraint(*c.get()); #endif } + bool solver::can_propagate() { return m_qhead < m_search.size() && !is_conflict(); @@ -592,7 +599,7 @@ namespace polysat { SASSERT(!m_conflict.empty()); } - void solver::unsat_core(unsigned_vector& deps) { + void solver::unsat_core(svector& deps) { deps.reset(); for (auto c : m_conflict) { auto d = m_bvars.dep(c.blit()); diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 1d676ca22..5776037d7 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -192,8 +192,6 @@ namespace polysat { void narrow(pvar v); void linear_propagate(); - /// Evaluate term under the current assignment. - bool try_eval(pdd const& p, rational& out_value) const; bool is_conflict() const { return !m_conflict.empty(); } bool at_base_level() const; @@ -231,6 +229,9 @@ namespace polysat { bool wlist_invariant(); bool assignment_invariant(); bool verify_sat(); + + bool can_propagate(); + void propagate(); public: @@ -255,7 +256,7 @@ namespace polysat { /** * retrieve unsat core dependencies */ - void unsat_core(unsigned_vector& deps); + void unsat_core(svector& deps); /** * Add variable with bit-size. @@ -302,6 +303,11 @@ namespace polysat { unsigned get_level(pvar v) const { SASSERT(is_assigned(v)); return m_justification[v].level(); } + /** + * Evaluate term under the current assignment. + */ + bool try_eval(pdd const& p, rational& out_value) const; + /** Create constraints */ signed_constraint eq(pdd const& p) { return m_constraints.eq(p); } signed_constraint diseq(pdd const& p) { return ~m_constraints.eq(p); } @@ -325,39 +331,38 @@ namespace polysat { signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); } /** Create and activate polynomial constraints. */ - void add_eq(pdd const& p, unsigned dep = null_dependency) { assign_eh(eq(p), dep); } - void add_diseq(pdd const& p, unsigned dep = null_dependency) { assign_eh(diseq(p), dep); } - void add_ule(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(ule(p, q), dep); } - void add_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(ult(p, q), dep); } - void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(sle(p, q), dep); } - void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(slt(p, q), dep); } - void add_noovfl(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(~mul_ovfl(p, q), dep); } - void add_ovfl(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(mul_ovfl(p, q), dep); } + void add_eq(pdd const& p, dep_t dep = null_dependency) { assign_eh(eq(p), dep); } + void add_diseq(pdd const& p, dep_t dep = null_dependency) { assign_eh(diseq(p), dep); } + void add_ule(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(ule(p, q), dep); } + void add_ult(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(ult(p, q), dep); } + void add_sle(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(sle(p, q), dep); } + void add_slt(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(slt(p, q), dep); } + void add_noovfl(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(~mul_ovfl(p, q), dep); } + void add_ovfl(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(mul_ovfl(p, q), dep); } - void add_ule(pdd const& p, rational const& q, unsigned dep = null_dependency) { add_ule(p, p.manager().mk_val(q), dep); } - void add_ule(rational const& p, pdd const& q, unsigned dep = null_dependency) { add_ule(q.manager().mk_val(p), q, dep); } - void add_ule(pdd const& p, unsigned q, unsigned dep = null_dependency) { add_ule(p, rational(q), dep); } - void add_ule(unsigned p, pdd const& q, unsigned dep = null_dependency) { add_ule(rational(p), q, dep); } - void add_ult(pdd const& p, rational const& q, unsigned dep = null_dependency) { add_ult(p, p.manager().mk_val(q), dep); } - void add_ult(rational const& p, pdd const& q, unsigned dep = null_dependency) { add_ult(q.manager().mk_val(p), q, dep); } - void add_ult(pdd const& p, unsigned q, unsigned dep = null_dependency) { add_ult(p, rational(q), dep); } - void add_ult(unsigned p, pdd const& q, unsigned dep = null_dependency) { add_ult(rational(p), q, dep); } - void add_noovfl(pdd const& p, rational const& q, unsigned dep = null_dependency) { add_noovfl(p, p.manager().mk_val(q), dep); } - void add_noovfl(rational const& p, pdd const& q, unsigned dep = null_dependency) { add_noovfl(q, p, dep); } - void add_noovfl(pdd const& p, unsigned q, unsigned dep = null_dependency) { add_noovfl(p, rational(q), dep); } - void add_noovfl(unsigned p, pdd const& q, unsigned dep = null_dependency) { add_noovfl(q, p, dep); } + void add_ule(pdd const& p, rational const& q, dep_t dep = null_dependency) { add_ule(p, p.manager().mk_val(q), dep); } + void add_ule(rational const& p, pdd const& q, dep_t dep = null_dependency) { add_ule(q.manager().mk_val(p), q, dep); } + void add_ule(pdd const& p, unsigned q, dep_t dep = null_dependency) { add_ule(p, rational(q), dep); } + void add_ule(unsigned p, pdd const& q, dep_t dep = null_dependency) { add_ule(rational(p), q, dep); } + void add_ult(pdd const& p, rational const& q, dep_t dep = null_dependency) { add_ult(p, p.manager().mk_val(q), dep); } + void add_ult(rational const& p, pdd const& q, dep_t dep = null_dependency) { add_ult(q.manager().mk_val(p), q, dep); } + void add_ult(pdd const& p, unsigned q, dep_t dep = null_dependency) { add_ult(p, rational(q), dep); } + void add_ult(unsigned p, pdd const& q, dep_t dep = null_dependency) { add_ult(rational(p), q, dep); } + void add_noovfl(pdd const& p, rational const& q, dep_t dep = null_dependency) { add_noovfl(p, p.manager().mk_val(q), dep); } + void add_noovfl(rational const& p, pdd const& q, dep_t dep = null_dependency) { add_noovfl(q, p, dep); } + void add_noovfl(pdd const& p, unsigned q, dep_t dep = null_dependency) { add_noovfl(p, rational(q), dep); } + void add_noovfl(unsigned p, pdd const& q, dep_t dep = null_dependency) { add_noovfl(q, p, dep); } /** * Activate the constraint corresponding to the given boolean variable. * Note: to deactivate, use push/pop. */ - void assign_eh(signed_constraint c, unsigned dep); + void assign_eh(signed_constraint c, dep_t dep); /** - * main state transitions. + * Unit propagation accessible over API. */ - bool can_propagate(); - void propagate(); + lbool unit_propagate(); /** * External context managment. diff --git a/src/math/polysat/types.h b/src/math/polysat/types.h index 0a5cd24b4..6c02b0dd6 100644 --- a/src/math/polysat/types.h +++ b/src/math/polysat/types.h @@ -29,8 +29,8 @@ namespace polysat { typedef dd::bdd bdd; typedef dd::bddv bddv; typedef unsigned pvar; - - const unsigned null_dependency = UINT_MAX; + typedef unsigned dep_t; + const dep_t null_dependency = std::numeric_limits::max();; const pvar null_var = UINT_MAX; } diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index a75c0022d..aefe8cac9 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -14,6 +14,7 @@ z3_add_component(sat_smt bv_delay_internalize.cpp bv_internalize.cpp bv_invariant.cpp + bv_polysat.cpp bv_solver.cpp dt_solver.cpp euf_ackerman.cpp @@ -46,5 +47,6 @@ z3_add_component(sat_smt euf mbp smt_params + polysat ) diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp index 796d0bda1..3b4067532 100644 --- a/src/sat/smt/bv_delay_internalize.cpp +++ b/src/sat/smt/bv_delay_internalize.cpp @@ -357,28 +357,12 @@ namespace bv { } solver::internalize_mode solver::get_internalize_mode(expr* e) { - if (!bv.is_bv(e)) - return internalize_mode::no_delay_i; if (!reflect()) return internalize_mode::no_delay_i; - if (get_config().m_bv_polysat) { - switch (to_app(e)->get_decl_kind()) { - case OP_BMUL: - case OP_BUMUL_NO_OVFL: - case OP_BSMOD_I: - case OP_BUREM_I: - case OP_BUDIV_I: - case OP_BADD: - return internalize_mode::polysat_i; - case OP_BSMUL_NO_OVFL: - case OP_BSMUL_NO_UDFL: - case OP_BSDIV_I: - case OP_BSREM_I: - default: - return internalize_mode::no_delay_i; - } - } - + if (get_config().m_bv_polysat) + return internalize_mode::polysat_i; + if (!bv.is_bv(e)) + return internalize_mode::no_delay_i; if (!get_config().m_bv_delay) return internalize_mode::no_delay_i; internalize_mode mode; diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index 33bede1bd..3922f6d31 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -96,6 +96,8 @@ namespace bv { void solver::apply_sort_cnstr(euf::enode * n, sort * s) { force_push(); + if (polysat_sort_cnstr(n)) + return; get_var(n); } @@ -149,7 +151,7 @@ namespace bv { internalize_circuit(a); break; case internalize_mode::polysat_i: - NOT_IMPLEMENTED_YET(); + internalize_polysat(a); break; default: mk_bits(n->get_th_var(get_id())); @@ -351,8 +353,8 @@ namespace bv { for (expr* bit : bits) { sat::literal lit = ctx.internalize(bit, false, false, m_is_redundant); TRACE("bv", tout << "set " << m_bits[v][i] << " == " << lit << "\n";); - add_clause(~lit, m_bits[v][i]); - add_clause(lit, ~m_bits[v][i]); + add_equiv(lit, m_bits[v][i]); + ctx.add_aux_equiv(lit, m_bits[v][i]); ++i; } return; @@ -545,8 +547,8 @@ namespace bv { unsigned sz = bv.get_bv_size(n); expr_ref zero(bv.mk_numeral(0, sz), m); sat::literal eqZ = eq_internalize(arg2, zero); - sat::literal eqU = mk_literal(iun(arg1)); - sat::literal eqI = mk_literal(ibin(arg1, arg2)); + sat::literal eqU = eq_internalize(n, iun(arg1)); + sat::literal eqI = eq_internalize(n, ibin(arg1, arg2)); add_clause(~eqZ, eqU); add_clause(eqZ, eqI); ctx.add_aux(~eqZ, eqU); @@ -676,12 +678,13 @@ namespace bv { TRACE("bv", tout << "add-bit: " << lit << " " << literal2expr(lit) << "\n";); atom* a = new (get_region()) atom(lit.var()); a->m_occs = new (get_region()) var_pos_occ(v_arg, idx); + polysat_bit2bool(a, arg, idx); insert_bv2a(lit.var(), a); ctx.push(mk_atom_trail(lit.var(), *this)); } else if (lit != lit0) { - add_clause(lit0, ~lit); - add_clause(~lit0, lit); + add_equiv(lit0, lit); + ctx.add_aux_equiv(lit0, lit); } // validate_atoms(); diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp new file mode 100644 index 000000000..860a35daf --- /dev/null +++ b/src/sat/smt/bv_polysat.cpp @@ -0,0 +1,324 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + bv_polysat.cpp + +Abstract: + + PolySAT interface to bit-vector + +Author: + + Nikolaj Bjorner (nbjorner) 2022-01-26 + +Notes: +- equality propagation from polysat? +- reuse bit propagation from bv-solver? +- finish other bit-vector operations +- introduce gradual bit-blasting? + +--*/ + +#include "params/bv_rewriter_params.hpp" +#include "sat/smt/bv_solver.h" +#include "sat/smt/euf_solver.h" +#include "math/polysat/solver.h" + +namespace bv { + + typedef polysat::pdd pdd; + + void solver::internalize_polysat(app* a) { + + std::function bin; + +#define mk_binary(a, fn) bin = fn; polysat_binary(a, bin); + + switch (to_app(a)->get_decl_kind()) { + case OP_BMUL: mk_binary(a, [&](pdd const& p, pdd const& q) { return p * q; }); break; + case OP_BADD: mk_binary(a, [&](pdd const& p, pdd const& q) { return p + q; }); break; + case OP_BSUB: mk_binary(a, [&](pdd const& p, pdd const& q) { return p - q; }); break; + case OP_BLSHR: mk_binary(a, [&](pdd const& p, pdd const& q) { return m_polysat.lshr(p, q); }); break; + case OP_BAND: mk_binary(a, [&](pdd const& p, pdd const& q) { return m_polysat.band(p, q); }); break; + + case OP_BNEG: polysat_neg(a); break; + case OP_MKBV: polysat_mkbv(a); break; + case OP_BV_NUM: polysat_num(a); break; + + case OP_ULEQ: polysat_le(a); break; + case OP_SLEQ: polysat_le(a); break; + case OP_UGEQ: polysat_le(a); break; + case OP_SGEQ: polysat_le(a); break; + case OP_ULT: polysat_le(a); break; + case OP_SLT: polysat_le(a); break; + case OP_UGT: polysat_le(a); break; + case OP_SGT: polysat_le(a); break; + + case OP_BUMUL_NO_OVFL: polysat_umul_noovfl(a); break; + case OP_BUDIV_I: polysat_div_rem_i(a, true); break; + case OP_BUREM_I: polysat_div_rem_i(a, false); break; + + case OP_BUDIV: polysat_div_rem(a, true); break; + case OP_BUREM: polysat_div_rem(a, false); break; + case OP_BSDIV0: break; + case OP_BUDIV0: break; + case OP_BSREM0: break; + case OP_BUREM0: break; + case OP_BSMOD0: break; + + // polysat::solver should also support at least: + case OP_BREDAND: // x == 2^K - 1 + case OP_BREDOR: // x > 0 + case OP_BSDIV: + case OP_BSREM: + case OP_BSMOD: + case OP_BSMUL_NO_OVFL: + case OP_BSMUL_NO_UDFL: + case OP_BSDIV_I: + case OP_BSREM_I: + case OP_BSMOD_I: + case OP_BSHL: + case OP_BASHR: + case OP_BOR: + case OP_BXOR: + case OP_BNAND: + case OP_BNOR: + case OP_BNOT: + case OP_BCOMP: + case OP_SIGN_EXT: + case OP_ZERO_EXT: + case OP_CONCAT: + case OP_EXTRACT: + std::cout << mk_pp(a, m) << "\n"; + NOT_IMPLEMENTED_YET(); + return; + default: + std::cout << "fall back to circuit " << mk_pp(a, m) << "\n"; + internalize_circuit(a); + break; + } + } + + void solver::polysat_umul_noovfl(app* e) { + auto p = expr2pdd(e->get_arg(0)); + auto q = expr2pdd(e->get_arg(1)); + auto sc = ~m_polysat.mul_ovfl(p, q); + sat::literal lit = expr2literal(e); + atom* a = mk_atom(lit.var()); + a->m_sc = sc; + } + + void solver::polysat_div_rem_i(app* e, bool is_div) { + auto p = expr2pdd(e->get_arg(0)); + auto q = expr2pdd(e->get_arg(1)); + auto [quot, rem] = m_polysat.quot_rem(p, q); + polysat_set(e, is_div ? quot : rem); + } + + void solver::polysat_div_rem(app* e, bool is_div) { + bv_rewriter_params p(s().params()); + if (p.hi_div0()) { + polysat_div_rem_i(e, is_div); + return; + } + expr* arg1 = e->get_arg(0); + expr* arg2 = e->get_arg(1); + unsigned sz = bv.get_bv_size(e); + expr_ref zero(bv.mk_numeral(0, sz), m); + sat::literal eqZ = eq_internalize(arg2, zero); + sat::literal eqU = eq_internalize(e, is_div ? bv.mk_bv_udiv0(arg1) : bv.mk_bv_urem0(arg1)); + sat::literal eqI = eq_internalize(e, is_div ? bv.mk_bv_udiv_i(arg1, arg2) : bv.mk_bv_urem_i(arg1, arg2)); + add_clause(~eqZ, eqU); + add_clause(eqZ, eqI); + ctx.add_aux(~eqZ, eqU); + ctx.add_aux(eqZ, eqI); + } + + void solver::polysat_neg(app* e) { + SASSERT(e->get_num_args() == 1); + auto p = expr2pdd(e->get_arg(0)); + polysat_set(e, -p); + } + + void solver::polysat_num(app* a) { + numeral val; + unsigned sz = 0; + VERIFY(bv.is_numeral(a, val, sz)); + auto p = m_polysat.value(val, sz); + polysat_set(a, p); + } + + // TODO - test that internalize works with recursive call on bit2bool + void solver::polysat_mkbv(app* a) { + unsigned i = 0; + for (expr* arg : *a) { + expr_ref b2b(m); + b2b = bv.mk_bit2bool(a, i); + sat::literal bit_i = ctx.internalize(b2b, false, false, m_is_redundant); + sat::literal lit = expr2literal(arg); + add_equiv(lit, bit_i); + ctx.add_aux_equiv(lit, bit_i); + ++i; + } + } + + void solver::polysat_binary(app* e, std::function& fn) { + SASSERT(e->get_num_args() >= 1); + auto p = expr2pdd(e->get_arg(0)); + for (unsigned i = 1; i < e->get_num_args(); ++i) + p = fn(p, expr2pdd(e->get_arg(i))); + polysat_set(e, p); + } + + template + void solver::polysat_le(app* e) { + auto p = expr2pdd(e->get_arg(0)); + auto q = expr2pdd(e->get_arg(1)); + if (Rev) + std::swap(p, q); + + auto sc = Signed ? m_polysat.sle(p, q) : m_polysat.ule(p, q); + if (Negated) + sc = ~sc; + + sat::literal lit = expr2literal(e); + atom* a = mk_atom(lit.var()); + a->m_sc = sc; + } + + void solver::polysat_bit2bool(atom* a, expr* e, unsigned idx) { + if (!use_polysat()) + return; + pdd p = expr2pdd(e); + a->m_sc = m_polysat.bit(p, idx); + } + + void solver::polysat_assign(atom* a) { + polysat::signed_constraint sc = a->m_sc; + if (!sc) + return; + SASSERT(s().value(a->m_bv) != l_undef); + bool sign = l_false == s().value(a->m_bv); + sat::literal lit(a->m_bv, sign); + if (sign) + sc = ~sc; + m_polysat.assign_eh(sc, 1 + 2*lit.index()); + } + + bool solver::polysat_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { + if (!use_polysat()) + return false; + pdd p = var2pdd(r1); + pdd q = var2pdd(r2); + auto sc = m_polysat.eq(p, q); + m_var_eqs.setx(m_var_eqs_head, std::make_pair(v1, v2), std::make_pair(v1, v2)); + ctx.push(value_trail(m_var_eqs_head)); + m_polysat.assign_eh(sc, 2 * m_var_eqs_head); + m_var_eqs_head++; + return true; + } + + bool solver::polysat_diseq_eh(euf::th_eq const& ne) { + 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()); + m_polysat.assign_eh(sc, 1 + 2 * neq.index()); + return true; + } + + void solver::polysat_propagate() { + if (!use_polysat()) + return; + lbool r = m_polysat.unit_propagate(); + if (r == l_false) + polysat_core(); + } + + lbool solver::polysat_final() { + if (!use_polysat()) + return l_true; + lbool r = m_polysat.check_sat(); + if (r == l_false) + polysat_core(); + return r; + } + + void solver::polysat_core() { + svector deps; + sat::literal_vector core; + euf::enode_pair_vector eqs; + m_polysat.unsat_core(deps); + for (auto n : deps) { + if (0 != (n & 1)) + core.push_back(sat::to_literal(n / 2)); + else { + auto [v1, v2] = m_var_eqs[n / 2]; + eqs.push_back(euf::enode_pair(var2enode(v1), var2enode(v2))); + } + } + auto* ex = euf::th_explain::conflict(*this, core, eqs); + ctx.set_conflict(ex); + } + + polysat::pdd solver::expr2pdd(expr* e) { + return var2pdd(get_th_var(e)); + } + + polysat::pdd solver::var2pdd(euf::theory_var v) { + if (!m_var2pdd_valid.get(v, false)) { + unsigned bv_size = get_bv_size(v); + polysat::pvar pv = m_polysat.add_var(bv_size); + m_pddvar2var.setx(pv, v, UINT_MAX); + pdd p = m_polysat.var(pv); + polysat_set(v, p); + return p; + } + return m_var2pdd[v]; + } + + bool solver::polysat_sort_cnstr(euf::enode* n) { + if (!use_polysat()) + return false; + if (!bv.is_bv(n->get_expr())) + return false; + theory_var v = n->get_th_var(get_id()); + if (v == euf::null_theory_var) + v = mk_var(n); + var2pdd(v); + return true; + } + + void solver::polysat_set(expr* e, pdd const& p) { + polysat_set(get_th_var(e), p); + } + + void solver::polysat_set(euf::theory_var v, pdd const& p) { + m_var2pdd.reserve(get_num_vars(), p); + m_var2pdd_valid.reserve(get_num_vars(), false); + ctx.push(set_bitvector_trail(m_var2pdd_valid, v)); + m_var2pdd[v] = p; + } + + void solver::polysat_pop(unsigned n) { + if (!use_polysat()) + return; + m_polysat.pop(n); + } + + void solver::polysat_push() { + if (!use_polysat()) + return; + m_polysat.push(); + } + + void solver::polysat_add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { + auto p = expr2pdd(n->get_expr()); + rational val; + VERIFY(m_polysat.try_eval(p, val)); + values[n->get_root_id()] = bv.mk_numeral(val, get_bv_size(n)); + } +} \ No newline at end of file diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index bc435d7eb..f1237a168 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -52,6 +52,7 @@ namespace bv { euf::th_euf_solver(ctx, symbol("bv"), id), bv(m), m_autil(m), + m_polysat(m.limit()), m_ackerman(*this), m_bb(m, get_config()), m_find(*this) { @@ -217,6 +218,8 @@ namespace bv { return; if (s().is_probing()) return; + if (polysat_diseq_eh(ne)) + return; TRACE("bv", tout << "diff: " << v1 << " != " << v2 << " @" << s().scope_lvl() << "\n";); unsigned sz = m_bits[v1].size(); @@ -400,9 +403,8 @@ namespace bv { if (a) { force_push(); m_prop_queue.push_back(propagation_item(a)); - for (auto p : a->m_bit2occ) { - del_eq_occurs(p.first, p.second); - } + for (auto p : a->m_bit2occ) + del_eq_occurs(p.first, p.second); } } @@ -417,11 +419,13 @@ namespace bv { for (auto vp : *p.m_atom) propagate_bits(vp); for (eq_occurs const& eq : p.m_atom->eqs()) - propagate_eq_occurs(eq); + propagate_eq_occurs(eq); + polysat_assign(p.m_atom); } else propagate_bits(p.m_vp); } + polysat_propagate(); // check_missing_propagation(); return true; } @@ -521,13 +525,19 @@ namespace bv { if (!ok) return sat::check_result::CR_CONTINUE; - return sat::check_result::CR_DONE; + + switch (polysat_final()) { + case l_true: return sat::check_result::CR_DONE; + case l_false: return sat::check_result::CR_CONTINUE; + default: return sat::check_result::CR_GIVEUP; + } } void solver::push_core() { TRACE("bv", tout << "push: " << get_num_vars() << "@" << m_prop_queue_lim.size() << "\n";); th_euf_solver::push_core(); m_prop_queue_lim.push_back(m_prop_queue.size()); + polysat_push(); } void solver::pop_core(unsigned n) { @@ -540,6 +550,8 @@ namespace bv { m_bits.shrink(old_sz); m_wpos.shrink(old_sz); m_zero_one_bits.shrink(old_sz); + polysat_pop(n); + TRACE("bv", tout << "num vars " << old_sz << "@" << m_prop_queue_lim.size() << "\n";); } @@ -605,10 +617,13 @@ namespace bv { lbool solver::get_phase(bool_var v) { return l_undef; } std::ostream& solver::display(std::ostream& out) const { unsigned num_vars = get_num_vars(); - if (num_vars > 0) - out << "bv-solver:\n"; + if (num_vars == 0) + return out; + out << "bv-solver:\n"; for (unsigned v = 0; v < num_vars; v++) out << pp(v); + if (use_polysat()) + m_polysat.display(out); return out; } @@ -662,6 +677,7 @@ namespace bv { st.update("bv bit2eq", m_stats.m_num_bit2eq); st.update("bv bit2ne", m_stats.m_num_bit2ne); st.update("bv ackerman", m_stats.m_ackerman); + m_polysat.collect_statistics(st); } sat::extension* solver::copy(sat::solver* s) { UNREACHABLE(); return nullptr; } @@ -727,6 +743,10 @@ namespace bv { return; } theory_var v = n->get_th_var(get_id()); + if (m_bits[v].empty() && use_polysat()) { + polysat_add_value(n, mdl, values); + return; + } rational val; unsigned i = 0; for (auto l : m_bits[v]) { @@ -748,6 +768,9 @@ namespace bv { void solver::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { + if (polysat_merge_eh(r1, r2, v1, v2)) + return; + TRACE("bv", tout << "merging: v" << v1 << " #" << var2enode(v1)->get_expr_id() << " v" << v2 << " #" << var2enode(v2)->get_expr_id() << "\n";); if (!merge_zero_one_bits(r1, r2)) { diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index 5453871b4..97e389994 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -19,6 +19,7 @@ Author: #include "sat/smt/sat_th.h" #include "sat/smt/bv_ackerman.h" #include "ast/rewriter/bit_blaster/bit_blaster.h" +#include "math/polysat/solver.h" namespace euf { class solver; @@ -166,6 +167,7 @@ namespace bv { svector> m_bit2occ; literal m_var = sat::null_literal; literal m_def = sat::null_literal; + polysat::signed_constraint m_sc; atom(bool_var b) :m_bv(b), m_eqs(nullptr), m_occs(nullptr) {} ~atom() { m_bit2occ.clear(); } var_pos_it begin() const { return var_pos_it(m_occs); } @@ -194,6 +196,7 @@ namespace bv { bv_util bv; arith_util m_autil; + polysat::solver m_polysat; stats m_stats; ackerman m_ackerman; bit_blaster m_bb; @@ -232,7 +235,7 @@ namespace bv { void add_bit(theory_var v, sat::literal lit); atom* mk_atom(sat::bool_var b); void eq_internalized(sat::bool_var b1, sat::bool_var b2, unsigned idx, theory_var v1, theory_var v2, sat::literal eq, euf::enode* n); - void del_eq_occurs(atom* a, eq_occurs* occ); + void del_eq_occurs(atom* a, eq_occurs* occ); void set_bit_eh(theory_var v, literal l, unsigned idx); void init_bits(expr* e, expr_ref_vector const & bits); @@ -263,6 +266,39 @@ namespace bv { void assert_ackerman(theory_var v1, theory_var v2); bool reflect() const { return get_config().m_bv_reflect; } + // polysat + void internalize_polysat(app* a); + void polysat_push(); + void polysat_pop(unsigned n); + void polysat_binary(app* e, std::function& fn); + polysat::pdd expr2pdd(expr* e); + void polysat_set(euf::theory_var v, polysat::pdd const& p); + polysat::pdd var2pdd(euf::theory_var v); + void polysat_set(expr* e, polysat::pdd const& p); + template + void polysat_le(app* n); + void polysat_neg(app* a); + void polysat_num(app* a); + void polysat_mkbv(app* a); + void solver::polysat_umul_noovfl(app* e); + void solver::polysat_div_rem_i(app* e, bool is_div); + void solver::polysat_div_rem(app* e, bool is_div); + void polysat_bit2bool(atom* a, expr* e, unsigned idx); + bool polysat_sort_cnstr(euf::enode* n); + void polysat_assign(atom* a); + void polysat_propagate(); + void polysat_core(); + bool polysat_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2); + bool polysat_diseq_eh(euf::th_eq const& ne); + void polysat_add_value(euf::enode* n, model& mdl, expr_ref_vector& values); + lbool polysat_final(); + bool use_polysat() const { return get_config().m_bv_polysat; } + vector m_var2pdd; + bool_vector m_var2pdd_valid; + unsigned_vector m_pddvar2var; + svector> m_var_eqs; + unsigned m_var_eqs_head = 0; + // delay internalize enum class internalize_mode { delay_i, diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index d299c92d0..d921a6b2c 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -384,6 +384,7 @@ namespace euf { void add_aux(sat::literal_vector const& lits) { add_aux(lits.size(), lits.data()); } void add_aux(unsigned n, sat::literal const* lits) { m_relevancy.add_def(n, lits); } void add_aux(sat::literal a) { sat::literal lits[1] = { a }; add_aux(1, lits); } + void add_aux_equiv(sat::literal a, sat::literal b) { add_aux(~a, b); add_aux(a, ~b); } void add_aux(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_aux(2, lits); } void add_aux(sat::literal a, sat::literal b, sat::literal c) { sat::literal lits[3] = { a, b, c }; add_aux(3, lits); } void mark_relevant(sat::literal lit) { m_relevancy.mark_relevant(lit); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index c0ec6086c..6167a844b 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -50,7 +50,7 @@ def_module_params(module_name='smt', ('bv.eq_axioms', BOOL, True, 'add dynamic equality axioms'), ('bv.watch_diseq', BOOL, False, 'use watch lists instead of eager axioms for bit-vectors'), ('bv.delay', BOOL, True, 'delay internalize expensive bit-vector operations'), - ('bv.polysat', BOOL, True, 'use polysat bit-vector solver'), + ('bv.polysat', BOOL, False, 'use polysat bit-vector solver'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'), diff --git a/src/smt/params/theory_bv_params.h b/src/smt/params/theory_bv_params.h index 4fa62e664..5cfa2fe9a 100644 --- a/src/smt/params/theory_bv_params.h +++ b/src/smt/params/theory_bv_params.h @@ -36,7 +36,7 @@ struct theory_bv_params { bool m_bv_enable_int2bv2int = true; bool m_bv_watch_diseq = false; bool m_bv_delay = true; - bool m_bv_polysat = true; + bool m_bv_polysat = false; theory_bv_params(params_ref const & p = params_ref()) { updt_params(p); }