From 7c4b2b04a7f8a24c0338153781e2029eb575be69 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 Sep 2013 08:54:02 -0700 Subject: [PATCH 1/2] fix coi-filter to not ignore relational tables Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_coi_filter.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index fc4c411ff..8583fbe45 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -52,10 +52,14 @@ namespace datalog { ptr_vector todo; rule_set::decl2rules body2rules; // initialization for reachability + rel_context_base* rc = m_context.get_rel_context(); for (rule_set::iterator it = source.begin(); it != source.end(); ++it) { rule * r = *it; all.insert(r->get_decl()); - if (r->get_uninterpreted_tail_size() == 0) { + bool non_empty = + (rc && !rc->is_empty_relation(r->get_decl())) || + r->get_uninterpreted_tail_size() == 0; + if (non_empty) { if (!reached.contains(r->get_decl())) { reached.insert(r->get_decl()); todo.insert(r->get_decl()); From 5908e24728c4fef4017d66abd7d315137cee0fb2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Sep 2013 09:36:15 -0700 Subject: [PATCH 2/2] fix bug missing NNF of equality as IFF reported by Sticksel Signed-off-by: Nikolaj Bjorner --- src/qe/qe.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index d0aafb896..d63f0ae00 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -482,7 +482,7 @@ namespace qe { } void nnf_iff(app* a, bool p) { - SASSERT(m.is_iff(a) || m.is_xor(a)); + SASSERT(m.is_iff(a) || m.is_xor(a) || m.is_eq(a)); expr* a0 = a->get_arg(0); expr* a1 = a->get_arg(1); @@ -616,7 +616,7 @@ namespace qe { else if (m.is_ite(a)) { nnf_ite(a, p); } - else if (m.is_iff(a)) { + else if (m.is_iff(a) || (m.is_eq(a) && m.is_bool(a->get_arg(0)))) { nnf_iff(a, p); } else if (m.is_xor(a)) { @@ -1926,6 +1926,7 @@ namespace qe { plugin(x).get_num_branches(contains(x), fml, num_branches)) { return true; } + TRACE("qe", tout << "setting variable " << mk_pp(x, m) << " free\n";); m_free_vars.push_back(x); m_current->del_var(x); } @@ -2493,6 +2494,7 @@ namespace qe { // callback to replace variable at index 'idx' with definition 'def' and updated formula 'fml' virtual void elim_var(unsigned idx, expr* fml, expr* def) { + TRACE("qe", tout << mk_pp(m_vars->get(idx), m) << " " << mk_pp(fml, m) << "\n";); *m_fml = fml; m_vars->set(idx, m_vars->get(m_vars->size()-1)); m_vars->pop_back();