Bug Fixes

[satune.git] / src / ASTTransform / integerencoding.cc

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index d8150b311d633a34f3aeb932caedfda8136851ab..78f1b733204d3be9b7116c3ae1230b9d5bae4851 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -10,50 +10,44 @@
 IntegerEncodingTransform::IntegerEncodingTransform(CSolver *_solver)
        : Transform(_solver)
 {
-       orderIntEncoding = new HashTableOrderIntEncoding();
 }
 
 IntegerEncodingTransform::~IntegerEncodingTransform() {
-       orderIntEncoding->resetanddelete();
 }
 
 void IntegerEncodingTransform::doTransform() {
-       Vector<Order *> *orders = solver->getOrders();
-       uint size = orders->getSize();
-       for (uint i = 0; i < size; i++) {
-               Order *order = orders->get(i);
-               if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &onoff))
+       HashsetOrder *orders = solver->getActiveOrders()->copy();
+       SetIteratorOrder *orderit = orders->iterator();
+       while (orderit->hasNext()) {
+               Order *order = orderit->next();
+               if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &offon))
                        integerEncode(order);
        }
+       delete orders;
+       delete orderit;
 }
 
 void IntegerEncodingTransform::integerEncode(Order *currOrder) {
-       IntegerEncodingRecord *encodingRecord = NULL;
-       if (!orderIntEncoding->contains(currOrder)) {
-               encodingRecord = new IntegerEncodingRecord(
-                       solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize() - 1));
-               orderIntEncoding->put(currOrder, encodingRecord);
-       } else {
-               encodingRecord = orderIntEncoding->get(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));
+               orderIntegerEncodingSATEncoder(currOrder->constraints.get(i), encodingRecord);
        }
        currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));
+       solver->getActiveOrders()->remove(currOrder);
 }
 
 
-void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) {
-       IntegerEncodingRecord *ierec = orderIntEncoding->get(currOrder);
+void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder, IntegerEncodingRecord *ierec) {
        //getting two elements and using LT predicate ...
        Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first);
        Element *elem2 = ierec->getOrderIntegerElement(solver, boolOrder->second);
        Set *sarray[] = {ierec->getSecondarySet(), ierec->getSecondarySet()};
        Predicate *predicate = solver->createPredicateOperator(SATC_LT, sarray, 2);
        Element *parray[] = {elem1, elem2};
-       Boolean *boolean = solver->applyPredicate(predicate, parray, 2);
-       solver->addConstraint(boolean);
+       BooleanEdge boolean = solver->applyPredicate(predicate, parray, 2);
        solver->replaceBooleanWithBoolean(boolOrder, boolean);
 }