1 /**CFile***********************************************************************
2
3 FileName [cuddDecomp.c]
4
5 PackageName [cudd]
6
7 Synopsis [Functions for BDD decomposition.]
8
9 Description [External procedures included in this file:
10 <ul>
11 <li> Cudd_bddApproxConjDecomp()
12 <li> Cudd_bddApproxDisjDecomp()
13 <li> Cudd_bddIterConjDecomp()
14 <li> Cudd_bddIterDisjDecomp()
15 <li> Cudd_bddGenConjDecomp()
16 <li> Cudd_bddGenDisjDecomp()
17 <li> Cudd_bddVarConjDecomp()
18 <li> Cudd_bddVarDisjDecomp()
19 </ul>
20 Static procedures included in this module:
21 <ul>
22 <li> cuddConjunctsAux()
23 <li> CreateBotDist()
24 <li> BuildConjuncts()
25 <li> ConjunctsFree()
26 </ul>]
27
28 Author [Kavita Ravi, Fabio Somenzi]
29
30 Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
31
32 All rights reserved.
33
34 Redistribution and use in source and binary forms, with or without
35 modification, are permitted provided that the following conditions
36 are met:
37
38 Redistributions of source code must retain the above copyright
39 notice, this list of conditions and the following disclaimer.
40
41 Redistributions in binary form must reproduce the above copyright
42 notice, this list of conditions and the following disclaimer in the
43 documentation and/or other materials provided with the distribution.
44
45 Neither the name of the University of Colorado nor the names of its
46 contributors may be used to endorse or promote products derived from
47 this software without specific prior written permission.
48
49 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
50 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
51 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
52 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
53 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
54 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
55 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
56 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
57 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
58 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
59 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
60 POSSIBILITY OF SUCH DAMAGE.]
61
62 ******************************************************************************/
63
64 #include "util.h"
65 #include "cuddInt.h"
66
67 /*---------------------------------------------------------------------------*/
68 /* Constant declarations */
69 /*---------------------------------------------------------------------------*/
70 #define DEPTH 5
71 #define THRESHOLD 10
72 #define NONE 0
73 #define PAIR_ST 1
74 #define PAIR_CR 2
75 #define G_ST 3
76 #define G_CR 4
77 #define H_ST 5
78 #define H_CR 6
79 #define BOTH_G 7
80 #define BOTH_H 8
81
82 /*---------------------------------------------------------------------------*/
83 /* Stucture declarations */
84 /*---------------------------------------------------------------------------*/
85
86 /*---------------------------------------------------------------------------*/
87 /* Type declarations */
88 /*---------------------------------------------------------------------------*/
89 typedef struct Conjuncts {
90 DdNode *g;
91 DdNode *h;
92 } Conjuncts;
93
94 typedef struct NodeStat {
95 int distance;
96 int localRef;
97 } NodeStat;
98
99
100 /*---------------------------------------------------------------------------*/
101 /* Variable declarations */
102 /*---------------------------------------------------------------------------*/
103
104 #ifndef lint
105 static char rcsid[] DD_UNUSED = "$Id: cuddDecomp.c,v 1.45 2012/02/05 01:07:18 fabio Exp $";
106 #endif
107
108 static DdNode *one, *zero;
109 long lastTimeG;
110
111 /*---------------------------------------------------------------------------*/
112 /* Macro declarations */
113 /*---------------------------------------------------------------------------*/
114
115
116 #define FactorsNotStored(factors) ((int)((long)(factors) & 01))
117
118 #define FactorsComplement(factors) ((Conjuncts *)((long)(factors) | 01))
119
120 #define FactorsUncomplement(factors) ((Conjuncts *)((long)(factors) ^ 01))
121
122 /**AutomaticStart*************************************************************/
123
124 /*---------------------------------------------------------------------------*/
125 /* Static function prototypes */
126 /*---------------------------------------------------------------------------*/
127
128 static NodeStat * CreateBotDist (DdNode * node, st_table * distanceTable);
129 static double CountMinterms (DdNode * node, double max, st_table * mintermTable, FILE *fp);
130 static void ConjunctsFree (DdManager * dd, Conjuncts * factors);
131 static int PairInTables (DdNode * g, DdNode * h, st_table * ghTable);
132 static Conjuncts * CheckTablesCacheAndReturn (DdNode * node, DdNode * g, DdNode * h, st_table * ghTable, st_table * cacheTable);
133 static Conjuncts * PickOnePair (DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable);
134 static Conjuncts * CheckInTables (DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable, int * outOfMem);
135 static Conjuncts * ZeroCase (DdManager * dd, DdNode * node, Conjuncts * factorsNv, st_table * ghTable, st_table * cacheTable, int switched);
136 static Conjuncts * BuildConjuncts (DdManager * dd, DdNode * node, st_table * distanceTable, st_table * cacheTable, int approxDistance, int maxLocalRef, st_table * ghTable, st_table * mintermTable);
137 static int cuddConjunctsAux (DdManager * dd, DdNode * f, DdNode ** c1, DdNode ** c2);
138
139 /**AutomaticEnd***************************************************************/
140
141
142 /*---------------------------------------------------------------------------*/
143 /* Definition of exported functions */
144 /*---------------------------------------------------------------------------*/
145
146
147 /**Function********************************************************************
148
149 Synopsis [Performs two-way conjunctive decomposition of a BDD.]
150
151 Description [Performs two-way conjunctive decomposition of a
152 BDD. This procedure owes its name to the use of supersetting to
153 obtain an initial factor of the given function. Returns the number
154 of conjuncts produced, that is, 2 if successful; 1 if no meaningful
155 decomposition was found; 0 otherwise. The conjuncts produced by this
156 procedure tend to be imbalanced.]
157
158 SideEffects [The factors are returned in an array as side effects.
159 The array is allocated by this function. It is the caller's responsibility
160 to free it. On successful completion, the conjuncts are already
161 referenced. If the function returns 0, the array for the conjuncts is
162 not allocated. If the function returns 1, the only factor equals the
163 function to be decomposed.]
164
165 SeeAlso [Cudd_bddApproxDisjDecomp Cudd_bddIterConjDecomp
166 Cudd_bddGenConjDecomp Cudd_bddVarConjDecomp Cudd_RemapOverApprox
167 Cudd_bddSqueeze Cudd_bddLICompaction]
168
169 ******************************************************************************/
170 int
Cudd_bddApproxConjDecomp(DdManager * dd,DdNode * f,DdNode *** conjuncts)171 Cudd_bddApproxConjDecomp(
172 DdManager * dd /* manager */,
173 DdNode * f /* function to be decomposed */,
174 DdNode *** conjuncts /* address of the first factor */)
175 {
176 DdNode *superset1, *superset2, *glocal, *hlocal;
177 int nvars = Cudd_SupportSize(dd,f);
178
179 /* Find a tentative first factor by overapproximation and minimization. */
180 superset1 = Cudd_RemapOverApprox(dd,f,nvars,0,1.0);
181 if (superset1 == NULL) return(0);
182 cuddRef(superset1);
183 superset2 = Cudd_bddSqueeze(dd,f,superset1);
184 if (superset2 == NULL) {
185 Cudd_RecursiveDeref(dd,superset1);
186 return(0);
187 }
188 cuddRef(superset2);
189 Cudd_RecursiveDeref(dd,superset1);
190
191 /* Compute the second factor by minimization. */
192 hlocal = Cudd_bddLICompaction(dd,f,superset2);
193 if (hlocal == NULL) {
194 Cudd_RecursiveDeref(dd,superset2);
195 return(0);
196 }
197 cuddRef(hlocal);
198
199 /* Refine the first factor by minimization. If h turns out to be f, this
200 ** step guarantees that g will be 1. */
201 glocal = Cudd_bddLICompaction(dd,superset2,hlocal);
202 if (glocal == NULL) {
203 Cudd_RecursiveDeref(dd,superset2);
204 Cudd_RecursiveDeref(dd,hlocal);
205 return(0);
206 }
207 cuddRef(glocal);
208 Cudd_RecursiveDeref(dd,superset2);
209
210 if (glocal != DD_ONE(dd)) {
211 if (hlocal != DD_ONE(dd)) {
212 *conjuncts = ALLOC(DdNode *,2);
213 if (*conjuncts == NULL) {
214 Cudd_RecursiveDeref(dd,glocal);
215 Cudd_RecursiveDeref(dd,hlocal);
216 dd->errorCode = CUDD_MEMORY_OUT;
217 return(0);
218 }
219 (*conjuncts)[0] = glocal;
220 (*conjuncts)[1] = hlocal;
221 return(2);
222 } else {
223 Cudd_RecursiveDeref(dd,hlocal);
224 *conjuncts = ALLOC(DdNode *,1);
225 if (*conjuncts == NULL) {
226 Cudd_RecursiveDeref(dd,glocal);
227 dd->errorCode = CUDD_MEMORY_OUT;
228 return(0);
229 }
230 (*conjuncts)[0] = glocal;
231 return(1);
232 }
233 } else {
234 Cudd_RecursiveDeref(dd,glocal);
235 *conjuncts = ALLOC(DdNode *,1);
236 if (*conjuncts == NULL) {
237 Cudd_RecursiveDeref(dd,hlocal);
238 dd->errorCode = CUDD_MEMORY_OUT;
239 return(0);
240 }
241 (*conjuncts)[0] = hlocal;
242 return(1);
243 }
244
245 } /* end of Cudd_bddApproxConjDecomp */
246
247
248 /**Function********************************************************************
249
250 Synopsis [Performs two-way disjunctive decomposition of a BDD.]
251
252 Description [Performs two-way disjunctive decomposition of a BDD.
253 Returns the number of disjuncts produced, that is, 2 if successful;
254 1 if no meaningful decomposition was found; 0 otherwise. The
255 disjuncts produced by this procedure tend to be imbalanced.]
256
257 SideEffects [The two disjuncts are returned in an array as side effects.
258 The array is allocated by this function. It is the caller's responsibility
259 to free it. On successful completion, the disjuncts are already
260 referenced. If the function returns 0, the array for the disjuncts is
261 not allocated. If the function returns 1, the only factor equals the
262 function to be decomposed.]
263
264 SeeAlso [Cudd_bddApproxConjDecomp Cudd_bddIterDisjDecomp
265 Cudd_bddGenDisjDecomp Cudd_bddVarDisjDecomp]
266
267 ******************************************************************************/
268 int
Cudd_bddApproxDisjDecomp(DdManager * dd,DdNode * f,DdNode *** disjuncts)269 Cudd_bddApproxDisjDecomp(
270 DdManager * dd /* manager */,
271 DdNode * f /* function to be decomposed */,
272 DdNode *** disjuncts /* address of the array of the disjuncts */)
273 {
274 int result, i;
275
276 result = Cudd_bddApproxConjDecomp(dd,Cudd_Not(f),disjuncts);
277 for (i = 0; i < result; i++) {
278 (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
279 }
280 return(result);
281
282 } /* end of Cudd_bddApproxDisjDecomp */
283
284
285 /**Function********************************************************************
286
287 Synopsis [Performs two-way conjunctive decomposition of a BDD.]
288
289 Description [Performs two-way conjunctive decomposition of a
290 BDD. This procedure owes its name to the iterated use of
291 supersetting to obtain a factor of the given function. Returns the
292 number of conjuncts produced, that is, 2 if successful; 1 if no
293 meaningful decomposition was found; 0 otherwise. The conjuncts
294 produced by this procedure tend to be imbalanced.]
295
296 SideEffects [The factors are returned in an array as side effects.
297 The array is allocated by this function. It is the caller's responsibility
298 to free it. On successful completion, the conjuncts are already
299 referenced. If the function returns 0, the array for the conjuncts is
300 not allocated. If the function returns 1, the only factor equals the
301 function to be decomposed.]
302
303 SeeAlso [Cudd_bddIterDisjDecomp Cudd_bddApproxConjDecomp
304 Cudd_bddGenConjDecomp Cudd_bddVarConjDecomp Cudd_RemapOverApprox
305 Cudd_bddSqueeze Cudd_bddLICompaction]
306
307 ******************************************************************************/
308 int
Cudd_bddIterConjDecomp(DdManager * dd,DdNode * f,DdNode *** conjuncts)309 Cudd_bddIterConjDecomp(
310 DdManager * dd /* manager */,
311 DdNode * f /* function to be decomposed */,
312 DdNode *** conjuncts /* address of the array of conjuncts */)
313 {
314 DdNode *superset1, *superset2, *old[2], *res[2];
315 int sizeOld, sizeNew;
316 int nvars = Cudd_SupportSize(dd,f);
317
318 old[0] = DD_ONE(dd);
319 cuddRef(old[0]);
320 old[1] = f;
321 cuddRef(old[1]);
322 sizeOld = Cudd_SharingSize(old,2);
323
324 do {
325 /* Find a tentative first factor by overapproximation and
326 ** minimization. */
327 superset1 = Cudd_RemapOverApprox(dd,old[1],nvars,0,1.0);
328 if (superset1 == NULL) {
329 Cudd_RecursiveDeref(dd,old[0]);
330 Cudd_RecursiveDeref(dd,old[1]);
331 return(0);
332 }
333 cuddRef(superset1);
334 superset2 = Cudd_bddSqueeze(dd,old[1],superset1);
335 if (superset2 == NULL) {
336 Cudd_RecursiveDeref(dd,old[0]);
337 Cudd_RecursiveDeref(dd,old[1]);
338 Cudd_RecursiveDeref(dd,superset1);
339 return(0);
340 }
341 cuddRef(superset2);
342 Cudd_RecursiveDeref(dd,superset1);
343 res[0] = Cudd_bddAnd(dd,old[0],superset2);
344 if (res[0] == NULL) {
345 Cudd_RecursiveDeref(dd,superset2);
346 Cudd_RecursiveDeref(dd,old[0]);
347 Cudd_RecursiveDeref(dd,old[1]);
348 return(0);
349 }
350 cuddRef(res[0]);
351 Cudd_RecursiveDeref(dd,superset2);
352 if (res[0] == old[0]) {
353 Cudd_RecursiveDeref(dd,res[0]);
354 break; /* avoid infinite loop */
355 }
356
357 /* Compute the second factor by minimization. */
358 res[1] = Cudd_bddLICompaction(dd,old[1],res[0]);
359 if (res[1] == NULL) {
360 Cudd_RecursiveDeref(dd,old[0]);
361 Cudd_RecursiveDeref(dd,old[1]);
362 return(0);
363 }
364 cuddRef(res[1]);
365
366 sizeNew = Cudd_SharingSize(res,2);
367 if (sizeNew <= sizeOld) {
368 Cudd_RecursiveDeref(dd,old[0]);
369 old[0] = res[0];
370 Cudd_RecursiveDeref(dd,old[1]);
371 old[1] = res[1];
372 sizeOld = sizeNew;
373 } else {
374 Cudd_RecursiveDeref(dd,res[0]);
375 Cudd_RecursiveDeref(dd,res[1]);
376 break;
377 }
378
379 } while (1);
380
381 /* Refine the first factor by minimization. If h turns out to
382 ** be f, this step guarantees that g will be 1. */
383 superset1 = Cudd_bddLICompaction(dd,old[0],old[1]);
384 if (superset1 == NULL) {
385 Cudd_RecursiveDeref(dd,old[0]);
386 Cudd_RecursiveDeref(dd,old[1]);
387 return(0);
388 }
389 cuddRef(superset1);
390 Cudd_RecursiveDeref(dd,old[0]);
391 old[0] = superset1;
392
393 if (old[0] != DD_ONE(dd)) {
394 if (old[1] != DD_ONE(dd)) {
395 *conjuncts = ALLOC(DdNode *,2);
396 if (*conjuncts == NULL) {
397 Cudd_RecursiveDeref(dd,old[0]);
398 Cudd_RecursiveDeref(dd,old[1]);
399 dd->errorCode = CUDD_MEMORY_OUT;
400 return(0);
401 }
402 (*conjuncts)[0] = old[0];
403 (*conjuncts)[1] = old[1];
404 return(2);
405 } else {
406 Cudd_RecursiveDeref(dd,old[1]);
407 *conjuncts = ALLOC(DdNode *,1);
408 if (*conjuncts == NULL) {
409 Cudd_RecursiveDeref(dd,old[0]);
410 dd->errorCode = CUDD_MEMORY_OUT;
411 return(0);
412 }
413 (*conjuncts)[0] = old[0];
414 return(1);
415 }
416 } else {
417 Cudd_RecursiveDeref(dd,old[0]);
418 *conjuncts = ALLOC(DdNode *,1);
419 if (*conjuncts == NULL) {
420 Cudd_RecursiveDeref(dd,old[1]);
421 dd->errorCode = CUDD_MEMORY_OUT;
422 return(0);
423 }
424 (*conjuncts)[0] = old[1];
425 return(1);
426 }
427
428 } /* end of Cudd_bddIterConjDecomp */
429
430
431 /**Function********************************************************************
432
433 Synopsis [Performs two-way disjunctive decomposition of a BDD.]
434
435 Description [Performs two-way disjunctive decomposition of a BDD.
436 Returns the number of disjuncts produced, that is, 2 if successful;
437 1 if no meaningful decomposition was found; 0 otherwise. The
438 disjuncts produced by this procedure tend to be imbalanced.]
439
440 SideEffects [The two disjuncts are returned in an array as side effects.
441 The array is allocated by this function. It is the caller's responsibility
442 to free it. On successful completion, the disjuncts are already
443 referenced. If the function returns 0, the array for the disjuncts is
444 not allocated. If the function returns 1, the only factor equals the
445 function to be decomposed.]
446
447 SeeAlso [Cudd_bddIterConjDecomp Cudd_bddApproxDisjDecomp
448 Cudd_bddGenDisjDecomp Cudd_bddVarDisjDecomp]
449
450 ******************************************************************************/
451 int
Cudd_bddIterDisjDecomp(DdManager * dd,DdNode * f,DdNode *** disjuncts)452 Cudd_bddIterDisjDecomp(
453 DdManager * dd /* manager */,
454 DdNode * f /* function to be decomposed */,
455 DdNode *** disjuncts /* address of the array of the disjuncts */)
456 {
457 int result, i;
458
459 result = Cudd_bddIterConjDecomp(dd,Cudd_Not(f),disjuncts);
460 for (i = 0; i < result; i++) {
461 (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
462 }
463 return(result);
464
465 } /* end of Cudd_bddIterDisjDecomp */
466
467
468 /**Function********************************************************************
469
470 Synopsis [Performs two-way conjunctive decomposition of a BDD.]
471
472 Description [Performs two-way conjunctive decomposition of a
473 BDD. This procedure owes its name to the fact tht it generalizes the
474 decomposition based on the cofactors with respect to one
475 variable. Returns the number of conjuncts produced, that is, 2 if
476 successful; 1 if no meaningful decomposition was found; 0
477 otherwise. The conjuncts produced by this procedure tend to be
478 balanced.]
479
480 SideEffects [The two factors are returned in an array as side effects.
481 The array is allocated by this function. It is the caller's responsibility
482 to free it. On successful completion, the conjuncts are already
483 referenced. If the function returns 0, the array for the conjuncts is
484 not allocated. If the function returns 1, the only factor equals the
485 function to be decomposed.]
486
487 SeeAlso [Cudd_bddGenDisjDecomp Cudd_bddApproxConjDecomp
488 Cudd_bddIterConjDecomp Cudd_bddVarConjDecomp]
489
490 ******************************************************************************/
491 int
Cudd_bddGenConjDecomp(DdManager * dd,DdNode * f,DdNode *** conjuncts)492 Cudd_bddGenConjDecomp(
493 DdManager * dd /* manager */,
494 DdNode * f /* function to be decomposed */,
495 DdNode *** conjuncts /* address of the array of conjuncts */)
496 {
497 int result;
498 DdNode *glocal, *hlocal;
499
500 one = DD_ONE(dd);
501 zero = Cudd_Not(one);
502
503 do {
504 dd->reordered = 0;
505 result = cuddConjunctsAux(dd, f, &glocal, &hlocal);
506 } while (dd->reordered == 1);
507
508 if (result == 0) {
509 return(0);
510 }
511
512 if (glocal != one) {
513 if (hlocal != one) {
514 *conjuncts = ALLOC(DdNode *,2);
515 if (*conjuncts == NULL) {
516 Cudd_RecursiveDeref(dd,glocal);
517 Cudd_RecursiveDeref(dd,hlocal);
518 dd->errorCode = CUDD_MEMORY_OUT;
519 return(0);
520 }
521 (*conjuncts)[0] = glocal;
522 (*conjuncts)[1] = hlocal;
523 return(2);
524 } else {
525 Cudd_RecursiveDeref(dd,hlocal);
526 *conjuncts = ALLOC(DdNode *,1);
527 if (*conjuncts == NULL) {
528 Cudd_RecursiveDeref(dd,glocal);
529 dd->errorCode = CUDD_MEMORY_OUT;
530 return(0);
531 }
532 (*conjuncts)[0] = glocal;
533 return(1);
534 }
535 } else {
536 Cudd_RecursiveDeref(dd,glocal);
537 *conjuncts = ALLOC(DdNode *,1);
538 if (*conjuncts == NULL) {
539 Cudd_RecursiveDeref(dd,hlocal);
540 dd->errorCode = CUDD_MEMORY_OUT;
541 return(0);
542 }
543 (*conjuncts)[0] = hlocal;
544 return(1);
545 }
546
547 } /* end of Cudd_bddGenConjDecomp */
548
549
550 /**Function********************************************************************
551
552 Synopsis [Performs two-way disjunctive decomposition of a BDD.]
553
554 Description [Performs two-way disjunctive decomposition of a BDD.
555 Returns the number of disjuncts produced, that is, 2 if successful;
556 1 if no meaningful decomposition was found; 0 otherwise. The
557 disjuncts produced by this procedure tend to be balanced.]
558
559 SideEffects [The two disjuncts are returned in an array as side effects.
560 The array is allocated by this function. It is the caller's responsibility
561 to free it. On successful completion, the disjuncts are already
562 referenced. If the function returns 0, the array for the disjuncts is
563 not allocated. If the function returns 1, the only factor equals the
564 function to be decomposed.]
565
566 SeeAlso [Cudd_bddGenConjDecomp Cudd_bddApproxDisjDecomp
567 Cudd_bddIterDisjDecomp Cudd_bddVarDisjDecomp]
568
569 ******************************************************************************/
570 int
Cudd_bddGenDisjDecomp(DdManager * dd,DdNode * f,DdNode *** disjuncts)571 Cudd_bddGenDisjDecomp(
572 DdManager * dd /* manager */,
573 DdNode * f /* function to be decomposed */,
574 DdNode *** disjuncts /* address of the array of the disjuncts */)
575 {
576 int result, i;
577
578 result = Cudd_bddGenConjDecomp(dd,Cudd_Not(f),disjuncts);
579 for (i = 0; i < result; i++) {
580 (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
581 }
582 return(result);
583
584 } /* end of Cudd_bddGenDisjDecomp */
585
586
587 /**Function********************************************************************
588
589 Synopsis [Performs two-way conjunctive decomposition of a BDD.]
590
591 Description [Conjunctively decomposes one BDD according to a
592 variable. If <code>f</code> is the function of the BDD and
593 <code>x</code> is the variable, the decomposition is
594 <code>(f+x)(f+x')</code>. The variable is chosen so as to balance
595 the sizes of the two conjuncts and to keep them small. Returns the
596 number of conjuncts produced, that is, 2 if successful; 1 if no
597 meaningful decomposition was found; 0 otherwise.]
598
599 SideEffects [The two factors are returned in an array as side effects.
600 The array is allocated by this function. It is the caller's responsibility
601 to free it. On successful completion, the conjuncts are already
602 referenced. If the function returns 0, the array for the conjuncts is
603 not allocated. If the function returns 1, the only factor equals the
604 function to be decomposed.]
605
606 SeeAlso [Cudd_bddVarDisjDecomp Cudd_bddGenConjDecomp
607 Cudd_bddApproxConjDecomp Cudd_bddIterConjDecomp]
608
609 *****************************************************************************/
610 int
Cudd_bddVarConjDecomp(DdManager * dd,DdNode * f,DdNode *** conjuncts)611 Cudd_bddVarConjDecomp(
612 DdManager * dd /* manager */,
613 DdNode * f /* function to be decomposed */,
614 DdNode *** conjuncts /* address of the array of conjuncts */)
615 {
616 int best;
617 int min;
618 DdNode *support, *scan, *var, *glocal, *hlocal;
619
620 /* Find best cofactoring variable. */
621 support = Cudd_Support(dd,f);
622 if (support == NULL) return(0);
623 if (Cudd_IsConstant(support)) {
624 *conjuncts = ALLOC(DdNode *,1);
625 if (*conjuncts == NULL) {
626 dd->errorCode = CUDD_MEMORY_OUT;
627 return(0);
628 }
629 (*conjuncts)[0] = f;
630 cuddRef((*conjuncts)[0]);
631 return(1);
632 }
633 cuddRef(support);
634 min = 1000000000;
635 best = -1;
636 scan = support;
637 while (!Cudd_IsConstant(scan)) {
638 int i = scan->index;
639 int est1 = Cudd_EstimateCofactor(dd,f,i,1);
640 int est0 = Cudd_EstimateCofactor(dd,f,i,0);
641 /* Minimize the size of the larger of the two cofactors. */
642 int est = (est1 > est0) ? est1 : est0;
643 if (est < min) {
644 min = est;
645 best = i;
646 }
647 scan = cuddT(scan);
648 }
649 #ifdef DD_DEBUG
650 assert(best >= 0 && best < dd->size);
651 #endif
652 Cudd_RecursiveDeref(dd,support);
653
654 var = Cudd_bddIthVar(dd,best);
655 glocal = Cudd_bddOr(dd,f,var);
656 if (glocal == NULL) {
657 return(0);
658 }
659 cuddRef(glocal);
660 hlocal = Cudd_bddOr(dd,f,Cudd_Not(var));
661 if (hlocal == NULL) {
662 Cudd_RecursiveDeref(dd,glocal);
663 return(0);
664 }
665 cuddRef(hlocal);
666
667 if (glocal != DD_ONE(dd)) {
668 if (hlocal != DD_ONE(dd)) {
669 *conjuncts = ALLOC(DdNode *,2);
670 if (*conjuncts == NULL) {
671 Cudd_RecursiveDeref(dd,glocal);
672 Cudd_RecursiveDeref(dd,hlocal);
673 dd->errorCode = CUDD_MEMORY_OUT;
674 return(0);
675 }
676 (*conjuncts)[0] = glocal;
677 (*conjuncts)[1] = hlocal;
678 return(2);
679 } else {
680 Cudd_RecursiveDeref(dd,hlocal);
681 *conjuncts = ALLOC(DdNode *,1);
682 if (*conjuncts == NULL) {
683 Cudd_RecursiveDeref(dd,glocal);
684 dd->errorCode = CUDD_MEMORY_OUT;
685 return(0);
686 }
687 (*conjuncts)[0] = glocal;
688 return(1);
689 }
690 } else {
691 Cudd_RecursiveDeref(dd,glocal);
692 *conjuncts = ALLOC(DdNode *,1);
693 if (*conjuncts == NULL) {
694 Cudd_RecursiveDeref(dd,hlocal);
695 dd->errorCode = CUDD_MEMORY_OUT;
696 return(0);
697 }
698 (*conjuncts)[0] = hlocal;
699 return(1);
700 }
701
702 } /* end of Cudd_bddVarConjDecomp */
703
704
705 /**Function********************************************************************
706
707 Synopsis [Performs two-way disjunctive decomposition of a BDD.]
708
709 Description [Performs two-way disjunctive decomposition of a BDD
710 according to a variable. If <code>f</code> is the function of the
711 BDD and <code>x</code> is the variable, the decomposition is
712 <code>f*x + f*x'</code>. The variable is chosen so as to balance
713 the sizes of the two disjuncts and to keep them small. Returns the
714 number of disjuncts produced, that is, 2 if successful; 1 if no
715 meaningful decomposition was found; 0 otherwise.]
716
717 SideEffects [The two disjuncts are returned in an array as side effects.
718 The array is allocated by this function. It is the caller's responsibility
719 to free it. On successful completion, the disjuncts are already
720 referenced. If the function returns 0, the array for the disjuncts is
721 not allocated. If the function returns 1, the only factor equals the
722 function to be decomposed.]
723
724 SeeAlso [Cudd_bddVarConjDecomp Cudd_bddApproxDisjDecomp
725 Cudd_bddIterDisjDecomp Cudd_bddGenDisjDecomp]
726
727 ******************************************************************************/
728 int
Cudd_bddVarDisjDecomp(DdManager * dd,DdNode * f,DdNode *** disjuncts)729 Cudd_bddVarDisjDecomp(
730 DdManager * dd /* manager */,
731 DdNode * f /* function to be decomposed */,
732 DdNode *** disjuncts /* address of the array of the disjuncts */)
733 {
734 int result, i;
735
736 result = Cudd_bddVarConjDecomp(dd,Cudd_Not(f),disjuncts);
737 for (i = 0; i < result; i++) {
738 (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
739 }
740 return(result);
741
742 } /* end of Cudd_bddVarDisjDecomp */
743
744
745 /*---------------------------------------------------------------------------*/
746 /* Definition of internal functions */
747 /*---------------------------------------------------------------------------*/
748
749 /*---------------------------------------------------------------------------*/
750 /* Definition of static functions */
751 /*---------------------------------------------------------------------------*/
752
753
754 /**Function********************************************************************
755
756 Synopsis [Get longest distance of node from constant.]
757
758 Description [Get longest distance of node from constant. Returns the
759 distance of the root from the constant if successful; CUDD_OUT_OF_MEM
760 otherwise.]
761
762 SideEffects [None]
763
764 SeeAlso []
765
766 ******************************************************************************/
767 static NodeStat *
CreateBotDist(DdNode * node,st_table * distanceTable)768 CreateBotDist(
769 DdNode * node,
770 st_table * distanceTable)
771 {
772 DdNode *N, *Nv, *Nnv;
773 int distance, distanceNv, distanceNnv;
774 NodeStat *nodeStat, *nodeStatNv, *nodeStatNnv;
775
776 #if 0
777 if (Cudd_IsConstant(node)) {
778 return(0);
779 }
780 #endif
781
782 /* Return the entry in the table if found. */
783 N = Cudd_Regular(node);
784 if (st_lookup(distanceTable, N, &nodeStat)) {
785 nodeStat->localRef++;
786 return(nodeStat);
787 }
788
789 Nv = cuddT(N);
790 Nnv = cuddE(N);
791 Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
792 Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
793
794 /* Recur on the children. */
795 nodeStatNv = CreateBotDist(Nv, distanceTable);
796 if (nodeStatNv == NULL) return(NULL);
797 distanceNv = nodeStatNv->distance;
798
799 nodeStatNnv = CreateBotDist(Nnv, distanceTable);
800 if (nodeStatNnv == NULL) return(NULL);
801 distanceNnv = nodeStatNnv->distance;
802 /* Store max distance from constant; note sometimes this distance
803 ** may be to 0.
804 */
805 distance = (distanceNv > distanceNnv) ? (distanceNv+1) : (distanceNnv + 1);
806
807 nodeStat = ALLOC(NodeStat, 1);
808 if (nodeStat == NULL) {
809 return(0);
810 }
811 nodeStat->distance = distance;
812 nodeStat->localRef = 1;
813
814 if (st_insert(distanceTable, (char *)N, (char *)nodeStat) ==
815 ST_OUT_OF_MEM) {
816 return(0);
817
818 }
819 return(nodeStat);
820
821 } /* end of CreateBotDist */
822
823
824 /**Function********************************************************************
825
826 Synopsis [Count the number of minterms of each node ina a BDD and
827 store it in a hash table.]
828
829 Description []
830
831 SideEffects [None]
832
833 SeeAlso []
834
835 ******************************************************************************/
836 static double
CountMinterms(DdNode * node,double max,st_table * mintermTable,FILE * fp)837 CountMinterms(
838 DdNode * node,
839 double max,
840 st_table * mintermTable,
841 FILE *fp)
842 {
843 DdNode *N, *Nv, *Nnv;
844 double min, minNv, minNnv;
845 double *dummy;
846
847 N = Cudd_Regular(node);
848
849 if (cuddIsConstant(N)) {
850 if (node == zero) {
851 return(0);
852 } else {
853 return(max);
854 }
855 }
856
857 /* Return the entry in the table if found. */
858 if (st_lookup(mintermTable, node, &dummy)) {
859 min = *dummy;
860 return(min);
861 }
862
863 Nv = cuddT(N);
864 Nnv = cuddE(N);
865 Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
866 Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
867
868 /* Recur on the children. */
869 minNv = CountMinterms(Nv, max, mintermTable, fp);
870 if (minNv == -1.0) return(-1.0);
871 minNnv = CountMinterms(Nnv, max, mintermTable, fp);
872 if (minNnv == -1.0) return(-1.0);
873 min = minNv / 2.0 + minNnv / 2.0;
874 /* store
875 */
876
877 dummy = ALLOC(double, 1);
878 if (dummy == NULL) return(-1.0);
879 *dummy = min;
880 if (st_insert(mintermTable, (char *)node, (char *)dummy) == ST_OUT_OF_MEM) {
881 (void) fprintf(fp, "st table insert failed\n");
882 }
883 return(min);
884
885 } /* end of CountMinterms */
886
887
888 /**Function********************************************************************
889
890 Synopsis [Free factors structure]
891
892 Description []
893
894 SideEffects [None]
895
896 SeeAlso []
897
898 ******************************************************************************/
899 static void
ConjunctsFree(DdManager * dd,Conjuncts * factors)900 ConjunctsFree(
901 DdManager * dd,
902 Conjuncts * factors)
903 {
904 Cudd_RecursiveDeref(dd, factors->g);
905 Cudd_RecursiveDeref(dd, factors->h);
906 FREE(factors);
907 return;
908
909 } /* end of ConjunctsFree */
910
911
912 /**Function********************************************************************
913
914 Synopsis [Check whether the given pair is in the tables.]
915
916 Description [.Check whether the given pair is in the tables. gTable
917 and hTable are combined.
918 absence in both is indicated by 0,
919 presence in gTable is indicated by 1,
920 presence in hTable by 2 and
921 presence in both by 3.
922 The values returned by this function are PAIR_ST,
923 PAIR_CR, G_ST, G_CR, H_ST, H_CR, BOTH_G, BOTH_H, NONE.
924 PAIR_ST implies g in gTable and h in hTable
925 PAIR_CR implies g in hTable and h in gTable
926 G_ST implies g in gTable and h not in any table
927 G_CR implies g in hTable and h not in any table
928 H_ST implies h in hTable and g not in any table
929 H_CR implies h in gTable and g not in any table
930 BOTH_G implies both in gTable
931 BOTH_H implies both in hTable
932 NONE implies none in table; ]
933
934 SideEffects []
935
936 SeeAlso [CheckTablesCacheAndReturn CheckInTables]
937
938 ******************************************************************************/
939 static int
PairInTables(DdNode * g,DdNode * h,st_table * ghTable)940 PairInTables(
941 DdNode * g,
942 DdNode * h,
943 st_table * ghTable)
944 {
945 int valueG, valueH, gPresent, hPresent;
946
947 valueG = valueH = gPresent = hPresent = 0;
948
949 gPresent = st_lookup_int(ghTable, (char *)Cudd_Regular(g), &valueG);
950 hPresent = st_lookup_int(ghTable, (char *)Cudd_Regular(h), &valueH);
951
952 if (!gPresent && !hPresent) return(NONE);
953
954 if (!hPresent) {
955 if (valueG & 1) return(G_ST);
956 if (valueG & 2) return(G_CR);
957 }
958 if (!gPresent) {
959 if (valueH & 1) return(H_CR);
960 if (valueH & 2) return(H_ST);
961 }
962 /* both in tables */
963 if ((valueG & 1) && (valueH & 2)) return(PAIR_ST);
964 if ((valueG & 2) && (valueH & 1)) return(PAIR_CR);
965
966 if (valueG & 1) {
967 return(BOTH_G);
968 } else {
969 return(BOTH_H);
970 }
971
972 } /* end of PairInTables */
973
974
975 /**Function********************************************************************
976
977 Synopsis [Check the tables for the existence of pair and return one
978 combination, cache the result.]
979
980 Description [Check the tables for the existence of pair and return
981 one combination, cache the result. The assumption is that one of the
982 conjuncts is already in the tables.]
983
984 SideEffects [g and h referenced for the cache]
985
986 SeeAlso [ZeroCase]
987
988 ******************************************************************************/
989 static Conjuncts *
CheckTablesCacheAndReturn(DdNode * node,DdNode * g,DdNode * h,st_table * ghTable,st_table * cacheTable)990 CheckTablesCacheAndReturn(
991 DdNode * node,
992 DdNode * g,
993 DdNode * h,
994 st_table * ghTable,
995 st_table * cacheTable)
996 {
997 int pairValue;
998 int value;
999 Conjuncts *factors;
1000
1001 value = 0;
1002 /* check tables */
1003 pairValue = PairInTables(g, h, ghTable);
1004 assert(pairValue != NONE);
1005 /* if both dont exist in table, we know one exists(either g or h).
1006 * Therefore store the other and proceed
1007 */
1008 factors = ALLOC(Conjuncts, 1);
1009 if (factors == NULL) return(NULL);
1010 if ((pairValue == BOTH_H) || (pairValue == H_ST)) {
1011 if (g != one) {
1012 value = 0;
1013 if (st_lookup_int(ghTable, (char *)Cudd_Regular(g), &value)) {
1014 value |= 1;
1015 } else {
1016 value = 1;
1017 }
1018 if (st_insert(ghTable, (char *)Cudd_Regular(g),
1019 (char *)(long)value) == ST_OUT_OF_MEM) {
1020 return(NULL);
1021 }
1022 }
1023 factors->g = g;
1024 factors->h = h;
1025 } else if ((pairValue == BOTH_G) || (pairValue == G_ST)) {
1026 if (h != one) {
1027 value = 0;
1028 if (st_lookup_int(ghTable, (char *)Cudd_Regular(h), &value)) {
1029 value |= 2;
1030 } else {
1031 value = 2;
1032 }
1033 if (st_insert(ghTable, (char *)Cudd_Regular(h),
1034 (char *)(long)value) == ST_OUT_OF_MEM) {
1035 return(NULL);
1036 }
1037 }
1038 factors->g = g;
1039 factors->h = h;
1040 } else if (pairValue == H_CR) {
1041 if (g != one) {
1042 value = 2;
1043 if (st_insert(ghTable, (char *)Cudd_Regular(g),
1044 (char *)(long)value) == ST_OUT_OF_MEM) {
1045 return(NULL);
1046 }
1047 }
1048 factors->g = h;
1049 factors->h = g;
1050 } else if (pairValue == G_CR) {
1051 if (h != one) {
1052 value = 1;
1053 if (st_insert(ghTable, (char *)Cudd_Regular(h),
1054 (char *)(long)value) == ST_OUT_OF_MEM) {
1055 return(NULL);
1056 }
1057 }
1058 factors->g = h;
1059 factors->h = g;
1060 } else if (pairValue == PAIR_CR) {
1061 /* pair exists in table */
1062 factors->g = h;
1063 factors->h = g;
1064 } else if (pairValue == PAIR_ST) {
1065 factors->g = g;
1066 factors->h = h;
1067 }
1068
1069 /* cache the result for this node */
1070 if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
1071 FREE(factors);
1072 return(NULL);
1073 }
1074
1075 return(factors);
1076
1077 } /* end of CheckTablesCacheAndReturn */
1078
1079 /**Function********************************************************************
1080
1081 Synopsis [Check the tables for the existence of pair and return one
1082 combination, store in cache.]
1083
1084 Description [Check the tables for the existence of pair and return
1085 one combination, store in cache. The pair that has more pointers to
1086 it is picked. An approximation of the number of local pointers is
1087 made by taking the reference count of the pairs sent. ]
1088
1089 SideEffects []
1090
1091 SeeAlso [ZeroCase BuildConjuncts]
1092
1093 ******************************************************************************/
1094 static Conjuncts *
PickOnePair(DdNode * node,DdNode * g1,DdNode * h1,DdNode * g2,DdNode * h2,st_table * ghTable,st_table * cacheTable)1095 PickOnePair(
1096 DdNode * node,
1097 DdNode * g1,
1098 DdNode * h1,
1099 DdNode * g2,
1100 DdNode * h2,
1101 st_table * ghTable,
1102 st_table * cacheTable)
1103 {
1104 int value;
1105 Conjuncts *factors;
1106 int oneRef, twoRef;
1107
1108 factors = ALLOC(Conjuncts, 1);
1109 if (factors == NULL) return(NULL);
1110
1111 /* count the number of pointers to pair 2 */
1112 if (h2 == one) {
1113 twoRef = (Cudd_Regular(g2))->ref;
1114 } else if (g2 == one) {
1115 twoRef = (Cudd_Regular(h2))->ref;
1116 } else {
1117 twoRef = ((Cudd_Regular(g2))->ref + (Cudd_Regular(h2))->ref)/2;
1118 }
1119
1120 /* count the number of pointers to pair 1 */
1121 if (h1 == one) {
1122 oneRef = (Cudd_Regular(g1))->ref;
1123 } else if (g1 == one) {
1124 oneRef = (Cudd_Regular(h1))->ref;
1125 } else {
1126 oneRef = ((Cudd_Regular(g1))->ref + (Cudd_Regular(h1))->ref)/2;
1127 }
1128
1129 /* pick the pair with higher reference count */
1130 if (oneRef >= twoRef) {
1131 factors->g = g1;
1132 factors->h = h1;
1133 } else {
1134 factors->g = g2;
1135 factors->h = h2;
1136 }
1137
1138 /*
1139 * Store computed factors in respective tables to encourage
1140 * recombination.
1141 */
1142 if (factors->g != one) {
1143 /* insert g in htable */
1144 value = 0;
1145 if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->g), &value)) {
1146 if (value == 2) {
1147 value |= 1;
1148 if (st_insert(ghTable, (char *)Cudd_Regular(factors->g),
1149 (char *)(long)value) == ST_OUT_OF_MEM) {
1150 FREE(factors);
1151 return(NULL);
1152 }
1153 }
1154 } else {
1155 value = 1;
1156 if (st_insert(ghTable, (char *)Cudd_Regular(factors->g),
1157 (char *)(long)value) == ST_OUT_OF_MEM) {
1158 FREE(factors);
1159 return(NULL);
1160 }
1161 }
1162 }
1163
1164 if (factors->h != one) {
1165 /* insert h in htable */
1166 value = 0;
1167 if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->h), &value)) {
1168 if (value == 1) {
1169 value |= 2;
1170 if (st_insert(ghTable, (char *)Cudd_Regular(factors->h),
1171 (char *)(long)value) == ST_OUT_OF_MEM) {
1172 FREE(factors);
1173 return(NULL);
1174 }
1175 }
1176 } else {
1177 value = 2;
1178 if (st_insert(ghTable, (char *)Cudd_Regular(factors->h),
1179 (char *)(long)value) == ST_OUT_OF_MEM) {
1180 FREE(factors);
1181 return(NULL);
1182 }
1183 }
1184 }
1185
1186 /* Store factors in cache table for later use. */
1187 if (st_insert(cacheTable, (char *)node, (char *)factors) ==
1188 ST_OUT_OF_MEM) {
1189 FREE(factors);
1190 return(NULL);
1191 }
1192
1193 return(factors);
1194
1195 } /* end of PickOnePair */
1196
1197
1198 /**Function********************************************************************
1199
1200 Synopsis [Check if the two pairs exist in the table, If any of the
1201 conjuncts do exist, store in the cache and return the corresponding pair.]
1202
1203 Description [Check if the two pairs exist in the table. If any of
1204 the conjuncts do exist, store in the cache and return the
1205 corresponding pair.]
1206
1207 SideEffects []
1208
1209 SeeAlso [ZeroCase BuildConjuncts]
1210
1211 ******************************************************************************/
1212 static Conjuncts *
CheckInTables(DdNode * node,DdNode * g1,DdNode * h1,DdNode * g2,DdNode * h2,st_table * ghTable,st_table * cacheTable,int * outOfMem)1213 CheckInTables(
1214 DdNode * node,
1215 DdNode * g1,
1216 DdNode * h1,
1217 DdNode * g2,
1218 DdNode * h2,
1219 st_table * ghTable,
1220 st_table * cacheTable,
1221 int * outOfMem)
1222 {
1223 int pairValue1, pairValue2;
1224 Conjuncts *factors;
1225 int value;
1226
1227 *outOfMem = 0;
1228
1229 /* check existence of pair in table */
1230 pairValue1 = PairInTables(g1, h1, ghTable);
1231 pairValue2 = PairInTables(g2, h2, ghTable);
1232
1233 /* if none of the 4 exist in the gh tables, return NULL */
1234 if ((pairValue1 == NONE) && (pairValue2 == NONE)) {
1235 return NULL;
1236 }
1237
1238 factors = ALLOC(Conjuncts, 1);
1239 if (factors == NULL) {
1240 *outOfMem = 1;
1241 return NULL;
1242 }
1243
1244 /* pairs that already exist in the table get preference. */
1245 if (pairValue1 == PAIR_ST) {
1246 factors->g = g1;
1247 factors->h = h1;
1248 } else if (pairValue2 == PAIR_ST) {
1249 factors->g = g2;
1250 factors->h = h2;
1251 } else if (pairValue1 == PAIR_CR) {
1252 factors->g = h1;
1253 factors->h = g1;
1254 } else if (pairValue2 == PAIR_CR) {
1255 factors->g = h2;
1256 factors->h = g2;
1257 } else if (pairValue1 == G_ST) {
1258 /* g exists in the table, h is not found in either table */
1259 factors->g = g1;
1260 factors->h = h1;
1261 if (h1 != one) {
1262 value = 2;
1263 if (st_insert(ghTable, (char *)Cudd_Regular(h1),
1264 (char *)(long)value) == ST_OUT_OF_MEM) {
1265 *outOfMem = 1;
1266 FREE(factors);
1267 return(NULL);
1268 }
1269 }
1270 } else if (pairValue1 == BOTH_G) {
1271 /* g and h are found in the g table */
1272 factors->g = g1;
1273 factors->h = h1;
1274 if (h1 != one) {
1275 value = 3;
1276 if (st_insert(ghTable, (char *)Cudd_Regular(h1),
1277 (char *)(long)value) == ST_OUT_OF_MEM) {
1278 *outOfMem = 1;
1279 FREE(factors);
1280 return(NULL);
1281 }
1282 }
1283 } else if (pairValue1 == H_ST) {
1284 /* h exists in the table, g is not found in either table */
1285 factors->g = g1;
1286 factors->h = h1;
1287 if (g1 != one) {
1288 value = 1;
1289 if (st_insert(ghTable, (char *)Cudd_Regular(g1),
1290 (char *)(long)value) == ST_OUT_OF_MEM) {
1291 *outOfMem = 1;
1292 FREE(factors);
1293 return(NULL);
1294 }
1295 }
1296 } else if (pairValue1 == BOTH_H) {
1297 /* g and h are found in the h table */
1298 factors->g = g1;
1299 factors->h = h1;
1300 if (g1 != one) {
1301 value = 3;
1302 if (st_insert(ghTable, (char *)Cudd_Regular(g1),
1303 (char *)(long)value) == ST_OUT_OF_MEM) {
1304 *outOfMem = 1;
1305 FREE(factors);
1306 return(NULL);
1307 }
1308 }
1309 } else if (pairValue2 == G_ST) {
1310 /* g exists in the table, h is not found in either table */
1311 factors->g = g2;
1312 factors->h = h2;
1313 if (h2 != one) {
1314 value = 2;
1315 if (st_insert(ghTable, (char *)Cudd_Regular(h2),
1316 (char *)(long)value) == ST_OUT_OF_MEM) {
1317 *outOfMem = 1;
1318 FREE(factors);
1319 return(NULL);
1320 }
1321 }
1322 } else if (pairValue2 == BOTH_G) {
1323 /* g and h are found in the g table */
1324 factors->g = g2;
1325 factors->h = h2;
1326 if (h2 != one) {
1327 value = 3;
1328 if (st_insert(ghTable, (char *)Cudd_Regular(h2),
1329 (char *)(long)value) == ST_OUT_OF_MEM) {
1330 *outOfMem = 1;
1331 FREE(factors);
1332 return(NULL);
1333 }
1334 }
1335 } else if (pairValue2 == H_ST) {
1336 /* h exists in the table, g is not found in either table */
1337 factors->g = g2;
1338 factors->h = h2;
1339 if (g2 != one) {
1340 value = 1;
1341 if (st_insert(ghTable, (char *)Cudd_Regular(g2),
1342 (char *)(long)value) == ST_OUT_OF_MEM) {
1343 *outOfMem = 1;
1344 FREE(factors);
1345 return(NULL);
1346 }
1347 }
1348 } else if (pairValue2 == BOTH_H) {
1349 /* g and h are found in the h table */
1350 factors->g = g2;
1351 factors->h = h2;
1352 if (g2 != one) {
1353 value = 3;
1354 if (st_insert(ghTable, (char *)Cudd_Regular(g2),
1355 (char *)(long)value) == ST_OUT_OF_MEM) {
1356 *outOfMem = 1;
1357 FREE(factors);
1358 return(NULL);
1359 }
1360 }
1361 } else if (pairValue1 == G_CR) {
1362 /* g found in h table and h in none */
1363 factors->g = h1;
1364 factors->h = g1;
1365 if (h1 != one) {
1366 value = 1;
1367 if (st_insert(ghTable, (char *)Cudd_Regular(h1),
1368 (char *)(long)value) == ST_OUT_OF_MEM) {
1369 *outOfMem = 1;
1370 FREE(factors);
1371 return(NULL);
1372 }
1373 }
1374 } else if (pairValue1 == H_CR) {
1375 /* h found in g table and g in none */
1376 factors->g = h1;
1377 factors->h = g1;
1378 if (g1 != one) {
1379 value = 2;
1380 if (st_insert(ghTable, (char *)Cudd_Regular(g1),
1381 (char *)(long)value) == ST_OUT_OF_MEM) {
1382 *outOfMem = 1;
1383 FREE(factors);
1384 return(NULL);
1385 }
1386 }
1387 } else if (pairValue2 == G_CR) {
1388 /* g found in h table and h in none */
1389 factors->g = h2;
1390 factors->h = g2;
1391 if (h2 != one) {
1392 value = 1;
1393 if (st_insert(ghTable, (char *)Cudd_Regular(h2),
1394 (char *)(long)value) == ST_OUT_OF_MEM) {
1395 *outOfMem = 1;
1396 FREE(factors);
1397 return(NULL);
1398 }
1399 }
1400 } else if (pairValue2 == H_CR) {
1401 /* h found in g table and g in none */
1402 factors->g = h2;
1403 factors->h = g2;
1404 if (g2 != one) {
1405 value = 2;
1406 if (st_insert(ghTable, (char *)Cudd_Regular(g2),
1407 (char *)(long)value) == ST_OUT_OF_MEM) {
1408 *outOfMem = 1;
1409 FREE(factors);
1410 return(NULL);
1411 }
1412 }
1413 }
1414
1415 /* Store factors in cache table for later use. */
1416 if (st_insert(cacheTable, (char *)node, (char *)factors) ==
1417 ST_OUT_OF_MEM) {
1418 *outOfMem = 1;
1419 FREE(factors);
1420 return(NULL);
1421 }
1422 return factors;
1423 } /* end of CheckInTables */
1424
1425
1426
1427 /**Function********************************************************************
1428
1429 Synopsis [If one child is zero, do explicitly what Restrict does or better]
1430
1431 Description [If one child is zero, do explicitly what Restrict does or better.
1432 First separate a variable and its child in the base case. In case of a cube
1433 times a function, separate the cube and function. As a last resort, look in
1434 tables.]
1435
1436 SideEffects [Frees the BDDs in factorsNv. factorsNv itself is not freed
1437 because it is freed above.]
1438
1439 SeeAlso [BuildConjuncts]
1440
1441 ******************************************************************************/
1442 static Conjuncts *
ZeroCase(DdManager * dd,DdNode * node,Conjuncts * factorsNv,st_table * ghTable,st_table * cacheTable,int switched)1443 ZeroCase(
1444 DdManager * dd,
1445 DdNode * node,
1446 Conjuncts * factorsNv,
1447 st_table * ghTable,
1448 st_table * cacheTable,
1449 int switched)
1450 {
1451 int topid;
1452 DdNode *g, *h, *g1, *g2, *h1, *h2, *x, *N, *G, *H, *Gv, *Gnv;
1453 DdNode *Hv, *Hnv;
1454 int value;
1455 int outOfMem;
1456 Conjuncts *factors;
1457
1458 /* get var at this node */
1459 N = Cudd_Regular(node);
1460 topid = N->index;
1461 x = dd->vars[topid];
1462 x = (switched) ? Cudd_Not(x): x;
1463 cuddRef(x);
1464
1465 /* Seprate variable and child */
1466 if (factorsNv->g == one) {
1467 Cudd_RecursiveDeref(dd, factorsNv->g);
1468 factors = ALLOC(Conjuncts, 1);
1469 if (factors == NULL) {
1470 dd->errorCode = CUDD_MEMORY_OUT;
1471 Cudd_RecursiveDeref(dd, factorsNv->h);
1472 Cudd_RecursiveDeref(dd, x);
1473 return(NULL);
1474 }
1475 factors->g = x;
1476 factors->h = factorsNv->h;
1477 /* cache the result*/
1478 if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
1479 dd->errorCode = CUDD_MEMORY_OUT;
1480 Cudd_RecursiveDeref(dd, factorsNv->h);
1481 Cudd_RecursiveDeref(dd, x);
1482 FREE(factors);
1483 return NULL;
1484 }
1485
1486 /* store x in g table, the other node is already in the table */
1487 if (st_lookup_int(ghTable, (char *)Cudd_Regular(x), &value)) {
1488 value |= 1;
1489 } else {
1490 value = 1;
1491 }
1492 if (st_insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == ST_OUT_OF_MEM) {
1493 dd->errorCode = CUDD_MEMORY_OUT;
1494 return NULL;
1495 }
1496 return(factors);
1497 }
1498
1499 /* Seprate variable and child */
1500 if (factorsNv->h == one) {
1501 Cudd_RecursiveDeref(dd, factorsNv->h);
1502 factors = ALLOC(Conjuncts, 1);
1503 if (factors == NULL) {
1504 dd->errorCode = CUDD_MEMORY_OUT;
1505 Cudd_RecursiveDeref(dd, factorsNv->g);
1506 Cudd_RecursiveDeref(dd, x);
1507 return(NULL);
1508 }
1509 factors->g = factorsNv->g;
1510 factors->h = x;
1511 /* cache the result. */
1512 if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
1513 dd->errorCode = CUDD_MEMORY_OUT;
1514 Cudd_RecursiveDeref(dd, factorsNv->g);
1515 Cudd_RecursiveDeref(dd, x);
1516 FREE(factors);
1517 return(NULL);
1518 }
1519 /* store x in h table, the other node is already in the table */
1520 if (st_lookup_int(ghTable, (char *)Cudd_Regular(x), &value)) {
1521 value |= 2;
1522 } else {
1523 value = 2;
1524 }
1525 if (st_insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == ST_OUT_OF_MEM) {
1526 dd->errorCode = CUDD_MEMORY_OUT;
1527 return NULL;
1528 }
1529 return(factors);
1530 }
1531
1532 G = Cudd_Regular(factorsNv->g);
1533 Gv = cuddT(G);
1534 Gnv = cuddE(G);
1535 Gv = Cudd_NotCond(Gv, Cudd_IsComplement(node));
1536 Gnv = Cudd_NotCond(Gnv, Cudd_IsComplement(node));
1537 /* if the child below is a variable */
1538 if ((Gv == zero) || (Gnv == zero)) {
1539 h = factorsNv->h;
1540 g = cuddBddAndRecur(dd, x, factorsNv->g);
1541 if (g != NULL) cuddRef(g);
1542 Cudd_RecursiveDeref(dd, factorsNv->g);
1543 Cudd_RecursiveDeref(dd, x);
1544 if (g == NULL) {
1545 Cudd_RecursiveDeref(dd, factorsNv->h);
1546 return NULL;
1547 }
1548 /* CheckTablesCacheAndReturn responsible for allocating
1549 * factors structure., g,h referenced for cache store the
1550 */
1551 factors = CheckTablesCacheAndReturn(node,
1552 g,
1553 h,
1554 ghTable,
1555 cacheTable);
1556 if (factors == NULL) {
1557 dd->errorCode = CUDD_MEMORY_OUT;
1558 Cudd_RecursiveDeref(dd, g);
1559 Cudd_RecursiveDeref(dd, h);
1560 }
1561 return(factors);
1562 }
1563
1564 H = Cudd_Regular(factorsNv->h);
1565 Hv = cuddT(H);
1566 Hnv = cuddE(H);
1567 Hv = Cudd_NotCond(Hv, Cudd_IsComplement(node));
1568 Hnv = Cudd_NotCond(Hnv, Cudd_IsComplement(node));
1569 /* if the child below is a variable */
1570 if ((Hv == zero) || (Hnv == zero)) {
1571 g = factorsNv->g;
1572 h = cuddBddAndRecur(dd, x, factorsNv->h);
1573 if (h!= NULL) cuddRef(h);
1574 Cudd_RecursiveDeref(dd, factorsNv->h);
1575 Cudd_RecursiveDeref(dd, x);
1576 if (h == NULL) {
1577 Cudd_RecursiveDeref(dd, factorsNv->g);
1578 return NULL;
1579 }
1580 /* CheckTablesCacheAndReturn responsible for allocating
1581 * factors structure.g,h referenced for table store
1582 */
1583 factors = CheckTablesCacheAndReturn(node,
1584 g,
1585 h,
1586 ghTable,
1587 cacheTable);
1588 if (factors == NULL) {
1589 dd->errorCode = CUDD_MEMORY_OUT;
1590 Cudd_RecursiveDeref(dd, g);
1591 Cudd_RecursiveDeref(dd, h);
1592 }
1593 return(factors);
1594 }
1595
1596 /* build g1 = x*g; h1 = h */
1597 /* build g2 = g; h2 = x*h */
1598 Cudd_RecursiveDeref(dd, x);
1599 h1 = factorsNv->h;
1600 g1 = cuddBddAndRecur(dd, x, factorsNv->g);
1601 if (g1 != NULL) cuddRef(g1);
1602 if (g1 == NULL) {
1603 Cudd_RecursiveDeref(dd, factorsNv->g);
1604 Cudd_RecursiveDeref(dd, factorsNv->h);
1605 return NULL;
1606 }
1607
1608 g2 = factorsNv->g;
1609 h2 = cuddBddAndRecur(dd, x, factorsNv->h);
1610 if (h2 != NULL) cuddRef(h2);
1611 if (h2 == NULL) {
1612 Cudd_RecursiveDeref(dd, factorsNv->h);
1613 Cudd_RecursiveDeref(dd, factorsNv->g);
1614 return NULL;
1615 }
1616
1617 /* check whether any pair is in tables */
1618 factors = CheckInTables(node, g1, h1, g2, h2, ghTable, cacheTable, &outOfMem);
1619 if (outOfMem) {
1620 dd->errorCode = CUDD_MEMORY_OUT;
1621 Cudd_RecursiveDeref(dd, g1);
1622 Cudd_RecursiveDeref(dd, h1);
1623 Cudd_RecursiveDeref(dd, g2);
1624 Cudd_RecursiveDeref(dd, h2);
1625 return NULL;
1626 }
1627 if (factors != NULL) {
1628 if ((factors->g == g1) || (factors->g == h1)) {
1629 Cudd_RecursiveDeref(dd, g2);
1630 Cudd_RecursiveDeref(dd, h2);
1631 } else {
1632 Cudd_RecursiveDeref(dd, g1);
1633 Cudd_RecursiveDeref(dd, h1);
1634 }
1635 return factors;
1636 }
1637
1638 /* check for each pair in tables and choose one */
1639 factors = PickOnePair(node,g1, h1, g2, h2, ghTable, cacheTable);
1640 if (factors == NULL) {
1641 dd->errorCode = CUDD_MEMORY_OUT;
1642 Cudd_RecursiveDeref(dd, g1);
1643 Cudd_RecursiveDeref(dd, h1);
1644 Cudd_RecursiveDeref(dd, g2);
1645 Cudd_RecursiveDeref(dd, h2);
1646 } else {
1647 /* now free what was created and not used */
1648 if ((factors->g == g1) || (factors->g == h1)) {
1649 Cudd_RecursiveDeref(dd, g2);
1650 Cudd_RecursiveDeref(dd, h2);
1651 } else {
1652 Cudd_RecursiveDeref(dd, g1);
1653 Cudd_RecursiveDeref(dd, h1);
1654 }
1655 }
1656
1657 return(factors);
1658 } /* end of ZeroCase */
1659
1660
1661 /**Function********************************************************************
1662
1663 Synopsis [Builds the conjuncts recursively, bottom up.]
1664
1665 Description [Builds the conjuncts recursively, bottom up. Constants
1666 are returned as (f, f). The cache is checked for previously computed
1667 result. The decomposition points are determined by the local
1668 reference count of this node and the longest distance from the
1669 constant. At the decomposition point, the factors returned are (f,
1670 1). Recur on the two children. The order is determined by the
1671 heavier branch. Combine the factors of the two children and pick the
1672 one that already occurs in the gh table. Occurence in g is indicated
1673 by value 1, occurence in h by 2, occurence in both 3.]
1674
1675 SideEffects []
1676
1677 SeeAlso [cuddConjunctsAux]
1678
1679 ******************************************************************************/
1680 static Conjuncts *
BuildConjuncts(DdManager * dd,DdNode * node,st_table * distanceTable,st_table * cacheTable,int approxDistance,int maxLocalRef,st_table * ghTable,st_table * mintermTable)1681 BuildConjuncts(
1682 DdManager * dd,
1683 DdNode * node,
1684 st_table * distanceTable,
1685 st_table * cacheTable,
1686 int approxDistance,
1687 int maxLocalRef,
1688 st_table * ghTable,
1689 st_table * mintermTable)
1690 {
1691 int topid, distance;
1692 Conjuncts *factorsNv, *factorsNnv, *factors;
1693 Conjuncts *dummy;
1694 DdNode *N, *Nv, *Nnv, *temp, *g1, *g2, *h1, *h2, *topv;
1695 double minNv = 0.0, minNnv = 0.0;
1696 double *doubleDummy;
1697 int switched =0;
1698 int outOfMem;
1699 int freeNv = 0, freeNnv = 0, freeTemp;
1700 NodeStat *nodeStat;
1701 int value;
1702
1703 /* if f is constant, return (f,f) */
1704 if (Cudd_IsConstant(node)) {
1705 factors = ALLOC(Conjuncts, 1);
1706 if (factors == NULL) {
1707 dd->errorCode = CUDD_MEMORY_OUT;
1708 return(NULL);
1709 }
1710 factors->g = node;
1711 factors->h = node;
1712 return(FactorsComplement(factors));
1713 }
1714
1715 /* If result (a pair of conjuncts) in cache, return the factors. */
1716 if (st_lookup(cacheTable, node, &dummy)) {
1717 factors = dummy;
1718 return(factors);
1719 }
1720
1721 /* check distance and local reference count of this node */
1722 N = Cudd_Regular(node);
1723 if (!st_lookup(distanceTable, N, &nodeStat)) {
1724 (void) fprintf(dd->err, "Not in table, Something wrong\n");
1725 dd->errorCode = CUDD_INTERNAL_ERROR;
1726 return(NULL);
1727 }
1728 distance = nodeStat->distance;
1729
1730 /* at or below decomposition point, return (f, 1) */
1731 if (((nodeStat->localRef > maxLocalRef*2/3) &&
1732 (distance < approxDistance*2/3)) ||
1733 (distance <= approxDistance/4)) {
1734 factors = ALLOC(Conjuncts, 1);
1735 if (factors == NULL) {
1736 dd->errorCode = CUDD_MEMORY_OUT;
1737 return(NULL);
1738 }
1739 /* alternate assigning (f,1) */
1740 value = 0;
1741 if (st_lookup_int(ghTable, (char *)Cudd_Regular(node), &value)) {
1742 if (value == 3) {
1743 if (!lastTimeG) {
1744 factors->g = node;
1745 factors->h = one;
1746 lastTimeG = 1;
1747 } else {
1748 factors->g = one;
1749 factors->h = node;
1750 lastTimeG = 0;
1751 }
1752 } else if (value == 1) {
1753 factors->g = node;
1754 factors->h = one;
1755 } else {
1756 factors->g = one;
1757 factors->h = node;
1758 }
1759 } else if (!lastTimeG) {
1760 factors->g = node;
1761 factors->h = one;
1762 lastTimeG = 1;
1763 value = 1;
1764 if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) {
1765 dd->errorCode = CUDD_MEMORY_OUT;
1766 FREE(factors);
1767 return NULL;
1768 }
1769 } else {
1770 factors->g = one;
1771 factors->h = node;
1772 lastTimeG = 0;
1773 value = 2;
1774 if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) {
1775 dd->errorCode = CUDD_MEMORY_OUT;
1776 FREE(factors);
1777 return NULL;
1778 }
1779 }
1780 return(FactorsComplement(factors));
1781 }
1782
1783 /* get the children and recur */
1784 Nv = cuddT(N);
1785 Nnv = cuddE(N);
1786 Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
1787 Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
1788
1789 /* Choose which subproblem to solve first based on the number of
1790 * minterms. We go first where there are more minterms.
1791 */
1792 if (!Cudd_IsConstant(Nv)) {
1793 if (!st_lookup(mintermTable, Nv, &doubleDummy)) {
1794 (void) fprintf(dd->err, "Not in table: Something wrong\n");
1795 dd->errorCode = CUDD_INTERNAL_ERROR;
1796 return(NULL);
1797 }
1798 minNv = *doubleDummy;
1799 }
1800
1801 if (!Cudd_IsConstant(Nnv)) {
1802 if (!st_lookup(mintermTable, Nnv, &doubleDummy)) {
1803 (void) fprintf(dd->err, "Not in table: Something wrong\n");
1804 dd->errorCode = CUDD_INTERNAL_ERROR;
1805 return(NULL);
1806 }
1807 minNnv = *doubleDummy;
1808 }
1809
1810 if (minNv < minNnv) {
1811 temp = Nv;
1812 Nv = Nnv;
1813 Nnv = temp;
1814 switched = 1;
1815 }
1816
1817 /* build gt, ht recursively */
1818 if (Nv != zero) {
1819 factorsNv = BuildConjuncts(dd, Nv, distanceTable,
1820 cacheTable, approxDistance, maxLocalRef,
1821 ghTable, mintermTable);
1822 if (factorsNv == NULL) return(NULL);
1823 freeNv = FactorsNotStored(factorsNv);
1824 factorsNv = (freeNv) ? FactorsUncomplement(factorsNv) : factorsNv;
1825 cuddRef(factorsNv->g);
1826 cuddRef(factorsNv->h);
1827
1828 /* Deal with the zero case */
1829 if (Nnv == zero) {
1830 /* is responsible for freeing factorsNv */
1831 factors = ZeroCase(dd, node, factorsNv, ghTable,
1832 cacheTable, switched);
1833 if (freeNv) FREE(factorsNv);
1834 return(factors);
1835 }
1836 }
1837
1838 /* build ge, he recursively */
1839 if (Nnv != zero) {
1840 factorsNnv = BuildConjuncts(dd, Nnv, distanceTable,
1841 cacheTable, approxDistance, maxLocalRef,
1842 ghTable, mintermTable);
1843 if (factorsNnv == NULL) {
1844 Cudd_RecursiveDeref(dd, factorsNv->g);
1845 Cudd_RecursiveDeref(dd, factorsNv->h);
1846 if (freeNv) FREE(factorsNv);
1847 return(NULL);
1848 }
1849 freeNnv = FactorsNotStored(factorsNnv);
1850 factorsNnv = (freeNnv) ? FactorsUncomplement(factorsNnv) : factorsNnv;
1851 cuddRef(factorsNnv->g);
1852 cuddRef(factorsNnv->h);
1853
1854 /* Deal with the zero case */
1855 if (Nv == zero) {
1856 /* is responsible for freeing factorsNv */
1857 factors = ZeroCase(dd, node, factorsNnv, ghTable,
1858 cacheTable, switched);
1859 if (freeNnv) FREE(factorsNnv);
1860 return(factors);
1861 }
1862 }
1863
1864 /* construct the 2 pairs */
1865 /* g1 = x*gt + x'*ge; h1 = x*ht + x'*he; */
1866 /* g2 = x*gt + x'*he; h2 = x*ht + x'*ge */
1867 if (switched) {
1868 factors = factorsNnv;
1869 factorsNnv = factorsNv;
1870 factorsNv = factors;
1871 freeTemp = freeNv;
1872 freeNv = freeNnv;
1873 freeNnv = freeTemp;
1874 }
1875
1876 /* Build the factors for this node. */
1877 topid = N->index;
1878 topv = dd->vars[topid];
1879
1880 g1 = cuddBddIteRecur(dd, topv, factorsNv->g, factorsNnv->g);
1881 if (g1 == NULL) {
1882 Cudd_RecursiveDeref(dd, factorsNv->g);
1883 Cudd_RecursiveDeref(dd, factorsNv->h);
1884 Cudd_RecursiveDeref(dd, factorsNnv->g);
1885 Cudd_RecursiveDeref(dd, factorsNnv->h);
1886 if (freeNv) FREE(factorsNv);
1887 if (freeNnv) FREE(factorsNnv);
1888 return(NULL);
1889 }
1890
1891 cuddRef(g1);
1892
1893 h1 = cuddBddIteRecur(dd, topv, factorsNv->h, factorsNnv->h);
1894 if (h1 == NULL) {
1895 Cudd_RecursiveDeref(dd, factorsNv->g);
1896 Cudd_RecursiveDeref(dd, factorsNv->h);
1897 Cudd_RecursiveDeref(dd, factorsNnv->g);
1898 Cudd_RecursiveDeref(dd, factorsNnv->h);
1899 Cudd_RecursiveDeref(dd, g1);
1900 if (freeNv) FREE(factorsNv);
1901 if (freeNnv) FREE(factorsNnv);
1902 return(NULL);
1903 }
1904
1905 cuddRef(h1);
1906
1907 g2 = cuddBddIteRecur(dd, topv, factorsNv->g, factorsNnv->h);
1908 if (g2 == NULL) {
1909 Cudd_RecursiveDeref(dd, factorsNv->h);
1910 Cudd_RecursiveDeref(dd, factorsNv->g);
1911 Cudd_RecursiveDeref(dd, factorsNnv->g);
1912 Cudd_RecursiveDeref(dd, factorsNnv->h);
1913 Cudd_RecursiveDeref(dd, g1);
1914 Cudd_RecursiveDeref(dd, h1);
1915 if (freeNv) FREE(factorsNv);
1916 if (freeNnv) FREE(factorsNnv);
1917 return(NULL);
1918 }
1919 cuddRef(g2);
1920 Cudd_RecursiveDeref(dd, factorsNv->g);
1921 Cudd_RecursiveDeref(dd, factorsNnv->h);
1922
1923 h2 = cuddBddIteRecur(dd, topv, factorsNv->h, factorsNnv->g);
1924 if (h2 == NULL) {
1925 Cudd_RecursiveDeref(dd, factorsNv->g);
1926 Cudd_RecursiveDeref(dd, factorsNv->h);
1927 Cudd_RecursiveDeref(dd, factorsNnv->g);
1928 Cudd_RecursiveDeref(dd, factorsNnv->h);
1929 Cudd_RecursiveDeref(dd, g1);
1930 Cudd_RecursiveDeref(dd, h1);
1931 Cudd_RecursiveDeref(dd, g2);
1932 if (freeNv) FREE(factorsNv);
1933 if (freeNnv) FREE(factorsNnv);
1934 return(NULL);
1935 }
1936 cuddRef(h2);
1937 Cudd_RecursiveDeref(dd, factorsNv->h);
1938 Cudd_RecursiveDeref(dd, factorsNnv->g);
1939 if (freeNv) FREE(factorsNv);
1940 if (freeNnv) FREE(factorsNnv);
1941
1942 /* check for each pair in tables and choose one */
1943 factors = CheckInTables(node, g1, h1, g2, h2, ghTable, cacheTable, &outOfMem);
1944 if (outOfMem) {
1945 dd->errorCode = CUDD_MEMORY_OUT;
1946 Cudd_RecursiveDeref(dd, g1);
1947 Cudd_RecursiveDeref(dd, h1);
1948 Cudd_RecursiveDeref(dd, g2);
1949 Cudd_RecursiveDeref(dd, h2);
1950 return(NULL);
1951 }
1952 if (factors != NULL) {
1953 if ((factors->g == g1) || (factors->g == h1)) {
1954 Cudd_RecursiveDeref(dd, g2);
1955 Cudd_RecursiveDeref(dd, h2);
1956 } else {
1957 Cudd_RecursiveDeref(dd, g1);
1958 Cudd_RecursiveDeref(dd, h1);
1959 }
1960 return(factors);
1961 }
1962
1963 /* if not in tables, pick one pair */
1964 factors = PickOnePair(node,g1, h1, g2, h2, ghTable, cacheTable);
1965 if (factors == NULL) {
1966 dd->errorCode = CUDD_MEMORY_OUT;
1967 Cudd_RecursiveDeref(dd, g1);
1968 Cudd_RecursiveDeref(dd, h1);
1969 Cudd_RecursiveDeref(dd, g2);
1970 Cudd_RecursiveDeref(dd, h2);
1971 } else {
1972 /* now free what was created and not used */
1973 if ((factors->g == g1) || (factors->g == h1)) {
1974 Cudd_RecursiveDeref(dd, g2);
1975 Cudd_RecursiveDeref(dd, h2);
1976 } else {
1977 Cudd_RecursiveDeref(dd, g1);
1978 Cudd_RecursiveDeref(dd, h1);
1979 }
1980 }
1981
1982 return(factors);
1983
1984 } /* end of BuildConjuncts */
1985
1986
1987 /**Function********************************************************************
1988
1989 Synopsis [Procedure to compute two conjunctive factors of f and place in *c1 and *c2.]
1990
1991 Description [Procedure to compute two conjunctive factors of f and
1992 place in *c1 and *c2. Sets up the required data - table of distances
1993 from the constant and local reference count. Also minterm table. ]
1994
1995 SideEffects []
1996
1997 SeeAlso []
1998
1999 ******************************************************************************/
2000 static int
cuddConjunctsAux(DdManager * dd,DdNode * f,DdNode ** c1,DdNode ** c2)2001 cuddConjunctsAux(
2002 DdManager * dd,
2003 DdNode * f,
2004 DdNode ** c1,
2005 DdNode ** c2)
2006 {
2007 st_table *distanceTable = NULL;
2008 st_table *cacheTable = NULL;
2009 st_table *mintermTable = NULL;
2010 st_table *ghTable = NULL;
2011 st_generator *stGen;
2012 char *key, *value;
2013 Conjuncts *factors;
2014 int distance, approxDistance;
2015 double max, minterms;
2016 int freeFactors;
2017 NodeStat *nodeStat;
2018 int maxLocalRef;
2019
2020 /* initialize */
2021 *c1 = NULL;
2022 *c2 = NULL;
2023
2024 /* initialize distances table */
2025 distanceTable = st_init_table(st_ptrcmp,st_ptrhash);
2026 if (distanceTable == NULL) goto outOfMem;
2027
2028 /* make the entry for the constant */
2029 nodeStat = ALLOC(NodeStat, 1);
2030 if (nodeStat == NULL) goto outOfMem;
2031 nodeStat->distance = 0;
2032 nodeStat->localRef = 1;
2033 if (st_insert(distanceTable, (char *)one, (char *)nodeStat) == ST_OUT_OF_MEM) {
2034 goto outOfMem;
2035 }
2036
2037 /* Count node distances from constant. */
2038 nodeStat = CreateBotDist(f, distanceTable);
2039 if (nodeStat == NULL) goto outOfMem;
2040
2041 /* set the distance for the decomposition points */
2042 approxDistance = (DEPTH < nodeStat->distance) ? nodeStat->distance : DEPTH;
2043 distance = nodeStat->distance;
2044
2045 if (distance < approxDistance) {
2046 /* Too small to bother. */
2047 *c1 = f;
2048 *c2 = DD_ONE(dd);
2049 cuddRef(*c1); cuddRef(*c2);
2050 stGen = st_init_gen(distanceTable);
2051 if (stGen == NULL) goto outOfMem;
2052 while(st_gen(stGen, (char **)&key, (char **)&value)) {
2053 FREE(value);
2054 }
2055 st_free_gen(stGen); stGen = NULL;
2056 st_free_table(distanceTable);
2057 return(1);
2058 }
2059
2060 /* record the maximum local reference count */
2061 maxLocalRef = 0;
2062 stGen = st_init_gen(distanceTable);
2063 if (stGen == NULL) goto outOfMem;
2064 while(st_gen(stGen, (char **)&key, (char **)&value)) {
2065 nodeStat = (NodeStat *)value;
2066 maxLocalRef = (nodeStat->localRef > maxLocalRef) ?
2067 nodeStat->localRef : maxLocalRef;
2068 }
2069 st_free_gen(stGen); stGen = NULL;
2070
2071
2072 /* Count minterms for each node. */
2073 max = pow(2.0, (double)Cudd_SupportSize(dd,f)); /* potential overflow */
2074 mintermTable = st_init_table(st_ptrcmp,st_ptrhash);
2075 if (mintermTable == NULL) goto outOfMem;
2076 minterms = CountMinterms(f, max, mintermTable, dd->err);
2077 if (minterms == -1.0) goto outOfMem;
2078
2079 lastTimeG = Cudd_Random() & 1;
2080 cacheTable = st_init_table(st_ptrcmp, st_ptrhash);
2081 if (cacheTable == NULL) goto outOfMem;
2082 ghTable = st_init_table(st_ptrcmp, st_ptrhash);
2083 if (ghTable == NULL) goto outOfMem;
2084
2085 /* Build conjuncts. */
2086 factors = BuildConjuncts(dd, f, distanceTable, cacheTable,
2087 approxDistance, maxLocalRef, ghTable, mintermTable);
2088 if (factors == NULL) goto outOfMem;
2089
2090 /* free up tables */
2091 stGen = st_init_gen(distanceTable);
2092 if (stGen == NULL) goto outOfMem;
2093 while(st_gen(stGen, (char **)&key, (char **)&value)) {
2094 FREE(value);
2095 }
2096 st_free_gen(stGen); stGen = NULL;
2097 st_free_table(distanceTable); distanceTable = NULL;
2098 st_free_table(ghTable); ghTable = NULL;
2099
2100 stGen = st_init_gen(mintermTable);
2101 if (stGen == NULL) goto outOfMem;
2102 while(st_gen(stGen, (char **)&key, (char **)&value)) {
2103 FREE(value);
2104 }
2105 st_free_gen(stGen); stGen = NULL;
2106 st_free_table(mintermTable); mintermTable = NULL;
2107
2108 freeFactors = FactorsNotStored(factors);
2109 factors = (freeFactors) ? FactorsUncomplement(factors) : factors;
2110 if (factors != NULL) {
2111 *c1 = factors->g;
2112 *c2 = factors->h;
2113 cuddRef(*c1);
2114 cuddRef(*c2);
2115 if (freeFactors) FREE(factors);
2116
2117 #if 0
2118 if ((*c1 == f) && (!Cudd_IsConstant(f))) {
2119 assert(*c2 == one);
2120 }
2121 if ((*c2 == f) && (!Cudd_IsConstant(f))) {
2122 assert(*c1 == one);
2123 }
2124
2125 if ((*c1 != one) && (!Cudd_IsConstant(f))) {
2126 assert(!Cudd_bddLeq(dd, *c2, *c1));
2127 }
2128 if ((*c2 != one) && (!Cudd_IsConstant(f))) {
2129 assert(!Cudd_bddLeq(dd, *c1, *c2));
2130 }
2131 #endif
2132 }
2133
2134 stGen = st_init_gen(cacheTable);
2135 if (stGen == NULL) goto outOfMem;
2136 while(st_gen(stGen, (char **)&key, (char **)&value)) {
2137 ConjunctsFree(dd, (Conjuncts *)value);
2138 }
2139 st_free_gen(stGen); stGen = NULL;
2140
2141 st_free_table(cacheTable); cacheTable = NULL;
2142
2143 return(1);
2144
2145 outOfMem:
2146 if (distanceTable != NULL) {
2147 stGen = st_init_gen(distanceTable);
2148 if (stGen == NULL) goto outOfMem;
2149 while(st_gen(stGen, (char **)&key, (char **)&value)) {
2150 FREE(value);
2151 }
2152 st_free_gen(stGen); stGen = NULL;
2153 st_free_table(distanceTable); distanceTable = NULL;
2154 }
2155 if (mintermTable != NULL) {
2156 stGen = st_init_gen(mintermTable);
2157 if (stGen == NULL) goto outOfMem;
2158 while(st_gen(stGen, (char **)&key, (char **)&value)) {
2159 FREE(value);
2160 }
2161 st_free_gen(stGen); stGen = NULL;
2162 st_free_table(mintermTable); mintermTable = NULL;
2163 }
2164 if (ghTable != NULL) st_free_table(ghTable);
2165 if (cacheTable != NULL) {
2166 stGen = st_init_gen(cacheTable);
2167 if (stGen == NULL) goto outOfMem;
2168 while(st_gen(stGen, (char **)&key, (char **)&value)) {
2169 ConjunctsFree(dd, (Conjuncts *)value);
2170 }
2171 st_free_gen(stGen); stGen = NULL;
2172 st_free_table(cacheTable); cacheTable = NULL;
2173 }
2174 dd->errorCode = CUDD_MEMORY_OUT;
2175 return(0);
2176
2177 } /* end of cuddConjunctsAux */
2178