More bug fix

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index fe3d9d91a0c69fd0e9854715eb3fcfbc20232e27..5b8f4cacdb0907bffbcba397434bf3a657e4dbf4 100644 (file)
--- 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();
@@ -87,23 +88,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) {
@@ -393,9 +393,12 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {
-       if (constraint.isNegated())
-               model_print("!");
-       constraint.getBoolean()->print();
+#ifdef TRACE_DEBUG
+        model_println("****New Constraint******");
+#endif
+        if(constraint.isNegated())
+                model_print("!");
+        constraint.getBoolean()->print();
        if (isTrue(constraint))
                return;
        else if (isFalse(constraint)) {
@@ -447,19 +450,19 @@ int CSolver::solve() {
        long long startTime = getTimeNano();
        computePolarities(this);
 
-       //Preprocess pp(this);
-       //pp.doTransform();
-
-       //DecomposeOrderTransform dot(this);
-       //      dot.doTransform();
+       Preprocess pp(this);
+       pp.doTransform();
 
-       //IntegerEncodingTransform iet(this);
-       //      iet.doTransform();
+       DecomposeOrderTransform dot(this);
+       dot.doTransform();
 
-       //EncodingGraph eg(this);
-       //eg.buildGraph();
-       //eg.encode();
+       IntegerEncodingTransform iet(this);
+       iet.doTransform();
 
+       EncodingGraph eg(this);
+       eg.buildGraph();
+       eg.encode();
+//     printConstraints();
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
@@ -474,6 +477,19 @@ int CSolver::solve() {
        return result;
 }
 
+void CSolver::printConstraints() {
+       SetIteratorBooleanEdge *it = getConstraints();
+       while (it->hasNext()) {
+               BooleanEdge b = it->next();
+               if (b.isNegated())
+                       model_print("!");
+               b->print();
+               model_print("\n");
+       }
+       delete it;
+
+}
+
 uint64_t CSolver::getElementValue(Element *element) {
        switch (element->type) {
        case ELEMSET: