tabbing more tuners

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

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index b35b45602efb98e76f2739e5a9cdbd934e6bc06e..f92c223e528cca00163ffd4aaa5844269d30aa98 100644 (file)
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -192,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) {
@@ -573,7 +584,7 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
        }
 }
 
-void addClause(CNF *cnf, uint numliterals, int *literals){
+void addClause(CNF *cnf, uint numliterals, int *literals) {
        cnf->clausecount++;
        addArrayClauseLiteral(cnf->solver, numliterals, literals);
 }