mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

simplify body

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-10-26 14:32:19 -07:00
parent 5b181156b2
commit 09f37e49b0
1 changed files with 6 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/muz_qe/horn_subsume_model_converter.cpp
View file

@ -186,30 +186,29 @@ void horn_subsume_model_converter::operator()(model_ref& mr) {
TRACE("dl_mc", tout << "eval: " << h->get_name() << "\n" << mk_pp(body, m) << "\n";); TRACE("dl_mc", tout << "eval: " << h->get_name() << "\n" << mk_pp(body, m) << "\n";);
expr_ref tmp(body); expr_ref tmp(body);
mr->eval(tmp, body); mr->eval(tmp, body);
m_rewrite(body);
TRACE("dl_mc", tout << "to:\n" << mk_pp(body, m) << "\n";); TRACE("dl_mc", tout << "to:\n" << mk_pp(body, m) << "\n";);
if (arity == 0) { if (arity == 0) {
expr* e = mr->get_const_interp(h); expr* e = mr->get_const_interp(h);
if (e) { if (e) {
mr->register_decl(h, m.mk_or(e, body)); body = m.mk_or(e, body);
}
else {
mr->register_decl(h, body);
} }
m_rewrite(body);
mr->register_decl(h, m.mk_or(e, body));
} }
else { else {
func_interp* f = mr->get_func_interp(h); func_interp* f = mr->get_func_interp(h);
if (f) { if (f) {
expr* e = f->get_else(); expr* e = f->get_else();
f->set_else(m.mk_or(e, body.get())); body = m.mk_or(e, body);
} }
else { else {
f = alloc(func_interp, m, arity); f = alloc(func_interp, m, arity);
f->set_else(body);
mr->register_decl(h, f); mr->register_decl(h, f);
} }
m_rewrite(body);
f->set_else(body);
} }
} }
} }