X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FSerialize%2Fdeserializer.cc;h=548619fe221d45a380bb35933b08e08f552dafe1;hb=c64cf3c2712780c3898523039fcfc49f7b306432;hp=cd1e1a232fca290d3401e140e96854bbaf1dfbbb;hpb=d8a822b4166c0e1da167d756bc10cffbaded8972;p=satune.git

diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc
index cd1e1a2..548619f 100644
--- a/src/Serialize/deserializer.cc
+++ b/src/Serialize/deserializer.cc
@@ -15,7 +15,13 @@
 #include "element.h"
 #include "mutableset.h"
 
+#define READBUFFERSIZE 16384
+
 Deserializer::Deserializer(const char *file) :
+	buffer((char *) ourmalloc(READBUFFERSIZE)),
+	bufferindex(0),
+	bufferbytes(0),
+	buffercap(READBUFFERSIZE),
 	solver(new CSolver())
 {
 	filedesc = open(file, O_RDONLY);
@@ -26,15 +32,38 @@ Deserializer::Deserializer(const char *file) :
 }
 
 Deserializer::~Deserializer() {
-	delete solver;
-
 	if (-1 == close(filedesc)) {
 		exit(-1);
 	}
+	ourfree(buffer);
 }
 
-ssize_t Deserializer::myread(void *__buf, size_t __nbytes) {
-	return read (filedesc, __buf, __nbytes);
+ssize_t Deserializer::myread(void *__buf, size_t bytestoread) {
+	char *out = (char * ) __buf;
+	size_t totalbytesread = 0;
+	while (bytestoread) {
+		if (bufferbytes != 0) {
+			uint bytestocopy = (bufferbytes > bytestoread) ? bytestoread : bufferbytes;
+			memcpy(out, &buffer[bufferindex], bytestocopy);
+			//update local buffer
+			bufferbytes -= bytestocopy;
+			bufferindex += bytestocopy;
+			totalbytesread += bytestocopy;
+			//update request pointers
+			out += bytestocopy;
+			bytestoread -= bytestocopy;
+		} else {
+			ssize_t bytesread = read (filedesc, buffer, buffercap);
+			bufferindex = 0;
+			bufferbytes = bytesread;
+			if (bytesread == 0) {
+				break;
+			} else if (bytesread < 0) {
+				exit(-1);
+			}
+		}
+	}
+	return totalbytesread;
 }
 
 CSolver *Deserializer::deserialize() {
@@ -47,6 +76,9 @@ CSolver *Deserializer::deserialize() {
 		case BOOLEANVAR:
 			deserializeBooleanVar();
 			break;
+		case BOOLCONST:
+			deserializeBooleanConst();
+			break;
 		case ORDERCONST:
 			deserializeBooleanOrder();
 			break;
@@ -94,14 +126,18 @@ CSolver *Deserializer::deserialize() {
 }
 
 void Deserializer::deserializeBooleanEdge() {
-	Boolean *b;
-	myread(&b, sizeof(Boolean *));
-	BooleanEdge tmp(b);
+	Boolean *b_ptr;
+	myread(&b_ptr, sizeof(Boolean *));
+	BooleanEdge tmp(b_ptr);
 	bool isNegated = tmp.isNegated();
 	ASSERT(map.contains(tmp.getBoolean()));
-	b = (Boolean *) map.get(tmp.getBoolean());
-	BooleanEdge res(b);
-	solver->addConstraint(isNegated ? res.negate() : res);
+	b_ptr = (Boolean *) map.get(tmp.getBoolean());
+	BooleanEdge res(b_ptr);
+	bool isTopLevel;
+	myread(&isTopLevel, sizeof(bool));
+	if (isTopLevel) {
+		solver->addConstraint(isNegated ? res.negate() : res);
+	}
 }
 
 void Deserializer::deserializeBooleanVar() {
@@ -112,6 +148,15 @@ void Deserializer::deserializeBooleanVar() {
 	map.put(b, solver->getBooleanVar(vtype).getBoolean());
 }
 
+void Deserializer::deserializeBooleanConst() {
+	BooleanVar *b;
+	myread(&b, sizeof(BooleanVar *));
+	bool istrue;
+	myread(&istrue, sizeof(bool));
+	map.put(b, istrue?solver->getBooleanTrue().getBoolean():
+			solver->getBooleanFalse().getBoolean());
+}
+
 void Deserializer::deserializeBooleanOrder() {
 	BooleanOrder *bo_ptr;
 	myread(&bo_ptr, sizeof(BooleanOrder *));
@@ -145,33 +190,36 @@ void Deserializer::deserializeSet() {
 	myread(&type, sizeof(VarType));
 	bool isRange;
 	myread(&isRange, sizeof(bool));
-	uint64_t low;
-	myread(&low, sizeof(uint64_t));
-	uint64_t high;
-	myread(&high, sizeof(uint64_t));
 	bool isMutable;
 	myread(&isMutable, sizeof(bool));
-	Set *set;
-	if (isMutable) {
-		set = new MutableSet(type);
-	}
-	uint size;
-	myread(&size, sizeof(uint));
-	Vector<uint64_t> members;
-	for (uint i = 0; i < size; i++) {
-		uint64_t mem;
-		myread(&mem, sizeof(uint64_t));
+	if (isRange) {
+		uint64_t low;
+		myread(&low, sizeof(uint64_t));
+		uint64_t high;
+		myread(&high, sizeof(uint64_t));
+		map.put(s_ptr, new Set(type, low, high));
+	} else {
+		Set *set = NULL;
 		if (isMutable) {
-			((MutableSet *) set)->addElementMSet(mem);
-		} else {
-			members.push(mem);
+			set = new MutableSet(type);
 		}
+		uint size;
+		myread(&size, sizeof(uint));
+		Vector<uint64_t> members;
+		for (uint i = 0; i < size; i++) {
+			uint64_t mem;
+			myread(&mem, sizeof(uint64_t));
+			if (isMutable) {
+				((MutableSet *) set)->addElementMSet(mem);
+			} else {
+				members.push(mem);
+			}
+		}
+		if (!isMutable) {
+			set = solver->createSet(type, members.expose(), size);
+		}
+		map.put(s_ptr, set);
 	}
-	if (!isMutable) {
-		set = isRange ? solver->createRangeSet(type, low, high) :
-					solver->createSet(type, members.expose(), size);
-	}
-	map.put(s_ptr, set);
 }
 
 void Deserializer::deserializeBooleanLogic() {
@@ -247,40 +295,21 @@ void Deserializer::deserializePredicateOperator() {
 	myread(&po_ptr, sizeof(PredicateOperator *));
 	CompOp op;
 	myread(&op, sizeof(CompOp));
-	uint size;
-	myread(&size, sizeof(uint));
-	Vector<Set *> domains;
-	for (uint i = 0; i < size; i++) {
-		Set *domain;
-		myread(&domain, sizeof(Set *));
-		ASSERT(map.contains(domain));
-		domain = (Set *) map.get(domain);
-		domains.push(domain);
-	}
 
-	map.put(po_ptr, solver->createPredicateOperator(op, domains.expose(), size));
+	map.put(po_ptr, solver->createPredicateOperator(op));
 }
 
 void Deserializer::deserializeTable() {
 	Table *t_ptr;
 	myread(&t_ptr, sizeof(Table *));
-	uint size;
-	myread(&size, sizeof(uint));
-	Vector<Set *> domains;
-	for (uint i = 0; i < size; i++) {
-		Set *domain;
-		myread(&domain, sizeof(Set *));
-		ASSERT(map.contains(domain));
-		domain = (Set *) map.get(domain);
-		domains.push(domain);
-	}
 	Set *range;
 	myread(&range, sizeof(Set *));
 	if (range != NULL) {
 		ASSERT(map.contains(range));
 		range = (Set *) map.get(range);
 	}
-	Table *table = solver->createTable(domains.expose(), size, range);
+	Table *table = solver->createTable(range);
+	uint size;
 	myread(&size, sizeof(uint));
 	for (uint i = 0; i < size; i++) {
 		uint64_t output;
@@ -298,26 +327,36 @@ void Deserializer::deserializeTable() {
 
 
 void Deserializer::deserializeElementSet() {
+	bool anyValue = false;
+	myread(&anyValue, sizeof(bool));
 	ElementSet *es_ptr;
 	myread(&es_ptr, sizeof(ElementSet *));
 	Set *set;
 	myread(&set, sizeof(Set *));
 	ASSERT(map.contains(set));
 	set  = (Set *) map.get(set);
-	map.put(es_ptr, solver->getElementVar(set));
+	Element *newEl = solver->getElementVar(set);
+	newEl->anyValue = anyValue;
+	map.put(es_ptr, newEl);
 }
 
 void Deserializer::deserializeElementConst() {
+	bool anyValue = false;
+	myread(&anyValue, sizeof(bool));
 	ElementSet *es_ptr;
 	myread(&es_ptr, sizeof(ElementSet *));
 	VarType type;
 	myread(&type, sizeof(VarType));
 	uint64_t value;
 	myread(&value, sizeof(uint64_t));
-	map.put(es_ptr, solver->getElementConst(type, value));
+	Element *newEl = solver->getElementConst(type, value);
+	newEl->anyValue = anyValue;
+	map.put(es_ptr, newEl);
 }
 
 void Deserializer::deserializeElementFunction() {
+	bool anyValue = false;
+	myread(&anyValue, sizeof(bool));
 	ElementFunction *ef_ptr;
 	myread(&ef_ptr, sizeof(ElementFunction *));
 	Function *function;
@@ -343,8 +382,9 @@ void Deserializer::deserializeElementFunction() {
 	overflowstatus = (Boolean *) map.get(tmp.getBoolean());
 	BooleanEdge res(overflowstatus);
 	BooleanEdge undefStatus = isNegated ? res.negate() : res;
-
-	map.put(ef_ptr, solver->applyFunction(function, members.expose(), size, undefStatus));
+	Element *newEl = solver->applyFunction(function, members.expose(), size, undefStatus);
+	newEl->anyValue = anyValue;
+	map.put(ef_ptr, newEl);
 }
 
 
@@ -353,23 +393,13 @@ void Deserializer::deserializeFunctionOperator() {
 	myread(&fo_ptr, sizeof(FunctionOperator *));
 	ArithOp op;
 	myread(&op, sizeof(ArithOp));
-	uint size;
-	myread(&size, sizeof(uint));
-	Vector<Set *> domains;
-	for (uint i = 0; i < size; i++) {
-		Set *domain;
-		myread(&domain, sizeof(Set *));
-		ASSERT(map.contains(domain));
-		domain = (Set *) map.get(domain);
-		domains.push(domain);
-	}
 	Set *range;
 	myread(&range, sizeof(Set *));
 	ASSERT(map.contains(range));
 	range = (Set *) map.get(range);
 	OverFlowBehavior overflowbehavior;
 	myread(&overflowbehavior, sizeof(OverFlowBehavior));
-	map.put(fo_ptr, solver->createFunctionOperator(op, domains.expose(), size, range, overflowbehavior));
+	map.put(fo_ptr, solver->createFunctionOperator(op, range, overflowbehavior));
 }
 
 void Deserializer::deserializeFunctionTable() {
@@ -383,4 +413,4 @@ void Deserializer::deserializeFunctionTable() {
 	myread(&undefinedbehavior, sizeof(UndefinedBehavior));
 
 	map.put(ft_ptr, solver->completeTable(table, undefinedbehavior));
-}
\ No newline at end of file
+}