From: bdemsky <bdemsky@uci.edu>
Date: Mon, 23 Oct 2017 22:12:22 +0000 (-0700)
Subject: Merge
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=44ac39afe074506f18b8d2c29430cc7d88ace944;hp=649d48d2697fb45f36bbbdd52ee067d7b5490fb2

Merge
---

diff --git a/src/AST/element.h b/src/AST/element.h
index b74e582..1e7b1f2 100644
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -26,6 +26,7 @@ public:
 class ElementSet : public Element {
 public:
 	ElementSet(ASTNodeType type, Set *s);
+        virtual ~ElementSet(){}
 	ElementSet(Set *s);
 	virtual Element *clone(CSolver *solver, CloneMap *map);
 	virtual void serialize(Serializer *serializer);
@@ -40,6 +41,7 @@ protected:
 class ElementConst : public ElementSet {
 public:
 	ElementConst(uint64_t value, Set *_set);
+        virtual ~ElementConst(){}
 	uint64_t value;
 	virtual void serialize(Serializer *serializer);
 	virtual void print();
@@ -49,6 +51,7 @@ public:
 
 class ElementFunction : public Element {
 public:
+        virtual ~ElementFunction(){}
 	ElementFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus);
 	Array<Element *> inputs;
 	BooleanEdge overflowstatus;
diff --git a/src/AST/set.cc b/src/AST/set.cc
index 0a6e14f..52494e3 100644
--- a/src/AST/set.cc
+++ b/src/AST/set.cc
@@ -139,16 +139,19 @@ void Set::serialize(Serializer *serializer) {
 	serializer->mywrite(&This, sizeof(Set *));
 	serializer->mywrite(&type, sizeof(VarType));
 	serializer->mywrite(&isRange, sizeof(bool));
-	serializer->mywrite(&low, sizeof(uint64_t));
-	serializer->mywrite(&high, sizeof(uint64_t));
-	bool isMutable = isMutableSet();
+        bool isMutable = isMutableSet();
 	serializer->mywrite(&isMutable, sizeof(bool));
-	uint size = members->getSize();
-	serializer->mywrite(&size, sizeof(uint));
-	for (uint i = 0; i < size; i++) {
-		uint64_t mem = members->get(i);
-		serializer->mywrite(&mem, sizeof(uint64_t));
-	}
+        if(isRange){
+                serializer->mywrite(&low, sizeof(uint64_t));
+                serializer->mywrite(&high, sizeof(uint64_t));
+        }else {
+                uint size = members->getSize();
+                serializer->mywrite(&size, sizeof(uint));
+                for(uint i=0; i<size; i++){
+                        uint64_t mem = members->get(i);
+                        serializer->mywrite(&mem, sizeof(uint64_t));
+                }
+        }
 }
 
 void Set::print() {
diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc
index cd1e1a2..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() {
@@ -145,33 +147,36 @@ void Deserializer::deserializeSet() {
 	myread(&type, sizeof(VarType));
 	bool isRange;
 	myread(&isRange, sizeof(bool));
-	uint64_t low;
-	myread(&low, sizeof(uint64_t));
-	uint64_t high;
-	myread(&high, sizeof(uint64_t));
-	bool isMutable;
+        bool isMutable;
 	myread(&isMutable, sizeof(bool));
-	Set *set;
-	if (isMutable) {
-		set = new MutableSet(type);
-	}
-	uint size;
-	myread(&size, sizeof(uint));
-	Vector<uint64_t> members;
-	for (uint i = 0; i < size; i++) {
-		uint64_t mem;
-		myread(&mem, sizeof(uint64_t));
-		if (isMutable) {
-			((MutableSet *) set)->addElementMSet(mem);
-		} else {
-			members.push(mem);
-		}
-	}
-	if (!isMutable) {
-		set = isRange ? solver->createRangeSet(type, low, high) :
-					solver->createSet(type, members.expose(), size);
-	}
-	map.put(s_ptr, set);
+        if(isRange){
+                uint64_t low;
+                myread(&low, sizeof(uint64_t));
+                uint64_t high;
+                myread(&high, sizeof(uint64_t));
+                map.put(s_ptr, new Set(type, low, high));
+        } else{
+                Set *set;
+                if(isMutable){
+                        set = new MutableSet(type);
+                }
+                uint size;
+                myread(&size, sizeof(uint));
+                Vector<uint64_t> members;
+                for(uint i=0; i<size; i++){
+                        uint64_t mem;
+                        myread(&mem, sizeof(uint64_t));
+                        if(isMutable) {
+                                ((MutableSet*) set)->addElementMSet(mem);
+                        }else {
+                                members.push(mem);
+                        }
+                }
+                if(!isMutable){
+                        set = solver->createSet(type, members.expose(), size);
+                }
+                map.put(s_ptr, set);
+        }
 }
 
 void Deserializer::deserializeBooleanLogic() {
@@ -343,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));
 }
 
@@ -383,4 +387,4 @@ void Deserializer::deserializeFunctionTable() {
 	myread(&undefinedbehavior, sizeof(UndefinedBehavior));
 
 	map.put(ft_ptr, solver->completeTable(table, undefinedbehavior));
-}
\ No newline at end of file
+}
diff --git a/src/Serialize/serializer.cc b/src/Serialize/serializer.cc
index 810ece8..118cf86 100644
--- a/src/Serialize/serializer.cc
+++ b/src/Serialize/serializer.cc
@@ -30,12 +30,14 @@ 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)){
+                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/deserializertest.cc b/src/Test/deserializertest.cc
new file mode 100644
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/common.h b/src/common.h
index fb4d7ba..3d3adba 100644
--- a/src/common.h
+++ b/src/common.h
@@ -19,17 +19,21 @@
 #include "time.h"
 
 
-#if 1
+#ifdef SATCHECK_CONFIG
 extern int model_out;
 extern int model_err;
 extern int switch_alloc;
 
 #define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0)
+
 #define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0)
 #define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
 #else
-#define model_print printf
+    #define model_print printf
 #endif
+#define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0)
+
+
 
 #define NEXTPOW2(x) ((x == 1) ? 1 : (1 << (sizeof(uint) * 8 - __builtin_clz(x - 1))))
 #define NUMBITS(x) ((x == 0) ? 0 : 8 * sizeof(x) - __builtin_clz(x))
diff --git a/src/config.h b/src/config.h
index db02014..0c53dd6 100644
--- a/src/config.h
+++ b/src/config.h
@@ -19,7 +19,7 @@
 //#define CONFIG_DEBUG
 #define TRACE_DEBUG
 #endif
-
+//#define SATCHECK_CONFIG
 #ifndef CONFIG_ASSERT
 #define CONFIG_ASSERT
 #endif
diff --git a/src/csolver.cc b/src/csolver.cc
index a2163a0..71205f6 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -48,7 +48,8 @@ CSolver::~CSolver() {
 
 	size = allElements.getSize();
 	for (uint i = 0; i < size; i++) {
-		delete allElements.get(i);
+                Element* el = allElements.get(i);
+		delete el;
 	}
 
 	size = allTables.getSize();
@@ -86,22 +87,22 @@ CSolver *CSolver::clone() {
 	return copy;
 }
 
+CSolver* CSolver::deserialize(const char * file){
+	model_print("deserializing ...\n");
+	Deserializer deserializer(file);
+	return deserializer.deserialize();
+}
+
 void CSolver::serialize() {
 	model_print("serializing ...\n");
-	{
-		Serializer serializer("dump");
-		SetIteratorBooleanEdge *it = getConstraints();
-		while (it->hasNext()) {
-			BooleanEdge b = it->next();
-			serializeBooleanEdge(&serializer, b);
-		}
-		delete it;
-	}
-	model_print("deserializing ...\n");
-	{
-		Deserializer deserializer("dump");
-		deserializer.deserialize();
+        printConstraints();
+	Serializer serializer("dump");
+	SetIteratorBooleanEdge *it = getConstraints();
+	while (it->hasNext()) {
+		BooleanEdge b = it->next();
+		serializeBooleanEdge(&serializer, b, true);
 	}
+	delete it;
 }
 
 Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
@@ -411,6 +412,12 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
 }
 
 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)) {
@@ -471,10 +478,10 @@ int CSolver::solve() {
 	//IntegerEncodingTransform iet(this);
 	//iet.doTransform();
 
-	//EncodingGraph eg(this);
-	//eg.buildGraph();
-	//eg.encode();
-	//printConstraints();
+	EncodingGraph eg(this);
+	eg.buildGraph();
+	eg.encode();
+//	printConstraints();
 	naiveEncodingDecision(this);
 	satEncoder->encodeAllSATEncoder(this);
 	model_print("Is problem UNSAT after encoding: %d\n", unsat);
@@ -499,7 +506,6 @@ void CSolver::printConstraints() {
 		model_print("\n");
 	}
 	delete it;
-
 }
 
 void CSolver::printConstraint(BooleanEdge b) {
diff --git a/src/csolver.h b/src/csolver.h
index 2730a93..16396f9 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -152,6 +152,7 @@ public:
 	void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
 	CSolver *clone();
 	void serialize();
+	static CSolver* deserialize(const char * file);
 	void autoTune(uint budget);
 
 	void setTuner(Tuner *_tuner) { tuner = _tuner; }
diff --git a/src/mymemory.h b/src/mymemory.h
index 92fb0fe..700fb4f 100644
--- a/src/mymemory.h
+++ b/src/mymemory.h
@@ -26,7 +26,7 @@
    void * ourrealloc(void *ptr, size_t size);
  */
 
-#if 1
+#ifdef SATCHECK_CONFIG
 void *model_malloc(size_t size);
 void model_free(void *ptr);
 void *model_calloc(size_t count, size_t size);