Adding checks to avoid further processing on UNSAT Problems

[satune.git] / src / Backend / satencoder.cc

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 4c49b16442950ea1aa7142afe87cd32b1a244cc0..618b8c17c22114177393754313dda6a3c1d8aa5c 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -29,21 +29,19 @@ void SATEncoder::resetSATEncoder() {
        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;