From c5f8bf43ba9657a96f0989dfaecd41741c7340c2 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Mon, 21 Aug 2017 22:22:07 -0700
Subject: [PATCH] Add calls into tuner framework

---
 src/Encoders/orderencoder.c | 39 +++++++++++++++++++++++++------------
 src/Tuner/tunable.h         |  6 ++++--
 2 files changed, 31 insertions(+), 14 deletions(-)

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index 084995b..e97a17b 100644
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -7,6 +7,7 @@
 #include "ordernode.h"
 #include "rewriter.h"
 #include "mutableset.h"
+#include "tunable.h"
 
 OrderGraph *buildOrderGraph(Order *order) {
 	OrderGraph *orderGraph = allocOrderGraph(order);
@@ -397,6 +398,11 @@ void orderAnalysis(CSolver *This) {
 	uint size = getSizeVectorOrder(This->allOrders);
 	for (uint i = 0; i < size; i++) {
 		Order *order = getVectorOrder(This->allOrders, i);
+		TunableDesc onoff={9, 1, 1};
+		bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
+		if (!doDecompose)
+			continue;
+		
 		OrderGraph *graph = buildOrderGraph(order);
 		if (order->type == PARTIAL) {
 			//Required to do SCC analysis for partial order graphs.  It
@@ -405,24 +411,33 @@ void orderAnalysis(CSolver *This) {
 			completePartialOrderGraph(graph);
 		}
 
-		//This analysis is completely optional
-		reachMustAnalysis(This, graph, false);
 
-		//This pair of analysis is also optional
-		if (order->type == PARTIAL) {
-			localMustAnalysisPartial(This, graph);
-		} else {
-			localMustAnalysisTotal(This, graph);
-		}
+		bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff);
+
+		if (mustReachGlobal)
+			reachMustAnalysis(This, graph, false);
 
-		//This optimization is completely optional
-		removeMustBeTrueNodes(graph);
+		bool mustReachLocal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHLOCAL, &onoff);
+		
+		if (mustReachLocal) {
+			//This pair of analysis is also optional
+			if (order->type == PARTIAL) {
+				localMustAnalysisPartial(This, graph);
+			} else {
+				localMustAnalysisTotal(This, graph);
+			}
+		}
 
+		bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff);
+		
+		if (mustReachPrune)
+			removeMustBeTrueNodes(graph);
+		
 		//This is needed for splitorder
 		computeStronglyConnectedComponentGraph(graph);
-
+		
 		decomposeOrder(This, order, graph);
-
+		
 		deleteOrderGraph(graph);
 	}
 }
diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index 45744b0..66c4638 100644
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -18,7 +18,9 @@ void deleteTuner(Tuner *This);
 int getTunable(Tuner *This, TunableParam param, TunableDesc * descriptor);
 int getVarTunable(Tuner *This, VarType vartype, TunableParam param, TunableDesc * descriptor);
 
-#define GETTUNABLE(This, param, descriptor) getTunable(This, param, descriptor);
-#define GETVARTUNABLE(This, vartype, param, descriptor) getTunable(This, param, descriptor);
+#define GETTUNABLE(This, param, descriptor) getTunable(This, param, descriptor)
+#define GETVARTUNABLE(This, vartype, param, descriptor) getTunable(This, param, descriptor)
 
+enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE};
+typedef enum Tunables Tunables;
 #endif
-- 
2.34.1