From f3c86fbf07d5c10e4b0bbd6054f75dccb6f622f0 Mon Sep 17 00:00:00 2001
From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Mon, 23 Oct 2017 13:54:01 -0700
Subject: [PATCH] Bug fix

---
 src/Serialize/deserializer.cc                 | 19 ++++++++++---------
 src/Serialize/serializer.cc                   | 10 +++++++---
 src/Serialize/serializer.h                    |  2 +-
 .../{deserializer.cc => deserializertest.cc}  |  1 +
 src/csolver.cc                                |  8 ++++++--
 5 files changed, 25 insertions(+), 15 deletions(-)
 rename src/Test/{deserializer.cc => deserializertest.cc} (91%)

diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc
index 6f14484..c0b8bf4 100644
--- 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 810ece8..bd57925 100644
--- 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 f147773..cf30a55 100644
--- 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/deserializertest.cc
similarity index 91%
rename from src/Test/deserializer.cc
rename to src/Test/deserializertest.cc
index 85fffc3..bbef427 100644
--- a/src/Test/deserializer.cc
+++ b/src/Test/deserializertest.cc
@@ -8,6 +8,7 @@ int main(int argc, char ** argv){
 	}
 	CSolver* solver = CSolver::deserialize(argv[1]);
 	solver->printConstraints();
+        delete solver;
 	return 1;
 		
 }
diff --git a/src/csolver.cc b/src/csolver.cc
index 624160e..5b8f4ca 100644
--- 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);
-- 
2.34.1