From 84990ffa277002d0b8737af95bb890c0d7ab6191 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Jul 2019 14:21:22 +0100 Subject: [PATCH] fixing #2378 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 1 + src/ast/rewriter/array_rewriter.cpp | 93 ++++++++++++++++++----------- src/ast/rewriter/array_rewriter.h | 6 +- src/model/model_evaluator.cpp | 14 +++++ src/qe/qe_arrays.cpp | 2 +- 5 files changed, 79 insertions(+), 37 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index d7b81b424..a829cb200 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1119,6 +1119,7 @@ sort* basic_decl_plugin::join(sort* s1, sort* s2) { } std::ostringstream buffer; buffer << "Sorts " << mk_pp(s1, *m_manager) << " and " << mk_pp(s2, *m_manager) << " are incompatible"; + INVOKE_DEBUGGER(); throw ast_exception(buffer.str()); } diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index a458a3674..a8a8c30ec 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -539,53 +539,75 @@ void array_rewriter::mk_eq(expr* e, expr* lhs, expr* rhs, expr_ref_vector& fmls) } } -bool array_rewriter::has_index_set(expr* e, expr_ref& e0, vector& indices) { +bool array_rewriter::has_index_set(expr* e, expr_ref& else_case, vector& stores) { expr_ref_vector args(m()); expr_ref a(m()), v(m()); a = e; while (m_util.is_store_ext(e, a, args, v)) { - indices.push_back(args); + args.push_back(v); + stores.push_back(args); e = a; } - e0 = e; - if (is_lambda(e0)) { - quantifier* q = to_quantifier(e0); + if (m_util.is_const(e, e)) { + else_case = e; + return true; + } + if (is_lambda(e)) { + quantifier* q = to_quantifier(e); e = q->get_expr(); unsigned num_idxs = q->get_num_decls(); - expr* e1, *e2, *e3; - ptr_vector eqs; - while (!is_ground(e) && m().is_ite(e, e1, e2, e3) && is_ground(e2)) { - args.reset(); - args.resize(num_idxs, nullptr); - eqs.reset(); - eqs.push_back(e1); - for (unsigned i = 0; i < eqs.size(); ++i) { - expr* e = eqs[i]; - if (m().is_and(e)) { - eqs.append(to_app(e)->get_num_args(), to_app(e)->get_args()); - } - else if (m().is_eq(e, e1, e2)) { - if (is_var(e2)) { - std::swap(e1, e2); - } - if (is_var(e1) && is_ground(e2)) { - unsigned idx = to_var(e1)->get_idx(); - args[num_idxs - idx - 1] = e2; - } - else { - return false; - } - } + expr* e1, *e3, *store_val; + if (!is_ground(e) && m().is_or(e)) { + for (expr* arg : *to_app(e)) { + if (!add_store(args, num_idxs, arg, m().mk_true(), stores)) { + return false; + } } - for (unsigned i = 0; i < num_idxs; ++i) { - if (!args.get(i)) return false; - } - indices.push_back(args); + else_case = m().mk_false(); + return true; + } + while (!is_ground(e) && m().is_ite(e, e1, store_val, e3) && is_ground(store_val)) { + if (!add_store(args, num_idxs, e1, store_val, stores)) { + return false; + } e = e3; } - e0 = e; + else_case = e; return is_ground(e); } + return false; +} + +bool array_rewriter::add_store(expr_ref_vector& args, unsigned num_idxs, expr* e, expr* store_val, vector& stores) { + + expr* e1, *e2; + ptr_vector eqs; + args.reset(); + args.resize(num_idxs + 1, nullptr); + eqs.push_back(e); + for (unsigned i = 0; i < eqs.size(); ++i) { + e = eqs[i]; + if (m().is_and(e)) { + eqs.append(to_app(e)->get_num_args(), to_app(e)->get_args()); + } + else if (m().is_eq(e, e1, e2)) { + if (is_var(e2)) { + std::swap(e1, e2); + } + if (is_var(e1) && is_ground(e2)) { + unsigned idx = to_var(e1)->get_idx(); + args[num_idxs - idx - 1] = e2; + } + else { + return false; + } + } + } + for (unsigned i = 0; i < num_idxs; ++i) { + if (!args.get(i)) return false; + } + args[num_idxs] = store_val; + stores.push_back(args); return true; } @@ -616,7 +638,8 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) for (auto const& idxs : indices) { args.reset(); args.push_back(lhs); - args.append(idxs); + idxs.pop_back(); + args.append(idxs); mk_select(args.size(), args.c_ptr(), tmp1); args[0] = rhs; mk_select(args.size(), args.c_ptr(), tmp2); diff --git a/src/ast/rewriter/array_rewriter.h b/src/ast/rewriter/array_rewriter.h index 18fb74adb..23cbbacde 100644 --- a/src/ast/rewriter/array_rewriter.h +++ b/src/ast/rewriter/array_rewriter.h @@ -35,11 +35,12 @@ class array_rewriter { bool m_expand_select_ite; template lbool compare_args(unsigned num_args, expr * const * args1, expr * const * args2); - bool has_index_set(expr* e, expr_ref& e0, vector& indices); void mk_eq(expr* e, expr* lhs, expr* rhs, expr_ref_vector& fmls); sort_ref get_map_array_sort(func_decl* f, unsigned num_args, expr* const* args); + bool add_store(expr_ref_vector& args, unsigned num_idxs, expr* e, expr* store_val, vector& stores); + public: array_rewriter(ast_manager & m, params_ref const & p = params_ref()): m_util(m) { @@ -65,6 +66,9 @@ public: void mk_select(unsigned num_args, expr * const * args, expr_ref & result); void mk_map(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); + bool has_index_set(expr* e, expr_ref& e0, vector& indices); + + // The following methods never return BR_FAILED br_status mk_set_union(unsigned num_args, expr * const * args, expr_ref & result); br_status mk_set_intersect(unsigned num_args, expr * const * args, expr_ref & result); diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index ca670cc04..6986fa79b 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -184,6 +184,14 @@ struct evaluator_cfg : public default_rewriter_cfg { st = m_seq_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_ar_rw.get_fid()) st = mk_array_eq(args[0], args[1], result); + else if (m.are_equal(args[0], args[1])) { + result = m.mk_true(); + st = BR_DONE; + } + else if (m.are_distinct(args[0], args[1])) { + result = m.mk_false(); + st = BR_DONE; + } TRACE("model_evaluator", tout << st << " " << mk_pp(s, m) << " " << s_fid << " " << m_ar_rw.get_fid() << " " << mk_pp(args[0], m) << " " << mk_pp(args[1], m) << " " << result << "\n";); @@ -508,6 +516,12 @@ struct evaluator_cfg : public default_rewriter_cfg { return true; } + if (m_ar_rw.has_index_set(a, else_case, stores)) { + for (auto const& store : stores) { + are_values &= args_are_values(store, are_unique); + } + return true; + } if (!m_ar.is_as_array(a)) { TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m) << "\n";); TRACE("model_evaluator", tout << m_model << "\n";); diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp index 460f9ea37..766cfbb66 100644 --- a/src/qe/qe_arrays.cpp +++ b/src/qe/qe_arrays.cpp @@ -389,7 +389,7 @@ namespace qe { if (!m_has_stores_v.is_marked (lhs)) { std::swap (lhs, rhs); } - if (m_has_stores_v.is_marked (lhs)) { + if (m_has_stores_v.is_marked (lhs) && m_arr_u.is_store(lhs)) { /** project using the equivalence: * * (store(arr0,idx,x) ==I arr1) <->