Make integerencoding a completely separate pass... Fix issue of changing ordersets

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

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index f1b99199c802efca86045282238e3799a41bc9c4..6664a677f2b10664e7e11ab894f8f98287e807e4 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -1,4 +1,3 @@
-
 #include "integerencoding.h"
 #include "set.h"
 #include "order.h"
@@ -6,41 +5,50 @@
 #include "csolver.h"
 #include "integerencodingrecord.h"
 #include "integerencorderresolver.h"
+#include "tunable.h"
 
-
-IntegerEncodingTransform::IntegerEncodingTransform(CSolver* _solver) 
-       :Transform(_solver)
-{      
+IntegerEncodingTransform::IntegerEncodingTransform(CSolver *_solver)
+       : Transform(_solver)
+{
        orderIntEncoding = new HashTableOrderIntEncoding();
 }
 
-IntegerEncodingTransform::~IntegerEncodingTransform(){
+IntegerEncodingTransform::~IntegerEncodingTransform() {
        orderIntEncoding->resetanddelete();
 }
 
-bool IntegerEncodingTransform::canExecuteTransform(){
-       return canExecutePass(solver, currOrder->type, ORDERINTEGERENCODING, &offon);
+void IntegerEncodingTransform::doTransform() {
+       HashsetOrder *orders = solver->getActiveOrders()->copy();
+       SetIteratorOrder * orderit=orders->iterator();
+       while(orderit->hasNext()) {
+               Order *order = orderit->next();
+               if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &onoff))
+                       integerEncode(order);
+       }
+       delete orders;
+       delete orderit;
 }
 
-void IntegerEncodingTransform::doTransform(){
-       IntegerEncodingRecord* encodingRecord = NULL;
+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));
+                       solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize() - 1));
                orderIntEncoding->put(currOrder, encodingRecord);
        } else {
                encodingRecord = orderIntEncoding->get(currOrder);
        }
        uint size = currOrder->constraints.getSize();
-       for(uint i=0; i<size; i++){
-               orderIntegerEncodingSATEncoder(currOrder->constraints.get(i));
+       for (uint i = 0; i < size; i++) {
+               orderIntegerEncodingSATEncoder(currOrder, currOrder->constraints.get(i));
        }
        currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));
+       solver->getActiveOrders()->remove(currOrder);
 }
 
 
-void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) {
-       IntegerEncodingRecord* ierec = orderIntEncoding->get(currOrder);
+void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(Order * currOrder, BooleanOrder *boolOrder) {
+       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);