Adding support for mutableset in backend + OO-style Set
authorHamed <hamed.gorjiara@gmail.com>
Wed, 30 Aug 2017 00:41:12 +0000 (17:41 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Wed, 30 Aug 2017 00:41:12 +0000 (17:41 -0700)
src/AST/set.cc
src/AST/set.h
src/ASTTransform/analyzer.cc
src/ASTTransform/decomposeordertransform.cc
src/ASTTransform/integerencoding.cc
src/Backend/satorderencoder.cc
src/Encoders/elementencoding.cc
src/csolver.cc

index b0e1d8a..e33bad0 100644 (file)
@@ -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;
index 938027b..eb406bb 100644 (file)
@@ -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 */
index 4c8562e..cfc01a8 100644 (file)
@@ -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;
        }
 }
 
index 4a31eac..598928d 100644 (file)
@@ -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)
index 6a525cd..2d405e0 100644 (file)
@@ -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++){
index 3bff52b..f48b72d 100644 (file)
@@ -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);
index 69036a1..89d3c32 100644 (file)
@@ -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);
        }
 }
index db42f31..e16574f 100644 (file)
@@ -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;
 }