From 3ecf79a7ceb011a9f0aff7345b7122bee540a31a Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 24 Jul 2018 12:55:59 -0700 Subject: [PATCH] edits --- src/AST/element.h | 2 +- src/AST/set.cc | 2 +- src/AST/set.h | 1 + src/ASTTransform/elementopt.cc | 96 ++++++++++++++++++++++++++++++++-- src/ASTTransform/elementopt.h | 3 ++ src/Tuner/tunable.h | 2 +- src/csolver.h | 16 ++++++ 7 files changed, 114 insertions(+), 8 deletions(-) diff --git a/src/AST/element.h b/src/AST/element.h index 5259c09..ac1ed2f 100644 --- 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 9342484..67fe9e0 100644 --- 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 aaa8f38..ca85331 100644 --- 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 *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 c9ccc44..775a5d2 100755 --- 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; igetElement(i); + if (val >= cvalue) + elemArray[count++] = val; + } + break; + } + case SATC_GT: { + for(uint i=0; igetElement(i); + if (val <= cvalue) + elemArray[count++] = val; + } + break; + } + case SATC_LTE: { + for(uint i=0; igetElement(i); + if (val > cvalue) + elemArray[count++] = val; + } + break; + } + case SATC_GTE: { + for(uint i=0; igetElement(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; igetElement(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 980bb87..a1f6005 100755 --- 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 workList; + bool updateSets; }; #endif diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h index d88f2c7..2e526d3 100644 --- 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 044f79e..c916c58 100644 --- 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 -- 2.34.1