mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
commit
481b177d47
|
@ -1383,7 +1383,7 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) {
|
|||
--i;
|
||||
tmp = args[i].get();
|
||||
tmp = m_autil.mk_mul(m_autil.mk_numeral(power(numeral(2), sz), true), tmp);
|
||||
args[i] = tmp;
|
||||
args[i] = std::move(tmp);
|
||||
sz += get_bv_size(to_app(arg)->get_arg(i));
|
||||
}
|
||||
result = m_autil.mk_add(args.size(), args.c_ptr());
|
||||
|
@ -2400,8 +2400,8 @@ bool bv_rewriter::isolate_term(expr* lhs, expr* rhs, expr_ref& result) {
|
|||
return false;
|
||||
}
|
||||
unsigned sz = to_app(rhs)->get_num_args();
|
||||
expr_ref t1(m()), t2(m());
|
||||
t1 = to_app(rhs)->get_arg(0);
|
||||
expr * t1 = to_app(rhs)->get_arg(0);
|
||||
expr_ref t2(m());
|
||||
if (sz > 2) {
|
||||
t2 = m().mk_app(get_fid(), OP_BADD, sz-1, to_app(rhs)->get_args()+1);
|
||||
}
|
||||
|
@ -2597,14 +2597,10 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
result = m().mk_bool_val(new_lhs == new_rhs);
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
else {
|
||||
new_lhs = lhs;
|
||||
new_rhs = rhs;
|
||||
lhs = new_lhs;
|
||||
rhs = new_rhs;
|
||||
}
|
||||
|
||||
lhs = new_lhs;
|
||||
rhs = new_rhs;
|
||||
// Try to rewrite t1 + t2 = c --> t1 = c - t2
|
||||
// Reason: it is much cheaper to bit-blast.
|
||||
if (isolate_term(lhs, rhs, result)) {
|
||||
|
|
|
@ -35,6 +35,7 @@ Notes:
|
|||
#include "ast/ast_util.h"
|
||||
#include "ast/well_sorted.h"
|
||||
|
||||
namespace {
|
||||
struct th_rewriter_cfg : public default_rewriter_cfg {
|
||||
bool_rewriter m_b_rw;
|
||||
arith_rewriter m_a_rw;
|
||||
|
@ -337,16 +338,16 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
|
|||
family_id fid = t->get_family_id();
|
||||
if (fid == m_a_rw.get_fid()) {
|
||||
switch (t->get_decl_kind()) {
|
||||
case OP_ADD: n = m_a_util.mk_numeral(rational(0), m().get_sort(t)); return true;
|
||||
case OP_MUL: n = m_a_util.mk_numeral(rational(1), m().get_sort(t)); return true;
|
||||
case OP_ADD: n = m_a_util.mk_numeral(rational::zero(), m().get_sort(t)); return true;
|
||||
case OP_MUL: n = m_a_util.mk_numeral(rational::one(), m().get_sort(t)); return true;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
}
|
||||
if (fid == m_bv_rw.get_fid()) {
|
||||
switch (t->get_decl_kind()) {
|
||||
case OP_BADD: n = m_bv_util.mk_numeral(rational(0), m().get_sort(t)); return true;
|
||||
case OP_BMUL: n = m_bv_util.mk_numeral(rational(1), m().get_sort(t)); return true;
|
||||
case OP_BADD: n = m_bv_util.mk_numeral(rational::zero(), m().get_sort(t)); return true;
|
||||
case OP_BMUL: n = m_bv_util.mk_numeral(rational::one(), m().get_sort(t)); return true;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
|
@ -468,9 +469,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
|
|||
// terms matched...
|
||||
bool is_int = m_a_util.is_int(t1);
|
||||
if (!new_t1)
|
||||
new_t1 = m_a_util.mk_numeral(rational(0), is_int);
|
||||
new_t1 = m_a_util.mk_numeral(rational::zero(), is_int);
|
||||
if (!new_t2)
|
||||
new_t2 = m_a_util.mk_numeral(rational(0), is_int);
|
||||
new_t2 = m_a_util.mk_numeral(rational::zero(), is_int);
|
||||
// mk common part
|
||||
ptr_buffer<expr> args;
|
||||
for (unsigned i = 0; i < num1; i++) {
|
||||
|
@ -709,6 +710,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
|
|||
|
||||
|
||||
};
|
||||
}
|
||||
|
||||
template class rewriter_tpl<th_rewriter_cfg>;
|
||||
|
||||
|
@ -764,8 +766,8 @@ unsigned th_rewriter::get_num_steps() const {
|
|||
|
||||
void th_rewriter::cleanup() {
|
||||
ast_manager & m = m_imp->m();
|
||||
dealloc(m_imp);
|
||||
m_imp = alloc(imp, m, m_params);
|
||||
m_imp->~imp();
|
||||
new (m_imp) imp(m, m_params);
|
||||
}
|
||||
|
||||
void th_rewriter::reset() {
|
||||
|
|
Loading…
Reference in a new issue