Bug fix

diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc
index 6f14484c95646b2da6752ef9cb77e8d2fa27b437..c0b8bf4fcddbcc9e6a5c655df31fdf1e3db6d6ca 100644 (file)
--- a/src/Serialize/deserializer.cc
+++ b/src/Serialize/deserializer.cc
@@ -26,8 +26,6 @@ Deserializer::Deserializer(const char *file) :
 }
 
 Deserializer::~Deserializer() {
-       delete solver;
-
        if (-1 == close(filedesc)) {
                exit(-1);
        }
@@ -94,14 +92,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() {
@@ -346,7 +348,6 @@ 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));
 }
 

diff --git a/src/Serialize/serializer.cc b/src/Serialize/serializer.cc
index 810ece81237929aed77dba5d43c2764d42f7f8c8..bd579258f355caaccfbb7d0e592649b3f6fc0ce5 100644 (file)
--- a/src/Serialize/serializer.cc
+++ b/src/Serialize/serializer.cc
@@ -30,12 +30,16 @@ void Serializer::mywrite(const void *__buf, size_t __n) {
 }
 
 
-void serializeBooleanEdge(Serializer *serializer, BooleanEdge be) {
-       if (be == BooleanEdge(NULL))
-               return;
+void serializeBooleanEdge(Serializer *serializer, BooleanEdge be, bool isTopLevel) {
+       if (be == BooleanEdge(NULL)){
+               Boolean* boolean = NULL;
+                serializer->mywrite(&boolean, sizeof(Boolean *));
+                return;
+        }
        be.getBoolean()->serialize(serializer);
        ASTNodeType type = BOOLEANEDGE;
        serializer->mywrite(&type, sizeof(ASTNodeType));
        Boolean *boolean = be.getRaw();
        serializer->mywrite(&boolean, sizeof(Boolean *));
+        serializer->mywrite(&isTopLevel, sizeof(bool));
 }
\ No newline at end of file

diff --git a/src/Serialize/serializer.h b/src/Serialize/serializer.h
index f147773f5ebf9fae2533ebd38da5d4130d0ab9c3..cf30a55e952494cd6b480aca694a6dcf1797e444 100644 (file)
--- a/src/Serialize/serializer.h
+++ b/src/Serialize/serializer.h
@@ -33,7 +33,7 @@ inline bool Serializer::isSerialized(void *obj) {
 
 
 
-void serializeBooleanEdge(Serializer *serializer, BooleanEdge be);
+void serializeBooleanEdge(Serializer *serializer, BooleanEdge be, bool isTopLevel=false);
 
 #endif/* SERIALIZER_H */
 

diff --git a/src/Test/deserializer.cc b/src/Test/deserializer.cc
deleted file mode 100644 (file)
index 85fffc3..0000000
--- a/src/Test/deserializer.cc
+++ /dev/null
@@ -1,13 +0,0 @@
-#include "csolver.h"
-
-
-int main(int argc, char ** argv){
-       if(argc != 2){
-               printf("You only specify the name of the file ...");
-               exit(-1);       
-       }
-       CSolver* solver = CSolver::deserialize(argv[1]);
-       solver->printConstraints();
-       return 1;
-               
-}

diff --git a/src/Test/deserializertest.cc b/src/Test/deserializertest.cc
new file mode 100644 (file)
index 0000000..bbef427
--- /dev/null
+++ b/src/Test/deserializertest.cc
@@ -0,0 +1,14 @@
+#include "csolver.h"
+
+
+int main(int argc, char ** argv){
+       if(argc != 2){
+               printf("You only specify the name of the file ...");
+               exit(-1);       
+       }
+       CSolver* solver = CSolver::deserialize(argv[1]);
+       solver->printConstraints();
+        delete solver;
+       return 1;
+               
+}

diff --git a/src/csolver.cc b/src/csolver.cc
index 624160ecb0b8696230eb40e01d347fca03a8476c..5b8f4cacdb0907bffbcba397434bf3a657e4dbf4 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -96,11 +96,12 @@ CSolver* CSolver::deserialize(const char * file){
 
 void CSolver::serialize() {
        model_print("serializing ...\n");
+        printConstraints();
        Serializer serializer("dump");
        SetIteratorBooleanEdge *it = getConstraints();
        while (it->hasNext()) {
                BooleanEdge b = it->next();
-               serializeBooleanEdge(&serializer, b);
+               serializeBooleanEdge(&serializer, b, true);
        }
        delete it;
 }
@@ -395,6 +396,9 @@ void CSolver::addConstraint(BooleanEdge constraint) {
 #ifdef TRACE_DEBUG
         model_println("****New Constraint******");
 #endif
+        if(constraint.isNegated())
+                model_print("!");
+        constraint.getBoolean()->print();
        if (isTrue(constraint))
                return;
        else if (isFalse(constraint)) {
@@ -458,7 +462,7 @@ int CSolver::solve() {
        EncodingGraph eg(this);
        eg.buildGraph();
        eg.encode();
-       printConstraints();
+//     printConstraints();
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
        model_print("Is problem UNSAT after encoding: %d\n", unsat);