X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FAST%2Fset.cc;h=d3801f8d498eb98e3a55440a4ac7faf243a195f3;hb=8289a5fe3c5298b2477ffa611ca976376554afc7;hp=76d6713ad17ebc9f178ee8a506b5f098c44f6bc4;hpb=abe0dee853780f8254436b0de7c8330d326d4017;p=satune.git

diff --git a/src/AST/set.cc b/src/AST/set.cc
index 76d6713..d3801f8 100644
--- a/src/AST/set.cc
+++ b/src/AST/set.cc
@@ -2,15 +2,30 @@
 #include <stddef.h>
 #include "csolver.h"
 #include "serializer.h"
+#include "qsort.h"
+
+int intcompare(const void *p1, const void *p2) {
+	uint64_t a=*(uint64_t const *) p1;
+	uint64_t b=*(uint64_t const *) p2;
+	if (a < b)
+		return -1;
+	else if (a==b)
+		return 0;
+	else
+		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);
 }
 
+
 Set::Set(VarType t, uint64_t lowrange, uint64_t highrange) : type(t), isRange(true), low(lowrange), high(highrange), members(NULL) {
 }
 
@@ -18,12 +33,24 @@ bool Set::exists(uint64_t element) {
 	if (isRange) {
 		return element >= low && element <= high;
 	} else {
-		uint size = members->getSize();
-		for (uint i = 0; i < size; i++) {
-			if (element == members->get(i))
+		//Use Binary Search
+		uint low=0;
+		uint high=members->getSize()-1;
+		while(true) {
+			uint middle=(low+high)/2;
+			uint64_t val=members->get(middle);
+			if (element < val) {
+				high=middle-1;
+				if (middle<=low)
+					return false;
+			} else if (element > val) {
+				low=middle+1;
+				if (middle>=high)
+					return false;
+			} else {
 				return true;
+			}
 		}
-		return false;
 	}
 }
 
@@ -68,6 +95,31 @@ Set *Set::clone(CSolver *solver, CloneMap *map) {
 	return s;
 }
 
+uint Set::getUnionSize(Set *s) {
+	uint sSize = s->getSize();
+	uint thisSize = getSize();
+	uint sIndex = 0;
+	uint thisIndex = 0;
+	uint sum = 0;
+	uint64_t sValue = s->getElement(sIndex);
+	uint64_t thisValue = getElement(thisIndex);
+	while(thisIndex < thisSize && sIndex < sSize) {
+		if (sValue < thisValue) {
+			sValue = s->getElement(++sIndex);
+			sum++;
+		} else if (thisValue < sValue) {
+			thisValue = getElement(++thisIndex);
+			sum++;
+		} else {
+			thisValue = getElement(++thisIndex);
+			sValue = s->getElement(++sIndex);
+			sum++;
+		}
+	}
+	sum += (thisSize - thisIndex) + (sSize - sIndex);
+	
+	return sum;
+}
 
 void Set::serialize(Serializer* serializer){
 	if(serializer->isSerialized(this))
@@ -81,10 +133,12 @@ void Set::serialize(Serializer* serializer){
 	serializer->mywrite(&isRange, sizeof(bool));
 	serializer->mywrite(&low, sizeof(uint64_t));
 	serializer->mywrite(&high, sizeof(uint64_t));
+	bool isMutable = isMutableSet();
+	serializer->mywrite(&isMutable, sizeof(bool));
 	uint size = members->getSize();
 	serializer->mywrite(&size, sizeof(uint));
 	for(uint i=0; i<size; i++){
 		uint64_t mem = members->get(i);
 		serializer->mywrite(&mem, sizeof(uint64_t));
 	}
-}
\ No newline at end of file
+}