mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 11:26:21 +00:00
Code Activity

detect quantifiers in patterns

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-05-21 10:37:15 -07:00
parent af7a4de258
commit af33dfaa7d
2 changed files with 26 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -254,6 +254,27 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
}
return;
}
case AST_QUANTIFIER: {
quantifier * q = to_quantifier(n);
unsigned num_decls = q->get_num_decls();
info * body_info = nullptr;
m_cache.find(entry(q->get_expr(), delta + num_decls), body_info);
if (body_info == nullptr) {
save(n, delta, nullptr);
return;
}
// The lambda/quantifier itself is a valid sub-term in a pattern.
// Propagate the free variables from the body (they already refer
// to the outer quantifier's bindings) and keep the node as-is.
expr * new_body = body_info->m_node.get();
quantifier_ref new_q(m);
if (new_body != q->get_expr())
new_q = m.update_quantifier(q, new_body);
else
new_q = q;
save(n, delta, alloc(info, m, new_q, body_info->m_free_vars, body_info->m_size + 1));
return;
}
default:
save(n, delta, nullptr);
return;

6
src/ast/rewriter/rewriter_def.h
View file

@ -561,9 +561,13 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
expr * const * np = it + 1;
expr * const * nnp = np + num_pats;
unsigned j = 0;
for (unsigned i = 0; i < num_pats; ++i)
for (unsigned i = 0; i < num_pats; ++i) {
if (m_manager.is_pattern(np[i]))
new_pats[j++] = np[i];
else {
IF_VERBOSE(10, verbose_stream() << "[rewriter] dropping pattern (is_pattern check failed) for qid=" << q->get_qid() << " pattern[" << i << "]: " << mk_ismt2_pp(np[i], m_manager, 3) << "\n";);
}
}
new_pats.shrink(j);
num_pats = j;
j = 0;