+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);
+}
+
+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;