more code

diff --git a/src/ASTTransform/elementopt.cc b/src/ASTTransform/elementopt.cc
index 5fa38e6684cf2baf772e2440654df485575f7263..c9ccc443531224c82bb51b87a5ebd54276f1364e 100755 (executable)
--- a/src/ASTTransform/elementopt.cc
+++ b/src/ASTTransform/elementopt.cc
@@ -17,13 +17,18 @@ ElementOpt::~ElementOpt() {
 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) {
@@ -42,10 +47,51 @@ void ElementOpt::processPredicate(BooleanPredicate * pred) {
        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;
 
-       } else if (right->type == ELEMCONST) {
-
-       } else {
+       if (left->type !=ELEMSET)
                return;
+       
+       if (op == SATC_EQUALS) {
+               handlePredicateEquals(pred, (ElementSet *) left, (ElementConst *) right);
+       } else {
+               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()) {
+               
+       } else ASSERT(0);
+}
+
+void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *left, ElementConst *right) {
+
+}
+
+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);
+                                       workList.push(newpred);
+                                       break;
+                               }
+                       }
+               }
        }
 }

diff --git a/src/ASTTransform/elementopt.h b/src/ASTTransform/elementopt.h
index ad6e7902dd05004bec307e2c364d732260c584da..980bb87b75b43423d9984890b316a7063567463b 100755 (executable)
--- a/src/ASTTransform/elementopt.h
+++ b/src/ASTTransform/elementopt.h
@@ -12,6 +12,10 @@ public:
        CMEMALLOC;
 private:
        void processPredicate(BooleanPredicate *);
+       void handlePredicateEquals(BooleanPredicate *pred, ElementSet *left, ElementConst *right);
+       void handlePredicateInequality(BooleanPredicate *pred, ElementSet *left, ElementConst *right);
+       void replaceVarWithConst(BooleanPredicate * pred, ElementSet *var, ElementConst * value);
+       Vector<BooleanPredicate *> workList;
 };
 
 #endif

diff --git a/src/csolver.h b/src/csolver.h
index e02e3407c626928aa9a810a96518ad951a5d5c16..044f79e9a3693ea34c6c31e9eca4bad293ce0891 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -57,7 +57,7 @@ public:
 
        Set *getElementRange (Element *element);
 
-        void mustHaveValue(Element *element);
+       void mustHaveValue(Element *element);
         
        BooleanEdge getBooleanTrue();
 
@@ -159,7 +159,6 @@ public:
        void replaceBooleanWithFalse(BooleanEdge bexpr);
        void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
        CSolver *clone();
-//        Set* addItemsToRange(Element* element, uint num, ...);
        void serialize();
        static CSolver *deserialize(const char *file);
        void autoTune(uint budget);
@@ -220,5 +219,22 @@ private:
        bool unsat;
        Tuner *tuner;
        long long elapsedTime;
+       friend class ElementOpt;
 };
+
+inline CompOp flipOp(CompOp op) {
+       switch (op) {
+       case SATC_EQUALS:
+               return SATC_EQUALS;
+       case SATC_LT:
+               return SATC_GT;
+       case SATC_GT:
+               return SATC_LT;
+       case SATC_LTE:
+               return SATC_GTE;
+       case SATC_GTE:
+               return SATC_LTE;
+       }
+       ASSERT(0);
+}
 #endif