5 VectorImpl(Edge, Edge, 16)
8 CNF * cnf=ourmalloc(sizeof(CNF));
10 cnf->capacity=DEFAULT_CNF_ARRAY_SIZE;
11 cnf->mask=cnf->capacity-1;
12 cnf->node_array=ourcalloc(1, sizeof(Node *)*cnf->capacity);
14 cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
15 cnf->enableMatching=true;
16 allocInlineDefVectorEdge(& cnf->constraints);
20 void deleteCNF(CNF * cnf) {
21 for(uint i=0;i<cnf->capacity;i++) {
22 Node *n=cnf->node_array[i];
26 deleteVectorArrayEdge(& cnf->constraints);
27 ourfree(cnf->node_array);
31 void resizeCNF(CNF *cnf, uint newCapacity) {
32 Node **old_array=cnf->node_array;
33 Node **new_array=ourcalloc(1, sizeof(Node *)*newCapacity);
34 uint oldCapacity=cnf->capacity;
35 uint newMask=newCapacity-1;
36 for(uint i=0;i<oldCapacity;i++) {
38 uint hashCode=n->hashCode;
39 uint newindex=hashCode & newMask;
40 for(;;newindex=(newindex+1) & newMask) {
41 if (new_array[newindex] == NULL) {
42 new_array[newindex]=n;
48 cnf->node_array=new_array;
49 cnf->capacity=newCapacity;
50 cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
54 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashcode) {
55 Node *n=(Node *)ourmalloc(sizeof(Node)+sizeof(Edge)*numEdges);
56 memcpy(n->edges, edges, sizeof(Edge)*numEdges);
58 n->flags.wasExpanded=0;
61 n->intAnnot[0]=0;n->intAnnot[1]=0;
62 n->ptrAnnot[0]=NULL;n->ptrAnnot[1]=NULL;
66 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge * edges) {
67 if (cnf->size > cnf->maxsize) {
68 resizeCNF(cnf, cnf->capacity << 1);
70 uint hashvalue=hashNode(type, numEdges, edges);
72 uint index=hashvalue & mask;
74 for(;;index=(index+1)&mask) {
75 n_ptr=&cnf->node_array[index];
77 if ((*n_ptr)->hashCode==hashvalue) {
78 if (compareNodes(*n_ptr, type, numEdges, edges)) {
87 *n_ptr=allocNode(type, numEdges, edges, hashvalue);
92 uint hashNode(NodeType type, uint numEdges, Edge * edges) {
93 uint hashvalue=type ^ numEdges;
94 for(uint i=0;i<numEdges;i++) {
95 hashvalue ^= (uint) edges[i].node_ptr;
96 hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
98 return (uint) hashvalue;
101 bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges) {
102 if (node->flags.type!=type || node->numEdges != numEdges)
104 Edge *nodeedges=node->edges;
105 for(uint i=0;i<numEdges;i++) {
106 if (!equalsEdge(nodeedges[i], edges[i]))
112 Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges) {
113 Edge edgearray[numEdges];
115 for(uint i=0; i<numEdges; i++) {
116 edgearray[i]=constraintNegate(edges[i]);
118 Edge eand=constraintAND(cnf, numEdges, edgearray);
119 return constraintNegate(eand);
122 Edge constraintOR2(CNF * cnf, Edge left, Edge right) {
123 Edge lneg=constraintNegate(left);
124 Edge rneg=constraintNegate(right);
125 Edge eand=constraintAND2(cnf, left, right);
126 return constraintNegate(eand);
129 int comparefunction(const Edge * e1, const Edge * e2) {
130 return ((uintptr_t)e1->node_ptr)-((uintptr_t)e2->node_ptr);
133 Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
134 qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *)) comparefunction);
136 while(initindex<numEdges && equalsEdge(edges[initindex], E_True))
139 uint remainSize=numEdges-initindex;
143 else if (remainSize == 1)
144 return edges[initindex];
145 else if (equalsEdge(edges[initindex], E_False))
148 /** De-duplicate array */
150 edges[lowindex++]=edges[initindex++];
152 for(;initindex<numEdges;initindex++) {
153 Edge e1=edges[lowindex];
154 Edge e2=edges[initindex];
155 if (sameNodeVarEdge(e1, e2)) {
156 if (!sameSignEdge(e1, e2)) {
160 edges[lowindex++]=edges[initindex];
165 if (cnf->enableMatching && lowindex==2 &&
166 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
167 getNodeType(edges[0]) == NodeType_AND &&
168 getNodeType(edges[1]) == NodeType_AND &&
169 getNodeSize(edges[0]) == 2 &&
170 getNodeSize(edges[1]) == 2) {
171 Edge * e0edges=getEdgeArray(edges[0]);
172 Edge * e1edges=getEdgeArray(edges[1]);
173 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
174 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
175 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
176 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
177 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
178 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
179 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
180 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
184 return createNode(cnf, NodeType_AND, numEdges, edges);
187 Edge constraintAND2(CNF * cnf, Edge left, Edge right) {
188 Edge edges[2]={left, right};
189 return constraintAND(cnf, 2, edges);
192 Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right) {
195 array[1]=constraintNegate(right);
196 Edge eand=constraintAND(cnf, 2, array);
197 return constraintNegate(eand);
200 Edge constraintIFF(CNF * cnf, Edge left, Edge right) {
201 bool negate=sameSignEdge(left, right);
202 Edge lpos=getNonNeg(left);
203 Edge rpos=getNonNeg(right);
206 if (equalsEdge(lpos, rpos)) {
208 } else if (ltEdge(lpos, rpos)) {
209 Edge edges[]={lpos, rpos};
210 e=(edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
212 Edge edges[]={rpos, lpos};
213 e=(edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
216 e=constraintNegate(e);
220 Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) {
221 if (isNegEdge(cond)) {
222 cond=constraintNegate(cond);
228 bool negate = isNegEdge(thenedge);
230 thenedge=constraintNegate(thenedge);
231 elseedge=constraintNegate(elseedge);
235 if (equalsEdge(cond, E_True)) {
237 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
238 result=constraintOR(cnf, 2, (Edge[]) {cond, elseedge});
239 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
240 result=constraintIMPLIES(cnf, cond, thenedge);
241 } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
242 result=constraintAND(cnf, 2, (Edge[]) {cond, thenedge});
243 } else if (equalsEdge(thenedge, elseedge)) {
245 } else if (sameNodeOppSign(thenedge, elseedge)) {
246 if (ltEdge(cond, thenedge)) {
247 result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {cond, thenedge});
249 result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {thenedge, cond});
252 Edge edges[]={cond, thenedge, elseedge};
253 result=createNode(cnf, NodeType_ITE, 3, edges);
256 result=constraintNegate(result);
260 void addConstraint(CNF *cnf, Edge constraint) {
261 pushVectorEdge(&cnf->constraints, constraint);
264 Edge constraintNewVar(CNF *cnf) {
265 uint varnum=cnf->varcount++;
266 Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
270 void countPass(CNF *cnf) {
271 uint numConstraints=getSizeVectorEdge(&cnf->constraints);
272 VectorEdge *ve=allocDefVectorEdge();
273 for(uint i=0; i<numConstraints;i++) {
274 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
276 deleteVectorEdge(ve);
279 void countConstraint(CNF *cnf, VectorEdge *stack, Edge e) {
280 //Skip constants and variables...
281 if (edgeIsVarConst(e))
284 clearVectorEdge(stack);pushVectorEdge(stack, e);
286 bool isMatching=cnf->enableMatching;
288 while(getSizeVectorEdge(stack) != 0) {
289 Edge e=lastVectorEdge(stack); popVectorEdge(stack);
290 bool polarity=isNegEdge(e);
291 Node *n=getNodePtrFromEdge(e);
292 if (getExpanded(n, polarity)) {
293 if (n->flags.type == NodeType_IFF ||
294 n->flags.type == NodeType_ITE) {
295 Edge pExp={n->ptrAnnot[polarity]};
296 getNodePtrFromEdge(pExp)->intAnnot[0]++;
298 n->intAnnot[polarity]++;
301 setExpanded(n, polarity); n->intAnnot[polarity]=1;
303 if (n->flags.type == NodeType_ITE||
304 n->flags.type == NodeType_IFF) {
305 n->intAnnot[polarity]=0;
306 Edge cond=n->edges[0];
307 Edge thenedge=n->edges[1];
308 Edge elseedge=n->flags.type == NodeType_IFF? constraintNegate(thenedge): n->edges[2];
309 thenedge=constraintNegateIf(thenedge, !polarity);
310 elseedge=constraintNegateIf(elseedge, !polarity);
311 thenedge=constraintAND2(cnf, cond, thenedge);
312 cond=constraintNegate(cond);
313 elseedge=constraintAND2(cnf, cond, elseedge);
314 thenedge=constraintNegate(thenedge);
315 elseedge=constraintNegate(elseedge);
316 cnf->enableMatching=false;
317 Edge succ1=constraintAND2(cnf, thenedge, elseedge);
318 n->ptrAnnot[polarity]=succ1.node_ptr;
319 cnf->enableMatching=isMatching;
320 pushVectorEdge(stack, succ1);
321 if (getExpanded(n, !polarity)) {
322 Edge succ2={(Node *)n->ptrAnnot[!polarity]};
323 Node *n1=getNodePtrFromEdge(succ1);
324 Node *n2=getNodePtrFromEdge(succ2);
325 n1->ptrAnnot[0]=succ2.node_ptr;
326 n2->ptrAnnot[0]=succ1.node_ptr;
327 n1->ptrAnnot[1]=succ2.node_ptr;
328 n2->ptrAnnot[1]=succ1.node_ptr;
331 for (uint i=0;i<n->numEdges;i++) {
332 Edge succ=n->edges[i];
333 succ=constraintNegateIf(succ, polarity);
334 if(!edgeIsVarConst(succ)) {
335 pushVectorEdge(stack, succ);