From 3e27c15520a179e1107547685fa69fc53e0c307e Mon Sep 17 00:00:00 2001
From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 18 Jul 2017 11:52:13 -0700
Subject: [PATCH] bug fix for the order test case ...

---
 src/Backend/satorderencoder.c | 25 ++++++++++++++-----------
 src/Backend/sattranslator.c   |  3 +--
 src/Test/testorder.c          |  5 +++--
 3 files changed, 18 insertions(+), 15 deletions(-)

diff --git a/src/Backend/satorderencoder.c b/src/Backend/satorderencoder.c
index dee9b26..36c16f2 100644
--- a/src/Backend/satorderencoder.c
+++ b/src/Backend/satorderencoder.c
@@ -20,7 +20,7 @@ Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
 Edge getPairConstraint(SATEncoder *This, HashTableOrderPair * table, OrderPair * pair) {
 	bool negate = false;
 	OrderPair flipped;
-	if (pair->first > pair->second) {
+	if (pair->first < pair->second) {
 		negate=true;
 		flipped.first=pair->second;
 		flipped.second=pair->first;
@@ -79,17 +79,20 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
 
 Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair){
 	ASSERT(pair->first!= pair->second);
-	OrderPair* value = getOrderPair(table, pair);
-	if(value == NULL)
+	bool negate = false;
+	OrderPair flipped;
+	if (pair->first < pair->second) {
+		negate=true;
+		flipped.first=pair->second;
+		flipped.second=pair->first;
+		pair = &flipped;
+	}
+	if (!containsOrderPair(table, pair)) {
 		return E_NULL;
-	Edge constraint = value->constraint;
-	model_print("Constraint:\n");
-	printCNF(constraint);
-	model_print("\n***********\n");
-	if(pair->first > pair->second || edgeIsNull(constraint))
-		return constraint;
-	else
-		return constraintNegate(constraint);
+	}
+	Edge constraint= getOrderPair(table, pair)->constraint;
+	ASSERT(!edgeIsNull(constraint));
+	return negate ? constraintNegate(constraint) : constraint;
 }
 
 Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK){
diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index ee22879..a3245d8 100644
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -82,9 +82,8 @@ bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
 
 HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, Order * order, uint64_t first, uint64_t second){
 	ASSERT(order->orderPairTable!= NULL);
-	model_print("Frist:%llu\tSecond:%llu\n", first, second);
 	OrderPair pair={first, second, E_NULL};
-	Edge var = getOrderConstraint(order->orderPairTable, & pair);
+	Edge var = getOrderConstraint(order->orderPairTable, &pair); 
 	if(edgeIsNull(var))
 		return UNORDERED;
 	return getValueCNF(This->satEncoder->cnf, var)? FIRST: SECOND;
diff --git a/src/Test/testorder.c b/src/Test/testorder.c
index 0ebd5e2..4970cac 100644
--- a/src/Test/testorder.c
+++ b/src/Test/testorder.c
@@ -11,11 +11,12 @@ int main(int numargs, char ** argv) {
 	addConstraint(solver, b1);
 	addConstraint(solver, b2);
 	if (startEncoding(solver)==1)
-		printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n", 
+		printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d O(1111,5)=%d\n", 
 			getOrderConstraintValue(solver, order, 5, 1), 
 			getOrderConstraintValue(solver, order, 1, 4),
 			getOrderConstraintValue(solver, order, 5, 4),
-			getOrderConstraintValue(solver, order, 1, 5));
+			getOrderConstraintValue(solver, order, 1, 5),
+			getOrderConstraintValue(solver, order, 1111, 5));
 	else
 		printf("UNSAT\n");
 	deleteSolver(solver);
-- 
2.34.1