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

fixing build break, adding fixedpoint object to C++ API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-10 22:52:55 +01:00
parent fbf81c88a2
commit 338193548b
2 changed files with 37 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/rewriter.h
View file

@ -315,6 +315,8 @@ protected:
template<bool ProofGen> template<bool ProofGen>
void process_app(app * t, frame & fr); void process_app(app * t, frame & fr);
bool constant_fold(app* t, frame& fr);
template<bool ProofGen> template<bool ProofGen>
void process_quantifier(quantifier * q, frame & fr); void process_quantifier(quantifier * q, frame & fr);

44
src/ast/rewriter/rewriter_def.h
View file

@ -174,6 +174,38 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
} }
} }
template<typename Config>
bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
if (fr.m_i == 1 && m().is_ite(t)) {
expr * cond = result_stack()[fr.m_spos].get();
expr* arg = 0;
if (m().is_true(cond)) {
arg = t->get_arg(1);
}
else if (m().is_false(cond)) {
arg = t->get_arg(2);
}
if (arg) {
result_stack().shrink(fr.m_spos);
result_stack().push_back(arg);
fr.m_state = REWRITE_BUILTIN;
unsigned max_depth = fr.m_max_depth;
if (visit<false>(arg, fr.m_max_depth)) {
m_r = result_stack().back();
result_stack().pop_back();
result_stack().pop_back();
result_stack().push_back(m_r);
cache_result<false>(t, m_r, m_pr, fr.m_cache_result);
frame_stack().pop_back();
set_new_child_flag(t);
}
m_r = 0;
return true;
}
}
return false;
}
template<typename Config> template<typename Config>
template<bool ProofGen> template<bool ProofGen>
void rewriter_tpl<Config>::process_app(app * t, frame & fr) { void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
@ -183,16 +215,10 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
case PROCESS_CHILDREN: { case PROCESS_CHILDREN: {
unsigned num_args = t->get_num_args(); unsigned num_args = t->get_num_args();
while (fr.m_i < num_args) { while (fr.m_i < num_args) {
expr * arg = t->get_arg(fr.m_i); if (!ProofGen && constant_fold(t, fr)) {
if (fr.m_i >= 1 && m().is_ite(t) && !ProofGen) { return;
expr * cond = result_stack()[fr.m_spos].get();
if (m().is_true(cond)) {
arg = t->get_arg(1);
}
else if (m().is_false(cond)) {
arg = t->get_arg(2);
}
} }
expr * arg = t->get_arg(fr.m_i);
fr.m_i++; fr.m_i++;
if (!visit<ProofGen>(arg, fr.m_max_depth)) if (!visit<ProofGen>(arg, fr.m_max_depth))
return; return;