int SATEncoder::solve(long timeout) {
cnf->solver->timeout = timeout;
+ long long startTime = getTimeNano();
+ finishedClauses(cnf->solver);
+ cnf->encodeTime = getTimeNano() - startTime;
+ if(solver->isIncrementalMode()){
+ solver->freezeElementsVariables();
+ }
return solveCNF(cnf);
}
SetIteratorBooleanEdge *iterator = csolver->getConstraints();
while (iterator->hasNext()) {
BooleanEdge constraint = iterator->next();
- Edge c = encodeConstraintSATEncoder(constraint);
- addConstraintCNF(cnf, c);
+ if(!csolver->isConstraintEncoded(constraint)){
+ Edge c = encodeConstraintSATEncoder(constraint);
+ addConstraintCNF(cnf, c);
+ csolver->addEncodedConstraint(constraint);
+ }
}
delete iterator;
}