Renaming

diff --git a/src/AST/order.c b/src/AST/order.c
index 1499dcb16be20425d260c1f9db2b1341a08055f7..92c52ae64069a575a64d538284333fa924fd4c9c 100644 (file)
--- a/src/AST/order.c
+++ b/src/AST/order.c
@@ -9,12 +9,12 @@ Order* allocOrder(OrderType type, Set * set){
        initDefVectorBoolean(& This->constraints);
        This->type=type;
        initOrderEncoding(& This->order, This);
-       This->boolsToConstraints = NULL;
+       This->orderPairTable = NULL;
        return This;
 }
 
 void initializeOrderHashTable(Order* This){
-       This->boolsToConstraints= allocHashTableBoolConst(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+       This->orderPairTable=allocHashTableOrderPair(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
 }
 
 void addOrderConstraint(Order* This, BooleanOrder* constraint){
@@ -28,9 +28,9 @@ void setOrderEncodingType(Order* This, OrderEncodingType type){
 void deleteOrder(Order* This){
        deleteVectorArrayBoolean(& This->constraints);
        deleteOrderEncoding(& This->order);
-       if(This->boolsToConstraints!= NULL) {
-               resetAndDeleteHashTableBoolConst(This->boolsToConstraints);
-               deleteHashTableBoolConst(This->boolsToConstraints);
+       if(This->orderPairTable != NULL) {
+               resetAndDeleteHashTableOrderPair(This->orderPairTable);
+               deleteHashTableOrderPair(This->orderPairTable);
        }
        ourfree(This);
 }

diff --git a/src/AST/order.h b/src/AST/order.h
index dcbfb313bc492de84302f84d3e96ecdf2dd0e63b..bb35603069b3bb857da0a46223cb24d7e890baa0 100644 (file)
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -10,7 +10,7 @@
 struct Order {
        OrderType type;
        Set * set;
-       HashTableBoolConst* boolsToConstraints;
+       HashTableOrderPair * orderPairTable;
        VectorBoolean constraints;
        OrderEncoding order;
 };

diff --git a/src/Backend/inc_solver.c b/src/Backend/inc_solver.c
index 0754fd94b8b4ca0f8e0d31ff7fa5d69c294dfec5..8a37343935e4df02cefcb38c35bbece9bd940c8b 100644 (file)
--- a/src/Backend/inc_solver.c
+++ b/src/Backend/inc_solver.c
@@ -81,7 +81,6 @@ int solve(IncrementalSolver * This) {
        return getSolution(This);
 }
 
-
 void startSolve(IncrementalSolver *This) {
        addClauseLiteral(This, IS_RUNSOLVER);
        flushBufferSolver(This);
@@ -173,11 +172,15 @@ void killSolver(IncrementalSolver * This) {
                waitpid(This->solver_pid, &status, 0);
        }
 }
+
+//DEBUGGING CODE STARTS
 bool first=true;
+//DEBUGGING CODE ENDS
 
 void flushBufferSolver(IncrementalSolver * This) {
        ssize_t bytestowrite=sizeof(int)*This->offset;
        ssize_t byteswritten=0;
+       //DEBUGGING CODE STARTS
        for(uint i=0;i<This->offset;i++) {
                if (first)
                        printf("(");
@@ -191,6 +194,7 @@ void flushBufferSolver(IncrementalSolver * This) {
                        printf("%d", This->buffer[i]);
                }
        }
+       //DEBUGGING CODE ENDS
        do {
                ssize_t n=write(This->to_solver_fd, &((char *)This->buffer)[byteswritten], bytestowrite);
                if (n == -1) {

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 1cf408d0ca404e15e67de8ae730bdd9854f3d6e2..4bc1d61f6fb370de10d9dc361a31a02639b698a3 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -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++){

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 0d6999fddb55cf7d3a3d5ea741e70d331003d11b..b9af8efb6ad520d31b6ce381e4b054f3bf23c91a 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -19,7 +19,7 @@ void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Edge*carray);
 Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint);
 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
 void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order);
-Edge getOrderConstraint(HashTableBoolConst *table, OrderPair *pair);
+Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair);
 Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ, Edge constJK, Edge constIK);
 Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
 Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);

diff --git a/src/Collections/structs.c b/src/Collections/structs.c
index 29c7abe0d5e7ba0809e6dfe40f12978f62b52c58..64821c9513a5020bee96da921ebae4c01953cf7e 100644 (file)
--- a/src/Collections/structs.c
+++ b/src/Collections/structs.c
@@ -29,4 +29,4 @@ static inline unsigned int order_pair_equals(OrderPair* key1, OrderPair* key2){
        return key1->first== key2->first && key1->second == key2->second;
 }
 
-HashTableImpl(BoolConst, OrderPair *, OrderPair *, order_pair_hash_Function, order_pair_equals, ourfree);
+HashTableImpl(OrderPair, OrderPair *, OrderPair *, order_pair_hash_Function, order_pair_equals, ourfree);

diff --git a/src/Collections/structs.h b/src/Collections/structs.h
index 86addfbe03c21704998f0c06049c63e2d8689cde..3a4e81a8a0e26e477d6ec4c67cb1427bcc9ca196 100644 (file)
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -22,7 +22,7 @@ VectorDef(ASTNode, ASTNode *);
 VectorDef(Int, uint64_t);
 
 HashTableDef(Void, void *, void *);
-HashTableDef(BoolConst, OrderPair *, OrderPair *);
+HashTableDef(OrderPair, OrderPair *, OrderPair *);
 
 HashSetDef(Void, void *);
 

diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
index 20cd5cd4668cdc001941a0c90b09adccc291a8c3..6740543ffaeef71821e83a5f0721310e1866295c 100644 (file)
--- a/src/Test/testcnf.c
+++ b/src/Test/testcnf.c
@@ -7,7 +7,6 @@ int main(int numargs, char ** argv) {
        Edge v2=constraintNewVar(cnf);
        Edge v3=constraintNewVar(cnf);
        Edge v4=constraintNewVar(cnf);
-       Edge v5=constraintNewVar(cnf);
 
        Edge nv1=constraintNegate(v1);
        Edge nv2=constraintNegate(v2);
@@ -18,7 +17,7 @@ int main(int numargs, char ** argv) {
        Edge c2=constraintAND2(cnf, v3, nv4);
        Edge c3=constraintAND2(cnf, nv1, v2);
        Edge c4=constraintAND2(cnf, nv3, v4);
-       Edge cor=constraintOR2(cnf, constraintAND2(cnf, c1, c2), v5);
+       Edge cor=constraintOR2(cnf, constraintAND2(cnf, c1, c2), constraintAND2(cnf, c3, c4));
        printCNF(cor);
        printf("\n");
        addConstraintCNF(cnf, cor);