+Edge simplifyCNF(CNF *cnf, Edge input) {
+ if (edgeIsVarConst(input)) {
+ Node *newvec = allocResizeNode(1);
+ addEdgeToResizeNode(&newvec, input);
+ return (Edge) {newvec};
+ }
+ bool negated = isNegEdge(input);
+ Node * node = getNodePtrFromEdge(input);
+ NodeType type = node->type;
+ if (!negated) {
+ if (type == NodeType_AND) {
+ //AND case
+ Node *newvec = allocResizeNode(node->numEdges);
+ uint numEdges = node->numEdges;
+ for(uint i = 0; i < numEdges; i++) {
+ Edge e = simplifyCNF(cnf, node->edges[i]);
+ mergeFreeNodeToResizeNode(&newvec, e.node_ptr);
+ }
+ return (Edge) {newvec};
+ } else {
+ Edge cond = node->edges[0];
+ Edge thenedge = node->edges[1];
+ Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
+ Edge thenedges[] = {cond, constraintNegate(thenedge)};
+ Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges));
+ Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
+ Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges));
+ Edge thencnf = simplifyCNF(cnf, thencons);
+ Edge elsecnf = simplifyCNF(cnf, elsecons);
+ //free temporary nodes
+ ourfree(getNodePtrFromEdge(thencons));
+ ourfree(getNodePtrFromEdge(elsecons));
+ Node * result = thencnf.node_ptr;
+ mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr);
+ return (Edge) {result};
+ }
+ } else {
+ if (type == NodeType_AND) {
+ //OR Case
+ uint numEdges = node->numEdges;
+
+ for(uint i = 0; i < numEdges; i++) {
+ Edge e = node->edges[i];
+ bool enegate = isNegEdge(e);
+ if (!edgeIsVarConst(e)) {
+ Node * enode = getNodePtrFromEdge(e);
+ NodeType etype = enode->type;
+ if (enegate) {
+ if (etype == NodeType_AND) {
+ //OR of AND Case
+ uint eNumEdges = enode->numEdges;
+ Node * newnode = allocResizeNode(0);
+ Node * clause = allocBaseNode(NodeType_AND, numEdges);
+ memcpy(clause->edges, node->edges, sizeof(Edge) * i);
+ if ((i + 1) < numEdges) {
+ memcpy(&clause->edges[i+1], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
+ }
+
+ for(uint j = 0; j < eNumEdges; j++) {
+ clause->edges[i] = constraintNegate(enode->edges[j]);
+ Edge simplify = simplifyCNF(cnf, constraintNegate((Edge){clause}));
+ mergeFreeNodeToResizeNode(&newnode, simplify.node_ptr);
+ }
+ ourfree(clause);
+ return (Edge) {newnode};
+ } else {
+ //OR of IFF or ITE
+ Edge cond = enode->edges[0];
+ Edge thenedge = enode->edges[1];
+ Edge elseedge = (enode->type == NodeType_IFF) ? constraintNegate(thenedge) : enode->edges[2];
+ Edge thenedges[] = {cond, constraintNegate(thenedge)};
+ Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges));
+ Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
+ Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges));
+
+ //OR of AND Case
+ Node * newnode = allocResizeNode(0);
+ Node * clause = allocBaseNode(NodeType_AND, numEdges);
+ memcpy(clause->edges, node->edges, sizeof(Edge) * i);
+ if ((i + 1) < numEdges) {
+ memcpy(&clause->edges[i+1], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
+ }
+
+ clause->edges[i] = constraintNegate(thencons);
+ Edge simplify = simplifyCNF(cnf, constraintNegate((Edge){clause}));
+ mergeFreeNodeToResizeNode(&newnode, simplify.node_ptr);
+
+ clause->edges[i] = constraintNegate(elsecons);
+ simplify = simplifyCNF(cnf, constraintNegate((Edge){clause}));
+ mergeFreeNodeToResizeNode(&newnode, simplify.node_ptr);
+
+ //free temporary nodes
+ ourfree(getNodePtrFromEdge(thencons));
+ ourfree(getNodePtrFromEdge(elsecons));
+ ourfree(clause);
+ return (Edge) {newnode};
+ }
+ } else {
+ if (etype == NodeType_AND) {
+ //OR of OR Case
+ uint eNumEdges = enode->numEdges;
+ Node * clause = allocBaseNode(NodeType_AND, eNumEdges + numEdges - 1);
+ memcpy(clause->edges, node->edges, sizeof(Edge) * i);
+ if ((i + 1) < numEdges) {
+ memcpy(&clause->edges[i], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
+ }
+ memcpy(&clause->edges[numEdges-1], enode->edges, sizeof(Edge) * eNumEdges);
+ Edge eclause = {clause};
+ Edge result = simplifyCNF(cnf, constraintNegate(eclause));
+ ourfree(clause);
+ return result;
+ } else {
+ //OR of !(IFF or ITE)
+ Edge cond = node->edges[0];
+ Edge thenedge = node->edges[1];
+ Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
+ Edge thenedges[] = {cond, constraintNegate(thenedge)};
+ Edge thencons = createNode(NodeType_AND, 2, thenedges);
+ Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
+ Edge elsecons = createNode(NodeType_AND, 2, elseedges);
+
+
+ Node * clause = allocBaseNode(NodeType_AND, numEdges + 1);
+ memcpy(clause->edges, node->edges, sizeof(Edge) * i);
+ if ((i + 1) < numEdges) {
+ memcpy(&clause->edges[i], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
+ }
+ clause->edges[numEdges-1] = constraintNegate(thencons);
+ clause->edges[numEdges] = constraintNegate(elsecons);
+ Edge result = simplifyCNF(cnf, constraintNegate((Edge) {clause}));
+ //free temporary nodes
+ ourfree(getNodePtrFromEdge(thencons));
+ ourfree(getNodePtrFromEdge(elsecons));
+ ourfree(clause);
+ return result;
+ }
+ }
+ }
+ }
+
+ Node *newvec = allocResizeNode(numEdges);
+ for(uint i=0; i < numEdges; i++) {
+ addEdgeToResizeNode(&newvec, constraintNegate(node->edges[i]));
+ }
+ Node * result = allocResizeNode(1);
+ addEdgeToResizeNode(&result, (Edge){newvec});
+ return (Edge) {result};
+ } else {
+ Edge cond = node->edges[0];
+ Edge thenedge = node->edges[1];
+ Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
+
+
+ Edge thenedges[] = {cond, constraintNegate(thenedge)};
+ Edge thencons = createNode(NodeType_AND, 2, thenedges);
+ Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
+ Edge elsecons = createNode(NodeType_AND, 2, elseedges);
+
+ Edge combinededges[] = {constraintNegate(thencons), constraintNegate(elsecons)};
+ Edge combined = constraintNegate(createNode(NodeType_AND, 2, combinededges));
+ Edge result = simplifyCNF(cnf, combined);
+ //free temporary nodes
+ ourfree(getNodePtrFromEdge(thencons));
+ ourfree(getNodePtrFromEdge(elsecons));
+ ourfree(getNodePtrFromEdge(combined));
+ return result;
+ }
+ }
+}
+
+void outputCNF(CNF *cnf, Edge cnfform) {
+ Node * andNode = cnfform.node_ptr;
+ uint numEdges = andNode->numEdges;
+ for(uint i=0; i < numEdges; i++) {
+ Edge e = andNode->edges[i];
+ if (edgeIsVarConst(e)) {
+ int array[1] = {getEdgeVar(e)};
+ ASSERT(array[0] != 0);
+ addArrayClauseLiteral(cnf->solver, 1, array);
+ } else {
+ Node * clause = e.node_ptr;
+ uint cnumEdges = clause->numEdges;
+ if (cnumEdges > cnf->asize) {
+ cnf->asize = cnumEdges << 1;
+ ourfree(cnf->array);
+ cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
+ }
+ int * array = cnf->array;
+ for(uint j=0; j < cnumEdges; j++) {
+ array[j] = getEdgeVar(clause->edges[j]);
+ ASSERT(array[j] != 0);
+ }
+ addArrayClauseLiteral(cnf->solver, cnumEdges, array);
+ }
+ }
+}
+