From: bdemsky <bdemsky@uci.edu>
Date: Mon, 3 Jul 2017 22:03:31 +0000 (-0700)
Subject: more bug fixes, think this should work
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=efcbd9094ed33e523594e8bb38a117e5e11a5092;p=satune.git

more bug fixes, think this should work
---

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 845b368..70bfce0 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -179,27 +179,32 @@ Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint)
 }
 
 Constraint * getPairConstraint(SATEncoder *This, HashTableBoolConst * table, OrderPair * pair) {
-	ASSERT(pair->first < pair->second);
+	bool negate = false;
+	OrderPair flipped;
+	if (pair->first > pair->second) {
+		negate=true;
+		flipped.first=pair->second;
+		flipped.second=pair->first;
+		pair = &flipped;
+	}
+	Constraint * constraint;
 	if (!containsBoolConst(table, pair)) {
-		Constraint *constraint = getNewVarSATEncoder(This);
+		constraint = getNewVarSATEncoder(This);
 		OrderPair * paircopy = allocOrderPair(pair->first, pair->second);
 		putBoolConst(table, paircopy, constraint);
-		return constraint;
 	} else
-		return getBoolConst(table, pair);
+		constraint = getBoolConst(table, pair);
+	if (negate)
+		return negateConstraint(constraint);
+	else
+		return constraint;
+	
 }
 
 Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
 	ASSERT(boolOrder->order->type == TOTAL);
 	HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
-	OrderPair pair;
-	if (boolOrder->first < boolOrder->second) {
-		pair.first=boolOrder->first;
-		pair.second=boolOrder->second;
-	} else {
-		pair.first=boolOrder->second;
-		pair.second=boolOrder->first;
-	}
+	OrderPair pair={boolOrder->first, boolOrder->second};
 	Constraint* constraint = getPairConstraint(This, boolToConsts, & pair);
 	return constraint;
 }