Renaming
[satune.git] / src / Backend / satencoder.c
index 1cf408d0ca404e15e67de8ae730bdd9854f3d6e2..4bc1d61f6fb370de10d9dc361a31a02639b698a3 100644 (file)
@@ -145,22 +145,22 @@ Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
        return E_BOGUS;
 }
 
-Edge getPairConstraint(SATEncoder *This, HashTableBoolConst * table, OrderPair * pair) {
+Edge getPairConstraint(SATEncoder *This, HashTableOrderPair * 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;        //FIXME: accessing a local variable from outside of the function?
+               pair = &flipped;
        }
        Edge constraint;
-       if (!containsBoolConst(table, pair)) {
+       if (!containsOrderPair(table, pair)) {
                constraint = getNewVarSATEncoder(This);
                OrderPair * paircopy = allocOrderPair(pair->first, pair->second, constraint);
-               putBoolConst(table, paircopy, paircopy);
+               putOrderPair(table, paircopy, paircopy);
        } else
-               constraint = getBoolConst(table, pair)->constraint;
+               constraint = getOrderPair(table, pair)->constraint;
        if (negate)
                return constraintNegate(constraint);
        else
@@ -170,20 +170,20 @@ Edge getPairConstraint(SATEncoder *This, HashTableBoolConst * table, OrderPair *
 
 Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
        ASSERT(boolOrder->order->type == TOTAL);
-       if(boolOrder->order->boolsToConstraints == NULL){
+       if(boolOrder->order->orderPairTable == NULL){
                initializeOrderHashTable(boolOrder->order);
                createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
        }
-       HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
+       HashTableOrderPair* orderPairTable = boolOrder->order->orderPairTable;
        OrderPair pair={boolOrder->first, boolOrder->second, E_NULL};
-       Edge constraint = getPairConstraint(This, boolToConsts, & pair);
+       Edge constraint = getPairConstraint(This, orderPairTable, & pair);
        return constraint;
 }
 
 void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
        ASSERT(order->type == TOTAL);
        VectorInt* mems = order->set->members;
-       HashTableBoolConst* table = order->boolsToConstraints;
+       HashTableOrderPair* table = order->orderPairTable;
        uint size = getSizeVectorInt(mems);
        uint csize =0;
        for(uint i=0; i<size; i++){
@@ -204,9 +204,9 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
        }
 }
 
-Edge getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
+Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair){
        ASSERT(pair->first!= pair->second);
-       Edge constraint = getBoolConst(table, pair)->constraint;
+       Edge constraint = getOrderPair(table, pair)->constraint;
        if(pair->first > pair->second)
                return constraint;
        else
@@ -227,12 +227,12 @@ Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){
        // when client specify sparse constraints for the total order!)
        ASSERT(constraint->order->type == PARTIAL);
 /*
-       HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
-       if( containsBoolConst(boolToConsts, boolOrder) ){
-               return getBoolConst(boolToConsts, boolOrder);
+       HashTableOrderPair* boolToConsts = boolOrder->order->boolsToConstraints;
+       if( containsOrderPair(boolToConsts, boolOrder) ){
+               return getOrderPair(boolToConsts, boolOrder);
        } else {
                Edge constraint = getNewVarSATEncoder(This); 
-               putBoolConst(boolToConsts,boolOrder, constraint);
+               putOrderPair(boolToConsts,boolOrder, constraint);
                VectorBoolean* orderConstrs = &boolOrder->order->constraints;
                uint size= getSizeVectorBoolean(orderConstrs);
                for(uint i=0; i<size; i++){