Calling alloy first when deserializing

diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc
index c9a708ce4e625311d905da22bb1b37781327b74f..8b1e3fd00cf1a81745763b8f0236dafea783a249 100644 (file)
--- 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 81baeef65b17e7c34ac8985c7972ff94912acc1f..6af58800ca8ec739be548f4e062bb7bf0c631642 100644 (file)
--- 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 d607621358bd0d814be54fead7f15cad23ffd224..3cb13feb95f9fc8b3c2147f02d55fe29826081c5 100644 (file)
--- 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 3c8fffa510f16b01b6be889703e84ea83a5b7972..c81e2f3e1c1941789dc0259467dc1f206881193e 100644 (file)
--- 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 e972b7c598471fd77adacbdd741dcbce78a92828..74d0bf6e2c64b9e237f7ab0e9381b6b40a3f7c63 100644 (file)
--- 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);