1 #include "elementopt.h"
10 ElementOpt::ElementOpt(CSolver *_solver)
12 updateSets(solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1)
16 ElementOpt::~ElementOpt() {
19 void ElementOpt::doTransform() {
20 if (solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
23 SetIteratorBooleanEdge *iterator = solver->getConstraints();
24 while (iterator->hasNext()) {
25 BooleanEdge constraint = iterator->next();
26 if (constraint->type == PREDICATEOP)
27 workList.push((BooleanPredicate *)constraint.getBoolean());
29 while (workList.getSize() != 0) {
30 BooleanPredicate * pred = workList.last(); workList.pop();
31 processPredicate(pred);
36 void ElementOpt::processPredicate(BooleanPredicate * pred) {
37 uint numInputs = pred->inputs.getSize();
41 Predicate * p = pred->getPredicate();
42 if (p->type == TABLEPRED)
45 PredicateOperator * pop = (PredicateOperator *) p;
46 CompOp op = pop->getOp();
48 Element * left = pred->inputs.get(0);
49 Element * right = pred->inputs.get(1);
51 if (left->type == ELEMCONST) {
56 } else if (right->type != ELEMCONST)
59 if (left->type !=ELEMSET)
62 if (op == SATC_EQUALS) {
63 handlePredicateEquals(pred, (ElementSet *) left, (ElementConst *) right);
64 } else if (updateSets) {
65 handlePredicateInequality(pred, (ElementSet *) left, (ElementConst *) right);
69 void ElementOpt::handlePredicateEquals(BooleanPredicate *pred, ElementSet *left, ElementConst *right) {
71 replaceVarWithConst(pred, left, right);
72 } else if (pred->isFalse() && updateSets) {
73 constrainVarWithConst(pred, left, right);
77 void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
78 Predicate * p = pred->getPredicate();
79 PredicateOperator * pop = (PredicateOperator *) p;
80 CompOp op = pop->getOp();
82 if (pred->isFalse()) {
84 } else if (!pred->isTrue()) {
88 Set * s = var->getRange();
92 uint size = s->getSize();
93 uint64_t elemArray[size];
95 uint64_t cvalue = value->value;
99 for(uint i=0; i<size; i++) {
100 uint64_t val = s->getElement(i);
102 elemArray[count++] = val;
107 for(uint i=0; i<size; i++) {
108 uint64_t val = s->getElement(i);
110 elemArray[count++] = val;
115 for(uint i=0; i<size; i++) {
116 uint64_t val = s->getElement(i);
118 elemArray[count++] = val;
123 for(uint i=0; i<size; i++) {
124 uint64_t val = s->getElement(i);
126 elemArray[count++] = val;
137 Set *newset = solver->createSet(s->type, elemArray, count);
138 solver->elemMap.remove(var);
140 solver->elemMap.put(var, var);
143 ElementConst * elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
144 replaceVarWithConst(pred, var, elemconst);
148 void ElementOpt::constrainVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
149 Set * s = var->getRange();
152 uint size = s->getSize();
153 uint64_t elemArray[size];
155 uint64_t cvalue = value->value;
156 for(uint i=0; i<size; i++) {
157 uint64_t val = s->getElement(i);
159 elemArray[count++] = val;
164 Set *newset = solver->createSet(s->type, elemArray, count);
165 solver->elemMap.remove(var);
167 solver->elemMap.put(var, var);
170 ElementConst * elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
171 replaceVarWithConst(pred, var, elemconst);
175 void ElementOpt::replaceVarWithConst(BooleanPredicate * pred, ElementSet *var, ElementConst * value) {
176 uint size = var->parents.getSize();
177 for(uint i=0; i < size; i++) {
178 ASTNode * parent = var->parents.get(i);
179 if (parent->type == PREDICATEOP && pred != parent) {
180 BooleanPredicate * newpred = (BooleanPredicate *) parent;
181 for(uint j=0; j < newpred->inputs.getSize(); j++) {
182 Element * e = newpred->inputs.get(j);
184 solver->boolMap.remove(newpred);
185 newpred->inputs.set(j, value);
186 solver->boolMap.put(newpred, newpred);
187 workList.push(newpred);