mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
parent
61b85d7123
commit
ebce0b3612
|
@ -691,16 +691,29 @@ expr_ref array_rewriter::expand_store(expr* s) {
|
|||
|
||||
br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
|
||||
TRACE("array_rewriter", tout << mk_bounded_pp(lhs, m(), 2) << " " << mk_bounded_pp(rhs, m(), 2) << "\n";);
|
||||
expr* v = nullptr;
|
||||
expr* v = nullptr, *w = nullptr;
|
||||
if (m_util.is_const(rhs) && is_lambda(lhs)) {
|
||||
std::swap(lhs, rhs);
|
||||
}
|
||||
if (m_util.is_const(rhs) && m_util.is_store(lhs)) {
|
||||
std::swap(lhs, rhs);
|
||||
}
|
||||
if (m_util.is_const(lhs, v) && m_util.is_const(rhs, w)) {
|
||||
result = m().mk_eq(v, w);
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
if (m_util.is_const(lhs, v) && is_lambda(rhs)) {
|
||||
quantifier* lam = to_quantifier(rhs);
|
||||
expr_ref e(m().mk_eq(lam->get_expr(), v), m());
|
||||
result = m().update_quantifier(lam, quantifier_kind::forall_k, e);
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
if (m_util.is_const(lhs, v) && m_util.is_store(rhs)) {
|
||||
expr_ref eq1(m().mk_eq(v, to_app(rhs)->get_arg(to_app(rhs)->get_num_args()-1)), m());
|
||||
expr_ref eq2(m().mk_eq(lhs, to_app(rhs)->get_arg(0)), m());
|
||||
result = m().mk_and(eq1, eq2);
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
expr_ref lh1(m()), rh1(m());
|
||||
if (m_expand_nested_stores) {
|
||||
if (is_expandable_store(lhs)) {
|
||||
|
|
Loading…
Reference in a new issue