From bdb495e03a14ca5adf4b4b4a53233ed373121642 Mon Sep 17 00:00:00 2001
From: Hamed <hamed.gorjiara@gmail.com>
Date: Fri, 15 Sep 2017 15:01:33 -0700
Subject: [PATCH] Adding an API for finalizing MutableSet

---
 src/AST/mutableset.cc | 8 +++++++-
 src/AST/mutableset.h  | 1 +
 src/AST/set.cc        | 9 +++++----
 src/AST/set.h         | 1 +
 src/csolver.cc        | 4 ++++
 src/csolver.h         | 5 +++++
 6 files changed, 23 insertions(+), 5 deletions(-)

diff --git a/src/AST/mutableset.cc b/src/AST/mutableset.cc
index d6657c5..3d9db49 100644
--- a/src/AST/mutableset.cc
+++ b/src/AST/mutableset.cc
@@ -1,5 +1,6 @@
 #include "mutableset.h"
 #include "csolver.h"
+#include "qsort.h"
 
 MutableSet::MutableSet(VarType t) : Set(t) {
 }
@@ -15,8 +16,13 @@ Set *MutableSet::clone(CSolver *solver, CloneMap *map) {
 	s = solver->createMutableSet(type);
 	for (uint i = 0; i < members->getSize(); i++) {
 		((MutableSet *)s)->addElementMSet(members->get(i));
-		//		solver->addItem((MutableSet *) s, members->get(i));
+				solver->addItem((MutableSet *) s, members->get(i));
 	}
+	((MutableSet*)s)->finalize();
 	map->put(this, s);
 	return s;
 }
+
+void MutableSet::finalize(){
+	bsdqsort(members->expose(), members->getSize(), sizeof(uint64_t), intcompare);
+}
\ No newline at end of file
diff --git a/src/AST/mutableset.h b/src/AST/mutableset.h
index c608f3f..9cfa9e6 100644
--- a/src/AST/mutableset.h
+++ b/src/AST/mutableset.h
@@ -8,6 +8,7 @@ public:
 	void addElementMSet(uint64_t element);
 	Set *clone(CSolver *solver, CloneMap *map);
 	bool isMutableSet() {return true;}
+	void finalize();
 	CMEMALLOC;
 };
 #endif
diff --git a/src/AST/set.cc b/src/AST/set.cc
index fc8bf15..66f8461 100644
--- a/src/AST/set.cc
+++ b/src/AST/set.cc
@@ -4,10 +4,6 @@
 #include "serializer.h"
 #include "qsort.h"
 
-Set::Set(VarType t) : type(t), isRange(false), low(0), high(0) {
-	members = new Vector<uint64_t>();
-}
-
 int intcompare(const void *p1, const void *p2) {
 	uint64_t a=*(uint64_t const *) p1;
 	uint64_t b=*(uint64_t const *) p2;
@@ -19,6 +15,11 @@ int intcompare(const void *p1, const void *p2) {
 		return 1;
 }
 
+Set::Set(VarType t) : type(t), isRange(false), low(0), high(0) {
+	members = new Vector<uint64_t>();
+}
+
+
 Set::Set(VarType t, uint64_t *elements, uint num) : type(t), isRange(false), low(0), high(0) {
 	members = new Vector<uint64_t>(num, elements);
 	bsdqsort(members->expose(), members->getSize(), sizeof(uint64_t), intcompare);
diff --git a/src/AST/set.h b/src/AST/set.h
index efd281d..ef10b39 100644
--- a/src/AST/set.h
+++ b/src/AST/set.h
@@ -37,5 +37,6 @@ protected:
 
 };
 
+int intcompare(const void *p1, const void *p2);
 #endif/* SET_H */
 
diff --git a/src/csolver.cc b/src/csolver.cc
index 0eebb17..575a12b 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -138,6 +138,10 @@ uint64_t CSolver::createUniqueItem(MutableSet *set) {
 	return element;
 }
 
+void CSolver::finalizeMutableSet(MutableSet* set){
+	set->finalize();
+}
+
 Element *CSolver::getElementVar(Set *set) {
 	Element *element = new ElementSet(set);
 	allElements.push(element);
diff --git a/src/csolver.h b/src/csolver.h
index 42a6216..e492781 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -34,6 +34,11 @@ public:
 	    items to the set. */
 
 	uint64_t createUniqueItem(MutableSet *set);
+	
+	/**
+	 * Freeze and finalize the mutableSet ...
+	 */
+	void finalizeMutableSet(MutableSet* set);
 
 	/** This function creates an element variable over a set. */
 
-- 
2.34.1