Merging with branch Master

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

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index d15c60e365798254924277c8fd77c0fe86935359..411ddc9ddafeab489c9ce3e0b368c8d67847562a 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -6,40 +6,39 @@
 #include "csolver.h"
 #include "integerencodingrecord.h"
 
-HashtableOrderIntegerEncoding* IntegerEncodingTransform::orderIntegerEncoding = new HashtableOrderIntegerEncoding();
 
-IntegerEncodingTransform::IntegerEncodingTransform(CSolver* _solver, Order* _order) 
-       :Transform(_solver),
-       order(_order)
-       
+IntegerEncodingTransform::IntegerEncodingTransform(CSolver* _solver) 
+       :Transform(_solver)
 {      
+       orderIntEncoding = new HashTableOrderIntEncoding();
 }
 
 IntegerEncodingTransform::~IntegerEncodingTransform(){
+       orderIntEncoding->resetanddelete();
 }
 
 bool IntegerEncodingTransform::canExecuteTransform(){
-       return canExecutePass(solver, order->type, ORDERINTEGERENCODING, &offon);
+       return canExecutePass(solver, currOrder->type, ORDERINTEGERENCODING, &offon);
 }
 
 void IntegerEncodingTransform::doTransform(){
-       if (!orderIntegerEncoding->contains(order)) {
-               orderIntegerEncoding->put(order, new IntegerEncodingRecord(
-               solver->createRangeSet(order->set->getType(), 0, (uint64_t) order->set->getSize()-1)));
+       if (!orderIntEncoding->contains(currOrder)) {
+               orderIntEncoding->put(currOrder, new IntegerEncodingRecord(
+               solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize()-1)));
        }
-       uint size = order->constraints.getSize();
+       uint size = currOrder->constraints.getSize();
        for(uint i=0; i<size; i++){
-               orderIntegerEncodingSATEncoder(order->constraints.get(i));
+               orderIntegerEncodingSATEncoder(currOrder->constraints.get(i));
        }
 }
 
 
 void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) {
-       IntegerEncodingRecord* ierec = orderIntegerEncoding->get(order);
-       //getting two elements and using SATC_LT predicate ...
+       IntegerEncodingRecord* ierec = orderIntEncoding->get(currOrder);
+       //getting two elements and using LT predicate ...
        Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first);
        Element *elem2 = ierec->getOrderIntegerElement(solver, boolOrder->second);
-       Set *sarray[] = {ierec->set, ierec->set};
+       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);