From 0b17a14c83cfbc597802283b7a24bb946ce47179 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 21 Jul 2023 10:19:21 +0200 Subject: [PATCH] extract/concat plumbing --- src/math/polysat/solver.h | 11 ++++----- src/sat/smt/bv_polysat.cpp | 49 +++++++++++++++++++++++++++++++------- src/sat/smt/bv_solver.cpp | 4 ++++ src/sat/smt/bv_solver.h | 3 +++ 4 files changed, 52 insertions(+), 15 deletions(-) diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index ddade9d2f..f7e6ed48f 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -320,9 +320,6 @@ namespace polysat { void push_reinit_stack(clause& c); - /** Get variable representing v[hi:lo] */ - pvar extract_var(pvar v, unsigned hi, unsigned lo); - void add_clause(clause_ref clause); void add_clause(clause& clause); void add_clause(signed_constraint c1, bool is_redundant); @@ -415,11 +412,11 @@ namespace polysat { */ pdd var(pvar v) { return m_vars[v]; } - /** Create expression for v[hi:lo] */ - pdd extract(pvar v, unsigned hi, unsigned lo); - /** Create expression for p[hi:lo] */ - pdd extract(pdd const& p, unsigned hi, unsigned lo); + pdd extract(pdd const& p, unsigned hi, unsigned lo) { return m_constraints.extract(p, hi, lo); } + + /** Create expression for concatenation of args */ + pdd concat(unsigned num_args, pdd const* args) { return m_constraints.concat(num_args, args); } /** * Create terms for unsigned quot-rem diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp index e529d66ba..b07b6315c 100644 --- a/src/sat/smt/bv_polysat.cpp +++ b/src/sat/smt/bv_polysat.cpp @@ -32,9 +32,11 @@ namespace bv { void solver::internalize_polysat(app* a) { + // verbose_stream() << "internalize_polysat: " << mk_ismt2_pp(a, m) << "\n"; + #define if_unary(F) if (a->get_num_args() == 1) { polysat_unary(a, [&](pdd const& p) { return F(p); }); break; } - switch (to_app(a)->get_decl_kind()) { + switch (a->get_decl_kind()) { case OP_BMUL: polysat_binary(a, [&](pdd const& p, pdd const& q) { return p * q; }); break; case OP_BADD: polysat_binary(a, [&](pdd const& p, pdd const& q) { return p + q; }); break; case OP_BSUB: polysat_binary(a, [&](pdd const& p, pdd const& q) { return p - q; }); break; @@ -64,11 +66,23 @@ namespace bv { case OP_BUMUL_NO_OVFL: polysat_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.umul_ovfl(p, q); }); break; case OP_BSMUL_NO_OVFL: polysat_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.smul_ovfl(p, q); }); break; case OP_BSMUL_NO_UDFL: polysat_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.smul_udfl(p, q); }); break; - - case OP_BUDIV_I: polysat_div_rem_i(a, true); break; + + case OP_BUMUL_OVFL: + case OP_BSMUL_OVFL: + case OP_BSDIV_OVFL: + case OP_BNEG_OVFL: + case OP_BUADD_OVFL: + case OP_BSADD_OVFL: + case OP_BUSUB_OVFL: + case OP_BSSUB_OVFL: + // handled by bv_rewriter for now + UNREACHABLE(); + 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_BUDIV: polysat_div_rem(a, true); break; case OP_BUREM: polysat_div_rem(a, false); break; case OP_BSDIV0: break; case OP_BUDIV0: break; @@ -76,6 +90,12 @@ namespace bv { case OP_BUREM0: break; case OP_BSMOD0: break; + case OP_EXTRACT: polysat_extract(a); break; + case OP_CONCAT: polysat_concat(a); break; + + case OP_ZERO_EXT: + case OP_SIGN_EXT: + // polysat::solver should also support at least: case OP_BREDAND: // x == 2^K - 1 case OP_BREDOR: // x > 0 @@ -87,10 +107,6 @@ namespace bv { case OP_BSMOD_I: case OP_BASHR: 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; @@ -164,6 +180,23 @@ namespace bv { } } + void solver::polysat_extract(app* e) { + unsigned const hi = bv.get_extract_high(e); + unsigned const lo = bv.get_extract_low(e); + auto const src = expr2pdd(e->get_arg(0)); + auto const p = m_polysat.extract(src, hi, lo); + polysat_set(e, p); + } + + void solver::polysat_concat(app* e) { + SASSERT(bv.is_concat(e)); + vector args; + for (unsigned i = 0; i < e->get_num_args(); ++i) + args.push_back(expr2pdd(e->get_arg(i))); + auto const p = m_polysat.concat(args.size(), args.data()); + polysat_set(e, p); + } + void solver::polysat_binary(app* e, std::function const& fn) { SASSERT(e->get_num_args() >= 1); auto p = expr2pdd(e->get_arg(0)); diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index 2c00e888b..976930d29 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -59,6 +59,10 @@ namespace bv { m_bb.set_flat_and_or(false); } + void solver::updt_params(params_ref const& p) { + m_polysat.updt_params(p); + } + bool solver::is_fixed(euf::theory_var v, expr_ref& val, sat::literal_vector& lits) { numeral n; if (!get_fixed_value(v, n)) diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index 8f5e45569..30fcc9fe4 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -325,6 +325,8 @@ namespace bv { void polysat_pop(unsigned n); void polysat_unary(app* e, std::function const& fn); void polysat_binary(app* e, std::function const& fn); + void polysat_extract(app* e); + void polysat_concat(app* e); polysat::pdd expr2pdd(expr* e); void polysat_set(euf::theory_var v, polysat::pdd const& p); polysat::pdd var2pdd(euf::theory_var v); @@ -404,6 +406,7 @@ namespace bv { public: solver(euf::solver& ctx, theory_id id); + void updt_params(params_ref const& p) override; void set_lookahead(sat::lookahead* s) override { } void init_search() override {} double get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const override;