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 (!equalsEdge(nodeedges[i], edges[i]))
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 && equalsEdge(edges[initindex], E_True))
131 uint remainSize=numEdges-initindex;
135 else if (remainSize == 1)
136 return edges[initindex];
137 else if (equalsEdge(edges[initindex], E_False))
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) {
193 bool negate=sameSignEdge(left, right);
194 Edge lpos=getNonNeg(left);
195 Edge rpos=getNonNeg(right);
198 if (equalsEdge(lpos, rpos)) {
200 } else if (ltEdge(lpos, rpos)) {
201 Edge edges[]={lpos, rpos};
202 e=(edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
204 Edge edges[]={rpos, lpos};
205 e=(edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
208 e=constraintNegate(e);
212 Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) {
213 if (isNegEdge(cond)) {
214 cond=constraintNegate(cond);
220 bool negate = isNegEdge(thenedge);
222 thenedge=constraintNegate(thenedge);
223 elseedge=constraintNegate(elseedge);
227 if (equalsEdge(cond, E_True)) {
229 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
230 result=constraintOR(cnf, 2, (Edge[]) {cond, elseedge});
231 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
232 result=constraintIMPLIES(cnf, cond, thenedge);
233 } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
234 result=constraintAND(cnf, 2, (Edge[]) {cond, thenedge});
235 } else if (equalsEdge(thenedge, elseedge)) {
237 } else if (sameNodeOppSign(thenedge, elseedge)) {
238 if (ltEdge(cond, thenedge)) {
239 result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {cond, thenedge});
241 result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {thenedge, cond});
244 Edge edges[]={cond, thenedge, elseedge};
245 result=createNode(cnf, NodeType_ITE, 3, edges);
248 result=constraintNegate(result);
252 Edge constraintNewVar(CNF *cnf) {
253 uint varnum=cnf->varcount++;
254 Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };