From f5fa6b0bcb80b2ee16930ec1df6445b230d8c6e0 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Mon, 31 Jul 2017 15:58:00 -0400
Subject: [PATCH] optionally disable subsumption checker

---
 src/muz/transforms/dl_mk_subsumption_checker.cpp | 3 +++
 src/muz/transforms/dl_transforms.cpp             | 9 +++++++++
 2 files changed, 12 insertions(+)

diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp
index 6a3ea8735..d3b959792 100644
--- a/src/muz/transforms/dl_mk_subsumption_checker.cpp
+++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp
@@ -25,6 +25,7 @@ Revision History:
 #include "ast/rewriter/rewriter_def.h"
 #include "muz/transforms/dl_mk_subsumption_checker.h"
 
+#include "fixedpoint_params.hpp"
 namespace datalog {
 
 
@@ -328,6 +329,8 @@ namespace datalog {
 
     rule_set * mk_subsumption_checker::operator()(rule_set const & source) {
         // TODO mc
+        if (!m_context.get_params ().xform_subsumption_checker()) 
+          return 0;
 
         m_have_new_total_rule = false;
         collect_ground_unconditional_rule_heads(source);
diff --git a/src/muz/transforms/dl_transforms.cpp b/src/muz/transforms/dl_transforms.cpp
index 48e956979..c727a29d4 100644
--- a/src/muz/transforms/dl_transforms.cpp
+++ b/src/muz/transforms/dl_transforms.cpp
@@ -51,17 +51,22 @@ namespace datalog {
         }
         transf.register_plugin(alloc(datalog::mk_quantifier_instantiation, ctx, 37000));
 
+        if (ctx.get_params().datalog_subsumption()) {
         transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 35005));
+        }
         transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 35000));
         transf.register_plugin(alloc(datalog::mk_coi_filter, ctx, 34990));
         transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, ctx, 34980));
 
         //and another round of inlining
+        if (ctx.get_params().datalog_subsumption()) {
         transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34975));
+        }
         transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34970));
         transf.register_plugin(alloc(datalog::mk_coi_filter, ctx, 34960));
         transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, ctx, 34950));
 
+        if (ctx.get_params().datalog_subsumption()) {
         transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34940));
         transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34930));
         transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34920));
@@ -69,6 +74,10 @@ namespace datalog {
         transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34900));
         transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34890));
         transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34880));
+        }
+        else {
+            transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34930));
+        }
 
         transf.register_plugin(alloc(datalog::mk_bit_blast, ctx, 35000));
         transf.register_plugin(alloc(datalog::mk_karr_invariants, ctx, 36010));