Bug Fixes

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

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index a4aacdf5a1f93d171d963e57c1eff127f8bdd430..78f1b733204d3be9b7116c3ae1230b9d5bae4851 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -10,19 +10,17 @@
 IntegerEncodingTransform::IntegerEncodingTransform(CSolver *_solver)
        : Transform(_solver)
 {
-       orderIntEncoding = new HashTableOrderIntEncoding();
 }
 
 IntegerEncodingTransform::~IntegerEncodingTransform() {
-       orderIntEncoding->resetanddelete();
 }
 
 void IntegerEncodingTransform::doTransform() {
        HashsetOrder *orders = solver->getActiveOrders()->copy();
-       SetIteratorOrder * orderit=orders->iterator();
-       while(orderit->hasNext()) {
+       SetIteratorOrder *orderit = orders->iterator();
+       while (orderit->hasNext()) {
                Order *order = orderit->next();
-               if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &onoff))
+               if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &offon))
                        integerEncode(order);
        }
        delete orders;
@@ -30,25 +28,19 @@ void IntegerEncodingTransform::doTransform() {
 }
 
 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, currOrder->constraints.get(i));
+               orderIntegerEncodingSATEncoder(currOrder->constraints.get(i), encodingRecord);
        }
        currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));
        solver->getActiveOrders()->remove(currOrder);
 }
 
 
-void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(Order * currOrder, 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);
@@ -56,7 +48,6 @@ void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(Order * currOrder,
        Predicate *predicate = solver->createPredicateOperator(SATC_LT, sarray, 2);
        Element *parray[] = {elem1, elem2};
        BooleanEdge boolean = solver->applyPredicate(predicate, parray, 2);
-       solver->addConstraint(boolean);
        solver->replaceBooleanWithBoolean(boolOrder, boolean);
 }