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 c9ccc44..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)
 {
 }
 
@@ -17,7 +19,7 @@ ElementOpt::~ElementOpt() {
 void ElementOpt::doTransform() {
        if (solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
                return;
-       
+
        SetIteratorBooleanEdge *iterator = solver->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge constraint = iterator->next();
@@ -25,41 +27,41 @@ void ElementOpt::doTransform() {
                        workList.push((BooleanPredicate *)constraint.getBoolean());
        }
        while (workList.getSize() != 0) {
-               BooleanPredicate * pred = workList.last(); workList.pop();
+               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;
+               Element *tmp = left;
                left = right;
                right = tmp;
                op = flipOp(op);
        } else if (right->type != ELEMCONST)
                return;
 
-       if (left->type !=ELEMSET)
+       if (left->type != ELEMSET)
                return;
-       
+
        if (op == SATC_EQUALS) {
                handlePredicateEquals(pred, (ElementSet *) left, (ElementConst *) right);
-       } else {
+       } else if (updateSets) {
                handlePredicateInequality(pred, (ElementSet *) left, (ElementConst *) right);
        }
 }
@@ -67,28 +69,123 @@ void ElementOpt::processPredicate(BooleanPredicate * pred) {
 void ElementOpt::handlePredicateEquals(BooleanPredicate *pred, ElementSet *left, ElementConst *right) {
        if (pred->isTrue()) {
                replaceVarWithConst(pred, left, right);
-       } else if (pred->isFalse()) {
-               
-       } else ASSERT(0);
+       } 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;
+
+       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);
+       }
 }
 
-void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *left, ElementConst *right) {
+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) {
+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);
+       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);
+                       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);
-                                       workList.push(newpred);
+                                       if (newpred->isTrue() || newpred->isFalse())
+                                               workList.push(newpred);
                                        break;
                                }
                        }