From 8014c371c763fbc3fe65ec15e5320c1a9b859a8d Mon Sep 17 00:00:00 2001
From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 29 Aug 2017 17:41:12 -0700
Subject: [PATCH] Adding support for mutableset in backend + OO-style Set

---
 src/AST/set.cc                              |  8 ++++++++
 src/AST/set.h                               |  8 ++++++--
 src/ASTTransform/analyzer.cc                |  3 +--
 src/ASTTransform/decomposeordertransform.cc |  2 +-
 src/ASTTransform/integerencoding.cc         |  2 +-
 src/Backend/satorderencoder.cc              | 10 +++++-----
 src/Encoders/elementencoding.cc             |  5 ++---
 src/csolver.cc                              |  2 +-
 8 files changed, 25 insertions(+), 15 deletions(-)

diff --git a/src/AST/set.cc b/src/AST/set.cc
index b0e1d8a..e33bad0 100644
--- 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 938027b..eb406bb 100644
--- 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 4c8562e..cfc01a8 100644
--- 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 4a31eac..598928d 100644
--- 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 6a525cd..2d405e0 100644
--- 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 3bff52b..f48b72d 100644
--- 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 69036a1..89d3c32 100644
--- 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 db42f31..e16574f 100644
--- 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;
 }
-- 
2.34.1