mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-05 00:20:50 +00:00
Code Activity

move closure conversion to solver internalization

Browse source 
- only the internalizer performs closure conversion
- theory_array treats propagation of lambdas similar to stores
- ho_matcher treats top-level flex patterns as first-order
- pattern-inference fix to handle quantifiers (lambdas) in patterns that are computed
This commit is contained in:
Nikolaj Bjorner 2026-05-30 18:41:37 -07:00
parent 2cc4422018
commit dbe986fdf7
10 changed files with 97 additions and 87 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/ast/euf/ho_matcher.cpp
View file

@ -689,20 +689,21 @@ namespace euf {
});
if (!is_ho)
return { q, p };
ptr_vector<expr> todo;
vector<std::pair<expr*, unsigned>> todo;
ptr_buffer<var> bound;
expr_ref_vector cache(m);
unsigned nb = q->get_num_decls();
bool contains_pat2abs = m_pat2abs.contains(p);
todo.push_back(p);
SASSERT(m.is_pattern(p));
todo.push_back({p, 0});
while (!todo.empty()) {
auto t = todo.back();
auto [t, lvl] = todo.back();
if (is_var(t)) {
cache.setx(t->get_id(), t);
todo.pop_back();
continue;
}
if (m_unitary.is_flex(0, t) || m.is_lambda_def(t) || is_lambda(t)) {
if ((m_unitary.is_flex(0, t) && lvl > 1) || m.is_lambda_def(t) || is_lambda(t)) {
if (!contains_pat2abs)
m_pat2abs.insert_if_not_there(p, svector<std::pair<unsigned, expr*>>()).push_back({ nb, t });
auto v = m.mk_var(nb++, t->get_sort());
@ -720,7 +721,7 @@ namespace euf {
cache.reserve(arg->get_id() + 1);
expr* arg1 = cache.get(arg->get_id());
if (!arg1)
todo.push_back(arg);
todo.push_back({arg, lvl + 1});
else
args.push_back(arg1);
}
@ -736,6 +737,9 @@ namespace euf {
}
}
p1 = to_app(cache.get(p->get_id()));
if (p1 == p)
return {q, p};
expr_free_vars free_vars;
free_vars(p1);
app_ref_vector new_ground(m);
@ -762,6 +766,8 @@ namespace euf {
auto body = q->get_expr();
if (!new_patterns.empty()) {
ptr_vector<app> pats;
CTRACE(ho_matching, !m.is_pattern(p1),
tout << mk_pp(p, m) << "\n" << mk_pp(p1, m) << "\n";);
VERIFY(m.is_pattern(p1, pats));
for (auto p : new_patterns) // patterns for variables that are not free in new pattern
pats.push_back(p);
@ -800,6 +806,10 @@ namespace euf {
if (!contains_pat2abs)
trail().push(insert_map(m_pat2abs, p));
TRACE(ho_matching, tout << mk_pp(q, m) << "\n"
<< mk_pp(p, m) << "\n->\n"
<< mk_pp(q1, m) << "\n"
<< mk_pp(p1, m) << "\n");
return { q1, p1 };
}

38
src/ast/normal_forms/defined_names.cpp
View file

@ -193,43 +193,7 @@ void defined_names::impl::mk_definition(expr * e, app * n, sort_ref_buffer & var
else if (m.is_term_ite(e)) {
bound_vars(var_sorts, var_names, MK_OR(MK_NOT(to_app(e)->get_arg(0)), MK_EQ(n, to_app(e)->get_arg(1))), n, defs);
bound_vars(var_sorts, var_names, MK_OR(to_app(e)->get_arg(0), MK_EQ(n, to_app(e)->get_arg(2))), n, defs);
}
else if (is_lambda(e)) {
// n(y) = \x . M[x,y]
// =>
// n(y)[x] = M, forall x y
//
// NB. The pattern is incomplete.
// consider store(a, i, v) == \lambda j . if i = j then v else a[j]
// the instantiation rules for store(a, i, v) are:
// store(a, i, v)[j] = if i = j then v else a[j] with patterns {a[j], store(a, i, v)} { store(a, i, v)[j] }
// The first pattern is not included.
// TBD use a model-based scheme for extracting instantiations instead of
// using multi-patterns.
//
quantifier* q = to_quantifier(e);
expr_ref_vector args(m);
expr_ref n2(m), n3(m);
var_shifter vs(m);
vs(n, q->get_num_decls(), n2);
args.push_back(n2);
var_sorts.append(q->get_num_decls(), q->get_decl_sorts());
var_names.append(q->get_num_decls(), q->get_decl_names());
for (unsigned i = 0; i < q->get_num_decls(); ++i) {
args.push_back(m.mk_var(q->get_num_decls() - i - 1, q->get_decl_sort(i)));
}
array_util autil(m);
func_decl * f = nullptr;
if (autil.is_as_array(n2, f)) {
n3 = m.mk_app(f, args.size()-1, args.data() + 1);
}
else {
n3 = autil.mk_select(args.size(), args.data());
}
bound_vars(var_sorts, var_names, MK_EQ(q->get_expr(), n3), to_app(n3), defs, m.lambda_def_qid());
}
}
else {
bound_vars(var_sorts, var_names, MK_EQ(e, n), n, defs);
}

4
src/ast/normal_forms/name_exprs.cpp
View file

@ -100,7 +100,7 @@ class name_quantifier_labels : public name_exprs_core {
public:
pred(ast_manager & m):m(m) {}
bool operator()(expr * t) override {
return is_quantifier(t) || m.is_label(t);
return (is_quantifier(t) && !is_lambda(t)) || m.is_label(t);
}
};
@ -127,7 +127,7 @@ class name_nested_formulas : public name_exprs_core {
TRACE(name_exprs, tout << "name_nested_formulas::pred:\n" << mk_ismt2_pp(t, m) << "\n";);
if (is_app(t))
return to_app(t)->get_family_id() == m.get_basic_family_id() && to_app(t)->get_num_args() > 0 && t != m_root;
return m.is_label(t) || is_quantifier(t);
return m.is_label(t) || (is_quantifier(t) && !is_lambda(t));
}
};

2
src/ast/pattern/pattern_inference.cpp
View file

@ -384,6 +384,8 @@ bool pattern_inference_cfg::contains_subpattern::operator()(expr * n) {
break;
case AST_VAR:
break;
case AST_QUANTIFIER:
break;
default:
UNREACHABLE();
}

17
src/smt/smt_internalizer.cpp
View file

@ -598,19 +598,7 @@ namespace smt {
if (e_internalized(q))
return;
app_ref lam_name(m.mk_fresh_const("lambda", q->get_sort()), m);
app_ref eq(m), lam_app(m);
expr_ref_vector vars(m);
vars.push_back(lam_name);
unsigned sz = q->get_num_decls();
for (unsigned i = 0; i < sz; ++i)
vars.push_back(m.mk_var(sz - i - 1, q->get_decl_sort(i)));
array_util autil(m);
lam_app = autil.mk_select(vars.size(), vars.data());
eq = m.mk_eq(lam_app, q->get_expr());
quantifier_ref fa(m);
expr * patterns[1] = { m.mk_pattern(lam_app) };
fa = m.mk_forall(sz, q->get_decl_sorts(), q->get_decl_names(), eq, 0, m.lambda_def_qid(), symbol::null, 1, patterns);
internalize_quantifier(fa, true);
m.add_lambda_def(lam_name->get_decl(), q);
if (!e_internalized(lam_name))
internalize_uninterpreted(lam_name);
enode* lam_node = get_enode(lam_name);
@ -619,9 +607,6 @@ namespace smt {
m_app2enode.setx(q->get_id(), lam_node, nullptr);
m_l_internalized_stack.push_back(q);
m_trail_stack.push_ptr(&m_mk_lambda_trail);
bool_var bv = get_bool_var(fa);
assign(literal(bv, false), nullptr);
mark_as_relevant(bv);
}
bool context::has_lambda() {

22
src/smt/theory_array.cpp
View file

@ -68,12 +68,12 @@ namespace smt {
m_var_data.push_back(alloc(var_data));
var_data * d = m_var_data[r];
TRACE(array, tout << mk_bounded_pp(n->get_expr(), m) << "\nis_array: " << is_array_sort(n) << ", is_select: " << is_select(n) <<
", is_store: " << is_store(n) << "\n";);
", is_store: " << is_store(n) << ", is_lambda: " << is_lambda(n) << "\n";);
d->m_is_array = is_array_sort(n);
if (d->m_is_array)
register_sort(n->get_expr()->get_sort());
d->m_is_select = is_select(n);
if (is_store(n))
if (is_store(n) || is_lambda(n))
d->m_stores.push_back(n);
ctx.attach_th_var(n, this, r);
if (laziness() <= 1 && is_store(n))
@ -95,7 +95,7 @@ namespace smt {
if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
for (enode* store : d->m_parent_stores) {
SASSERT(is_store(store));
SASSERT(is_store(store) || is_lambda(store));
if (!m_params.m_array_cg || store->is_cgr()) {
instantiate_axiom2b(s, store);
}
@ -106,7 +106,7 @@ namespace smt {
void theory_array::add_parent_store(theory_var v, enode * s) {
if (m_params.m_array_cg && !s->is_cgr())
return;
SASSERT(is_store(s));
SASSERT(is_store(s) || is_lambda(s));
v = find(v);
var_data * d = m_var_data[v];
d->m_parent_stores.push_back(s);
@ -177,7 +177,7 @@ namespace smt {
void theory_array::add_store(theory_var v, enode * s) {
if (m_params.m_array_cg && !s->is_cgr())
return;
SASSERT(is_store(s));
SASSERT(is_store(s) || is_lambda(s));
v = find(v);
var_data * d = m_var_data[v];
unsigned lambda_equiv_class_size = get_lambda_equiv_size(v, d);
@ -204,7 +204,7 @@ namespace smt {
void theory_array::instantiate_axiom2a(enode * select, enode * store) {
TRACE(array, tout << "axiom 2a: #" << select->get_owner_id() << " #" << store->get_owner_id() << "\n";);
SASSERT(is_select(select));
SASSERT(is_store(store));
SASSERT(is_store(store) || is_lambda(store));
if (assert_store_axiom2(store, select))
m_stats.m_num_axiom2a++;
}
@ -212,7 +212,7 @@ namespace smt {
bool theory_array::instantiate_axiom2b(enode * select, enode * store) {
TRACE(array_axiom2b, tout << "axiom 2b: #" << select->get_owner_id() << " #" << store->get_owner_id() << "\n";);
SASSERT(is_select(select));
SASSERT(is_store(store));
SASSERT(is_store(store) || is_lambda(store));
if (assert_store_axiom2(store, select)) {
m_stats.m_num_axiom2b++;
return true;
@ -261,7 +261,7 @@ namespace smt {
}
bool theory_array::internalize_term(app * n) {
if (!is_store(n) && !is_select(n)) {
if (!is_store(n) && !is_select(n) && !is_lambda(n)) {
if (!is_array_ext(n))
found_unsupported_op(n);
return false;
@ -282,7 +282,7 @@ namespace smt {
if (is_select(n)) {
add_parent_select(v_arg, ctx.get_enode(n));
}
else if (is_store(n)) {
else if (is_store(n) || is_lambda(n)) {
add_parent_store(v_arg, ctx.get_enode(n));
}
}
@ -325,9 +325,11 @@ namespace smt {
if (m.is_ite(n)) {
TRACE(array, tout << "relevant ite " << mk_pp(n, m) << "\n";);
}
if (!is_store(n) && !is_select(n))
if (!is_store(n) && !is_select(n) && !is_lambda(n))
return;
if (!ctx.e_internalized(n)) ctx.internalize(n, false);
if (is_lambda(n))
return;
enode * arg = ctx.get_enode(to_app(n)->get_arg(0));
theory_var v_arg = arg->get_th_var(get_id());
SASSERT(v_arg != null_theory_var);

32
src/smt/theory_array_base.cpp
View file

@ -217,18 +217,41 @@ namespace smt {
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
}
void theory_array_base::assert_lambda_axiom_core(enode* n, enode* select) {
SASSERT(is_lambda(n));
SASSERT(is_select(select));
expr *e = n->get_expr();
app *s = select->get_app();
auto q = is_quantifier(e) ? to_quantifier(e) : m.is_lambda_def(e);
SASSERT(q);
SASSERT(::is_lambda(q));
SASSERT(q->get_num_decls() == s->get_num_args() - 1);
// do the same thing as in sat/smt/array_axioms:
ptr_vector<expr> args(s->get_num_args(), s->get_args());
args[0] = q;
array_util a(m);
expr_ref alpha(a.mk_select(args), m);
expr_ref beta(alpha);
ctx.get_rewriter()(beta);
TRACE(array, tout << alpha << " == " << beta << "\n";);
auto alpha_n = ensure_enode(alpha);
auto beta_n = ensure_enode(beta);
ctx.assign_eq(alpha_n, beta_n, eq_justification::mk_axiom());
}
bool theory_array_base::assert_store_axiom2(enode * store, enode * select) {
SASSERT(is_store(store) || is_lambda(store));
unsigned num_args = select->get_num_args();
unsigned i = 1;
for (; i < num_args; ++i)
if (store->get_arg(i)->get_root() != select->get_arg(i)->get_root())
if (is_store(store) && store->get_arg(i)->get_root() != select->get_arg(i)->get_root())
break;
if (i == num_args)
return false;
if (ctx.add_fingerprint(store, store->get_owner_id(), select->get_num_args() - 1, select->get_args() + 1)) {
TRACE(array, tout << "adding axiom2 to todo queue\n";);
m_axiom2_todo.push_back(std::make_pair(store, select));
m_axiom2_todo.push_back({store, select});
return true;
}
TRACE(array, tout << "axiom already instantiated: #" << store->get_owner_id() << " #" << select->get_owner_id() << "\n";);
@ -426,7 +449,10 @@ namespace smt {
m_axiom1_todo.reset();
for (unsigned i = 0; i < m_axiom2_todo.size(); ++i) {
auto [store, select] = m_axiom2_todo[i];
assert_store_axiom2_core(store, select);
if (is_store(store))
assert_store_axiom2_core(store, select);
else
assert_lambda_axiom_core(store, select);
}
m_axiom2_todo.reset();
for (unsigned i = 0; i < m_extensionality_todo.size(); ++i) {

11
src/smt/theory_array_base.h
View file

@ -46,6 +46,10 @@ namespace smt {
bool is_choice(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_CHOICE); }
bool is_array_sort(sort const* s) const { return s->is_sort_of(get_id(), ARRAY_SORT); }
bool is_array_sort(expr const* n) const { return is_array_sort(n->get_sort()); }
bool is_lambda(expr *n) const {
return m.is_lambda_def(n) || ::is_lambda(n);
}
bool is_store(enode const * n) const { return is_store(n->get_expr()); }
bool is_map(enode const* n) const { return is_map(n->get_expr()); }
@ -55,6 +59,12 @@ namespace smt {
bool is_choice(enode const* n) const { return is_choice(n->get_expr()); }
bool is_default(enode const* n) const { return is_default(n->get_expr()); }
bool is_array_sort(enode const* n) const { return is_array_sort(n->get_sort()); }
bool is_lambda(enode const *n) const {
return is_lambda(n->get_expr());
}
bool is_select_arg(enode* r);
app * mk_select(unsigned num_args, expr * const * args);
@ -76,6 +86,7 @@ namespace smt {
void assert_axiom(literal l);
void assert_store_axiom1_core(enode * n);
void assert_store_axiom2_core(enode * store, enode * select);
void assert_lambda_axiom_core(enode *lambda, enode *select);
void assert_store_axiom1(enode * n) { m_axiom1_todo.push_back(n); }
bool assert_store_axiom2(enode * store, enode * select);

34
src/smt/theory_array_full.cpp
View file

@ -248,7 +248,7 @@ namespace smt {
instantiate_default_as_array_axiom(n);
d->m_as_arrays.push_back(n);
}
else if (m.is_lambda_def(n->get_expr())) {
else if (is_lambda(n)) {
instantiate_default_lambda_def_axiom(n);
d->m_lambdas.push_back(n);
m_lambdas.push_back(n);
@ -329,9 +329,6 @@ namespace smt {
ctx.push_trail(push_back_vector(m_as_array));
instantiate_default_as_array_axiom(node);
}
else if (is_choice(n)) {
instantiate_choice_axiom(node);
}
else if (is_array_ext(n)) {
SASSERT(n->get_num_args() == 2);
instantiate_extensionality(ctx.get_enode(n->get_arg(0)), ctx.get_enode(n->get_arg(1)));
@ -371,8 +368,8 @@ namespace smt {
TRACE(array, tout << "v" << v << " " << pp(get_enode(v), m) << " "
<< d->m_prop_upward << " " << m_params.m_array_delay_exp_axiom << "\n";);
for (enode * store : d->m_stores) {
SASSERT(is_store(store));
instantiate_default_store_axiom(store);
if (is_store(store))
instantiate_default_store_axiom(store);
}
if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
@ -410,7 +407,7 @@ namespace smt {
TRACE(array, tout << mk_pp(n, m) << "\n";);
theory_array::relevant_eh(n);
if (!is_default(n) && !is_select(n) && !is_map(n) &&
!is_const(n) && !is_as_array(n) && !is_choice(n) && !is_lambda(n)){
!is_const(n) && !is_as_array(n) && !is_choice(n)) {
return;
}
ctx.ensure_internalized(n);
@ -447,10 +444,8 @@ namespace smt {
instantiate_default_as_array_axiom(node);
}
else if (is_choice(n)) {
instantiate_choice_axiom(node);
}
else if (is_lambda(n)) {
NOT_IMPLEMENTED_YET();
m_choice_terms.push_back(node);
ctx.push_trail(push_back_vector(m_choice_terms));
}
}
@ -585,7 +580,7 @@ namespace smt {
m_stats.m_num_default_lambda_axiom++;
expr* e = arr->get_expr();
expr_ref def(mk_default(e), m);
quantifier* lam = m.is_lambda_def(e);
quantifier* lam = is_quantifier(e) ? to_quantifier(e) : m.is_lambda_def(e);
TRACE(array, tout << mk_pp(lam, m) << "\n" << mk_pp(e, m) << "\n");
expr_ref_vector args(m);
var_subst subst(m, false);
@ -627,8 +622,9 @@ namespace smt {
symbol x_name("x");
expr_ref q(m.mk_forall(1, &x_sort, &x_name, ax), m);
ctx.get_rewriter()(q);
literal l = mk_literal(q);
assert_axiom(l);
TRACE(array, tout << "choice " << q << "\n");
ctx.assert_expr(q);
ctx.internalize_assertions();
return true;
}
@ -783,6 +779,16 @@ namespace smt {
return {eps, diag};
}
void theory_array_full::propagate() {
if (m_choice_qhead == m_choice_terms.size())
return;
ctx.push_trail(value_trail(m_choice_qhead));
for (; m_choice_qhead < m_choice_terms.size(); ++m_choice_qhead) {
enode *choice = m_choice_terms[m_choice_qhead];
instantiate_choice_axiom(choice);
}
}
final_check_status theory_array_full::assert_delayed_axioms() {
final_check_status r = FC_DONE;
if (!m_params.m_array_delay_exp_axiom) {

4
src/smt/theory_array_full.h
View file

@ -37,6 +37,8 @@ namespace smt {
ast2ast_trailmap<sort, app> m_sort2epsilon;
ast2ast_trailmap<sort, func_decl> m_sort2diag;
obj_pair_map<expr, expr, bool> m_eqs;
enode_vector m_choice_terms;
unsigned m_choice_qhead = 0;
static unsigned const m_default_map_fingerprint = UINT_MAX - 112;
static unsigned const m_default_store_fingerprint = UINT_MAX - 113;
@ -111,6 +113,8 @@ namespace smt {
void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var) override;
void display_var(std::ostream & out, theory_var v) const override;
void collect_statistics(::statistics & st) const override;
bool can_propagate() override { return theory_array::can_propagate() || m_choice_qhead < m_choice_terms.size(); }
void propagate() override;
};
};