X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FBackend%2Fsatencoder.cc;h=618b8c17c22114177393754313dda6a3c1d8aa5c;hp=4c49b16442950ea1aa7142afe87cd32b1a244cc0;hb=cbd921ee35b6a29934fd7cecccde7f160228af17;hpb=cb27924ba5a3ef99d44a1e0cbdd43906b2a28d61

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 4c49b16..618b8c1 100644
--- 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;