Incremental solver works and the test case passes

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

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 00219efe24ece732c6aeb57ed3ba450ded890dee..5312b4f7266d7f2812378a63195e04ce705e8325 100755 (executable)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -31,6 +31,12 @@ void SATEncoder::resetSATEncoder() {
 
 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);
 }
 
@@ -41,8 +47,11 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
        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;
 }