From 6372bfaf0fe5c6e24bd46005e95209316d8d5a9a Mon Sep 17 00:00:00 2001
From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Mon, 27 Nov 2017 13:38:16 -0800
Subject: [PATCH] Adding reset to the solver

---
 src/Backend/constraint.cc | 19 +++++++++++++
 src/Backend/constraint.h  |  1 +
 src/Backend/satencoder.cc |  5 ++++
 src/Backend/satencoder.h  |  1 +
 src/csolver.cc            | 60 ++++++++++++++++++++++++++++++++++++++-
 src/csolver.h             |  2 +-
 6 files changed, 86 insertions(+), 2 deletions(-)

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 356b415..8486282 100644
--- 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 1333b6c..0683230 100644
--- 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 2a58c06..206d2b7 100644
--- 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 08ec527..dcf3b86 100644
--- 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 e844e79..e4e0452 100644
--- 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 bac1a49..ffbfe35 100644
--- 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);
 
-- 
2.34.1