diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 1aaecf736c..559b329b05 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -882,6 +882,8 @@ namespace smt { void apply_sort_cnstr(app * term, enode * e); + void apply_sort_cnstr(quantifier *term, enode *e); + bool simplify_aux_clause_literals(unsigned & num_lits, literal * lits, literal_buffer & simp_lits); bool simplify_aux_lemma_literals(unsigned & num_lits, literal * lits); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 063b7297b7..59d10e1c3e 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -597,9 +597,10 @@ namespace smt { SASSERT(is_lambda(q)); if (e_internalized(q)) return; - mk_enode(q, true, /* do suppress args */ + auto e = mk_enode(q, true, /* do suppress args */ false, /* it is a term, so it should not be merged with true/false */ true); + apply_sort_cnstr(q, e); } bool context::has_lambda() { @@ -1092,6 +1093,14 @@ namespace smt { } } + void context::apply_sort_cnstr(quantifier *lambda_term, enode *e) { + sort *s = lambda_term->get_sort(); + theory *th = m_theories.get_plugin(s->get_family_id()); + if (th) { + th->apply_sort_cnstr(e, s); + } + } + /** \brief Return the literal associated with n. */ diff --git a/src/smt/theory_array.h b/src/smt/theory_array.h index d6ce0f4b9f..88f5678aea 100644 --- a/src/smt/theory_array.h +++ b/src/smt/theory_array.h @@ -29,6 +29,7 @@ namespace smt { unsigned m_num_map_axiom, m_num_default_map_axiom; unsigned m_num_select_const_axiom, m_num_default_store_axiom, m_num_default_const_axiom, m_num_default_as_array_axiom; unsigned m_num_select_as_array_axiom, m_num_default_lambda_axiom, m_num_choice_axiom; + unsigned m_num_select_lambda_axiom; void reset() { memset(this, 0, sizeof(theory_array_stats)); } theory_array_stats() { reset(); } }; diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 428c134087..19e89bd656 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -534,6 +534,7 @@ namespace smt { unsigned num_vars = get_num_vars(); for (unsigned i = 0; i < num_vars; ++i) { enode * n = get_enode(i); + TRACE(array, tout << enode_pp(n, ctx) << " is_relevant: " << ctx.is_relevant(n) << " is_array: " << is_array_sort(n) << "\n";); if (!ctx.is_relevant(n) || !is_array_sort(n)) { continue; } @@ -580,6 +581,7 @@ namespace smt { sort * s2 = n2->get_sort(); if (s1 == s2 && !ctx.is_diseq(n1, n2)) { app_ref eq = app_ref(mk_eq_atom(n1->get_expr(), n2->get_expr()), m); + TRACE(array_bug, tout << "mk_interface_eqs: adding: " << eq << "\n";); if (!ctx.b_internalized(eq.get()) || !ctx.is_relevant(eq.get())) { result++; ctx.internalize(eq, true); diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 137359841e..e00f4cff93 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -393,6 +393,10 @@ namespace smt { SASSERT(is_map(map)); instantiate_select_map_axiom(s, map); } + for (enode *lam : d_full->m_lambdas) { + SASSERT(is_lambda(lam->get_expr())); + instantiate_select_lambda_axiom(s, lam); + } if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) { for (enode * map : d_full->m_parent_maps) { SASSERT(is_map(map)); @@ -468,7 +472,6 @@ namespace smt { SASSERT(map->get_num_args() > 0); func_decl* f = to_func_decl(map->get_decl()->get_parameter(0).get_ast()); - TRACE(array_map_bug, tout << "invoked instantiate_select_map_axiom\n"; tout << sl->get_owner_id() << " " << mp->get_owner_id() << "\n"; tout << mk_ismt2_pp(sl->get_expr(), m) << "\n" << mk_ismt2_pp(mp->get_expr(), m) << "\n";); @@ -518,6 +521,34 @@ namespace smt { return try_assign_eq(sel1, sel2); } + bool theory_array_full::instantiate_select_lambda_axiom(enode* sl, enode* lambda) { + app* select = sl->get_app(); + SASSERT(is_select(select)); + SASSERT(is_lambda(lambda->get_expr())); + SASSERT(lambda->get_sort() == sl->get_arg(0)->get_sort()); + + if (!ctx.add_fingerprint(lambda, lambda->get_owner_id(), sl->get_num_args() - 1, sl->get_args() + 1)) { + return false; + } + + m_stats.m_num_select_lambda_axiom++; + + unsigned num_args = select->get_num_args(); + ptr_buffer args; + args.push_back(lambda->get_expr()); + for (unsigned i = 1; i < num_args; ++i) + args.push_back(select->get_arg(i)); + + expr_ref sel1(m), sel2(m); + sel1 = mk_select(args.size(), args.data()); + sel2 = sel1; + ctx.get_rewriter()(sel2); + ctx.internalize(sel1, false); + ctx.internalize(sel2, false); + TRACE(array, tout << mk_bounded_pp(sel1, m) << "\n==\n" << mk_bounded_pp(sel2, m) << "\n";); + return try_assign_eq(sel1, sel2); + } + // // @@ -881,6 +912,7 @@ namespace smt { st.update("array def as-array", m_stats.m_num_default_as_array_axiom); st.update("array sel as-array", m_stats.m_num_select_as_array_axiom); st.update("array def lambda", m_stats.m_num_default_lambda_axiom); + st.update("array sel lambda", m_stats.m_num_select_lambda_axiom); st.update("array choice ax", m_stats.m_num_choice_axiom); } } diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h index f66762e6b8..9dae2dcb96 100644 --- a/src/smt/theory_array_full.h +++ b/src/smt/theory_array_full.h @@ -83,7 +83,7 @@ namespace smt { bool instantiate_default_map_axiom(enode* map); bool instantiate_default_as_array_axiom(enode* arr); bool instantiate_default_lambda_def_axiom(enode* arr); - bool instantiate_select_lambda_axiom(enode *lambda); + bool instantiate_choice_axiom(enode* ch); bool instantiate_parent_stores_default(theory_var v); @@ -96,6 +96,7 @@ namespace smt { bool instantiate_select_const_axiom(enode* select, enode* cnst); bool instantiate_select_as_array_axiom(enode* select, enode* arr); bool instantiate_select_map_axiom(enode* select, enode* map); + bool instantiate_select_lambda_axiom(enode *select, enode *lambda); bool instantiate_axiom_map_for(theory_var v);