From 46ca7e17e02b923103d83896e27c622b3ca23bb9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Jun 2015 18:57:16 +0200 Subject: [PATCH] disable bottom-up COI on rules with negated predicates. Fixes issue #140 Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_context.cpp | 1 + src/muz/base/dl_context.h | 1 + src/muz/base/fixedpoint_params.pyg | 1 + src/muz/transforms/dl_mk_coi_filter.cpp | 7 +++++++ 4 files changed, 10 insertions(+) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 9fb597600..a84b1899c 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -298,6 +298,7 @@ namespace datalog { bool context::explanations_on_relation_level() const { return m_params->datalog_explanations_on_relation_level(); } bool context::magic_sets_for_queries() const { return m_params->datalog_magic_sets_for_queries(); } symbol context::tab_selection() const { return m_params->tab_selection(); } + bool context::xform_coi() const { return m_params->xform_coi(); } bool context::xform_slice() const { return m_params->xform_slice(); } bool context::xform_bit_blast() const { return m_params->xform_bit_blast(); } bool context::karr() const { return m_params->xform_karr(); } diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 9f94bd869..d8d961a6a 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -277,6 +277,7 @@ namespace datalog { bool instantiate_quantifiers() const; bool xform_bit_blast() const; bool xform_slice() const; + bool xform_coi() const; void register_finite_sort(sort * s, sort_kind k); diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index 33d1daf57..86cfb30ac 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -142,6 +142,7 @@ def_module_params('fixedpoint', ('xform.instantiate_quantifiers', BOOL, False, "instantiate quantified Horn clauses using E-matching heuristic"), ('xform.coalesce_rules', BOOL, False, "coalesce rules"), + ('xform.coi', BOOL, True, "use cone of influence simplificaiton"), ('duality.enable_restarts', BOOL, False, 'DUALITY: enable restarts'), )) diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index cdb4a5b9e..477eda408 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -36,6 +36,9 @@ namespace datalog { // ----------------------------------- rule_set * mk_coi_filter::operator()(rule_set const & source) { + if (!m_context.xform_coi()) { + return 0; + } if (source.empty()) { return 0; } @@ -70,6 +73,10 @@ namespace datalog { e->get_data().m_value = alloc(ptr_vector); } e->get_data().m_value->push_back(r); + if (r->is_neg_tail(i)) { + // don't try COI on rule with negation. + return 0; + } } } }