From: Hamed <hamed.gorjiara@gmail.com>
Date: Fri, 25 Aug 2017 05:09:26 +0000 (-0700)
Subject: replacing booleanOrder with booleanPredicate in IntegerEncoding ...
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=83f6092a03d132c75f676a9f5cf4d9efd7364ccb

replacing booleanOrder with booleanPredicate in IntegerEncoding ...
---

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index f4b17b4..a992f8f 100644
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -5,6 +5,7 @@
 #include "csolver.h"
 #include "predicate.h"
 #include "element.h"
+#include "rewriter.h"
 
 void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
 	Order* order = boolOrder->order;
@@ -25,6 +26,7 @@ void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
 		This->solver->allElements.push(elem2);
 		This->solver->constraints.add(boolean);
 	}
+	replaceBooleanWithBoolean(This->solver, boolOrder, boolean);
 }
 
 
diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 2e24629..9061f76 100644
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -14,29 +14,16 @@
 #include "orderelement.h"
 
 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
-	switch (constraint->order->order.type){
-		case PAIRWISE:
-			switch ( constraint->order->type) {
-				case PARTIAL:
-					return encodePartialOrderSATEncoder(This, constraint);
-				case TOTAL:
-					return encodeTotalOrderSATEncoder(This, constraint);
-				default:
-					ASSERT(0);
-			}
-		case INTEGERENCODING:{
-			//Infer the value from graph ...
-			Order* order = constraint->order;
-			Edge gvalue = inferOrderConstraintFromGraph(order, constraint->first, constraint->second);
-			if(!edgeIsNull(gvalue))
-				return gvalue;
-			//If we couldn't infer the value from graph, we have already generated a predicate for that ...
-			// So, we should do nothing
-			return E_BOGUS;
-		}
+	switch ( constraint->order->type) {
+		case PARTIAL:
+			return encodePartialOrderSATEncoder(This, constraint);
+		case TOTAL:
+			return encodeTotalOrderSATEncoder(This, constraint);
 		default:
 			ASSERT(0);
 	}
+	default:
+		ASSERT(0);
 	return E_BOGUS;
 }