Adding a variable for counting the number of clauses

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 302206037ecb246c3bab10e7fe3bb4184b549972..b35b45602efb98e76f2739e5a9cdbd934e6bc06e 100644 (file)
--- 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 d7d2744ebd6bb1fa7fda827a1b8d90e132cf5939..18164f535afd4e659f52758d3dc9be98de5eba11 100644 (file)
--- 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);