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

add partial evaluation cases for algebraic data-types for recursive functions.

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-06-16 16:07:16 -07:00
parent 81ebd52f61
commit ef86f5fcc2
2 changed files with 36 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/recfun_decl_plugin.cpp
View file

@ -301,7 +301,6 @@ namespace recfun {
// skip // skip
} }
else if (m.is_ite(e)) { else if (m.is_ite(e)) {
verbose_stream() << "unfold " << mk_pp(e, m) << "\n";
// 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);
} }

42
src/ast/rewriter/recfun_rewriter.cpp
View file

@ -19,20 +19,50 @@ Author:
#include "ast/rewriter/recfun_rewriter.h" #include "ast/rewriter/recfun_rewriter.h"
#include "ast/rewriter/var_subst.h" #include "ast/rewriter/var_subst.h"
#include "ast/datatype_decl_plugin.h"
#include "ast/for_each_expr.h"
br_status recfun_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { 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) { if (m_rec.is_defined(f) && num_args > 0) {
for (unsigned i = 0; i < num_args; ++i)
if (!m.is_value(args[i]))
return BR_FAILED;
if (!m_rec.has_def(f)) if (!m_rec.has_def(f))
return BR_FAILED; return BR_FAILED;
recfun::def const& d = m_rec.get_def(f); recfun::def const& d = m_rec.get_def(f);
if (!d.get_rhs()) if (!d.get_rhs())
return BR_FAILED; return BR_FAILED;
var_subst sub(m); auto r = d.get_rhs();
result = sub(d.get_rhs(), num_args, args); bool safe_to_subst = true;
return BR_REWRITE_FULL; for (unsigned i = 0; i < num_args; ++i)
if (!m.is_value(args[i]))
safe_to_subst = false;
// check if there is an argument that is a constructor
// such that the recursive function can be partially evaluated.
if (!safe_to_subst && !has_quantifiers(r)) {
datatype::util u(m);
auto is_decreasing = [&](unsigned i) {
bool is_dec = true;
unsigned idx = num_args - i - 1;
for (auto t : subterms::all(expr_ref(r, m)))
if (is_app(t) && any_of(*to_app(t), [&](expr* e) { return is_var(e) && to_var(e)->get_idx() == idx; }))
if (!u.is_accessor(t) && !u.is_is(t) && !u.is_recognizer(t))
is_dec = false;
return is_dec;
};
for (unsigned i = 0; i < num_args; ++i) {
auto arg = args[i];
if (u.is_constructor(arg) && is_decreasing(i)) {
safe_to_subst = true;
break;
}
}
}
if (safe_to_subst) {
var_subst sub(m);
result = sub(d.get_rhs(), num_args, args);
return BR_REWRITE_FULL;
}
return BR_FAILED;
} }
else else
return BR_FAILED; return BR_FAILED;