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

enable auxiliary recursive function definitions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-27 16:12:32 -08:00
parent 3cbc7099ce
commit 15f5444b8c
1 changed files with 6 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/recfun_decl_plugin.cpp
View file

@ -216,7 +216,7 @@ namespace recfun {
unsigned case_idx = 0; unsigned case_idx = 0;
std::string name("case-"); std::string name("case-");
name.append(m_name.bare_str()); name.append(m_name.str());
m_vars.append(n_vars, vars); m_vars.append(n_vars, vars);
m_rhs = rhs; m_rhs = rhs;
@ -337,11 +337,8 @@ namespace recfun {
void util::set_definition(replace& subst, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) { void util::set_definition(replace& subst, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) {
d.set_definition(subst, n_vars, vars, rhs);
#if 0
expr_ref rhs1 = get_plugin().redirect_ite(subst, n_vars, vars, rhs); expr_ref rhs1 = get_plugin().redirect_ite(subst, n_vars, vars, rhs);
d.set_definition(subst, n_vars, vars, rhs1); d.set_definition(subst, n_vars, vars, rhs1);
#endif
} }
app_ref util::mk_depth_limit_pred(unsigned d) { app_ref util::mk_depth_limit_pred(unsigned d) {
@ -480,9 +477,9 @@ namespace recfun {
} }
if (m().is_ite(t)) { if (m().is_ite(t)) {
score++; score++;
TRACEFN("score " << mk_pp(t, m()) << ": " << score);
} }
scores.insert(t, score); scores.insert(t, score);
TRACEFN("score " << mk_pp(t, m()) << ": " << score);
} }
} }
} }
@ -491,11 +488,11 @@ namespace recfun {
expr_ref result(e, m()); expr_ref result(e, m());
while (true) { while (true) {
obj_map<expr, unsigned> scores; obj_map<expr, unsigned> scores;
compute_scores(e, scores); compute_scores(result, scores);
unsigned max_score = 0; unsigned max_score = 0;
expr* max_expr = nullptr; expr* max_expr = nullptr;
for (auto const& kv : scores) { for (auto const& kv : scores) {
if (kv.m_value > max_score) { if (m().is_ite(kv.m_key) && kv.m_value > max_score) {
max_expr = kv.m_key; max_expr = kv.m_key;
max_score = kv.m_value; max_score = kv.m_value;
} }
@ -516,8 +513,8 @@ namespace recfun {
expr_ref new_body(m().mk_app(f, n, args.c_ptr()), m()); expr_ref new_body(m().mk_app(f, n, args.c_ptr()), m());
set_definition(subst, pd, n, vars, new_body); set_definition(subst, pd, n, vars, new_body);
subst.insert(max_expr, new_body); subst.insert(max_expr, new_body);
TRACEFN("substitute " << mk_pp(max_expr, m()) << " -> " << new_body); result = subst(result);
subst(result); TRACEFN("substituted " << mk_pp(max_expr, m()) << " -> " << new_body << "\n" << result);
} }
return result; return result;
} }