X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FSerialize%2Fdeserializer.cc;h=8b1e3fd00cf1a81745763b8f0236dafea783a249;hp=56acc523676c382af2a15edb3a1abebd76f243eb;hb=dbe12973cd2236f5e76a70c24f68a05aeb3660c5;hpb=e80028bf761f04dd410b45d1dadc0b8b5fd5817e

diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc
index 56acc52..8b1e3fd 100644
--- a/src/Serialize/deserializer.cc
+++ b/src/Serialize/deserializer.cc
@@ -17,7 +17,7 @@
 
 #define READBUFFERSIZE 16384
 
-Deserializer::Deserializer(const char *file) :
+Deserializer::Deserializer(const char *file, bool alloy) :
 	buffer((char *) ourmalloc(READBUFFERSIZE)),
 	bufferindex(0),
 	bufferbytes(0),
@@ -29,6 +29,9 @@ Deserializer::Deserializer(const char *file) :
 	if (filedesc < 0) {
 		exit(-1);
 	}
+	if(alloy){
+		solver->setAlloyEncoder();
+	}
 }
 
 Deserializer::~Deserializer() {
@@ -76,6 +79,9 @@ CSolver *Deserializer::deserialize() {
 		case BOOLEANVAR:
 			deserializeBooleanVar();
 			break;
+		case BOOLCONST:
+			deserializeBooleanConst();
+			break;
 		case ORDERCONST:
 			deserializeBooleanOrder();
 			break;
@@ -145,6 +151,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 *));
@@ -283,40 +298,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;
@@ -334,26 +330,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;
@@ -379,7 +385,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);
 }
 
 
@@ -388,23 +396,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() {