}
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) {
}
}
-void addClause(CNF *cnf, uint numliterals, int *literals){
+void addClause(CNF *cnf, uint numliterals, int *literals) {
cnf->clausecount++;
- for(uint i=0; i< numliterals; i++)
- model_print("%d ", literals[i]);
- model_print("\n");
addArrayClauseLiteral(cnf->solver, numliterals, literals);
}
if (p == P_TRUE || p == P_BOTHTRUEFALSE) {
// proxy => expression
Edge cnfexpr = simplifyCNF(cnf, expression);
- Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
if (p == P_TRUE)
freeEdgeRec(expression);
outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
- outputCNFOR(cnf, cnfnegexpr, proxy);
freeEdgeCNF(cnfexpr);
- freeEdgeCNF(cnfnegexpr);
}
if (p == P_FALSE || p == P_BOTHTRUEFALSE) {
// expression => proxy
Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
- Edge cnfexpr = simplifyCNF(cnf, expression);
freeEdgeRec(expression);
outputCNFOR(cnf, cnfnegexpr, proxy);
- outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
freeEdgeCNF(cnfnegexpr);
- freeEdgeCNF(cnfexpr);
}
}