From 93be3d2b2ce3bc78205a42d33594d73703e07c67 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 13 Jan 2024 10:29:50 -0800 Subject: [PATCH] arithmetic Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat/forbidden_intervals.cpp | 3 +- src/sat/smt/polysat/viable.cpp | 13 ++++-- src/sat/smt/polysat_internalize.cpp | 13 +++--- src/sat/smt/polysat_solver.cpp | 46 ++++++++++++++++----- 4 files changed, 53 insertions(+), 22 deletions(-) diff --git a/src/sat/smt/polysat/forbidden_intervals.cpp b/src/sat/smt/polysat/forbidden_intervals.cpp index 3b573548c..009630236 100644 --- a/src/sat/smt/polysat/forbidden_intervals.cpp +++ b/src/sat/smt/polysat/forbidden_intervals.cpp @@ -22,7 +22,8 @@ Author: namespace polysat { std::ostream& operator<<(std::ostream& out, fi_record const& fi) { - out << "fi_record(bw = " << fi.bit_width << ", coeff = " << fi.coeff << ", " << fi.interval << ", " << fi.src << fi.side_cond << fi.deps << ")"; + out << "fi_record(bw = " << fi.bit_width << ", coeff = " << fi.coeff << ", " << fi.interval << ", " + << fi.src << (fi.src.empty()?"": " ") << fi.side_cond << (fi.side_cond.empty()?"":" ") << fi.deps << ")"; return out; } diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index 075852fba..e2933aaaa 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -643,9 +643,15 @@ namespace polysat { // Then value is chosen, min x . coeff * x >= t. // In other words: // - // coeff * (value - 1) <= t < coeff*value + 1 - // - auto vlo = c.value(mod((e.value - 1) * p2eb, p2b), bw); + // x >= t div coeff + // => t <= coeff * x + + // (x - 1) * coeff < t <= x * coeff + + // a < x <= b <=> + // a + 1 <= x < b + 1 + + auto vlo = c.value(mod((e.value - 1) * p2eb + 1, p2b), bw); auto vhi = c.value(mod(e.value * p2eb + 1, p2b), bw); #if 0 @@ -655,6 +661,7 @@ namespace polysat { verbose_stream() << "before bw " << ebw << " " << bw << " " << *e.e << "\nafter bw " << abw << " " << aw << " " << *after.e << "\n"; if (!t.is_val()) IF_VERBOSE(0, verbose_stream() << "symbolic t : " << t << "\n"); + #endif auto sc = cs.ult(t - vlo, vhi - vlo); CTRACE("bv", sc.is_always_false(), c.display(tout)); diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index 4f9e821bf..b2be6439d 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -531,12 +531,12 @@ namespace polysat { // Axioms for quotient/remainder // - // a = b*q + r + // x = y*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. + // addition does not overflow in (y*q) + r; for now expressed as: r <= yq+r + // y ≠ 0 ==> r < y + // y = 0 ==> q = -1 + // TODO: when x,y 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_axiom("quot-rem", { eq_internalize(bv.mk_bv_add(bv.mk_bv_mul(y, quot), rem), x)}, false); @@ -545,12 +545,11 @@ namespace polysat { // { apply equivalence: p <= q <=> q-p <= -p-1 } // b*q <= -r-1 auto minus_one = bv.mk_numeral(rational::power_of_two(sz) - 1, sz); - auto one = bv.mk_numeral(1, sz); auto zero = bv.mk_numeral(0, sz); add_axiom("quot-rem", { mk_literal(bv.mk_ule(bv.mk_bv_mul(y, quot), bv.mk_bv_sub(minus_one, rem))) }, false); auto c_eq = eq_internalize(y, zero); add_axiom("quot-rem", { c_eq, ~mk_literal(bv.mk_ule(y, rem)) }, false); - add_axiom("quot-rem", { ~c_eq, eq_internalize(bv.mk_bv_add(quot, one), zero) }, false); + add_axiom("quot-rem", { ~c_eq, eq_internalize(quot, minus_one) }, false); } void solver::internalize_sign_extend(app* e) { diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index 81893c544..17c57d263 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -459,18 +459,42 @@ namespace polysat { } expr_ref solver::pdd2expr(pdd const& p) { - if (p.is_val()) { - expr* n = bv.mk_numeral(p.val(), p.power_of_2()); - return expr_ref(n, m); - } - auto v = var2enode(m_pddvar2var[p.var()]); + + auto mk_num = [&](rational const& c) { + return bv.mk_numeral(c, p.power_of_2()); + }; + + auto mk_var = [&](pvar v) { + return var2expr(m_pddvar2var[v]); + }; + + if (p.is_val()) + return expr_ref(mk_num(p.val()), m); + + expr_ref_vector args(m); + for (auto const& mon : p) { + auto c = mon.coeff; + if (mon.vars.empty()) + args.push_back(mk_num(c)); + else if (mon.coeff == 1 && mon.vars.size() == 1) + args.push_back(mk_var(mon.vars[0])); + else if (mon.vars.size() == 1) + args.push_back(bv.mk_bv_mul(mk_num(c), mk_var(mon.vars[0]))); + else { + expr_ref_vector args2(m); + for (auto v : mon.vars) + args2.push_back(mk_var(v)); + if (c == 1) + args.push_back(bv.mk_bv_mul(args2)); + else + args.push_back(bv.mk_bv_mul(mk_num(c), bv.mk_bv_mul(args2))); + } + } expr_ref r(m); - r = v->get_expr(); - if (!p.hi().is_one()) - r = bv.mk_bv_mul(r, pdd2expr(p.hi())); - if (!p.lo().is_zero()) - r = bv.mk_bv_add(r, pdd2expr(p.lo())); - ctx.get_rewriter()(r); + if (args.size() == 1) + r = args.get(0); + else + r = bv.mk_bv_add(args); return r; }