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 dde77c14e4b938118dcfc855a54a1915a2504f57..618b8c17c22114177393754313dda6a3c1d8aa5c 100644 (file)
--- 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,11 +29,15 @@ 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();
@@ -74,14 +78,12 @@ Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
        }
        Polarity p = constraint->polarity;
        uint pSize = constraint->parents.getSize();
-       if (solver->getTuner()->getTunable(PROXYVARIABLE, &offon) == 1) {
-//     if ((pSize > 1 && p != P_BOTHTRUEFALSE ) || pSize > 2) {
+
+       if ( !edgeIsVarConst(result) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter) ) {
                Edge e = getNewVarSATEncoder();
                generateProxy(cnf, result, e, p);
                booledgeMap.put(constraint, e.node_ptr);
                result = e;
-       } else{
-               booledgeMap.put(constraint, result.node_ptr);
        }
 
        return c.isNegated() ? constraintNegate(result) : result;