sparse or decompose

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

diff --git a/src/ASTTransform/preprocess.cc b/src/ASTTransform/preprocess.cc
index a23d918e600833b534187f84f08fc60d1ac1201d..ca2a655987b6395b286e045bb72e281c995d4f82 100644 (file)
--- a/src/ASTTransform/preprocess.cc
+++ b/src/ASTTransform/preprocess.cc
@@ -5,7 +5,7 @@
 #include "iterator.h"
 
 Preprocess::Preprocess(CSolver *_solver)
-        : Transform(_solver)
+       : Transform(_solver)
 {
 }
 
@@ -13,12 +13,12 @@ Preprocess::~Preprocess() {
 }
 
 void Preprocess::doTransform() {
-       if (solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
+       if (solver->isUnSAT() || !solver->isBooleanVarUsed() || solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
                return;
-       
+
        BooleanIterator bit(solver);
-       while(bit.hasNext()) {
-               Boolean *b=bit.next();
+       while (bit.hasNext()) {
+               Boolean *b = bit.next();
                if (b->type == BOOLEANVAR)
                        processBooleanVar((BooleanVar *)b);
        }
@@ -26,7 +26,7 @@ void Preprocess::doTransform() {
 }
 
 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,9 +38,9 @@ void Preprocess::resolveBooleanVars() {
        delete iterator;
 }
 
-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);
        }
 }