X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2Fcsolver.cc;h=ce749b13c27b20d1645383f86e27f5101e3a6234;hp=d8e08729ab27d2fc5dd3b90dbe0b8d73f138402a;hb=abe0dee853780f8254436b0de7c8330d326d4017;hpb=516fb5585a776bde6277eeb3c46f09620dd20a5f

diff --git a/src/csolver.cc b/src/csolver.cc
index d8e0872..ce749b1 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -17,7 +17,10 @@
 #include "structs.h"
 #include "orderresolver.h"
 #include "integerencoding.h"
-#include <stdlib.h>
+#include "qsort.h"
+#include "preprocess.h"
+#include "serializer.h"
+#include "deserializer.h"
 
 CSolver::CSolver() :
 	boolTrue(BooleanEdge(new BooleanConst(true))),
@@ -83,6 +86,25 @@ CSolver *CSolver::clone() {
 	return copy;
 }
 
+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();
+	}
+	
+}
+
 Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
 	Set *set = new Set(type, elements, numelements);
 	allSets.push(set);
@@ -125,7 +147,7 @@ Element *CSolver::getElementVar(Set *set) {
 Element *CSolver::getElementConst(VarType type, uint64_t value) {
 	uint64_t array[] = {value};
 	Set *set = new Set(type, array, 1);
-	Element *element = new ElementConst(value, type, set);
+	Element *element = new ElementConst(value, set);
 	Element *e = elemMap.get(element);
 	if (e == NULL) {
 		allSets.push(set);
@@ -318,7 +340,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 		} else if (newindex == 1) {
 			return newarray[0];
 		} else {
-			qsort(newarray, newindex, sizeof(BooleanEdge), ptrcompares);
+			bsdqsort(newarray, newindex, sizeof(BooleanEdge), ptrcompares);
 			array = newarray;
 			asize = newindex;
 		}
@@ -403,6 +425,9 @@ int CSolver::solve() {
 	long long startTime = getTimeNano();
 	computePolarities(this);
 
+	Preprocess pp(this);
+	pp.doTransform();
+	
 	DecomposeOrderTransform dot(this);
 	dot.doTransform();