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