Adding support for mutableset in backend + OO-style Set

diff --git a/src/AST/set.cc b/src/AST/set.cc
index b0e1d8aabb6aadde4dc755b0a67f7ed545a6035c..e33bad0e65308827771f53cb24ac7b78995cdbf8 100644 (file)
--- a/src/AST/set.cc
+++ b/src/AST/set.cc
@@ -41,6 +41,14 @@ uint Set::getSize() {
        }
 }
 
+uint64_t Set::getMemberAt(uint index){
+       if(isRange){
+               return low+index;
+       }else {
+               return members->get(index);
+       }
+}
+
 Set::~Set() {
        if (!isRange)
                delete members;

diff --git a/src/AST/set.h b/src/AST/set.h
index 938027b65d06145f834a1ff65ee9a5c72d28072f..eb406bb553c6ed4feded557fc57454a46dd0b13c 100644 (file)
--- a/src/AST/set.h
+++ b/src/AST/set.h
@@ -20,15 +20,19 @@ public:
        virtual ~Set();
        bool exists(uint64_t element);
        uint getSize();
+       VarType getType(){return type;}
+       uint64_t getNewUniqueItem(){return low++;}
+       uint64_t getMemberAt(uint index);
        uint64_t getElement(uint index);
        virtual Set *clone(CSolver *solver, CloneMap *map);
-
+       MEMALLOC;
+protected:
        VarType type;
        bool isRange;
        uint64_t low;//also used to count unique items
        uint64_t high;
        Vector<uint64_t> *members;
-       MEMALLOC;
+       
 };
 
 #endif/* SET_H */

diff --git a/src/ASTTransform/analyzer.cc b/src/ASTTransform/analyzer.cc
index 4c8562e53511cf1f0cfc0777add4b2fd8c911e2f..cfc01a840d2224c6977b6b09d917d2f32bb51478 100644 (file)
--- a/src/ASTTransform/analyzer.cc
+++ b/src/ASTTransform/analyzer.cc
@@ -64,14 +64,13 @@ void orderAnalysis(CSolver *This) {
                delete decompose;
                delete graph;
 
-               /*
                IntegerEncodingTransform* integerEncoding = new IntegerEncodingTransform(This, order);
                if(!integerEncoding->canExecuteTransform()){
                        delete integerEncoding;
                        continue;
                }
                integerEncoding->doTransform();
-               delete integerEncoding;*/
+               delete integerEncoding;
        }
 }
 

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 4a31eac1cf7e52dfb317b2db85314990b353d235..598928d7be922455e3ca0f6833dd2add23fac9c2 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -53,7 +53,7 @@ void DecomposeOrderTransform::doTransform(){
                        if (ordervec.getSize() > from->sccNum)
                                neworder = ordervec.get(from->sccNum);
                        if (neworder == NULL) {
-                               MutableSet *set = solver->createMutableSet(order->set->type);
+                               MutableSet *set = solver->createMutableSet(order->set->getType());
                                neworder = solver->createOrder(order->type, set);
                                ordervec.setExpand(from->sccNum, neworder);
                                if (order->type == PARTIAL)

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index 6a525cdfc8830a4e4ac12531083723527c049d3f..2d405e0fe82712f527d05252829793aff4a0c7b8 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -25,7 +25,7 @@ bool IntegerEncodingTransform::canExecuteTransform(){
 void IntegerEncodingTransform::doTransform(){
        if (!orderIntegerEncoding->contains(order)) {
                orderIntegerEncoding->put(order, new IntegerEncodingRecord(
-               solver->createRangeSet(order->set->type, 0, (uint64_t) order->set->getSize()-1)));
+               solver->createRangeSet(order->set->getType(), 0, (uint64_t) order->set->getSize()-1)));
        }
        uint size = order->constraints.getSize();
        for(uint i=0; i<size; i++){

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 3bff52bd885f02410c599c7ef4bcd5b20f4a1a2d..f48b72dbd7ee4dead8e55780ae36c47b3af93b94 100644 (file)
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -97,16 +97,16 @@ void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) {
        model_print("in total order ...\n");
 #endif
        ASSERT(order->type == TOTAL);
-       Vector<uint64_t> *mems = order->set->members;
-       uint size = mems->getSize();
+       Set *set = order->set;
+       uint size = order->set->getSize();
        for (uint i = 0; i < size; i++) {
-               uint64_t valueI = mems->get(i);
+               uint64_t valueI = set->getMemberAt(i);
                for (uint j = i + 1; j < size; j++) {
-                       uint64_t valueJ = mems->get(j);
+                       uint64_t valueJ = set->getMemberAt(j);
                        OrderPair pairIJ(valueI, valueJ, E_NULL);
                        Edge constIJ = getPairConstraint(order, &pairIJ);
                        for (uint k = j + 1; k < size; k++) {
-                               uint64_t valueK = mems->get(k);
+                               uint64_t valueK = set->getMemberAt(k);
                                OrderPair pairJK(valueJ, valueK, E_NULL);
                                OrderPair pairIK(valueI, valueK, E_NULL);
                                Edge constIK = getPairConstraint(order, &pairIK);

diff --git a/src/Encoders/elementencoding.cc b/src/Encoders/elementencoding.cc
index 69036a1f2a7baf210340db31711d0ecec9dd6862..89d3c3262e11105e3c52de2b488de953d271ea8f 100644 (file)
--- a/src/Encoders/elementencoding.cc
+++ b/src/Encoders/elementencoding.cc
@@ -40,13 +40,12 @@ void ElementEncoding::setElementEncodingType(ElementEncodingType _type) {
 
 void ElementEncoding::encodingArrayInitialization() {
        Set *set = getElementSet(element);
-       ASSERT(!set->isRange);
-       uint size = set->members->getSize();
+       uint size = set->getSize();
        uint encSize = getSizeEncodingArray(size);
        allocEncodingArrayElement(encSize);
        allocInUseArrayElement(encSize);
        for (uint i = 0; i < size; i++) {
-               encodingArray[i] = set->members->get(i);
+               encodingArray[i] = set->getMemberAt(i);
                setInUseElement(i);
        }
 }

diff --git a/src/csolver.cc b/src/csolver.cc
index db42f316afaff7d19da8dbe610f822df5c53f84f..e16574f20249428eb1ec18c1e96fba8aa2c98d42 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -98,7 +98,7 @@ void CSolver::addItem(MutableSet *set, uint64_t element) {
 }
 
 uint64_t CSolver::createUniqueItem(MutableSet *set) {
-       uint64_t element = set->low++;
+       uint64_t element = set->getNewUniqueItem();
        set->addElementMSet(element);
        return element;
 }