source: vis_dev/glu-2.3/src/cuBdd/cuddDecomp.c @ 100

Last change on this file since 100 was 13, checked in by cecile, 13 years ago

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