Adding checks to avoid further processing on UNSAT Problems

[satune.git] / src / ASTTransform / elementopt.cc

diff --git a/src/ASTTransform/elementopt.cc b/src/ASTTransform/elementopt.cc
index 6fec15597d29f84d21b7cef38130ee7467eca364..899f6591c2b4ce4a7eed0f18e8e1134d73895b4f 100644 (file)
--- a/src/ASTTransform/elementopt.cc
+++ b/src/ASTTransform/elementopt.cc
@@ -9,7 +9,7 @@
 
 ElementOpt::ElementOpt(CSolver *_solver)
        : Transform(_solver),
-       updateSets(solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1)
+         updateSets(false)
 {
 }
 
@@ -17,9 +17,12 @@ ElementOpt::~ElementOpt() {
 }
 
 void ElementOpt::doTransform() {
-       if (solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
+       if (solver->isUnSAT() || solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
                return;
 
+       //Set once we know we are going to use it.
+       updateSets = solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1;
+       
        SetIteratorBooleanEdge *iterator = solver->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge constraint = iterator->next();
@@ -71,7 +74,7 @@ void ElementOpt::handlePredicateEquals(BooleanPredicate *pred, ElementSet *left,
                replaceVarWithConst(pred, left, right);
        } else if (pred->isFalse() && updateSets) {
                constrainVarWithConst(pred, left, right);
-       } else ASSERT(0);
+       }
 }
 
 void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
@@ -184,7 +187,8 @@ void ElementOpt::replaceVarWithConst(BooleanPredicate *pred, ElementSet *var, El
                                        solver->boolMap.remove(newpred);
                                        newpred->inputs.set(j, value);
                                        solver->boolMap.put(newpred, newpred);
-                                       workList.push(newpred);
+                                       if (newpred->isTrue() || newpred->isFalse())
+                                               workList.push(newpred);
                                        break;
                                }
                        }