From c1ff3d31920d6b5474fc4faa008bddb40c05a381 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 30 Nov 2022 13:46:00 +0700 Subject: [PATCH] wip - adding quasi macro detection --- src/ast/simplifiers/eliminate_predicates.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/ast/simplifiers/eliminate_predicates.cpp b/src/ast/simplifiers/eliminate_predicates.cpp index eb7006da6..700f96ce3 100644 --- a/src/ast/simplifiers/eliminate_predicates.cpp +++ b/src/ast/simplifiers/eliminate_predicates.cpp @@ -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 */ -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)) return false; 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; for (expr* arg : *head) { if (!is_var(arg)) - return continue; + continue; unsigned idx = to_var(arg)->get_idx(); if (indices.contains(idx)) - return continue; + continue; if (idx >= num_bound) return false; indices.insert(idx); } - return indices.size() == num_bound; + return indices.num_elems() == num_bound; }