mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix filtering for recursive functions

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-12-02 07:53:53 -08:00
parent cf7bba6288
commit 758c3b2c3b
2 changed files with 14 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/ast/simplifiers/dependent_expr_state.cpp
View file

@ -65,14 +65,22 @@ void dependent_expr_state::freeze_terms(expr* e, bool only_as_array, ast_mark& v
*/ */
void dependent_expr_state::freeze_recfun() { void dependent_expr_state::freeze_recfun() {
if (m_recfun_frozen)
return;
m_recfun_frozen = true;
auto& m = m_frozen_trail.get_manager(); auto& m = m_frozen_trail.get_manager();
recfun::util rec(m); recfun::util rec(m);
if (!rec.has_rec_defs())
return;
unsigned sz = rec.get_rec_funs().size();
if (m_num_recfun >= sz)
return;
ast_mark visited; ast_mark visited;
for (func_decl* f : rec.get_rec_funs()) for (func_decl* f : rec.get_rec_funs()) {
freeze_terms(rec.get_def(f).get_rhs(), false, visited); auto& d = rec.get_def(f);
if (!d.is_macro())
freeze_terms(d.get_rhs(), false, visited);
}
m_trail.push(value_trail(m_num_recfun));
m_num_recfun = sz;
} }
/** /**

2
src/ast/simplifiers/dependent_expr_state.h
View file

@ -43,7 +43,7 @@ Author:
class dependent_expr_state { class dependent_expr_state {
unsigned m_qhead = 0; unsigned m_qhead = 0;
bool m_suffix_frozen = false; bool m_suffix_frozen = false;
bool m_recfun_frozen = false; unsigned m_num_recfun = 0;
lbool m_has_quantifiers = l_undef; lbool m_has_quantifiers = l_undef;
ast_mark m_frozen; ast_mark m_frozen;
func_decl_ref_vector m_frozen_trail; func_decl_ref_vector m_frozen_trail;