diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 6a652c2f7..a45f20d9e 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -78,91 +78,91 @@ void bv_rewriter::get_param_descrs(param_descrs & r) { poly_rewriter::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 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 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 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 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; } }