From: Hamed <hamed.gorjiara@gmail.com>
Date: Sat, 26 Aug 2017 00:18:19 +0000 (-0700)
Subject: Adding back the IntegerEncoding ...
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=e4713ffeb2209261c1583667e1c8ff83f223dc6a;p=satune.git

Adding back the IntegerEncoding ...
---

diff --git a/src/ASTTransform/orderdecompose.cc b/src/ASTTransform/orderdecompose.cc
index 2effff5..8b3aa73 100644
--- a/src/ASTTransform/orderdecompose.cc
+++ b/src/ASTTransform/orderdecompose.cc
@@ -11,6 +11,7 @@
 #include "csolver.h"
 #include "orderencoder.h"
 #include "tunable.h"
+#include "integerencoding.h"
 
 void orderAnalysis(CSolver *This) {
 	uint size = This->allOrders.getSize();
@@ -52,10 +53,17 @@ void orderAnalysis(CSolver *This) {
 		
 		//This is needed for splitorder
 		computeStronglyConnectedComponentGraph(graph);
-		
 		decomposeOrder(This, order, graph);
-		
 		deleteOrderGraph(graph);
+		
+		bool doIntegerEncoding = GETVARTUNABLE(This->tuner, order->order.type, ORDERINTEGERENCODING, &onoff );
+		if(!doIntegerEncoding)
+			continue;
+		uint size = order->constraints.getSize();
+		for(uint i=0; i<size; i++){
+			orderIntegerEncodingSATEncoder(This->satEncoder, order->constraints.get(i));
+		}
+
 	}
 }