1 #include "elementopt.h"
10 ElementOpt::ElementOpt(CSolver *_solver)
16 ElementOpt::~ElementOpt() {
19 void ElementOpt::doTransform() {
20 if (solver->isUnSAT() || solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
23 //Set once we know we are going to use it.
24 updateSets = solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1;
26 SetIteratorBooleanEdge *iterator = solver->getConstraints();
27 while (iterator->hasNext()) {
28 BooleanEdge constraint = iterator->next();
29 if (!solver->isConstraintEncoded(constraint) && constraint->type == PREDICATEOP)
30 workList.push((BooleanPredicate *)constraint.getBoolean());
32 while (workList.getSize() != 0) {
33 BooleanPredicate *pred = workList.last(); workList.pop();
34 processPredicate(pred);
39 void ElementOpt::processPredicate(BooleanPredicate *pred) {
40 uint numInputs = pred->inputs.getSize();
44 Predicate *p = pred->getPredicate();
45 if (p->type == TABLEPRED)
48 PredicateOperator *pop = (PredicateOperator *) p;
49 CompOp op = pop->getOp();
51 Element *left = pred->inputs.get(0);
52 Element *right = pred->inputs.get(1);
54 if (left->type == ELEMCONST) {
59 } else if (right->type != ELEMCONST)
62 if (left->type != ELEMSET)
65 if (op == SATC_EQUALS) {
66 handlePredicateEquals(pred, (ElementSet *) left, (ElementConst *) right);
67 } else if (updateSets) {
68 handlePredicateInequality(pred, (ElementSet *) left, (ElementConst *) right);
72 void ElementOpt::handlePredicateEquals(BooleanPredicate *pred, ElementSet *left, ElementConst *right) {
74 replaceVarWithConst(pred, left, right);
75 } else if (pred->isFalse() && updateSets) {
76 constrainVarWithConst(pred, left, right);
80 void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
81 Predicate *p = pred->getPredicate();
82 PredicateOperator *pop = (PredicateOperator *) p;
83 CompOp op = pop->getOp();
85 if (pred->isFalse()) {
87 } else if (!pred->isTrue()) {
91 Set *s = var->getRange();
95 uint size = s->getSize();
96 uint64_t elemArray[size];
98 uint64_t cvalue = value->value;
102 for (uint i = 0; i < size; i++) {
103 uint64_t val = s->getElement(i);
105 elemArray[count++] = val;
110 for (uint i = 0; i < size; i++) {
111 uint64_t val = s->getElement(i);
113 elemArray[count++] = val;
118 for (uint i = 0; i < size; i++) {
119 uint64_t val = s->getElement(i);
121 elemArray[count++] = val;
126 for (uint i = 0; i < size; i++) {
127 uint64_t val = s->getElement(i);
129 elemArray[count++] = val;
140 Set *newset = solver->createSet(s->type, elemArray, count);
141 solver->elemMap.remove(var);
143 solver->elemMap.put(var, var);
146 ElementConst *elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
147 replaceVarWithConst(pred, var, elemconst);
151 void ElementOpt::constrainVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
152 Set *s = var->getRange();
155 uint size = s->getSize();
156 uint64_t elemArray[size];
158 uint64_t cvalue = value->value;
159 for (uint i = 0; i < size; i++) {
160 uint64_t val = s->getElement(i);
162 elemArray[count++] = val;
167 Set *newset = solver->createSet(s->type, elemArray, count);
168 solver->elemMap.remove(var);
170 solver->elemMap.put(var, var);
173 ElementConst *elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
174 replaceVarWithConst(pred, var, elemconst);
178 void ElementOpt::replaceVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
179 uint size = var->parents.getSize();
180 for (uint i = 0; i < size; i++) {
181 ASTNode *parent = var->parents.get(i);
182 if (parent->type == PREDICATEOP && pred != parent) {
183 BooleanPredicate *newpred = (BooleanPredicate *) parent;
184 for (uint j = 0; j < newpred->inputs.getSize(); j++) {
185 Element *e = newpred->inputs.get(j);
187 solver->boolMap.remove(newpred);
188 newpred->inputs.set(j, value);
189 solver->boolMap.put(newpred, newpred);
190 if (newpred->isTrue() || newpred->isFalse())
191 workList.push(newpred);