bug fix

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

diff --git a/src/ASTTransform/elementopt.cc b/src/ASTTransform/elementopt.cc
old mode 100755 (executable)
new mode 100644 (file)
index 5fa38e6..b0866ed
--- a/src/ASTTransform/elementopt.cc
+++ b/src/ASTTransform/elementopt.cc
@@ -5,9 +5,11 @@
 #include "boolean.h"
 #include "element.h"
 #include "predicate.h"
+#include "set.h"
 
 ElementOpt::ElementOpt(CSolver *_solver)
-       : Transform(_solver)
+       : Transform(_solver),
+       updateSets(solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1)
 {
 }
 
@@ -18,34 +20,175 @@ void ElementOpt::doTransform() {
        if (solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
                return;
 
-       BooleanIterator bit(solver);
-       while (bit.hasNext()) {
-               Boolean *b = bit.next();
-               if (b->type == PREDICATEOP)
-                       processPredicate((BooleanPredicate *)b);
+       SetIteratorBooleanEdge *iterator = solver->getConstraints();
+       while (iterator->hasNext()) {
+               BooleanEdge constraint = iterator->next();
+               if (constraint->type == PREDICATEOP)
+                       workList.push((BooleanPredicate *)constraint.getBoolean());
        }
+       while (workList.getSize() != 0) {
+               BooleanPredicate *pred = workList.last(); workList.pop();
+               processPredicate(pred);
+       }
+       delete iterator;
 }
 
-void ElementOpt::processPredicate(BooleanPredicate * pred) {
+void ElementOpt::processPredicate(BooleanPredicate *pred) {
        uint numInputs = pred->inputs.getSize();
        if (numInputs != 2)
                return;
 
-       Predicate * p = pred->getPredicate();
+       Predicate *p = pred->getPredicate();
        if (p->type == TABLEPRED)
-                       return;
+               return;
 
-       PredicateOperator * pop = (PredicateOperator *) p;
+       PredicateOperator *pop = (PredicateOperator *) p;
        CompOp op = pop->getOp();
 
-       Element * left = pred->inputs.get(0);
-       Element * right = pred->inputs.get(1);
+       Element *left = pred->inputs.get(0);
+       Element *right = pred->inputs.get(1);
 
        if (left->type == ELEMCONST) {
+               Element *tmp = left;
+               left = right;
+               right = tmp;
+               op = flipOp(op);
+       } else if (right->type != ELEMCONST)
+               return;
+
+       if (left->type != ELEMSET)
+               return;
+
+       if (op == SATC_EQUALS) {
+               handlePredicateEquals(pred, (ElementSet *) left, (ElementConst *) right);
+       } else if (updateSets) {
+               handlePredicateInequality(pred, (ElementSet *) left, (ElementConst *) right);
+       }
+}
+
+void ElementOpt::handlePredicateEquals(BooleanPredicate *pred, ElementSet *left, ElementConst *right) {
+       if (pred->isTrue()) {
+               replaceVarWithConst(pred, left, right);
+       } else if (pred->isFalse() && updateSets) {
+               constrainVarWithConst(pred, left, right);
+       }
+}
+
+void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
+       Predicate *p = pred->getPredicate();
+       PredicateOperator *pop = (PredicateOperator *) p;
+       CompOp op = pop->getOp();
+
+       if (pred->isFalse()) {
+               op = negateOp(op);
+       } else if (!pred->isTrue()) {
+               ASSERT(0);
+       }
+
+       Set *s = var->getRange();
+       if (s->isRange)
+               return;
+
+       uint size = s->getSize();
+       uint64_t elemArray[size];
+       uint count = 0;
+       uint64_t cvalue = value->value;
 
-       } else if (right->type == ELEMCONST) {
+       switch (op) {
+       case SATC_LT: {
+               for (uint i = 0; i < size; i++) {
+                       uint64_t val = s->getElement(i);
+                       if (val < cvalue)
+                               elemArray[count++] = val;
+               }
+               break;
+       }
+       case SATC_GT: {
+               for (uint i = 0; i < size; i++) {
+                       uint64_t val = s->getElement(i);
+                       if (val > cvalue)
+                               elemArray[count++] = val;
+               }
+               break;
+       }
+       case SATC_LTE: {
+               for (uint i = 0; i < size; i++) {
+                       uint64_t val = s->getElement(i);
+                       if (val <= cvalue)
+                               elemArray[count++] = val;
+               }
+               break;
+       }
+       case SATC_GTE: {
+               for (uint i = 0; i < size; i++) {
+                       uint64_t val = s->getElement(i);
+                       if (val >= cvalue)
+                               elemArray[count++] = val;
+               }
+               break;
+       }
+
+       default:
+               ASSERT(0);
+       }
+       if (size == count)
+               return;
+
+       Set *newset = solver->createSet(s->type, elemArray, count);
+       solver->elemMap.remove(var);
+       var->set = newset;
+       solver->elemMap.put(var, var);
+
+       if (count == 1) {
+               ElementConst *elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
+               replaceVarWithConst(pred, var, elemconst);
+       }
+}
 
-       } else {
+void ElementOpt::constrainVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
+       Set *s = var->getRange();
+       if (s->isRange)
                return;
+       uint size = s->getSize();
+       uint64_t elemArray[size];
+       uint count = 0;
+       uint64_t cvalue = value->value;
+       for (uint i = 0; i < size; i++) {
+               uint64_t val = s->getElement(i);
+               if (val != cvalue)
+                       elemArray[count++] = val;
+       }
+       if (size == count)
+               return;
+
+       Set *newset = solver->createSet(s->type, elemArray, count);
+       solver->elemMap.remove(var);
+       var->set = newset;
+       solver->elemMap.put(var, var);
+
+       if (count == 1) {
+               ElementConst *elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
+               replaceVarWithConst(pred, var, elemconst);
+       }
+}
+
+void ElementOpt::replaceVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
+       uint size = var->parents.getSize();
+       for (uint i = 0; i < size; i++) {
+               ASTNode *parent = var->parents.get(i);
+               if (parent->type == PREDICATEOP && pred != parent) {
+                       BooleanPredicate *newpred = (BooleanPredicate *) parent;
+                       for (uint j = 0; j < newpred->inputs.getSize(); j++) {
+                               Element *e = newpred->inputs.get(j);
+                               if (e == var) {
+                                       solver->boolMap.remove(newpred);
+                                       newpred->inputs.set(j, value);
+                                       solver->boolMap.put(newpred, newpred);
+                                       if (newpred->isTrue() || newpred->isFalse())
+                                               workList.push(newpred);
+                                       break;
+                               }
+                       }
+               }
        }
 }