From ccc2a34444332fdf9610cb09d99f6d14641e513f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 7 Jan 2026 10:56:50 -0800 Subject: [PATCH] fix #8109 default behavior is conservative: if the body of a recursive function contains uninterpreted variables they are not rewritten. Model evaluation will bind values to uninterpreted variables so the filter should not apply here. --- src/ast/rewriter/recfun_rewriter.cpp | 14 +++++++++++--- src/ast/rewriter/recfun_rewriter.h | 4 ++++ src/ast/rewriter/th_rewriter.cpp | 1 + src/model/model_evaluator.cpp | 3 +++ src/params/rewriter_params.pyg | 1 + 5 files changed, 20 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/recfun_rewriter.cpp b/src/ast/rewriter/recfun_rewriter.cpp index c14c6152a..05b927810 100644 --- a/src/ast/rewriter/recfun_rewriter.cpp +++ b/src/ast/rewriter/recfun_rewriter.cpp @@ -21,6 +21,12 @@ Author: #include "ast/rewriter/var_subst.h" #include "ast/datatype_decl_plugin.h" #include "ast/for_each_expr.h" +#include "params/rewriter_params.hpp" + +void recfun_rewriter::updt_params(params_ref const &p) { + rewriter_params rp(p); + m_recfun_unfold = rp.unfold_recursive_functions(); +} br_status recfun_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { if (m_rec.is_defined(f) && num_args > 0) { @@ -34,9 +40,11 @@ br_status recfun_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * for (unsigned i = 0; i < num_args; ++i) if (!m.is_value(args[i])) safe_to_subst = false; - for (auto t : subterms::all(expr_ref(r, m))) - if (is_uninterp(t)) - return BR_FAILED; + if (!m_recfun_unfold) { + for (auto t : subterms::all(expr_ref(r, m))) + if (is_uninterp(t)) + return BR_FAILED; + } // check if there is an argument that is a constructor // such that the recursive function can be partially evaluated. diff --git a/src/ast/rewriter/recfun_rewriter.h b/src/ast/rewriter/recfun_rewriter.h index f1c2ae442..1ef2bcd26 100644 --- a/src/ast/rewriter/recfun_rewriter.h +++ b/src/ast/rewriter/recfun_rewriter.h @@ -24,6 +24,8 @@ Author: class recfun_rewriter { ast_manager& m; recfun::util m_rec; + bool m_recfun_unfold = false; + public: recfun_rewriter(ast_manager& m): m(m), m_rec(m) {} @@ -31,5 +33,7 @@ public: family_id get_fid() const { return m_rec.get_family_id(); } + void updt_params(params_ref const &p); + }; diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index f35d666d6..2a519880a 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -106,6 +106,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { m_ar_rw.updt_params(p); m_f_rw.updt_params(p); m_seq_rw.updt_params(p); + m_rec_rw.updt_params(p); updt_local_params(p); } diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 995feae62..b5f72c432 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -96,6 +96,9 @@ struct evaluator_cfg : public default_rewriter_cfg { m_bv_rw.set_mkbv2num(true); m_ar_rw.set_expand_select_store(true); m_ar_rw.set_expand_select_ite(true); + params_ref rp; + rp.set_bool("unfold_recursive_functions", true); + m_rec_rw.updt_params(rp); updt_params(p); //add_unspecified_function_models(md); } diff --git a/src/params/rewriter_params.pyg b/src/params/rewriter_params.pyg index 20490606c..54802295c 100644 --- a/src/params/rewriter_params.pyg +++ b/src/params/rewriter_params.pyg @@ -7,6 +7,7 @@ def_module_params('rewriter', ("push_ite_bv", BOOL, False, "push if-then-else over bit-vector terms."), ("pull_cheap_ite", BOOL, False, "pull if-then-else terms when cheap."), ("bv_ineq_consistency_test_max", UINT, 0, "max size of conjunctions on which to perform consistency test based on inequalities on bitvectors."), + ("unfold_recursive_functions", BOOL, False, "apply simplification recursively on recursive functions."), ("cache_all", BOOL, False, "cache all intermediate results."), ("enable_der", BOOL, True, "enable destructive equality resolution to quantifiers."), ("rewrite_patterns", BOOL, False, "rewrite patterns."),