-void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This) {
- HSIteratorBoolean *iterator=csolver->getConstraints();
- while(iterator->hasNext()) {
- Boolean *constraint = iterator->next();
- model_print("Encoding All ...\n\n");
- Edge c = encodeConstraintSATEncoder(This, constraint);
- model_print("Returned Constraint in EncodingAll:\n");
- ASSERT( ! equalsEdge(c, E_BOGUS));
- addConstraintCNF(This->cnf, c);
+void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
+ if(csolver->isUnSAT()){
+ return;
+ }
+ SetIteratorBooleanEdge *iterator = csolver->getConstraints();
+ while (iterator->hasNext()) {
+ BooleanEdge constraint = iterator->next();
+ Edge c = encodeConstraintSATEncoder(constraint);
+ addConstraintCNF(cnf, c);