From a5491804c79748cb9ee5fa04c828b7eef175ce35 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 Dec 2023 19:55:25 -0800 Subject: [PATCH] integrating int-blaster --- src/sat/smt/intblast_solver.cpp | 14 +-- src/sat/smt/polysat/polysat_constraints.cpp | 40 +++++++-- src/sat/smt/polysat/polysat_constraints.h | 24 ++--- src/sat/smt/polysat/polysat_core.cpp | 2 +- src/sat/smt/polysat/polysat_core.h | 36 ++++---- src/sat/smt/polysat/polysat_ule.cpp | 18 ++++ src/sat/smt/polysat/polysat_ule.h | 2 + src/sat/smt/polysat/polysat_umul_ovfl.h | 2 + src/sat/smt/polysat/polysat_viable.cpp | 4 +- src/sat/smt/polysat/polysat_viable.h | 14 +-- src/sat/smt/polysat_internalize.cpp | 99 ++++++++++++++++++--- src/sat/smt/polysat_solver.cpp | 14 +-- src/sat/smt/polysat_solver.h | 9 +- 13 files changed, 209 insertions(+), 69 deletions(-) diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index 80fbc845e..6c451e2a3 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -234,6 +234,8 @@ namespace intblast { } m_core.reset(); + m_vars.reset(); + m_trail.reset(); m_solver = mk_smt2_solver(m, s.params(), symbol::null); expr_ref_vector es(m); @@ -244,12 +246,19 @@ namespace intblast { for (auto const& [src, vi] : m_vars) { auto const& [v, b] = vi; + verbose_stream() << "asserting " << mk_pp(v, m) << " < " << b << "\n"; m_solver->assert_expr(a.mk_le(a.mk_int(0), v)); m_solver->assert_expr(a.mk_lt(v, a.mk_int(b))); } + + verbose_stream() << "check\n"; + m_solver->display(verbose_stream()); + verbose_stream() << es << "\n"; lbool r = m_solver->check_sat(es); + verbose_stream() << "result " << r << "\n"; + if (r == l_false) { expr_ref_vector core(m); m_solver->get_unsat_core(core); @@ -586,7 +595,6 @@ namespace intblast { } break; } -<<<<<<< HEAD case OP_EXTRACT: { unsigned lo, hi; expr* old_arg; @@ -860,10 +868,6 @@ namespace intblast { set_translated(e, e); else set_translated(e, m.mk_app(e->get_decl(), m_args)); -======= - for (unsigned i = 0; i < es.size(); ++i) - es[i] = translated[es.get(i)]; ->>>>>>> 09c2e0dd6 (integrate intblast solver) } rational solver::get_value(expr* e) const { diff --git a/src/sat/smt/polysat/polysat_constraints.cpp b/src/sat/smt/polysat/polysat_constraints.cpp index 99da7b0db..faeea62a4 100644 --- a/src/sat/smt/polysat/polysat_constraints.cpp +++ b/src/sat/smt/polysat/polysat_constraints.cpp @@ -1,4 +1,4 @@ -/*++ +/*++ Copyright (c) 2021 Microsoft Corporation Module Name: @@ -12,6 +12,7 @@ Author: --*/ +#include "util/log.h" #include "sat/smt/polysat/polysat_core.h" #include "sat/smt/polysat/polysat_constraints.h" #include "sat/smt/polysat/polysat_ule.h" @@ -23,16 +24,34 @@ namespace polysat { pdd lhs = p, rhs = q; bool is_positive = true; ule_constraint::simplify(is_positive, lhs, rhs); - auto* c = alloc(ule_constraint, p, q); - m_trail.push(new_obj_trail(c)); - auto sc = signed_constraint(ckind_t::ule_t, c); + auto* cnstr = alloc(ule_constraint, p, q); + c.trail().push(new_obj_trail(cnstr)); + auto sc = signed_constraint(ckind_t::ule_t, cnstr); return is_positive ? sc : ~sc; } signed_constraint constraints::umul_ovfl(pdd const& p, pdd const& q) { - auto* c = alloc(umul_ovfl_constraint, p, q); - m_trail.push(new_obj_trail(c)); - return signed_constraint(ckind_t::umul_ovfl_t, c); + auto* cnstr = alloc(umul_ovfl_constraint, p, q); + c.trail().push(new_obj_trail(cnstr)); + return signed_constraint(ckind_t::umul_ovfl_t, cnstr); + } + + bool signed_constraint::is_eq(pvar& v, rational& val) { + if (m_sign) + return false; + if (!is_ule()) + return false; + auto const& ule = to_ule(); + auto const& l = ule.lhs(), &r = ule.rhs(); + if (!r.is_zero()) + return false; + if (!l.is_unilinear()) + return false; + if (!l.hi().is_one()) + return false; + v = l.var(); + val = -l.lo().val(); + return true; } lbool signed_constraint::eval(assignment& a) const { @@ -44,4 +63,11 @@ namespace polysat { if (m_sign) out << "~"; return out << *m_constraint; } + + bool signed_constraint::is_always_true() const { + return m_sign ? m_constraint->is_always_false() : m_constraint->is_always_true(); + } + bool signed_constraint::is_always_false() const { + return m_sign ? m_constraint->is_always_true() : m_constraint->is_always_false(); + } } diff --git a/src/sat/smt/polysat/polysat_constraints.h b/src/sat/smt/polysat/polysat_constraints.h index 687b3d91a..fdef902e2 100644 --- a/src/sat/smt/polysat/polysat_constraints.h +++ b/src/sat/smt/polysat/polysat_constraints.h @@ -41,6 +41,8 @@ namespace polysat { virtual std::ostream& display(std::ostream& out) const = 0; virtual lbool eval() const = 0; virtual lbool eval(assignment const& a) const = 0; + virtual bool is_always_true() const = 0; + virtual bool is_always_false() const = 0; }; inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); } @@ -61,6 +63,8 @@ namespace polysat { unsigned_vector const& vars() const { return m_constraint->vars(); } unsigned var(unsigned idx) const { return m_constraint->var(idx); } bool contains_var(pvar v) const { return m_constraint->contains_var(v); } + bool is_always_true() const; + bool is_always_false() const; lbool eval(assignment& a) const; ckind_t op() const { return m_op; } bool is_ule() const { return m_op == ule_t; } @@ -68,27 +72,27 @@ namespace polysat { bool is_smul_fl() const { return m_op == smul_fl_t; } ule_constraint const& to_ule() const { return *reinterpret_cast(m_constraint); } umul_ovfl_constraint const& to_umul_ovfl() const { return *reinterpret_cast(m_constraint); } - bool is_eq(pvar& v, rational& val) { throw default_exception("nyi"); } + bool is_eq(pvar& v, rational& val); std::ostream& display(std::ostream& out) const; }; inline std::ostream& operator<<(std::ostream& out, signed_constraint const& c) { return c.display(out); } class constraints { - trail_stack& m_trail; + core& c; public: - constraints(trail_stack& c) : m_trail(c) {} + constraints(core& c) : c(c) {} signed_constraint eq(pdd const& p) { return ule(p, p.manager().mk_val(0)); } signed_constraint eq(pdd const& p, rational const& v) { return eq(p - p.manager().mk_val(v)); } signed_constraint ule(pdd const& p, pdd const& q); - signed_constraint sle(pdd const& p, pdd const& q) { throw default_exception("nyi"); } - signed_constraint ult(pdd const& p, pdd const& q) { throw default_exception("nyi"); } - signed_constraint slt(pdd const& p, pdd const& q) { throw default_exception("nyi"); } + signed_constraint sle(pdd const& p, pdd const& q) { auto sh = rational::power_of_two(p.power_of_2() - 1); return ule(p + sh, q + sh); } + signed_constraint ult(pdd const& p, pdd const& q) { return ~ule(q, p); } + signed_constraint slt(pdd const& p, pdd const& q) { return ~sle(q, p); } signed_constraint umul_ovfl(pdd const& p, pdd const& q); - signed_constraint smul_ovfl(pdd const& p, pdd const& q) { throw default_exception("nyi"); } - signed_constraint smul_udfl(pdd const& p, pdd const& q) { throw default_exception("nyi"); } - signed_constraint bit(pdd const& p, unsigned i) { throw default_exception("nyi"); } + signed_constraint smul_ovfl(pdd const& p, pdd const& q) { throw default_exception("smul ovfl nyi"); } + signed_constraint smul_udfl(pdd const& p, pdd const& q) { throw default_exception("smult-udfl nyi"); } + signed_constraint bit(pdd const& p, unsigned i) { throw default_exception("bit nyi"); } signed_constraint diseq(pdd const& p) { return ~eq(p); } signed_constraint diseq(pdd const& p, pdd const& q) { return diseq(p - q); } @@ -138,4 +142,4 @@ namespace polysat { //signed_constraint even(pdd const& p) { return parity_at_least(p, 1); } //signed_constraint odd(pdd const& p) { return ~even(p); } }; -} \ No newline at end of file +} diff --git a/src/sat/smt/polysat/polysat_core.cpp b/src/sat/smt/polysat/polysat_core.cpp index be25c9af8..f2bb995d7 100644 --- a/src/sat/smt/polysat/polysat_core.cpp +++ b/src/sat/smt/polysat/polysat_core.cpp @@ -80,7 +80,7 @@ namespace polysat { core::core(solver_interface& s) : s(s), m_viable(*this), - m_constraints(s.trail()), + m_constraints(*this), m_assignment(*this), m_var_queue(m_activity) {} diff --git a/src/sat/smt/polysat/polysat_core.h b/src/sat/smt/polysat/polysat_core.h index 144b1256b..5262f2bbe 100644 --- a/src/sat/smt/polysat/polysat_core.h +++ b/src/sat/smt/polysat/polysat_core.h @@ -84,7 +84,8 @@ namespace polysat { void get_bitvector_prefixes(pvar v, pvar_vector& out); void get_fixed_bits(pvar v, svector& fixed_bits); bool inconsistent() const; - + void add_clause(char const* name, std::initializer_list cs, bool is_redundant); + void add_watch(unsigned idx, unsigned var); @@ -114,29 +115,28 @@ namespace polysat { signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); } - pdd lshr(pdd a, pdd b) { throw default_exception("nyi"); } - pdd ashr(pdd a, pdd b) { throw default_exception("nyi"); } - pdd shl(pdd a, pdd b) { throw default_exception("nyi"); } - pdd band(pdd a, pdd b) { throw default_exception("nyi"); } - pdd bxor(pdd a, pdd b) { throw default_exception("nyi"); } - pdd bor(pdd a, pdd b) { throw default_exception("nyi"); } - pdd bnand(pdd a, pdd b) { throw default_exception("nyi"); } - pdd bxnor(pdd a, pdd b) { throw default_exception("nyi"); } - pdd bnor(pdd a, pdd b) { throw default_exception("nyi"); } - pdd bnot(pdd a) { throw default_exception("nyi"); } - std::pair quot_rem(pdd const& n, pdd const& d) { throw default_exception("nyi"); } - pdd zero_ext(pdd a, unsigned sz) { throw default_exception("nyi"); } - pdd sign_ext(pdd a, unsigned sz) { throw default_exception("nyi"); } - pdd extract(pdd src, unsigned hi, unsigned lo) { throw default_exception("nyi"); } - pdd concat(unsigned n, pdd const* args) { throw default_exception("nyi"); } + pdd lshr(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("lshr nyi"); } + pdd ashr(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("ashr nyi"); } + pdd shl(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("shlh nyi"); } + pdd band(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("band nyi"); } + pdd bxor(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("bxor nyi"); } + pdd bor(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("bir ==nyi"); } + pdd bnand(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("bnand nyi"); } + pdd bxnor(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("bxnor nyi"); } + pdd bnor(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("bnotr nyi"); } + pdd bnot(pdd a) { NOT_IMPLEMENTED_YET(); throw default_exception("bnot nyi"); } + pdd zero_ext(pdd a, unsigned sz) { NOT_IMPLEMENTED_YET(); throw default_exception("zero ext nyi"); } + pdd sign_ext(pdd a, unsigned sz) { NOT_IMPLEMENTED_YET(); throw default_exception("sign ext nyi"); } + pdd extract(pdd src, unsigned hi, unsigned lo) { NOT_IMPLEMENTED_YET(); throw default_exception("extract nyi"); } + pdd concat(unsigned n, pdd const* args) { NOT_IMPLEMENTED_YET(); throw default_exception("concat nyi"); } pvar add_var(unsigned sz); pdd var(pvar p) { return m_vars[p]; } - unsigned size(pvar v) const { return var2pdd(v).power_of_2(); } + unsigned size(pvar v) const { return m_vars[v].power_of_2(); } constraints& cs() { return m_constraints; } trail_stack& trail(); - std::ostream& display(std::ostream& out) const { throw default_exception("nyi"); } + std::ostream& display(std::ostream& out) const { NOT_IMPLEMENTED_YET(); throw default_exception("nyi"); } }; } diff --git a/src/sat/smt/polysat/polysat_ule.cpp b/src/sat/smt/polysat/polysat_ule.cpp index 0fb01bcae..7482ec36a 100644 --- a/src/sat/smt/polysat/polysat_ule.cpp +++ b/src/sat/smt/polysat/polysat_ule.cpp @@ -343,4 +343,22 @@ namespace polysat { return eval(a.apply_to(lhs()), a.apply_to(rhs())); } + bool ule_constraint::is_always_true() const { + if (lhs().is_zero()) + return true; // 0 <= p + if (rhs().is_max()) + return true; // p <= -1 + if (lhs().is_val() && rhs().is_val()) + return lhs().val() <= rhs().val(); + return false; + } + + bool ule_constraint::is_always_false() const { + if (lhs().is_never_zero() && rhs().is_zero()) + return true; // p > 0, q = 0 + if (lhs().is_val() && rhs().is_val()) + return lhs().val() > rhs().val(); + return false; + } + } diff --git a/src/sat/smt/polysat/polysat_ule.h b/src/sat/smt/polysat/polysat_ule.h index e21ed1029..2944bf614 100644 --- a/src/sat/smt/polysat/polysat_ule.h +++ b/src/sat/smt/polysat/polysat_ule.h @@ -35,6 +35,8 @@ namespace polysat { std::ostream& display(std::ostream& out) const override; lbool eval() const override; lbool eval(assignment const& a) const override; + bool is_always_true() const override; + bool is_always_false() const override; bool is_eq() const { return m_rhs.is_zero(); } unsigned power_of_2() const { return m_lhs.power_of_2(); } diff --git a/src/sat/smt/polysat/polysat_umul_ovfl.h b/src/sat/smt/polysat/polysat_umul_ovfl.h index 41972ef59..65a12c031 100644 --- a/src/sat/smt/polysat/polysat_umul_ovfl.h +++ b/src/sat/smt/polysat/polysat_umul_ovfl.h @@ -34,6 +34,8 @@ namespace polysat { std::ostream& display(std::ostream& out) const override; lbool eval() const override; lbool eval(assignment const& a) const override; + bool is_always_true() const override { return false; } // todo port + bool is_always_false() const override { return false; } }; } diff --git a/src/sat/smt/polysat/polysat_viable.cpp b/src/sat/smt/polysat/polysat_viable.cpp index 4152956de..35158b889 100644 --- a/src/sat/smt/polysat/polysat_viable.cpp +++ b/src/sat/smt/polysat/polysat_viable.cpp @@ -90,6 +90,8 @@ namespace polysat { } lbool viable::find_viable(pvar v, rational& lo, rational& hi) { + return l_undef; + fixed_bits_info fbi; #if 0 @@ -1007,7 +1009,7 @@ namespace polysat { } void viable::log(pvar v) { - throw default_exception("nyi"); + // } diff --git a/src/sat/smt/polysat/polysat_viable.h b/src/sat/smt/polysat/polysat_viable.h index f426dc326..88070a553 100644 --- a/src/sat/smt/polysat/polysat_viable.h +++ b/src/sat/smt/polysat/polysat_viable.h @@ -186,36 +186,36 @@ namespace polysat { template bool refine_viable(pvar v, rational const& val, fixed_bits_info const& fbi) { - throw default_exception("nyi"); + throw default_exception("refine nyi"); } bool refine_viable(pvar v, rational const& val) { - throw default_exception("nyi"); + throw default_exception("refine nyi"); } template bool refine_bits(pvar v, rational const& val, fixed_bits_info const& fbi) { - throw default_exception("nyi"); + throw default_exception("refine nyi"); } template entry* refine_bits(pvar v, rational const& val, unsigned num_bits, fixed_bits_info const& fbi) { - throw default_exception("nyi"); + throw default_exception("refine nyi"); } bool refine_equal_lin(pvar v, rational const& val) { - throw default_exception("nyi"); + throw default_exception("refine nyi"); } bool refine_disequal_lin(pvar v, rational const& val) { - throw default_exception("nyi"); + throw default_exception("refine nyi"); } void set_conflict_by_interval(pvar v, unsigned w, ptr_vector& intervals, unsigned first_interval); bool set_conflict_by_interval_rec(pvar v, unsigned w, entry** intervals, unsigned num_intervals, bool& create_lemma, uint_set& vars_to_explain); std::pair find_value(rational const& val, entry* entries) { - throw default_exception("nyi"); + throw default_exception("fine_value nyi"); } bool collect_bit_information(pvar v, bool add_conflict, fixed_bits_info& out_fbi); diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index 95979348d..96f7def0e 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -1,4 +1,4 @@ -/*++ +/*++ Copyright (c) 2022 Microsoft Corporation Module Name: @@ -22,7 +22,9 @@ Author: namespace polysat { euf::theory_var solver::mk_var(euf::enode* n) { - return euf::th_euf_solver::mk_var(n); + theory_var v = euf::th_euf_solver::mk_var(n); + ctx.attach_th_var(n, this, v); + return v; } sat::literal solver::internalize(expr* e, bool sign, bool root) { @@ -115,12 +117,13 @@ namespace polysat { case OP_BSADD_OVFL: case OP_BUSUB_OVFL: case OP_BSSUB_OVFL: + verbose_stream() << mk_pp(a, m) << "\n"; // handled by bv_rewriter for now UNREACHABLE(); break; - case OP_BUDIV_I: internalize_div_rem_i(a, true); break; - case OP_BUREM_I: internalize_div_rem_i(a, false); break; + case OP_BUDIV_I: internalize_udiv_i(a); break; + case OP_BUREM_I: internalize_urem_i(a); break; case OP_BUDIV: internalize_div_rem(a, true); break; case OP_BUREM: internalize_div_rem(a, false); break; @@ -187,17 +190,93 @@ namespace polysat { mk_atom(lit.var(), sc); } - void solver::internalize_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_core.quot_rem(p, q); - internalize_set(e, is_div ? quot : rem); + void solver::internalize_udiv_i(app* e) { + expr* x, *y; + VERIFY(bv.is_bv_udivi(e, x, y) || bv.is_bv_udiv(e, x, y)); + app_ref rm(bv.mk_bv_urem_i(x, y), m); + internalize(rm); + } + + void solver::internalize_urem_i(app* e) { + expr* x, *y; + if (expr2enode(e)) + return; + VERIFY(bv.is_bv_uremi(e, x, y) || bv.is_bv_urem(e, x, y)); + auto [quot, rem] = quot_rem(x, y); + internalize_set(e, rem); + internalize_set(bv.mk_bv_udiv_i(x, y), quot); + } + + std::pair solver::quot_rem(expr* x, expr* y) { + pdd a = expr2pdd(x); + pdd b = expr2pdd(y); + auto& m = a.manager(); + unsigned sz = m.power_of_2(); + if (b.is_zero()) + // By SMT-LIB specification, b = 0 ==> q = -1, r = a. + return { m.mk_val(m.max_value()), a }; + + if (b.is_one()) + return { a, m.zero() }; + + if (a.is_val() && b.is_val()) { + rational const av = a.val(); + rational const bv = b.val(); + SASSERT(!bv.is_zero()); + rational rv; + rational qv = machine_div_rem(av, bv, rv); + pdd q = m.mk_val(qv); + pdd r = m.mk_val(rv); + SASSERT_EQ(a, b * q + r); + SASSERT(b.val() * q.val() + r.val() <= m.max_value()); + SASSERT(r.val() <= (b * q + r).val()); + SASSERT(r.val() < b.val()); + return { std::move(q), std::move(r) }; + } + + expr* quot = bv.mk_bv_udiv_i(x, y); + expr* rem = bv.mk_bv_urem_i(x, y); + + ctx.internalize(quot); + ctx.internalize(rem); + auto quotv = expr2enode(quot)->get_th_var(get_id()); + auto remv = expr2enode(rem)->get_th_var(get_id()); + + pdd q = var2pdd(quotv); + pdd r = var2pdd(remv); + + // Axioms for quotient/remainder + // + // a = b*q + r + // multiplication does not overflow in b*q + // addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r + // b ≠ 0 ==> r < b + // b = 0 ==> q = -1 + // TODO: when a,b become evaluable, can we actually propagate q,r? doesn't seem like it. + // Maybe we need something like an op_constraint for better propagation. + add_polysat_clause("[axiom] quot_rem 1", { m_core.eq(b * q + r - a) }, false); + add_polysat_clause("[axiom] quot_rem 2", { ~m_core.umul_ovfl(b, q) }, false); + // r <= b*q+r + // { apply equivalence: p <= q <=> q-p <= -p-1 } + // b*q <= -r-1 + add_polysat_clause("[axiom] quot_rem 3", { m_core.ule(b * q, -r - 1) }, false); + + auto c_eq = m_core.eq(b); + if (!c_eq.is_always_true()) + add_polysat_clause("[axiom] quot_rem 4", { c_eq, ~m_core.ule(b, r) }, false); + if (!c_eq.is_always_false()) + add_polysat_clause("[axiom] quot_rem 5", { ~c_eq, m_core.eq(q + 1) }, false); + + return { std::move(q), std::move(r) }; } void solver::internalize_div_rem(app* e, bool is_div) { bv_rewriter_params p(s().params()); if (p.hi_div0()) { - internalize_div_rem_i(e, is_div); + if (bv.is_bv_udivi(e)) + internalize_udiv_i(e); + else + internalize_urem_i(e); return; } expr* arg1 = e->get_arg(0); diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index 8baf05de5..e4e022c6e 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -84,6 +84,8 @@ namespace polysat { } } } + UNREACHABLE(); + return sat::check_result::CR_GIVEUP; } void solver::asserted(literal l) { @@ -249,11 +251,11 @@ namespace polysat { return ctx.get_trail_stack(); } - void solver::add_lemma(vector const& lemma) { + void solver::add_polysat_clause(char const* name, std::initializer_list cs, bool is_redundant) { sat::literal_vector lits; - for (auto sc : lemma) + for (auto sc : cs) lits.push_back(ctx.mk_literal(constraint2expr(sc))); - s().add_clause(lits.size(), lits.data(), sat::status::th(true, get_id(), nullptr)); + s().add_clause(lits.size(), lits.data(), sat::status::th(is_redundant, get_id(), nullptr)); } void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) { @@ -271,14 +273,14 @@ namespace polysat { case ckind_t::umul_ovfl_t: { auto l = pdd2expr(sc.to_umul_ovfl().p()); auto r = pdd2expr(sc.to_umul_ovfl().q()); - return expr_ref(bv.mk_bvumul_ovfl(l, r), m); + return expr_ref(m.mk_not(bv.mk_bvumul_no_ovfl(l, r)), m); } case ckind_t::smul_fl_t: case ckind_t::op_t: NOT_IMPLEMENTED_YET(); break; } - throw default_exception("nyi"); + throw default_exception("constraint2expr nyi"); } expr_ref solver::pdd2expr(pdd const& p) { @@ -346,7 +348,7 @@ namespace polysat { continue; for (auto sib : euf::enode_class(p)) { if (bv.is_extract(sib->get_expr(), lo, hi, e) && r == expr2enode(e)->get_root()) { - throw default_exception("nyi"); + throw default_exception("get_fixed nyi"); // TODO // dependency d = dependency(p->get_th_var(get_id()), n->get_th_var(get_id()), s().scope_lvl()); // fixed_bits.push_back({ hi, lo, rational::zero(), null_dependency()}); diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h index e1a9221e9..f2c80a6e6 100644 --- a/src/sat/smt/polysat_solver.h +++ b/src/sat/smt/polysat_solver.h @@ -113,10 +113,10 @@ namespace polysat { void internalize_extract(app* n); void internalize_repeat(app* n); void internalize_bit2bool(app* n); - void internalize_udiv_i(app* n); template void internalize_le(app* n); - void internalize_div_rem_i(app* e, bool is_div); + void internalize_udiv_i(app* e); + void internalize_urem_i(app* e); void internalize_div_rem(app* e, bool is_div); void internalize_polysat(app* a); void assert_bv2int_axiom(app * n); @@ -126,6 +126,8 @@ namespace polysat { pdd var2pdd(euf::theory_var v); void internalize_set(expr* e, pdd const& p); void internalize_set(euf::theory_var v, pdd const& p); + std::pair quot_rem(expr* x, expr* y); + // callbacks from core void add_eq_literal(pvar v, rational const& val) override; @@ -137,8 +139,7 @@ namespace polysat { bool inconsistent() const override; void get_bitvector_prefixes(pvar v, pvar_vector& out) override; void get_fixed_bits(pvar v, svector& fixed_bits) override; - - void add_lemma(vector const& lemma); + void add_polysat_clause(char const* name, std::initializer_list cs, bool is_redundant); std::pair explain_deps(dependency_vector const& deps);