6 CNF * cnf=ourmalloc(sizeof(CNF));
8 cnf->capacity=DEFAULT_CNF_ARRAY_SIZE;
9 cnf->mask=cnf->capacity-1;
10 cnf->node_array=ourcalloc(1, sizeof(Node *)*cnf->capacity);
12 cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
16 void deleteCNF(CNF * cnf) {
17 for(uint i=0;i<cnf->capacity;i++) {
18 Node *n=cnf->node_array[i];
22 ourfree(cnf->node_array);
26 void resizeCNF(CNF *cnf, uint newCapacity) {
27 Node **old_array=cnf->node_array;
28 Node **new_array=ourcalloc(1, sizeof(Node *)*newCapacity);
29 uint oldCapacity=cnf->capacity;
30 uint newMask=newCapacity-1;
31 for(uint i=0;i<oldCapacity;i++) {
33 uint hashCode=n->hashCode;
34 uint newindex=hashCode & newMask;
35 for(;;newindex=(newindex+1) & newMask) {
36 if (new_array[newindex] == NULL) {
37 new_array[newindex]=n;
43 cnf->node_array=new_array;
44 cnf->capacity=newCapacity;
45 cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
49 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashcode) {
50 Node *n=(Node *)ourmalloc(sizeof(Node)+sizeof(Edge)*numEdges);
51 memcpy(n->edges, edges, sizeof(Edge)*numEdges);
58 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge * edges) {
59 if (cnf->size > cnf->maxsize) {
60 resizeCNF(cnf, cnf->capacity << 1);
62 uint hashvalue=hashNode(type, numEdges, edges);
64 uint index=hashvalue & mask;
66 for(;;index=(index+1)&mask) {
67 n_ptr=&cnf->node_array[index];
69 if ((*n_ptr)->hashCode==hashvalue) {
70 if (compareNodes(*n_ptr, type, numEdges, edges)) {
79 *n_ptr=allocNode(type, numEdges, edges, hashvalue);
84 uint hashNode(NodeType type, uint numEdges, Edge * edges) {
85 uint hashvalue=type ^ numEdges;
86 for(uint i=0;i<numEdges;i++) {
87 hashvalue ^= (uint) edges[i].node_ptr;
88 hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
90 return (uint) hashvalue;
93 bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges) {
94 if (node->flags.type!=type || node->numEdges != numEdges)
96 Edge *nodeedges=node->edges;
97 for(uint i=0;i<numEdges;i++) {
98 if (nodeedges[i].node_ptr!=edges[i].node_ptr)
104 Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges) {
105 Edge edgearray[numEdges];
107 for(uint i=0; i<numEdges; i++) {
108 edgearray[i]=constraintNegate(edges[i]);
110 Edge eand=constraintAND(cnf, numEdges, edgearray);
111 return constraintNegate(eand);
114 Edge constraintOR2(CNF * cnf, Edge left, Edge right) {
115 Edge lneg=constraintNegate(left);
116 Edge rneg=constraintNegate(right);
117 Edge eand=constraintAND2(cnf, left, right);
118 return constraintNegate(eand);
121 int comparefunction(const Edge * e1, const Edge * e2) {
122 return ((uintptr_t)e1->node_ptr)-((uintptr_t)e2->node_ptr);
125 Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
126 qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *)) comparefunction);
128 while(initindex<numEdges && edges[initindex].node_ptr == E_True.node_ptr)
131 uint remainSize=numEdges-initindex;
135 else if (remainSize == 1)
136 return edges[initindex];
137 else if (edges[initindex].node_ptr==E_False.node_ptr)
140 /** De-duplicate array */
142 edges[lowindex++]=edges[initindex++];
144 for(;initindex<numEdges;initindex++) {
145 Edge e1=edges[lowindex];
146 Edge e2=edges[initindex];
147 if (sameNodeVarEdge(e1, e2)) {
148 if (!sameSignEdge(e1, e2)) {
152 edges[lowindex++]=edges[initindex];
157 if (enableMatching && lowindex==2 &&
158 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
159 getNodeType(edges[0]) == NodeType_AND &&
160 getNodeType(edges[1]) == NodeType_AND &&
161 getNodeSize(edges[0]) == 2 &&
162 getNodeSize(edges[1]) == 2) {
163 Edge * e0edges=getEdgeArray(edges[0]);
164 Edge * e1edges=getEdgeArray(edges[1]);
165 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
166 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
167 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
168 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
169 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
170 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
171 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
172 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
176 return createNode(cnf, NodeType_AND, numEdges, edges);
179 Edge constraintAND2(CNF * cnf, Edge left, Edge right) {
180 Edge edges[2]={left, right};
181 return constraintAND(cnf, 2, edges);
184 Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right) {
187 array[1]=constraintNegate(right);
188 Edge eand=constraintAND(cnf, 2, array);
189 return constraintNegate(eand);
192 Edge constraintIFF(CNF * cnf, Edge left, Edge right) {
194 if ((uintptr_t)left.node_ptr < (uintptr_t) right.node_ptr) {
201 return createNode(cnf, NodeType_IFF, 2, edges);
204 Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) {
205 Edge edges[]={cond, thenedge, elseedge};
206 return createNode(cnf, NodeType_ITE, 3, edges);
209 Edge constraintNewVar(CNF *cnf) {
210 uint varnum=cnf->varcount++;
211 Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };