edits

diff --git a/src/AST/element.h b/src/AST/element.h
index 5259c0907d54ad2104c13e074b1f82e73b9498a2..ac1ed2f63a51f11cd9932659b40fc15dab8c72b5 100644 (file)
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -35,7 +35,7 @@ public:
        Set *getRange() {return set;}
 protected:
        Set *set;
-
+       friend class ElementOpt;
 };
 
 class ElementConst : public ElementSet {

diff --git a/src/AST/set.cc b/src/AST/set.cc
index 9342484a21a81ce61e73cd14fae87a9148d9902c..67fe9e00aaff208c88afd9e82ffbd06a98df7638 100644 (file)
--- a/src/AST/set.cc
+++ b/src/AST/set.cc
@@ -59,7 +59,7 @@ uint64_t Set::getElement(uint index) {
                return low + index;
        else
                return members->get(index);
-        }
+}
 
 uint Set::getSize() {
        if (isRange) {

diff --git a/src/AST/set.h b/src/AST/set.h
index aaa8f3819a28a23daa21155308ca783b9f752b11..ca8533153f18cba94c3a4541fa030dbf4a8fdabc 100644 (file)
--- a/src/AST/set.h
+++ b/src/AST/set.h
@@ -35,6 +35,7 @@ protected:
        uint64_t low;   //also used to count unique items
        uint64_t high;
        Vector<uint64_t> *members;
+       friend class ElementOpt;
 };
 
 int intcompare(const void *p1, const void *p2);

diff --git a/src/ASTTransform/elementopt.cc b/src/ASTTransform/elementopt.cc
index c9ccc443531224c82bb51b87a5ebd54276f1364e..775a5d2bad7ea5cbc43df70e5856abc0c3bad377 100755 (executable)
--- 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)
 {
 }
 
@@ -59,7 +61,7 @@ void ElementOpt::processPredicate(BooleanPredicate * pred) {
        
        if (op == SATC_EQUALS) {
                handlePredicateEquals(pred, (ElementSet *) left, (ElementConst *) right);
-       } else {
+       } else if (updateSets) {
                handlePredicateInequality(pred, (ElementSet *) left, (ElementConst *) right);
        }
 }
@@ -67,13 +69,97 @@ 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 if (pred->isFalse() && updateSets) {
+               constrainVarWithConst(pred, left, right);
        } else ASSERT(0);
 }
 
-void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *left, ElementConst *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);
+}
+
+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);
 }
 
 void ElementOpt::replaceVarWithConst(BooleanPredicate * pred, ElementSet *var, ElementConst * value) {

diff --git a/src/ASTTransform/elementopt.h b/src/ASTTransform/elementopt.h
index 980bb87b75b43423d9984890b316a7063567463b..a1f6005f7736a5f62bb8ca046216e80688a7f39e 100755 (executable)
--- a/src/ASTTransform/elementopt.h
+++ b/src/ASTTransform/elementopt.h
@@ -15,7 +15,10 @@ private:
        void handlePredicateEquals(BooleanPredicate *pred, ElementSet *left, ElementConst *right);
        void handlePredicateInequality(BooleanPredicate *pred, ElementSet *left, ElementConst *right);
        void replaceVarWithConst(BooleanPredicate * pred, ElementSet *var, ElementConst * value);
+       void constrainVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value);
+
        Vector<BooleanPredicate *> workList;
+       bool updateSets;
 };
 
 #endif

diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index d88f2c7c36fcdaf762cbe9d8189ae2d96dd32133..2e526d376380a24fad6c994153b5dc9108c68cfc 100644 (file)
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -39,7 +39,7 @@ public:
 static TunableDesc onoff(0, 1, 1);
 static TunableDesc offon(0, 1, 0);
 
-enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT};
+enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT, ELEMENTOPTSETS};
 typedef enum Tunables Tunables;
 
 const char* tunableParameterToString(Tunables tunable);

diff --git a/src/csolver.h b/src/csolver.h
index 044f79e9a3693ea34c6c31e9eca4bad293ce0891..c916c58499992b73450e294a26531801b8cc6791 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -237,4 +237,20 @@ inline CompOp flipOp(CompOp op) {
        }
        ASSERT(0);
 }
+
+inline CompOp negateOp(CompOp op) {
+       switch (op) {
+       case SATC_EQUALS:
+               ASSERT(0);
+       case SATC_LT:
+               return SATC_GTE;
+       case SATC_GT:
+               return SATC_LTE;
+       case SATC_LTE:
+               return SATC_GT;
+       case SATC_GTE:
+               return SATC_LT;
+       }
+       ASSERT(0);
+}
 #endif