From f7b2407a118ae50086c7f50ae5d190e31a672ac5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Jul 2020 10:14:56 -0700 Subject: [PATCH] for #4588 --- src/ast/rewriter/array_rewriter.cpp | 42 +++++++++++++++++++++++------ 1 file changed, 34 insertions(+), 8 deletions(-) diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 1df3d85ab..4a37b1e08 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -196,7 +196,7 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, return BR_REWRITE2; } else { - result = m().mk_ite(m().mk_and(eqs.size(), eqs.c_ptr()), v, sel_a_j); + result = m().mk_ite(m().mk_and(eqs), v, sel_a_j); return BR_REWRITE3; } } @@ -756,19 +756,45 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) #endif expr* lhs1 = lhs; + unsigned num_lhs = 0, num_rhs = 0; while (m_util.is_store(lhs1)) { lhs1 = to_app(lhs1)->get_arg(0); + ++num_lhs; } expr* rhs1 = rhs; while (m_util.is_store(rhs1)) { rhs1 = to_app(rhs1)->get_arg(0); + ++num_rhs; } - if (lhs1 != rhs1) { - return BR_FAILED; + if (lhs1 == rhs1) { + mk_eq(lhs, lhs, rhs, fmls); + mk_eq(rhs, lhs, rhs, fmls); + result = m().mk_and(fmls); + return BR_REWRITE_FULL; } - - mk_eq(lhs, lhs, rhs, fmls); - mk_eq(rhs, lhs, rhs, fmls); - result = m().mk_and(fmls.size(), fmls.c_ptr()); - return BR_REWRITE_FULL; + auto has_large_domain = [&](sort* s, unsigned num_stores) { + unsigned sz = get_array_arity(s); + uint64_t dsz = 1; + for (unsigned i = 0; i < sz; ++i) { + sort* d = get_array_domain(s, i); + if (d->is_infinite() || d->is_very_big()) + return true; + auto const& n = d->get_num_elements(); + if (n.size() > num_stores) + return true; + dsz *= n.size(); + if (dsz > num_stores) + return true; + } + return false; + }; + if (m_util.is_const(lhs1, v) && m_util.is_const(rhs1, w) && + has_large_domain(m().get_sort(lhs), std::max(num_lhs, num_rhs))) { + mk_eq(lhs, lhs, rhs, fmls); + mk_eq(rhs, lhs, rhs, fmls); + fmls.push_back(m().mk_eq(v, w)); + result = m().mk_and(fmls); + return BR_REWRITE_FULL; + } + return BR_FAILED; }