mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
fix #5102
This commit is contained in:
parent
1cb0dbae51
commit
18143d8932
|
@ -2193,6 +2193,9 @@ public:
|
|||
app * mk_xor(expr * lhs, expr * rhs) { return mk_app(m_basic_family_id, OP_XOR, lhs, rhs); }
|
||||
app * mk_ite(expr * c, expr * t, expr * e) { return mk_app(m_basic_family_id, OP_ITE, c, t, e); }
|
||||
app * mk_xor(unsigned num_args, expr * const * args) { return mk_app(m_basic_family_id, OP_XOR, num_args, args); }
|
||||
app * mk_xor(ptr_buffer<expr> const& args) { return mk_xor(args.size(), args.c_ptr()); }
|
||||
app * mk_xor(ptr_vector<expr> const& args) { return mk_xor(args.size(), args.c_ptr()); }
|
||||
app * mk_xor(ref_buffer<expr, ast_manager> const& args) { return mk_xor(args.size(), args.c_ptr()); }
|
||||
app * mk_or(unsigned num_args, expr * const * args) { return mk_app(m_basic_family_id, OP_OR, num_args, args); }
|
||||
app * mk_and(unsigned num_args, expr * const * args) { return mk_app(m_basic_family_id, OP_AND, num_args, args); }
|
||||
app * mk_or(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_OR, arg1, arg2); }
|
||||
|
|
|
@ -352,6 +352,8 @@ public:
|
|||
bool is_sign_ext(expr const * e) const { return is_app_of(e, get_fid(), OP_SIGN_EXT); }
|
||||
bool is_bv_umul_no_ovfl(expr const* e) const { return is_app_of(e, get_fid(), OP_BUMUL_NO_OVFL); }
|
||||
|
||||
MATCH_UNARY(is_bv_not);
|
||||
|
||||
MATCH_BINARY(is_bv_add);
|
||||
MATCH_BINARY(is_bv_mul);
|
||||
MATCH_BINARY(is_bv_sle);
|
||||
|
|
|
@ -2293,16 +2293,15 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
return BR_DONE;
|
||||
}
|
||||
|
||||
if (m().is_ite(lhs)) {
|
||||
result = m().mk_ite(to_app(lhs)->get_arg(0),
|
||||
m().mk_eq(to_app(lhs)->get_arg(1), rhs),
|
||||
m().mk_eq(to_app(lhs)->get_arg(2), rhs));
|
||||
expr* a = nullptr, *b = nullptr, *c = nullptr;
|
||||
if (m().is_ite(lhs, a, b, c)) {
|
||||
result = m().mk_ite(a, m().mk_eq(b, rhs), m().mk_eq(c, rhs));
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
||||
if (m_util.is_bv_not(lhs)) {
|
||||
|
||||
if (m_util.is_bv_not(lhs, a)) {
|
||||
SASSERT(v.is_one() || v.is_zero());
|
||||
result = m().mk_eq(to_app(lhs)->get_arg(0), mk_numeral(numeral(1) - v, 1));
|
||||
result = m().mk_eq(a, mk_numeral(numeral(1) - v, 1));
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
|
||||
|
@ -2313,11 +2312,9 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
|
||||
if (m_util.is_bv_or(lhs)) {
|
||||
ptr_buffer<expr> new_args;
|
||||
unsigned num = to_app(lhs)->get_num_args();
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
new_args.push_back(m().mk_eq(to_app(lhs)->get_arg(i), bit1));
|
||||
}
|
||||
result = m().mk_or(new_args.size(), new_args.c_ptr());
|
||||
for (expr* arg : *to_app(lhs))
|
||||
new_args.push_back(m().mk_eq(arg, bit1));
|
||||
result = m().mk_or(new_args);
|
||||
if (is_one) {
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
@ -2330,12 +2327,10 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
|
||||
if (m_util.is_bv_xor(lhs)) {
|
||||
ptr_buffer<expr> new_args;
|
||||
unsigned num = to_app(lhs)->get_num_args();
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
new_args.push_back(m().mk_eq(to_app(lhs)->get_arg(i), bit1));
|
||||
}
|
||||
for (expr* arg : *to_app(lhs))
|
||||
new_args.push_back(m().mk_eq(arg, bit1));
|
||||
// TODO: bool xor is not flat_assoc... must fix that.
|
||||
result = m().mk_xor(new_args.size(), new_args.c_ptr());
|
||||
result = m().mk_xor(new_args);
|
||||
if (is_one) {
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
@ -2372,7 +2367,7 @@ br_status bv_rewriter::mk_blast_eq_value(expr * lhs, expr * rhs, expr_ref & resu
|
|||
mk_numeral(bit0 ? 0 : 1, 1)));
|
||||
div(v, two, v);
|
||||
}
|
||||
result = m().mk_and(new_args.size(), new_args.c_ptr());
|
||||
result = m().mk_and(new_args);
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
|
||||
|
@ -2438,7 +2433,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
}
|
||||
SASSERT(i1 == 0 && i2 == 0);
|
||||
SASSERT(new_eqs.size() >= 1);
|
||||
result = m().mk_and(new_eqs.size(), new_eqs.c_ptr());
|
||||
result = m().mk_and(new_eqs);
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
|
||||
|
|
|
@ -110,14 +110,16 @@ namespace array {
|
|||
struct hash {
|
||||
solver& s;
|
||||
hash(solver& s) :s(s) {}
|
||||
unsigned hash_select(axiom_record const& r) const {
|
||||
unsigned h = mk_mix(r.n->get_expr_id(), (unsigned)r.m_kind, r.select->get_arg(1)->get_expr_id());
|
||||
for (unsigned i = 2; i < r.select->num_args(); ++i)
|
||||
h = mk_mix(h, h, r.select->get_arg(i)->get_expr_id());
|
||||
return h;
|
||||
}
|
||||
unsigned operator()(unsigned idx) const {
|
||||
auto const& r = s.m_axiom_trail[idx];
|
||||
if (r.m_kind == kind_t::is_select) {
|
||||
unsigned h = mk_mix(r.n->get_expr_id(), (unsigned)r.m_kind, r.select->get_arg(1)->get_expr_id());
|
||||
for (unsigned i = 2; i < r.select->num_args(); ++i)
|
||||
h = mk_mix(h, 1, r.select->get_arg(i)->get_expr_id());
|
||||
return h;
|
||||
}
|
||||
if (r.m_kind == kind_t::is_select)
|
||||
return hash_select(r);
|
||||
return mk_mix(r.n->get_expr_id(), (unsigned)r.m_kind, r.select ? r.select->get_expr_id() : 1);
|
||||
}
|
||||
};
|
||||
|
@ -125,17 +127,20 @@ namespace array {
|
|||
struct eq {
|
||||
solver& s;
|
||||
eq(solver& s) :s(s) {}
|
||||
unsigned operator()(unsigned a, unsigned b) const {
|
||||
auto const& p = s.m_axiom_trail[a];
|
||||
auto const& r = s.m_axiom_trail[b];
|
||||
bool eq_select(axiom_record const& p, axiom_record const& r) const {
|
||||
if (p.m_kind != r.m_kind || p.n != r.n)
|
||||
return false;
|
||||
if (p.m_kind != kind_t::is_select)
|
||||
return p.select == r.select;
|
||||
for (unsigned i = p.select->num_args(); i-- > 1; )
|
||||
if (p.select->get_arg(i) != r.select->get_arg(i))
|
||||
return false;
|
||||
return true;
|
||||
return true;
|
||||
}
|
||||
unsigned operator()(unsigned a, unsigned b) const {
|
||||
auto const& p = s.m_axiom_trail[a];
|
||||
auto const& r = s.m_axiom_trail[b];
|
||||
if (p.m_kind == kind_t::is_select)
|
||||
return eq_select(p, r);
|
||||
return p.m_kind == r.m_kind && p.n == r.n && p.select == r.select;
|
||||
}
|
||||
};
|
||||
};
|
||||
|
|
|
@ -312,6 +312,8 @@ namespace recfun {
|
|||
}
|
||||
if (found) {
|
||||
++m_num_rounds;
|
||||
if (!to_delete && !m_disabled_guards.empty())
|
||||
to_delete = m_disabled_guards.back();
|
||||
if (to_delete) {
|
||||
m_disabled_guards.erase(to_delete);
|
||||
m_enabled_guards.push_back(to_delete);
|
||||
|
|
|
@ -436,13 +436,15 @@ namespace smt {
|
|||
}
|
||||
if (found) {
|
||||
m_num_rounds++;
|
||||
if (!to_delete && !m_disabled_guards.empty())
|
||||
to_delete = m_disabled_guards.back();
|
||||
if (to_delete) {
|
||||
m_disabled_guards.erase(to_delete);
|
||||
m_enabled_guards.push_back(to_delete);
|
||||
IF_VERBOSE(2, verbose_stream() << "(smt.recfun :enable-guard " << mk_pp(to_delete, m) << ")\n");
|
||||
}
|
||||
else {
|
||||
IF_VERBOSE(2, verbose_stream() << "(smt.recfun :increment-round)\n");
|
||||
IF_VERBOSE(2, verbose_stream() << "(smt.recfun :increment-round " << m_num_rounds << ")\n");
|
||||
}
|
||||
for (expr* g : m_enabled_guards)
|
||||
push_guard(g);
|
||||
|
|
Loading…
Reference in a new issue