mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 11:35:42 +00:00
Code Activity

fixup pattern inference

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-07-14 21:00:56 -07:00
parent 1b39b0e50f
commit 7c8c6a4df0
4 changed files with 60 additions and 56 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -15,6 +15,16 @@ Author:
Revision History:
Rules:
- A pattern can contain a binder (lambda).
- A pattern can occur under a binder
- A pattern cannot contain bound variables
Patterns are down-shifted by number of bound variables in scope to
align with quantifier where pattern is associated.
--*/
#include "util/warning.h"
@ -173,11 +183,13 @@ inline void pattern_inference_cfg::collect::save(expr * n, unsigned delta, info
void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
switch (n->get_kind()) {
case AST_VAR: {
uint_set free_vars;
uint_set free_vars, bound_vars;
unsigned idx = to_var(n)->get_idx();
if (delta <= idx && idx < m_num_bindings + delta)
free_vars.insert(idx - delta);
info * i = alloc(info, m, n, free_vars, 1);
else if (idx < delta)
bound_vars.insert(idx);
info * i = alloc(info, free_vars, bound_vars, 1);
save(n, delta, i);
return;
}
@ -190,55 +202,38 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
}
if (c->get_num_args() == 0) {
save(n, delta, alloc(info, m, n, uint_set(), 1));
save(n, delta, alloc(info, uint_set(), uint_set(), 1));
return;
}
ptr_buffer<expr> buffer;
bool changed = false; // false if none of the children is mapped to a node different from itself.
uint_set free_vars;
uint_set free_vars, bound_vars;
unsigned size = 1;
unsigned num = c->get_num_args();
for (unsigned i = 0; i < num; ++i) {
expr * child = c->get_arg(i);
for (expr *child : *c) {
info * child_info = nullptr;
#ifdef Z3DEBUG
bool found =
#endif
m_cache.find(entry(child, delta), child_info);
SASSERT(found);
if (child_info == nullptr) {
VERIFY(m_cache.find(entry(child, delta), child_info));
if (!child_info) {
save(n, delta, nullptr);
return;
}
buffer.push_back(child_info->m_node.get());
free_vars |= child_info->m_free_vars;
size += child_info->m_size;
if (child != child_info->m_node.get())
changed = true;
free_vars |= child_info->m_free_vars;
bound_vars |= child_info->m_bound_vars;
size += child_info->m_size;
}
app * new_node = nullptr;
if (changed)
new_node = m.mk_app(decl, buffer.size(), buffer.data());
else
new_node = to_app(n);
save(n, delta, alloc(info, m, new_node, free_vars, size));
save(n, delta, alloc(info, free_vars, bound_vars, size));
// Remark: arithmetic patterns are only used if they are nested inside other terms.
// That is, we never consider x + 1 as pattern. On the other hand, f(x+1) can be a pattern
// if arithmetic is not in the forbidden list.
//
// Remark: The rule above has an exception. The operators (div, idiv, mod) are allowed to be
// used as patterns even when they are not nested in other terms. The motivation is that
// Z3 currently doesn't implement them (i.e., they are uninterpreted). So, some users add axioms
// stating properties about these operators.
// if arithmetic is not in the forbidden list.
family_id fid = c->get_family_id();
decl_kind k = c->get_decl_kind();
if (!free_vars.empty() &&
delta == 0 &&
bound_vars.empty() &&
(fid != m_afid || (fid == m_afid && !m_owner.m_nested_arith_only && (k == OP_DIV || k == OP_IDIV || k == OP_MOD || k == OP_REM || k == OP_MUL)))) {
TRACE(pattern_inference, tout << "potential candidate: \n" << mk_pp(new_node, m) << "\n";);
m_owner.add_candidate(new_node, free_vars, size);
TRACE(pattern_inference, tout << "potential candidate: \n" << mk_pp(n, m) << "\n";);
inv_var_shifter sh(m);
expr_ref r(m);
sh(n, delta, r);
m_owner.add_candidate(to_app(r), free_vars, size);
}
return;
}
@ -252,13 +247,12 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
save(n, delta, nullptr);
return;
}
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));
uint_set bound_vars;
for (auto b : body_info->m_bound_vars)
if (b >= num_decls)
bound_vars.insert(b - num_decls);
save(n, delta, alloc(info, body_info->m_free_vars, bound_vars, body_info->m_size + 1));
return;
}
default:

7
src/ast/pattern/pattern_inference.h
View file

@ -125,11 +125,10 @@ class pattern_inference_cfg : public default_rewriter_cfg {
};
struct info {
expr_ref m_node;
uint_set m_free_vars;
uint_set m_free_vars, m_bound_vars;
unsigned m_size;
info(ast_manager & m, expr * n, uint_set const & vars, unsigned sz):
m_node(n, m), m_free_vars(vars), m_size(sz) {}
info(uint_set const & fvars, uint_set const& bvars, unsigned sz):
m_free_vars(fvars), m_bound_vars(bvars), m_size(sz) {}
};
ast_manager & m;

2
src/ast/rewriter/rewriter.cpp
View file

@ -396,7 +396,7 @@ void var_shifter::process_var(var * v) {
}
void inv_var_shifter::operator()(expr * t, unsigned shift, expr_ref & r) {
if (is_ground(t)) {
if (is_ground(t) || shift == 0) {
r = t;
return;
}

29
src/smt/theory_array_base.cpp
View file

@ -865,16 +865,27 @@ namespace smt {
for (auto [r, s1] : m_selects) {
for (auto n : *r) {
if (!ctx.is_relevant(n) || !is_store(n))
if (false && !ctx.is_relevant(n))
continue;
auto st = n->get_arg(0)->get_root();
if (!ctx.is_relevant(st))
continue;
auto & s2 = m_selects[st];
if (!check_selects(n, *s1, *s2))
return false;
if (!check_selects(n, *s2, *s1))
return false;
if (is_store(n)) {
auto st = n->get_arg(0)->get_root();
auto &s2 = m_selects[st];
if (!check_selects(n, *s1, *s2))
return false;
if (!check_selects(n, *s2, *s1))
return false;
}
if (is_const(n)) {
auto v = n->get_arg(0)->get_root();
for (auto sel : *s1) {
if (v != sel->get_root()) {
verbose_stream() << pp(n, m) << " != " << pp(sel, m) << "\n";
return false;
}
}
}
}
}
return true;