Merge

diff --combined src/csolver.cc
index a2163a0c839103179fc6a31df3608ea71651d8a9,d316724791f2648aa332e989d6a3507d99b8c0aa..71205f68aab557baf933689510435ee4f312d328
--- 1/src/csolver.cc
--- 2/src/csolver.cc
+++ b/src/csolver.cc
@@@ -48,7 -48,8 +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();
@@@ -65,6 -66,7 +66,6 @@@
        for (uint i = 0; i < size; i++) {
                delete allOrders.get(i);
        }
 -
        size = allFunctions.getSize();
        for (uint i = 0; i < size; i++) {
                delete allFunctions.get(i);
@@@ -86,22 -88,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) {
@@@ -173,7 -175,6 +174,7 @@@ Element *CSolver::getElementConst(VarTy
        }
  }
  
 +
  Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) {
        Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
        Element *e = elemMap.get(element);
@@@ -310,11 -311,13 +311,11 @@@ BooleanEdge CSolver::applyLogicalOperat
        }
        case SATC_IFF: {
                for (uint i = 0; i < 2; i++) {
 -                      if (array[i]->type == BOOLCONST) {
 -                              if (isTrue(array[i])) { // It can be undefined
 -                                      return array[1 - i];
 -                              } else if (isFalse(array[i])) {
 -                                      newarray[0] = array[1 - i];
 -                                      return applyLogicalOperation(SATC_NOT, newarray, 1);
 -                              }
 +                      if (isTrue(array[i])) { // It can be undefined
 +                              return array[1 - i];
 +                      } else if (isFalse(array[i])) {
 +                              newarray[0] = array[1 - i];
 +                              return applyLogicalOperation(SATC_NOT, newarray, 1);
                        } else if (array[i]->type == LOGICOP) {
                                BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
                                if (b->replaced) {
@@@ -338,10 -341,12 +339,10 @@@
                                if (((BooleanLogic *)b.getBoolean())->replaced)
                                        return rewriteLogicalOperation(op, array, asize);
                        }
 -                      if (b->type == BOOLCONST) {
 -                              if (isTrue(b))
 -                                      continue;
 -                              else {
 -                                      return boolFalse;
 -                              }
 +                      if (isTrue(b))
 +                              continue;
 +                      else if (isFalse(b)) {
 +                              return boolFalse;
                        } else
                                newarray[newindex++] = b;
                }
@@@ -384,7 -389,7 +385,7 @@@ BooleanEdge CSolver::orderConstraint(Or
        //      ASSERT(first != second);
        if (first == second)
                return getBooleanFalse();
 -      
 +
        bool negate = false;
        if (order->type == SATC_TOTAL) {
                if (first > second) {
@@@ -411,6 -416,12 +412,12 @@@
  }
  
  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 -482,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 -510,7 +506,6 @@@ void CSolver::printConstraints() 
                model_print("\n");
        }
        delete it;
--
  }
  
  void CSolver::printConstraint(BooleanEdge b) {