X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FBackend%2Fsatencoder.cc;h=5312b4f7266d7f2812378a63195e04ce705e8325;hp=b13541d63c3f7411964f3b2c38f29eff24f23999;hb=3a614d0deec343d2474efaabaa7220e7bcbed0d0;hpb=ca8d8a586f64af922025ab69de7b853b5f331a49

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
old mode 100644
new mode 100755
index b13541d..5312b4f
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -16,7 +16,7 @@
 SATEncoder::SATEncoder(CSolver *_solver) :
 	cnf(createCNF()),
 	solver(_solver),
-  vector(allocDefVectorEdge()) {
+	vector(allocDefVectorEdge()) {
 }
 
 SATEncoder::~SATEncoder() {
@@ -29,16 +29,29 @@ void SATEncoder::resetSATEncoder() {
 	booledgeMap.reset();
 }
 
-int SATEncoder::solve() {
+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);
 }
 
 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);
+		if(!csolver->isConstraintEncoded(constraint)){
+			Edge c = encodeConstraintSATEncoder(constraint);
+			addConstraintCNF(cnf, c);
+			csolver->addEncodedConstraint(constraint);
+		}
 	}
 	delete iterator;
 }