Bug fix for long array

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

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
old mode 100644 (file)
new mode 100755 (executable)
index 3022060..d69e194
--- 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;
@@ -190,13 +192,24 @@ Edge createNode(NodeType type, uint numEdges, Edge *edges) {
 }
 
 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
-       Edge edgearray[numEdges];
+       if (numEdges < 200000) {
+               Edge edgearray[numEdges];
 
-       for (uint i = 0; i < numEdges; i++) {
-               edgearray[i] = constraintNegate(edges[i]);
+               for (uint i = 0; i < numEdges; i++) {
+                       edgearray[i] = constraintNegate(edges[i]);
+               }
+               Edge eand = constraintAND(cnf, numEdges, edgearray);
+               return constraintNegate(eand);
+       } else {
+               Edge * edgearray=(Edge *)ourmalloc(numEdges*sizeof(Edge));
+               
+               for (uint i = 0; i < numEdges; i++) {
+                       edgearray[i] = constraintNegate(edges[i]);
+               }
+               Edge eand = constraintAND(cnf, numEdges, edgearray);
+               ourfree(edgearray);
+               return constraintNegate(eand);
        }
-       Edge eand = constraintAND(cnf, numEdges, edgearray);
-       return constraintNegate(eand);
 }
 
 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
@@ -571,6 +584,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 +599,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 +614,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 +627,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 +641,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 +699,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;