mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-04-11 04:09:59 +02:00
parent 0d06bc5990
commit 551d72b294
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/ast/recfun_decl_plugin.cpp
View file

@ -238,6 +238,7 @@ namespace recfun {
while (! stack.empty()) { while (! stack.empty()) {
expr * e = stack.back(); expr * e = stack.back();
stack.pop_back(); stack.pop_back();
TRACEFN("unfold: " << mk_pp(e, m));
if (m.is_ite(e)) { if (m.is_ite(e)) {
// need to do a case split on `e`, forking the search space // need to do a case split on `e`, forking the search space
@ -257,6 +258,7 @@ namespace recfun {
if (b.to_split != nullptr) { if (b.to_split != nullptr) {
// split one `ite`, which will lead to distinct (sets of) cases // split one `ite`, which will lead to distinct (sets of) cases
app * ite = b.to_split->ite; app * ite = b.to_split->ite;
TRACEFN("split: " << mk_pp(ite, m));
expr* c = nullptr, *th = nullptr, *el = nullptr; expr* c = nullptr, *th = nullptr, *el = nullptr;
VERIFY(m.is_ite(ite, c, th, el)); VERIFY(m.is_ite(ite, c, th, el));
@ -287,6 +289,7 @@ namespace recfun {
// substitute, to get rid of `ite` terms // substitute, to get rid of `ite` terms
expr_ref case_rhs = subst(rhs); expr_ref case_rhs = subst(rhs);
TRACEFN("case_rhs: " << case_rhs);
for (unsigned i = 0; i < conditions.size(); ++i) { for (unsigned i = 0; i < conditions.size(); ++i) {
conditions[i] = subst(conditions.get(i)); conditions[i] = subst(conditions.get(i));
} }