From 988466705c47cabb216b892b72dcf60939086a90 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Sat, 19 May 2018 17:53:28 -0700 Subject: [PATCH] port array projection to qe_arrays ensure it works with multi-dimensional arrays commit on behalf of Nikolaj --- src/qe/qe_arrays.cpp | 1106 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 1103 insertions(+), 3 deletions(-) diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp index a227d755e..ad9d5d63f 100644 --- a/src/qe/qe_arrays.cpp +++ b/src/qe/qe_arrays.cpp @@ -18,16 +18,144 @@ Revision History: --*/ -#include "qe/qe_arrays.h" +#include "util/lbool.h" #include "ast/rewriter/rewriter_def.h" #include "ast/expr_functors.h" #include "ast/rewriter/expr_safe_replace.h" -#include "util/lbool.h" +#include "ast/rewriter/th_rewriter.h" #include "ast/ast_util.h" #include "ast/ast_pp.h" +#include "model/model_evaluator.h" +#include "qe/qe_arrays.h" + + +namespace { + bool is_partial_eq (app* a); + + /** + * \brief utility class for partial equalities + * + * A partial equality (a ==I b), for two arrays a,b and a finite set of indices I holds + * iff (Forall i. i \not\in I => a[i] == b[i]); in other words, it is a + * restricted form of the extensionality axiom + * + * using this class, we denote (a =I b) as f(a,b,i0,i1,...) + * where f is an uninterpreted predicate with name PARTIAL_EQ and + * I = {i0,i1,...} + */ + + // TBD: make work for arrays with multiple arguments. + class peq { + ast_manager& m; + expr_ref m_lhs; + expr_ref m_rhs; + vector m_diff_indices; + func_decl_ref m_decl; // the partial equality declaration + app_ref m_peq; // partial equality application + app_ref m_eq; // equivalent std equality using def. of partial eq + array_util m_arr_u; + + public: + static const char* PARTIAL_EQ; + + peq (app* p, ast_manager& m): + m (m), + m_lhs (p->get_arg (0), m), + m_rhs (p->get_arg (1), m), + m_decl (p->get_decl (), m), + m_peq (p, m), + m_eq (m), + m_arr_u (m) + { + VERIFY (is_partial_eq (p)); + SASSERT (m_arr_u.is_array (m_lhs) && + m_arr_u.is_array (m_rhs) && + m.get_sort(m_lhs) == m.get_sort(m_rhs)); + unsigned arity = get_array_arity(m.get_sort(m_lhs)); + for (unsigned i = 2; i < p->get_num_args (); i += arity) { + SASSERT(arity + i <= p->get_num_args()); + expr_ref_vector vec(m); + vec.append(arity, p->get_args() + i); + m_diff_indices.push_back (vec); + } + } + + peq (expr* lhs, expr* rhs, vector const& diff_indices, ast_manager& m): + m (m), + m_lhs (lhs, m), + m_rhs (rhs, m), + m_diff_indices (diff_indices), + m_decl (m), + m_peq (m), + m_eq (m), + m_arr_u (m) { + SASSERT (m_arr_u.is_array (lhs) && + m_arr_u.is_array (rhs) && + m.get_sort(lhs) == m.get_sort(rhs)); + ptr_vector sorts; + sorts.push_back (m.get_sort (m_lhs)); + sorts.push_back (m.get_sort (m_rhs)); + for (auto const& v : diff_indices) { + SASSERT(v.size() == get_array_arity(m.get_sort(m_lhs))); + for (expr* e : v) + sorts.push_back (m.get_sort(e)); + } + m_decl = m.mk_func_decl (symbol (PARTIAL_EQ), sorts.size (), sorts.c_ptr (), m.mk_bool_sort ()); + } + + expr_ref lhs () { return m_lhs; } + + expr_ref rhs () { return m_rhs; } + + void get_diff_indices (vector& result) { result.append(m_diff_indices); } + + app_ref mk_peq () { + if (!m_peq) { + ptr_vector args; + args.push_back (m_lhs); + args.push_back (m_rhs); + for (auto const& v : m_diff_indices) { + args.append (v.size(), v.c_ptr()); + } + m_peq = m.mk_app (m_decl, args.size (), args.c_ptr ()); + } + return m_peq; + } + + app_ref mk_eq (app_ref_vector& aux_consts, bool stores_on_rhs = true) { + if (!m_eq) { + expr_ref lhs (m_lhs, m), rhs (m_rhs, m); + if (!stores_on_rhs) { + std::swap (lhs, rhs); + } + // lhs = (...(store (store rhs i0 v0) i1 v1)...) + sort* val_sort = get_array_range (m.get_sort (lhs)); + for (expr_ref_vector const& diff : m_diff_indices) { + ptr_vector store_args; + store_args.push_back (rhs); + store_args.append (diff.size(), diff.c_ptr()); + app_ref val(m.mk_fresh_const ("diff", val_sort), m); + store_args.push_back (val); + aux_consts.push_back (val); + rhs = m_arr_u.mk_store (store_args.size (), store_args.c_ptr ()); + } + m_eq = m.mk_eq (lhs, rhs); + } + return m_eq; + } + }; + + const char* peq::PARTIAL_EQ = "!partial_eq"; + + bool is_partial_eq (app* a) { + return a->get_decl ()->get_name () == peq::PARTIAL_EQ; + } +} namespace qe { + + struct array_project_plugin::imp { // rewriter or direct procedure. @@ -187,7 +315,8 @@ namespace qe { return (*m_var)(e); } - void mk_eq(indices& x, indices y, expr_ref_vector& lits) { + void mk_eq(indices const& x, indices const& y, expr_ref_vector& lits) { + SASSERT(x.m_values.size() == y.m_values.size()); unsigned n = x.m_values.size(); for (unsigned j = 0; j < n; ++j) { lits.push_back(m.mk_eq(x.m_vars[j], y.m_vars[j])); @@ -430,5 +559,976 @@ namespace qe { return m_imp->a.get_family_id(); } + static bool is_eq(expr_ref_vector const& xs, expr_ref_vector const& ys) { + for (unsigned i = 0; i < xs.size(); ++i) if (xs[i] != ys[i]) return false; + return true; + } + + static expr_ref mk_eq(expr_ref_vector const& xs, expr_ref_vector const& ys) { + ast_manager& m = xs.get_manager(); + expr_ref_vector eqs(m); + for (unsigned i = 0; i < xs.size(); ++i) eqs.push_back(m.mk_eq(xs[i], ys[i])); + return mk_and(eqs); + } + + + class array_project_eqs_util { + ast_manager& m; + array_util m_arr_u; + model_ref M; + model_evaluator* m_mev; + app_ref m_v; // array var to eliminate + ast_mark m_has_stores_v; // has stores for m_v + expr_ref m_subst_term_v; // subst term for m_v + expr_safe_replace m_true_sub_v; // subst for true equalities + expr_safe_replace m_false_sub_v; // subst for false equalities + expr_ref_vector m_aux_lits_v; + expr_ref_vector m_idx_lits_v; + app_ref_vector m_aux_vars; + + void reset_v () { + m_v = nullptr; + m_has_stores_v.reset (); + m_subst_term_v = nullptr; + m_true_sub_v.reset (); + m_false_sub_v.reset (); + m_aux_lits_v.reset (); + m_idx_lits_v.reset (); + } + + void reset () { + M = nullptr; + m_mev = nullptr; + reset_v (); + m_aux_vars.reset (); + } + + /** + * find all array equalities on m_v or containing stores on/of m_v + * + * also mark terms containing stores on/of m_v + */ + void find_arr_eqs (expr_ref const& fml, app_ref_vector& eqs) { + if (!is_app (fml)) return; + ast_mark done; + ptr_vector todo; + todo.push_back (to_app (fml)); + while (!todo.empty ()) { + app* a = todo.back (); + if (done.is_marked (a)) { + todo.pop_back (); + continue; + } + bool all_done = true; + bool args_have_stores = false; + for (expr * arg : *a) { + if (!is_app (arg)) continue; + if (!done.is_marked (arg)) { + all_done = false; + todo.push_back (to_app (arg)); + } + else if (!args_have_stores && m_has_stores_v.is_marked (arg)) { + args_have_stores = true; + } + } + if (!all_done) continue; + todo.pop_back (); + + // mark if a has stores + if ((!m_arr_u.is_select (a) && args_have_stores) || + (m_arr_u.is_store (a) && (a->get_arg (0) == m_v))) { + m_has_stores_v.mark (a, true); + + TRACE ("qe", + tout << "has stores:\n"; + tout << mk_pp (a, m) << "\n"; + ); + } + + // check if a is a relevant array equality + expr * a0 = nullptr, *a1 = nullptr; + if (m.is_eq (a, a0, a1)) { + if (a0 == m_v || a1 == m_v || + (m_arr_u.is_array (a0) && m_has_stores_v.is_marked (a))) { + eqs.push_back (a); + } + } + // else, we can check for disequalities and handle them using extensionality, + // but it's not necessary + + done.mark (a, true); + } + } + + /** + * factor out select terms on m_v using fresh consts + */ + void factor_selects (app_ref& fml) { + expr_map sel_cache (m); + ast_mark done; + ptr_vector todo; + expr_ref_vector pinned (m); // to ensure a reference + + todo.push_back (fml); + while (!todo.empty ()) { + app* a = todo.back (); + if (done.is_marked (a)) { + todo.pop_back (); + continue; + } + expr_ref_vector args (m); + bool all_done = true; + for (expr * arg : *a) { + if (!is_app (arg)) continue; + if (!done.is_marked (arg)) { + all_done = false; + todo.push_back (to_app (arg)); + } + else if (all_done) { // all done so far.. + expr* arg_new = nullptr; proof* pr; + sel_cache.get (arg, arg_new, pr); + if (!arg_new) { + arg_new = arg; + } + args.push_back (arg_new); + } + } + if (!all_done) continue; + todo.pop_back (); + + expr_ref a_new (m.mk_app (a->get_decl (), args.size (), args.c_ptr ()), m); + + // if a_new is select on m_v, introduce new constant + if (m_arr_u.is_select (a) && + (args.get (0) == m_v || m_has_stores_v.is_marked (args.get (0)))) { + sort* val_sort = get_array_range (m.get_sort (m_v)); + app_ref val_const (m.mk_fresh_const ("sel", val_sort), m); + m_aux_vars.push_back (val_const); + // extend M to include val_const + expr_ref val = (*m_mev)(a_new); + M->register_decl (val_const->get_decl (), val); + // add equality + m_aux_lits_v.push_back (m.mk_eq (val_const, a_new)); + // replace select by const + a_new = val_const; + } + + if (a != a_new) { + sel_cache.insert (a, a_new, nullptr); + pinned.push_back (a_new); + } + done.mark (a, true); + } + expr* res = nullptr; proof* pr; + sel_cache.get (fml, res, pr); + if (res) { + fml = to_app (res); + } + } + + /** + * convert partial equality expression p_exp to an equality by + * recursively adding stores on diff indices + * + * add stores on lhs or rhs depending on whether stores_on_rhs is false/true + */ + void convert_peq_to_eq (expr* p_exp, app_ref& eq, bool stores_on_rhs = true) { + peq p (to_app (p_exp), m); + app_ref_vector diff_val_consts (m); + eq = p.mk_eq (diff_val_consts, stores_on_rhs); + m_aux_vars.append (diff_val_consts); + // extend M to include diff_val_consts + vector I; + expr_ref arr = p.lhs (); + p.get_diff_indices (I); + expr_ref val (m); + unsigned num_diff = diff_val_consts.size (); + SASSERT (num_diff == I.size ()); + for (unsigned i = 0; i < num_diff; i++) { + // mk val term + ptr_vector sel_args; + sel_args.push_back (arr); + sel_args.append(I[i].size(), I[i].c_ptr()); + expr_ref val_term (m_arr_u.mk_select (sel_args.size (), sel_args.c_ptr ()), m); + // evaluate and assign to ith diff_val_const + val = (*m_mev)(val_term); + M->register_decl (diff_val_consts.get (i)->get_decl (), val); + } + } + + /** + * mk (e0 ==indices e1) + * + * result has stores if either e0 or e1 or an index term has stores + */ + app_ref mk_peq (expr* e0, expr* e1, vector const& indices) { + peq p (e0, e1, indices, m); + return p.mk_peq (); + } + + void find_subst_term (app* eq) { + SASSERT(m.is_eq(eq)); + vector empty; + app_ref p_exp = mk_peq (eq->get_arg (0), eq->get_arg (1), empty); + bool subst_eq_found = false; + while (true) { + TRACE ("qe", tout << "processing peq:\n" << p_exp << "\n";); + + peq p (p_exp, m); + expr_ref lhs = p.lhs(), rhs = p.rhs(); + if (!m_has_stores_v.is_marked (lhs)) { + std::swap (lhs, rhs); + } + if (m_has_stores_v.is_marked (lhs)) { + /** project using the equivalence: + * + * (store(arr0,idx,x) ==I arr1) <-> + * + * (idx \in I => (arr0 ==I arr1)) /\ + * (idx \not\in I => (arr0 ==I+idx arr1) /\ (arr1[idx] == x))) + */ + vector I; + expr_ref_vector idxs (m); + p.get_diff_indices (I); + app* a_lhs = to_app (lhs); + expr* arr0 = a_lhs->get_arg (0); + idxs.append(a_lhs->get_num_args() - 2, a_lhs->get_args() + 1); + expr* x = a_lhs->get_arg (2); + expr* arr1 = rhs; + // check if (idx \in I) in M + bool idx_in_I = false; + expr_ref_vector idx_diseq (m); + if (!I.empty ()) { + expr_ref_vector vals = (*m_mev)(idxs); + for (unsigned i = 0; i < I.size () && !idx_in_I; i++) { + if (is_eq(idxs, I.get(i))) { + idx_in_I = true; + } + else { + expr_ref idx_eq = mk_eq(idxs, I[i]); + expr_ref_vector vals1 = (*m_mev)(I[i]); + if (is_eq(vals, vals1)) { + idx_in_I = true; + m_idx_lits_v.push_back (idx_eq); + } + else { + idx_diseq.push_back (m.mk_not (idx_eq)); + } + } + } + } + if (idx_in_I) { + TRACE ("qe", + tout << "store index in diff indices:\n"; + tout << mk_pp (m_idx_lits_v.back (), m) << "\n"; + ); + + // arr0 ==I arr1 + p_exp = mk_peq (arr0, arr1, I); + + TRACE ("qe", + tout << "new peq:\n"; + tout << mk_pp (p_exp, m) << "\n"; + ); + } + else { + m_idx_lits_v.append (idx_diseq); + // arr0 ==I+idx arr1 + I.push_back (idxs); + p_exp = mk_peq (arr0, arr1, I); + + TRACE ("qe", tout << "new peq:\n" << p_exp << "\n"; ); + + // arr1[idx] == x + ptr_vector sel_args; + sel_args.push_back (arr1); + sel_args.append(idxs.size(), idxs.c_ptr()); + expr_ref arr1_idx (m_arr_u.mk_select (sel_args.size (), sel_args.c_ptr ()), m); + expr_ref eq (m.mk_eq (arr1_idx, x), m); + m_aux_lits_v.push_back (eq); + + TRACE ("qe", + tout << "new eq:\n"; + tout << mk_pp (eq, m) << "\n"; + ); + } + } + else if (lhs == rhs) { // trivial peq (a ==I a) + break; + } + else if (lhs == m_v || rhs == m_v) { + subst_eq_found = true; + TRACE ("qe", + tout << "subst eq found!\n"; + ); + break; + } + else { + UNREACHABLE (); + } + } + + // factor out select terms on m_v from p_exp using fresh constants + if (subst_eq_found) { + factor_selects (p_exp); + + TRACE ("qe", + tout << "after factoring selects:\n"; + tout << mk_pp (p_exp, m) << "\n"; + for (unsigned i = m_aux_lits_v.size () - m_aux_vars.size (); i < m_aux_lits_v.size (); i++) { + tout << mk_pp (m_aux_lits_v.get (i), m) << "\n"; + } + ); + + // find subst_term + bool stores_on_rhs = true; + app* a = to_app (p_exp); + if (a->get_arg (1) == m_v) { + stores_on_rhs = false; + } + app_ref eq (m); + convert_peq_to_eq (p_exp, eq, stores_on_rhs); + m_subst_term_v = eq->get_arg (1); + + TRACE ("qe", + tout << "subst term found:\n"; + tout << mk_pp (m_subst_term_v, m) << "\n"; + ); + } + } + + /** + * compute nesting depths of stores on m_v in true_eqs, as follows: + * 0 if m_v appears on both sides of equality + * 1 if equality is (m_v=t) + * 2 if equality is (store(m_v,i,v)=t) + * ... + */ + unsigned get_nesting_depth(app* eq) { + SASSERT(m.is_eq(eq)); + expr* lhs = eq->get_arg (0); + expr* rhs = eq->get_arg (1); + 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; + + SASSERT (lhs_has_v || rhs_has_v); + + if (!lhs_has_v && is_app(rhs)) { + store = to_app (rhs); + } + else if (!rhs_has_v && is_app(lhs)) { + store = to_app (lhs); + } + else { + // v appears on both sides -- trivial equality + // put it in the beginning to simplify it away + return 0; + } + + unsigned nd = 0; // nesting depth + for (nd = 1; m_arr_u.is_store (store); nd++, store = to_app (store->get_arg (0))) + /* empty */ ; + SASSERT (store == m_v); + return nd; + } + + struct compare_nd { + bool operator()(std::pair const& x, std::pair const& y) const { + return x < y; + } + }; + + /** + * try to substitute for m_v, using array equalities + * + * compute substitution term and aux lits + */ + bool project (expr_ref const& fml) { + app_ref_vector eqs (m); + svector > true_eqs; + + find_arr_eqs (fml, eqs); + TRACE ("qe", + tout << "array equalities:\n"; + for (app * eq : eqs) tout << mk_pp(eq, m) << "\n";); + + // evaluate eqs in M + for (app * eq : eqs) { + TRACE ("qe", tout << "array equality:\n" << mk_pp (eq, m) << "\n"; ); + + if (m_mev->is_false(eq)) { + m_false_sub_v.insert (eq, m.mk_false()); + } + else { + true_eqs.push_back (std::make_pair(get_nesting_depth(eq), eq)); + } + } + std::sort(true_eqs.begin(), true_eqs.end(), compare_nd()); + DEBUG_CODE(for (unsigned i = 0; i + 1 < true_eqs.size(); ++i) SASSERT(true_eqs[i].first <= true_eqs[i+1].first);); + + // search for subst term + for (unsigned i = 0; !m_subst_term_v && i < true_eqs.size(); i++) { + app* eq = true_eqs[i].second; + m_true_sub_v.insert (eq, m.mk_true ()); + // try to find subst term + find_subst_term (eq); + } + + return true; + } + + void mk_result (expr_ref& fml) { + th_rewriter rw(m); + rw (fml); + // add in aux_lits and idx_lits + expr_ref_vector lits (m); + // TODO: eliminate possible duplicates, especially in idx_lits + // theory rewriting is a possibility, but not sure if it + // introduces unwanted terms such as ite's + lits.append (m_idx_lits_v); + lits.append (m_aux_lits_v); + lits.push_back (fml); + fml = mk_and(lits); + + if (m_subst_term_v) { + m_true_sub_v.insert (m_v, m_subst_term_v); + m_true_sub_v (fml); + } + else { + m_true_sub_v (fml); + m_false_sub_v (fml); + } + rw(fml); + SASSERT (!m.is_false (fml)); + } + + public: + + array_project_eqs_util (ast_manager& m): + m (m), + m_arr_u (m), + m_v (m), + m_subst_term_v (m), + m_true_sub_v (m), + m_false_sub_v (m), + m_aux_lits_v (m), + m_idx_lits_v (m), + m_aux_vars (m) + {} + + void operator () (model& mdl, app_ref_vector& arr_vars, expr_ref& fml, app_ref_vector& aux_vars) { + reset (); + model_evaluator mev(mdl); + M = &mdl; + m_mev = &mev; + + unsigned j = 0; + for (unsigned i = 0; i < arr_vars.size (); i++) { + reset_v (); + m_v = arr_vars.get (i); + if (!m_arr_u.is_array (m_v)) { + TRACE ("qe", + tout << "not an array variable: " << mk_pp (m_v, m) << "\n"; + ); + aux_vars.push_back (m_v); + continue; + } + TRACE ("qe", + tout << "projecting equalities on variable: " << mk_pp (m_v, m) << "\n"; + ); + + if (project (fml)) { + mk_result (fml); + + contains_app contains_v (m, m_v); + if (!m_subst_term_v || contains_v (m_subst_term_v)) { + arr_vars[j++] = m_v; + } + TRACE ("qe", + tout << "after projection: \n"; + tout << mk_pp (fml, m) << "\n"; + ); + } + else { + IF_VERBOSE(2, verbose_stream() << "can't project:" << mk_pp(m_v, m) << "\n";); + TRACE ("qe", tout << "Failed to project: " << mk_pp (m_v, m) << "\n";); + arr_vars[j++] = m_v; + } + } + arr_vars.shrink(j); + aux_vars.append (m_aux_vars); + } + }; + + + class array_select_reducer { + ast_manager& m; + array_util m_arr_u; + obj_map m_cache; + expr_ref_vector m_pinned; // to ensure a reference + expr_ref_vector m_idx_lits; + model_ref M; + model_evaluator* m_mev; + th_rewriter m_rw; + ast_mark m_arr_test; + ast_mark m_has_stores; + bool m_reduce_all_selects; + + void reset () { + m_cache.reset (); + m_pinned.reset (); + m_idx_lits.reset (); + M = nullptr; + m_mev = nullptr; + m_arr_test.reset (); + m_has_stores.reset (); + m_reduce_all_selects = false; + } + + bool is_equals (expr *e1, expr *e2) { + return e1 == e2 || (*m_mev)(e1) == (*m_mev)(e2); + } + + bool is_equals (unsigned arity, expr * const* xs, expr * const * ys) { + for (unsigned i = 0; i < arity; ++i) { + if (!is_equals(xs[i], ys[i])) return false; + } + return true; + } + + expr_ref mk_eq(unsigned arity, expr * const* xs, expr * const * ys) { + expr_ref_vector r(m); + for (unsigned i = 0; i < arity; ++i) { + r.push_back(m.mk_eq(xs[i], ys[i])); + } + return mk_and(r); + } + + void add_idx_cond (expr_ref& cond) { + m_rw (cond); + if (!m.is_true (cond)) m_idx_lits.push_back (cond); + } + + bool has_stores (expr* e) { + if (m_reduce_all_selects) return true; + return m_has_stores.is_marked (e); + } + + void mark_stores (app* a, bool args_have_stores) { + if (m_reduce_all_selects) return; + if (args_have_stores || + (m_arr_u.is_store (a) && m_arr_test.is_marked (a->get_arg (0)))) { + m_has_stores.mark (a, true); + } + } + + bool reduce (expr_ref& e) { + if (!is_app (e)) return true; + + expr *r = nullptr; + if (m_cache.find (e, r)) { + e = r; + return true; + } + + ptr_vector todo; + todo.push_back (to_app (e)); + expr_ref_vector args (m); + + while (!todo.empty ()) { + app *a = todo.back (); + unsigned sz = todo.size (); + bool dirty = false; + bool args_have_stores = false; + args.reset(); + for (expr * arg : *a) { + expr *narg = nullptr; + if (!is_app (arg)) { + args.push_back (arg); + } + else if (m_cache.find (arg, narg)) { + args.push_back (narg); + dirty |= (arg != narg); + if (!args_have_stores && has_stores (narg)) { + args_have_stores = true; + } + } + else { + todo.push_back (to_app (arg)); + } + } + + if (todo.size () > sz) continue; + todo.pop_back (); + + if (dirty) { + r = m.mk_app (a->get_decl (), args.size (), args.c_ptr ()); + m_pinned.push_back (r); + } + else { + r = a; + } + + if (m_arr_u.is_select (r) && has_stores (to_app (r)->get_arg (0))) { + r = reduce_core (to_app(r)); + } + else { + mark_stores (to_app (r), args_have_stores); + } + + m_cache.insert (a, r); + } + + SASSERT (r); + e = r; + return true; + } + + expr* reduce_core (app *a) { + if (!m_arr_u.is_store (a->get_arg (0))) return a; + unsigned arity = get_array_arity(m.get_sort(a)); + expr* array = a->get_arg (0); + expr* const* js = a->get_args() + 1; + + while (m_arr_u.is_store (array)) { + a = to_app (array); + expr* const* idxs = a->get_args() + 1; + expr_ref cond = mk_eq(arity, idxs, js); + + if (is_equals (arity, idxs, js)) { + add_idx_cond (cond); + return a->get_arg (2); + } + else { + cond = m.mk_not (cond); + add_idx_cond (cond); + array = a->get_arg (0); + } + } + ptr_vector args; + args.push_back(array); + args.append(arity, js); + expr* r = m_arr_u.mk_select (args.size(), args.c_ptr()); + m_pinned.push_back (r); + return r; + } + + void mk_result (expr_ref& fml) { + // conjoin idx lits + expr_ref_vector lits (m); + lits.append (m_idx_lits); + lits.push_back (fml); + fml = mk_and(lits); + // simplify all trivial expressions introduced + m_rw (fml); + TRACE ("qe", tout << "after reducing selects:\n" << fml << "\n";); + } + + public: + + array_select_reducer (ast_manager& m): + m (m), + m_arr_u (m), + m_pinned (m), + m_idx_lits (m), + m_rw (m), + m_reduce_all_selects (false) + {} + + void operator () (model& mdl, app_ref_vector const& arr_vars, expr_ref& fml, bool reduce_all_selects = false) { + if (!reduce_all_selects && arr_vars.empty ()) return; + + reset (); + model_evaluator mev(mdl); + M = &mdl; + m_mev = &mev; + m_reduce_all_selects = reduce_all_selects; + + // mark vars to eliminate + for (app* v : arr_vars) { + m_arr_test.mark (v, true); + } + + // assume all arr_vars are of array sort + // and assume no store equalities on arr_vars + if (reduce (fml)) { + mk_result (fml); + } + else { + IF_VERBOSE(2, verbose_stream() << "can't project arrays:" << "\n";); + TRACE ("qe", tout << "Failed to project arrays\n";); + } + } + }; + + + class array_project_selects_util { + typedef obj_map*> sel_map; + + struct idx_val { + expr_ref_vector idx, val; + idx_val(expr_ref_vector & idx, expr_ref_vector & val): idx(idx), val(val) {} + idx_val& operator=(idx_val const& o) { idx.reset(); val.reset(); idx.append(o.idx); val.append(o.val); return *this; } + }; + ast_manager& m; + array_util m_arr_u; + arith_util m_ari_u; + sel_map m_sel_terms; + // representative indices for eliminating selects + vector m_idxs; + app_ref_vector m_sel_consts; + expr_ref_vector m_idx_lits; + model_ref M; + model_evaluator* m_mev; + expr_safe_replace m_sub; + ast_mark m_arr_test; + + void reset () { + m_sel_terms.reset (); + m_idxs.reset(); + m_sel_consts.reset (); + m_idx_lits.reset (); + M = nullptr; + m_mev = nullptr; + m_sub.reset (); + m_arr_test.reset (); + } + + /** + * collect sel terms on array vars as given by m_arr_test + */ + void collect_selects (expr* fml) { + if (!is_app (fml)) return; + ast_mark done; + ptr_vector todo; + todo.push_back (to_app (fml)); + for (unsigned i = 0; i < todo.size(); ++i) { + app* a = todo[i]; + if (done.is_marked (a)) continue; + done.mark (a, true); + for (expr* arg : *a) { + if (!done.is_marked (arg) && is_app (arg)) { + todo.push_back (to_app (arg)); + } + } + if (m_arr_u.is_select (a)) { + expr* arr = a->get_arg (0); + if (m_arr_test.is_marked (arr)) { + ptr_vector* lst = m_sel_terms.find (to_app (arr));; + lst->push_back (a); + } + } + } + } + + struct compare_idx { + array_project_selects_util& u; + compare_idx(array_project_selects_util& u):u(u) {} + bool operator()(idx_val const& x, idx_val const& y) { + for (unsigned j = 0; j < x.val.size(); ++j) { + rational xv, yv; + VERIFY (u.m_ari_u.is_numeral(x.val[j], xv)); + VERIFY (u.m_ari_u.is_numeral(y.val[j], yv)); + if (xv < yv) return true; + if (xv > yv) return false; + } + return false; + } + }; + + expr_ref mk_lex_lt(expr_ref_vector const& xs, expr_ref_vector const& ys) { + SASSERT(xs.size() == ys.size()); + expr_ref result(m_ari_u.mk_lt(xs.back(), ys.back()), m); + for (unsigned i = xs.size()-1; i-- > 0; ) { + result = m.mk_or(m_ari_u.mk_lt(xs[i], ys[i]), + m.mk_and(m.mk_eq(xs[i], ys[i]), result)); + } + return result; + } + + /** + * model based ackermannization for sel terms of some array + * + * update sub with val consts for sel terms + */ + void ackermann (ptr_vector const& sel_terms) { + if (sel_terms.empty ()) return; + + expr* v = sel_terms.get (0)->get_arg (0); // array variable + sort* v_sort = m.get_sort (v); + sort* val_sort = get_array_range (v_sort); + unsigned arity = get_array_arity(v_sort); + + for (unsigned i = 0; i < arity; ++i) { + sort* srt = get_array_domain(v_sort, i); + if (!m_ari_u.is_real(srt) && !m_ari_u.is_int(srt)) { + TRACE("qe", tout << "unsupported index sort for Ackerman" << mk_pp(srt, m) << "\n";); + return; + } + } + + unsigned start = m_idxs.size (); // append at the end + + for (app * a : sel_terms) { + expr_ref_vector idxs(m, arity, a->get_args() + 1); + expr_ref_vector vals = (*m_mev)(idxs); + bool is_new = true; + for (unsigned j = start; j < m_idxs.size (); j++) { + if (!is_eq(m_idxs[j].val, vals)) continue; + // idx belongs to the jth equivalence class; + // substitute sel term with ith sel const + expr* c = m_sel_consts.get (j); + m_sub.insert (a, c); + // add equality (idx == repr) + m_idx_lits.push_back (mk_eq (idxs, m_idxs[j].idx)); + is_new = false; + break; + } + if (is_new) { + // new repr, val, and sel const + m_idxs.push_back(idx_val(idxs, vals)); + app_ref c (m.mk_fresh_const ("sel", val_sort), m); + m_sel_consts.push_back (c); + // substitute sel term with new const + m_sub.insert (a, c); + // extend M to include c + expr_ref val = (*m_mev)(a); + M->register_decl (c->get_decl (), val); + } + } + + // sort reprs by their value and add a chain of strict inequalities + + compare_idx cmp(*this); + std::sort(m_idxs.begin() + start, m_idxs.end(), cmp); + + for (unsigned i = start; i < m_idxs.size()-1; i++) { + m_idx_lits.push_back (mk_lex_lt(m_idxs[i].idx, m_idxs[i+1].idx)); + } + } + + void mk_result (expr_ref& fml) { + // conjoin idx lits + m_idx_lits.push_back(fml); + fml = mk_and (m_idx_lits); + + // substitute for sel terms + m_sub (fml); + + TRACE ("qe", tout << "after projection of selects:\n" << fml << "\n";); + } + + /** + * project selects + * populates idx lits and obtains substitution for sel terms + */ + bool project (expr* fml) { + // collect sel terms -- populate the map m_sel_terms + collect_selects (fml); + // model based ackermannization + for (auto & kv : m_sel_terms) { + TRACE ("qe",tout << "ackermann for var: " << mk_pp (kv.m_key, m) << "\n";); + ackermann (*(kv.m_value)); + } + TRACE ("qe", tout << "idx lits:\n" << m_idx_lits; ); + return true; + } + + public: + + array_project_selects_util (ast_manager& m): + m (m), + m_arr_u (m), + m_ari_u (m), + m_sel_consts (m), + m_idx_lits (m), + m_sub (m) + {} + + void operator () (model& mdl, app_ref_vector& arr_vars, expr_ref& fml, app_ref_vector& aux_vars) { + reset (); + model_evaluator mev(mdl); + M = &mdl; + m_mev = &mev; + + // mark vars to eliminate + // alloc empty map from array var to sel terms over it + for (app* v : arr_vars) { + m_arr_test.mark(v, true); + m_sel_terms.insert(v, alloc (ptr_vector)); + } + + // assume all arr_vars are of array sort + // and they only appear in select terms + if (project (fml)) { + mk_result (fml); + aux_vars.append (m_sel_consts); + arr_vars.reset (); + } + else { + IF_VERBOSE(2, verbose_stream() << "can't project arrays:" << "\n";); + TRACE ("qe", tout << "Failed to project arrays\n";); + } + + // dealloc + for (auto & kv : m_sel_terms) dealloc(kv.m_value); + m_sel_terms.reset (); + } + }; + + + static void array_project_eqs (model& mdl, app_ref_vector& arr_vars, expr_ref& fml, app_ref_vector& aux_vars) { + ast_manager& m = arr_vars.get_manager (); + array_project_eqs_util ap (m); + ap (mdl, arr_vars, fml, aux_vars); + } + + static void reduce_array_selects (model& mdl, app_ref_vector const& arr_vars, expr_ref& fml, bool reduce_all_selects) { + ast_manager& m = arr_vars.get_manager (); + array_select_reducer ap (m); + ap (mdl, arr_vars, fml, reduce_all_selects); + } + + static void reduce_array_selects (model& mdl, expr_ref& fml) { + ast_manager& m = fml.get_manager (); + app_ref_vector _tmp (m); + reduce_array_selects (mdl, _tmp, fml, true); + } + + static void array_project_selects (model& mdl, app_ref_vector& arr_vars, expr_ref& fml, app_ref_vector& aux_vars) { + ast_manager& m = arr_vars.get_manager (); + array_project_selects_util ap (m); + ap (mdl, arr_vars, fml, aux_vars); + } + + void new_array_project (model& mdl, app_ref_vector& arr_vars, expr_ref& fml, app_ref_vector& aux_vars, bool reduce_all_selects) { + // 1. project array equalities + array_project_eqs (mdl, arr_vars, fml, aux_vars); + TRACE ("qe", + tout << "Projected array eqs:\n" << fml << "\n"; + tout << "Remaining array vars:\n" << arr_vars; + tout << "Aux vars:\n" << aux_vars; + ); + + // 2. reduce selects + if (reduce_all_selects) { + reduce_array_selects (mdl, fml); + } + else { + reduce_array_selects (mdl, arr_vars, fml, false); + } + TRACE ("qe", + tout << "Reduced selects:\n" << fml << "\n"; + ); + + // 3. project selects using model based ackermannization + array_project_selects (mdl, arr_vars, fml, aux_vars); + TRACE ("qe", + tout << "Projected array selects:\n" << fml << "\n"; + tout << "All aux vars:\n" << aux_vars; + ); + } + };