Adding reset to the solver

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 356b4153bebb33d7f1b3cccc4d49ac410201679a..84862828a9c72928cc565cf86d285de9571d0103 100644 (file)
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -78,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);

diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index 1333b6cbab052c2390402bef123975f75080eb37..0683230f24c23c475275b69bef915c7d7a8da2a3 100644 (file)
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -177,6 +177,7 @@ static inline Literal getProxy(CNFExpr *expr) {
 
 CNF *createCNF();
 void deleteCNF(CNF *cnf);
+void resetCNF(CNF *cnf);
 
 uint hashNode(NodeType type, uint numEdges, Edge *edges);
 Node *allocNode(NodeType type, uint numEdges, Edge *edges, uint hashCode);

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 2a58c0682ae57e88e75f39312afcc4378642e40c..206d2b7fe30857c553fcc651f967c9ed44fd45e0 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -21,6 +21,11 @@ SATEncoder::~SATEncoder() {
        deleteCNF(cnf);
 }
 
+void SATEncoder::resetSATEncoder(){
+        resetCNF(cnf);
+        booledgeMap.reset();
+}
+
 int SATEncoder::solve() {
        return solveCNF(cnf);
 }

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 08ec52707c2fe57988df6670022be6263085e888..dcf3b86ad30cb40a0fb3770144d6550eba11bd94 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -13,6 +13,7 @@ public:
        int solve();
        SATEncoder(CSolver *solver);
        ~SATEncoder();
+        void resetSATEncoder();
        void encodeAllSATEncoder(CSolver *csolver);
        Edge encodeConstraintSATEncoder(BooleanEdge constraint);
        CNF *getCNF() { return cnf;}

diff --git a/src/csolver.cc b/src/csolver.cc
index e844e792eb305c4cc1c53cb59022326de8a71113..e4e045293ab1bf846abf2b4a6ffa182e7bd66e5e 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -40,7 +40,7 @@ CSolver::CSolver() :
 /** This function tears down the solver and the entire AST */
 
 CSolver::~CSolver() {
-       serialize();
+       //serialize();
        uint size = allBooleans.getSize();
        for (uint i = 0; i < size; i++) {
                delete allBooleans.get(i);
@@ -80,6 +80,64 @@ CSolver::~CSolver() {
        delete satEncoder;
 }
 
+void CSolver::resetSolver(){
+        //serialize();
+        uint size = allBooleans.getSize();
+       for (uint i = 0; i < size; i++) {
+               delete allBooleans.get(i);
+       }
+
+       size = allSets.getSize();
+       for (uint i = 0; i < size; i++) {
+               delete allSets.get(i);
+       }
+
+       size = allElements.getSize();
+       for (uint i = 0; i < size; i++) {
+                Element* el = allElements.get(i);
+               delete el;
+       }
+
+       size = allTables.getSize();
+       for (uint i = 0; i < size; i++) {
+               delete allTables.get(i);
+       }
+
+       size = allPredicates.getSize();
+       for (uint i = 0; i < size; i++) {
+               delete allPredicates.get(i);
+       }
+
+       size = allOrders.getSize();
+       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);
+       }
+       delete boolTrue.getBoolean();
+        allBooleans.clear();
+        allSets.clear();
+        allElements.clear();
+        allTables.clear();
+        allPredicates.clear();
+        allOrders.clear();
+        allFunctions.clear();
+        constraints.reset();
+        activeOrders.reset();
+        boolMap.reset();
+       elemMap.reset();
+        
+        boolTrue = BooleanEdge(new BooleanConst(true));
+       boolFalse = boolTrue.negate();
+        unsat = false;
+        elapsedTime = 0;
+        tuner = NULL;
+        satEncoder->resetSATEncoder();
+        
+}
+
 CSolver *CSolver::clone() {
        CSolver *copy = new CSolver();
        CloneMap map;

diff --git a/src/csolver.h b/src/csolver.h
index bac1a4961488defbbb4dcf1d45bfb140783614a0..ffbfe3585227062329e1eae09cdc3643f16f32b7 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -11,7 +11,7 @@ class CSolver {
 public:
        CSolver();
        ~CSolver();
-
+        void resetSolver();
        /** This function creates a set containing the elements passed in the array. */
        Set *createSet(VarType type, uint64_t *elements, uint num);