mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-01 04:48:54 +00:00
Code Activity

add missing registration of lambdas with legacy array solver, add missing beta reduction axiom

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-29 19:13:33 -07:00
parent 8fe2f3c58a
commit 63259d8a43
6 changed files with 50 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.h
View file

@ -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);

11
src/smt/smt_internalizer.cpp
View file

@ -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.
*/

1
src/smt/theory_array.h
View file

@ -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(); }
};

2
src/smt/theory_array_base.cpp
View file

@ -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);

34
src/smt/theory_array_full.cpp
View file

@ -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<expr> 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);
}
}

3
src/smt/theory_array_full.h
View file

@ -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);