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

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index ec8b0204c3360a3b53980a9a5e0fa97f1507dfba..85b43b12e1d063d9cdcf98e516fb21de1abbf177 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -27,10 +27,10 @@ DecomposeOrderTransform::~DecomposeOrderTransform() {
 }
 
 void DecomposeOrderTransform::doTransform() {
 }
 
 void DecomposeOrderTransform::doTransform() {

-       Vector<Order *> *orders = solver->getOrders();
-       uint size = orders->getSize();
-       for (uint i = 0; i < size; i++) {
-               Order *order = orders->get(i);
+       HashsetOrder *orders = solver->getActiveOrders()->copy();
+       SetIteratorOrder * orderit=orders->iterator();
+       while(orderit->hasNext()) {
+               Order *order = orderit->next();

 
                if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
                        continue;
 
                if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
                        continue;


@@ -70,8 +70,11 @@ void DecomposeOrderTransform::doTransform() {
                decomposeOrder(order, graph);
                delete graph;
        }
                decomposeOrder(order, graph);
                delete graph;
        }

+       delete orderit;
+       delete orders;

 }
 
 }
 

+

 void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph) {
        Vector<Order *> ordervec;
        Vector<Order *> partialcandidatevec;
 void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph) {
        Vector<Order *> ordervec;
        Vector<Order *> partialcandidatevec;


@@ -122,6 +125,7 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
                }
        }
        currOrder->setOrderResolver( new DecomposeOrderResolver(currGraph, ordervec) );
                }
        }
        currOrder->setOrderResolver( new DecomposeOrderResolver(currGraph, ordervec) );

+       solver->getActiveOrders()->remove(currOrder);

        uint pcvsize = partialcandidatevec.getSize();
        for (uint i = 0; i < pcvsize; i++) {
                Order *neworder = partialcandidatevec.get(i);
        uint pcvsize = partialcandidatevec.getSize();
        for (uint i = 0; i < pcvsize; i++) {
                Order *neworder = partialcandidatevec.get(i);

diff --git a/src/ASTTransform/decomposeordertransform.h b/src/ASTTransform/decomposeordertransform.h
index 69f7a1f2cadbab75d8d84c8f0c390d5347bcebb3..1a2865cef6f64033752be24696005db51d4091d5 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.h
+++ b/src/ASTTransform/decomposeordertransform.h
@@ -20,8 +20,6 @@ public:
 
        CMEMALLOC;
 private:
 
        CMEMALLOC;
 private:

-       Order *currOrder;
-       OrderGraph *currGraph;

 };
 
 #endif/* ORDERTRANSFORM_H */
 };
 
 #endif/* ORDERTRANSFORM_H */

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index d8150b311d633a34f3aeb932caedfda8136851ab..6664a677f2b10664e7e11ab894f8f98287e807e4 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -18,13 +18,15 @@ IntegerEncodingTransform::~IntegerEncodingTransform() {
 }
 
 void IntegerEncodingTransform::doTransform() {
 }
 
 void IntegerEncodingTransform::doTransform() {

-       Vector<Order *> *orders = solver->getOrders();
-       uint size = orders->getSize();
-       for (uint i = 0; i < size; i++) {
-               Order *order = orders->get(i);
+       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);
        }
                if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &onoff))
                        integerEncode(order);
        }

+       delete orders;
+       delete orderit;

 }
 
 void IntegerEncodingTransform::integerEncode(Order *currOrder) {
 }
 
 void IntegerEncodingTransform::integerEncode(Order *currOrder) {


@@ -38,13 +40,14 @@ void IntegerEncodingTransform::integerEncode(Order *currOrder) {
        }
        uint size = currOrder->constraints.getSize();
        for (uint i = 0; i < size; i++) {
        }
        uint size = currOrder->constraints.getSize();
        for (uint i = 0; i < size; i++) {

-               orderIntegerEncodingSATEncoder(currOrder->constraints.get(i));
+               orderIntegerEncodingSATEncoder(currOrder, currOrder->constraints.get(i));

        }
        currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));
        }
        currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));

+       solver->getActiveOrders()->remove(currOrder);

 }
 
 
 }
 
 

-void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) {
+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);
        IntegerEncodingRecord *ierec = orderIntEncoding->get(currOrder);
        //getting two elements and using LT predicate ...
        Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first);

diff --git a/src/ASTTransform/integerencoding.h b/src/ASTTransform/integerencoding.h
index f051a41d17c66ad698f37142ff4581d91782ed20..8066c2acf678924b7b7ffb8fe3306cc6b0f9ca10 100644 (file)
--- a/src/ASTTransform/integerencoding.h
+++ b/src/ASTTransform/integerencoding.h
@@ -14,13 +14,12 @@
 class IntegerEncodingTransform : public Transform {
 public:
        IntegerEncodingTransform(CSolver *solver);
 class IntegerEncodingTransform : public Transform {
 public:
        IntegerEncodingTransform(CSolver *solver);

-       void orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder);
+       void orderIntegerEncodingSATEncoder(Order * currOrder, BooleanOrder *boolOrder);

        void doTransform();
        void integerEncode(Order *currOrder);
 
        virtual ~IntegerEncodingTransform();
 private:
        void doTransform();
        void integerEncode(Order *currOrder);
 
        virtual ~IntegerEncodingTransform();
 private:

-       Order *currOrder;

        //FIXME:We can remove it, because we don't need it for translating anymore... -HG
        HashTableOrderIntEncoding *orderIntEncoding;
 };
        //FIXME:We can remove it, because we don't need it for translating anymore... -HG
        HashTableOrderIntEncoding *orderIntEncoding;
 };

diff --git a/src/Collections/corestructs.h b/src/Collections/corestructs.h
index 1e808cb6166b63052a75dd2211f099d987f19717..982e0c5cfed2d397e95a3f1f8bdf486aedfcd8e8 100644 (file)
--- a/src/Collections/corestructs.h
+++ b/src/Collections/corestructs.h
@@ -5,6 +5,8 @@
 #include "hashset.h"
 
 typedef Hashset<Boolean *, uintptr_t, 4> HashsetBoolean;
 #include "hashset.h"
 
 typedef Hashset<Boolean *, uintptr_t, 4> HashsetBoolean;

+typedef Hashset<Order *, uintptr_t, 4> HashsetOrder;

 typedef SetIterator<Boolean *, uintptr_t, 4> SetIteratorBoolean;
 typedef SetIterator<Boolean *, uintptr_t, 4> SetIteratorBoolean;

+typedef SetIterator<Order *, uintptr_t, 4> SetIteratorOrder;

 
 #endif
 
 #endif

diff --git a/src/csolver.cc b/src/csolver.cc
index de9543edc3482fe5e6f99afd577fbefc9e19748f..b351914cd2b0fbe81faa68149bd993a6056e6833 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -383,6 +383,7 @@ void CSolver::addConstraint(Boolean *constraint) {
 Order *CSolver::createOrder(OrderType type, Set *set) {
        Order *order = new Order(type, set);
        allOrders.push(order);
 Order *CSolver::createOrder(OrderType type, Set *set) {
        Order *order = new Order(type, set);
        allOrders.push(order);

+       activeOrders.add(order);

        return order;
 }
 
        return order;
 }
 

diff --git a/src/csolver.h b/src/csolver.h
index 1ff4cd113ef317860f116a74b45d291687e1dbae..7e8bbad871019bcc59f06d5e170de317fc2cae02 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -125,6 +125,7 @@ public:
        bool isUnSAT() { return unsat; }
 
        Vector<Order *> *getOrders() { return &allOrders;}
        bool isUnSAT() { return unsat; }
 
        Vector<Order *> *getOrders() { return &allOrders;}

+       HashsetOrder * getActiveOrders() { return &activeOrders;}

 
        Tuner *getTuner() { return tuner; }
 
 
        Tuner *getTuner() { return tuner; }
 


@@ -173,6 +174,8 @@ private:
        /** This is a vector of all order structs that we have allocated. */
        Vector<Order *> allOrders;
 
        /** This is a vector of all order structs that we have allocated. */
        Vector<Order *> allOrders;
 

+       HashsetOrder activeOrders;
+       

        /** This is a vector of all function structs that we have allocated. */
        Vector<Function *> allFunctions;
 
        /** This is a vector of all function structs that we have allocated. */
        Vector<Function *> allFunctions;