mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 10:55:50 +00:00
tune and debug elim-unconstrained (v2 - for simplifiers infrastructure)
This commit is contained in:
Nikolaj Bjorner
parent
59fa8964ca
commit
79e6d4e32d
6 changed files with 132 additions and 64 deletions
|
|
@ -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 {
|
||||
|
|
|
|||
|
|
@ -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<expr> 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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<expr> 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<expr> 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;
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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<expr> 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<dependent_expr> 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<dependent_expr> old_fmls;
|
||||
assert_normalized(old_fmls);
|
||||
update_model_trail(*mc, old_fmls);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -47,6 +47,7 @@ class elim_unconstrained : public dependent_expr_simplifier {
|
|||
ptr_vector<expr> 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();
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue