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){
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);
}
struct Order {
OrderType type;
Set * set;
- HashTableBoolConst* boolsToConstraints;
+ HashTableOrderPair * orderPairTable;
VectorBoolean constraints;
OrderEncoding order;
};
return getSolution(This);
}
-
void startSolve(IncrementalSolver *This) {
addClauseLiteral(This, IS_RUNSOLVER);
flushBufferSolver(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("(");
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) {
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
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++){
}
}
-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
// 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++){
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);
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);
VectorDef(Int, uint64_t);
HashTableDef(Void, void *, void *);
-HashTableDef(BoolConst, OrderPair *, OrderPair *);
+HashTableDef(OrderPair, OrderPair *, OrderPair *);
HashSetDef(Void, void *);
Edge v2=constraintNewVar(cnf);
Edge v3=constraintNewVar(cnf);
Edge v4=constraintNewVar(cnf);
- Edge v5=constraintNewVar(cnf);
Edge nv1=constraintNegate(v1);
Edge nv2=constraintNegate(v2);
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);