From 7c07450f8c8a3878de97508054a1399aa6d761f1 Mon Sep 17 00:00:00 2001
From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Thu, 13 Sep 2018 15:10:15 -0700
Subject: [PATCH] Adding a variable for counting the number of clauses

---
 src/Backend/constraint.cc | 16 ++++++++++++----
 src/Backend/constraint.h  |  3 ++-
 2 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 3022060..b35b456 100644
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -18,6 +18,7 @@ Edge E_NULL = {(Node *)NULL};
 CNF *createCNF() {
 	CNF *cnf = (CNF *) ourmalloc(sizeof(CNF));
 	cnf->varcount = 1;
+	cnf->clausecount = 0;
 	cnf->solver = allocIncrementalSolver();
 	cnf->solveTime = 0;
 	cnf->encodeTime = 0;
@@ -36,6 +37,7 @@ void deleteCNF(CNF *cnf) {
 void resetCNF(CNF *cnf) {
 	resetSolver(cnf->solver);
 	cnf->varcount = 1;
+	cnf->clausecount = 0;
 	cnf->solveTime = 0;
 	cnf->encodeTime = 0;
 	cnf->unsat = false;
@@ -571,6 +573,11 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
 	}
 }
 
+void addClause(CNF *cnf, uint numliterals, int *literals){
+	cnf->clausecount++;
+	addArrayClauseLiteral(cnf->solver, numliterals, literals);
+}
+
 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
 	Node *andNode = cnfform.node_ptr;
 	int orvar = getEdgeVar(eorvar);
@@ -581,7 +588,7 @@ void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
 		if (edgeIsVarConst(e)) {
 			int array[2] = {getEdgeVar(e), orvar};
 			ASSERT(array[0] != 0);
-			addArrayClauseLiteral(cnf->solver, 2, array);
+			addClause(cnf, 2, array);
 		} else {
 			Node *clause = e.node_ptr;
 			uint cnumEdges = clause->numEdges + 1;
@@ -596,7 +603,7 @@ void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
 				ASSERT(array[j] != 0);
 			}
 			array[cnumEdges - 1] = orvar;
-			addArrayClauseLiteral(cnf->solver, cnumEdges, array);
+			addClause(cnf, cnumEdges, array);
 		}
 	}
 }
@@ -609,7 +616,7 @@ void outputCNF(CNF *cnf, Edge cnfform) {
 		if (edgeIsVarConst(e)) {
 			int array[1] = {getEdgeVar(e)};
 			ASSERT(array[0] != 0);
-			addArrayClauseLiteral(cnf->solver, 1, array);
+			addClause(cnf, 1, array);
 		} else {
 			Node *clause = e.node_ptr;
 			uint cnumEdges = clause->numEdges;
@@ -623,7 +630,7 @@ void outputCNF(CNF *cnf, Edge cnfform) {
 				array[j] = getEdgeVar(clause->edges[j]);
 				ASSERT(array[j] != 0);
 			}
-			addArrayClauseLiteral(cnf->solver, cnumEdges, array);
+			addClause(cnf, cnumEdges, array);
 		}
 	}
 }
@@ -681,6 +688,7 @@ int solveCNF(CNF *cnf) {
 	long long startTime = getTimeNano();
 	finishedClauses(cnf->solver);
 	long long startSolve = getTimeNano();
+	model_print("#Clauses = %u\t#Vars = %u\n", cnf->clausecount, cnf->varcount);
 	int result = cnf->unsat ? IS_UNSAT : solve(cnf->solver);
 	long long finishTime = getTimeNano();
 	cnf->encodeTime = startSolve - startTime;
diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index d7d2744..18164f5 100644
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -46,6 +46,7 @@ typedef struct Node Node;
 
 struct CNF {
 	uint varcount;
+        uint clausecount;
 	uint asize;
 	IncrementalSolver *solver;
 	int *array;
@@ -180,7 +181,7 @@ void freeEdgeRec(Edge e);
 void outputCNF(CNF *cnf, Edge cnfform);
 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar);
 void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p);
-
+void addClause(CNF *cnf, uint numliterals, int *literals);
 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
-- 
2.34.1