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

block recursive definitions with lambdas until they are properly supported #5813

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-02-06 08:57:58 +02:00
parent 1c10ce4070
commit 03ff3201b9
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/ast/recfun_decl_plugin.cpp
View file

@ -225,6 +225,11 @@ namespace recfun {
m_vars.append(n_vars, vars); m_vars.append(n_vars, vars);
m_rhs = rhs; m_rhs = rhs;
if (!is_macro)
for (expr* e : subterms::all(m_rhs))
if (is_lambda(e))
throw default_exception("recursive definitions with lambdas are not supported");
expr_ref_vector conditions(m); expr_ref_vector conditions(m);
// is the function a macro (unconditional body)? // is the function a macro (unconditional body)?
@ -233,6 +238,8 @@ namespace recfun {
add_case(name, 0, conditions, rhs); add_case(name, 0, conditions, rhs);
return; return;
} }
// analyze control flow of `rhs`, accumulating guards and // analyze control flow of `rhs`, accumulating guards and
// rebuilding a `ite`-free RHS on the fly for each path in `rhs`. // rebuilding a `ite`-free RHS on the fly for each path in `rhs`.