mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 21:57:00 +00:00
Code Activity

wip - adding quasi macro detection

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-30 13:46:00 +07:00
parent 7b9dfb8e1e
commit c1ff3d3192
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/simplifiers/eliminate_predicates.cpp
View file

@ -135,7 +135,7 @@ bool eliminate_predicates::can_be_macro_head(expr* _head, unsigned num_bound) {
* f(x,y,x+y+3,1) where x, y are the only bound variables * f(x,y,x+y+3,1) where x, y are the only bound variables
*/ */
bool eliminate_predicates::can_be_quasi_macro_head(expr* head, unsigned num_bound) { bool eliminate_predicates::can_be_quasi_macro_head(expr* _head, unsigned num_bound) {
if (!is_app(_head)) if (!is_app(_head))
return false; return false;
app* head = to_app(_head); app* head = to_app(_head);
@ -149,15 +149,15 @@ bool eliminate_predicates::can_be_quasi_macro_head(expr* head, unsigned num_boun
uint_set indices; uint_set indices;
for (expr* arg : *head) { for (expr* arg : *head) {
if (!is_var(arg)) if (!is_var(arg))
return continue; continue;
unsigned idx = to_var(arg)->get_idx(); unsigned idx = to_var(arg)->get_idx();
if (indices.contains(idx)) if (indices.contains(idx))
return continue; continue;
if (idx >= num_bound) if (idx >= num_bound)
return false; return false;
indices.insert(idx); indices.insert(idx);
} }
return indices.size() == num_bound; return indices.num_elems() == num_bound;
} }