mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-16 02:46:16 +00:00
Code Activity

fix #6304

Browse source 
Conditionals are used to guard unfolding of recursive functions.
This is, as shown in #6304, incompatible with the case where recursive functions are used inside if-then-else guards.
We address this by disabling if-conditions as guards if they contain a recursive definition.
The approach is simplistic: if a recursive function, defined prior (not mutually recursive) is used in a guard it should be fine and the condition can guard the current recursive unfolding.
This commit is contained in:
Nikolaj Bjorner 2022-08-30 09:50:58 -07:00
parent 45d8d73fce
commit 36d76a5bb2
1 changed files with 7 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/recfun_decl_plugin.cpp
View file

@ -291,7 +291,11 @@ namespace recfun {
expr * e = stack.back(); expr * e = stack.back();
stack.pop_back(); stack.pop_back();
if (m.is_ite(e)) { expr* cond = nullptr, *th = nullptr, *el = nullptr;
if (m.is_ite(e, cond, th, el) && contains_def(u, cond)) {
// skip
}
else if (m.is_ite(e)) {
// need to do a case split on `e`, forking the search space // need to do a case split on `e`, forking the search space
b.to_split = st.cons_ite(to_app(e), b.to_split); b.to_split = st.cons_ite(to_app(e), b.to_split);
} }
@ -338,9 +342,8 @@ namespace recfun {
// substitute, to get rid of `ite` terms // substitute, to get rid of `ite` terms
expr_ref case_rhs = subst(rhs); expr_ref case_rhs = subst(rhs);
for (unsigned i = 0; i < conditions.size(); ++i) { for (unsigned i = 0; i < conditions.size(); ++i)
conditions[i] = subst(conditions.get(i)); conditions[i] = subst(conditions.get(i));
}
// yield new case // yield new case
bool is_imm = is_i(case_rhs); bool is_imm = is_i(case_rhs);
@ -471,9 +474,8 @@ namespace recfun {
void plugin::set_definition(replace& r, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) { void plugin::set_definition(replace& r, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) {
u().set_definition(r, d, is_macro, n_vars, vars, rhs); u().set_definition(r, d, is_macro, n_vars, vars, rhs);
for (case_def & c : d.get_def()->get_cases()) { for (case_def & c : d.get_def()->get_cases())
m_case_defs.insert(c.get_decl(), &c); m_case_defs.insert(c.get_decl(), &c);
}
} }
bool plugin::has_defs() const { bool plugin::has_defs() const {