From 2f2bf749b9d3fb71f2ae49ffaafde5b6e370f96c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Dec 2023 18:15:51 -0800 Subject: [PATCH] fixes to intblast encoding and more arithmetic rewriters Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 52 ++++++++++++++++++++++------- src/ast/rewriter/arith_rewriter.h | 1 + src/sat/smt/intblast_solver.cpp | 10 +++--- 3 files changed, 46 insertions(+), 17 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 13e50da4a..635d5a3f2 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1232,19 +1232,20 @@ static rational symmod(rational const& a, rational const& b) { br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) { set_curr_sort(arg1->get_sort()); - numeral v1, v2; - bool is_int; - if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) { - result = m_util.mk_numeral(mod(v1, v2), is_int); + numeral x, y; + bool is_num_x = m_util.is_numeral(arg1, x); + bool is_num_y = m_util.is_numeral(arg2, y); + if (is_num_x && is_num_y && !y.is_zero()) { + result = m_util.mk_int(mod(x, y)); return BR_DONE; } - if (m_util.is_numeral(arg2, v2, is_int) && is_int && (v2.is_one() || v2.is_minus_one())) { + if (is_num_y && y.is_int() && (y.is_one() || y.is_minus_one())) { result = m_util.mk_numeral(numeral(0), true); return BR_DONE; } - if (arg1 == arg2 && !m_util.is_numeral(arg2)) { + if (arg1 == arg2 && !is_num_y) { expr_ref zero(m_util.mk_int(0), m); result = m.mk_ite(m.mk_eq(arg2, zero), m_util.mk_mod(zero, zero), zero); return BR_DONE; @@ -1252,29 +1253,35 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul // mod is idempotent on non-zero modulus. expr* t1, *t2; - if (m_util.is_mod(arg1, t1, t2) && t2 == arg2 && m_util.is_numeral(arg2, v2, is_int) && is_int && !v2.is_zero()) { + if (m_util.is_mod(arg1, t1, t2) && t2 == arg2 && is_num_y && y.is_int() && !y.is_zero()) { + result = arg1; + return BR_DONE; + } + + rational lo, hi; + if (is_num_y && get_range(arg1, lo, hi) && 0 <= lo && hi < y) { result = arg1; return BR_DONE; } // propagate mod inside only if there is something to reduce. - if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos() && (is_add(arg1) || is_mul(arg1))) { + if (is_num_y && y.is_int() && y.is_pos() && (is_add(arg1) || is_mul(arg1))) { TRACE("mod_bug", tout << "mk_mod:\n" << mk_ismt2_pp(arg1, m) << "\n" << mk_ismt2_pp(arg2, m) << "\n";); expr_ref_buffer args(m); bool change = false; for (expr* arg : *to_app(arg1)) { rational arg_v; - if (m_util.is_numeral(arg, arg_v) && mod(arg_v, v2) != arg_v) { + if (m_util.is_numeral(arg, arg_v) && mod(arg_v, y) != arg_v) { change = true; - args.push_back(m_util.mk_numeral(mod(arg_v, v2), true)); + args.push_back(m_util.mk_numeral(mod(arg_v, y), true)); } else if (m_util.is_mod(arg, t1, t2) && t2 == arg2) { change = true; args.push_back(t1); } - else if (m_util.is_mul(arg, t1, t2) && m_util.is_numeral(t1, arg_v) && symmod(arg_v, v2) != arg_v) { + else if (m_util.is_mul(arg, t1, t2) && m_util.is_numeral(t1, arg_v) && symmod(arg_v, y) != arg_v) { change = true; - args.push_back(m_util.mk_mul(m_util.mk_numeral(symmod(arg_v, v2), true), t2)); + args.push_back(m_util.mk_mul(m_util.mk_numeral(symmod(arg_v, y), true), t2)); } else { args.push_back(arg); @@ -1291,6 +1298,27 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul return BR_FAILED; } +bool arith_rewriter::get_range(expr* e, rational& lo, rational& hi) { + expr* x, *y; + rational r; + if (m_util.is_idiv(e, x, y) && m_util.is_numeral(y, r) && get_range(x, lo, hi) && 0 <= lo && r > 0) { + lo = div(lo, r); + hi = div(hi, r); + return true; + } + if (m_util.is_mod(e, x, y) && m_util.is_numeral(y, r) && r > 0) { + lo = 0; + hi = r - 1; + return true; + } + if (m_util.is_numeral(e, r)) { + lo = hi = r; + return true; + } + return false; +} + + br_status arith_rewriter::mk_rem_core(expr * arg1, expr * arg2, expr_ref & result) { set_curr_sort(arg1->get_sort()); numeral v1, v2; diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index 6066c9eb4..a9a30fe00 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -63,6 +63,7 @@ class arith_rewriter : public poly_rewriter { bool m_eq2ineq; unsigned m_max_degree; + bool get_range(expr* e, rational& lo, rational& hi); void get_coeffs_gcd(expr * t, numeral & g, bool & first, unsigned & num_consts); enum const_treatment { CT_FLOOR, CT_CEIL, CT_FALSE }; bool div_polynomial(expr * t, numeral const & g, const_treatment ct, expr_ref & result); diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index d0ecff794..d1b3a7205 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -37,7 +37,6 @@ namespace intblast { euf::theory_var solver::mk_var(euf::enode* n) { auto r = euf::th_euf_solver::mk_var(n); ctx.attach_th_var(n, this, r); - TRACE("bv", tout << "mk-var: v" << r << " " << ctx.bpp(n) << "\n";); return r; } @@ -98,7 +97,7 @@ namespace intblast { ensure_translated(y); m_args.reset(); m_args.push_back(a.mk_sub(translated(x), translated(y))); - set_translated(e, m.mk_eq(umod(x, 0), a.mk_int(0))); + set_translated(e, m.mk_eq(umod(x, 0), a.mk_int(0))); } m_preds.push_back(e); ctx.push(push_back_vector(m_preds)); @@ -148,7 +147,7 @@ namespace intblast { auto a = expr2literal(e); auto b = mk_literal(r); ctx.mark_relevant(b); - // verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n"; + TRACE("intblast", tout << "add-predicate-axiom: " << mk_bounded_pp(e, m) << " \n" << r << "\n"); add_equiv(a, b); } return true; @@ -606,9 +605,10 @@ namespace intblast { unsigned lo, hi; expr* old_arg; VERIFY(bv.is_extract(e, lo, hi, old_arg)); - r = arg(0); if (lo > 0) - r = a.mk_idiv(r, a.mk_int(rational::power_of_two(lo))); + r = a.mk_idiv(umod(old_arg, 0), a.mk_int(rational::power_of_two(lo))); + else + r = arg(0); break; } case OP_BV_NUM: {