1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
/*++
Copyright (c) 2018 Microsoft Corporation
Module Name:
recfun_rewriter.cpp
Abstract:
Rewriter recursive function applications to values
Author:
Nikolaj Bjorner (nbjorner) 2020-04-26
--*/
#include "ast/rewriter/recfun_rewriter.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) {
if (m_rec.is_defined(f) && num_args > 0) {
if (!m_rec.has_def(f))
return BR_FAILED;
recfun::def const& d = m_rec.get_def(f);
if (!d.get_rhs())
return BR_FAILED;
auto r = d.get_rhs();
bool safe_to_subst = true;
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.
// at most one kind of accessor is allowed to prevent recursive
// patterns that reconstruct the argument indirectly.
// This can be relaxed to omitting at least one accessor, and probably other patterns.
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;
func_decl* dec_fun = nullptr;
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;
else if (u.is_accessor(t) && dec_fun && to_app(t)->get_decl() != dec_fun)
is_dec = false;
else if (u.is_accessor(t))
dec_fun = to_app(t)->get_decl();
}
}
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
return BR_FAILED;
}