From 79e6d4e32dc329b4be35d413feaa299ea5da3c4a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 2 Dec 2022 20:23:46 -0800 Subject: [PATCH] tune and debug elim-unconstrained (v2 - for simplifiers infrastructure) --- src/ast/bv_decl_plugin.h | 5 ++ src/ast/converters/expr_inverter.cpp | 54 ++++++++++--- src/ast/rewriter/bv_rewriter.cpp | 89 +++++++++++----------- src/ast/rewriter/bv_rewriter.h | 4 + src/ast/simplifiers/elim_unconstrained.cpp | 42 ++++++++-- src/ast/simplifiers/elim_unconstrained.h | 2 + 6 files changed, 132 insertions(+), 64 deletions(-) diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index ee618b42c..fc7e35245 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -411,6 +411,11 @@ public: app * mk_numeral(rational const & val, sort* s) const; app * mk_numeral(rational const & val, unsigned bv_size) const; app * mk_numeral(uint64_t u, unsigned bv_size) const { return mk_numeral(rational(u, rational::ui64()), bv_size); } + app * mk_zero(sort* s) const { return mk_numeral(rational::zero(), s); } + app * mk_zero(unsigned bv_size) const { return mk_numeral(rational::zero(), bv_size); } + app * mk_one(sort* s) const { return mk_numeral(rational::one(), s); } + app * mk_one(unsigned bv_size) const { return mk_numeral(rational::one(), bv_size); } + sort * mk_sort(unsigned bv_size); unsigned get_bv_size(sort const * s) const { diff --git a/src/ast/converters/expr_inverter.cpp b/src/ast/converters/expr_inverter.cpp index 2874abd68..5553420ad 100644 --- a/src/ast/converters/expr_inverter.cpp +++ b/src/ast/converters/expr_inverter.cpp @@ -300,7 +300,7 @@ class bv_expr_inverter : public iexpr_inverter { sort* s = args[0]->get_sort(); mk_fresh_uncnstr_var_for(f, r); if (m_mc) - add_defs(num, args, r, bv.mk_numeral(rational(1), s)); + add_defs(num, args, r, bv.mk_one(s)); return true; } // c * v (c is odd) case @@ -335,7 +335,7 @@ class bv_expr_inverter : public iexpr_inverter { } mk_fresh_uncnstr_var_for(f, r); if (sh > 0) - r = bv.mk_concat(bv.mk_extract(sz - sh - 1, 0, r), bv.mk_numeral(0, sh)); + r = bv.mk_concat(bv.mk_extract(sz - sh - 1, 0, r), bv.mk_zero(sh)); if (m_mc) { rational inv_r; @@ -376,10 +376,10 @@ class bv_expr_inverter : public iexpr_inverter { else { ptr_buffer args; if (high < bv_size - 1) - args.push_back(bv.mk_numeral(rational(0), bv_size - high - 1)); + args.push_back(bv.mk_zero(bv_size - high - 1)); args.push_back(r); if (low > 0) - args.push_back(bv.mk_numeral(rational(0), low)); + args.push_back(bv.mk_zero(low)); add_def(arg, bv.mk_concat(args.size(), args.data())); } return true; @@ -391,7 +391,7 @@ class bv_expr_inverter : public iexpr_inverter { mk_fresh_uncnstr_var_for(f, r); if (m_mc) { add_def(arg1, r); - add_def(arg2, bv.mk_numeral(rational(1), s)); + add_def(arg2, bv.mk_one(s)); } return true; } @@ -419,13 +419,22 @@ class bv_expr_inverter : public iexpr_inverter { } bool process_bv_le(func_decl* f, expr* arg1, expr* arg2, bool is_signed, expr_ref& r) { + unsigned bv_sz = bv.get_bv_size(arg1); + if (uncnstr(arg1) && uncnstr(arg2)) { + mk_fresh_uncnstr_var_for(f, r); + if (m_mc) { + add_def(arg1, m.mk_ite(r, bv.mk_zero(bv_sz), bv.mk_one(bv_sz))); + add_def(arg2, bv.mk_zero(bv_sz)); + } + return true; + } if (uncnstr(arg1)) { // v <= t expr* v = arg1; expr* t = arg2; // v <= t ---> (u or t == MAX) u is fresh // add definition v = ite(u or t == MAX, t, t+1) - unsigned bv_sz = bv.get_bv_size(arg1); + rational MAX; if (is_signed) MAX = rational::power_of_two(bv_sz - 1) - rational(1); @@ -434,7 +443,7 @@ class bv_expr_inverter : public iexpr_inverter { mk_fresh_uncnstr_var_for(f, r); r = m.mk_or(r, m.mk_eq(t, bv.mk_numeral(MAX, bv_sz))); if (m_mc) - add_def(v, m.mk_ite(r, t, bv.mk_bv_add(t, bv.mk_numeral(rational(1), bv_sz)))); + add_def(v, m.mk_ite(r, t, bv.mk_bv_add(t, bv.mk_one(bv_sz)))); return true; } if (uncnstr(arg2)) { @@ -443,7 +452,6 @@ class bv_expr_inverter : public iexpr_inverter { expr* t = arg1; // v >= t ---> (u ot t == MIN) u is fresh // add definition v = ite(u or t == MIN, t, t-1) - unsigned bv_sz = bv.get_bv_size(arg1); rational MIN; if (is_signed) MIN = -rational::power_of_two(bv_sz - 1); @@ -452,7 +460,7 @@ class bv_expr_inverter : public iexpr_inverter { mk_fresh_uncnstr_var_for(f, r); r = m.mk_or(r, m.mk_eq(t, bv.mk_numeral(MIN, bv_sz))); if (m_mc) - add_def(v, m.mk_ite(r, t, bv.mk_bv_sub(t, bv.mk_numeral(rational(1), bv_sz)))); + add_def(v, m.mk_ite(r, t, bv.mk_bv_sub(t, bv.mk_one(bv_sz)))); return true; } return false; @@ -467,6 +475,18 @@ class bv_expr_inverter : public iexpr_inverter { return true; } + bool process_shift(func_decl* f, expr* arg1, expr* arg2, expr_ref& r) { + if (uncnstr(arg1) && uncnstr(arg2)) { + mk_fresh_uncnstr_var_for(f, r); + if (m_mc) { + add_def(arg1, r); + add_def(arg2, bv.mk_zero(arg2->get_sort())); + } + return true; + } + return false; + } + public: bv_expr_inverter(ast_manager& m) : iexpr_inverter(m), bv(m) {} @@ -543,10 +563,23 @@ class bv_expr_inverter : public iexpr_inverter { sort* s = args[0]->get_sort(); mk_fresh_uncnstr_var_for(f, r); if (m_mc) - add_defs(num, args, r, bv.mk_numeral(rational(0), s)); + add_defs(num, args, r, bv.mk_zero(s)); return true; } return false; + case OP_BAND: + if (num > 0 && uncnstr(num, args)) { + sort* s = args[0]->get_sort(); + mk_fresh_uncnstr_var_for(f, r); + if (m_mc) + add_defs(num, args, r, bv.mk_numeral(rational::power_of_two(bv.get_bv_size(s)) - 1, s)); + return true; + } + return false; + case OP_BSHL: + case OP_BASHR: + case OP_BLSHR: + return process_shift(f, args[0], args[1], r); default: return false; } @@ -599,6 +632,7 @@ public: } return true; } + return false; default: return false; } diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 1557c9b3c..34d2f6508 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -55,8 +55,8 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons SASSERT(f->get_family_id() == get_fid()); switch(f->get_decl_kind()) { - case OP_BIT0: SASSERT(num_args == 0); result = m_util.mk_numeral(0, 1); return BR_DONE; - case OP_BIT1: SASSERT(num_args == 0); result = m_util.mk_numeral(1, 1); return BR_DONE; + case OP_BIT0: SASSERT(num_args == 0); result = mk_zero(1); return BR_DONE; + case OP_BIT1: SASSERT(num_args == 0); result = mk_one(1); return BR_DONE; case OP_ULEQ: SASSERT(num_args == 2); return mk_ule(args[0], args[1], result); @@ -570,11 +570,11 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref if (first_non_zero == UINT_MAX) { // all bits are zero - result = m.mk_eq(a, m_util.mk_numeral(numeral(0), bv_sz)); + result = m.mk_eq(a, mk_zero(bv_sz)); return BR_REWRITE1; } else if (first_non_zero < bv_sz - 1 && m_le2extract) { - result = m.mk_and(m.mk_eq(m_mk_extract(bv_sz - 1, first_non_zero + 1, a), m_util.mk_numeral(numeral(0), bv_sz - first_non_zero - 1)), + result = m.mk_and(m.mk_eq(m_mk_extract(bv_sz - 1, first_non_zero + 1, a), mk_zero(bv_sz - first_non_zero - 1)), m_util.mk_ule(m_mk_extract(first_non_zero, 0, a), m_mk_extract(first_non_zero, 0, b))); return BR_REWRITE3; } @@ -817,7 +817,7 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) { } if (r2 >= numeral(bv_size)) { - result = mk_numeral(0, bv_size); + result = mk_zero(bv_size); return BR_DONE; } @@ -846,7 +846,7 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) { // (bvshl x k) -> (concat (extract [n-1-k:0] x) bv0:k) unsigned k = r2.get_unsigned(); expr * new_args[2] = { m_mk_extract(bv_size - k - 1, 0, arg1), - mk_numeral(0, k) }; + mk_zero(k) }; result = m_util.mk_concat(2, new_args); return BR_REWRITE2; } @@ -857,7 +857,7 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) { expr_ref cond(m_util.mk_ule(y, sum), m); result = m.mk_ite(cond, m_util.mk_bv_shl(x, sum), - mk_numeral(0, bv_size)); + mk_zero(bv_size)); return BR_REWRITE3; } @@ -877,7 +877,7 @@ br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) { } if (r2 >= numeral(bv_size)) { - result = mk_numeral(0, bv_size); + result = mk_zero(bv_size); return BR_DONE; } @@ -904,14 +904,14 @@ br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) { // (bvlshr x k) -> (concat bv0:k (extract [n-1:k] x)) SASSERT(r2.is_unsigned()); unsigned k = r2.get_unsigned(); - expr * new_args[2] = { mk_numeral(0, k), + expr * new_args[2] = { mk_zero(k), m_mk_extract(bv_size - 1, k, arg1) }; result = m_util.mk_concat(2, new_args); return BR_REWRITE2; } if (arg1 == arg2) { - result = mk_numeral(0, bv_size); + result = mk_zero(bv_size); return BR_DONE; } @@ -960,7 +960,7 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) { if (m_util.has_sign_bit(r1, bv_size)) result = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size); else - result = mk_numeral(0, bv_size); + result = mk_zero(bv_size); return BR_DONE; } @@ -1027,8 +1027,8 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e } else { // The "hardware interpretation" for (bvsdiv x 0) is (ite (bvslt x #x0000) #x0001 #xffff) - result = m.mk_ite(m.mk_app(get_fid(), OP_SLT, arg1, mk_numeral(0, bv_size)), - mk_numeral(1, bv_size), + result = m.mk_ite(m.mk_app(get_fid(), OP_SLT, arg1, mk_zero(bv_size)), + mk_one(bv_size), mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size)); return BR_REWRITE2; } @@ -1055,7 +1055,7 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e } bv_size = get_bv_size(arg2); - result = m.mk_ite(m.mk_eq(arg2, mk_numeral(0, bv_size)), + result = m.mk_ite(m.mk_eq(arg2, mk_zero(bv_size)), m_util.mk_bv_sdiv0(arg1), m_util.mk_bv_sdiv_i(arg1, arg2)); return BR_REWRITE2; @@ -1110,7 +1110,7 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e } bv_size = get_bv_size(arg2); - result = m.mk_ite(m.mk_eq(arg2, mk_numeral(0, bv_size)), + result = m.mk_ite(m.mk_eq(arg2, mk_zero(bv_size)), m_util.mk_bv_udiv0(arg1), m_util.mk_bv_udiv_i(arg1, arg2)); @@ -1137,7 +1137,7 @@ br_status bv_rewriter::mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, e } if (r2.is_one()) { - result = mk_numeral(0, bv_size); + result = mk_zero(bv_size); return BR_DONE; } @@ -1157,7 +1157,7 @@ br_status bv_rewriter::mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, e } bv_size = get_bv_size(arg2); - result = m.mk_ite(m.mk_eq(arg2, mk_numeral(0, bv_size)), + result = m.mk_ite(m.mk_eq(arg2, mk_zero(bv_size)), m.mk_app(get_fid(), OP_BSREM0, arg1), m.mk_app(get_fid(), OP_BSREM_I, arg1, arg2)); return BR_REWRITE2; @@ -1222,7 +1222,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e } if (r2.is_one()) { - result = mk_numeral(0, bv_size); + result = mk_zero(bv_size); return BR_DONE; } @@ -1236,7 +1236,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e unsigned shift; if (r2.is_power_of_two(shift)) { expr * args[2] = { - mk_numeral(0, bv_size - shift), + mk_zero(bv_size - shift), m_mk_extract(shift-1, 0, arg1) }; result = m_util.mk_concat(2, args); @@ -1263,7 +1263,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e bv_size = get_bv_size(arg1); expr * x_minus_1 = arg1; expr * minus_one = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size); - result = m.mk_ite(m.mk_eq(x, mk_numeral(0, bv_size)), + result = m.mk_ite(m.mk_eq(x, mk_zero(bv_size)), m_util.mk_bv_urem0(minus_one), x_minus_1); return BR_REWRITE2; @@ -1293,7 +1293,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e } bv_size = get_bv_size(arg2); - result = m.mk_ite(m.mk_eq(arg2, mk_numeral(0, bv_size)), + result = m.mk_ite(m.mk_eq(arg2, mk_zero(bv_size)), m_util.mk_bv_urem0(arg1), m_util.mk_bv_urem_i(arg1, arg2)); return BR_REWRITE2; @@ -1343,7 +1343,7 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e if (r2.is_one()) { // (bvsmod x 1) --> 0 - result = mk_numeral(0, bv_size); + result = mk_zero(bv_size); return BR_REWRITE2; } @@ -1357,8 +1357,8 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e unsigned nb = r2.get_num_bits(); expr_ref a1(m_util.mk_bv_smod(a, arg2), m); expr_ref a2(m_util.mk_bv_smod(b, arg2), m); - a1 = m_util.mk_concat( mk_numeral(0, bv_size - nb), m_mk_extract(nb-1,0,a1)); - a2 = m_util.mk_concat( mk_numeral(0, bv_size - nb), m_mk_extract(nb-1,0,a2)); + a1 = m_util.mk_concat( mk_zero(bv_size - nb), m_mk_extract(nb-1,0,a1)); + a2 = m_util.mk_concat( mk_zero(bv_size - nb), m_mk_extract(nb-1,0,a2)); result = m_util.mk_bv_mul(a1, a2); std::cout << result << "\n"; result = m_util.mk_bv_smod(result, arg2); @@ -1374,7 +1374,7 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e } bv_size = get_bv_size(arg2); - result = m.mk_ite(m.mk_eq(arg2, mk_numeral(0, bv_size)), + result = m.mk_ite(m.mk_eq(arg2, mk_zero(bv_size)), m.mk_app(get_fid(), OP_BSMOD0, arg1), m.mk_app(get_fid(), OP_BSMOD_I, arg1, arg2)); return BR_REWRITE2; @@ -1585,7 +1585,7 @@ br_status bv_rewriter::mk_zero_extend(unsigned n, expr * arg, expr_ref & result) return BR_DONE; } else { - expr * args[2] = { mk_numeral(0, n), arg }; + expr * args[2] = { mk_zero(n), arg }; result = m_util.mk_concat(2, args); return BR_REWRITE1; } @@ -1789,7 +1789,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re switch (new_args.size()) { case 0: - result = mk_numeral(0, sz); + result = mk_zero(sz); return BR_DONE; case 1: result = new_args[0]; @@ -1959,7 +1959,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r switch (new_args.size()) { case 0: - result = mk_numeral(0, sz); + result = mk_zero(sz); return BR_DONE; case 1: result = new_args[0]; @@ -2054,7 +2054,7 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) { // ~(x + y) --> (~x + ~y + 1) when x and y are easy to negate if (is_negatable(t, nt) && is_negatable(s, ns)) { bv_size = m_util.get_bv_size(s); - expr * nargs[3] = { m_util.mk_numeral(rational::one(), bv_size), ns.get(), nt.get() }; + expr * nargs[3] = { mk_one(bv_size), ns.get(), nt.get() }; result = m.mk_app(m_util.get_fid(), OP_BADD, 3, nargs); return BR_REWRITE1; } @@ -2146,7 +2146,7 @@ br_status bv_rewriter::mk_bv_ext_rotate_right(expr * arg1, expr * arg2, expr_ref br_status bv_rewriter::mk_bv_redor(expr * arg, expr_ref & result) { if (is_numeral(arg)) { - result = m_util.is_zero(arg) ? mk_numeral(0, 1) : mk_numeral(1, 1); + result = m_util.is_zero(arg) ? mk_zero(1) : mk_one(1); return BR_DONE; } return BR_FAILED; @@ -2156,7 +2156,7 @@ br_status bv_rewriter::mk_bv_redand(expr * arg, expr_ref & result) { numeral r; unsigned bv_size; if (is_numeral(arg, r, bv_size)) { - result = (r == rational::power_of_two(bv_size) - numeral(1)) ? mk_numeral(1, 1) : mk_numeral(0, 1); + result = (r == rational::power_of_two(bv_size) - numeral(1)) ? mk_one(1) : mk_zero(1); return BR_DONE; } return BR_FAILED; @@ -2164,19 +2164,19 @@ br_status bv_rewriter::mk_bv_redand(expr * arg, expr_ref & result) { br_status bv_rewriter::mk_bv_comp(expr * arg1, expr * arg2, expr_ref & result) { if (arg1 == arg2) { - result = mk_numeral(1,1); + result = mk_one(1); return BR_DONE; } if (is_numeral(arg1) && is_numeral(arg2)) { SASSERT(arg1 != arg2); - result = mk_numeral(0, 1); + result = mk_zero(1); return BR_DONE; } result = m.mk_ite(m.mk_eq(arg1, arg2), - mk_numeral(1, 1), - mk_numeral(0, 1)); + mk_one(1), + mk_zero(1)); return BR_REWRITE2; } @@ -2334,7 +2334,7 @@ br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_re SASSERT(shift >= 1); expr * args[2] = { m_mk_extract(bv_size-shift-1, 0, y), - mk_numeral(0, shift) + mk_zero(shift) }; result = m_util.mk_concat(2, args); return BR_REWRITE2; @@ -2399,7 +2399,7 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) { if (m_util.is_bv_or(lhs)) { if (!m_bit1) - m_bit1 = is_one ? rhs : mk_numeral(numeral(1), 1); + m_bit1 = is_one ? rhs : mk_one(1); ptr_buffer new_args; for (expr* arg : *to_app(lhs)) new_args.push_back(m.mk_eq(arg, m_bit1)); @@ -2416,7 +2416,7 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) { if (m_util.is_bv_xor(lhs)) { if (!m_bit1) - m_bit1 = is_one ? rhs : mk_numeral(numeral(1), 1); + m_bit1 = is_one ? rhs : mk_one(1); ptr_buffer new_args; for (expr* arg : *to_app(lhs)) new_args.push_back(m.mk_eq(arg, m_bit1)); @@ -2499,7 +2499,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) { unsigned rsz2 = sz2 - low2; if (rsz1 == rsz2) { new_eqs.push_back(m.mk_eq(m_mk_extract(sz1 - 1, low1, arg1), - m_mk_extract(sz2 - 1, low2, arg2))); + m_mk_extract(sz2 - 1, low2, arg2))); low1 = 0; low2 = 0; --i1; @@ -2508,14 +2508,14 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) { } else if (rsz1 < rsz2) { new_eqs.push_back(m.mk_eq(m_mk_extract(sz1 - 1, low1, arg1), - m_mk_extract(rsz1 + low2 - 1, low2, arg2))); + m_mk_extract(rsz1 + low2 - 1, low2, arg2))); low1 = 0; low2 += rsz1; --i1; } else { new_eqs.push_back(m.mk_eq(m_mk_extract(rsz2 + low1 - 1, low1, arg1), - m_mk_extract(sz2 - 1, low2, arg2))); + m_mk_extract(sz2 - 1, low2, arg2))); low1 += rsz2; low2 = 0; --i2; @@ -2572,12 +2572,9 @@ bool bv_rewriter::isolate_term(expr* lhs, expr* rhs, expr_ref& result) { } bool bv_rewriter::is_add_mul_const(expr* e) const { - if (!m_util.is_bv_add(e)) { + if (!m_util.is_bv_add(e)) return false; - } - unsigned num = to_app(e)->get_num_args(); - for (unsigned i = 0; i < num; i++) { - expr * arg = to_app(e)->get_arg(i); + for (expr * arg : *to_app(e)) { expr * c2, * x2; if (m_util.is_numeral(arg)) continue; diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index b22a11947..ca999c793 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -173,6 +173,10 @@ public: bool is_bv(expr * t) const { return m_util.is_bv(t); } expr * mk_numeral(numeral const & v, unsigned sz) { return m_util.mk_numeral(v, sz); } expr * mk_numeral(unsigned v, unsigned sz) { return m_util.mk_numeral(numeral(v), sz); } + app * mk_zero(sort* s) { return m_util.mk_zero(s); } + app * mk_one(sort* s) { return m_util.mk_one(s); } + app * mk_zero(unsigned sz) { return m_util.mk_zero(sz); } + app * mk_one(unsigned sz) { return m_util.mk_one(sz); } br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); void mk_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp index 713d7941c..7404382a3 100644 --- a/src/ast/simplifiers/elim_unconstrained.cpp +++ b/src/ast/simplifiers/elim_unconstrained.cpp @@ -96,14 +96,17 @@ void elim_unconstrained::eliminate() { m_trail.push_back(r); SASSERT(r); gc(e); + init_children(e, r); m_root.setx(r->get_id(), e->get_id(), UINT_MAX); get_node(e).m_term = r; get_node(e).m_refcount++; IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(e, m) << "\n"); SASSERT(!m_heap.contains(root(e))); - if (is_uninterp_const(r)) - m_heap.insert(root(e)); + if (is_uninterp_const(r)) + m_heap.insert(root(e)); + else + m_created_compound = true; IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(n.m_orig, m) << " " << mk_bounded_pp(t, m) << " -> " << r << " " << get_node(e).m_refcount << "\n";); @@ -177,6 +180,24 @@ void elim_unconstrained::init_terms(expr_ref_vector const& terms) { } } +void elim_unconstrained::init_children(expr* e, expr* r) { + expr_ref_vector children(m); + SASSERT(e != r); + if (is_quantifier(r)) + children.push_back(to_quantifier(r)->get_expr()); + else if (is_app(r)) + children.append(to_app(r)->get_num_args(), to_app(r)->get_args()); + else + return; + if (children.empty()) + return; + init_terms(children); + for (expr* arg : children) { + get_node(arg).m_parents.push_back(e); + inc_ref(arg); + } +} + void elim_unconstrained::gc(expr* t) { ptr_vector todo; todo.push_back(t); @@ -284,10 +305,15 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector< void elim_unconstrained::reduce() { generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained"); m_inverter.set_model_converter(mc.get()); - init_nodes(); - eliminate(); - reconstruct_terms(); - vector old_fmls; - assert_normalized(old_fmls); - update_model_trail(*mc, old_fmls); + m_created_compound = true; + for (unsigned rounds = 0; m_created_compound && rounds < 3; ++rounds) { + m_created_compound = false; + init_nodes(); + eliminate(); + reconstruct_terms(); + vector old_fmls; + assert_normalized(old_fmls); + update_model_trail(*mc, old_fmls); + } + } diff --git a/src/ast/simplifiers/elim_unconstrained.h b/src/ast/simplifiers/elim_unconstrained.h index 9da0f3fc2..1eb5d732b 100644 --- a/src/ast/simplifiers/elim_unconstrained.h +++ b/src/ast/simplifiers/elim_unconstrained.h @@ -47,6 +47,7 @@ class elim_unconstrained : public dependent_expr_simplifier { ptr_vector m_args; stats m_stats; unsigned_vector m_root; + bool m_created_compound = false; bool is_var_lt(int v1, int v2) const; node& get_node(unsigned n) { return m_nodes[n]; } @@ -58,6 +59,7 @@ class elim_unconstrained : public dependent_expr_simplifier { void inc_ref(expr* t) { ++get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.increased(root(t)); } void dec_ref(expr* t) { --get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.decreased(root(t)); } void gc(expr* t); + void init_children(expr* e, expr* r); expr* get_parent(unsigned n) const; void init_terms(expr_ref_vector const& terms); void init_nodes();