Merge branch 'hamed' into brian

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index dc557b5ee40b7147744e22cc84dc54cebb10c144..70bfce095076c0b4d888800690936a177181f396 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -178,16 +178,34 @@ Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint)
        return NULL;
 }
 
+Constraint * getPairConstraint(SATEncoder *This, HashTableBoolConst * table, OrderPair * pair) {
+       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 = getNewVarSATEncoder(This);
+               OrderPair * paircopy = allocOrderPair(pair->first, pair->second);
+               putBoolConst(table, paircopy, constraint);
+       } else
+               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 = allocOrderPair(boolOrder->first, boolOrder->second);
-       if( !containsBoolConst(boolToConsts, pair) ){
-               createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
-       }
-       Constraint* constraint = getOrderConstraint(boolToConsts, pair);
-       deleteOrderPair(pair);
+       OrderPair pair={boolOrder->first, boolOrder->second};
+       Constraint* constraint = getPairConstraint(This, boolToConsts, & pair);
        return constraint;
 }
 
@@ -200,23 +218,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 58d37286193327f51491701a0f1a7bb2c15bdcdc..458ec796f78853175e9146fe25e44191de568ab7 100644 (file)
--- 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){