Adding checks to avoid further processing on UNSAT Problems

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

diff --git a/src/ASTTransform/preprocess.cc b/src/ASTTransform/preprocess.cc
index 00d324e9e3e21b2c10ce041acdba3afc4e2af242..ca2a655987b6395b286e045bb72e281c995d4f82 100644 (file)
--- a/src/ASTTransform/preprocess.cc
+++ b/src/ASTTransform/preprocess.cc
@@ -2,9 +2,10 @@
 #include "boolean.h"
 #include "csolver.h"
 #include "tunable.h"
+#include "iterator.h"
 
 Preprocess::Preprocess(CSolver *_solver)
-        : Transform(_solver)
+       : Transform(_solver)
 {
 }
 
@@ -12,21 +13,20 @@ Preprocess::~Preprocess() {
 }
 
 void Preprocess::doTransform() {
-       if (solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
+       if (solver->isUnSAT() || !solver->isBooleanVarUsed() || solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
                return;
-       
-       SetIteratorBooleanEdge *iterator = solver->getConstraints();
-       while (iterator->hasNext()) {
-               BooleanEdge boolean = iterator->next();
-               Boolean *b = boolean.getBoolean();
-               transformBoolean(b);
+
+       BooleanIterator bit(solver);
+       while (bit.hasNext()) {
+               Boolean *b = bit.next();
+               if (b->type == BOOLEANVAR)
+                       processBooleanVar((BooleanVar *)b);
        }
-       delete iterator;
        resolveBooleanVars();
 }
 
 void Preprocess::resolveBooleanVars() {
-       SetIteratorBoolean * iterator = toremove.iterator();
+       SetIteratorBoolean *iterator = toremove.iterator();
        while (iterator->hasNext()) {
                BooleanVar *bv = (BooleanVar *) iterator->next();
                if (bv->polarity == P_TRUE) {
@@ -38,29 +38,9 @@ void Preprocess::resolveBooleanVars() {
        delete iterator;
 }
 
-void Preprocess::transformBoolean(Boolean *b) {
-       if (!processed.add(b))
-               return;
-       switch (b->type) {
-       case BOOLEANVAR:
-               processBooleanVar((BooleanVar *)b);
-               break;
-       case LOGICOP:
-               processLogicOp((BooleanLogic *)b);
-               break;
-       default:
-               break;
-       }
-}
-
-void Preprocess::processBooleanVar(BooleanVar * b) {
-       if (b->polarity==P_TRUE ||
-                       b->polarity==P_FALSE) {
+void Preprocess::processBooleanVar(BooleanVar *b) {
+       if (b->polarity == P_TRUE ||
+                       b->polarity == P_FALSE) {
                toremove.add(b);
        }
 }
-
-void Preprocess::processLogicOp(BooleanLogic * b) {
-       for(uint i=0; i < b->inputs.getSize(); i++)
-               transformBoolean(b->inputs.get(i).getBoolean());
-}