Improve hash function to fix collision problem

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index 7fa33f2459c2d18df7dfc43683f667c4e75b3f81..533fc4b8dfd0023c3b66498c898599056fb7b2c4 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -22,6 +22,7 @@
 #include "serializer.h"
 #include "deserializer.h"
 #include "encodinggraph.h"
+#include <time.h>
 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),
@@ -48,7 +49,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,7 +67,6 @@ CSolver::~CSolver() {
        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);
@@ -87,23 +88,27 @@ 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();
-       }
+       char buffer[255];
+       struct timespec t;
+       clock_gettime(CLOCK_REALTIME, &t);
 
+       unsigned long long nanotime=t.tv_sec*1000000000+t.tv_nsec;
+       int numchars=sprintf(buffer, "DUMP%llu", nanotime);
+       Serializer serializer(buffer);
+       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) {
@@ -175,6 +180,7 @@ Element *CSolver::getElementConst(VarType type, uint64_t value) {
        }
 }
 
+
 Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) {
        Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
        Element *e = elemMap.get(element);
@@ -311,13 +317,11 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
        }
        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) {
@@ -341,12 +345,10 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
                                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;
                }
@@ -386,7 +388,10 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 }
 
 BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
-       ASSERT(first != second);
+       //      ASSERT(first != second);
+       if (first == second)
+               return getBooleanFalse();
+
        bool negate = false;
        if (order->type == SATC_TOTAL) {
                if (first > second) {
@@ -408,7 +413,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
                constraint = b;
        }
 
-       BooleanEdge be=BooleanEdge(constraint);
+       BooleanEdge be = BooleanEdge(constraint);
        return negate ? be.negate() : be;
 }
 
@@ -460,7 +465,7 @@ int CSolver::solve() {
                tuner = new DefaultTuner();
                deleteTuner = true;
        }
-
+       
        long long startTime = getTimeNano();
        computePolarities(this);
 
@@ -476,7 +481,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);
@@ -501,7 +506,13 @@ void CSolver::printConstraints() {
                model_print("\n");
        }
        delete it;
+}
 
+void CSolver::printConstraint(BooleanEdge b) {
+       if (b.isNegated())
+               model_print("!");
+       b->print();
+       model_print("\n");
 }
 
 uint64_t CSolver::getElementValue(Element *element) {