mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
whitespace
This commit is contained in:
Christoph M. Wintersteiger
parent
2a65503235
commit
21b85c27e1
|
|
@ -78,91 +78,91 @@ void bv_rewriter::get_param_descrs(param_descrs & r) {
|
|||
poly_rewriter<bv_rewriter_core>::get_param_descrs(r);
|
||||
bv_rewriter_params::collect_param_descrs(r);
|
||||
#ifndef _EXTERNAL_RELEASE
|
||||
r.insert("mkbv2num", CPK_BOOL, "(default: false) convert (mkbv [true/false]*) into a numeral");
|
||||
r.insert("mkbv2num", CPK_BOOL, "(default: false) convert (mkbv [true/false]*) into a numeral");
|
||||
#endif
|
||||
}
|
||||
|
||||
br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
|
||||
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_ULEQ:
|
||||
SASSERT(num_args == 2);
|
||||
case OP_ULEQ:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_ule(args[0], args[1], result);
|
||||
case OP_UGEQ:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_uge(args[0], args[1], result);
|
||||
case OP_ULT:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_ult(args[0], args[1], result);
|
||||
case OP_UGT:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_ult(args[1], args[0], result);
|
||||
case OP_SLEQ:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_sle(args[0], args[1], result);
|
||||
case OP_SGEQ:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_sge(args[0], args[1], result);
|
||||
case OP_SLT:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_slt(args[0], args[1], result);
|
||||
case OP_SGT:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_slt(args[1], args[0], result);
|
||||
case OP_BADD:
|
||||
SASSERT(num_args > 0);
|
||||
return mk_bv_add(num_args, args, result);
|
||||
case OP_UGEQ:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_uge(args[0], args[1], result);
|
||||
case OP_ULT:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_ult(args[0], args[1], result);
|
||||
case OP_UGT:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_ult(args[1], args[0], result);
|
||||
case OP_SLEQ:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_sle(args[0], args[1], result);
|
||||
case OP_SGEQ:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_sge(args[0], args[1], result);
|
||||
case OP_SLT:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_slt(args[0], args[1], result);
|
||||
case OP_SGT:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_slt(args[1], args[0], result);
|
||||
case OP_BADD:
|
||||
SASSERT(num_args > 0);
|
||||
return mk_bv_add(num_args, args, result);
|
||||
case OP_BMUL:
|
||||
SASSERT(num_args > 0);
|
||||
return mk_bv_mul(num_args, args, result);
|
||||
case OP_BSUB:
|
||||
SASSERT(num_args > 0);
|
||||
return mk_sub(num_args, args, result);
|
||||
case OP_BNEG:
|
||||
SASSERT(num_args == 1);
|
||||
SASSERT(num_args > 0);
|
||||
return mk_bv_mul(num_args, args, result);
|
||||
case OP_BSUB:
|
||||
SASSERT(num_args > 0);
|
||||
return mk_sub(num_args, args, result);
|
||||
case OP_BNEG:
|
||||
SASSERT(num_args == 1);
|
||||
return mk_uminus(args[0], result);
|
||||
case OP_BSHL:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_shl(args[0], args[1], result);
|
||||
case OP_BSHL:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_shl(args[0], args[1], result);
|
||||
case OP_BLSHR:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_lshr(args[0], args[1], result);
|
||||
case OP_BASHR:
|
||||
SASSERT(num_args == 2);
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_lshr(args[0], args[1], result);
|
||||
case OP_BASHR:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_ashr(args[0], args[1], result);
|
||||
case OP_BSDIV:
|
||||
SASSERT(num_args == 2);
|
||||
case OP_BSDIV:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_sdiv(args[0], args[1], result);
|
||||
case OP_BUDIV:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_udiv(args[0], args[1], result);
|
||||
case OP_BSREM:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_srem(args[0], args[1], result);
|
||||
case OP_BUREM:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_urem(args[0], args[1], result);
|
||||
case OP_BSMOD:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_smod(args[0], args[1], result);
|
||||
case OP_BSDIV_I:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_sdiv_i(args[0], args[1], result);
|
||||
case OP_BUDIV_I:
|
||||
SASSERT(num_args == 2);
|
||||
case OP_BUDIV:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_udiv(args[0], args[1], result);
|
||||
case OP_BSREM:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_srem(args[0], args[1], result);
|
||||
case OP_BUREM:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_urem(args[0], args[1], result);
|
||||
case OP_BSMOD:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_smod(args[0], args[1], result);
|
||||
case OP_BSDIV_I:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_sdiv_i(args[0], args[1], result);
|
||||
case OP_BUDIV_I:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_udiv_i(args[0], args[1], result);
|
||||
case OP_BSREM_I:
|
||||
SASSERT(num_args == 2);
|
||||
case OP_BSREM_I:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_srem_i(args[0], args[1], result);
|
||||
case OP_BUREM_I:
|
||||
SASSERT(num_args == 2);
|
||||
case OP_BUREM_I:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_urem_i(args[0], args[1], result);
|
||||
case OP_BSMOD_I:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_smod_i(args[0], args[1], result);
|
||||
case OP_BSMOD_I:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_smod_i(args[0], args[1], result);
|
||||
case OP_CONCAT:
|
||||
return mk_concat(num_args, args, result);
|
||||
case OP_EXTRACT:
|
||||
|
|
@ -193,10 +193,10 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
|
|||
case OP_BXNOR:
|
||||
return mk_bv_xnor(num_args, args, result);
|
||||
case OP_ROTATE_LEFT:
|
||||
SASSERT(num_args == 1);
|
||||
return mk_bv_rotate_left(f->get_parameter(0).get_int(), args[0], result);
|
||||
case OP_ROTATE_RIGHT:
|
||||
SASSERT(num_args == 1);
|
||||
SASSERT(num_args == 1);
|
||||
return mk_bv_rotate_left(f->get_parameter(0).get_int(), args[0], result);
|
||||
case OP_ROTATE_RIGHT:
|
||||
SASSERT(num_args == 1);
|
||||
return mk_bv_rotate_right(f->get_parameter(0).get_int(), args[0], result);
|
||||
case OP_EXT_ROTATE_LEFT:
|
||||
SASSERT(num_args == 2);
|
||||
|
|
@ -210,14 +210,14 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
|
|||
case OP_INT2BV:
|
||||
SASSERT(num_args == 1);
|
||||
return mk_int2bv(m_util.get_bv_size(f->get_range()), args[0], result);
|
||||
case OP_BREDOR:
|
||||
SASSERT(num_args == 1);
|
||||
return mk_bv_redor(args[0], result);
|
||||
case OP_BREDAND:
|
||||
SASSERT(num_args == 1);
|
||||
return mk_bv_redand(args[0], result);
|
||||
case OP_BCOMP:
|
||||
SASSERT(num_args == 2);
|
||||
case OP_BREDOR:
|
||||
SASSERT(num_args == 1);
|
||||
return mk_bv_redor(args[0], result);
|
||||
case OP_BREDAND:
|
||||
SASSERT(num_args == 1);
|
||||
return mk_bv_redand(args[0], result);
|
||||
case OP_BCOMP:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_bv_comp(args[0], args[1], result);
|
||||
case OP_MKBV:
|
||||
return mk_mkbv(num_args, args, result);
|
||||
|
|
@ -232,7 +232,7 @@ br_status bv_rewriter::mk_ule(expr * a, expr * b, expr_ref & result) {
|
|||
|
||||
br_status bv_rewriter::mk_uge(expr * a, expr * b, expr_ref & result) {
|
||||
br_status st = mk_ule(b, a, result);
|
||||
if (st != BR_FAILED)
|
||||
if (st != BR_FAILED)
|
||||
return st;
|
||||
result = m_util.mk_ule(b, a);
|
||||
return BR_DONE;
|
||||
|
|
@ -249,7 +249,7 @@ br_status bv_rewriter::mk_sle(expr * a, expr * b, expr_ref & result) {
|
|||
|
||||
br_status bv_rewriter::mk_sge(expr * a, expr * b, expr_ref & result) {
|
||||
br_status st = mk_sle(b, a, result);
|
||||
if (st != BR_FAILED)
|
||||
if (st != BR_FAILED)
|
||||
return st;
|
||||
result = m_util.mk_sle(b, a);
|
||||
return BR_DONE;
|
||||
|
|
@ -272,7 +272,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
|
|||
return BR_DONE;
|
||||
}
|
||||
|
||||
if (is_num1)
|
||||
if (is_num1)
|
||||
r1 = m_util.norm(r1, sz, is_signed);
|
||||
if (is_num2)
|
||||
r2 = m_util.norm(r2, sz, is_signed);
|
||||
|
|
@ -322,7 +322,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
|
|||
|
||||
#if 0
|
||||
if (!is_signed && m_util.is_concat(b) && to_app(b)->get_num_args() == 2 && m_util.is_zero(to_app(b)->get_arg(0))) {
|
||||
//
|
||||
//
|
||||
// a <=_u (concat 0 c) ---> a[h:l] = 0 && a[l-1:0] <=_u c
|
||||
//
|
||||
expr * b_1 = to_app(b)->get_arg(0);
|
||||
|
|
@ -337,9 +337,9 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
|
|||
if (!is_signed) {
|
||||
// Extended version of the rule above using is_zero_bit.
|
||||
// It also catches examples atoms such as:
|
||||
//
|
||||
//
|
||||
// a <=_u #x000f
|
||||
//
|
||||
//
|
||||
unsigned bv_sz = m_util.get_bv_size(b);
|
||||
unsigned i = bv_sz;
|
||||
unsigned first_non_zero = UINT_MAX;
|
||||
|
|
@ -350,7 +350,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
|
|||
break;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
if (first_non_zero == UINT_MAX) {
|
||||
// all bits are zero
|
||||
result = m().mk_eq(a, m_util.mk_numeral(numeral(0), bv_sz));
|
||||
|
|
@ -361,7 +361,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
|
|||
m_util.mk_ule(m_mk_extract(first_non_zero, 0, a), m_mk_extract(first_non_zero, 0, b)));
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
#endif
|
||||
|
||||
|
|
@ -385,7 +385,7 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_
|
|||
result = arg;
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
numeral v;
|
||||
if (is_numeral(arg, v, sz)) {
|
||||
sz = high - low + 1;
|
||||
|
|
@ -420,7 +420,7 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_
|
|||
if (idx > high)
|
||||
continue;
|
||||
// found first argument
|
||||
if (idx <= low) {
|
||||
if (idx <= low) {
|
||||
// result is a fragment of this argument
|
||||
if (low == idx && high - idx == curr_sz - 1) {
|
||||
result = curr;
|
||||
|
|
@ -486,13 +486,13 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_
|
|||
m_mk_extract(high, low, to_app(arg)->get_arg(2)));
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
numeral r1, r2;
|
||||
unsigned bv_size = get_bv_size(arg1);
|
||||
unsigned bv_size = get_bv_size(arg1);
|
||||
unsigned sz;
|
||||
|
||||
if (is_numeral(arg2, r2, sz)) {
|
||||
|
|
@ -501,9 +501,9 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) {
|
|||
result = arg1;
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
if (r2 >= numeral(bv_size)) {
|
||||
result = mk_numeral(0, bv_size);
|
||||
result = mk_numeral(0, bv_size);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
|
@ -511,7 +511,7 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) {
|
|||
if (bv_size <= 64) {
|
||||
SASSERT(r1.is_uint64() && r2.is_uint64());
|
||||
SASSERT(r2.get_uint64() < bv_size);
|
||||
|
||||
|
||||
uint64 r = shift_left(r1.get_uint64(), r2.get_uint64());
|
||||
numeral rn(r, numeral::ui64());
|
||||
rn = m_util.norm(rn, bv_size);
|
||||
|
|
@ -519,7 +519,7 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) {
|
|||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
|
||||
SASSERT(r2 < numeral(bv_size));
|
||||
SASSERT(r2.is_unsigned());
|
||||
r1 = m_util.norm(r1 * rational::power_of_two(r2.get_unsigned()), bv_size);
|
||||
|
|
@ -539,10 +539,10 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) {
|
|||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
|
||||
br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
numeral r1, r2;
|
||||
unsigned bv_size = get_bv_size(arg1);
|
||||
unsigned bv_size = get_bv_size(arg1);
|
||||
unsigned sz;
|
||||
|
||||
if (is_numeral(arg2, r2, sz)) {
|
||||
|
|
@ -551,15 +551,15 @@ br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) {
|
|||
result = arg1;
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
if (r2 >= numeral(bv_size)) {
|
||||
result = mk_numeral(0, bv_size);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
if (is_numeral(arg1, r1, sz)) {
|
||||
if (bv_size <= 64) {
|
||||
SASSERT(r1.is_uint64());
|
||||
if (bv_size <= 64) {
|
||||
SASSERT(r1.is_uint64());
|
||||
SASSERT(r2.is_uint64());
|
||||
uint64 r = shift_right(r1.get_uint64(), r2.get_uint64());
|
||||
numeral rn(r, numeral::ui64());
|
||||
|
|
@ -574,7 +574,7 @@ br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) {
|
|||
result = mk_numeral(r1, bv_size);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
SASSERT(r2.is_pos());
|
||||
SASSERT(r2 < numeral(bv_size));
|
||||
// (bvlshr x k) -> (concat bv0:k (extract [n-1:k] x))
|
||||
|
|
@ -652,13 +652,13 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) {
|
|||
result = mk_numeral(r1, bv_size);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
// (bvashr (bvashr x r1) r2) --> (bvashr x r1+r2)
|
||||
if (is_num2 && m_util.is_bv_ashr(arg1) && is_numeral(to_app(arg1)->get_arg(1), r1, bv_size)) {
|
||||
r1 += r2;
|
||||
if (r1 > numeral(bv_size))
|
||||
r1 = numeral(bv_size);
|
||||
result = m().mk_app(get_fid(), OP_BASHR,
|
||||
result = m().mk_app(get_fid(), OP_BASHR,
|
||||
to_app(arg1)->get_arg(0),
|
||||
mk_numeral(r1, bv_size));
|
||||
return BR_REWRITE1; // not really needed at this time.
|
||||
|
|
@ -709,13 +709,13 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e
|
|||
result = arg1;
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
if (!r2.is_zero() && is_numeral(arg1, r1, bv_size)) {
|
||||
r1 = m_util.norm(r1, bv_size, true);
|
||||
result = mk_numeral(machine_div(r1, r2), bv_size);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
result = m().mk_app(get_fid(), OP_BSDIV_I, arg1, arg2);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
|
@ -735,9 +735,9 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e
|
|||
br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result) {
|
||||
numeral r1, r2;
|
||||
unsigned bv_size;
|
||||
|
||||
|
||||
TRACE("bv_udiv", tout << "hi_div0: " << hi_div0 << "\n";);
|
||||
|
||||
|
||||
TRACE("udiv2mul", tout << mk_ismt2_pp(arg2, m()) << " udiv2mul: " << m_udiv2mul << "\n";);
|
||||
|
||||
if (is_numeral(arg2, r2, bv_size)) {
|
||||
|
|
@ -751,7 +751,7 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e
|
|||
// The "hardware interpretation" for (bvudiv x 0) is #xffff
|
||||
result = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size);
|
||||
return BR_DONE;
|
||||
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -765,7 +765,7 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e
|
|||
result = mk_numeral(machine_div(r1, r2), bv_size);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
unsigned shift;
|
||||
if (r2.is_power_of_two(shift)) {
|
||||
result = m().mk_app(get_fid(), OP_BLSHR, arg1, mk_numeral(shift, bv_size));
|
||||
|
|
@ -821,13 +821,13 @@ br_status bv_rewriter::mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, e
|
|||
result = mk_numeral(0, bv_size);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
if (!r2.is_zero() && is_numeral(arg1, r1, bv_size)) {
|
||||
r1 = m_util.norm(r1, bv_size, true);
|
||||
result = mk_numeral(r1 % r2, bv_size);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
result = m().mk_app(get_fid(), OP_BSREM_I, arg1, arg2);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
|
@ -890,7 +890,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e
|
|||
result = mk_numeral(0, bv_size);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
if (!r2.is_zero() && is_num1) {
|
||||
r1 = m_util.norm(r1, bv_size);
|
||||
r1 %= r2;
|
||||
|
|
@ -907,7 +907,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e
|
|||
result = m_util.mk_concat(2, args);
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
||||
|
||||
result = m().mk_app(get_fid(), OP_BUREM_I, arg1, arg2);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
|
@ -921,7 +921,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e
|
|||
zero);
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
||||
|
||||
// urem(x - 1, x) ==> ite(x = 0, urem0(x-1), x - 1) ==> ite(x = 0, urem0(-1), x - 1)
|
||||
expr * x;
|
||||
if (is_x_minus_one(arg1, x) && x == arg2) {
|
||||
|
|
@ -942,7 +942,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e
|
|||
result = zero;
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
// urem(x - 1, x) --> x - 1
|
||||
expr * x;
|
||||
if (is_x_minus_one(arg1, x) && x == arg2) {
|
||||
|
|
@ -986,7 +986,7 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e
|
|||
result = arg1;
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
if (is_num1) {
|
||||
numeral abs_r1 = m_util.norm(abs(r1), bv_size);
|
||||
numeral abs_r2 = m_util.norm(abs(r2), bv_size);
|
||||
|
|
@ -1012,7 +1012,7 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e
|
|||
return BR_REWRITE2;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
if (hi_div0) {
|
||||
result = m().mk_app(get_fid(), OP_BSMOD_I, arg1, arg2);
|
||||
return BR_DONE;
|
||||
|
|
@ -1028,13 +1028,13 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e
|
|||
br_status bv_rewriter::mk_int2bv(unsigned bv_size, expr * arg, expr_ref & result) {
|
||||
numeral val;
|
||||
bool is_int;
|
||||
|
||||
|
||||
if (m_autil.is_numeral(arg, val, is_int)) {
|
||||
val = m_util.norm(val, bv_size);
|
||||
result = mk_numeral(val, bv_size);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
// (int2bv (bv2int x)) --> x
|
||||
if (m_util.is_bv2int(arg) && bv_size == get_bv_size(to_app(arg)->get_arg(0))) {
|
||||
result = to_app(arg)->get_arg(0);
|
||||
|
|
@ -1051,7 +1051,7 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) {
|
|||
result = m_autil.mk_numeral(v, true);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
// TODO: add other simplifications
|
||||
|
||||
return BR_FAILED;
|
||||
|
|
@ -1068,7 +1068,7 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
|
|||
for (unsigned i = 0; i < num_args; i++) {
|
||||
expr * arg = args[i];
|
||||
expr * prev = 0;
|
||||
if (i > 0)
|
||||
if (i > 0)
|
||||
prev = new_args.back();
|
||||
if (is_numeral(arg, v1, sz1) && prev != 0 && is_numeral(prev, v2, sz2)) {
|
||||
v2 *= rational::power_of_two(sz1);
|
||||
|
|
@ -1084,7 +1084,7 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
|
|||
}
|
||||
expanded = true;
|
||||
}
|
||||
else if (m_util.is_extract(arg) &&
|
||||
else if (m_util.is_extract(arg) &&
|
||||
prev != 0 &&
|
||||
m_util.is_extract(prev) &&
|
||||
to_app(arg)->get_arg(0) == to_app(prev)->get_arg(0) &&
|
||||
|
|
@ -1101,7 +1101,7 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
|
|||
new_args.push_back(arg);
|
||||
}
|
||||
}
|
||||
if (!fused_numeral && !expanded && !fused_extract)
|
||||
if (!fused_numeral && !expanded && !fused_extract)
|
||||
return BR_FAILED;
|
||||
SASSERT(!new_args.empty());
|
||||
if (new_args.size() == 1) {
|
||||
|
|
@ -1144,18 +1144,18 @@ br_status bv_rewriter::mk_sign_extend(unsigned n, expr * arg, expr_ref & result)
|
|||
result = mk_numeral(r, result_bv_size);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
if (m_elim_sign_ext) {
|
||||
unsigned sz = get_bv_size(arg);
|
||||
expr * sign = m_mk_extract(sz-1, sz-1, arg);
|
||||
ptr_buffer<expr> args;
|
||||
for (unsigned i = 0; i < n; i++)
|
||||
for (unsigned i = 0; i < n; i++)
|
||||
args.push_back(sign);
|
||||
args.push_back(arg);
|
||||
result = m_util.mk_concat(args.size(), args.c_ptr());
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
|
|
@ -1185,7 +1185,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
|
|||
expr * arg = args[i];
|
||||
if (m_util.is_bv_or(arg)) {
|
||||
unsigned num2 = to_app(arg)->get_num_args();
|
||||
for (unsigned j = 0; j < num2; j++)
|
||||
for (unsigned j = 0; j < num2; j++)
|
||||
flat_args.push_back(to_app(arg)->get_arg(j));
|
||||
}
|
||||
else {
|
||||
|
|
@ -1244,12 +1244,12 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
|
|||
result = mk_numeral(v1, sz);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
// Simplifications of the form:
|
||||
// (bvor (concat x #x00) (concat #x00 y)) --> (concat x y)
|
||||
if (new_args.size() == 2 &&
|
||||
num_coeffs == 0 &&
|
||||
m_util.is_concat(new_args[0]) &&
|
||||
if (new_args.size() == 2 &&
|
||||
num_coeffs == 0 &&
|
||||
m_util.is_concat(new_args[0]) &&
|
||||
m_util.is_concat(new_args[1])) {
|
||||
app * concat1 = to_app(new_args[0]);
|
||||
app * concat2 = to_app(new_args[1]);
|
||||
|
|
@ -1311,8 +1311,8 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
|
|||
}
|
||||
std::reverse(exs.begin(), exs.end());
|
||||
result = m_util.mk_concat(exs.size(), exs.c_ptr());
|
||||
TRACE("mask_bug",
|
||||
tout << "(assert (distinct (bvor (_ bv" << old_v1 << " " << sz << ")\n" << mk_ismt2_pp(t, m()) << ")\n";
|
||||
TRACE("mask_bug",
|
||||
tout << "(assert (distinct (bvor (_ bv" << old_v1 << " " << sz << ")\n" << mk_ismt2_pp(t, m()) << ")\n";
|
||||
tout << mk_ismt2_pp(result, m()) << "))\n";);
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
|
@ -1324,7 +1324,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
|
|||
if (!v1.is_zero()) {
|
||||
new_args.push_back(mk_numeral(v1, sz));
|
||||
}
|
||||
|
||||
|
||||
switch (new_args.size()) {
|
||||
case 0:
|
||||
result = mk_numeral(0, sz);
|
||||
|
|
@ -1354,7 +1354,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
|
|||
expr * arg = args[i];
|
||||
if (m_util.is_bv_xor(arg)) {
|
||||
unsigned num2 = to_app(arg)->get_num_args();
|
||||
for (unsigned j = 0; j < num2; j++)
|
||||
for (unsigned j = 0; j < num2; j++)
|
||||
flat_args.push_back(to_app(arg)->get_arg(j));
|
||||
}
|
||||
else {
|
||||
|
|
@ -1367,7 +1367,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
|
|||
args = flat_args.c_ptr();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
expr_fast_mark1 pos_args;
|
||||
expr_fast_mark2 neg_args;
|
||||
bool merged = false;
|
||||
|
|
@ -1380,7 +1380,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
|
|||
num_coeffs++;
|
||||
continue;
|
||||
}
|
||||
|
||||
|
||||
if (m_util.is_bv_not(arg)) {
|
||||
expr * atom = to_app(arg)->get_arg(0);
|
||||
if (neg_args.is_marked(atom)) {
|
||||
|
|
@ -1411,14 +1411,14 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// XOR is a mask
|
||||
// All arguments but one is a numeral.
|
||||
//
|
||||
//
|
||||
// Apply a transformation of the form:
|
||||
//
|
||||
// (bvxor a 0011) --> (concat ((_ extract 3 2) a) ((_ extract 1 0) (bvnot a)))
|
||||
//
|
||||
//
|
||||
if (!v1.is_zero() && num_coeffs == num - 1) {
|
||||
// find argument that is not a numeral
|
||||
expr * t = 0;
|
||||
|
|
@ -1453,12 +1453,12 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
|
|||
}
|
||||
}
|
||||
std::reverse(exs.c_ptr(), exs.c_ptr() + exs.size());
|
||||
if (exs.size() == 1)
|
||||
if (exs.size() == 1)
|
||||
result = exs[0];
|
||||
else
|
||||
result = m_util.mk_concat(exs.size(), exs.c_ptr());
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
}
|
||||
|
||||
if (!merged && !flattened && (num_coeffs == 0 || (num_coeffs == 1 && !v1.is_zero() && v1 != (rational::power_of_two(sz) - numeral(1)))) &&
|
||||
(!m_bv_sort_ac || is_sorted(num, args)))
|
||||
|
|
@ -1487,7 +1487,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
|
|||
pos_args.mark(arg, false);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
switch (new_args.size()) {
|
||||
case 0:
|
||||
result = mk_numeral(0, sz);
|
||||
|
|
@ -1653,7 +1653,7 @@ br_status bv_rewriter::mk_bv_comp(expr * arg1, expr * arg2, expr_ref & result) {
|
|||
|
||||
br_status bv_rewriter::mk_bv_add(unsigned num_args, expr * const * args, expr_ref & result) {
|
||||
br_status st = mk_add_core(num_args, args, result);
|
||||
if (st != BR_FAILED && st != BR_DONE)
|
||||
if (st != BR_FAILED && st != BR_DONE)
|
||||
return st;
|
||||
#if 0
|
||||
expr * x;
|
||||
|
|
@ -1673,14 +1673,14 @@ br_status bv_rewriter::mk_bv_add(unsigned num_args, expr * const * args, expr_re
|
|||
return st;
|
||||
if (!m_util.is_concat(y) && !is_numeral(y))
|
||||
return st;
|
||||
|
||||
|
||||
unsigned sz = get_bv_size(x);
|
||||
|
||||
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
if (!is_zero_bit(x,i) && !is_zero_bit(y,i))
|
||||
return st;
|
||||
}
|
||||
|
||||
|
||||
result = m().mk_app(get_fid(), OP_BOR, x, y);
|
||||
return BR_REWRITE1;
|
||||
#else
|
||||
|
|
@ -1747,7 +1747,7 @@ bool bv_rewriter::is_zero_bit(expr * x, unsigned idx) {
|
|||
|
||||
br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_ref & result) {
|
||||
br_status st = mk_mul_core(num_args, args, result);
|
||||
if (st != BR_FAILED && st != BR_DONE)
|
||||
if (st != BR_FAILED && st != BR_DONE)
|
||||
return st;
|
||||
expr * x;
|
||||
expr * y;
|
||||
|
|
@ -1761,7 +1761,7 @@ br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_re
|
|||
else {
|
||||
return st;
|
||||
}
|
||||
|
||||
|
||||
if (m_mul2concat) {
|
||||
numeral v;
|
||||
unsigned bv_size;
|
||||
|
|
@ -1810,12 +1810,12 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
result = m().mk_eq(to_app(lhs)->get_arg(0), mk_numeral(numeral(1) - v, 1));
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
|
||||
|
||||
bool is_one = v.is_one();
|
||||
|
||||
expr_ref bit1(m());
|
||||
bit1 = is_one ? rhs : mk_numeral(numeral(1), 1);
|
||||
|
||||
|
||||
if (m_util.is_bv_or(lhs)) {
|
||||
ptr_buffer<expr> new_args;
|
||||
unsigned num = to_app(lhs)->get_num_args();
|
||||
|
|
@ -1831,8 +1831,8 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
return BR_REWRITE3;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
if (m_util.is_bv_xor(lhs)) {
|
||||
ptr_buffer<expr> new_args;
|
||||
unsigned num = to_app(lhs)->get_num_args();
|
||||
|
|
@ -1849,7 +1849,7 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
return BR_REWRITE3;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
|
@ -1861,14 +1861,14 @@ br_status bv_rewriter::mk_blast_eq_value(expr * lhs, expr * rhs, expr_ref & resu
|
|||
TRACE("blast_eq_value", tout << "sz: " << sz << "\n" << mk_ismt2_pp(lhs, m()) << "\n";);
|
||||
if (is_numeral(lhs))
|
||||
std::swap(lhs, rhs);
|
||||
|
||||
|
||||
numeral v;
|
||||
|
||||
if (!is_numeral(rhs, v, sz))
|
||||
return BR_FAILED;
|
||||
if (!m_util.is_bv_or(lhs) && !m_util.is_bv_xor(lhs) && !m_util.is_bv_not(lhs))
|
||||
return BR_FAILED;
|
||||
|
||||
|
||||
numeral two(2);
|
||||
ptr_buffer<expr> new_args;
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
|
|
@ -1888,7 +1888,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
|
||||
if (m_util.is_concat(lhs)) {
|
||||
num1 = to_app(lhs)->get_num_args();
|
||||
args1 = to_app(lhs)->get_args();
|
||||
args1 = to_app(lhs)->get_args();
|
||||
}
|
||||
else {
|
||||
num1 = 1;
|
||||
|
|
@ -1897,7 +1897,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
|
||||
if (m_util.is_concat(rhs)) {
|
||||
num2 = to_app(rhs)->get_num_args();
|
||||
args2 = to_app(rhs)->get_args();
|
||||
args2 = to_app(rhs)->get_args();
|
||||
}
|
||||
else {
|
||||
num2 = 1;
|
||||
|
|
@ -1930,7 +1930,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
new_eqs.push_back(m().mk_eq(m_mk_extract(sz1 - 1, low1, arg1),
|
||||
m_mk_extract(rsz1 + low2 - 1, low2, arg2)));
|
||||
low1 = 0;
|
||||
low2 += rsz1;
|
||||
low2 += rsz1;
|
||||
--i1;
|
||||
}
|
||||
else {
|
||||
|
|
@ -1948,8 +1948,8 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
}
|
||||
|
||||
bool bv_rewriter::is_concat_split_target(expr * t) const {
|
||||
return
|
||||
m_split_concat_eq ||
|
||||
return
|
||||
m_split_concat_eq ||
|
||||
m_util.is_concat(t) ||
|
||||
m_util.is_numeral(t) ||
|
||||
m_util.is_bv_or(t);
|
||||
|
|
@ -1964,7 +1964,7 @@ void bv_rewriter::mk_t1_add_t2_eq_c(expr * t1, expr * t2, expr * c, expr_ref & r
|
|||
SASSERT(is_numeral(c));
|
||||
if (is_minus_one_times_t(t1))
|
||||
result = m().mk_eq(t2, m_util.mk_bv_sub(c, t1));
|
||||
else
|
||||
else
|
||||
result = m().mk_eq(t1, m_util.mk_bv_sub(c, t2));
|
||||
}
|
||||
|
||||
|
|
@ -2024,14 +2024,14 @@ bool bv_rewriter::has_numeral(app* a) const {
|
|||
}
|
||||
|
||||
br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
|
||||
|
||||
|
||||
expr * c, * x;
|
||||
numeral c_val, c_inv_val;
|
||||
unsigned sz;
|
||||
if (m_util.is_bv_mul(lhs, c, x) &&
|
||||
m_util.is_numeral(c, c_val, sz) &&
|
||||
if (m_util.is_bv_mul(lhs, c, x) &&
|
||||
m_util.is_numeral(c, c_val, sz) &&
|
||||
m_util.mult_inverse(c_val, sz, c_inv_val)) {
|
||||
|
||||
|
||||
SASSERT(m_util.norm(c_val * c_inv_val, sz).is_one());
|
||||
|
||||
numeral rhs_val;
|
||||
|
|
@ -2048,7 +2048,7 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
if (m_util.is_bv_mul(rhs, c2, x2) && m_util.is_numeral(c2, c2_val, sz)) {
|
||||
// x = c_inv * c2 * x2
|
||||
numeral new_c2 = m_util.norm(c_inv_val * c2_val, sz);
|
||||
if (new_c2.is_one())
|
||||
if (new_c2.is_one())
|
||||
result = m().mk_eq(x, x2);
|
||||
else
|
||||
result = m().mk_eq(x, m_util.mk_bv_mul(m_util.mk_numeral(c_inv_val * c2_val, sz), x2));
|
||||
|
|
@ -2077,7 +2077,7 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
}
|
||||
}
|
||||
if (found) {
|
||||
result = m().mk_eq(m_util.mk_numeral(c2_inv_val*c_val, sz),
|
||||
result = m().mk_eq(m_util.mk_numeral(c2_inv_val*c_val, sz),
|
||||
m_util.mk_bv_mul(m_util.mk_numeral(c2_inv_val, sz), rhs));
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
|
|
@ -2095,7 +2095,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
bool swapped = false;
|
||||
if (is_numeral(lhs)) {
|
||||
swapped = true;
|
||||
|
|
@ -2120,7 +2120,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
TRACE("mk_mul_eq", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result,m()) << "\n";);
|
||||
return st;
|
||||
}
|
||||
|
||||
|
||||
if (m_blast_eq_value) {
|
||||
st = mk_blast_eq_value(lhs, rhs, result);
|
||||
if (st != BR_FAILED)
|
||||
|
|
@ -2142,10 +2142,10 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
new_lhs = lhs;
|
||||
new_rhs = rhs;
|
||||
}
|
||||
|
||||
|
||||
lhs = new_lhs;
|
||||
rhs = new_rhs;
|
||||
// Try to rewrite t1 + t2 = c --> t1 = c - t2
|
||||
// Try to rewrite t1 + t2 = c --> t1 = c - t2
|
||||
// Reason: it is much cheaper to bit-blast.
|
||||
if (isolate_term(lhs, rhs, result)) {
|
||||
return BR_REWRITE2;
|
||||
|
|
@ -2155,7 +2155,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
}
|
||||
|
||||
if (st != BR_FAILED) {
|
||||
result = m().mk_eq(lhs, rhs);
|
||||
result = m().mk_eq(lhs, rhs);
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue