From e1d2480a8b247d35f3a79c983c7c3ef1bc9b4a66 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Apr 2020 16:09:37 -0700 Subject: [PATCH] fix #3860 fix #3861 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/array_rewriter.cpp | 19 +++++++++----- src/ast/rewriter/bv_trailing.cpp | 30 ++++++++++++++-------- src/ast/rewriter/enum2bv_rewriter.cpp | 4 ++- src/ast/rewriter/rewriter_def.h | 36 ++++++++++----------------- src/ast/rewriter/var_subst.cpp | 9 +++---- src/smt/theory_array_base.cpp | 17 +++++++++++-- 6 files changed, 67 insertions(+), 48 deletions(-) diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 87e82d121..ac90617f3 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -644,6 +644,8 @@ bool array_rewriter::add_store(expr_ref_vector& args, unsigned num_idxs, expr* e bool array_rewriter::is_expandable_store(expr* s) { unsigned count = 0; unsigned depth = 0; + if (false && !is_ground(s)) + return false; while (m_util.is_store(s)) { s = to_app(s)->get_arg(0); count += s->get_ref_count(); @@ -653,8 +655,11 @@ bool array_rewriter::is_expandable_store(expr* s) { } expr_ref array_rewriter::expand_store(expr* s) { + sort* srt = m().get_sort(s); + unsigned arity = get_array_arity(srt); ptr_vector stores; - expr_ref result(m()); + expr_ref result(m()), tmp(m()); + var_shifter sh(m()); while (m_util.is_store(s)) { stores.push_back(to_app(s)); s = to_app(s)->get_arg(0); @@ -663,9 +668,9 @@ expr_ref array_rewriter::expand_store(expr* s) { expr_ref_vector args(m()), eqs(m()); ptr_vector sorts; svector names; - sort* srt = m().get_sort(s); - args.push_back(s); - for (unsigned i = get_array_arity(srt); i-- > 0; ) { + sh(s, arity, tmp); + args.push_back(tmp); + for (unsigned i = arity; i-- > 0; ) { args.push_back(m().mk_var(i, get_array_domain(srt, i))); sorts.push_back(get_array_domain(srt, i)); names.push_back(symbol(i)); @@ -676,9 +681,11 @@ expr_ref array_rewriter::expand_store(expr* s) { for (app* st : stores) { eqs.reset(); for (unsigned i = 1; i < args.size(); ++i) { - eqs.push_back(m().mk_eq(args.get(i), st->get_arg(i))); + sh(st->get_arg(i), arity, tmp); + eqs.push_back(m().mk_eq(args.get(i), tmp)); } - result = m().mk_ite(mk_and(eqs), st->get_arg(args.size()), result); + sh(st->get_arg(args.size()), arity, tmp); + result = m().mk_ite(mk_and(eqs), tmp, result); } result = m().mk_lambda(sorts.size(), sorts.c_ptr(), names.c_ptr(), result); return result; diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp index 0dd59e5c2..e06f5eeb2 100644 --- a/src/ast/rewriter/bv_trailing.cpp +++ b/src/ast/rewriter/bv_trailing.cpp @@ -17,6 +17,7 @@ #include "ast/rewriter/bv_trailing.h" #include "ast/bv_decl_plugin.h" #include "ast/ast_pp.h" +#include "ast/ast_ll_pp.h" // The analyzer gives up analysis after going TRAILING_DEPTH deep. // This number shouldn't be too big. @@ -69,6 +70,7 @@ struct bv_trailing::imp { } expr_ref out1(m); expr_ref out2(m); + TRACE("bv-trailing", tout << min << "\n";); VERIFY(min == remove_trailing(e1, min, out1, TRAILING_DEPTH)); VERIFY(min == remove_trailing(e2, min, out2, TRAILING_DEPTH)); const bool are_eq = m.are_equal(out1, out2); @@ -152,13 +154,11 @@ struct bv_trailing::imp { if (!m_util.is_numeral(tmp, c_val, c_sz) || !c_val.is_one()) new_args.push_back(std::move(tmp)); - if (new_sz == 0) { result = nullptr; return retv; } - for (unsigned i = 1; i < num; i++) { expr * const curr = a->get_arg(i); new_args.push_back(m_mk_extract(new_sz - 1, 0, curr)); @@ -168,6 +168,7 @@ struct bv_trailing::imp { case 1: result = new_args.get(0); break; default: result = m.mk_app(m_util.get_fid(), OP_BMUL, new_args.size(), new_args.c_ptr()); } + SASSERT(retv == m_util.get_bv_size(result)); return retv; } @@ -179,22 +180,28 @@ struct bv_trailing::imp { } const unsigned num = a->get_num_args(); unsigned retv = 0; - unsigned i = num; + unsigned i; expr_ref new_last(nullptr, m); - while (i && retv < n) { - i--; + for (i = num; retv < n && i-- > 0; ) { + new_last = nullptr; expr * const curr = a->get_arg(i); - const unsigned cur_rm = remove_trailing(curr, n, new_last, depth - 1); - const unsigned curr_sz = m_util.get_bv_size(curr); + unsigned cur_rm = remove_trailing(curr, n, new_last, depth - 1); + unsigned curr_sz = m_util.get_bv_size(curr); retv += cur_rm; - if (cur_rm < curr_sz) break; + if (cur_rm < curr_sz) { + break; + } } + if (retv == 0) { result = a; return 0; } - if (!i && !new_last) {// all args eaten completely + if (i == 0 && retv != m_util.get_bv_size(a)) + new_last = a->get_arg(0); + + if (i == 0 && !new_last) { // all args eaten completely SASSERT(retv == m_util.get_bv_size(a)); result = nullptr; return retv; @@ -222,7 +229,10 @@ struct bv_trailing::imp { unsigned remove_trailing_core(expr * e, unsigned n, expr_ref& result, unsigned depth) { SASSERT(m_util.is_bv(e)); - if (!depth || !n) { + if (depth == 0) { + return 0; + } + if (n == 0) { return 0; } unsigned sz; diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp index 0778b98db..a8edb2dcc 100644 --- a/src/ast/rewriter/enum2bv_rewriter.cpp +++ b/src/ast/rewriter/enum2bv_rewriter.cpp @@ -54,6 +54,7 @@ struct enum2bv_rewriter::imp { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { expr_ref a0(m), a1(m); expr_ref_vector _args(m); + result_pr = nullptr; if (m.is_eq(f) && reduce_arg(args[0], a0) && reduce_arg(args[1], a1)) { result = m.mk_eq(a0, a1); return BR_DONE; @@ -201,7 +202,8 @@ struct enum2bv_rewriter::imp { q->get_weight(), q->get_qid(), q->get_skid(), q->get_num_patterns(), new_patterns, q->get_num_no_patterns(), new_no_patterns); - result_pr = nullptr; + if (m.proofs_enabled()) + result_pr = m.mk_rewrite(q, result); return true; } diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 8fe1c3747..f5b568969 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -47,8 +47,7 @@ void rewriter_tpl::process_var(var * v) { tout << "index " << index << " bindings " << m_bindings.size() << "\n"; display_bindings(tout);); SASSERT(v->get_sort() == m().get_sort(r)); - if (!is_ground(r) && m_shifts[index] != m_bindings.size()) { - + if (!is_ground(r) && m_shifts[index] != m_bindings.size()) { unsigned shift_amount = m_bindings.size() - m_shifts[index]; expr* c = get_cached(r, shift_amount); if (c) { @@ -58,8 +57,7 @@ void rewriter_tpl::process_var(var * v) { expr_ref tmp(m()); m_shifter(r, shift_amount, tmp); result_stack().push_back(tmp); - TRACE("rewriter", tout << "shift: " << shift_amount << " idx: " << idx << " --> " << tmp << "\n"; - display_bindings(tout);); + TRACE("rewriter", display_bindings(tout << "shift: " << shift_amount << " idx: " << idx << " --> " << tmp << "\n");); cache_shifted_result(r, shift_amount, tmp); } } @@ -514,14 +512,12 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { SASSERT(fr.m_state == PROCESS_CHILDREN); unsigned num_decls = q->get_num_decls(); if (fr.m_i == 0) { - if (!ProofGen) { - begin_scope(); - m_root = q->get_expr(); - unsigned sz = m_bindings.size(); - for (unsigned i = 0; i < num_decls; i++) { - m_bindings.push_back(nullptr); - m_shifts.push_back(sz); - } + begin_scope(); + m_root = q->get_expr(); + unsigned sz = m_bindings.size(); + for (unsigned i = 0; i < num_decls; i++) { + m_bindings.push_back(nullptr); + m_shifts.push_back(sz); } m_num_qvars += num_decls; } @@ -595,17 +591,11 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { result_stack().shrink(fr.m_spos); result_stack().push_back(m_r.get()); SASSERT(m().get_sort(q) == m().get_sort(m_r)); - if (!ProofGen) { - SASSERT(num_decls <= m_bindings.size()); - m_bindings.shrink(m_bindings.size() - num_decls); - m_shifts.shrink(m_shifts.size() - num_decls); - end_scope(); - cache_result(q, m_r, m_pr, fr.m_cache_result); - } - else { - cache_result(q, m_r, m_pr, fr.m_cache_result); - m_pr = nullptr; - } + SASSERT(num_decls <= m_bindings.size()); + m_bindings.shrink(m_bindings.size() - num_decls); + m_shifts.shrink(m_shifts.size() - num_decls); + end_scope(); + cache_result(q, m_r, m_pr, fr.m_cache_result); m_r = nullptr; frame_stack().pop_back(); set_new_child_flag(q, m_r); diff --git a/src/ast/rewriter/var_subst.cpp b/src/ast/rewriter/var_subst.cpp index ff479b565..d833cfd3b 100644 --- a/src/ast/rewriter/var_subst.cpp +++ b/src/ast/rewriter/var_subst.cpp @@ -41,7 +41,7 @@ expr_ref var_subst::operator()(expr * n, unsigned num_args, expr * const * args) tout << "m_std_order: " << m_std_order << "\n" << mk_ismt2_pp(n, m_reducer.m()) << "\nusing\n"; for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m_reducer.m()) << "\n"; tout << "\n------>\n"; - tout << mk_ismt2_pp(result, m_reducer.m()) << "\n";); + tout << result << "\n";); return result; } @@ -119,7 +119,6 @@ expr_ref unused_vars_eliminator::operator()(quantifier* q) { var_mapping.push_back(nullptr); } - // Remark: // (VAR 0) should be in the last position of var_mapping. // ... @@ -215,10 +214,8 @@ static void get_free_vars_offset(expr_sparse_mark& mark, ptr_vector& todo, break; } case AST_APP: { - app* a = to_app(e); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - todo.push_back(a->get_arg(i)); - } + for (expr* arg : *to_app(e)) + todo.push_back(arg); break; } default: diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 06f1c0ed0..919829e87 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -401,8 +401,21 @@ namespace smt { quantifier * q = m.is_lambda_def(e->get_decl()); expr_ref f(e, m); if (q) { - var_subst sub(m); - f = sub(q, e->get_num_args(), e->get_args()); + // the variables in q are maybe not consecutive. + var_subst sub(m, false); + expr_free_vars fv; + fv(q); + expr_ref_vector es(m); + es.resize(fv.size()); + for (unsigned i = 0, j = 0; i < e->get_num_args(); ++i) { + SASSERT(j < es.size()); + while (!fv[j]) { + ++j; + SASSERT(j < es.size()); + } + es[j++] = e->get_arg(i); + } + f = sub(q, es.size(), es.c_ptr()); } return f; }