Calling alloy first when deserializing
authorHamed Gorjiara <hgorjiar@uci.edu>
Thu, 7 Feb 2019 01:00:29 +0000 (17:00 -0800)
committerHamed Gorjiara <hgorjiar@uci.edu>
Thu, 7 Feb 2019 01:00:29 +0000 (17:00 -0800)
src/Serialize/deserializer.cc
src/Serialize/deserializer.h
src/Test/deserializealloytest.cc
src/csolver.cc
src/csolver.h

index c9a708c..8b1e3fd 100644 (file)
@@ -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() {
index 81baeef..6af5880 100644 (file)
@@ -19,7 +19,7 @@
  */
 class Deserializer {
 public:
-       Deserializer(const char *file);
+       Deserializer(const char *file, bool alloy = false);
        CSolver *deserialize();
        virtual ~Deserializer();
 private:
index d607621..3cb13fe 100644 (file)
@@ -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]);
index 3c8fffa..c81e2f3 100644 (file)
@@ -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() {
index e972b7c..74d0bf6 100644 (file)
@@ -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);