Make integerencoding a completely separate pass... Fix issue of changing ordersets
authorbdemsky <bdemsky@uci.edu>
Sat, 2 Sep 2017 07:00:52 +0000 (00:00 -0700)
committerbdemsky <bdemsky@uci.edu>
Sat, 2 Sep 2017 07:00:52 +0000 (00:00 -0700)
src/ASTTransform/decomposeordertransform.cc
src/ASTTransform/decomposeordertransform.h
src/ASTTransform/integerencoding.cc
src/ASTTransform/integerencoding.h
src/Collections/corestructs.h
src/csolver.cc
src/csolver.h

index ec8b020..85b43b1 100644 (file)
@@ -27,10 +27,10 @@ DecomposeOrderTransform::~DecomposeOrderTransform() {
 }
 
 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;
@@ -70,8 +70,11 @@ void DecomposeOrderTransform::doTransform() {
                decomposeOrder(order, graph);
                delete graph;
        }
+       delete orderit;
+       delete orders;
 }
 
+
 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) );
+       solver->getActiveOrders()->remove(currOrder);
        uint pcvsize = partialcandidatevec.getSize();
        for (uint i = 0; i < pcvsize; i++) {
                Order *neworder = partialcandidatevec.get(i);
index 69f7a1f..1a2865c 100644 (file)
@@ -20,8 +20,6 @@ public:
 
        CMEMALLOC;
 private:
-       Order *currOrder;
-       OrderGraph *currGraph;
 };
 
 #endif/* ORDERTRANSFORM_H */
index d8150b3..6664a67 100644 (file)
@@ -18,13 +18,15 @@ IntegerEncodingTransform::~IntegerEncodingTransform() {
 }
 
 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);
        }
+       delete orders;
+       delete orderit;
 }
 
 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++) {
-               orderIntegerEncodingSATEncoder(currOrder->constraints.get(i));
+               orderIntegerEncodingSATEncoder(currOrder, currOrder->constraints.get(i));
        }
        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);
index f051a41..8066c2a 100644 (file)
 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:
-       Order *currOrder;
        //FIXME:We can remove it, because we don't need it for translating anymore... -HG
        HashTableOrderIntEncoding *orderIntEncoding;
 };
index 1e808cb..982e0c5 100644 (file)
@@ -5,6 +5,8 @@
 #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<Order *, uintptr_t, 4> SetIteratorOrder;
 
 #endif
index de9543e..b351914 100644 (file)
@@ -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);
+       activeOrders.add(order);
        return order;
 }
 
index 1ff4cd1..7e8bbad 100644 (file)
@@ -125,6 +125,7 @@ public:
        bool isUnSAT() { return unsat; }
 
        Vector<Order *> *getOrders() { return &allOrders;}
+       HashsetOrder * getActiveOrders() { return &activeOrders;}
 
        Tuner *getTuner() { return tuner; }
 
@@ -173,6 +174,8 @@ private:
        /** 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;