source: vis_dev/glu-2.3/src/cuBdd/cuddUtil.c @ 102

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

library glu 2.3
File size: 103.6 KB
RevLine 
[13]1/**CFile***********************************************************************
2
3  FileName    [cuddUtil.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Utility functions.]
8
9  Description [External procedures included in this module:
10                <ul>
11                <li> Cudd_PrintMinterm()
12                <li> Cudd_bddPrintCover()
13                <li> Cudd_PrintDebug()
14                <li> Cudd_DagSize()
15                <li> Cudd_EstimateCofactor()
16                <li> Cudd_EstimateCofactorSimple()
17                <li> Cudd_SharingSize()
18                <li> Cudd_CountMinterm()
19                <li> Cudd_EpdCountMinterm()
20                <li> Cudd_CountPath()
21                <li> Cudd_CountPathsToNonZero()
22                <li> Cudd_Support()
23                <li> Cudd_SupportIndex()
24                <li> Cudd_SupportSize()
25                <li> Cudd_VectorSupport()
26                <li> Cudd_VectorSupportIndex()
27                <li> Cudd_VectorSupportSize()
28                <li> Cudd_ClassifySupport()
29                <li> Cudd_CountLeaves()
30                <li> Cudd_bddPickOneCube()
31                <li> Cudd_bddPickOneMinterm()
32                <li> Cudd_bddPickArbitraryMinterms()
33                <li> Cudd_SubsetWithMaskVars()
34                <li> Cudd_FirstCube()
35                <li> Cudd_NextCube()
36                <li> Cudd_bddComputeCube()
37                <li> Cudd_addComputeCube()
38                <li> Cudd_FirstNode()
39                <li> Cudd_NextNode()
40                <li> Cudd_GenFree()
41                <li> Cudd_IsGenEmpty()
42                <li> Cudd_IndicesToCube()
43                <li> Cudd_PrintVersion()
44                <li> Cudd_AverageDistance()
45                <li> Cudd_Random()
46                <li> Cudd_Srandom()
47                <li> Cudd_Density()
48                </ul>
49        Internal procedures included in this module:
50                <ul>
51                <li> cuddP()
52                <li> cuddStCountfree()
53                <li> cuddCollectNodes()
54                <li> cuddNodeArray()
55                </ul>
56        Static procedures included in this module:
57                <ul>
58                <li> dp2()
59                <li> ddPrintMintermAux()
60                <li> ddDagInt()
61                <li> ddCountMintermAux()
62                <li> ddEpdCountMintermAux()
63                <li> ddCountPathAux()
64                <li> ddSupportStep()
65                <li> ddClearFlag()
66                <li> ddLeavesInt()
67                <li> ddPickArbitraryMinterms()
68                <li> ddPickRepresentativeCube()
69                <li> ddEpdFree()
70                </ul>]
71
72  Author      [Fabio Somenzi]
73
74  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
75
76  All rights reserved.
77
78  Redistribution and use in source and binary forms, with or without
79  modification, are permitted provided that the following conditions
80  are met:
81
82  Redistributions of source code must retain the above copyright
83  notice, this list of conditions and the following disclaimer.
84
85  Redistributions in binary form must reproduce the above copyright
86  notice, this list of conditions and the following disclaimer in the
87  documentation and/or other materials provided with the distribution.
88
89  Neither the name of the University of Colorado nor the names of its
90  contributors may be used to endorse or promote products derived from
91  this software without specific prior written permission.
92
93  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
94  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
95  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
96  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
97  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
98  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
99  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
100  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
101  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
102  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
103  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
104  POSSIBILITY OF SUCH DAMAGE.]
105
106******************************************************************************/
107
108#include "util.h"
109#include "cuddInt.h"
110
111/*---------------------------------------------------------------------------*/
112/* Constant declarations                                                     */
113/*---------------------------------------------------------------------------*/
114
115/* Random generator constants. */
116#define MODULUS1 2147483563
117#define LEQA1 40014
118#define LEQQ1 53668
119#define LEQR1 12211
120#define MODULUS2 2147483399
121#define LEQA2 40692
122#define LEQQ2 52774
123#define LEQR2 3791
124#define STAB_SIZE 64
125#define STAB_DIV (1 + (MODULUS1 - 1) / STAB_SIZE)
126
127/*---------------------------------------------------------------------------*/
128/* Stucture declarations                                                     */
129/*---------------------------------------------------------------------------*/
130
131/*---------------------------------------------------------------------------*/
132/* Type declarations                                                         */
133/*---------------------------------------------------------------------------*/
134
135
136/*---------------------------------------------------------------------------*/
137/* Variable declarations                                                     */
138/*---------------------------------------------------------------------------*/
139
140#ifndef lint
141static char rcsid[] DD_UNUSED = "$Id: cuddUtil.c,v 1.81 2009/03/08 02:49:02 fabio Exp $";
142#endif
143
144static  DdNode  *background, *zero;
145
146static  long cuddRand = 0;
147static  long cuddRand2;
148static  long shuffleSelect;
149static  long shuffleTable[STAB_SIZE];
150
151/*---------------------------------------------------------------------------*/
152/* Macro declarations                                                        */
153/*---------------------------------------------------------------------------*/
154
155#define bang(f) ((Cudd_IsComplement(f)) ? '!' : ' ')
156
157#ifdef __cplusplus
158extern "C" {
159#endif
160
161/**AutomaticStart*************************************************************/
162
163/*---------------------------------------------------------------------------*/
164/* Static function prototypes                                                */
165/*---------------------------------------------------------------------------*/
166
167static int dp2 (DdManager *dd, DdNode *f, st_table *t);
168static void ddPrintMintermAux (DdManager *dd, DdNode *node, int *list);
169static int ddDagInt (DdNode *n);
170static int cuddNodeArrayRecur (DdNode *f, DdNodePtr *table, int index);
171static int cuddEstimateCofactor (DdManager *dd, st_table *table, DdNode * node, int i, int phase, DdNode ** ptr);
172static DdNode * cuddUniqueLookup (DdManager * unique, int  index, DdNode * T, DdNode * E);
173static int cuddEstimateCofactorSimple (DdNode * node, int i);
174static double ddCountMintermAux (DdNode *node, double max, DdHashTable *table);
175static int ddEpdCountMintermAux (DdNode *node, EpDouble *max, EpDouble *epd, st_table *table);
176static double ddCountPathAux (DdNode *node, st_table *table);
177static double ddCountPathsToNonZero (DdNode * N, st_table * table);
178static void ddSupportStep (DdNode *f, int *support);
179static void ddClearFlag (DdNode *f);
180static int ddLeavesInt (DdNode *n);
181static int ddPickArbitraryMinterms (DdManager *dd, DdNode *node, int nvars, int nminterms, char **string);
182static int ddPickRepresentativeCube (DdManager *dd, DdNode *node, double *weight, char *string);
183static enum st_retval ddEpdFree (char * key, char * value, char * arg);
184
185/**AutomaticEnd***************************************************************/
186
187#ifdef __cplusplus
188}
189#endif
190
191/*---------------------------------------------------------------------------*/
192/* Definition of exported functions                                          */
193/*---------------------------------------------------------------------------*/
194
195
196/**Function********************************************************************
197
198  Synopsis    [Prints a disjoint sum of products.]
199
200  Description [Prints a disjoint sum of product cover for the function
201  rooted at node. Each product corresponds to a path from node to a
202  leaf node different from the logical zero, and different from the
203  background value. Uses the package default output file.  Returns 1
204  if successful; 0 otherwise.]
205
206  SideEffects [None]
207
208  SeeAlso     [Cudd_PrintDebug Cudd_bddPrintCover]
209
210******************************************************************************/
211int
212Cudd_PrintMinterm(
213  DdManager * manager,
214  DdNode * node)
215{
216    int         i, *list;
217
218    background = manager->background;
219    zero = Cudd_Not(manager->one);
220    list = ALLOC(int,manager->size);
221    if (list == NULL) {
222        manager->errorCode = CUDD_MEMORY_OUT;
223        return(0);
224    }
225    for (i = 0; i < manager->size; i++) list[i] = 2;
226    ddPrintMintermAux(manager,node,list);
227    FREE(list);
228    return(1);
229
230} /* end of Cudd_PrintMinterm */
231
232
233/**Function********************************************************************
234
235  Synopsis    [Prints a sum of prime implicants of a BDD.]
236
237  Description [Prints a sum of product cover for an incompletely
238  specified function given by a lower bound and an upper bound.  Each
239  product is a prime implicant obtained by expanding the product
240  corresponding to a path from node to the constant one.  Uses the
241  package default output file.  Returns 1 if successful; 0 otherwise.]
242
243  SideEffects [None]
244
245  SeeAlso     [Cudd_PrintMinterm]
246
247******************************************************************************/
248int
249Cudd_bddPrintCover(
250  DdManager *dd,
251  DdNode *l,
252  DdNode *u)
253{
254    int *array;
255    int q, result;
256    DdNode *lb;
257#ifdef DD_DEBUG
258    DdNode *cover;
259#endif
260
261    array = ALLOC(int, Cudd_ReadSize(dd));
262    if (array == NULL) return(0);
263    lb = l;
264    cuddRef(lb);
265#ifdef DD_DEBUG
266    cover = Cudd_ReadLogicZero(dd);
267    cuddRef(cover);
268#endif
269    while (lb != Cudd_ReadLogicZero(dd)) {
270        DdNode *implicant, *prime, *tmp;
271        int length;
272        implicant = Cudd_LargestCube(dd,lb,&length);
273        if (implicant == NULL) {
274            Cudd_RecursiveDeref(dd,lb);
275            FREE(array);
276            return(0);
277        }
278        cuddRef(implicant);
279        prime = Cudd_bddMakePrime(dd,implicant,u);
280        if (prime == NULL) {
281            Cudd_RecursiveDeref(dd,lb);
282            Cudd_RecursiveDeref(dd,implicant);
283            FREE(array);
284            return(0);
285        }
286        cuddRef(prime);
287        Cudd_RecursiveDeref(dd,implicant);
288        tmp = Cudd_bddAnd(dd,lb,Cudd_Not(prime));
289        if (tmp == NULL) {
290            Cudd_RecursiveDeref(dd,lb);
291            Cudd_RecursiveDeref(dd,prime);
292            FREE(array);
293            return(0);
294        }
295        cuddRef(tmp);
296        Cudd_RecursiveDeref(dd,lb);
297        lb = tmp;
298        result = Cudd_BddToCubeArray(dd,prime,array);
299        if (result == 0) {
300            Cudd_RecursiveDeref(dd,lb);
301            Cudd_RecursiveDeref(dd,prime);
302            FREE(array);
303            return(0);
304        }
305        for (q = 0; q < dd->size; q++) {
306            switch (array[q]) {
307            case 0:
308                (void) fprintf(dd->out, "0");
309                break;
310            case 1:
311                (void) fprintf(dd->out, "1");
312                break;
313            case 2:
314                (void) fprintf(dd->out, "-");
315                break;
316            default:
317                (void) fprintf(dd->out, "?");
318            }
319        }
320        (void) fprintf(dd->out, " 1\n");
321#ifdef DD_DEBUG
322        tmp = Cudd_bddOr(dd,prime,cover);
323        if (tmp == NULL) {
324            Cudd_RecursiveDeref(dd,cover);
325            Cudd_RecursiveDeref(dd,lb);
326            Cudd_RecursiveDeref(dd,prime);
327            FREE(array);
328            return(0);
329        }
330        cuddRef(tmp);
331        Cudd_RecursiveDeref(dd,cover);
332        cover = tmp;
333#endif
334        Cudd_RecursiveDeref(dd,prime);
335    }
336    (void) fprintf(dd->out, "\n");
337    Cudd_RecursiveDeref(dd,lb);
338    FREE(array);
339#ifdef DD_DEBUG
340    if (!Cudd_bddLeq(dd,cover,u) || !Cudd_bddLeq(dd,l,cover)) {
341        Cudd_RecursiveDeref(dd,cover);
342        return(0);
343    }
344    Cudd_RecursiveDeref(dd,cover);
345#endif
346    return(1);
347
348} /* end of Cudd_bddPrintCover */
349
350
351/**Function********************************************************************
352
353  Synopsis    [Prints to the standard output a DD and its statistics.]
354
355  Description [Prints to the standard output a DD and its statistics.
356  The statistics include the number of nodes, the number of leaves, and
357  the number of minterms. (The number of minterms is the number of
358  assignments to the variables that cause the function to be different
359  from the logical zero (for BDDs) and from the background value (for
360  ADDs.) The statistics are printed if pr &gt; 0. Specifically:
361  <ul>
362  <li> pr = 0 : prints nothing
363  <li> pr = 1 : prints counts of nodes and minterms
364  <li> pr = 2 : prints counts + disjoint sum of product
365  <li> pr = 3 : prints counts + list of nodes
366  <li> pr &gt; 3 : prints counts + disjoint sum of product + list of nodes
367  </ul>
368  For the purpose of counting the number of minterms, the function is
369  supposed to depend on n variables. Returns 1 if successful; 0 otherwise.]
370
371  SideEffects [None]
372
373  SeeAlso     [Cudd_DagSize Cudd_CountLeaves Cudd_CountMinterm
374  Cudd_PrintMinterm]
375
376******************************************************************************/
377int
378Cudd_PrintDebug(
379  DdManager * dd,
380  DdNode * f,
381  int  n,
382  int  pr)
383{
384    DdNode *azero, *bzero;
385    int    nodes;
386    int    leaves;
387    double minterms;
388    int    retval = 1;
389
390    if (f == NULL) {
391        (void) fprintf(dd->out,": is the NULL DD\n");
392        (void) fflush(dd->out);
393        return(0);
394    }
395    azero = DD_ZERO(dd);
396    bzero = Cudd_Not(DD_ONE(dd));
397    if ((f == azero || f == bzero) && pr > 0){
398       (void) fprintf(dd->out,": is the zero DD\n");
399       (void) fflush(dd->out);
400       return(1);
401    }
402    if (pr > 0) {
403        nodes = Cudd_DagSize(f);
404        if (nodes == CUDD_OUT_OF_MEM) retval = 0;
405        leaves = Cudd_CountLeaves(f);
406        if (leaves == CUDD_OUT_OF_MEM) retval = 0;
407        minterms = Cudd_CountMinterm(dd, f, n);
408        if (minterms == (double)CUDD_OUT_OF_MEM) retval = 0;
409        (void) fprintf(dd->out,": %d nodes %d leaves %g minterms\n",
410                       nodes, leaves, minterms);
411        if (pr > 2) {
412            if (!cuddP(dd, f)) retval = 0;
413        }
414        if (pr == 2 || pr > 3) {
415            if (!Cudd_PrintMinterm(dd,f)) retval = 0;
416            (void) fprintf(dd->out,"\n");
417        }
418        (void) fflush(dd->out);
419    }
420    return(retval);
421
422} /* end of Cudd_PrintDebug */
423
424
425/**Function********************************************************************
426
427  Synopsis    [Counts the number of nodes in a DD.]
428
429  Description [Counts the number of nodes in a DD. Returns the number
430  of nodes in the graph rooted at node.]
431
432  SideEffects [None]
433
434  SeeAlso     [Cudd_SharingSize Cudd_PrintDebug]
435
436******************************************************************************/
437int
438Cudd_DagSize(
439  DdNode * node)
440{
441    int i;
442
443    i = ddDagInt(Cudd_Regular(node));
444    ddClearFlag(Cudd_Regular(node));
445
446    return(i);
447
448} /* end of Cudd_DagSize */
449
450
451/**Function********************************************************************
452
453  Synopsis    [Estimates the number of nodes in a cofactor of a DD.]
454
455  Description [Estimates the number of nodes in a cofactor of a DD.
456  Returns an estimate of the number of nodes in a cofactor of
457  the graph rooted at node with respect to the variable whose index is i.
458  In case of failure, returns CUDD_OUT_OF_MEM.
459  This function uses a refinement of the algorithm of Cabodi et al.
460  (ICCAD96). The refinement allows the procedure to account for part
461  of the recombination that may occur in the part of the cofactor above
462  the cofactoring variable. This procedure does no create any new node.
463  It does keep a small table of results; therefore it may run out of memory.
464  If this is a concern, one should use Cudd_EstimateCofactorSimple, which
465  is faster, does not allocate any memory, but is less accurate.]
466
467  SideEffects [None]
468
469  SeeAlso     [Cudd_DagSize Cudd_EstimateCofactorSimple]
470
471******************************************************************************/
472int
473Cudd_EstimateCofactor(
474  DdManager *dd /* manager */,
475  DdNode * f    /* function */,
476  int i         /* index of variable */,
477  int phase     /* 1: positive; 0: negative */
478  )
479{
480    int val;
481    DdNode *ptr;
482    st_table *table;
483
484    table = st_init_table(st_ptrcmp,st_ptrhash);
485    if (table == NULL) return(CUDD_OUT_OF_MEM);
486    val = cuddEstimateCofactor(dd,table,Cudd_Regular(f),i,phase,&ptr);
487    ddClearFlag(Cudd_Regular(f));
488    st_free_table(table);
489
490    return(val);
491
492} /* end of Cudd_EstimateCofactor */
493
494
495/**Function********************************************************************
496
497  Synopsis    [Estimates the number of nodes in a cofactor of a DD.]
498
499  Description [Estimates the number of nodes in a cofactor of a DD.
500  Returns an estimate of the number of nodes in the positive cofactor of
501  the graph rooted at node with respect to the variable whose index is i.
502  This procedure implements with minor changes the algorithm of Cabodi et al.
503  (ICCAD96). It does not allocate any memory, it does not change the
504  state of the manager, and it is fast. However, it has been observed to
505  overestimate the size of the cofactor by as much as a factor of 2.]
506
507  SideEffects [None]
508
509  SeeAlso     [Cudd_DagSize]
510
511******************************************************************************/
512int
513Cudd_EstimateCofactorSimple(
514  DdNode * node,
515  int i)
516{
517    int val;
518
519    val = cuddEstimateCofactorSimple(Cudd_Regular(node),i);
520    ddClearFlag(Cudd_Regular(node));
521
522    return(val);
523
524} /* end of Cudd_EstimateCofactorSimple */
525
526
527/**Function********************************************************************
528
529  Synopsis    [Counts the number of nodes in an array of DDs.]
530
531  Description [Counts the number of nodes in an array of DDs. Shared
532  nodes are counted only once.  Returns the total number of nodes.]
533
534  SideEffects [None]
535
536  SeeAlso     [Cudd_DagSize]
537
538******************************************************************************/
539int
540Cudd_SharingSize(
541  DdNode ** nodeArray,
542  int  n)
543{
544    int i,j;
545
546    i = 0;
547    for (j = 0; j < n; j++) {
548        i += ddDagInt(Cudd_Regular(nodeArray[j]));
549    }
550    for (j = 0; j < n; j++) {
551        ddClearFlag(Cudd_Regular(nodeArray[j]));
552    }
553    return(i);
554
555} /* end of Cudd_SharingSize */
556
557
558/**Function********************************************************************
559
560  Synopsis    [Counts the number of minterms of a DD.]
561
562  Description [Counts the number of minterms of a DD. The function is
563  assumed to depend on nvars variables. The minterm count is
564  represented as a double, to allow for a larger number of variables.
565  Returns the number of minterms of the function rooted at node if
566  successful; (double) CUDD_OUT_OF_MEM otherwise.]
567
568  SideEffects [None]
569
570  SeeAlso     [Cudd_PrintDebug Cudd_CountPath]
571
572******************************************************************************/
573double
574Cudd_CountMinterm(
575  DdManager * manager,
576  DdNode * node,
577  int  nvars)
578{
579    double      max;
580    DdHashTable *table;
581    double      res;
582    CUDD_VALUE_TYPE epsilon;
583
584    background = manager->background;
585    zero = Cudd_Not(manager->one);
586
587    max = pow(2.0,(double)nvars);
588    table = cuddHashTableInit(manager,1,2);
589    if (table == NULL) {
590        return((double)CUDD_OUT_OF_MEM);
591    }
592    epsilon = Cudd_ReadEpsilon(manager);
593    Cudd_SetEpsilon(manager,(CUDD_VALUE_TYPE)0.0);
594    res = ddCountMintermAux(node,max,table);
595    cuddHashTableQuit(table);
596    Cudd_SetEpsilon(manager,epsilon);
597
598    return(res);
599
600} /* end of Cudd_CountMinterm */
601
602
603/**Function********************************************************************
604
605  Synopsis    [Counts the number of paths of a DD.]
606
607  Description [Counts the number of paths of a DD.  Paths to all
608  terminal nodes are counted. The path count is represented as a
609  double, to allow for a larger number of variables.  Returns the
610  number of paths of the function rooted at node if successful;
611  (double) CUDD_OUT_OF_MEM otherwise.]
612
613  SideEffects [None]
614
615  SeeAlso     [Cudd_CountMinterm]
616
617******************************************************************************/
618double
619Cudd_CountPath(
620  DdNode * node)
621{
622
623    st_table    *table;
624    double      i;
625
626    table = st_init_table(st_ptrcmp,st_ptrhash);
627    if (table == NULL) {
628        return((double)CUDD_OUT_OF_MEM);
629    }
630    i = ddCountPathAux(Cudd_Regular(node),table);
631    st_foreach(table, cuddStCountfree, NULL);
632    st_free_table(table);
633    return(i);
634
635} /* end of Cudd_CountPath */
636
637
638/**Function********************************************************************
639
640  Synopsis    [Counts the number of minterms of a DD with extended precision.]
641
642  Description [Counts the number of minterms of a DD with extended precision.
643  The function is assumed to depend on nvars variables. The minterm count is
644  represented as an EpDouble, to allow any number of variables.
645  Returns 0 if successful; CUDD_OUT_OF_MEM otherwise.]
646
647  SideEffects [None]
648
649  SeeAlso     [Cudd_PrintDebug Cudd_CountPath]
650
651******************************************************************************/
652int
653Cudd_EpdCountMinterm(
654  DdManager * manager,
655  DdNode * node,
656  int  nvars,
657  EpDouble * epd)
658{
659    EpDouble    max, tmp;
660    st_table    *table;
661    int         status;
662
663    background = manager->background;
664    zero = Cudd_Not(manager->one);
665
666    EpdPow2(nvars, &max);
667    table = st_init_table(EpdCmp, st_ptrhash);
668    if (table == NULL) {
669        EpdMakeZero(epd, 0);
670        return(CUDD_OUT_OF_MEM);
671    }
672    status = ddEpdCountMintermAux(Cudd_Regular(node),&max,epd,table);
673    st_foreach(table, ddEpdFree, NULL);
674    st_free_table(table);
675    if (status == CUDD_OUT_OF_MEM) {
676        EpdMakeZero(epd, 0);
677        return(CUDD_OUT_OF_MEM);
678    }
679    if (Cudd_IsComplement(node)) {
680        EpdSubtract3(&max, epd, &tmp);
681        EpdCopy(&tmp, epd);
682    }
683    return(0);
684
685} /* end of Cudd_EpdCountMinterm */
686
687
688/**Function********************************************************************
689
690  Synopsis    [Counts the number of paths to a non-zero terminal of a DD.]
691
692  Description [Counts the number of paths to a non-zero terminal of a
693  DD.  The path count is
694  represented as a double, to allow for a larger number of variables.
695  Returns the number of paths of the function rooted at node.]
696
697  SideEffects [None]
698
699  SeeAlso     [Cudd_CountMinterm Cudd_CountPath]
700
701******************************************************************************/
702double
703Cudd_CountPathsToNonZero(
704  DdNode * node)
705{
706
707    st_table    *table;
708    double      i;
709
710    table = st_init_table(st_ptrcmp,st_ptrhash);
711    if (table == NULL) {
712        return((double)CUDD_OUT_OF_MEM);
713    }
714    i = ddCountPathsToNonZero(node,table);
715    st_foreach(table, cuddStCountfree, NULL);
716    st_free_table(table);
717    return(i);
718
719} /* end of Cudd_CountPathsToNonZero */
720
721
722/**Function********************************************************************
723
724  Synopsis    [Finds the variables on which a DD depends.]
725
726  Description [Finds the variables on which a DD depends.
727  Returns a BDD consisting of the product of the variables if
728  successful; NULL otherwise.]
729
730  SideEffects [None]
731
732  SeeAlso     [Cudd_VectorSupport Cudd_ClassifySupport]
733
734******************************************************************************/
735DdNode *
736Cudd_Support(
737  DdManager * dd /* manager */,
738  DdNode * f /* DD whose support is sought */)
739{
740    int *support;
741    DdNode *res, *tmp, *var;
742    int i,j;
743    int size;
744
745    /* Allocate and initialize support array for ddSupportStep. */
746    size = ddMax(dd->size, dd->sizeZ);
747    support = ALLOC(int,size);
748    if (support == NULL) {
749        dd->errorCode = CUDD_MEMORY_OUT;
750        return(NULL);
751    }
752    for (i = 0; i < size; i++) {
753        support[i] = 0;
754    }
755
756    /* Compute support and clean up markers. */
757    ddSupportStep(Cudd_Regular(f),support);
758    ddClearFlag(Cudd_Regular(f));
759
760    /* Transform support from array to cube. */
761    do {
762        dd->reordered = 0;
763        res = DD_ONE(dd);
764        cuddRef(res);
765        for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
766            i = (j >= dd->size) ? j : dd->invperm[j];
767            if (support[i] == 1) {
768                /* The following call to cuddUniqueInter is guaranteed
769                ** not to trigger reordering because the node we look up
770                ** already exists. */
771                var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
772                cuddRef(var);
773                tmp = cuddBddAndRecur(dd,res,var);
774                if (tmp == NULL) {
775                    Cudd_RecursiveDeref(dd,res);
776                    Cudd_RecursiveDeref(dd,var);
777                    res = NULL;
778                    break;
779                }
780                cuddRef(tmp);
781                Cudd_RecursiveDeref(dd,res);
782                Cudd_RecursiveDeref(dd,var);
783                res = tmp;
784            }
785        }
786    } while (dd->reordered == 1);
787
788    FREE(support);
789    if (res != NULL) cuddDeref(res);
790    return(res);
791
792} /* end of Cudd_Support */
793
794
795/**Function********************************************************************
796
797  Synopsis    [Finds the variables on which a DD depends.]
798
799  Description [Finds the variables on which a DD depends.  Returns an
800  index array of the variables if successful; NULL otherwise.  The
801  size of the array equals the number of variables in the manager.
802  Each entry of the array is 1 if the corresponding variable is in the
803  support of the DD and 0 otherwise.]
804
805  SideEffects [None]
806
807  SeeAlso     [Cudd_Support Cudd_VectorSupport Cudd_ClassifySupport]
808
809******************************************************************************/
810int *
811Cudd_SupportIndex(
812  DdManager * dd /* manager */,
813  DdNode * f /* DD whose support is sought */)
814{
815    int *support;
816    int i;
817    int size;
818
819    /* Allocate and initialize support array for ddSupportStep. */
820    size = ddMax(dd->size, dd->sizeZ);
821    support = ALLOC(int,size);
822    if (support == NULL) {
823        dd->errorCode = CUDD_MEMORY_OUT;
824        return(NULL);
825    }
826    for (i = 0; i < size; i++) {
827        support[i] = 0;
828    }
829
830    /* Compute support and clean up markers. */
831    ddSupportStep(Cudd_Regular(f),support);
832    ddClearFlag(Cudd_Regular(f));
833
834    return(support);
835
836} /* end of Cudd_SupportIndex */
837
838
839/**Function********************************************************************
840
841  Synopsis    [Counts the variables on which a DD depends.]
842
843  Description [Counts the variables on which a DD depends.
844  Returns the number of the variables if successful; CUDD_OUT_OF_MEM
845  otherwise.]
846
847  SideEffects [None]
848
849  SeeAlso     [Cudd_Support]
850
851******************************************************************************/
852int
853Cudd_SupportSize(
854  DdManager * dd /* manager */,
855  DdNode * f /* DD whose support size is sought */)
856{
857    int *support;
858    int i;
859    int size;
860    int count;
861
862    /* Allocate and initialize support array for ddSupportStep. */
863    size = ddMax(dd->size, dd->sizeZ);
864    support = ALLOC(int,size);
865    if (support == NULL) {
866        dd->errorCode = CUDD_MEMORY_OUT;
867        return(CUDD_OUT_OF_MEM);
868    }
869    for (i = 0; i < size; i++) {
870        support[i] = 0;
871    }
872
873    /* Compute support and clean up markers. */
874    ddSupportStep(Cudd_Regular(f),support);
875    ddClearFlag(Cudd_Regular(f));
876
877    /* Count support variables. */
878    count = 0;
879    for (i = 0; i < size; i++) {
880        if (support[i] == 1) count++;
881    }
882
883    FREE(support);
884    return(count);
885
886} /* end of Cudd_SupportSize */
887
888
889/**Function********************************************************************
890
891  Synopsis    [Finds the variables on which a set of DDs depends.]
892
893  Description [Finds the variables on which a set of DDs depends.
894  The set must contain either BDDs and ADDs, or ZDDs.
895  Returns a BDD consisting of the product of the variables if
896  successful; NULL otherwise.]
897
898  SideEffects [None]
899
900  SeeAlso     [Cudd_Support Cudd_ClassifySupport]
901
902******************************************************************************/
903DdNode *
904Cudd_VectorSupport(
905  DdManager * dd /* manager */,
906  DdNode ** F /* array of DDs whose support is sought */,
907  int  n /* size of the array */)
908{
909    int *support;
910    DdNode *res, *tmp, *var;
911    int i,j;
912    int size;
913
914    /* Allocate and initialize support array for ddSupportStep. */
915    size = ddMax(dd->size, dd->sizeZ);
916    support = ALLOC(int,size);
917    if (support == NULL) {
918        dd->errorCode = CUDD_MEMORY_OUT;
919        return(NULL);
920    }
921    for (i = 0; i < size; i++) {
922        support[i] = 0;
923    }
924
925    /* Compute support and clean up markers. */
926    for (i = 0; i < n; i++) {
927        ddSupportStep(Cudd_Regular(F[i]),support);
928    }
929    for (i = 0; i < n; i++) {
930        ddClearFlag(Cudd_Regular(F[i]));
931    }
932
933    /* Transform support from array to cube. */
934    res = DD_ONE(dd);
935    cuddRef(res);
936    for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
937        i = (j >= dd->size) ? j : dd->invperm[j];
938        if (support[i] == 1) {
939            var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
940            cuddRef(var);
941            tmp = Cudd_bddAnd(dd,res,var);
942            if (tmp == NULL) {
943                Cudd_RecursiveDeref(dd,res);
944                Cudd_RecursiveDeref(dd,var);
945                FREE(support);
946                return(NULL);
947            }
948            cuddRef(tmp);
949            Cudd_RecursiveDeref(dd,res);
950            Cudd_RecursiveDeref(dd,var);
951            res = tmp;
952        }
953    }
954
955    FREE(support);
956    cuddDeref(res);
957    return(res);
958
959} /* end of Cudd_VectorSupport */
960
961
962/**Function********************************************************************
963
964  Synopsis    [Finds the variables on which a set of DDs depends.]
965
966  Description [Finds the variables on which a set of DDs depends.
967  The set must contain either BDDs and ADDs, or ZDDs.
968  Returns an index array of the variables if successful; NULL otherwise.]
969
970  SideEffects [None]
971
972  SeeAlso     [Cudd_SupportIndex Cudd_VectorSupport Cudd_ClassifySupport]
973
974******************************************************************************/
975int *
976Cudd_VectorSupportIndex(
977  DdManager * dd /* manager */,
978  DdNode ** F /* array of DDs whose support is sought */,
979  int  n /* size of the array */)
980{
981    int *support;
982    int i;
983    int size;
984
985    /* Allocate and initialize support array for ddSupportStep. */
986    size = ddMax(dd->size, dd->sizeZ);
987    support = ALLOC(int,size);
988    if (support == NULL) {
989        dd->errorCode = CUDD_MEMORY_OUT;
990        return(NULL);
991    }
992    for (i = 0; i < size; i++) {
993        support[i] = 0;
994    }
995
996    /* Compute support and clean up markers. */
997    for (i = 0; i < n; i++) {
998        ddSupportStep(Cudd_Regular(F[i]),support);
999    }
1000    for (i = 0; i < n; i++) {
1001        ddClearFlag(Cudd_Regular(F[i]));
1002    }
1003
1004    return(support);
1005
1006} /* end of Cudd_VectorSupportIndex */
1007
1008
1009/**Function********************************************************************
1010
1011  Synopsis    [Counts the variables on which a set of DDs depends.]
1012
1013  Description [Counts the variables on which a set of DDs depends.
1014  The set must contain either BDDs and ADDs, or ZDDs.
1015  Returns the number of the variables if successful; CUDD_OUT_OF_MEM
1016  otherwise.]
1017
1018  SideEffects [None]
1019
1020  SeeAlso     [Cudd_VectorSupport Cudd_SupportSize]
1021
1022******************************************************************************/
1023int
1024Cudd_VectorSupportSize(
1025  DdManager * dd /* manager */,
1026  DdNode ** F /* array of DDs whose support is sought */,
1027  int  n /* size of the array */)
1028{
1029    int *support;
1030    int i;
1031    int size;
1032    int count;
1033
1034    /* Allocate and initialize support array for ddSupportStep. */
1035    size = ddMax(dd->size, dd->sizeZ);
1036    support = ALLOC(int,size);
1037    if (support == NULL) {
1038        dd->errorCode = CUDD_MEMORY_OUT;
1039        return(CUDD_OUT_OF_MEM);
1040    }
1041    for (i = 0; i < size; i++) {
1042        support[i] = 0;
1043    }
1044
1045    /* Compute support and clean up markers. */
1046    for (i = 0; i < n; i++) {
1047        ddSupportStep(Cudd_Regular(F[i]),support);
1048    }
1049    for (i = 0; i < n; i++) {
1050        ddClearFlag(Cudd_Regular(F[i]));
1051    }
1052
1053    /* Count vriables in support. */
1054    count = 0;
1055    for (i = 0; i < size; i++) {
1056        if (support[i] == 1) count++;
1057    }
1058
1059    FREE(support);
1060    return(count);
1061
1062} /* end of Cudd_VectorSupportSize */
1063
1064
1065/**Function********************************************************************
1066
1067  Synopsis    [Classifies the variables in the support of two DDs.]
1068
1069  Description [Classifies the variables in the support of two DDs
1070  <code>f</code> and <code>g</code>, depending on whther they appear
1071  in both DDs, only in <code>f</code>, or only in <code>g</code>.
1072  Returns 1 if successful; 0 otherwise.]
1073
1074  SideEffects [The cubes of the three classes of variables are
1075  returned as side effects.]
1076
1077  SeeAlso     [Cudd_Support Cudd_VectorSupport]
1078
1079******************************************************************************/
1080int
1081Cudd_ClassifySupport(
1082  DdManager * dd /* manager */,
1083  DdNode * f /* first DD */,
1084  DdNode * g /* second DD */,
1085  DdNode ** common /* cube of shared variables */,
1086  DdNode ** onlyF /* cube of variables only in f */,
1087  DdNode ** onlyG /* cube of variables only in g */)
1088{
1089    int *supportF, *supportG;
1090    DdNode *tmp, *var;
1091    int i,j;
1092    int size;
1093
1094    /* Allocate and initialize support arrays for ddSupportStep. */
1095    size = ddMax(dd->size, dd->sizeZ);
1096    supportF = ALLOC(int,size);
1097    if (supportF == NULL) {
1098        dd->errorCode = CUDD_MEMORY_OUT;
1099        return(0);
1100    }
1101    supportG = ALLOC(int,size);
1102    if (supportG == NULL) {
1103        dd->errorCode = CUDD_MEMORY_OUT;
1104        FREE(supportF);
1105        return(0);
1106    }
1107    for (i = 0; i < size; i++) {
1108        supportF[i] = 0;
1109        supportG[i] = 0;
1110    }
1111
1112    /* Compute supports and clean up markers. */
1113    ddSupportStep(Cudd_Regular(f),supportF);
1114    ddClearFlag(Cudd_Regular(f));
1115    ddSupportStep(Cudd_Regular(g),supportG);
1116    ddClearFlag(Cudd_Regular(g));
1117
1118    /* Classify variables and create cubes. */
1119    *common = *onlyF = *onlyG = DD_ONE(dd);
1120    cuddRef(*common); cuddRef(*onlyF); cuddRef(*onlyG);
1121    for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
1122        i = (j >= dd->size) ? j : dd->invperm[j];
1123        if (supportF[i] == 0 && supportG[i] == 0) continue;
1124        var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
1125        cuddRef(var);
1126        if (supportG[i] == 0) {
1127            tmp = Cudd_bddAnd(dd,*onlyF,var);
1128            if (tmp == NULL) {
1129                Cudd_RecursiveDeref(dd,*common);
1130                Cudd_RecursiveDeref(dd,*onlyF);
1131                Cudd_RecursiveDeref(dd,*onlyG);
1132                Cudd_RecursiveDeref(dd,var);
1133                FREE(supportF); FREE(supportG);
1134                return(0);
1135            }
1136            cuddRef(tmp);
1137            Cudd_RecursiveDeref(dd,*onlyF);
1138            *onlyF = tmp;
1139        } else if (supportF[i] == 0) {
1140            tmp = Cudd_bddAnd(dd,*onlyG,var);
1141            if (tmp == NULL) {
1142                Cudd_RecursiveDeref(dd,*common);
1143                Cudd_RecursiveDeref(dd,*onlyF);
1144                Cudd_RecursiveDeref(dd,*onlyG);
1145                Cudd_RecursiveDeref(dd,var);
1146                FREE(supportF); FREE(supportG);
1147                return(0);
1148            }
1149            cuddRef(tmp);
1150            Cudd_RecursiveDeref(dd,*onlyG);
1151            *onlyG = tmp;
1152        } else {
1153            tmp = Cudd_bddAnd(dd,*common,var);
1154            if (tmp == NULL) {
1155                Cudd_RecursiveDeref(dd,*common);
1156                Cudd_RecursiveDeref(dd,*onlyF);
1157                Cudd_RecursiveDeref(dd,*onlyG);
1158                Cudd_RecursiveDeref(dd,var);
1159                FREE(supportF); FREE(supportG);
1160                return(0);
1161            }
1162            cuddRef(tmp);
1163            Cudd_RecursiveDeref(dd,*common);
1164            *common = tmp;
1165        }
1166        Cudd_RecursiveDeref(dd,var);
1167    }
1168
1169    FREE(supportF); FREE(supportG);
1170    cuddDeref(*common); cuddDeref(*onlyF); cuddDeref(*onlyG);
1171    return(1);
1172
1173} /* end of Cudd_ClassifySupport */
1174
1175
1176/**Function********************************************************************
1177
1178  Synopsis    [Counts the number of leaves in a DD.]
1179
1180  Description [Counts the number of leaves in a DD. Returns the number
1181  of leaves in the DD rooted at node if successful; CUDD_OUT_OF_MEM
1182  otherwise.]
1183
1184  SideEffects [None]
1185
1186  SeeAlso     [Cudd_PrintDebug]
1187
1188******************************************************************************/
1189int
1190Cudd_CountLeaves(
1191  DdNode * node)
1192{
1193    int i;
1194
1195    i = ddLeavesInt(Cudd_Regular(node));
1196    ddClearFlag(Cudd_Regular(node));
1197    return(i);
1198
1199} /* end of Cudd_CountLeaves */
1200
1201
1202/**Function********************************************************************
1203
1204  Synopsis    [Picks one on-set cube randomly from the given DD.]
1205
1206  Description [Picks one on-set cube randomly from the given DD. The
1207  cube is written into an array of characters.  The array must have at
1208  least as many entries as there are variables. Returns 1 if
1209  successful; 0 otherwise.]
1210
1211  SideEffects [None]
1212
1213  SeeAlso     [Cudd_bddPickOneMinterm]
1214
1215******************************************************************************/
1216int
1217Cudd_bddPickOneCube(
1218  DdManager * ddm,
1219  DdNode * node,
1220  char * string)
1221{
1222    DdNode *N, *T, *E;
1223    DdNode *one, *bzero;
1224    char   dir;
1225    int    i;
1226
1227    if (string == NULL || node == NULL) return(0);
1228
1229    /* The constant 0 function has no on-set cubes. */
1230    one = DD_ONE(ddm);
1231    bzero = Cudd_Not(one);
1232    if (node == bzero) return(0);
1233
1234    for (i = 0; i < ddm->size; i++) string[i] = 2;
1235
1236    for (;;) {
1237
1238        if (node == one) break;
1239
1240        N = Cudd_Regular(node);
1241
1242        T = cuddT(N); E = cuddE(N);
1243        if (Cudd_IsComplement(node)) {
1244            T = Cudd_Not(T); E = Cudd_Not(E);
1245        }
1246        if (T == bzero) {
1247            string[N->index] = 0;
1248            node = E;
1249        } else if (E == bzero) {
1250            string[N->index] = 1;
1251            node = T;
1252        } else {
1253            dir = (char) ((Cudd_Random() & 0x2000) >> 13);
1254            string[N->index] = dir;
1255            node = dir ? T : E;
1256        }
1257    }
1258    return(1);
1259
1260} /* end of Cudd_bddPickOneCube */
1261
1262
1263/**Function********************************************************************
1264
1265  Synopsis    [Picks one on-set minterm randomly from the given DD.]
1266
1267  Description [Picks one on-set minterm randomly from the given
1268  DD. The minterm is in terms of <code>vars</code>. The array
1269  <code>vars</code> should contain at least all variables in the
1270  support of <code>f</code>; if this condition is not met the minterm
1271  built by this procedure may not be contained in
1272  <code>f</code>. Builds a BDD for the minterm and returns a pointer
1273  to it if successful; NULL otherwise. There are three reasons why the
1274  procedure may fail:
1275  <ul>
1276  <li> It may run out of memory;
1277  <li> the function <code>f</code> may be the constant 0;
1278  <li> the minterm may not be contained in <code>f</code>.
1279  </ul>]
1280
1281  SideEffects [None]
1282
1283  SeeAlso     [Cudd_bddPickOneCube]
1284
1285******************************************************************************/
1286DdNode *
1287Cudd_bddPickOneMinterm(
1288  DdManager * dd /* manager */,
1289  DdNode * f /* function from which to pick one minterm */,
1290  DdNode ** vars /* array of variables */,
1291  int  n /* size of <code>vars</code> */)
1292{
1293    char *string;
1294    int i, size;
1295    int *indices;
1296    int result;
1297    DdNode *old, *neW;
1298
1299    size = dd->size;
1300    string = ALLOC(char, size);
1301    if (string == NULL) {
1302        dd->errorCode = CUDD_MEMORY_OUT;
1303        return(NULL);
1304    }
1305    indices = ALLOC(int,n);
1306    if (indices == NULL) {
1307        dd->errorCode = CUDD_MEMORY_OUT;
1308        FREE(string);
1309        return(NULL);
1310    }
1311
1312    for (i = 0; i < n; i++) {
1313        indices[i] = vars[i]->index;
1314    }
1315
1316    result = Cudd_bddPickOneCube(dd,f,string);
1317    if (result == 0) {
1318        FREE(string);
1319        FREE(indices);
1320        return(NULL);
1321    }
1322
1323    /* Randomize choice for don't cares. */
1324    for (i = 0; i < n; i++) {
1325        if (string[indices[i]] == 2)
1326            string[indices[i]] = (char) ((Cudd_Random() & 0x20) >> 5);
1327    }
1328
1329    /* Build result BDD. */
1330    old = Cudd_ReadOne(dd);
1331    cuddRef(old);
1332
1333    for (i = n-1; i >= 0; i--) {
1334        neW = Cudd_bddAnd(dd,old,Cudd_NotCond(vars[i],string[indices[i]]==0));
1335        if (neW == NULL) {
1336            FREE(string);
1337            FREE(indices);
1338            Cudd_RecursiveDeref(dd,old);
1339            return(NULL);
1340        }
1341        cuddRef(neW);
1342        Cudd_RecursiveDeref(dd,old);
1343        old = neW;
1344    }
1345
1346#ifdef DD_DEBUG
1347    /* Test. */
1348    if (Cudd_bddLeq(dd,old,f)) {
1349        cuddDeref(old);
1350    } else {
1351        Cudd_RecursiveDeref(dd,old);
1352        old = NULL;
1353    }
1354#else
1355    cuddDeref(old);
1356#endif
1357
1358    FREE(string);
1359    FREE(indices);
1360    return(old);
1361
1362}  /* end of Cudd_bddPickOneMinterm */
1363
1364
1365/**Function********************************************************************
1366
1367  Synopsis    [Picks k on-set minterms evenly distributed from given DD.]
1368
1369  Description [Picks k on-set minterms evenly distributed from given DD.
1370  The minterms are in terms of <code>vars</code>. The array
1371  <code>vars</code> should contain at least all variables in the
1372  support of <code>f</code>; if this condition is not met the minterms
1373  built by this procedure may not be contained in
1374  <code>f</code>. Builds an array of BDDs for the minterms and returns a
1375  pointer to it if successful; NULL otherwise. There are three reasons
1376  why the procedure may fail:
1377  <ul>
1378  <li> It may run out of memory;
1379  <li> the function <code>f</code> may be the constant 0;
1380  <li> the minterms may not be contained in <code>f</code>.
1381  </ul>]
1382
1383  SideEffects [None]
1384
1385  SeeAlso     [Cudd_bddPickOneMinterm Cudd_bddPickOneCube]
1386
1387******************************************************************************/
1388DdNode **
1389Cudd_bddPickArbitraryMinterms(
1390  DdManager * dd /* manager */,
1391  DdNode * f /* function from which to pick k minterms */,
1392  DdNode ** vars /* array of variables */,
1393  int  n /* size of <code>vars</code> */,
1394  int  k /* number of minterms to find */)
1395{
1396    char **string;
1397    int i, j, l, size;
1398    int *indices;
1399    int result;
1400    DdNode **old, *neW;
1401    double minterms;
1402    char *saveString;
1403    int saveFlag, savePoint, isSame;
1404
1405    minterms = Cudd_CountMinterm(dd,f,n);
1406    if ((double)k > minterms) {
1407        return(NULL);
1408    }
1409
1410    size = dd->size;
1411    string = ALLOC(char *, k);
1412    if (string == NULL) {
1413        dd->errorCode = CUDD_MEMORY_OUT;
1414        return(NULL);
1415    }
1416    for (i = 0; i < k; i++) {
1417        string[i] = ALLOC(char, size + 1);
1418        if (string[i] == NULL) {
1419            for (j = 0; j < i; j++)
1420                FREE(string[i]);
1421            FREE(string);
1422            dd->errorCode = CUDD_MEMORY_OUT;
1423            return(NULL);
1424        }
1425        for (j = 0; j < size; j++) string[i][j] = '2';
1426        string[i][size] = '\0';
1427    }
1428    indices = ALLOC(int,n);
1429    if (indices == NULL) {
1430        dd->errorCode = CUDD_MEMORY_OUT;
1431        for (i = 0; i < k; i++)
1432            FREE(string[i]);
1433        FREE(string);
1434        return(NULL);
1435    }
1436
1437    for (i = 0; i < n; i++) {
1438        indices[i] = vars[i]->index;
1439    }
1440
1441    result = ddPickArbitraryMinterms(dd,f,n,k,string);
1442    if (result == 0) {
1443        for (i = 0; i < k; i++)
1444            FREE(string[i]);
1445        FREE(string);
1446        FREE(indices);
1447        return(NULL);
1448    }
1449
1450    old = ALLOC(DdNode *, k);
1451    if (old == NULL) {
1452        dd->errorCode = CUDD_MEMORY_OUT;
1453        for (i = 0; i < k; i++)
1454            FREE(string[i]);
1455        FREE(string);
1456        FREE(indices);
1457        return(NULL);
1458    }
1459    saveString = ALLOC(char, size + 1);
1460    if (saveString == NULL) {
1461        dd->errorCode = CUDD_MEMORY_OUT;
1462        for (i = 0; i < k; i++)
1463            FREE(string[i]);
1464        FREE(string);
1465        FREE(indices);
1466        FREE(old);
1467        return(NULL);
1468    }
1469    saveFlag = 0;
1470
1471    /* Build result BDD array. */
1472    for (i = 0; i < k; i++) {
1473        isSame = 0;
1474        if (!saveFlag) {
1475            for (j = i + 1; j < k; j++) {
1476                if (strcmp(string[i], string[j]) == 0) {
1477                    savePoint = i;
1478                    strcpy(saveString, string[i]);
1479                    saveFlag = 1;
1480                    break;
1481                }
1482            }
1483        } else {
1484            if (strcmp(string[i], saveString) == 0) {
1485                isSame = 1;
1486            } else {
1487                saveFlag = 0;
1488                for (j = i + 1; j < k; j++) {
1489                    if (strcmp(string[i], string[j]) == 0) {
1490                        savePoint = i;
1491                        strcpy(saveString, string[i]);
1492                        saveFlag = 1;
1493                        break;
1494                    }
1495                }
1496            }
1497        }
1498        /* Randomize choice for don't cares. */
1499        for (j = 0; j < n; j++) {
1500            if (string[i][indices[j]] == '2')
1501                string[i][indices[j]] =
1502                  (char) ((Cudd_Random() & 0x20) ? '1' : '0');
1503        }
1504
1505        while (isSame) {
1506            isSame = 0;
1507            for (j = savePoint; j < i; j++) {
1508                if (strcmp(string[i], string[j]) == 0) {
1509                    isSame = 1;
1510                    break;
1511                }
1512            }
1513            if (isSame) {
1514                strcpy(string[i], saveString);
1515                /* Randomize choice for don't cares. */
1516                for (j = 0; j < n; j++) {
1517                    if (string[i][indices[j]] == '2')
1518                        string[i][indices[j]] =
1519                          (char) ((Cudd_Random() & 0x20) ? '1' : '0');
1520                }
1521            }
1522        }
1523
1524        old[i] = Cudd_ReadOne(dd);
1525        cuddRef(old[i]);
1526
1527        for (j = 0; j < n; j++) {
1528            if (string[i][indices[j]] == '0') {
1529                neW = Cudd_bddAnd(dd,old[i],Cudd_Not(vars[j]));
1530            } else {
1531                neW = Cudd_bddAnd(dd,old[i],vars[j]);
1532            }
1533            if (neW == NULL) {
1534                FREE(saveString);
1535                for (l = 0; l < k; l++)
1536                    FREE(string[l]);
1537                FREE(string);
1538                FREE(indices);
1539                for (l = 0; l <= i; l++)
1540                    Cudd_RecursiveDeref(dd,old[l]);
1541                FREE(old);
1542                return(NULL);
1543            }
1544            cuddRef(neW);
1545            Cudd_RecursiveDeref(dd,old[i]);
1546            old[i] = neW;
1547        }
1548
1549        /* Test. */
1550        if (!Cudd_bddLeq(dd,old[i],f)) {
1551            FREE(saveString);
1552            for (l = 0; l < k; l++)
1553                FREE(string[l]);
1554            FREE(string);
1555            FREE(indices);
1556            for (l = 0; l <= i; l++)
1557                Cudd_RecursiveDeref(dd,old[l]);
1558            FREE(old);
1559            return(NULL);
1560        }
1561    }
1562
1563    FREE(saveString);
1564    for (i = 0; i < k; i++) {
1565        cuddDeref(old[i]);
1566        FREE(string[i]);
1567    }
1568    FREE(string);
1569    FREE(indices);
1570    return(old);
1571
1572}  /* end of Cudd_bddPickArbitraryMinterms */
1573
1574
1575/**Function********************************************************************
1576
1577  Synopsis    [Extracts a subset from a BDD.]
1578
1579  Description [Extracts a subset from a BDD in the following procedure.
1580  1. Compute the weight for each mask variable by counting the number of
1581     minterms for both positive and negative cofactors of the BDD with
1582     respect to each mask variable. (weight = #positive - #negative)
1583  2. Find a representative cube of the BDD by using the weight. From the
1584     top variable of the BDD, for each variable, if the weight is greater
1585     than 0.0, choose THEN branch, othereise ELSE branch, until meeting
1586     the constant 1.
1587  3. Quantify out the variables not in maskVars from the representative
1588     cube and if a variable in maskVars is don't care, replace the
1589     variable with a constant(1 or 0) depending on the weight.
1590  4. Make a subset of the BDD by multiplying with the modified cube.]
1591
1592  SideEffects [None]
1593
1594  SeeAlso     []
1595
1596******************************************************************************/
1597DdNode *
1598Cudd_SubsetWithMaskVars(
1599  DdManager * dd /* manager */,
1600  DdNode * f /* function from which to pick a cube */,
1601  DdNode ** vars /* array of variables */,
1602  int  nvars /* size of <code>vars</code> */,
1603  DdNode ** maskVars /* array of variables */,
1604  int  mvars /* size of <code>maskVars</code> */)
1605{
1606    double      *weight;
1607    char        *string;
1608    int         i, size;
1609    int         *indices, *mask;
1610    int         result;
1611    DdNode      *zero, *cube, *newCube, *subset;
1612    DdNode      *cof;
1613
1614    DdNode      *support;
1615    support = Cudd_Support(dd,f);
1616    cuddRef(support);
1617    Cudd_RecursiveDeref(dd,support);
1618
1619    zero = Cudd_Not(dd->one);
1620    size = dd->size;
1621
1622    weight = ALLOC(double,size);
1623    if (weight == NULL) {
1624        dd->errorCode = CUDD_MEMORY_OUT;
1625        return(NULL);
1626    }
1627    for (i = 0; i < size; i++) {
1628        weight[i] = 0.0;
1629    }
1630    for (i = 0; i < mvars; i++) {
1631        cof = Cudd_Cofactor(dd, f, maskVars[i]);
1632        cuddRef(cof);
1633        weight[i] = Cudd_CountMinterm(dd, cof, nvars);
1634        Cudd_RecursiveDeref(dd,cof);
1635
1636        cof = Cudd_Cofactor(dd, f, Cudd_Not(maskVars[i]));
1637        cuddRef(cof);
1638        weight[i] -= Cudd_CountMinterm(dd, cof, nvars);
1639        Cudd_RecursiveDeref(dd,cof);
1640    }
1641
1642    string = ALLOC(char, size + 1);
1643    if (string == NULL) {
1644        dd->errorCode = CUDD_MEMORY_OUT;
1645        FREE(weight);
1646        return(NULL);
1647    }
1648    mask = ALLOC(int, size);
1649    if (mask == NULL) {
1650        dd->errorCode = CUDD_MEMORY_OUT;
1651        FREE(weight);
1652        FREE(string);
1653        return(NULL);
1654    }
1655    for (i = 0; i < size; i++) {
1656        string[i] = '2';
1657        mask[i] = 0;
1658    }
1659    string[size] = '\0';
1660    indices = ALLOC(int,nvars);
1661    if (indices == NULL) {
1662        dd->errorCode = CUDD_MEMORY_OUT;
1663        FREE(weight);
1664        FREE(string);
1665        FREE(mask);
1666        return(NULL);
1667    }
1668    for (i = 0; i < nvars; i++) {
1669        indices[i] = vars[i]->index;
1670    }
1671
1672    result = ddPickRepresentativeCube(dd,f,weight,string);
1673    if (result == 0) {
1674        FREE(weight);
1675        FREE(string);
1676        FREE(mask);
1677        FREE(indices);
1678        return(NULL);
1679    }
1680
1681    cube = Cudd_ReadOne(dd);
1682    cuddRef(cube);
1683    zero = Cudd_Not(Cudd_ReadOne(dd));
1684    for (i = 0; i < nvars; i++) {
1685        if (string[indices[i]] == '0') {
1686            newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
1687        } else if (string[indices[i]] == '1') {
1688            newCube = Cudd_bddIte(dd,cube,vars[i],zero);
1689        } else
1690            continue;
1691        if (newCube == NULL) {
1692            FREE(weight);
1693            FREE(string);
1694            FREE(mask);
1695            FREE(indices);
1696            Cudd_RecursiveDeref(dd,cube);
1697            return(NULL);
1698        }
1699        cuddRef(newCube);
1700        Cudd_RecursiveDeref(dd,cube);
1701        cube = newCube;
1702    }
1703    Cudd_RecursiveDeref(dd,cube);
1704
1705    for (i = 0; i < mvars; i++) {
1706        mask[maskVars[i]->index] = 1;
1707    }
1708    for (i = 0; i < nvars; i++) {
1709        if (mask[indices[i]]) {
1710            if (string[indices[i]] == '2') {
1711                if (weight[indices[i]] >= 0.0)
1712                    string[indices[i]] = '1';
1713                else
1714                    string[indices[i]] = '0';
1715            }
1716        } else {
1717            string[indices[i]] = '2';
1718        }
1719    }
1720
1721    cube = Cudd_ReadOne(dd);
1722    cuddRef(cube);
1723    zero = Cudd_Not(Cudd_ReadOne(dd));
1724
1725    /* Build result BDD. */
1726    for (i = 0; i < nvars; i++) {
1727        if (string[indices[i]] == '0') {
1728            newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
1729        } else if (string[indices[i]] == '1') {
1730            newCube = Cudd_bddIte(dd,cube,vars[i],zero);
1731        } else
1732            continue;
1733        if (newCube == NULL) {
1734            FREE(weight);
1735            FREE(string);
1736            FREE(mask);
1737            FREE(indices);
1738            Cudd_RecursiveDeref(dd,cube);
1739            return(NULL);
1740        }
1741        cuddRef(newCube);
1742        Cudd_RecursiveDeref(dd,cube);
1743        cube = newCube;
1744    }
1745
1746    subset = Cudd_bddAnd(dd,f,cube);
1747    cuddRef(subset);
1748    Cudd_RecursiveDeref(dd,cube);
1749
1750    /* Test. */
1751    if (Cudd_bddLeq(dd,subset,f)) {
1752        cuddDeref(subset);
1753    } else {
1754        Cudd_RecursiveDeref(dd,subset);
1755        subset = NULL;
1756    }
1757
1758    FREE(weight);
1759    FREE(string);
1760    FREE(mask);
1761    FREE(indices);
1762    return(subset);
1763
1764} /* end of Cudd_SubsetWithMaskVars */
1765
1766
1767/**Function********************************************************************
1768
1769  Synopsis    [Finds the first cube of a decision diagram.]
1770
1771  Description [Defines an iterator on the onset of a decision diagram
1772  and finds its first cube. Returns a generator that contains the
1773  information necessary to continue the enumeration if successful; NULL
1774  otherwise.<p>
1775  A cube is represented as an array of literals, which are integers in
1776  {0, 1, 2}; 0 represents a complemented literal, 1 represents an
1777  uncomplemented literal, and 2 stands for don't care. The enumeration
1778  produces a disjoint cover of the function associated with the diagram.
1779  The size of the array equals the number of variables in the manager at
1780  the time Cudd_FirstCube is called.<p>
1781  For each cube, a value is also returned. This value is always 1 for a
1782  BDD, while it may be different from 1 for an ADD.
1783  For BDDs, the offset is the set of cubes whose value is the logical zero.
1784  For ADDs, the offset is the set of cubes whose value is the
1785  background value. The cubes of the offset are not enumerated.]
1786
1787  SideEffects [The first cube and its value are returned as side effects.]
1788
1789  SeeAlso     [Cudd_ForeachCube Cudd_NextCube Cudd_GenFree Cudd_IsGenEmpty
1790  Cudd_FirstNode]
1791
1792******************************************************************************/
1793DdGen *
1794Cudd_FirstCube(
1795  DdManager * dd,
1796  DdNode * f,
1797  int ** cube,
1798  CUDD_VALUE_TYPE * value)
1799{
1800    DdGen *gen;
1801    DdNode *top, *treg, *next, *nreg, *prev, *preg;
1802    int i;
1803    int nvars;
1804
1805    /* Sanity Check. */
1806    if (dd == NULL || f == NULL) return(NULL);
1807
1808    /* Allocate generator an initialize it. */
1809    gen = ALLOC(DdGen,1);
1810    if (gen == NULL) {
1811        dd->errorCode = CUDD_MEMORY_OUT;
1812        return(NULL);
1813    }
1814
1815    gen->manager = dd;
1816    gen->type = CUDD_GEN_CUBES;
1817    gen->status = CUDD_GEN_EMPTY;
1818    gen->gen.cubes.cube = NULL;
1819    gen->gen.cubes.value = DD_ZERO_VAL;
1820    gen->stack.sp = 0;
1821    gen->stack.stack = NULL;
1822    gen->node = NULL;
1823
1824    nvars = dd->size;
1825    gen->gen.cubes.cube = ALLOC(int,nvars);
1826    if (gen->gen.cubes.cube == NULL) {
1827        dd->errorCode = CUDD_MEMORY_OUT;
1828        FREE(gen);
1829        return(NULL);
1830    }
1831    for (i = 0; i < nvars; i++) gen->gen.cubes.cube[i] = 2;
1832
1833    /* The maximum stack depth is one plus the number of variables.
1834    ** because a path may have nodes at all levels, including the
1835    ** constant level.
1836    */
1837    gen->stack.stack = ALLOC(DdNodePtr, nvars+1);
1838    if (gen->stack.stack == NULL) {
1839        dd->errorCode = CUDD_MEMORY_OUT;
1840        FREE(gen->gen.cubes.cube);
1841        FREE(gen);
1842        return(NULL);
1843    }
1844    for (i = 0; i <= nvars; i++) gen->stack.stack[i] = NULL;
1845
1846    /* Find the first cube of the onset. */
1847    gen->stack.stack[gen->stack.sp] = f; gen->stack.sp++;
1848
1849    while (1) {
1850        top = gen->stack.stack[gen->stack.sp-1];
1851        treg = Cudd_Regular(top);
1852        if (!cuddIsConstant(treg)) {
1853            /* Take the else branch first. */
1854            gen->gen.cubes.cube[treg->index] = 0;
1855            next = cuddE(treg);
1856            if (top != treg) next = Cudd_Not(next);
1857            gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
1858        } else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) {
1859            /* Backtrack */
1860            while (1) {
1861                if (gen->stack.sp == 1) {
1862                    /* The current node has no predecessor. */
1863                    gen->status = CUDD_GEN_EMPTY;
1864                    gen->stack.sp--;
1865                    goto done;
1866                }
1867                prev = gen->stack.stack[gen->stack.sp-2];
1868                preg = Cudd_Regular(prev);
1869                nreg = cuddT(preg);
1870                if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
1871                if (next != top) { /* follow the then branch next */
1872                    gen->gen.cubes.cube[preg->index] = 1;
1873                    gen->stack.stack[gen->stack.sp-1] = next;
1874                    break;
1875                }
1876                /* Pop the stack and try again. */
1877                gen->gen.cubes.cube[preg->index] = 2;
1878                gen->stack.sp--;
1879                top = gen->stack.stack[gen->stack.sp-1];
1880                treg = Cudd_Regular(top);
1881            }
1882        } else {
1883            gen->status = CUDD_GEN_NONEMPTY;
1884            gen->gen.cubes.value = cuddV(top);
1885            goto done;
1886        }
1887    }
1888
1889done:
1890    *cube = gen->gen.cubes.cube;
1891    *value = gen->gen.cubes.value;
1892    return(gen);
1893
1894} /* end of Cudd_FirstCube */
1895
1896
1897/**Function********************************************************************
1898
1899  Synopsis    [Generates the next cube of a decision diagram onset.]
1900
1901  Description [Generates the next cube of a decision diagram onset,
1902  using generator gen. Returns 0 if the enumeration is completed; 1
1903  otherwise.]
1904
1905  SideEffects [The cube and its value are returned as side effects. The
1906  generator is modified.]
1907
1908  SeeAlso     [Cudd_ForeachCube Cudd_FirstCube Cudd_GenFree Cudd_IsGenEmpty
1909  Cudd_NextNode]
1910
1911******************************************************************************/
1912int
1913Cudd_NextCube(
1914  DdGen * gen,
1915  int ** cube,
1916  CUDD_VALUE_TYPE * value)
1917{
1918    DdNode *top, *treg, *next, *nreg, *prev, *preg;
1919    DdManager *dd = gen->manager;
1920
1921    /* Backtrack from previously reached terminal node. */
1922    while (1) {
1923        if (gen->stack.sp == 1) {
1924            /* The current node has no predecessor. */
1925            gen->status = CUDD_GEN_EMPTY;
1926            gen->stack.sp--;
1927            goto done;
1928        }
1929        top = gen->stack.stack[gen->stack.sp-1];
1930        treg = Cudd_Regular(top);
1931        prev = gen->stack.stack[gen->stack.sp-2];
1932        preg = Cudd_Regular(prev);
1933        nreg = cuddT(preg);
1934        if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
1935        if (next != top) { /* follow the then branch next */
1936            gen->gen.cubes.cube[preg->index] = 1;
1937            gen->stack.stack[gen->stack.sp-1] = next;
1938            break;
1939        }
1940        /* Pop the stack and try again. */
1941        gen->gen.cubes.cube[preg->index] = 2;
1942        gen->stack.sp--;
1943    }
1944
1945    while (1) {
1946        top = gen->stack.stack[gen->stack.sp-1];
1947        treg = Cudd_Regular(top);
1948        if (!cuddIsConstant(treg)) {
1949            /* Take the else branch first. */
1950            gen->gen.cubes.cube[treg->index] = 0;
1951            next = cuddE(treg);
1952            if (top != treg) next = Cudd_Not(next);
1953            gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
1954        } else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) {
1955            /* Backtrack */
1956            while (1) {
1957                if (gen->stack.sp == 1) {
1958                    /* The current node has no predecessor. */
1959                    gen->status = CUDD_GEN_EMPTY;
1960                    gen->stack.sp--;
1961                    goto done;
1962                }
1963                prev = gen->stack.stack[gen->stack.sp-2];
1964                preg = Cudd_Regular(prev);
1965                nreg = cuddT(preg);
1966                if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
1967                if (next != top) { /* follow the then branch next */
1968                    gen->gen.cubes.cube[preg->index] = 1;
1969                    gen->stack.stack[gen->stack.sp-1] = next;
1970                    break;
1971                }
1972                /* Pop the stack and try again. */
1973                gen->gen.cubes.cube[preg->index] = 2;
1974                gen->stack.sp--;
1975                top = gen->stack.stack[gen->stack.sp-1];
1976                treg = Cudd_Regular(top);
1977            }
1978        } else {
1979            gen->status = CUDD_GEN_NONEMPTY;
1980            gen->gen.cubes.value = cuddV(top);
1981            goto done;
1982        }
1983    }
1984
1985done:
1986    if (gen->status == CUDD_GEN_EMPTY) return(0);
1987    *cube = gen->gen.cubes.cube;
1988    *value = gen->gen.cubes.value;
1989    return(1);
1990
1991} /* end of Cudd_NextCube */
1992
1993
1994/**Function********************************************************************
1995
1996  Synopsis    [Finds the first prime of a Boolean function.]
1997
1998  Description [Defines an iterator on a pair of BDDs describing a
1999  (possibly incompletely specified) Boolean functions and finds the
2000  first cube of a cover of the function.  Returns a generator
2001  that contains the information necessary to continue the enumeration
2002  if successful; NULL otherwise.<p>
2003
2004  The two argument BDDs are the lower and upper bounds of an interval.
2005  It is a mistake to call this function with a lower bound that is not
2006  less than or equal to the upper bound.<p>
2007
2008  A cube is represented as an array of literals, which are integers in
2009  {0, 1, 2}; 0 represents a complemented literal, 1 represents an
2010  uncomplemented literal, and 2 stands for don't care. The enumeration
2011  produces a prime and irredundant cover of the function associated
2012  with the two BDDs.  The size of the array equals the number of
2013  variables in the manager at the time Cudd_FirstCube is called.<p>
2014
2015  This iterator can only be used on BDDs.]
2016
2017  SideEffects [The first cube is returned as side effect.]
2018
2019  SeeAlso     [Cudd_ForeachPrime Cudd_NextPrime Cudd_GenFree Cudd_IsGenEmpty
2020  Cudd_FirstCube Cudd_FirstNode]
2021
2022******************************************************************************/
2023DdGen *
2024Cudd_FirstPrime(
2025  DdManager *dd,
2026  DdNode *l,
2027  DdNode *u,
2028  int **cube)
2029{
2030    DdGen *gen;
2031    DdNode *implicant, *prime, *tmp;
2032    int length, result;
2033
2034    /* Sanity Check. */
2035    if (dd == NULL || l == NULL || u == NULL) return(NULL);
2036
2037    /* Allocate generator an initialize it. */
2038    gen = ALLOC(DdGen,1);
2039    if (gen == NULL) {
2040        dd->errorCode = CUDD_MEMORY_OUT;
2041        return(NULL);
2042    }
2043
2044    gen->manager = dd;
2045    gen->type = CUDD_GEN_PRIMES;
2046    gen->status = CUDD_GEN_EMPTY;
2047    gen->gen.primes.cube = NULL;
2048    gen->gen.primes.ub = u;
2049    gen->stack.sp = 0;
2050    gen->stack.stack = NULL;
2051    gen->node = l;
2052    cuddRef(l);
2053
2054    gen->gen.primes.cube = ALLOC(int,dd->size);
2055    if (gen->gen.primes.cube == NULL) {
2056        dd->errorCode = CUDD_MEMORY_OUT;
2057        FREE(gen);
2058        return(NULL);
2059    }
2060
2061    if (gen->node == Cudd_ReadLogicZero(dd)) {
2062        gen->status = CUDD_GEN_EMPTY;
2063    } else {
2064        implicant = Cudd_LargestCube(dd,gen->node,&length);
2065        if (implicant == NULL) {
2066            Cudd_RecursiveDeref(dd,gen->node);
2067            FREE(gen->gen.primes.cube);
2068            FREE(gen);
2069            return(NULL);
2070        }
2071        cuddRef(implicant);
2072        prime = Cudd_bddMakePrime(dd,implicant,gen->gen.primes.ub);
2073        if (prime == NULL) {
2074            Cudd_RecursiveDeref(dd,gen->node);
2075            Cudd_RecursiveDeref(dd,implicant);
2076            FREE(gen->gen.primes.cube);
2077            FREE(gen);
2078            return(NULL);
2079        }
2080        cuddRef(prime);
2081        Cudd_RecursiveDeref(dd,implicant);
2082        tmp = Cudd_bddAnd(dd,gen->node,Cudd_Not(prime));
2083        if (tmp == NULL) {
2084            Cudd_RecursiveDeref(dd,gen->node);
2085            Cudd_RecursiveDeref(dd,prime);
2086            FREE(gen->gen.primes.cube);
2087            FREE(gen);
2088            return(NULL);
2089        }
2090        cuddRef(tmp);
2091        Cudd_RecursiveDeref(dd,gen->node);
2092        gen->node = tmp;
2093        result = Cudd_BddToCubeArray(dd,prime,gen->gen.primes.cube);
2094        if (result == 0) {
2095            Cudd_RecursiveDeref(dd,gen->node);
2096            Cudd_RecursiveDeref(dd,prime);
2097            FREE(gen->gen.primes.cube);
2098            FREE(gen);
2099            return(NULL);
2100        }
2101        Cudd_RecursiveDeref(dd,prime);
2102        gen->status = CUDD_GEN_NONEMPTY;
2103    }
2104    *cube = gen->gen.primes.cube;
2105    return(gen);
2106
2107} /* end of Cudd_FirstPrime */
2108
2109
2110/**Function********************************************************************
2111
2112  Synopsis    [Generates the next prime of a Boolean function.]
2113
2114  Description [Generates the next cube of a Boolean function,
2115  using generator gen. Returns 0 if the enumeration is completed; 1
2116  otherwise.]
2117
2118  SideEffects [The cube and is returned as side effects. The
2119  generator is modified.]
2120
2121  SeeAlso     [Cudd_ForeachPrime Cudd_FirstPrime Cudd_GenFree Cudd_IsGenEmpty
2122  Cudd_NextCube Cudd_NextNode]
2123
2124******************************************************************************/
2125int
2126Cudd_NextPrime(
2127  DdGen *gen,
2128  int **cube)
2129{
2130    DdNode *implicant, *prime, *tmp;
2131    DdManager *dd = gen->manager;
2132    int length, result;
2133
2134    if (gen->node == Cudd_ReadLogicZero(dd)) {
2135        gen->status = CUDD_GEN_EMPTY;
2136    } else {
2137        implicant = Cudd_LargestCube(dd,gen->node,&length);
2138        if (implicant == NULL) {
2139            gen->status = CUDD_GEN_EMPTY;
2140            return(0);
2141        }
2142        cuddRef(implicant);
2143        prime = Cudd_bddMakePrime(dd,implicant,gen->gen.primes.ub);
2144        if (prime == NULL) {
2145            Cudd_RecursiveDeref(dd,implicant);
2146            gen->status = CUDD_GEN_EMPTY;
2147            return(0);
2148        }
2149        cuddRef(prime);
2150        Cudd_RecursiveDeref(dd,implicant);
2151        tmp = Cudd_bddAnd(dd,gen->node,Cudd_Not(prime));
2152        if (tmp == NULL) {
2153            Cudd_RecursiveDeref(dd,prime);
2154            gen->status = CUDD_GEN_EMPTY;
2155            return(0);
2156        }
2157        cuddRef(tmp);
2158        Cudd_RecursiveDeref(dd,gen->node);
2159        gen->node = tmp;
2160        result = Cudd_BddToCubeArray(dd,prime,gen->gen.primes.cube);
2161        if (result == 0) {
2162            Cudd_RecursiveDeref(dd,prime);
2163            gen->status = CUDD_GEN_EMPTY;
2164            return(0);
2165        }
2166        Cudd_RecursiveDeref(dd,prime);
2167        gen->status = CUDD_GEN_NONEMPTY;
2168    }
2169    if (gen->status == CUDD_GEN_EMPTY) return(0);
2170    *cube = gen->gen.primes.cube;
2171    return(1);
2172
2173} /* end of Cudd_NextPrime */
2174
2175
2176/**Function********************************************************************
2177
2178  Synopsis    [Computes the cube of an array of BDD variables.]
2179
2180  Description [Computes the cube of an array of BDD variables. If
2181  non-null, the phase argument indicates which literal of each
2182  variable should appear in the cube. If phase\[i\] is nonzero, then the
2183  positive literal is used. If phase is NULL, the cube is positive unate.
2184  Returns a pointer to the result if successful; NULL otherwise.]
2185
2186  SideEffects [None]
2187
2188  SeeAlso     [Cudd_addComputeCube Cudd_IndicesToCube Cudd_CubeArrayToBdd]
2189
2190******************************************************************************/
2191DdNode *
2192Cudd_bddComputeCube(
2193  DdManager * dd,
2194  DdNode ** vars,
2195  int * phase,
2196  int  n)
2197{
2198    DdNode      *cube;
2199    DdNode      *fn;
2200    int         i;
2201
2202    cube = DD_ONE(dd);
2203    cuddRef(cube);
2204
2205    for (i = n - 1; i >= 0; i--) {
2206        if (phase == NULL || phase[i] != 0) {
2207            fn = Cudd_bddAnd(dd,vars[i],cube);
2208        } else {
2209            fn = Cudd_bddAnd(dd,Cudd_Not(vars[i]),cube);
2210        }
2211        if (fn == NULL) {
2212            Cudd_RecursiveDeref(dd,cube);
2213            return(NULL);
2214        }
2215        cuddRef(fn);
2216        Cudd_RecursiveDeref(dd,cube);
2217        cube = fn;
2218    }
2219    cuddDeref(cube);
2220
2221    return(cube);
2222
2223}  /* end of Cudd_bddComputeCube */
2224
2225
2226/**Function********************************************************************
2227
2228  Synopsis    [Computes the cube of an array of ADD variables.]
2229
2230  Description [Computes the cube of an array of ADD variables.  If
2231  non-null, the phase argument indicates which literal of each
2232  variable should appear in the cube. If phase\[i\] is nonzero, then the
2233  positive literal is used. If phase is NULL, the cube is positive unate.
2234  Returns a pointer to the result if successful; NULL otherwise.]
2235
2236  SideEffects [none]
2237
2238  SeeAlso     [Cudd_bddComputeCube]
2239
2240******************************************************************************/
2241DdNode *
2242Cudd_addComputeCube(
2243  DdManager * dd,
2244  DdNode ** vars,
2245  int * phase,
2246  int  n)
2247{
2248    DdNode      *cube, *zero;
2249    DdNode      *fn;
2250    int         i;
2251
2252    cube = DD_ONE(dd);
2253    cuddRef(cube);
2254    zero = DD_ZERO(dd);
2255
2256    for (i = n - 1; i >= 0; i--) {
2257        if (phase == NULL || phase[i] != 0) {
2258            fn = Cudd_addIte(dd,vars[i],cube,zero);
2259        } else {
2260            fn = Cudd_addIte(dd,vars[i],zero,cube);
2261        }
2262        if (fn == NULL) {
2263            Cudd_RecursiveDeref(dd,cube);
2264            return(NULL);
2265        }
2266        cuddRef(fn);
2267        Cudd_RecursiveDeref(dd,cube);
2268        cube = fn;
2269    }
2270    cuddDeref(cube);
2271
2272    return(cube);
2273
2274} /* end of Cudd_addComputeCube */
2275
2276
2277/**Function********************************************************************
2278
2279  Synopsis    [Builds the BDD of a cube from a positional array.]
2280
2281  Description [Builds a cube from a positional array.  The array must
2282  have one integer entry for each BDD variable.  If the i-th entry is
2283  1, the variable of index i appears in true form in the cube; If the
2284  i-th entry is 0, the variable of index i appears complemented in the
2285  cube; otherwise the variable does not appear in the cube.  Returns a
2286  pointer to the BDD for the cube if successful; NULL otherwise.]
2287
2288  SideEffects [None]
2289
2290  SeeAlso     [Cudd_bddComputeCube Cudd_IndicesToCube Cudd_BddToCubeArray]
2291
2292******************************************************************************/
2293DdNode *
2294Cudd_CubeArrayToBdd(
2295  DdManager *dd,
2296  int *array)
2297{
2298    DdNode *cube, *var, *tmp;
2299    int i;
2300    int size = Cudd_ReadSize(dd);
2301
2302    cube = DD_ONE(dd);
2303    cuddRef(cube);
2304    for (i = size - 1; i >= 0; i--) {
2305        if ((array[i] & ~1) == 0) {
2306            var = Cudd_bddIthVar(dd,i);
2307            tmp = Cudd_bddAnd(dd,cube,Cudd_NotCond(var,array[i]==0));
2308            if (tmp == NULL) {
2309                Cudd_RecursiveDeref(dd,cube);
2310                return(NULL);
2311            }
2312            cuddRef(tmp);
2313            Cudd_RecursiveDeref(dd,cube);
2314            cube = tmp;
2315        }
2316    }
2317    cuddDeref(cube);
2318    return(cube);
2319
2320} /* end of Cudd_CubeArrayToBdd */
2321
2322
2323/**Function********************************************************************
2324
2325  Synopsis    [Builds a positional array from the BDD of a cube.]
2326
2327  Description [Builds a positional array from the BDD of a cube.
2328  Array must have one entry for each BDD variable.  The positional
2329  array has 1 in i-th position if the variable of index i appears in
2330  true form in the cube; it has 0 in i-th position if the variable of
2331  index i appears in complemented form in the cube; finally, it has 2
2332  in i-th position if the variable of index i does not appear in the
2333  cube.  Returns 1 if successful (the BDD is indeed a cube); 0
2334  otherwise.]
2335
2336  SideEffects [The result is in the array passed by reference.]
2337
2338  SeeAlso     [Cudd_CubeArrayToBdd]
2339
2340******************************************************************************/
2341int
2342Cudd_BddToCubeArray(
2343  DdManager *dd,
2344  DdNode *cube,
2345  int *array)
2346{
2347    DdNode *scan, *t, *e;
2348    int i;
2349    int size = Cudd_ReadSize(dd);
2350    DdNode *zero = Cudd_Not(DD_ONE(dd));
2351
2352    for (i = size-1; i >= 0; i--) {
2353        array[i] = 2;
2354    }
2355    scan = cube;
2356    while (!Cudd_IsConstant(scan)) {
2357        int index = Cudd_Regular(scan)->index;
2358        cuddGetBranches(scan,&t,&e);
2359        if (t == zero) {
2360            array[index] = 0;
2361            scan = e;
2362        } else if (e == zero) {
2363            array[index] = 1;
2364            scan = t;
2365        } else {
2366            return(0);  /* cube is not a cube */
2367        }
2368    }
2369    if (scan == zero) {
2370        return(0);
2371    } else {
2372        return(1);
2373    }
2374
2375} /* end of Cudd_BddToCubeArray */
2376
2377
2378/**Function********************************************************************
2379
2380  Synopsis    [Finds the first node of a decision diagram.]
2381
2382  Description [Defines an iterator on the nodes of a decision diagram
2383  and finds its first node. Returns a generator that contains the
2384  information necessary to continue the enumeration if successful;
2385  NULL otherwise.  The nodes are enumerated in a reverse topological
2386  order, so that a node is always preceded in the enumeration by its
2387  descendants.]
2388
2389  SideEffects [The first node is returned as a side effect.]
2390
2391  SeeAlso     [Cudd_ForeachNode Cudd_NextNode Cudd_GenFree Cudd_IsGenEmpty
2392  Cudd_FirstCube]
2393
2394******************************************************************************/
2395DdGen *
2396Cudd_FirstNode(
2397  DdManager * dd,
2398  DdNode * f,
2399  DdNode ** node)
2400{
2401    DdGen *gen;
2402    int size;
2403
2404    /* Sanity Check. */
2405    if (dd == NULL || f == NULL) return(NULL);
2406
2407    /* Allocate generator an initialize it. */
2408    gen = ALLOC(DdGen,1);
2409    if (gen == NULL) {
2410        dd->errorCode = CUDD_MEMORY_OUT;
2411        return(NULL);
2412    }
2413
2414    gen->manager = dd;
2415    gen->type = CUDD_GEN_NODES;
2416    gen->status = CUDD_GEN_EMPTY;
2417    gen->stack.sp = 0;
2418    gen->node = NULL;
2419
2420    /* Collect all the nodes on the generator stack for later perusal. */
2421    gen->stack.stack = cuddNodeArray(Cudd_Regular(f), &size);
2422    if (gen->stack.stack == NULL) {
2423        FREE(gen);
2424        dd->errorCode = CUDD_MEMORY_OUT;
2425        return(NULL);
2426    }
2427    gen->gen.nodes.size = size;
2428
2429    /* Find the first node. */
2430    if (gen->stack.sp < gen->gen.nodes.size) {
2431        gen->status = CUDD_GEN_NONEMPTY;
2432        gen->node = gen->stack.stack[gen->stack.sp];
2433        *node = gen->node;
2434    }
2435
2436    return(gen);
2437
2438} /* end of Cudd_FirstNode */
2439
2440
2441/**Function********************************************************************
2442
2443  Synopsis    [Finds the next node of a decision diagram.]
2444
2445  Description [Finds the node of a decision diagram, using generator
2446  gen. Returns 0 if the enumeration is completed; 1 otherwise.]
2447
2448  SideEffects [The next node is returned as a side effect.]
2449
2450  SeeAlso     [Cudd_ForeachNode Cudd_FirstNode Cudd_GenFree Cudd_IsGenEmpty
2451  Cudd_NextCube]
2452
2453******************************************************************************/
2454int
2455Cudd_NextNode(
2456  DdGen * gen,
2457  DdNode ** node)
2458{
2459    /* Find the next node. */
2460    gen->stack.sp++;
2461    if (gen->stack.sp < gen->gen.nodes.size) {
2462        gen->node = gen->stack.stack[gen->stack.sp];
2463        *node = gen->node;
2464        return(1);
2465    } else {
2466        gen->status = CUDD_GEN_EMPTY;
2467        return(0);
2468    }
2469
2470} /* end of Cudd_NextNode */
2471
2472
2473/**Function********************************************************************
2474
2475  Synopsis    [Frees a CUDD generator.]
2476
2477  Description [Frees a CUDD generator. Always returns 0, so that it can
2478  be used in mis-like foreach constructs.]
2479
2480  SideEffects [None]
2481
2482  SeeAlso     [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube
2483  Cudd_FirstNode Cudd_NextNode Cudd_IsGenEmpty]
2484
2485******************************************************************************/
2486int
2487Cudd_GenFree(
2488  DdGen * gen)
2489{
2490    if (gen == NULL) return(0);
2491    switch (gen->type) {
2492    case CUDD_GEN_CUBES:
2493    case CUDD_GEN_ZDD_PATHS:
2494        FREE(gen->gen.cubes.cube);
2495        FREE(gen->stack.stack);
2496        break;
2497    case CUDD_GEN_PRIMES:
2498        FREE(gen->gen.primes.cube);
2499        Cudd_RecursiveDeref(gen->manager,gen->node);
2500        break;
2501    case CUDD_GEN_NODES:
2502        FREE(gen->stack.stack);
2503        break;
2504    default:
2505        return(0);
2506    }
2507    FREE(gen);
2508    return(0);
2509
2510} /* end of Cudd_GenFree */
2511
2512
2513/**Function********************************************************************
2514
2515  Synopsis    [Queries the status of a generator.]
2516
2517  Description [Queries the status of a generator. Returns 1 if the
2518  generator is empty or NULL; 0 otherswise.]
2519
2520  SideEffects [None]
2521
2522  SeeAlso     [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube
2523  Cudd_FirstNode Cudd_NextNode Cudd_GenFree]
2524
2525******************************************************************************/
2526int
2527Cudd_IsGenEmpty(
2528  DdGen * gen)
2529{
2530    if (gen == NULL) return(1);
2531    return(gen->status == CUDD_GEN_EMPTY);
2532
2533} /* end of Cudd_IsGenEmpty */
2534
2535
2536/**Function********************************************************************
2537
2538  Synopsis    [Builds a cube of BDD variables from an array of indices.]
2539
2540  Description [Builds a cube of BDD variables from an array of indices.
2541  Returns a pointer to the result if successful; NULL otherwise.]
2542
2543  SideEffects [None]
2544
2545  SeeAlso     [Cudd_bddComputeCube Cudd_CubeArrayToBdd]
2546
2547******************************************************************************/
2548DdNode *
2549Cudd_IndicesToCube(
2550  DdManager * dd,
2551  int * array,
2552  int  n)
2553{
2554    DdNode *cube, *tmp;
2555    int i;
2556
2557    cube = DD_ONE(dd);
2558    cuddRef(cube);
2559    for (i = n - 1; i >= 0; i--) {
2560        tmp = Cudd_bddAnd(dd,Cudd_bddIthVar(dd,array[i]),cube);
2561        if (tmp == NULL) {
2562            Cudd_RecursiveDeref(dd,cube);
2563            return(NULL);
2564        }
2565        cuddRef(tmp);
2566        Cudd_RecursiveDeref(dd,cube);
2567        cube = tmp;
2568    }
2569
2570    cuddDeref(cube);
2571    return(cube);
2572
2573} /* end of Cudd_IndicesToCube */
2574
2575
2576/**Function********************************************************************
2577
2578  Synopsis    [Prints the package version number.]
2579
2580  Description []
2581
2582  SideEffects [None]
2583
2584  SeeAlso     []
2585
2586******************************************************************************/
2587void
2588Cudd_PrintVersion(
2589  FILE * fp)
2590{
2591    (void) fprintf(fp, "%s\n", CUDD_VERSION);
2592
2593} /* end of Cudd_PrintVersion */
2594
2595
2596/**Function********************************************************************
2597
2598  Synopsis    [Computes the average distance between adjacent nodes.]
2599
2600  Description [Computes the average distance between adjacent nodes in
2601  the manager. Adjacent nodes are node pairs such that the second node
2602  is the then child, else child, or next node in the collision list.]
2603
2604  SideEffects [None]
2605
2606  SeeAlso     []
2607
2608******************************************************************************/
2609double
2610Cudd_AverageDistance(
2611  DdManager * dd)
2612{
2613    double tetotal, nexttotal;
2614    double tesubtotal, nextsubtotal;
2615    double temeasured, nextmeasured;
2616    int i, j;
2617    int slots, nvars;
2618    long diff;
2619    DdNode *scan;
2620    DdNodePtr *nodelist;
2621    DdNode *sentinel = &(dd->sentinel);
2622
2623    nvars = dd->size;
2624    if (nvars == 0) return(0.0);
2625
2626    /* Initialize totals. */
2627    tetotal = 0.0;
2628    nexttotal = 0.0;
2629    temeasured = 0.0;
2630    nextmeasured = 0.0;
2631
2632    /* Scan the variable subtables. */
2633    for (i = 0; i < nvars; i++) {
2634        nodelist = dd->subtables[i].nodelist;
2635        tesubtotal = 0.0;
2636        nextsubtotal = 0.0;
2637        slots = dd->subtables[i].slots;
2638        for (j = 0; j < slots; j++) {
2639            scan = nodelist[j];
2640            while (scan != sentinel) {
2641                diff = (long) scan - (long) cuddT(scan);
2642                tesubtotal += (double) ddAbs(diff);
2643                diff = (long) scan - (long) Cudd_Regular(cuddE(scan));
2644                tesubtotal += (double) ddAbs(diff);
2645                temeasured += 2.0;
2646                if (scan->next != sentinel) {
2647                    diff = (long) scan - (long) scan->next;
2648                    nextsubtotal += (double) ddAbs(diff);
2649                    nextmeasured += 1.0;
2650                }
2651                scan = scan->next;
2652            }
2653        }
2654        tetotal += tesubtotal;
2655        nexttotal += nextsubtotal;
2656    }
2657
2658    /* Scan the constant table. */
2659    nodelist = dd->constants.nodelist;
2660    nextsubtotal = 0.0;
2661    slots = dd->constants.slots;
2662    for (j = 0; j < slots; j++) {
2663        scan = nodelist[j];
2664        while (scan != NULL) {
2665            if (scan->next != NULL) {
2666                diff = (long) scan - (long) scan->next;
2667                nextsubtotal += (double) ddAbs(diff);
2668                nextmeasured += 1.0;
2669            }
2670            scan = scan->next;
2671        }
2672    }
2673    nexttotal += nextsubtotal;
2674
2675    return((tetotal + nexttotal) / (temeasured + nextmeasured));
2676
2677} /* end of Cudd_AverageDistance */
2678
2679
2680/**Function********************************************************************
2681
2682  Synopsis    [Portable random number generator.]
2683
2684  Description [Portable number generator based on ran2 from "Numerical
2685  Recipes in C." It is a long period (> 2 * 10^18) random number generator
2686  of L'Ecuyer with Bays-Durham shuffle. Returns a long integer uniformly
2687  distributed between 0 and 2147483561 (inclusive of the endpoint values).
2688  The random generator can be explicitly initialized by calling
2689  Cudd_Srandom. If no explicit initialization is performed, then the
2690  seed 1 is assumed.]
2691
2692  SideEffects [None]
2693
2694  SeeAlso     [Cudd_Srandom]
2695
2696******************************************************************************/
2697long
2698Cudd_Random(void)
2699{
2700    int i;      /* index in the shuffle table */
2701    long int w; /* work variable */
2702
2703    /* cuddRand == 0 if the geneartor has not been initialized yet. */
2704    if (cuddRand == 0) Cudd_Srandom(1);
2705
2706    /* Compute cuddRand = (cuddRand * LEQA1) % MODULUS1 avoiding
2707    ** overflows by Schrage's method.
2708    */
2709    w          = cuddRand / LEQQ1;
2710    cuddRand   = LEQA1 * (cuddRand - w * LEQQ1) - w * LEQR1;
2711    cuddRand  += (cuddRand < 0) * MODULUS1;
2712
2713    /* Compute cuddRand2 = (cuddRand2 * LEQA2) % MODULUS2 avoiding
2714    ** overflows by Schrage's method.
2715    */
2716    w          = cuddRand2 / LEQQ2;
2717    cuddRand2  = LEQA2 * (cuddRand2 - w * LEQQ2) - w * LEQR2;
2718    cuddRand2 += (cuddRand2 < 0) * MODULUS2;
2719
2720    /* cuddRand is shuffled with the Bays-Durham algorithm.
2721    ** shuffleSelect and cuddRand2 are combined to generate the output.
2722    */
2723
2724    /* Pick one element from the shuffle table; "i" will be in the range
2725    ** from 0 to STAB_SIZE-1.
2726    */
2727    i = (int) (shuffleSelect / STAB_DIV);
2728    /* Mix the element of the shuffle table with the current iterate of
2729    ** the second sub-generator, and replace the chosen element of the
2730    ** shuffle table with the current iterate of the first sub-generator.
2731    */
2732    shuffleSelect   = shuffleTable[i] - cuddRand2;
2733    shuffleTable[i] = cuddRand;
2734    shuffleSelect  += (shuffleSelect < 1) * (MODULUS1 - 1);
2735    /* Since shuffleSelect != 0, and we want to be able to return 0,
2736    ** here we subtract 1 before returning.
2737    */
2738    return(shuffleSelect - 1);
2739
2740} /* end of Cudd_Random */
2741
2742
2743/**Function********************************************************************
2744
2745  Synopsis    [Initializer for the portable random number generator.]
2746
2747  Description [Initializer for the portable number generator based on
2748  ran2 in "Numerical Recipes in C." The input is the seed for the
2749  generator. If it is negative, its absolute value is taken as seed.
2750  If it is 0, then 1 is taken as seed. The initialized sets up the two
2751  recurrences used to generate a long-period stream, and sets up the
2752  shuffle table.]
2753
2754  SideEffects [None]
2755
2756  SeeAlso     [Cudd_Random]
2757
2758******************************************************************************/
2759void
2760Cudd_Srandom(
2761  long  seed)
2762{
2763    int i;
2764
2765    if (seed < 0)       cuddRand = -seed;
2766    else if (seed == 0) cuddRand = 1;
2767    else                cuddRand = seed;
2768    cuddRand2 = cuddRand;
2769    /* Load the shuffle table (after 11 warm-ups). */
2770    for (i = 0; i < STAB_SIZE + 11; i++) {
2771        long int w;
2772        w = cuddRand / LEQQ1;
2773        cuddRand = LEQA1 * (cuddRand - w * LEQQ1) - w * LEQR1;
2774        cuddRand += (cuddRand < 0) * MODULUS1;
2775        shuffleTable[i % STAB_SIZE] = cuddRand;
2776    }
2777    shuffleSelect = shuffleTable[1 % STAB_SIZE];
2778
2779} /* end of Cudd_Srandom */
2780
2781
2782/**Function********************************************************************
2783
2784  Synopsis    [Computes the density of a BDD or ADD.]
2785
2786  Description [Computes the density of a BDD or ADD. The density is
2787  the ratio of the number of minterms to the number of nodes. If 0 is
2788  passed as number of variables, the number of variables existing in
2789  the manager is used. Returns the density if successful; (double)
2790  CUDD_OUT_OF_MEM otherwise.]
2791
2792  SideEffects [None]
2793
2794  SeeAlso     [Cudd_CountMinterm Cudd_DagSize]
2795
2796******************************************************************************/
2797double
2798Cudd_Density(
2799  DdManager * dd /* manager */,
2800  DdNode * f /* function whose density is sought */,
2801  int  nvars /* size of the support of f */)
2802{
2803    double minterms;
2804    int nodes;
2805    double density;
2806
2807    if (nvars == 0) nvars = dd->size;
2808    minterms = Cudd_CountMinterm(dd,f,nvars);
2809    if (minterms == (double) CUDD_OUT_OF_MEM) return(minterms);
2810    nodes = Cudd_DagSize(f);
2811    density = minterms / (double) nodes;
2812    return(density);
2813
2814} /* end of Cudd_Density */
2815
2816
2817/**Function********************************************************************
2818
2819  Synopsis    [Warns that a memory allocation failed.]
2820
2821  Description [Warns that a memory allocation failed.
2822  This function can be used as replacement of MMout_of_memory to prevent
2823  the safe_mem functions of the util package from exiting when malloc
2824  returns NULL. One possible use is in case of discretionary allocations;
2825  for instance, the allocation of memory to enlarge the computed table.]
2826
2827  SideEffects [None]
2828
2829  SeeAlso     []
2830
2831******************************************************************************/
2832void
2833Cudd_OutOfMem(
2834  long size /* size of the allocation that failed */)
2835{
2836    (void) fflush(stdout);
2837    (void) fprintf(stderr, "\nunable to allocate %ld bytes\n", size);
2838    return;
2839
2840} /* end of Cudd_OutOfMem */
2841
2842
2843/*---------------------------------------------------------------------------*/
2844/* Definition of internal functions                                          */
2845/*---------------------------------------------------------------------------*/
2846
2847
2848/**Function********************************************************************
2849
2850  Synopsis    [Prints a DD to the standard output. One line per node is
2851  printed.]
2852
2853  Description [Prints a DD to the standard output. One line per node is
2854  printed. Returns 1 if successful; 0 otherwise.]
2855
2856  SideEffects [None]
2857
2858  SeeAlso     [Cudd_PrintDebug]
2859
2860******************************************************************************/
2861int
2862cuddP(
2863  DdManager * dd,
2864  DdNode * f)
2865{
2866    int retval;
2867    st_table *table = st_init_table(st_ptrcmp,st_ptrhash);
2868
2869    if (table == NULL) return(0);
2870
2871    retval = dp2(dd,f,table);
2872    st_free_table(table);
2873    (void) fputc('\n',dd->out);
2874    return(retval);
2875
2876} /* end of cuddP */
2877
2878
2879/**Function********************************************************************
2880
2881  Synopsis [Frees the memory used to store the minterm counts recorded
2882  in the visited table.]
2883
2884  Description [Frees the memory used to store the minterm counts
2885  recorded in the visited table. Returns ST_CONTINUE.]
2886
2887  SideEffects [None]
2888
2889******************************************************************************/
2890enum st_retval
2891cuddStCountfree(
2892  char * key,
2893  char * value,
2894  char * arg)
2895{
2896    double      *d;
2897
2898    d = (double *)value;
2899    FREE(d);
2900    return(ST_CONTINUE);
2901
2902} /* end of cuddStCountfree */
2903
2904
2905/**Function********************************************************************
2906
2907  Synopsis    [Recursively collects all the nodes of a DD in a symbol
2908  table.]
2909
2910  Description [Traverses the DD f and collects all its nodes in a
2911  symbol table.  f is assumed to be a regular pointer and
2912  cuddCollectNodes guarantees this assumption in the recursive calls.
2913  Returns 1 in case of success; 0 otherwise.]
2914
2915  SideEffects [None]
2916
2917  SeeAlso     []
2918
2919******************************************************************************/
2920int
2921cuddCollectNodes(
2922  DdNode * f,
2923  st_table * visited)
2924{
2925    DdNode      *T, *E;
2926    int         retval;
2927
2928#ifdef DD_DEBUG
2929    assert(!Cudd_IsComplement(f));
2930#endif
2931
2932    /* If already visited, nothing to do. */
2933    if (st_is_member(visited, (char *) f) == 1)
2934        return(1);
2935
2936    /* Check for abnormal condition that should never happen. */
2937    if (f == NULL)
2938        return(0);
2939
2940    /* Mark node as visited. */
2941    if (st_add_direct(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
2942        return(0);
2943
2944    /* Check terminal case. */
2945    if (cuddIsConstant(f))
2946        return(1);
2947
2948    /* Recursive calls. */
2949    T = cuddT(f);
2950    retval = cuddCollectNodes(T,visited);
2951    if (retval != 1) return(retval);
2952    E = Cudd_Regular(cuddE(f));
2953    retval = cuddCollectNodes(E,visited);
2954    return(retval);
2955
2956} /* end of cuddCollectNodes */
2957
2958
2959/**Function********************************************************************
2960
2961  Synopsis    [Recursively collects all the nodes of a DD in an array.]
2962
2963  Description [Traverses the DD f and collects all its nodes in an array.
2964  The caller should free the array returned by cuddNodeArray.
2965  Returns a pointer to the array of nodes in case of success; NULL
2966  otherwise.  The nodes are collected in reverse topological order, so
2967  that a node is always preceded in the array by all its descendants.]
2968
2969  SideEffects [The number of nodes is returned as a side effect.]
2970
2971  SeeAlso     [Cudd_FirstNode]
2972
2973******************************************************************************/
2974DdNodePtr *
2975cuddNodeArray(
2976  DdNode *f,
2977  int *n)
2978{
2979    DdNodePtr *table;
2980    int size, retval;
2981
2982    size = ddDagInt(Cudd_Regular(f));
2983    table = ALLOC(DdNodePtr, size);
2984    if (table == NULL) {
2985        ddClearFlag(Cudd_Regular(f));
2986        return(NULL);
2987    }
2988
2989    retval = cuddNodeArrayRecur(f, table, 0);
2990    assert(retval == size);
2991
2992    *n = size;
2993    return(table);
2994
2995} /* cuddNodeArray */
2996
2997
2998/*---------------------------------------------------------------------------*/
2999/* Definition of static functions                                            */
3000/*---------------------------------------------------------------------------*/
3001
3002
3003/**Function********************************************************************
3004
3005  Synopsis    [Performs the recursive step of cuddP.]
3006
3007  Description [Performs the recursive step of cuddP. Returns 1 in case
3008  of success; 0 otherwise.]
3009
3010  SideEffects [None]
3011
3012******************************************************************************/
3013static int
3014dp2(
3015  DdManager *dd,
3016  DdNode * f,
3017  st_table * t)
3018{
3019    DdNode *g, *n, *N;
3020    int T,E;
3021
3022    if (f == NULL) {
3023        return(0);
3024    }
3025    g = Cudd_Regular(f);
3026    if (cuddIsConstant(g)) {
3027#if SIZEOF_VOID_P == 8
3028        (void) fprintf(dd->out,"ID = %c0x%lx\tvalue = %-9g\n", bang(f),
3029                (ptruint) g / (ptruint) sizeof(DdNode),cuddV(g));
3030#else
3031        (void) fprintf(dd->out,"ID = %c0x%x\tvalue = %-9g\n", bang(f),
3032                (ptruint) g / (ptruint) sizeof(DdNode),cuddV(g));
3033#endif
3034        return(1);
3035    }
3036    if (st_is_member(t,(char *) g) == 1) {
3037        return(1);
3038    }
3039    if (st_add_direct(t,(char *) g,NULL) == ST_OUT_OF_MEM)
3040        return(0);
3041#ifdef DD_STATS
3042#if SIZEOF_VOID_P == 8
3043    (void) fprintf(dd->out,"ID = %c0x%lx\tindex = %d\tr = %d\t", bang(f),
3044                (ptruint) g / (ptruint) sizeof(DdNode), g->index, g->ref);
3045#else
3046    (void) fprintf(dd->out,"ID = %c0x%x\tindex = %d\tr = %d\t", bang(f),
3047                (ptruint) g / (ptruint) sizeof(DdNode),g->index,g->ref);
3048#endif
3049#else
3050#if SIZEOF_VOID_P == 8
3051    (void) fprintf(dd->out,"ID = %c0x%lx\tindex = %u\t", bang(f),
3052                (ptruint) g / (ptruint) sizeof(DdNode),g->index);
3053#else
3054    (void) fprintf(dd->out,"ID = %c0x%x\tindex = %hu\t", bang(f),
3055                (ptruint) g / (ptruint) sizeof(DdNode),g->index);
3056#endif
3057#endif
3058    n = cuddT(g);
3059    if (cuddIsConstant(n)) {
3060        (void) fprintf(dd->out,"T = %-9g\t",cuddV(n));
3061        T = 1;
3062    } else {
3063#if SIZEOF_VOID_P == 8
3064        (void) fprintf(dd->out,"T = 0x%lx\t",(ptruint) n / (ptruint) sizeof(DdNode));
3065#else
3066        (void) fprintf(dd->out,"T = 0x%x\t",(ptruint) n / (ptruint) sizeof(DdNode));
3067#endif
3068        T = 0;
3069    }
3070
3071    n = cuddE(g);
3072    N = Cudd_Regular(n);
3073    if (cuddIsConstant(N)) {
3074        (void) fprintf(dd->out,"E = %c%-9g\n",bang(n),cuddV(N));
3075        E = 1;
3076    } else {
3077#if SIZEOF_VOID_P == 8
3078        (void) fprintf(dd->out,"E = %c0x%lx\n", bang(n), (ptruint) N/(ptruint) sizeof(DdNode));
3079#else
3080        (void) fprintf(dd->out,"E = %c0x%x\n", bang(n), (ptruint) N/(ptruint) sizeof(DdNode));
3081#endif
3082        E = 0;
3083    }
3084    if (E == 0) {
3085        if (dp2(dd,N,t) == 0)
3086            return(0);
3087    }
3088    if (T == 0) {
3089        if (dp2(dd,cuddT(g),t) == 0)
3090            return(0);
3091    }
3092    return(1);
3093
3094} /* end of dp2 */
3095
3096
3097/**Function********************************************************************
3098
3099  Synopsis    [Performs the recursive step of Cudd_PrintMinterm.]
3100
3101  Description []
3102
3103  SideEffects [None]
3104
3105******************************************************************************/
3106static void
3107ddPrintMintermAux(
3108  DdManager * dd /* manager */,
3109  DdNode * node /* current node */,
3110  int * list /* current recursion path */)
3111{
3112    DdNode      *N,*Nv,*Nnv;
3113    int         i,v,index;
3114
3115    N = Cudd_Regular(node);
3116
3117    if (cuddIsConstant(N)) {
3118        /* Terminal case: Print one cube based on the current recursion
3119        ** path, unless we have reached the background value (ADDs) or
3120        ** the logical zero (BDDs).
3121        */
3122        if (node != background && node != zero) {
3123            for (i = 0; i < dd->size; i++) {
3124                v = list[i];
3125                if (v == 0) (void) fprintf(dd->out,"0");
3126                else if (v == 1) (void) fprintf(dd->out,"1");
3127                else (void) fprintf(dd->out,"-");
3128            }
3129            (void) fprintf(dd->out," % g\n", cuddV(node));
3130        }
3131    } else {
3132        Nv  = cuddT(N);
3133        Nnv = cuddE(N);
3134        if (Cudd_IsComplement(node)) {
3135            Nv  = Cudd_Not(Nv);
3136            Nnv = Cudd_Not(Nnv);
3137        }
3138        index = N->index;
3139        list[index] = 0;
3140        ddPrintMintermAux(dd,Nnv,list);
3141        list[index] = 1;
3142        ddPrintMintermAux(dd,Nv,list);
3143        list[index] = 2;
3144    }
3145    return;
3146
3147} /* end of ddPrintMintermAux */
3148
3149
3150/**Function********************************************************************
3151
3152  Synopsis    [Performs the recursive step of Cudd_DagSize.]
3153
3154  Description [Performs the recursive step of Cudd_DagSize. Returns the
3155  number of nodes in the graph rooted at n.]
3156
3157  SideEffects [None]
3158
3159******************************************************************************/
3160static int
3161ddDagInt(
3162  DdNode * n)
3163{
3164    int tval, eval;
3165
3166    if (Cudd_IsComplement(n->next)) {
3167        return(0);
3168    }
3169    n->next = Cudd_Not(n->next);
3170    if (cuddIsConstant(n)) {
3171        return(1);
3172    }
3173    tval = ddDagInt(cuddT(n));
3174    eval = ddDagInt(Cudd_Regular(cuddE(n)));
3175    return(1 + tval + eval);
3176
3177} /* end of ddDagInt */
3178
3179
3180/**Function********************************************************************
3181
3182  Synopsis    [Performs the recursive step of cuddNodeArray.]
3183
3184  Description [Performs the recursive step of cuddNodeArray.  Returns
3185  an the number of nodes in the DD.  Clear the least significant bit
3186  of the next field that was used as visited flag by
3187  cuddNodeArrayRecur when counting the nodes.  node is supposed to be
3188  regular; the invariant is maintained by this procedure.]
3189
3190  SideEffects [None]
3191
3192  SeeAlso     []
3193
3194******************************************************************************/
3195static int
3196cuddNodeArrayRecur(
3197  DdNode *f,
3198  DdNodePtr *table,
3199  int index)
3200{
3201    int tindex, eindex;
3202
3203    if (!Cudd_IsComplement(f->next)) {
3204        return(index);
3205    }
3206    /* Clear visited flag. */
3207    f->next = Cudd_Regular(f->next);
3208    if (cuddIsConstant(f)) {
3209        table[index] = f;
3210        return(index + 1);
3211    }
3212    tindex = cuddNodeArrayRecur(cuddT(f), table, index);
3213    eindex = cuddNodeArrayRecur(Cudd_Regular(cuddE(f)), table, tindex);
3214    table[eindex] = f;
3215    return(eindex + 1);
3216
3217} /* end of cuddNodeArrayRecur */
3218
3219
3220/**Function********************************************************************
3221
3222  Synopsis    [Performs the recursive step of Cudd_CofactorEstimate.]
3223
3224  Description [Performs the recursive step of Cudd_CofactorEstimate.
3225  Returns an estimate of the number of nodes in the DD of a
3226  cofactor of node. Uses the least significant bit of the next field as
3227  visited flag. node is supposed to be regular; the invariant is maintained
3228  by this procedure.]
3229
3230  SideEffects [None]
3231
3232  SeeAlso     []
3233
3234******************************************************************************/
3235static int
3236cuddEstimateCofactor(
3237  DdManager *dd,
3238  st_table *table,
3239  DdNode * node,
3240  int i,
3241  int phase,
3242  DdNode ** ptr)
3243{
3244    int tval, eval, val;
3245    DdNode *ptrT, *ptrE;
3246
3247    if (Cudd_IsComplement(node->next)) {
3248        if (!st_lookup(table,(char *)node,(char **)ptr)) {
3249            if (st_add_direct(table,(char *)node,(char *)node) ==
3250                ST_OUT_OF_MEM)
3251                return(CUDD_OUT_OF_MEM);
3252            *ptr = node;
3253        }
3254        return(0);
3255    }
3256    node->next = Cudd_Not(node->next);
3257    if (cuddIsConstant(node)) {
3258        *ptr = node;
3259        if (st_add_direct(table,(char *)node,(char *)node) == ST_OUT_OF_MEM)
3260            return(CUDD_OUT_OF_MEM);
3261        return(1);
3262    }
3263    if ((int) node->index == i) {
3264        if (phase == 1) {
3265            *ptr = cuddT(node);
3266            val = ddDagInt(cuddT(node));
3267        } else {
3268            *ptr = cuddE(node);
3269            val = ddDagInt(Cudd_Regular(cuddE(node)));
3270        }
3271        if (node->ref > 1) {
3272            if (st_add_direct(table,(char *)node,(char *)*ptr) ==
3273                ST_OUT_OF_MEM)
3274                return(CUDD_OUT_OF_MEM);
3275        }
3276        return(val);
3277    }
3278    if (dd->perm[node->index] > dd->perm[i]) {
3279        *ptr = node;
3280        tval = ddDagInt(cuddT(node));
3281        eval = ddDagInt(Cudd_Regular(cuddE(node)));
3282        if (node->ref > 1) {
3283            if (st_add_direct(table,(char *)node,(char *)node) ==
3284                ST_OUT_OF_MEM)
3285                return(CUDD_OUT_OF_MEM);
3286        }
3287        val = 1 + tval + eval;
3288        return(val);
3289    }
3290    tval = cuddEstimateCofactor(dd,table,cuddT(node),i,phase,&ptrT);
3291    eval = cuddEstimateCofactor(dd,table,Cudd_Regular(cuddE(node)),i,
3292                                phase,&ptrE);
3293    ptrE = Cudd_NotCond(ptrE,Cudd_IsComplement(cuddE(node)));
3294    if (ptrT == ptrE) {         /* recombination */
3295        *ptr = ptrT;
3296        val = tval;
3297        if (node->ref > 1) {
3298            if (st_add_direct(table,(char *)node,(char *)*ptr) ==
3299                    ST_OUT_OF_MEM)
3300                return(CUDD_OUT_OF_MEM);
3301        }
3302    } else if ((ptrT != cuddT(node) || ptrE != cuddE(node)) &&
3303               (*ptr = cuddUniqueLookup(dd,node->index,ptrT,ptrE)) != NULL) {
3304        if (Cudd_IsComplement((*ptr)->next)) {
3305            val = 0;
3306        } else {
3307            val = 1 + tval + eval;
3308        }
3309        if (node->ref > 1) {
3310            if (st_add_direct(table,(char *)node,(char *)*ptr) ==
3311                    ST_OUT_OF_MEM)
3312                return(CUDD_OUT_OF_MEM);
3313        }
3314    } else {
3315        *ptr = node;
3316        val = 1 + tval + eval;
3317    }
3318    return(val);
3319
3320} /* end of cuddEstimateCofactor */
3321
3322
3323/**Function********************************************************************
3324
3325  Synopsis    [Checks the unique table for the existence of an internal node.]
3326
3327  Description [Checks the unique table for the existence of an internal
3328  node. Returns a pointer to the node if it is in the table; NULL otherwise.]
3329
3330  SideEffects [None]
3331
3332  SeeAlso     [cuddUniqueInter]
3333
3334******************************************************************************/
3335static DdNode *
3336cuddUniqueLookup(
3337  DdManager * unique,
3338  int  index,
3339  DdNode * T,
3340  DdNode * E)
3341{
3342    int posn;
3343    unsigned int level;
3344    DdNodePtr *nodelist;
3345    DdNode *looking;
3346    DdSubtable *subtable;
3347
3348    if (index >= unique->size) {
3349        return(NULL);
3350    }
3351
3352    level = unique->perm[index];
3353    subtable = &(unique->subtables[level]);
3354
3355#ifdef DD_DEBUG
3356    assert(level < (unsigned) cuddI(unique,T->index));
3357    assert(level < (unsigned) cuddI(unique,Cudd_Regular(E)->index));
3358#endif
3359
3360    posn = ddHash(T, E, subtable->shift);
3361    nodelist = subtable->nodelist;
3362    looking = nodelist[posn];
3363
3364    while (T < cuddT(looking)) {
3365        looking = Cudd_Regular(looking->next);
3366    }
3367    while (T == cuddT(looking) && E < cuddE(looking)) {
3368        looking = Cudd_Regular(looking->next);
3369    }
3370    if (cuddT(looking) == T && cuddE(looking) == E) {
3371        return(looking);
3372    }
3373
3374    return(NULL);
3375
3376} /* end of cuddUniqueLookup */
3377
3378
3379/**Function********************************************************************
3380
3381  Synopsis    [Performs the recursive step of Cudd_CofactorEstimateSimple.]
3382
3383  Description [Performs the recursive step of Cudd_CofactorEstimateSimple.
3384  Returns an estimate of the number of nodes in the DD of the positive
3385  cofactor of node. Uses the least significant bit of the next field as
3386  visited flag. node is supposed to be regular; the invariant is maintained
3387  by this procedure.]
3388
3389  SideEffects [None]
3390
3391  SeeAlso     []
3392
3393******************************************************************************/
3394static int
3395cuddEstimateCofactorSimple(
3396  DdNode * node,
3397  int i)
3398{
3399    int tval, eval;
3400
3401    if (Cudd_IsComplement(node->next)) {
3402        return(0);
3403    }
3404    node->next = Cudd_Not(node->next);
3405    if (cuddIsConstant(node)) {
3406        return(1);
3407    }
3408    tval = cuddEstimateCofactorSimple(cuddT(node),i);
3409    if ((int) node->index == i) return(tval);
3410    eval = cuddEstimateCofactorSimple(Cudd_Regular(cuddE(node)),i);
3411    return(1 + tval + eval);
3412
3413} /* end of cuddEstimateCofactorSimple */
3414
3415
3416/**Function********************************************************************
3417
3418  Synopsis    [Performs the recursive step of Cudd_CountMinterm.]
3419
3420  Description [Performs the recursive step of Cudd_CountMinterm.
3421  It is based on the following identity. Let |f| be the
3422  number of minterms of f. Then:
3423  <xmp>
3424    |f| = (|f0|+|f1|)/2
3425  </xmp>
3426  where f0 and f1 are the two cofactors of f.  Does not use the
3427  identity |f'| = max - |f|, to minimize loss of accuracy due to
3428  roundoff.  Returns the number of minterms of the function rooted at
3429  node.]
3430
3431  SideEffects [None]
3432
3433******************************************************************************/
3434static double
3435ddCountMintermAux(
3436  DdNode * node,
3437  double  max,
3438  DdHashTable * table)
3439{
3440    DdNode      *N, *Nt, *Ne;
3441    double      min, minT, minE;
3442    DdNode      *res;
3443
3444    N = Cudd_Regular(node);
3445
3446    if (cuddIsConstant(N)) {
3447        if (node == background || node == zero) {
3448            return(0.0);
3449        } else {
3450            return(max);
3451        }
3452    }
3453    if (N->ref != 1 && (res = cuddHashTableLookup1(table,node)) != NULL) {
3454        min = cuddV(res);
3455        if (res->ref == 0) {
3456            table->manager->dead++;
3457            table->manager->constants.dead++;
3458        }
3459        return(min);
3460    }
3461
3462    Nt = cuddT(N); Ne = cuddE(N);
3463    if (Cudd_IsComplement(node)) {
3464        Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
3465    }
3466
3467    minT = ddCountMintermAux(Nt,max,table);
3468    if (minT == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3469    minT *= 0.5;
3470    minE = ddCountMintermAux(Ne,max,table);
3471    if (minE == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3472    minE *= 0.5;
3473    min = minT + minE;
3474
3475    if (N->ref != 1) {
3476        ptrint fanout = (ptrint) N->ref;
3477        cuddSatDec(fanout);
3478        res = cuddUniqueConst(table->manager,min);
3479        if (!cuddHashTableInsert1(table,node,res,fanout)) {
3480            cuddRef(res); Cudd_RecursiveDeref(table->manager, res);
3481            return((double)CUDD_OUT_OF_MEM);
3482        }
3483    }
3484
3485    return(min);
3486
3487} /* end of ddCountMintermAux */
3488
3489
3490/**Function********************************************************************
3491
3492  Synopsis    [Performs the recursive step of Cudd_CountPath.]
3493
3494  Description [Performs the recursive step of Cudd_CountPath.
3495  It is based on the following identity. Let |f| be the
3496  number of paths of f. Then:
3497  <xmp>
3498    |f| = |f0|+|f1|
3499  </xmp>
3500  where f0 and f1 are the two cofactors of f.  Uses the
3501  identity |f'| = |f|, to improve the utilization of the (local) cache.
3502  Returns the number of paths of the function rooted at node.]
3503
3504  SideEffects [None]
3505
3506******************************************************************************/
3507static double
3508ddCountPathAux(
3509  DdNode * node,
3510  st_table * table)
3511{
3512
3513    DdNode      *Nv, *Nnv;
3514    double      paths, *ppaths, paths1, paths2;
3515    double      *dummy;
3516
3517
3518    if (cuddIsConstant(node)) {
3519        return(1.0);
3520    }
3521    if (st_lookup(table, node, &dummy)) {
3522        paths = *dummy;
3523        return(paths);
3524    }
3525
3526    Nv = cuddT(node); Nnv = cuddE(node);
3527
3528    paths1 = ddCountPathAux(Nv,table);
3529    if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3530    paths2 = ddCountPathAux(Cudd_Regular(Nnv),table);
3531    if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3532    paths = paths1 + paths2;
3533
3534    ppaths = ALLOC(double,1);
3535    if (ppaths == NULL) {
3536        return((double)CUDD_OUT_OF_MEM);
3537    }
3538
3539    *ppaths = paths;
3540
3541    if (st_add_direct(table,(char *)node, (char *)ppaths) == ST_OUT_OF_MEM) {
3542        FREE(ppaths);
3543        return((double)CUDD_OUT_OF_MEM);
3544    }
3545    return(paths);
3546
3547} /* end of ddCountPathAux */
3548
3549
3550/**Function********************************************************************
3551
3552  Synopsis    [Performs the recursive step of Cudd_EpdCountMinterm.]
3553
3554  Description [Performs the recursive step of Cudd_EpdCountMinterm.
3555  It is based on the following identity. Let |f| be the
3556  number of minterms of f. Then:
3557  <xmp>
3558    |f| = (|f0|+|f1|)/2
3559  </xmp>
3560  where f0 and f1 are the two cofactors of f.  Does not use the
3561  identity |f'| = max - |f|, to minimize loss of accuracy due to
3562  roundoff.  Returns the number of minterms of the function rooted at
3563  node.]
3564
3565  SideEffects [None]
3566
3567******************************************************************************/
3568static int
3569ddEpdCountMintermAux(
3570  DdNode * node,
3571  EpDouble * max,
3572  EpDouble * epd,
3573  st_table * table)
3574{
3575    DdNode      *Nt, *Ne;
3576    EpDouble    *min, minT, minE;
3577    EpDouble    *res;
3578    int         status;
3579
3580    /* node is assumed to be regular */
3581    if (cuddIsConstant(node)) {
3582        if (node == background || node == zero) {
3583            EpdMakeZero(epd, 0);
3584        } else {
3585            EpdCopy(max, epd);
3586        }
3587        return(0);
3588    }
3589    if (node->ref != 1 && st_lookup(table, node, &res)) {
3590        EpdCopy(res, epd);
3591        return(0);
3592    }
3593
3594    Nt = cuddT(node); Ne = cuddE(node);
3595
3596    status = ddEpdCountMintermAux(Nt,max,&minT,table);
3597    if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
3598    EpdMultiply(&minT, (double)0.5);
3599    status = ddEpdCountMintermAux(Cudd_Regular(Ne),max,&minE,table);
3600    if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
3601    if (Cudd_IsComplement(Ne)) {
3602        EpdSubtract3(max, &minE, epd);
3603        EpdCopy(epd, &minE);
3604    }
3605    EpdMultiply(&minE, (double)0.5);
3606    EpdAdd3(&minT, &minE, epd);
3607
3608    if (node->ref > 1) {
3609        min = EpdAlloc();
3610        if (!min)
3611            return(CUDD_OUT_OF_MEM);
3612        EpdCopy(epd, min);
3613        if (st_insert(table, (char *)node, (char *)min) == ST_OUT_OF_MEM) {
3614            EpdFree(min);
3615            return(CUDD_OUT_OF_MEM);
3616        }
3617    }
3618
3619    return(0);
3620
3621} /* end of ddEpdCountMintermAux */
3622
3623
3624/**Function********************************************************************
3625
3626  Synopsis    [Performs the recursive step of Cudd_CountPathsToNonZero.]
3627
3628  Description [Performs the recursive step of Cudd_CountPathsToNonZero.
3629  It is based on the following identity. Let |f| be the
3630  number of paths of f. Then:
3631  <xmp>
3632    |f| = |f0|+|f1|
3633  </xmp>
3634  where f0 and f1 are the two cofactors of f.  Returns the number of
3635  paths of the function rooted at node.]
3636
3637  SideEffects [None]
3638
3639******************************************************************************/
3640static double
3641ddCountPathsToNonZero(
3642  DdNode * N,
3643  st_table * table)
3644{
3645
3646    DdNode      *node, *Nt, *Ne;
3647    double      paths, *ppaths, paths1, paths2;
3648    double      *dummy;
3649
3650    node = Cudd_Regular(N);
3651    if (cuddIsConstant(node)) {
3652        return((double) !(Cudd_IsComplement(N) || cuddV(node)==DD_ZERO_VAL));
3653    }
3654    if (st_lookup(table, N, &dummy)) {
3655        paths = *dummy;
3656        return(paths);
3657    }
3658
3659    Nt = cuddT(node); Ne = cuddE(node);
3660    if (node != N) {
3661        Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
3662    }
3663
3664    paths1 = ddCountPathsToNonZero(Nt,table);
3665    if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3666    paths2 = ddCountPathsToNonZero(Ne,table);
3667    if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3668    paths = paths1 + paths2;
3669
3670    ppaths = ALLOC(double,1);
3671    if (ppaths == NULL) {
3672        return((double)CUDD_OUT_OF_MEM);
3673    }
3674
3675    *ppaths = paths;
3676
3677    if (st_add_direct(table,(char *)N, (char *)ppaths) == ST_OUT_OF_MEM) {
3678        FREE(ppaths);
3679        return((double)CUDD_OUT_OF_MEM);
3680    }
3681    return(paths);
3682
3683} /* end of ddCountPathsToNonZero */
3684
3685
3686/**Function********************************************************************
3687
3688  Synopsis    [Performs the recursive step of Cudd_Support.]
3689
3690  Description [Performs the recursive step of Cudd_Support. Performs a
3691  DFS from f. The support is accumulated in supp as a side effect. Uses
3692  the LSB of the then pointer as visited flag.]
3693
3694  SideEffects [None]
3695
3696  SeeAlso     [ddClearFlag]
3697
3698******************************************************************************/
3699static void
3700ddSupportStep(
3701  DdNode * f,
3702  int * support)
3703{
3704    if (cuddIsConstant(f) || Cudd_IsComplement(f->next)) {
3705        return;
3706    }
3707
3708    support[f->index] = 1;
3709    ddSupportStep(cuddT(f),support);
3710    ddSupportStep(Cudd_Regular(cuddE(f)),support);
3711    /* Mark as visited. */
3712    f->next = Cudd_Not(f->next);
3713    return;
3714
3715} /* end of ddSupportStep */
3716
3717
3718/**Function********************************************************************
3719
3720  Synopsis    [Performs a DFS from f, clearing the LSB of the next
3721  pointers.]
3722
3723  Description []
3724
3725  SideEffects [None]
3726
3727  SeeAlso     [ddSupportStep ddDagInt]
3728
3729******************************************************************************/
3730static void
3731ddClearFlag(
3732  DdNode * f)
3733{
3734    if (!Cudd_IsComplement(f->next)) {
3735        return;
3736    }
3737    /* Clear visited flag. */
3738    f->next = Cudd_Regular(f->next);
3739    if (cuddIsConstant(f)) {
3740        return;
3741    }
3742    ddClearFlag(cuddT(f));
3743    ddClearFlag(Cudd_Regular(cuddE(f)));
3744    return;
3745
3746} /* end of ddClearFlag */
3747
3748
3749/**Function********************************************************************
3750
3751  Synopsis    [Performs the recursive step of Cudd_CountLeaves.]
3752
3753  Description [Performs the recursive step of Cudd_CountLeaves. Returns
3754  the number of leaves in the DD rooted at n.]
3755
3756  SideEffects [None]
3757
3758  SeeAlso     [Cudd_CountLeaves]
3759
3760******************************************************************************/
3761static int
3762ddLeavesInt(
3763  DdNode * n)
3764{
3765    int tval, eval;
3766
3767    if (Cudd_IsComplement(n->next)) {
3768        return(0);
3769    }
3770    n->next = Cudd_Not(n->next);
3771    if (cuddIsConstant(n)) {
3772        return(1);
3773    }
3774    tval = ddLeavesInt(cuddT(n));
3775    eval = ddLeavesInt(Cudd_Regular(cuddE(n)));
3776    return(tval + eval);
3777
3778} /* end of ddLeavesInt */
3779
3780
3781/**Function********************************************************************
3782
3783  Synopsis    [Performs the recursive step of Cudd_bddPickArbitraryMinterms.]
3784
3785  Description [Performs the recursive step of Cudd_bddPickArbitraryMinterms.
3786  Returns 1 if successful; 0 otherwise.]
3787
3788  SideEffects [none]
3789
3790  SeeAlso [Cudd_bddPickArbitraryMinterms]
3791
3792******************************************************************************/
3793static int
3794ddPickArbitraryMinterms(
3795  DdManager *dd,
3796  DdNode *node,
3797  int nvars,
3798  int nminterms,
3799  char **string)
3800{
3801    DdNode *N, *T, *E;
3802    DdNode *one, *bzero;
3803    int    i, t, result;
3804    double min1, min2;
3805
3806    if (string == NULL || node == NULL) return(0);
3807
3808    /* The constant 0 function has no on-set cubes. */
3809    one = DD_ONE(dd);
3810    bzero = Cudd_Not(one);
3811    if (nminterms == 0 || node == bzero) return(1);
3812    if (node == one) {
3813        return(1);
3814    }
3815
3816    N = Cudd_Regular(node);
3817    T = cuddT(N); E = cuddE(N);
3818    if (Cudd_IsComplement(node)) {
3819        T = Cudd_Not(T); E = Cudd_Not(E);
3820    }
3821
3822    min1 = Cudd_CountMinterm(dd, T, nvars) / 2.0;
3823    if (min1 == (double)CUDD_OUT_OF_MEM) return(0);
3824    min2 = Cudd_CountMinterm(dd, E, nvars) / 2.0;
3825    if (min2 == (double)CUDD_OUT_OF_MEM) return(0);
3826
3827    t = (int)((double)nminterms * min1 / (min1 + min2) + 0.5);
3828    for (i = 0; i < t; i++)
3829        string[i][N->index] = '1';
3830    for (i = t; i < nminterms; i++)
3831        string[i][N->index] = '0';
3832
3833    result = ddPickArbitraryMinterms(dd,T,nvars,t,&string[0]);
3834    if (result == 0)
3835        return(0);
3836    result = ddPickArbitraryMinterms(dd,E,nvars,nminterms-t,&string[t]);
3837    return(result);
3838
3839} /* end of ddPickArbitraryMinterms */
3840
3841
3842/**Function********************************************************************
3843
3844  Synopsis    [Finds a representative cube of a BDD.]
3845
3846  Description [Finds a representative cube of a BDD with the weight of
3847  each variable. From the top variable, if the weight is greater than or
3848  equal to 0.0, choose THEN branch unless the child is the constant 0.
3849  Otherwise, choose ELSE branch unless the child is the constant 0.]
3850
3851  SideEffects [Cudd_SubsetWithMaskVars Cudd_bddPickOneCube]
3852
3853******************************************************************************/
3854static int
3855ddPickRepresentativeCube(
3856  DdManager *dd,
3857  DdNode *node,
3858  double *weight,
3859  char *string)
3860{
3861    DdNode *N, *T, *E;
3862    DdNode *one, *bzero;
3863
3864    if (string == NULL || node == NULL) return(0);
3865
3866    /* The constant 0 function has no on-set cubes. */
3867    one = DD_ONE(dd);
3868    bzero = Cudd_Not(one);
3869    if (node == bzero) return(0);
3870
3871    if (node == DD_ONE(dd)) return(1);
3872
3873    for (;;) {
3874        N = Cudd_Regular(node);
3875        if (N == one)
3876            break;
3877        T = cuddT(N);
3878        E = cuddE(N);
3879        if (Cudd_IsComplement(node)) {
3880            T = Cudd_Not(T);
3881            E = Cudd_Not(E);
3882        }
3883        if (weight[N->index] >= 0.0) {
3884            if (T == bzero) {
3885                node = E;
3886                string[N->index] = '0';
3887            } else {
3888                node = T;
3889                string[N->index] = '1';
3890            }
3891        } else {
3892            if (E == bzero) {
3893                node = T;
3894                string[N->index] = '1';
3895            } else {
3896                node = E;
3897                string[N->index] = '0';
3898            }
3899        }
3900    }
3901    return(1);
3902
3903} /* end of ddPickRepresentativeCube */
3904
3905
3906/**Function********************************************************************
3907
3908  Synopsis [Frees the memory used to store the minterm counts recorded
3909  in the visited table.]
3910
3911  Description [Frees the memory used to store the minterm counts
3912  recorded in the visited table. Returns ST_CONTINUE.]
3913
3914  SideEffects [None]
3915
3916******************************************************************************/
3917static enum st_retval
3918ddEpdFree(
3919  char * key,
3920  char * value,
3921  char * arg)
3922{
3923    EpDouble    *epd;
3924
3925    epd = (EpDouble *) value;
3926    EpdFree(epd);
3927    return(ST_CONTINUE);
3928
3929} /* end of ddEpdFree */
Note: See TracBrowser for help on using the repository browser.