ElementOpt::ElementOpt(CSolver *_solver)
: Transform(_solver),
- updateSets(solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1)
+ 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 if (updateSets) {
}
void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
- Predicate * p = pred->getPredicate();
- PredicateOperator * pop = (PredicateOperator *) p;
+ Predicate *p = pred->getPredicate();
+ PredicateOperator *pop = (PredicateOperator *) p;
CompOp op = pop->getOp();
if (pred->isFalse()) {
ASSERT(0);
}
- Set * s = var->getRange();
+ 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) {
+ switch (op) {
case SATC_LT: {
- for(uint i=0; i<size; i++) {
+ 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++) {
+ 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++) {
+ 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++) {
+ 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]);
+ 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();
+ 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++) {
+ for (uint i = 0; i < size; i++) {
uint64_t val = s->getElement(i);
if (val != cvalue)
elemArray[count++] = val;
solver->elemMap.put(var, var);
if (count == 1) {
- ElementConst * elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
+ 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;
}
}