1 #include "elementopt.h"
9 ElementOpt::ElementOpt(CSolver *_solver)
14 ElementOpt::~ElementOpt() {
17 void ElementOpt::doTransform() {
18 if (solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
21 SetIteratorBooleanEdge *iterator = solver->getConstraints();
22 while (iterator->hasNext()) {
23 BooleanEdge constraint = iterator->next();
24 if (constraint->type == PREDICATEOP)
25 workList.push((BooleanPredicate *)constraint.getBoolean());
27 while (workList.getSize() != 0) {
28 BooleanPredicate * pred = workList.last(); workList.pop();
29 processPredicate(pred);
34 void ElementOpt::processPredicate(BooleanPredicate * pred) {
35 uint numInputs = pred->inputs.getSize();
39 Predicate * p = pred->getPredicate();
40 if (p->type == TABLEPRED)
43 PredicateOperator * pop = (PredicateOperator *) p;
44 CompOp op = pop->getOp();
46 Element * left = pred->inputs.get(0);
47 Element * right = pred->inputs.get(1);
49 if (left->type == ELEMCONST) {
54 } else if (right->type != ELEMCONST)
57 if (left->type !=ELEMSET)
60 if (op == SATC_EQUALS) {
61 handlePredicateEquals(pred, (ElementSet *) left, (ElementConst *) right);
63 handlePredicateInequality(pred, (ElementSet *) left, (ElementConst *) right);
67 void ElementOpt::handlePredicateEquals(BooleanPredicate *pred, ElementSet *left, ElementConst *right) {
69 replaceVarWithConst(pred, left, right);
70 } else if (pred->isFalse()) {
75 void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *left, ElementConst *right) {
79 void ElementOpt::replaceVarWithConst(BooleanPredicate * pred, ElementSet *var, ElementConst * value) {
80 uint size = var->parents.getSize();
81 for(uint i=0; i < size; i++) {
82 ASTNode * parent = var->parents.get(i);
83 if (parent->type == PREDICATEOP && pred != parent) {
84 BooleanPredicate * newpred = (BooleanPredicate *) parent;
85 for(uint j=0; j < newpred->inputs.getSize(); j++) {
86 Element * e = newpred->inputs.get(j);
88 solver->boolMap.remove(newpred);
89 newpred->inputs.set(j, value);
90 solver->boolMap.put(newpred, newpred);
91 workList.push(newpred);