continue;
ASSERT(simp->type!=FALSE);
dumpConstraint(simp, satSolver);
+ freerecConstraint(simp);
}
deleteVectorConstraint(simplified);
}
for(uint i=0;i<size;i++) {
Boolean *constraint=getVectorBoolean(constraints, i);
Constraint* c= encodeConstraintSATEncoder(This, constraint);
- addConstraintToSATSolver(c, This->satSolver);
printConstraint(c);
model_print("\n\n");
+ addConstraintToSATSolver(c, This->satSolver);
//FIXME: When do we want to delete constraints? Should we keep an array of them
// and delete them later, or it would be better to just delete them right away?
}
Constraint * constraint;
if (!containsBoolConst(table, pair)) {
constraint = getNewVarSATEncoder(This);
- OrderPair * paircopy = allocOrderPair(pair->first, pair->second);
- putBoolConst(table, paircopy, constraint);
+ OrderPair * paircopy = allocOrderPair(pair->first, pair->second, constraint);
+ putBoolConst(table, paircopy, paircopy);
} else
- constraint = getBoolConst(table, pair);
+ constraint = getBoolConst(table, pair)->constraint;
if (negate)
return negateConstraint(constraint);
else
return createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
}
HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
- OrderPair pair={boolOrder->first, boolOrder->second};
- Constraint* constraint = getPairConstraint(This, boolToConsts, & pair);
- ASSERT(constraint != NULL);
+ OrderPair pair={boolOrder->first, boolOrder->second, NULL};
+ Constraint *constraint = getPairConstraint(This, boolToConsts, & pair);
return constraint;
}
Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
ASSERT(pair->first!= pair->second);
- Constraint* constraint= getBoolConst(table, pair);
- ASSERT(constraint!= NULL);
+ Constraint* constraint= getBoolConst(table, pair)->constraint;
if(pair->first > pair->second)
return constraint;
else