remove redundant sets

[satune.git] / src / AST / iterator.cc

diff --git a/src/AST/iterator.cc b/src/AST/iterator.cc
index ac81e96ad8fe8b91b1f86a1b4628e932725aa64c..03b368fd714d7a33978c21876f8980afe45db3d9 100644 (file)
--- a/src/AST/iterator.cc
+++ b/src/AST/iterator.cc
@@ -1,8 +1,9 @@
 #include "iterator.h"
 #include "boolean.h"
+#include "element.h"
 #include "csolver.h"
 
-BooleanIterator::BooleanIterator(CSolver * _solver) :
+BooleanIterator::BooleanIterator(CSolver *_solver) :
        solverit(_solver->getConstraints()) {
        updateNext();
 }
@@ -20,11 +21,11 @@ void BooleanIterator::updateNext() {
                boolean.pop();
                index.pop();
        }
-       
-       while(true) {
+
+       while (true) {
                if (boolean.getSize() == 0) {
                        if (solverit->hasNext()) {
-                               Boolean *b=solverit->next().getBoolean();
+                               Boolean *b = solverit->next().getBoolean();
                                if (discovered.add(b)) {
                                        boolean.push(b);
                                        index.push(0);
@@ -33,24 +34,24 @@ void BooleanIterator::updateNext() {
                        } else
                                return;
                }
-               Boolean *topboolean=boolean.last();
-               uint topindex=index.last();
-               switch(topboolean->type) {
+               Boolean *topboolean = boolean.last();
+               uint topindex = index.last();
+               switch (topboolean->type) {
                case ORDERCONST:
                case BOOLEANVAR:
                case PREDICATEOP:
                case BOOLCONST:
                        return;
                case LOGICOP: {
-                       BooleanLogic * logicop=(BooleanLogic*) topboolean;
-                       uint size=logicop->inputs.getSize();
+                       BooleanLogic *logicop = (BooleanLogic *) topboolean;
+                       uint size = logicop->inputs.getSize();
                        if (topindex == size)
                                return;
                        index.pop();
-                       index.push(topindex+1);
-                       Boolean *newchild=logicop->inputs.get(topindex).getBoolean();
+                       index.push(topindex + 1);
+                       Boolean *newchild = logicop->inputs.get(topindex).getBoolean();
                        if (discovered.add(newchild)) {
-                               boolean.push(logicop->inputs.get(topindex).getBoolean());
+                               boolean.push(newchild);
                                index.push(0);
                        }
                        break;
@@ -61,8 +62,87 @@ void BooleanIterator::updateNext() {
        }
 }
 
-Boolean * BooleanIterator::next() {
-       Boolean * b = boolean.last();
+Boolean *BooleanIterator::next() {
+       Boolean *b = boolean.last();
        updateNext();
        return b;
 }
+
+ElementIterator::ElementIterator(CSolver *_solver) :
+       bit(_solver),
+       base(NULL),
+       baseindex(0) {
+       updateNext();
+}
+
+ElementIterator::~ElementIterator() {
+}
+
+bool ElementIterator::hasNext() {
+       return element.getSize() != 0;
+}
+
+void ElementIterator::updateNext() {
+       if (element.getSize() != 0) {
+               element.pop();
+               index.pop();
+       }
+
+       while (true) {
+               if (element.getSize() == 0) {
+                       if (base != NULL) {
+                               if (baseindex == base->inputs.getSize()) {
+                                       base = NULL;
+                                       continue;
+                               } else {
+                                       Element *e = base->inputs.get(baseindex);
+                                       baseindex++;
+                                       if (discovered.add(e)) {
+                                               element.push(e);
+                                               index.push(0);
+                                       } else
+                                               continue;
+                               }
+                       } else {
+                               if (bit.hasNext()) {
+                                       Boolean *b = bit.next();
+                                       if (b->type == PREDICATEOP) {
+                                               base = (BooleanPredicate *)b;
+                                               baseindex = 0;
+                                       }
+                                       continue;
+                               } else
+                                       return;
+                       }
+               }
+               Element *topelement = element.last();
+               uint topindex = index.last();
+               switch (topelement->type) {
+               case ELEMSET:
+               case ELEMCONST:
+                       return;
+               case ELEMFUNCRETURN: {
+                       ElementFunction *func = (ElementFunction *) topelement;
+                       uint size = func->inputs.getSize();
+                       if (topindex == size)
+                               return;
+                       index.pop();
+                       index.push(topindex + 1);
+                       Element *newchild = func->inputs.get(topindex);
+                       if (discovered.add(newchild)) {
+                               element.push(newchild);
+                               index.push(0);
+                       }
+                       break;
+               }
+               default:
+                       ASSERT(0);
+               }
+       }
+}
+
+Element *ElementIterator::next() {
+       Element *e = element.last();
+       updateNext();
+       return e;
+}