From: bdemsky <bdemsky@uci.edu>
Date: Mon, 3 Jul 2017 21:54:34 +0000 (-0700)
Subject: some bug fixes
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=e79de0db0603286e08d3fb1328640e764a40d67f;p=satune.git

some bug fixes
---

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index fa124a6..b1162ac 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -178,16 +178,29 @@ Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint)
 	return NULL;
 }
 
+Constraint * getPairConstraint(SATEncoder *This, HashTableBoolConst * table, OrderPair * pair) {
+	ASSERT(pair->first < pair->second);
+	if (!containsBoolConst(table, pair)) {
+		Constraint *constraint = getNewVarSATEncoder(This);
+		OrderPair * paircopy = allocOrderPair(pair->first, pair->second);
+		putBoolConst(table, paircopy, constraint);
+		return constraint;
+	} else
+		return getBoolConst(table, pair);
+}
 
 Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
 	ASSERT(boolOrder->order->type == TOTAL);
 	HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
-	OrderPair* pair = allocOrderPair(boolOrder->first, boolOrder->second);
-	if( !containsBoolConst(boolToConsts, pair) ){
-		createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
+	OrderPair pair;
+	if (boolOrder->first < boolOrder->second) {
+		pair.first=boolOrder->first;
+		pair.second=boolOrder->second;
+	} else {
+		pair.first=boolOrder->second;
+		pair.second=boolOrder->first;
 	}
-	Constraint* constraint = getOrderConstraint(boolToConsts, pair);
-	deleteOrderPair(pair);
+	Constraint* constraint = getPairConstraint(This, boolToConsts, & pair);
 	return constraint;
 }
 
@@ -200,23 +213,14 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
 		uint64_t valueI = getVectorInt(mems, i);
 		for(uint j=i+1; j<size;j++){
 			uint64_t valueJ = getVectorInt(mems, j);
-			OrderPair* pairIJ = allocOrderPair(valueI, valueJ);
-			ASSERT(!containsBoolConst(table, pairIJ));
-			Constraint* constIJ = getNewVarSATEncoder(This);
-			putBoolConst(table, pairIJ, constIJ);
+			OrderPair pairIJ = {valueI, valueJ};
+			Constraint* constIJ=getPairConstraint(This, table, & pairIJ);
 			for(uint k=j+1; k<size; k++){
 				uint64_t valueK = getVectorInt(mems, k);
-				OrderPair* pairJK = allocOrderPair(valueJ, valueK);
-				OrderPair* pairIK = allocOrderPair(valueI, valueK);
-				Constraint* constJK, *constIK;
-				if(!containsBoolConst(table, pairJK)){
-					constJK = getNewVarSATEncoder(This);
-					putBoolConst(table, pairJK, constJK);
-				}
-				if(!containsBoolConst(table, pairIK)){
-					constIK = getNewVarSATEncoder(This);
-					putBoolConst(table, pairIK, constIK);
-				}
+				OrderPair pairJK = {valueJ, valueK};
+				OrderPair pairIK = {valueI, valueK};
+				Constraint* constIK = getPairConstraint(This, table, & pairIK);
+				Constraint* constJK = getPairConstraint(This, table, & pairJK);
 				generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK); 
 			}
 		}
diff --git a/src/Collections/structs.c b/src/Collections/structs.c
index 58d3728..458ec79 100644
--- a/src/Collections/structs.c
+++ b/src/Collections/structs.c
@@ -23,9 +23,7 @@ inline bool Ptr_equals(void * key1, void * key2) {
 }
 
 inline unsigned int order_pair_hash_Function(OrderPair* This){
-	uint64_t x=This->first^This->second;
-	uint64_t a=This->first&This->second;
-	return (uint)((x<<4)^(a));
+	return (uint) (This->first << 2) ^ This->second;
 }
 
 inline unsigned int order_pair_equals(OrderPair* key1, OrderPair* key2){