mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

fix pattern inference to deal with binders properly, pin sorts in tptp_frontend

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-07-08 15:29:05 -07:00
parent 965db51b5c
commit c56b2cbaa4
3 changed files with 22 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -121,6 +121,7 @@ void pattern_inference_cfg::collect::operator()(expr * n, unsigned num_bindings)
SASSERT(m_info.empty());
SASSERT(m_todo.empty());
SASSERT(m_cache.empty());
SASSERT(is_well_sorted(m, n));
m_num_bindings = num_bindings;
m_todo.push_back(entry(n, 0));
while (!m_todo.empty()) {
@ -173,21 +174,15 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
switch (n->get_kind()) {
case AST_VAR: {
unsigned idx = to_var(n)->get_idx();
if (idx >= delta) {
idx = idx - delta;
uint_set free_vars;
if (idx < m_num_bindings)
free_vars.insert(idx);
info * i = nullptr;
if (delta == 0)
i = alloc(info, m, n, free_vars, 1);
else
i = alloc(info, m, m.mk_var(idx, to_var(n)->get_sort()), free_vars, 1);
save(n, delta, i);
}
else {
if (idx >= m_num_bindings + delta) {
save(n, delta, nullptr);
return;
}
uint_set free_vars;
if (delta <= idx)
free_vars.insert(idx - delta);
info * i = alloc(info, m, n, free_vars, 1);
save(n, delta, i);
return;
}
case AST_APP: {
@ -243,7 +238,8 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
// stating properties about these operators.
family_id fid = c->get_family_id();
decl_kind k = c->get_decl_kind();
if (!free_vars.empty() &&
if (!free_vars.empty() &&
delta == 0 &&
(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);
@ -254,30 +250,15 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
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) {
expr *body = q->get_expr();
m_cache.find(entry(body, delta + num_decls), body_info);
if (!body_info) {
save(n, delta, nullptr);
return;
}
// The lambda/quantifier itself is a valid sub-term in a pattern.
// body_info->m_node was normalized into the *outer* quantifier's de
// Bruijn space (the enclosing binders, including this lambda's own
// num_decls binders, were stripped). Re-wrapping it under the lambda
// therefore requires shifting the (outer) free variables back up by
// num_decls so they do not collide with the lambda's bound variables.
// The lambda's own bound variables never occur in body_info (any
// sub-term referring to them was rejected as a candidate), so the
// shift is always sound.
expr * body = body_info->m_node.get();
expr_ref new_body(m);
if (num_decls > 0) {
var_shifter shift(m);
shift(body, num_decls, new_body);
}
else
new_body = body;
expr *new_body = body_info->m_node.get();
quantifier_ref new_q(m);
if (new_body.get() != q->get_expr())
if (new_body != q->get_expr())
new_q = m.update_quantifier(q, new_body);
else
new_q = q;

12
src/cmd_context/tptp_frontend.cpp
View file

@ -553,10 +553,9 @@ class tptp_parser {
// Multi-argument A * B > C is represented as Array(A, Array(B, C)) (curried).
sort* get_ho_sort(ptr_vector<sort> const& domain, sort* range) {
sort* s = range;
for (int i = (int)domain.size() - 1; i >= 0; --i) {
s = m_array.mk_array_sort(domain[i], s);
m_pinned_sorts.push_back(s);
}
for (unsigned i = domain.size(); i-- > 0; )
s = m_array.mk_array_sort(domain[i], s);
m_pinned_sorts.push_back(s);
return s;
}
@ -1535,7 +1534,7 @@ class tptp_parser {
// For function-style definitions, wrap value in lambdas
if (!param_vars.empty()) {
expr_ref result = value;
for (int i = (int)param_vars.size() - 1; i >= 0; --i) {
for (unsigned i = param_vars.size(); i-- > 0; ) {
expr_ref abs_body(m);
expr_abstract(m, 0, 1, (expr* const*)&param_vars[i], result, abs_body);
sort* s = param_vars[i]->get_sort();
@ -1976,7 +1975,7 @@ class tptp_parser {
// Create nested single-variable lambdas (curried) to match our curried array encoding.
// ^[X:A, Y:B] : body becomes ^[X:A] : (^[Y:B] : body) with sort Array(A, Array(B, body_sort))
expr_ref result = body;
for (int i = (int)vars.size() - 1; i >= 0; --i) {
for (unsigned i = vars.size(); i-- > 0; ) {
expr_ref abs_body(m);
expr_abstract(m, 0, 1, (expr* const*)&vars[i], result, abs_body);
sort* s = vars[i]->get_sort();
@ -2877,6 +2876,7 @@ expr_ref tptp_parser::parse_term() {
if (!m_array.is_array(e_sort)) {
sort* arg_sort = arg->get_sort();
sort* arr_sort = m_array.mk_array_sort(arg_sort, m_univ);
m_pinned_sorts.push_back(arr_sort);
e = coerce_arg(e, arr_sort);
} else {
sort* dom = get_array_domain(e_sort, 0);

1
src/solver/assertions/asserted_formulas.cpp
View file

@ -496,6 +496,7 @@ void asserted_formulas::simplify_fmls::operator()() {
expr_ref result(m);
proof_ref result_pr(m);
simplify(j, result, result_pr);
SASSERT(is_well_sorted(m, j.fml()));
if (m.proofs_enabled()) {
if (!result_pr) result_pr = m.mk_rewrite(j.fml(), result);
result_pr = m.mk_modus_ponens(j.pr(), result_pr);