Adding reset to the solver

[satune.git] / src / Backend / constraint.cc

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 61fba12ed5ed190aa967347bc3c05fefa74e0c29..84862828a9c72928cc565cf86d285de9571d0103 100644 (file)
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -4,6 +4,7 @@
 #include "inc_solver.h"
 #include "cnfexpr.h"
 #include "common.h"
+#include "qsort.h"
 /*
    V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
    Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
@@ -77,6 +78,25 @@ void deleteCNF(CNF *cnf) {
        ourfree(cnf);
 }
 
+void resetCNF(CNF *cnf){
+        for (uint i = 0; i < cnf->capacity; i++) {
+               Node *n = cnf->node_array[i];
+               if (n != NULL)
+                       ourfree(n);
+       }
+        clearVectorEdge(&cnf->constraints);
+        clearVectorEdge(&cnf->args);
+        deleteIncrementalSolver(cnf->solver);
+        memset(cnf->node_array, 0, sizeof(Node *) * cnf->capacity);
+        
+        cnf->varcount = 1;
+        cnf->size = 0;
+        cnf->enableMatching = true;
+        cnf->solver = allocIncrementalSolver();
+        cnf->solveTime = 0;
+       cnf->encodeTime = 0;
+}
+
 void resizeCNF(CNF *cnf, uint newCapacity) {
        Node **old_array = cnf->node_array;
        Node **new_array = (Node **) ourcalloc(1, sizeof(Node *) * newCapacity);
@@ -145,12 +165,19 @@ Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge *edges) {
 }
 
 uint hashNode(NodeType type, uint numEdges, Edge *edges) {
-       uint hashvalue = type ^ numEdges;
+       uint hash = type;
+       hash += hash << 10;
+       hash ^= hash >> 6;
        for (uint i = 0; i < numEdges; i++) {
-               hashvalue ^= (uint) ((uintptr_t) edges[i].node_ptr);
-               hashvalue = (hashvalue << 3) | (hashvalue >> 29);       //rotate left by 3 bits
+               uint c = (uint) ((uintptr_t) edges[i].node_ptr);
+               hash += c;
+               hash += hash << 10;
+               hash += hash >> 6;
        }
-       return (uint) hashvalue;
+       hash += hash << 3;
+       hash ^= hash >> 11;
+       hash += hash << 15;
+       return hash;
 }
 
 bool compareNodes(Node *node, NodeType type, uint numEdges, Edge *edges) {
@@ -187,7 +214,7 @@ int comparefunction(const Edge *e1, const Edge *e2) {
 
 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
        ASSERT(numEdges != 0);
-       qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
+       bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
        uint initindex = 0;
        while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
                initindex++;
@@ -343,7 +370,9 @@ int solveCNF(CNF *cnf) {
        int result = solve(cnf->solver);
        long long finishTime = getTimeNano();
        cnf->encodeTime = startSolve - startTime;
+        model_print("CNF Encode time: %f\n", cnf->encodeTime/1000000000.0);
        cnf->solveTime = finishTime - startSolve;
+       model_print("Solve time: %f\n", cnf->solveTime/ 1000000000.0);
        return result;
 }