booledgeMap.reset();
}
-int SATEncoder::solve() {
+int SATEncoder::solve(long timeout) {
+ cnf->solver->timeout = timeout;
return solveCNF(cnf);
}
void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
+ if(csolver->isUnSAT()){
+ return;
+ }
SetIteratorBooleanEdge *iterator = csolver->getConstraints();
while (iterator->hasNext()) {
BooleanEdge constraint = iterator->next();
- model_print("**********************************************************\n");
- constraint.print();
- model_print("\n");
Edge c = encodeConstraintSATEncoder(constraint);
- model_print("&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&\n");
- printCNF(c);
- model_print("\n");
addConstraintCNF(cnf, c);
}
delete iterator;