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

allow mam work with ground patterns

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-05-22 14:14:17 -07:00
parent 95b3ffeb25
commit e7eef2432d
1 changed files with 7 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/mam.cpp
View file

@ -2927,6 +2927,8 @@ namespace {
SASSERT(m.is_pattern(mp)); SASSERT(m.is_pattern(mp));
SASSERT(first_idx < mp->get_num_args()); SASSERT(first_idx < mp->get_num_args());
app * p = to_app(mp->get_arg(first_idx)); app * p = to_app(mp->get_arg(first_idx));
if (is_ground(p))
return;
func_decl * lbl = p->get_decl(); func_decl * lbl = p->get_decl();
unsigned lbl_id = lbl->get_small_id(); unsigned lbl_id = lbl->get_small_id();
m_trees.reserve(lbl_id+1, nullptr); m_trees.reserve(lbl_id+1, nullptr);
@ -3852,10 +3854,10 @@ namespace {
// Ground patterns are discarded. // Ground patterns are discarded.
// However, the simplifier may turn a non-ground pattern into a ground one. // However, the simplifier may turn a non-ground pattern into a ground one.
// So, we should check it again here. // So, we should check it again here.
unsigned num_patterns = mp->get_num_args(); if (all_of(*mp, [](expr *arg) { return is_ground(arg); }))
for (unsigned i = 0; i < num_patterns; ++i) return; // ignore multi-pattern containing only ground pattern.
if (is_ground(mp->get_arg(i))) if (any_of(*mp, [](expr *arg) { return has_quantifiers(arg); }))
return; // ignore multi-pattern containing ground pattern. return; // patterns with quantifiers are not handled.
update_filters(qa, mp); update_filters(qa, mp);
collect_ground_exprs(qa, mp); collect_ground_exprs(qa, mp);
m_new_patterns.push_back(qp_pair(qa, mp)); m_new_patterns.push_back(qp_pair(qa, mp));
@ -3863,7 +3865,7 @@ namespace {
// e-matching. So, for a multi-pattern [ p_1, ..., p_n ], // e-matching. So, for a multi-pattern [ p_1, ..., p_n ],
// we have to make n insertions. In the i-th insertion, // we have to make n insertions. In the i-th insertion,
// the pattern p_i is assumed to be the first one. // the pattern p_i is assumed to be the first one.
for (unsigned i = 0; i < num_patterns; ++i) for (unsigned i = 0; i < mp->get_num_args(); ++i)
m_trees.add_pattern(qa, mp, i); m_trees.add_pattern(qa, mp, i);
} }