#include "boolean.h"
#include "element.h"
#include "predicate.h"
+#include "set.h"
ElementOpt::ElementOpt(CSolver *_solver)
- : Transform(_solver)
+ : Transform(_solver),
+ updateSets(false)
{
}
}
void ElementOpt::doTransform() {
- if (solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
+ if (solver->isUnSAT() || solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
return;
-
+
+ //Set once we know we are going to use it.
+ updateSets = solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1;
+
SetIteratorBooleanEdge *iterator = solver->getConstraints();
while (iterator->hasNext()) {
BooleanEdge constraint = iterator->next();
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);
}
}
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 *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);
+
+ if (count == 1) {
+ ElementConst *elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
+ replaceVarWithConst(pred, var, elemconst);
+ }
+}
+
+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;
}
}