From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Thu, 7 Feb 2019 01:00:29 +0000 (-0800)
Subject: Calling alloy first when deserializing
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=dbe12973cd2236f5e76a70c24f68a05aeb3660c5

Calling alloy first when deserializing
---

diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc
index c9a708c..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() {
diff --git a/src/Serialize/deserializer.h b/src/Serialize/deserializer.h
index 81baeef..6af5880 100644
--- a/src/Serialize/deserializer.h
+++ b/src/Serialize/deserializer.h
@@ -19,7 +19,7 @@
  */
 class Deserializer {
 public:
-	Deserializer(const char *file);
+	Deserializer(const char *file, bool alloy = false);
 	CSolver *deserialize();
 	virtual ~Deserializer();
 private:
diff --git a/src/Test/deserializealloytest.cc b/src/Test/deserializealloytest.cc
index d607621..3cb13fe 100644
--- a/src/Test/deserializealloytest.cc
+++ b/src/Test/deserializealloytest.cc
@@ -8,9 +8,12 @@ int main(int argc, char **argv) {
 		printf("./run.sh deserializer test.dump [--alloy]\n");
 		exit(-1);
 	}
-	CSolver *solver = CSolver::deserialize(argv[1]);
-	if(argc == 3)
-		solver->setAlloyEncoder();
+	CSolver *solver; 
+	if(argc == 3){
+		solver = CSolver::deserialize(argv[1], true);
+	} else {
+		solver = CSolver::deserialize(argv[1]);
+	}
 	int value = solver->solve();
 	if (value == 1) {
 		printf("%s is SAT\n", argv[1]);
diff --git a/src/csolver.cc b/src/csolver.cc
index 3c8fffa..c81e2f3 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -158,9 +158,9 @@ CSolver *CSolver::clone() {
 	return copy;
 }
 
-CSolver *CSolver::deserialize(const char *file) {
+CSolver *CSolver::deserialize(const char *file, bool alloy) {
 	model_print("deserializing %s ...\n", file);
-	Deserializer deserializer(file);
+	Deserializer deserializer(file, alloy);
 	return deserializer.deserialize();
 }
 
@@ -676,7 +676,9 @@ int CSolver::solve() {
 }
 
 void CSolver::setAlloyEncoder(){
-	alloyEncoder = new AlloyEnc(this);
+	if(alloyEncoder == NULL){
+		alloyEncoder = new AlloyEnc(this);
+	}
 }
 
 void CSolver::printConstraints() {
diff --git a/src/csolver.h b/src/csolver.h
index e972b7c..74d0bf6 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -161,7 +161,7 @@ public:
 	void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
 	CSolver *clone();
 	void serialize();
-	static CSolver *deserialize(const char *file);
+	static CSolver *deserialize(const char *file, bool alloy = false);
 	void autoTune(uint budget);
 	void inferFixedOrders();
 	void inferFixedOrder(Order *order);