From 0ce0953a85b3abf68656b0c8fd10d32f6936e6bd Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 11 Jul 2017 13:06:06 -0700 Subject: [PATCH] Renaming --- src/AST/order.c | 10 +++++----- src/AST/order.h | 2 +- src/Backend/inc_solver.c | 6 +++++- src/Backend/satencoder.c | 30 +++++++++++++++--------------- src/Backend/satencoder.h | 2 +- src/Collections/structs.c | 2 +- src/Collections/structs.h | 2 +- src/Test/testcnf.c | 3 +-- 8 files changed, 30 insertions(+), 27 deletions(-) diff --git a/src/AST/order.c b/src/AST/order.c index 1499dcb..92c52ae 100644 --- 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 dcbfb31..bb35603 100644 --- 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 0754fd9..8a37343 100644 --- 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;ioffset;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 1cf408d..4bc1d61 100644 --- 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; ifirst!= 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; ifirst== 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 86addfb..3a4e81a 100644 --- 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 20cd5cd..6740543 100644 --- 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); -- 2.34.1