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