- //getting two elements and using LT predicate ...
- Element* elem1 = getOrderIntegerElement(This, order, boolOrder->first);
- Element* elem2 = getOrderIntegerElement(This, order, boolOrder->second);
- Set * sarray[]={order->auxSet, order->auxSet};
- Predicate *predicate =new PredicateOperator(LT, sarray, 2);
- Element * parray[]={elem1, elem2};
- BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL);
- {//Adding new elements and boolean/predicate to solver regarding memory management
- This->solver->allBooleans.push(boolean);
- This->solver->allPredicates.push(predicate);
- This->solver->allElements.push(elem1);
- This->solver->allElements.push(elem2);
- This->solver->constraints.add(boolean);
+ delete orders;
+ delete orderit;
+}
+
+void IntegerEncodingTransform::integerEncode(Order *currOrder) {
+ IntegerEncodingRecord *encodingRecord = new IntegerEncodingRecord(
+ solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize() - 1));
+ currOrder->setOrderEncodingType( INTEGERENCODING );
+ uint size = currOrder->constraints.getSize();
+ for (uint i = 0; i < size; i++) {
+ orderIntegerEncodingSATEncoder(currOrder->constraints.get(i), encodingRecord);