diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index a8a8c30ec..311d849a7 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -19,6 +19,7 @@ Notes: #include "ast/rewriter/array_rewriter.h" #include "ast/rewriter/array_rewriter_params.hpp" #include "ast/ast_lt.h" +#include "ast/ast_util.h" #include "ast/ast_pp.h" #include "ast/rewriter/var_subst.h" @@ -566,6 +567,15 @@ bool array_rewriter::has_index_set(expr* e, expr_ref& else_case, vector eqs; args.reset(); args.resize(num_idxs + 1, nullptr); + bool is_not = m().is_bool(store_val) && m().is_not(e, e); + 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()); + continue; } - else if (m().is_eq(e, e1, e2)) { + if (m().is_eq(e, e1, e2)) { if (is_var(e2)) { std::swap(e1, e2); } @@ -601,11 +614,16 @@ bool array_rewriter::add_store(expr_ref_vector& args, unsigned num_idxs, expr* e else { return false; } - } + continue; + } + return false; } for (unsigned i = 0; i < num_idxs; ++i) { if (!args.get(i)) return false; } + if (is_not) { + store_val = mk_not(m(), store_val); + } args[num_idxs] = store_val; stores.push_back(args); return true; diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index 58c7f7ddc..2eb3ccac3 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -75,7 +75,8 @@ func_interp::func_interp(ast_manager & m, unsigned arity): m_arity(arity), m_else(nullptr), m_args_are_values(true), - m_interp(nullptr) { + m_interp(nullptr), + m_array_interp(nullptr) { } func_interp::~func_interp() { @@ -84,6 +85,7 @@ func_interp::~func_interp() { } m_manager.dec_ref(m_else); m_manager.dec_ref(m_interp); + m_manager.dec_ref(m_array_interp); } func_interp * func_interp::copy() const { @@ -98,7 +100,9 @@ func_interp * func_interp::copy() const { void func_interp::reset_interp_cache() { m_manager.dec_ref(m_interp); + m_manager.dec_ref(m_array_interp); m_interp = nullptr; + m_array_interp = nullptr; } bool func_interp::is_fi_entry_expr(expr * e, ptr_vector & args) { @@ -317,36 +321,6 @@ bool func_interp::is_identity() const { return (sz.size() == m_entries.size() + 1); } -expr_ref func_interp::get_array_interp(sort_ref_vector const& domain) const { - if (m_else == nullptr) - return expr_ref(m_manager); - if (!is_ground(m_else)) { - return expr_ref(m_manager); - } - array_util autil(m_manager); - sort_ref A(autil.mk_array_sort(domain.size(), domain.c_ptr(), m_manager.get_sort(m_else)), m_manager); - expr_ref r(autil.mk_const_array(A, m_else), m_manager); - expr_ref_vector args(m_manager); - for (func_entry * curr : m_entries) { - expr * res = curr->get_result(); - - if (m_else == res) { - continue; - } - args.reset(); - args.push_back(r); - for (unsigned i = 0; i < m_arity; i++) { - expr* arg = curr->get_arg(i); - if (!is_ground(arg)) { - return expr_ref(m_manager); - } - args.push_back(arg); - } - args.push_back(res); - r = autil.mk_store(args.size(), args.c_ptr()); - } - return r; -} expr * func_interp::get_interp_core() const { if (m_else == nullptr) @@ -382,6 +356,57 @@ expr * func_interp::get_interp_core() const { return r; } +expr* func_interp::get_array_interp_core(func_decl * f) const { + if (m_else == nullptr) + return nullptr; + ptr_vector domain; + for (sort* s : *f) { + domain.push_back(s); + } + expr* r; + + bool ground = is_ground(m_else); + for (func_entry * curr : m_entries) { + ground &= is_ground(curr->get_result()); + for (unsigned i = 0; i < m_arity; i++) { + ground &= is_ground(curr->get_arg(i)); + } + } + if (!ground) { + r = get_interp(); + if (!r) return r; + sort_ref_vector vars(m_manager); + svector var_names; + for (unsigned i = 0; i < m_arity; ++i) { + var_names.push_back(symbol(i)); + vars.push_back(domain.get(m_arity - i - 1)); + } + r = m_manager.mk_lambda(vars.size(), vars.c_ptr(), var_names.c_ptr(), r); + return r; + } + + expr_ref_vector args(m_manager); + array_util autil(m_manager); + sort_ref A(autil.mk_array_sort(domain.size(), domain.c_ptr(), m_manager.get_sort(m_else)), m_manager); + r = autil.mk_const_array(A, m_else); + for (func_entry * curr : m_entries) { + expr * res = curr->get_result(); + + if (m_else == res) { + continue; + } + args.reset(); + args.push_back(r); + for (unsigned i = 0; i < m_arity; i++) { + args.push_back(curr->get_arg(i)); + } + args.push_back(res); + r = autil.mk_store(args.size(), args.c_ptr()); + } + return r; +} + + expr * func_interp::get_interp() const { if (m_interp != nullptr) return m_interp; @@ -393,6 +418,17 @@ expr * func_interp::get_interp() const { return r; } +expr * func_interp::get_array_interp(func_decl * f) const { + if (m_array_interp != nullptr) + return m_array_interp; + expr* r = get_array_interp_core(f); + if (r != nullptr) { + const_cast(this)->m_array_interp = r; + m_manager.inc_ref(m_array_interp); + } + return r; +} + func_interp * func_interp::translate(ast_translation & translator) const { func_interp * new_fi = alloc(func_interp, translator.to(), m_arity); diff --git a/src/model/func_interp.h b/src/model/func_interp.h index 3fd82b59a..33aa9d286 100644 --- a/src/model/func_interp.h +++ b/src/model/func_interp.h @@ -73,10 +73,14 @@ class func_interp { expr * m_interp; //!< cache for representing the whole interpretation as a single expression (it uses ite terms). + expr * m_array_interp; // get_array_interp(domain); + new_t = fi->get_array_interp(f); TRACE("model", tout << "array interpretation:" << new_t << "\n";); } } @@ -429,17 +426,6 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition) if (new_t) { // noop } - else if (fi && fi->get_interp()) { - f = autil.get_as_array_func_decl(a); - expr_ref_vector sargs(m); - sort_ref_vector vars(m); - svector var_names; - for (unsigned i = 0; i < f->get_arity(); ++i) { - var_names.push_back(symbol(i)); - vars.push_back(f->get_domain(f->get_arity() - i - 1)); - } - new_t = m.mk_lambda(vars.size(), vars.c_ptr(), var_names.c_ptr(), fi->get_interp()); - } else if (f->is_skolem() && can_inline_def(ts, f) && (fi = get_func_interp(f)) && fi->get_interp() && (!ts.partition_ids().find(f, pid) || pid != current_partition)) { var_subst vs(m, false); diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 6986fa79b..823d334b3 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -150,6 +150,7 @@ struct evaluator_cfg : public default_rewriter_cfg { expr * val = m_model.get_const_interp(f); if (val != nullptr) { result = val; + // return BR_DONE; return m_ar.is_as_array(val)? BR_REWRITE1 : BR_DONE; } else if (m_model_completion) { @@ -243,19 +244,8 @@ struct evaluator_cfg : public default_rewriter_cfg { result = def; return BR_DONE; } - if (get_macro(g, def, q, def_pr)) { - sort_ref_vector sorts(m); - expr_ref_vector vars(m); - svector var_names; - unsigned sz = g->get_arity(); - for (unsigned i = 0; i < sz; ++i) { - var_names.push_back(symbol(sz - i - 1)); - vars.push_back(m.mk_var(sz - i - 1, g->get_domain(i))); - sorts.push_back(g->get_domain(i)); - } - var_subst subst(m, false); - result = subst(def, sorts.size(), vars.c_ptr()); - result = m.mk_lambda(sorts.size(), sorts.c_ptr(), var_names.c_ptr(), result); + func_interp * fi = m_model.get_func_interp(g); + if (fi && (result = fi->get_array_interp(g))) { model_evaluator ev(m_model, m_params); result = ev(result); m_pinned.push_back(result); @@ -530,47 +520,34 @@ struct evaluator_cfg : public default_rewriter_cfg { func_decl* f = m_ar.get_as_array_func_decl(to_app(a)); func_interp* g = m_model.get_func_interp(f); - if (!g) return false; + if (!g) return false; + else_case = g->get_else(); + if (!else_case) { + TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m) << "\n";); + return false; + } + bool ground = is_ground(else_case); unsigned sz = g->num_entries(); - unsigned arity = f->get_arity(); - unsigned base_sz = stores.size(); + expr_ref_vector store(m); for (unsigned i = 0; i < sz; ++i) { - expr_ref_vector store(m); + store.reset(); func_entry const* fe = g->get_entry(i); - store.append(arity, fe->get_args()); - store.push_back(fe->get_result()); - for (unsigned j = 0; j < store.size(); ++j) { - if (!is_ground(store[j].get())) { - TRACE("model_evaluator", tout << "could not extract array interpretation: " << mk_pp(a, m) << "\n" << mk_pp(store[j].get(), m) << "\n";); - return false; - } + expr* res = fe->get_result(); + if (m.are_equal(else_case, res)) { + continue; + } + ground &= is_ground(res); + store.append(g->get_arity(), fe->get_args()); + store.push_back(res); + for (expr* arg : store) { + ground &= is_ground(arg); } stores.push_back(store); } - else_case = g->get_else(); - if (!else_case) { - TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m) << "\n"; - /*model_smt2_pp(tout, m, m_model, 0);*/ - ); + if (!ground) { + TRACE("model_evaluator", tout << "could not extract ground array interpretation: " << mk_pp(a, m) << "\n";); return false; } - if (!is_ground(else_case)) { - TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m) << "\n" << else_case << "\n";); - return false; - } - for (unsigned i = stores.size(); are_values && i > base_sz; ) { - --i; - if (m.are_equal(else_case, stores[i].back())) { - for (unsigned j = i + 1; j < stores.size(); ++j) { - stores[j-1].reset(); - stores[j-1].append(stores[j]); - } - stores.pop_back(); - continue; - } - are_values &= args_are_values(stores[i], are_unique); - } - TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m) << "\n";); return true; } }; diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp index 766cfbb66..828ed6a61 100644 --- a/src/qe/qe_arrays.cpp +++ b/src/qe/qe_arrays.cpp @@ -515,9 +515,8 @@ namespace qe { * ... */ unsigned get_nesting_depth(app* eq) { - SASSERT(m.is_eq(eq)); - expr* lhs = eq->get_arg (0); - expr* rhs = eq->get_arg (1); + expr* lhs = nullptr, *rhs = nullptr; + VERIFY(m.is_eq(eq, lhs, rhs)); bool lhs_has_v = (lhs == m_v || m_has_stores_v.is_marked (lhs)); bool rhs_has_v = (rhs == m_v || m_has_stores_v.is_marked (rhs)); app* store = nullptr; @@ -537,9 +536,13 @@ namespace qe { } unsigned nd = 0; // nesting depth - for (nd = 1; m_arr_u.is_store (store); nd++, store = to_app (store->get_arg (0))) + for (nd = 1; m_arr_u.is_store (store); nd++, store = to_app (store->get_arg (0))) { /* empty */ ; - SASSERT (store == m_v); + } + if (store != m_v) { + TRACE("qe", tout << "not a store " << mk_pp(eq, m) << " " << lhs_has_v << " " << rhs_has_v << " " << mk_pp(m_v, m) << "\n";); + return UINT_MAX; + } return nd; }