source: vis_dev/glu-2.1/src/cuBdd/cuddAPI.c @ 11

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

src glu

File size: 123.3 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddAPI.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Application interface functions.]
8
9  Description [External procedures included in this module:
10                <ul>
11                <li> Cudd_addNewVar()
12                <li> Cudd_addNewVarAtLevel()
13                <li> Cudd_bddNewVar()
14                <li> Cudd_bddNewVarAtLevel()
15                <li> Cudd_addIthVar()
16                <li> Cudd_bddIthVar()
17                <li> Cudd_zddIthVar()
18                <li> Cudd_zddVarsFromBddVars()
19                <li> Cudd_addConst()
20                <li> Cudd_IsNonConstant()
21                <li> Cudd_AutodynEnable()
22                <li> Cudd_AutodynDisable()
23                <li> Cudd_ReorderingStatus()
24                <li> Cudd_AutodynEnableZdd()
25                <li> Cudd_AutodynDisableZdd()
26                <li> Cudd_ReorderingStatusZdd()
27                <li> Cudd_zddRealignmentEnabled()
28                <li> Cudd_zddRealignEnable()
29                <li> Cudd_zddRealignDisable()
30                <li> Cudd_bddRealignmentEnabled()
31                <li> Cudd_bddRealignEnable()
32                <li> Cudd_bddRealignDisable()
33                <li> Cudd_ReadOne()
34                <li> Cudd_ReadZddOne()
35                <li> Cudd_ReadZero()
36                <li> Cudd_ReadLogicZero()
37                <li> Cudd_ReadPlusInfinity()
38                <li> Cudd_ReadMinusInfinity()
39                <li> Cudd_ReadBackground()
40                <li> Cudd_SetBackground()
41                <li> Cudd_ReadCacheSlots()
42                <li> Cudd_ReadCacheUsedSlots()
43                <li> Cudd_ReadCacheLookUps()
44                <li> Cudd_ReadCacheHits()
45                <li> Cudd_ReadMinHit()
46                <li> Cudd_SetMinHit()
47                <li> Cudd_ReadLooseUpTo()
48                <li> Cudd_SetLooseUpTo()
49                <li> Cudd_ReadMaxCache()
50                <li> Cudd_ReadMaxCacheHard()
51                <li> Cudd_SetMaxCacheHard()
52                <li> Cudd_ReadSize()
53                <li> Cudd_ReadSlots()
54                <li> Cudd_ReadUsedSlots()
55                <li> Cudd_ExpectedUsedSlots()
56                <li> Cudd_ReadKeys()
57                <li> Cudd_ReadDead()
58                <li> Cudd_ReadMinDead()
59                <li> Cudd_ReadReorderings()
60                <li> Cudd_ReadReorderingTime()
61                <li> Cudd_ReadGarbageCollections()
62                <li> Cudd_ReadGarbageCollectionTime()
63                <li> Cudd_ReadNodesFreed()
64                <li> Cudd_ReadNodesDropped()
65                <li> Cudd_ReadUniqueLookUps()
66                <li> Cudd_ReadUniqueLinks()
67                <li> Cudd_ReadSiftMaxVar()
68                <li> Cudd_SetSiftMaxVar()
69                <li> Cudd_ReadMaxGrowth()
70                <li> Cudd_SetMaxGrowth()
71                <li> Cudd_ReadMaxGrowthAlternate()
72                <li> Cudd_SetMaxGrowthAlternate()
73                <li> Cudd_ReadReorderingCycle()
74                <li> Cudd_SetReorderingCycle()
75                <li> Cudd_ReadTree()
76                <li> Cudd_SetTree()
77                <li> Cudd_FreeTree()
78                <li> Cudd_ReadZddTree()
79                <li> Cudd_SetZddTree()
80                <li> Cudd_FreeZddTree()
81                <li> Cudd_NodeReadIndex()
82                <li> Cudd_ReadPerm()
83                <li> Cudd_ReadInvPerm()
84                <li> Cudd_ReadVars()
85                <li> Cudd_ReadEpsilon()
86                <li> Cudd_SetEpsilon()
87                <li> Cudd_ReadGroupCheck()
88                <li> Cudd_SetGroupcheck()
89                <li> Cudd_GarbageCollectionEnabled()
90                <li> Cudd_EnableGarbageCollection()
91                <li> Cudd_DisableGarbageCollection()
92                <li> Cudd_DeadAreCounted()
93                <li> Cudd_TurnOnCountDead()
94                <li> Cudd_TurnOffCountDead()
95                <li> Cudd_ReadRecomb()
96                <li> Cudd_SetRecomb()
97                <li> Cudd_ReadSymmviolation()
98                <li> Cudd_SetSymmviolation()
99                <li> Cudd_ReadArcviolation()
100                <li> Cudd_SetArcviolation()
101                <li> Cudd_ReadPopulationSize()
102                <li> Cudd_SetPopulationSize()
103                <li> Cudd_ReadNumberXovers()
104                <li> Cudd_SetNumberXovers()
105                <li> Cudd_ReadMemoryInUse()
106                <li> Cudd_PrintInfo()
107                <li> Cudd_ReadPeakNodeCount()
108                <li> Cudd_ReadPeakLiveNodeCount()
109                <li> Cudd_ReadNodeCount()
110                <li> Cudd_zddReadNodeCount()
111                <li> Cudd_AddHook()
112                <li> Cudd_RemoveHook()
113                <li> Cudd_IsInHook()
114                <li> Cudd_StdPreReordHook()
115                <li> Cudd_StdPostReordHook()
116                <li> Cudd_EnableReorderingReporting()
117                <li> Cudd_DisableReorderingReporting()
118                <li> Cudd_ReorderingReporting()
119                <li> Cudd_ReadErrorCode()
120                <li> Cudd_ClearErrorCode()
121                <li> Cudd_ReadStdout()
122                <li> Cudd_SetStdout()
123                <li> Cudd_ReadStderr()
124                <li> Cudd_SetStderr()
125                <li> Cudd_ReadNextReordering()
126                <li> Cudd_SetNextReordering()
127                <li> Cudd_ReadSwapSteps()
128                <li> Cudd_ReadMaxLive()
129                <li> Cudd_SetMaxLive()
130                <li> Cudd_ReadMaxMemory()
131                <li> Cudd_SetMaxMemory()
132                <li> Cudd_bddBindVar()
133                <li> Cudd_bddUnbindVar()
134                <li> Cudd_bddVarIsBound()
135                <li> Cudd_bddSetPiVar()
136                <li> Cudd_bddSetPsVar()
137                <li> Cudd_bddSetNsVar()
138                <li> Cudd_bddIsPiVar()
139                <li> Cudd_bddIsPsVar()
140                <li> Cudd_bddIsNsVar()
141                <li> Cudd_bddSetPairIndex()
142                <li> Cudd_bddReadPairIndex()
143                <li> Cudd_bddSetVarToBeGrouped()
144                <li> Cudd_bddSetVarHardGroup()
145                <li> Cudd_bddResetVarToBeGrouped()
146                <li> Cudd_bddIsVarToBeGrouped()
147                <li> Cudd_bddSetVarToBeUngrouped()
148                <li> Cudd_bddIsVarToBeUngrouped()
149                <li> Cudd_bddIsVarHardGroup()
150                </ul>
151              Static procedures included in this module:
152                <ul>
153                <li> fixVarTree()
154                </ul>]
155
156  SeeAlso     []
157
158  Author      [Fabio Somenzi]
159
160  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
161
162  All rights reserved.
163
164  Redistribution and use in source and binary forms, with or without
165  modification, are permitted provided that the following conditions
166  are met:
167
168  Redistributions of source code must retain the above copyright
169  notice, this list of conditions and the following disclaimer.
170
171  Redistributions in binary form must reproduce the above copyright
172  notice, this list of conditions and the following disclaimer in the
173  documentation and/or other materials provided with the distribution.
174
175  Neither the name of the University of Colorado nor the names of its
176  contributors may be used to endorse or promote products derived from
177  this software without specific prior written permission.
178
179  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
180  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
181  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
182  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
183  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
184  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
185  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
186  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
187  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
188  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
189  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
190  POSSIBILITY OF SUCH DAMAGE.]
191
192******************************************************************************/
193
194#include "util.h"
195#include "cuddInt.h"
196
197/*---------------------------------------------------------------------------*/
198/* Constant declarations                                                     */
199/*---------------------------------------------------------------------------*/
200
201/*---------------------------------------------------------------------------*/
202/* Stucture declarations                                                     */
203/*---------------------------------------------------------------------------*/
204
205/*---------------------------------------------------------------------------*/
206/* Type declarations                                                         */
207/*---------------------------------------------------------------------------*/
208
209/*---------------------------------------------------------------------------*/
210/* Variable declarations                                                     */
211/*---------------------------------------------------------------------------*/
212
213#ifndef lint
214static char rcsid[] DD_UNUSED = "$Id: cuddAPI.c,v 1.57 2004/08/13 18:04:45 fabio Exp $";
215#endif
216
217/*---------------------------------------------------------------------------*/
218/* Macro declarations                                                        */
219/*---------------------------------------------------------------------------*/
220
221/**AutomaticStart*************************************************************/
222
223/*---------------------------------------------------------------------------*/
224/* Static function prototypes                                                */
225/*---------------------------------------------------------------------------*/
226
227static void fixVarTree (MtrNode *treenode, int *perm, int size);
228static int addMultiplicityGroups (DdManager *dd, MtrNode *treenode, int multiplicity, char *vmask, char *lmask);
229
230/**AutomaticEnd***************************************************************/
231
232
233/*---------------------------------------------------------------------------*/
234/* Definition of exported functions                                          */
235/*---------------------------------------------------------------------------*/
236
237
238/**Function********************************************************************
239
240  Synopsis    [Returns a new ADD variable.]
241
242  Description [Creates a new ADD variable.  The new variable has an
243  index equal to the largest previous index plus 1.  Returns a
244  pointer to the new variable if successful; NULL otherwise.
245  An ADD variable differs from a BDD variable because it points to the
246  arithmetic zero, instead of having a complement pointer to 1. ]
247
248  SideEffects [None]
249
250  SeeAlso     [Cudd_bddNewVar Cudd_addIthVar Cudd_addConst
251  Cudd_addNewVarAtLevel]
252
253******************************************************************************/
254DdNode *
255Cudd_addNewVar(
256  DdManager * dd)
257{
258    DdNode *res;
259
260    if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
261    do {
262        dd->reordered = 0;
263        res = cuddUniqueInter(dd,dd->size,DD_ONE(dd),DD_ZERO(dd));
264    } while (dd->reordered == 1);
265
266    return(res);
267
268} /* end of Cudd_addNewVar */
269
270
271/**Function********************************************************************
272
273  Synopsis    [Returns a new ADD variable at a specified level.]
274
275  Description [Creates a new ADD variable.  The new variable has an
276  index equal to the largest previous index plus 1 and is positioned at
277  the specified level in the order.  Returns a pointer to the new
278  variable if successful; NULL otherwise.]
279
280  SideEffects [None]
281
282  SeeAlso     [Cudd_addNewVar Cudd_addIthVar Cudd_bddNewVarAtLevel]
283
284******************************************************************************/
285DdNode *
286Cudd_addNewVarAtLevel(
287  DdManager * dd,
288  int  level)
289{
290    DdNode *res;
291
292    if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
293    if (level >= dd->size) return(Cudd_addIthVar(dd,level));
294    if (!cuddInsertSubtables(dd,1,level)) return(NULL);
295    do {
296        dd->reordered = 0;
297        res = cuddUniqueInter(dd,dd->size - 1,DD_ONE(dd),DD_ZERO(dd));
298    } while (dd->reordered == 1);
299
300    return(res);
301
302} /* end of Cudd_addNewVarAtLevel */
303
304
305/**Function********************************************************************
306
307  Synopsis    [Returns a new BDD variable.]
308
309  Description [Creates a new BDD variable.  The new variable has an
310  index equal to the largest previous index plus 1.  Returns a
311  pointer to the new variable if successful; NULL otherwise.]
312
313  SideEffects [None]
314
315  SeeAlso     [Cudd_addNewVar Cudd_bddIthVar Cudd_bddNewVarAtLevel]
316
317******************************************************************************/
318DdNode *
319Cudd_bddNewVar(
320  DdManager * dd)
321{
322    DdNode *res;
323
324    if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
325    res = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one));
326
327    return(res);
328
329} /* end of Cudd_bddNewVar */
330
331
332/**Function********************************************************************
333
334  Synopsis    [Returns a new BDD variable at a specified level.]
335
336  Description [Creates a new BDD variable.  The new variable has an
337  index equal to the largest previous index plus 1 and is positioned at
338  the specified level in the order.  Returns a pointer to the new
339  variable if successful; NULL otherwise.]
340
341  SideEffects [None]
342
343  SeeAlso     [Cudd_bddNewVar Cudd_bddIthVar Cudd_addNewVarAtLevel]
344
345******************************************************************************/
346DdNode *
347Cudd_bddNewVarAtLevel(
348  DdManager * dd,
349  int  level)
350{
351    DdNode *res;
352
353    if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
354    if (level >= dd->size) return(Cudd_bddIthVar(dd,level));
355    if (!cuddInsertSubtables(dd,1,level)) return(NULL);
356    res = dd->vars[dd->size - 1];
357
358    return(res);
359
360} /* end of Cudd_bddNewVarAtLevel */
361
362
363/**Function********************************************************************
364
365  Synopsis    [Returns the ADD variable with index i.]
366
367  Description [Retrieves the ADD variable with index i if it already
368  exists, or creates a new ADD variable.  Returns a pointer to the
369  variable if successful; NULL otherwise.  An ADD variable differs from
370  a BDD variable because it points to the arithmetic zero, instead of
371  having a complement pointer to 1. ]
372
373  SideEffects [None]
374
375  SeeAlso     [Cudd_addNewVar Cudd_bddIthVar Cudd_addConst
376  Cudd_addNewVarAtLevel]
377
378******************************************************************************/
379DdNode *
380Cudd_addIthVar(
381  DdManager * dd,
382  int  i)
383{
384    DdNode *res;
385
386    if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL);
387    do {
388        dd->reordered = 0;
389        res = cuddUniqueInter(dd,i,DD_ONE(dd),DD_ZERO(dd));
390    } while (dd->reordered == 1);
391
392    return(res);
393
394} /* end of Cudd_addIthVar */
395
396
397/**Function********************************************************************
398
399  Synopsis    [Returns the BDD variable with index i.]
400
401  Description [Retrieves the BDD variable with index i if it already
402  exists, or creates a new BDD variable.  Returns a pointer to the
403  variable if successful; NULL otherwise.]
404
405  SideEffects [None]
406
407  SeeAlso     [Cudd_bddNewVar Cudd_addIthVar Cudd_bddNewVarAtLevel
408  Cudd_ReadVars]
409
410******************************************************************************/
411DdNode *
412Cudd_bddIthVar(
413  DdManager * dd,
414  int  i)
415{
416    DdNode *res;
417
418    if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL);
419    if (i < dd->size) {
420        res = dd->vars[i];
421    } else {
422        res = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
423    }
424
425    return(res);
426
427} /* end of Cudd_bddIthVar */
428
429
430/**Function********************************************************************
431
432  Synopsis    [Returns the ZDD variable with index i.]
433
434  Description [Retrieves the ZDD variable with index i if it already
435  exists, or creates a new ZDD variable.  Returns a pointer to the
436  variable if successful; NULL otherwise.]
437
438  SideEffects [None]
439
440  SeeAlso     [Cudd_bddIthVar Cudd_addIthVar]
441
442******************************************************************************/
443DdNode *
444Cudd_zddIthVar(
445  DdManager * dd,
446  int  i)
447{
448    DdNode *res;
449    DdNode *zvar;
450    DdNode *lower;
451    int j;
452
453    if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL);
454
455    /* The i-th variable function has the following structure:
456    ** at the level corresponding to index i there is a node whose "then"
457    ** child points to the universe, and whose "else" child points to zero.
458    ** Above that level there are nodes with identical children.
459    */
460
461    /* First we build the node at the level of index i. */
462    lower = (i < dd->sizeZ - 1) ? dd->univ[dd->permZ[i]+1] : DD_ONE(dd);
463    do {
464        dd->reordered = 0;
465        zvar = cuddUniqueInterZdd(dd, i, lower, DD_ZERO(dd));
466    } while (dd->reordered == 1);
467
468    if (zvar == NULL)
469        return(NULL);
470    cuddRef(zvar);
471
472    /* Now we add the "filler" nodes above the level of index i. */
473    for (j = dd->permZ[i] - 1; j >= 0; j--) {
474        do {
475            dd->reordered = 0;
476            res = cuddUniqueInterZdd(dd, dd->invpermZ[j], zvar, zvar);
477        } while (dd->reordered == 1);
478        if (res == NULL) {
479            Cudd_RecursiveDerefZdd(dd,zvar);
480            return(NULL);
481        }
482        cuddRef(res);
483        Cudd_RecursiveDerefZdd(dd,zvar);
484        zvar = res;
485    }
486    cuddDeref(zvar);
487    return(zvar);
488
489} /* end of Cudd_zddIthVar */
490
491
492/**Function********************************************************************
493
494  Synopsis    [Creates one or more ZDD variables for each BDD variable.]
495
496  Description [Creates one or more ZDD variables for each BDD
497  variable.  If some ZDD variables already exist, only the missing
498  variables are created.  Parameter multiplicity allows the caller to
499  control how many variables are created for each BDD variable in
500  existence. For instance, if ZDDs are used to represent covers, two
501  ZDD variables are required for each BDD variable.  The order of the
502  BDD variables is transferred to the ZDD variables. If a variable
503  group tree exists for the BDD variables, a corresponding ZDD
504  variable group tree is created by expanding the BDD variable
505  tree. In any case, the ZDD variables derived from the same BDD
506  variable are merged in a ZDD variable group. If a ZDD variable group
507  tree exists, it is freed. Returns 1 if successful; 0 otherwise.]
508
509  SideEffects [None]
510
511  SeeAlso     [Cudd_bddNewVar Cudd_bddIthVar Cudd_bddNewVarAtLevel]
512
513******************************************************************************/
514int
515Cudd_zddVarsFromBddVars(
516  DdManager * dd /* DD manager */,
517  int multiplicity /* how many ZDD variables are created for each BDD variable */)
518{
519    int res;
520    int i, j;
521    int allnew;
522    int *permutation;
523
524    if (multiplicity < 1) return(0);
525    allnew = dd->sizeZ == 0;
526    if (dd->size * multiplicity > dd->sizeZ) {
527        res = cuddResizeTableZdd(dd,dd->size * multiplicity - 1);
528        if (res == 0) return(0);
529    }
530    /* Impose the order of the BDD variables to the ZDD variables. */
531    if (allnew) {
532        for (i = 0; i < dd->size; i++) {
533            for (j = 0; j < multiplicity; j++) {
534                dd->permZ[i * multiplicity + j] =
535                    dd->perm[i] * multiplicity + j;
536                dd->invpermZ[dd->permZ[i * multiplicity + j]] =
537                    i * multiplicity + j;
538            }
539        }
540        for (i = 0; i < dd->sizeZ; i++) {
541            dd->univ[i]->index = dd->invpermZ[i];
542        }
543    } else {
544        permutation = ALLOC(int,dd->sizeZ);
545        if (permutation == NULL) {
546            dd->errorCode = CUDD_MEMORY_OUT;
547            return(0);
548        }
549        for (i = 0; i < dd->size; i++) {
550            for (j = 0; j < multiplicity; j++) {
551                permutation[i * multiplicity + j] =
552                    dd->invperm[i] * multiplicity + j;
553            }
554        }
555        for (i = dd->size * multiplicity; i < dd->sizeZ; i++) {
556            permutation[i] = i;
557        }
558        res = Cudd_zddShuffleHeap(dd, permutation);
559        FREE(permutation);
560        if (res == 0) return(0);
561    }
562    /* Copy and expand the variable group tree if it exists. */
563    if (dd->treeZ != NULL) {
564        Cudd_FreeZddTree(dd);
565    }
566    if (dd->tree != NULL) {
567        dd->treeZ = Mtr_CopyTree(dd->tree, multiplicity);
568        if (dd->treeZ == NULL) return(0);
569    } else if (multiplicity > 1) {
570        dd->treeZ = Mtr_InitGroupTree(0, dd->sizeZ);
571        if (dd->treeZ == NULL) return(0);
572        dd->treeZ->index = dd->invpermZ[0];
573    }
574    /* Create groups for the ZDD variables derived from the same BDD variable.
575    */
576    if (multiplicity > 1) {
577        char *vmask, *lmask;
578
579        vmask = ALLOC(char, dd->size);
580        if (vmask == NULL) {
581            dd->errorCode = CUDD_MEMORY_OUT;
582            return(0);
583        }
584        lmask =  ALLOC(char, dd->size);
585        if (lmask == NULL) {
586            dd->errorCode = CUDD_MEMORY_OUT;
587            return(0);
588        }
589        for (i = 0; i < dd->size; i++) {
590            vmask[i] = lmask[i] = 0;
591        }
592        res = addMultiplicityGroups(dd,dd->treeZ,multiplicity,vmask,lmask);
593        FREE(vmask);
594        FREE(lmask);
595        if (res == 0) return(0);
596    }
597    return(1);
598
599} /* end of Cudd_zddVarsFromBddVars */
600
601
602/**Function********************************************************************
603
604  Synopsis    [Returns the ADD for constant c.]
605
606  Description [Retrieves the ADD for constant c if it already
607  exists, or creates a new ADD.  Returns a pointer to the
608  ADD if successful; NULL otherwise.]
609
610  SideEffects [None]
611
612  SeeAlso     [Cudd_addNewVar Cudd_addIthVar]
613
614******************************************************************************/
615DdNode *
616Cudd_addConst(
617  DdManager * dd,
618  CUDD_VALUE_TYPE  c)
619{
620    return(cuddUniqueConst(dd,c));
621
622} /* end of Cudd_addConst */
623
624
625/**Function********************************************************************
626
627  Synopsis    [Returns 1 if a DD node is not constant.]
628
629  Description [Returns 1 if a DD node is not constant. This function is
630  useful to test the results of Cudd_bddIteConstant, Cudd_addIteConstant,
631  Cudd_addEvalConst. These results may be a special value signifying
632  non-constant. In the other cases the macro Cudd_IsConstant can be used.]
633
634  SideEffects [None]
635
636  SeeAlso     [Cudd_IsConstant Cudd_bddIteConstant Cudd_addIteConstant
637  Cudd_addEvalConst]
638
639******************************************************************************/
640int
641Cudd_IsNonConstant(
642  DdNode *f)
643{
644    return(f == DD_NON_CONSTANT || !Cudd_IsConstant(f));
645
646} /* end of Cudd_IsNonConstant */
647
648
649/**Function********************************************************************
650
651  Synopsis    [Enables automatic dynamic reordering of BDDs and ADDs.]
652
653  Description [Enables automatic dynamic reordering of BDDs and
654  ADDs. Parameter method is used to determine the method used for
655  reordering. If CUDD_REORDER_SAME is passed, the method is
656  unchanged.]
657
658  SideEffects [None]
659
660  SeeAlso     [Cudd_AutodynDisable Cudd_ReorderingStatus
661  Cudd_AutodynEnableZdd]
662
663******************************************************************************/
664void
665Cudd_AutodynEnable(
666  DdManager * unique,
667  Cudd_ReorderingType  method)
668{
669    unique->autoDyn = 1;
670    if (method != CUDD_REORDER_SAME) {
671        unique->autoMethod = method;
672    }
673#ifndef DD_NO_DEATH_ROW
674    /* If reordering is enabled, using the death row causes too many
675    ** invocations. Hence, we shrink the death row to just one entry.
676    */
677    cuddClearDeathRow(unique);
678    unique->deathRowDepth = 1;
679    unique->deadMask = unique->deathRowDepth - 1;
680    if ((unsigned) unique->nextDead > unique->deadMask) {
681        unique->nextDead = 0;
682    }
683    unique->deathRow = REALLOC(DdNodePtr, unique->deathRow,
684        unique->deathRowDepth);
685#endif
686    return;
687
688} /* end of Cudd_AutodynEnable */
689
690
691/**Function********************************************************************
692
693  Synopsis    [Disables automatic dynamic reordering.]
694
695  Description []
696
697  SideEffects [None]
698
699  SeeAlso     [Cudd_AutodynEnable Cudd_ReorderingStatus
700  Cudd_AutodynDisableZdd]
701
702******************************************************************************/
703void
704Cudd_AutodynDisable(
705  DdManager * unique)
706{
707    unique->autoDyn = 0;
708    return;
709
710} /* end of Cudd_AutodynDisable */
711
712
713/**Function********************************************************************
714
715  Synopsis    [Reports the status of automatic dynamic reordering of BDDs
716  and ADDs.]
717
718  Description [Reports the status of automatic dynamic reordering of
719  BDDs and ADDs. Parameter method is set to the reordering method
720  currently selected. Returns 1 if automatic reordering is enabled; 0
721  otherwise.]
722
723  SideEffects [Parameter method is set to the reordering method currently
724  selected.]
725
726  SeeAlso     [Cudd_AutodynEnable Cudd_AutodynDisable
727  Cudd_ReorderingStatusZdd]
728
729******************************************************************************/
730int
731Cudd_ReorderingStatus(
732  DdManager * unique,
733  Cudd_ReorderingType * method)
734{
735    *method = unique->autoMethod;
736    return(unique->autoDyn);
737
738} /* end of Cudd_ReorderingStatus */
739
740
741/**Function********************************************************************
742
743  Synopsis    [Enables automatic dynamic reordering of ZDDs.]
744
745  Description [Enables automatic dynamic reordering of ZDDs. Parameter
746  method is used to determine the method used for reordering ZDDs. If
747  CUDD_REORDER_SAME is passed, the method is unchanged.]
748
749  SideEffects [None]
750
751  SeeAlso     [Cudd_AutodynDisableZdd Cudd_ReorderingStatusZdd
752  Cudd_AutodynEnable]
753
754******************************************************************************/
755void
756Cudd_AutodynEnableZdd(
757  DdManager * unique,
758  Cudd_ReorderingType method)
759{
760    unique->autoDynZ = 1;
761    if (method != CUDD_REORDER_SAME) {
762        unique->autoMethodZ = method;
763    }
764    return;
765
766} /* end of Cudd_AutodynEnableZdd */
767
768
769/**Function********************************************************************
770
771  Synopsis    [Disables automatic dynamic reordering of ZDDs.]
772
773  Description []
774
775  SideEffects [None]
776
777  SeeAlso     [Cudd_AutodynEnableZdd Cudd_ReorderingStatusZdd
778  Cudd_AutodynDisable]
779
780******************************************************************************/
781void
782Cudd_AutodynDisableZdd(
783  DdManager * unique)
784{
785    unique->autoDynZ = 0;
786    return;
787
788} /* end of Cudd_AutodynDisableZdd */
789
790
791/**Function********************************************************************
792
793  Synopsis    [Reports the status of automatic dynamic reordering of ZDDs.]
794
795  Description [Reports the status of automatic dynamic reordering of
796  ZDDs. Parameter method is set to the ZDD reordering method currently
797  selected. Returns 1 if automatic reordering is enabled; 0
798  otherwise.]
799
800  SideEffects [Parameter method is set to the ZDD reordering method currently
801  selected.]
802
803  SeeAlso     [Cudd_AutodynEnableZdd Cudd_AutodynDisableZdd
804  Cudd_ReorderingStatus]
805
806******************************************************************************/
807int
808Cudd_ReorderingStatusZdd(
809  DdManager * unique,
810  Cudd_ReorderingType * method)
811{
812    *method = unique->autoMethodZ;
813    return(unique->autoDynZ);
814
815} /* end of Cudd_ReorderingStatusZdd */
816
817
818/**Function********************************************************************
819
820  Synopsis    [Tells whether the realignment of ZDD order to BDD order is
821  enabled.]
822
823  Description [Returns 1 if the realignment of ZDD order to BDD order is
824  enabled; 0 otherwise.]
825
826  SideEffects [None]
827
828  SeeAlso     [Cudd_zddRealignEnable Cudd_zddRealignDisable
829  Cudd_bddRealignEnable Cudd_bddRealignDisable]
830
831******************************************************************************/
832int
833Cudd_zddRealignmentEnabled(
834  DdManager * unique)
835{
836    return(unique->realign);
837
838} /* end of Cudd_zddRealignmentEnabled */
839
840
841/**Function********************************************************************
842
843  Synopsis    [Enables realignment of ZDD order to BDD order.]
844
845  Description [Enables realignment of the ZDD variable order to the
846  BDD variable order after the BDDs and ADDs have been reordered.  The
847  number of ZDD variables must be a multiple of the number of BDD
848  variables for realignment to make sense. If this condition is not met,
849  Cudd_ReduceHeap will return 0. Let <code>M</code> be the
850  ratio of the two numbers. For the purpose of realignment, the ZDD
851  variables from <code>M*i</code> to <code>(M+1)*i-1</code> are
852  reagarded as corresponding to BDD variable <code>i</code>. Realignment
853  is initially disabled.]
854
855  SideEffects [None]
856
857  SeeAlso     [Cudd_ReduceHeap Cudd_zddRealignDisable
858  Cudd_zddRealignmentEnabled Cudd_bddRealignDisable
859  Cudd_bddRealignmentEnabled]
860
861******************************************************************************/
862void
863Cudd_zddRealignEnable(
864  DdManager * unique)
865{
866    unique->realign = 1;
867    return;
868
869} /* end of Cudd_zddRealignEnable */
870
871
872/**Function********************************************************************
873
874  Synopsis    [Disables realignment of ZDD order to BDD order.]
875
876  Description []
877
878  SideEffects [None]
879
880  SeeAlso     [Cudd_zddRealignEnable Cudd_zddRealignmentEnabled
881  Cudd_bddRealignEnable Cudd_bddRealignmentEnabled]
882
883******************************************************************************/
884void
885Cudd_zddRealignDisable(
886  DdManager * unique)
887{
888    unique->realign = 0;
889    return;
890
891} /* end of Cudd_zddRealignDisable */
892
893
894/**Function********************************************************************
895
896  Synopsis    [Tells whether the realignment of BDD order to ZDD order is
897  enabled.]
898
899  Description [Returns 1 if the realignment of BDD order to ZDD order is
900  enabled; 0 otherwise.]
901
902  SideEffects [None]
903
904  SeeAlso     [Cudd_bddRealignEnable Cudd_bddRealignDisable
905  Cudd_zddRealignEnable Cudd_zddRealignDisable]
906
907******************************************************************************/
908int
909Cudd_bddRealignmentEnabled(
910  DdManager * unique)
911{
912    return(unique->realignZ);
913
914} /* end of Cudd_bddRealignmentEnabled */
915
916
917/**Function********************************************************************
918
919  Synopsis    [Enables realignment of BDD order to ZDD order.]
920
921  Description [Enables realignment of the BDD variable order to the
922  ZDD variable order after the ZDDs have been reordered.  The
923  number of ZDD variables must be a multiple of the number of BDD
924  variables for realignment to make sense. If this condition is not met,
925  Cudd_zddReduceHeap will return 0. Let <code>M</code> be the
926  ratio of the two numbers. For the purpose of realignment, the ZDD
927  variables from <code>M*i</code> to <code>(M+1)*i-1</code> are
928  reagarded as corresponding to BDD variable <code>i</code>. Realignment
929  is initially disabled.]
930
931  SideEffects [None]
932
933  SeeAlso     [Cudd_zddReduceHeap Cudd_bddRealignDisable
934  Cudd_bddRealignmentEnabled Cudd_zddRealignDisable
935  Cudd_zddRealignmentEnabled]
936
937******************************************************************************/
938void
939Cudd_bddRealignEnable(
940  DdManager * unique)
941{
942    unique->realignZ = 1;
943    return;
944
945} /* end of Cudd_bddRealignEnable */
946
947
948/**Function********************************************************************
949
950  Synopsis    [Disables realignment of ZDD order to BDD order.]
951
952  Description []
953
954  SideEffects [None]
955
956  SeeAlso     [Cudd_bddRealignEnable Cudd_bddRealignmentEnabled
957  Cudd_zddRealignEnable Cudd_zddRealignmentEnabled]
958
959******************************************************************************/
960void
961Cudd_bddRealignDisable(
962  DdManager * unique)
963{
964    unique->realignZ = 0;
965    return;
966
967} /* end of Cudd_bddRealignDisable */
968
969
970/**Function********************************************************************
971
972  Synopsis    [Returns the one constant of the manager.]
973
974  Description [Returns the one constant of the manager. The one
975  constant is common to ADDs and BDDs.]
976
977  SideEffects [None]
978
979  SeeAlso [Cudd_ReadZero Cudd_ReadLogicZero Cudd_ReadZddOne]
980
981******************************************************************************/
982DdNode *
983Cudd_ReadOne(
984  DdManager * dd)
985{
986    return(dd->one);
987
988} /* end of Cudd_ReadOne */
989
990
991/**Function********************************************************************
992
993  Synopsis    [Returns the ZDD for the constant 1 function.]
994
995  Description [Returns the ZDD for the constant 1 function.
996  The representation of the constant 1 function as a ZDD depends on
997  how many variables it (nominally) depends on. The index of the
998  topmost variable in the support is given as argument <code>i</code>.]
999
1000  SideEffects [None]
1001
1002  SeeAlso [Cudd_ReadOne]
1003
1004******************************************************************************/
1005DdNode *
1006Cudd_ReadZddOne(
1007  DdManager * dd,
1008  int  i)
1009{
1010    if (i < 0)
1011        return(NULL);
1012    return(i < dd->sizeZ ? dd->univ[i] : DD_ONE(dd));
1013
1014} /* end of Cudd_ReadZddOne */
1015
1016
1017
1018/**Function********************************************************************
1019
1020  Synopsis    [Returns the zero constant of the manager.]
1021
1022  Description [Returns the zero constant of the manager. The zero
1023  constant is the arithmetic zero, rather than the logic zero. The
1024  latter is the complement of the one constant.]
1025
1026  SideEffects [None]
1027
1028  SeeAlso [Cudd_ReadOne Cudd_ReadLogicZero]
1029
1030******************************************************************************/
1031DdNode *
1032Cudd_ReadZero(
1033  DdManager * dd)
1034{
1035    return(DD_ZERO(dd));
1036
1037} /* end of Cudd_ReadZero */
1038
1039
1040/**Function********************************************************************
1041
1042  Synopsis    [Returns the logic zero constant of the manager.]
1043
1044  Description [Returns the zero constant of the manager. The logic zero
1045  constant is the complement of the one constant, and is distinct from
1046  the arithmetic zero.]
1047
1048  SideEffects [None]
1049
1050  SeeAlso [Cudd_ReadOne Cudd_ReadZero]
1051
1052******************************************************************************/
1053DdNode *
1054Cudd_ReadLogicZero(
1055  DdManager * dd)
1056{
1057    return(Cudd_Not(DD_ONE(dd)));
1058
1059} /* end of Cudd_ReadLogicZero */
1060
1061
1062/**Function********************************************************************
1063
1064  Synopsis    [Reads the plus-infinity constant from the manager.]
1065
1066  Description []
1067
1068  SideEffects [None]
1069
1070******************************************************************************/
1071DdNode *
1072Cudd_ReadPlusInfinity(
1073  DdManager * dd)
1074{
1075    return(dd->plusinfinity);
1076
1077} /* end of Cudd_ReadPlusInfinity */
1078
1079
1080/**Function********************************************************************
1081
1082  Synopsis    [Reads the minus-infinity constant from the manager.]
1083
1084  Description []
1085
1086  SideEffects [None]
1087
1088******************************************************************************/
1089DdNode *
1090Cudd_ReadMinusInfinity(
1091  DdManager * dd)
1092{
1093    return(dd->minusinfinity);
1094
1095} /* end of Cudd_ReadMinusInfinity */
1096
1097
1098/**Function********************************************************************
1099
1100  Synopsis    [Reads the background constant of the manager.]
1101
1102  Description []
1103
1104  SideEffects [None]
1105
1106******************************************************************************/
1107DdNode *
1108Cudd_ReadBackground(
1109  DdManager * dd)
1110{
1111    return(dd->background);
1112
1113} /* end of Cudd_ReadBackground */
1114
1115
1116/**Function********************************************************************
1117
1118  Synopsis    [Sets the background constant of the manager.]
1119
1120  Description [Sets the background constant of the manager. It assumes
1121  that the DdNode pointer bck is already referenced.]
1122
1123  SideEffects [None]
1124
1125******************************************************************************/
1126void
1127Cudd_SetBackground(
1128  DdManager * dd,
1129  DdNode * bck)
1130{
1131    dd->background = bck;
1132
1133} /* end of Cudd_SetBackground */
1134
1135
1136/**Function********************************************************************
1137
1138  Synopsis    [Reads the number of slots in the cache.]
1139
1140  Description []
1141
1142  SideEffects [None]
1143
1144  SeeAlso     [Cudd_ReadCacheUsedSlots]
1145
1146******************************************************************************/
1147unsigned int
1148Cudd_ReadCacheSlots(
1149  DdManager * dd)
1150{
1151    return(dd->cacheSlots);
1152
1153} /* end of Cudd_ReadCacheSlots */
1154
1155
1156/**Function********************************************************************
1157
1158  Synopsis    [Reads the fraction of used slots in the cache.]
1159
1160  Description [Reads the fraction of used slots in the cache. The unused
1161  slots are those in which no valid data is stored. Garbage collection,
1162  variable reordering, and cache resizing may cause used slots to become
1163  unused.]
1164
1165  SideEffects [None]
1166
1167  SeeAlso     [Cudd_ReadCacheSlots]
1168
1169******************************************************************************/
1170double
1171Cudd_ReadCacheUsedSlots(
1172  DdManager * dd)
1173{
1174    unsigned long used = 0;
1175    int slots = dd->cacheSlots;
1176    DdCache *cache = dd->cache;
1177    int i;
1178
1179    for (i = 0; i < slots; i++) {
1180        used += cache[i].h != 0;
1181    }
1182
1183    return((double)used / (double) dd->cacheSlots);
1184
1185} /* end of Cudd_ReadCacheUsedSlots */
1186
1187
1188/**Function********************************************************************
1189
1190  Synopsis    [Returns the number of cache look-ups.]
1191
1192  Description [Returns the number of cache look-ups.]
1193
1194  SideEffects [None]
1195
1196  SeeAlso     [Cudd_ReadCacheHits]
1197
1198******************************************************************************/
1199double
1200Cudd_ReadCacheLookUps(
1201  DdManager * dd)
1202{
1203    return(dd->cacheHits + dd->cacheMisses +
1204           dd->totCachehits + dd->totCacheMisses);
1205
1206} /* end of Cudd_ReadCacheLookUps */
1207
1208
1209/**Function********************************************************************
1210
1211  Synopsis    [Returns the number of cache hits.]
1212
1213  Description []
1214
1215  SideEffects [None]
1216
1217  SeeAlso     [Cudd_ReadCacheLookUps]
1218
1219******************************************************************************/
1220double
1221Cudd_ReadCacheHits(
1222  DdManager * dd)
1223{
1224    return(dd->cacheHits + dd->totCachehits);
1225
1226} /* end of Cudd_ReadCacheHits */
1227
1228
1229/**Function********************************************************************
1230
1231  Synopsis    [Returns the number of recursive calls.]
1232
1233  Description [Returns the number of recursive calls if the package is
1234  compiled with DD_COUNT defined.]
1235
1236  SideEffects [None]
1237
1238  SeeAlso     []
1239
1240******************************************************************************/
1241double
1242Cudd_ReadRecursiveCalls(
1243  DdManager * dd)
1244{
1245#ifdef DD_COUNT
1246    return(dd->recursiveCalls);
1247#else
1248    return(-1.0);
1249#endif
1250
1251} /* end of Cudd_ReadRecursiveCalls */
1252
1253
1254
1255/**Function********************************************************************
1256
1257  Synopsis    [Reads the hit rate that causes resizinig of the computed
1258  table.]
1259
1260  Description []
1261
1262  SideEffects [None]
1263
1264  SeeAlso     [Cudd_SetMinHit]
1265
1266******************************************************************************/
1267unsigned int
1268Cudd_ReadMinHit(
1269  DdManager * dd)
1270{
1271    /* Internally, the package manipulates the ratio of hits to
1272    ** misses instead of the ratio of hits to accesses. */
1273    return((unsigned int) (0.5 + 100 * dd->minHit / (1 + dd->minHit)));
1274
1275} /* end of Cudd_ReadMinHit */
1276
1277
1278/**Function********************************************************************
1279
1280  Synopsis    [Sets the hit rate that causes resizinig of the computed
1281  table.]
1282
1283  Description [Sets the minHit parameter of the manager. This
1284  parameter controls the resizing of the computed table. If the hit
1285  rate is larger than the specified value, and the cache is not
1286  already too large, then its size is doubled.]
1287
1288  SideEffects [None]
1289
1290  SeeAlso     [Cudd_ReadMinHit]
1291
1292******************************************************************************/
1293void
1294Cudd_SetMinHit(
1295  DdManager * dd,
1296  unsigned int hr)
1297{
1298    /* Internally, the package manipulates the ratio of hits to
1299    ** misses instead of the ratio of hits to accesses. */
1300    dd->minHit = (double) hr / (100.0 - (double) hr);
1301
1302} /* end of Cudd_SetMinHit */
1303
1304
1305/**Function********************************************************************
1306
1307  Synopsis    [Reads the looseUpTo parameter of the manager.]
1308
1309  Description []
1310
1311  SideEffects [None]
1312
1313  SeeAlso     [Cudd_SetLooseUpTo Cudd_ReadMinHit Cudd_ReadMinDead]
1314
1315******************************************************************************/
1316unsigned int
1317Cudd_ReadLooseUpTo(
1318  DdManager * dd)
1319{
1320    return(dd->looseUpTo);
1321
1322} /* end of Cudd_ReadLooseUpTo */
1323
1324
1325/**Function********************************************************************
1326
1327  Synopsis    [Sets the looseUpTo parameter of the manager.]
1328
1329  Description [Sets the looseUpTo parameter of the manager. This
1330  parameter of the manager controls the threshold beyond which no fast
1331  growth of the unique table is allowed. The threshold is given as a
1332  number of slots. If the value passed to this function is 0, the
1333  function determines a suitable value based on the available memory.]
1334
1335  SideEffects [None]
1336
1337  SeeAlso     [Cudd_ReadLooseUpTo Cudd_SetMinHit]
1338
1339******************************************************************************/
1340void
1341Cudd_SetLooseUpTo(
1342  DdManager * dd,
1343  unsigned int lut)
1344{
1345    if (lut == 0) {
1346        long datalimit = getSoftDataLimit();
1347        lut = (unsigned int) (datalimit / (sizeof(DdNode) *
1348                                           DD_MAX_LOOSE_FRACTION));
1349    }
1350    dd->looseUpTo = lut;
1351
1352} /* end of Cudd_SetLooseUpTo */
1353
1354
1355/**Function********************************************************************
1356
1357  Synopsis    [Returns the soft limit for the cache size.]
1358
1359  Description [Returns the soft limit for the cache size. The soft limit]
1360
1361  SideEffects [None]
1362
1363  SeeAlso     [Cudd_ReadMaxCache]
1364
1365******************************************************************************/
1366unsigned int
1367Cudd_ReadMaxCache(
1368  DdManager * dd)
1369{
1370    return(2 * dd->cacheSlots + dd->cacheSlack);
1371
1372} /* end of Cudd_ReadMaxCache */
1373
1374
1375/**Function********************************************************************
1376
1377  Synopsis    [Reads the maxCacheHard parameter of the manager.]
1378
1379  Description []
1380
1381  SideEffects [None]
1382
1383  SeeAlso     [Cudd_SetMaxCacheHard Cudd_ReadMaxCache]
1384
1385******************************************************************************/
1386unsigned int
1387Cudd_ReadMaxCacheHard(
1388  DdManager * dd)
1389{
1390    return(dd->maxCacheHard);
1391
1392} /* end of Cudd_ReadMaxCache */
1393
1394
1395/**Function********************************************************************
1396
1397  Synopsis    [Sets the maxCacheHard parameter of the manager.]
1398
1399  Description [Sets the maxCacheHard parameter of the manager. The
1400  cache cannot grow larger than maxCacheHard entries. This parameter
1401  allows an application to control the trade-off of memory versus
1402  speed. If the value passed to this function is 0, the function
1403  determines a suitable maximum cache size based on the available memory.]
1404
1405  SideEffects [None]
1406
1407  SeeAlso     [Cudd_ReadMaxCacheHard Cudd_SetMaxCache]
1408
1409******************************************************************************/
1410void
1411Cudd_SetMaxCacheHard(
1412  DdManager * dd,
1413  unsigned int mc)
1414{
1415    if (mc == 0) {
1416        long datalimit = getSoftDataLimit();
1417        mc = (unsigned int) (datalimit / (sizeof(DdCache) *
1418                                          DD_MAX_CACHE_FRACTION));
1419    }
1420    dd->maxCacheHard = mc;
1421
1422} /* end of Cudd_SetMaxCacheHard */
1423
1424
1425/**Function********************************************************************
1426
1427  Synopsis    [Returns the number of BDD variables in existance.]
1428
1429  Description []
1430
1431  SideEffects [None]
1432
1433  SeeAlso     [Cudd_ReadZddSize]
1434
1435******************************************************************************/
1436int
1437Cudd_ReadSize(
1438  DdManager * dd)
1439{
1440    return(dd->size);
1441
1442} /* end of Cudd_ReadSize */
1443
1444
1445/**Function********************************************************************
1446
1447  Synopsis    [Returns the number of ZDD variables in existance.]
1448
1449  Description []
1450
1451  SideEffects [None]
1452
1453  SeeAlso     [Cudd_ReadSize]
1454
1455******************************************************************************/
1456int
1457Cudd_ReadZddSize(
1458  DdManager * dd)
1459{
1460    return(dd->sizeZ);
1461
1462} /* end of Cudd_ReadZddSize */
1463
1464
1465/**Function********************************************************************
1466
1467  Synopsis    [Returns the total number of slots of the unique table.]
1468
1469  Description [Returns the total number of slots of the unique table.
1470  This number ismainly for diagnostic purposes.]
1471
1472  SideEffects [None]
1473
1474******************************************************************************/
1475unsigned int
1476Cudd_ReadSlots(
1477  DdManager * dd)
1478{
1479    return(dd->slots);
1480
1481} /* end of Cudd_ReadSlots */
1482
1483
1484/**Function********************************************************************
1485
1486  Synopsis    [Reads the fraction of used slots in the unique table.]
1487
1488  Description [Reads the fraction of used slots in the unique
1489  table. The unused slots are those in which no valid data is
1490  stored. Garbage collection, variable reordering, and subtable
1491  resizing may cause used slots to become unused.]
1492
1493  SideEffects [None]
1494
1495  SeeAlso     [Cudd_ReadSlots]
1496
1497******************************************************************************/
1498double
1499Cudd_ReadUsedSlots(
1500  DdManager * dd)
1501{
1502    unsigned long used = 0;
1503    int i, j;
1504    int size = dd->size;
1505    DdNodePtr *nodelist;
1506    DdSubtable *subtable;
1507    DdNode *node;
1508    DdNode *sentinel = &(dd->sentinel);
1509
1510    /* Scan each BDD/ADD subtable. */
1511    for (i = 0; i < size; i++) {
1512        subtable = &(dd->subtables[i]);
1513        nodelist = subtable->nodelist;
1514        for (j = 0; (unsigned) j < subtable->slots; j++) {
1515            node = nodelist[j];
1516            if (node != sentinel) {
1517                used++;
1518            }
1519        }
1520    }
1521
1522    /* Scan the ZDD subtables. */
1523    size = dd->sizeZ;
1524
1525    for (i = 0; i < size; i++) {
1526        subtable = &(dd->subtableZ[i]);
1527        nodelist = subtable->nodelist;
1528        for (j = 0; (unsigned) j < subtable->slots; j++) {
1529            node = nodelist[j];
1530            if (node != NULL) {
1531                used++;
1532            }
1533        }
1534    }
1535
1536    /* Constant table. */
1537    subtable = &(dd->constants);
1538    nodelist = subtable->nodelist;
1539    for (j = 0; (unsigned) j < subtable->slots; j++) {
1540        node = nodelist[j];
1541        if (node != NULL) {
1542            used++;
1543        }
1544    }
1545
1546    return((double)used / (double) dd->slots);
1547
1548} /* end of Cudd_ReadUsedSlots */
1549
1550
1551/**Function********************************************************************
1552
1553  Synopsis    [Computes the expected fraction of used slots in the unique
1554  table.]
1555
1556  Description [Computes the fraction of slots in the unique table that
1557  should be in use. This expected value is based on the assumption
1558  that the hash function distributes the keys randomly; it can be
1559  compared with the result of Cudd_ReadUsedSlots to monitor the
1560  performance of the unique table hash function.]
1561
1562  SideEffects [None]
1563
1564  SeeAlso     [Cudd_ReadSlots Cudd_ReadUsedSlots]
1565
1566******************************************************************************/
1567double
1568Cudd_ExpectedUsedSlots(
1569  DdManager * dd)
1570{
1571    int i;
1572    int size = dd->size;
1573    DdSubtable *subtable;
1574    double empty = 0.0;
1575
1576    /* To each subtable we apply the corollary to Theorem 8.5 (occupancy
1577    ** distribution) from Sedgewick and Flajolet's Analysis of Algorithms.
1578    ** The corollary says that for a a table with M buckets and a load ratio
1579    ** of r, the expected number of empty buckets is asymptotically given
1580    ** by M * exp(-r).
1581    */
1582
1583    /* Scan each BDD/ADD subtable. */
1584    for (i = 0; i < size; i++) {
1585        subtable = &(dd->subtables[i]);
1586        empty += (double) subtable->slots *
1587            exp(-(double) subtable->keys / (double) subtable->slots);
1588    }
1589
1590    /* Scan the ZDD subtables. */
1591    size = dd->sizeZ;
1592
1593    for (i = 0; i < size; i++) {
1594        subtable = &(dd->subtableZ[i]);
1595        empty += (double) subtable->slots *
1596            exp(-(double) subtable->keys / (double) subtable->slots);
1597    }
1598
1599    /* Constant table. */
1600    subtable = &(dd->constants);
1601    empty += (double) subtable->slots *
1602        exp(-(double) subtable->keys / (double) subtable->slots);
1603
1604    return(1.0 - empty / (double) dd->slots);
1605
1606} /* end of Cudd_ExpectedUsedSlots */
1607
1608
1609/**Function********************************************************************
1610
1611  Synopsis    [Returns the number of nodes in the unique table.]
1612
1613  Description [Returns the total number of nodes currently in the unique
1614  table, including the dead nodes.]
1615
1616  SideEffects [None]
1617
1618  SeeAlso     [Cudd_ReadDead]
1619
1620******************************************************************************/
1621unsigned int
1622Cudd_ReadKeys(
1623  DdManager * dd)
1624{
1625    return(dd->keys);
1626
1627} /* end of Cudd_ReadKeys */
1628
1629
1630/**Function********************************************************************
1631
1632  Synopsis    [Returns the number of dead nodes in the unique table.]
1633
1634  Description []
1635
1636  SideEffects [None]
1637
1638  SeeAlso     [Cudd_ReadKeys]
1639
1640******************************************************************************/
1641unsigned int
1642Cudd_ReadDead(
1643  DdManager * dd)
1644{
1645    return(dd->dead);
1646
1647} /* end of Cudd_ReadDead */
1648
1649
1650/**Function********************************************************************
1651
1652  Synopsis    [Reads the minDead parameter of the manager.]
1653
1654  Description [Reads the minDead parameter of the manager. The minDead
1655  parameter is used by the package to decide whether to collect garbage
1656  or resize a subtable of the unique table when the subtable becomes
1657  too full. The application can indirectly control the value of minDead
1658  by setting the looseUpTo parameter.]
1659
1660  SideEffects [None]
1661
1662  SeeAlso     [Cudd_ReadDead Cudd_ReadLooseUpTo Cudd_SetLooseUpTo]
1663
1664******************************************************************************/
1665unsigned int
1666Cudd_ReadMinDead(
1667  DdManager * dd)
1668{
1669    return(dd->minDead);
1670
1671} /* end of Cudd_ReadMinDead */
1672
1673
1674/**Function********************************************************************
1675
1676  Synopsis    [Returns the number of times reordering has occurred.]
1677
1678  Description [Returns the number of times reordering has occurred in the
1679  manager. The number includes both the calls to Cudd_ReduceHeap from
1680  the application program and those automatically performed by the
1681  package. However, calls that do not even initiate reordering are not
1682  counted. A call may not initiate reordering if there are fewer than
1683  minsize live nodes in the manager, or if CUDD_REORDER_NONE is specified
1684  as reordering method. The calls to Cudd_ShuffleHeap are not counted.]
1685
1686  SideEffects [None]
1687
1688  SeeAlso [Cudd_ReduceHeap Cudd_ReadReorderingTime]
1689
1690******************************************************************************/
1691int
1692Cudd_ReadReorderings(
1693  DdManager * dd)
1694{
1695    return(dd->reorderings);
1696
1697} /* end of Cudd_ReadReorderings */
1698
1699
1700/**Function********************************************************************
1701
1702  Synopsis    [Returns the time spent in reordering.]
1703
1704  Description [Returns the number of milliseconds spent reordering
1705  variables since the manager was initialized. The time spent in collecting
1706  garbage before reordering is included.]
1707
1708  SideEffects [None]
1709
1710  SeeAlso     [Cudd_ReadReorderings]
1711
1712******************************************************************************/
1713long
1714Cudd_ReadReorderingTime(
1715  DdManager * dd)
1716{
1717    return(dd->reordTime);
1718
1719} /* end of Cudd_ReadReorderingTime */
1720
1721
1722/**Function********************************************************************
1723
1724  Synopsis    [Returns the number of times garbage collection has occurred.]
1725
1726  Description [Returns the number of times garbage collection has
1727  occurred in the manager. The number includes both the calls from
1728  reordering procedures and those caused by requests to create new
1729  nodes.]
1730
1731  SideEffects [None]
1732
1733  SeeAlso     [Cudd_ReadGarbageCollectionTime]
1734
1735******************************************************************************/
1736int
1737Cudd_ReadGarbageCollections(
1738  DdManager * dd)
1739{
1740    return(dd->garbageCollections);
1741
1742} /* end of Cudd_ReadGarbageCollections */
1743
1744
1745/**Function********************************************************************
1746
1747  Synopsis    [Returns the time spent in garbage collection.]
1748
1749  Description [Returns the number of milliseconds spent doing garbage
1750  collection since the manager was initialized.]
1751
1752  SideEffects [None]
1753
1754  SeeAlso     [Cudd_ReadGarbageCollections]
1755
1756******************************************************************************/
1757long
1758Cudd_ReadGarbageCollectionTime(
1759  DdManager * dd)
1760{
1761    return(dd->GCTime);
1762
1763} /* end of Cudd_ReadGarbageCollectionTime */
1764
1765
1766/**Function********************************************************************
1767
1768  Synopsis    [Returns the number of nodes freed.]
1769
1770  Description [Returns the number of nodes returned to the free list if the
1771  keeping of this statistic is enabled; -1 otherwise. This statistic is
1772  enabled only if the package is compiled with DD_STATS defined.]
1773
1774  SideEffects [None]
1775
1776  SeeAlso     [Cudd_ReadNodesDropped]
1777
1778******************************************************************************/
1779double
1780Cudd_ReadNodesFreed(
1781  DdManager * dd)
1782{
1783#ifdef DD_STATS
1784    return(dd->nodesFreed);
1785#else
1786    return(-1.0);
1787#endif
1788
1789} /* end of Cudd_ReadNodesFreed */
1790
1791
1792/**Function********************************************************************
1793
1794  Synopsis    [Returns the number of nodes dropped.]
1795
1796  Description [Returns the number of nodes killed by dereferencing if the
1797  keeping of this statistic is enabled; -1 otherwise. This statistic is
1798  enabled only if the package is compiled with DD_STATS defined.]
1799
1800  SideEffects [None]
1801
1802  SeeAlso     [Cudd_ReadNodesFreed]
1803
1804******************************************************************************/
1805double
1806Cudd_ReadNodesDropped(
1807  DdManager * dd)
1808{
1809#ifdef DD_STATS
1810    return(dd->nodesDropped);
1811#else
1812    return(-1.0);
1813#endif
1814
1815} /* end of Cudd_ReadNodesDropped */
1816
1817
1818/**Function********************************************************************
1819
1820  Synopsis    [Returns the number of look-ups in the unique table.]
1821
1822  Description [Returns the number of look-ups in the unique table if the
1823  keeping of this statistic is enabled; -1 otherwise. This statistic is
1824  enabled only if the package is compiled with DD_UNIQUE_PROFILE defined.]
1825
1826  SideEffects [None]
1827
1828  SeeAlso     [Cudd_ReadUniqueLinks]
1829
1830******************************************************************************/
1831double
1832Cudd_ReadUniqueLookUps(
1833  DdManager * dd)
1834{
1835#ifdef DD_UNIQUE_PROFILE
1836    return(dd->uniqueLookUps);
1837#else
1838    return(-1.0);
1839#endif
1840
1841} /* end of Cudd_ReadUniqueLookUps */
1842
1843
1844/**Function********************************************************************
1845
1846  Synopsis    [Returns the number of links followed in the unique table.]
1847
1848  Description [Returns the number of links followed during look-ups in the
1849  unique table if the keeping of this statistic is enabled; -1 otherwise.
1850  If an item is found in the first position of its collision list, the
1851  number of links followed is taken to be 0. If it is in second position,
1852  the number of links is 1, and so on. This statistic is enabled only if
1853  the package is compiled with DD_UNIQUE_PROFILE defined.]
1854
1855  SideEffects [None]
1856
1857  SeeAlso     [Cudd_ReadUniqueLookUps]
1858
1859******************************************************************************/
1860double
1861Cudd_ReadUniqueLinks(
1862  DdManager * dd)
1863{
1864#ifdef DD_UNIQUE_PROFILE
1865    return(dd->uniqueLinks);
1866#else
1867    return(-1.0);
1868#endif
1869
1870} /* end of Cudd_ReadUniqueLinks */
1871
1872
1873/**Function********************************************************************
1874
1875  Synopsis    [Reads the siftMaxVar parameter of the manager.]
1876
1877  Description [Reads the siftMaxVar parameter of the manager. This
1878  parameter gives the maximum number of variables that will be sifted
1879  for each invocation of sifting.]
1880
1881  SideEffects [None]
1882
1883  SeeAlso     [Cudd_ReadSiftMaxSwap Cudd_SetSiftMaxVar]
1884
1885******************************************************************************/
1886int
1887Cudd_ReadSiftMaxVar(
1888  DdManager * dd)
1889{
1890    return(dd->siftMaxVar);
1891
1892} /* end of Cudd_ReadSiftMaxVar */
1893
1894
1895/**Function********************************************************************
1896
1897  Synopsis    [Sets the siftMaxVar parameter of the manager.]
1898
1899  Description [Sets the siftMaxVar parameter of the manager. This
1900  parameter gives the maximum number of variables that will be sifted
1901  for each invocation of sifting.]
1902
1903  SideEffects [None]
1904
1905  SeeAlso     [Cudd_SetSiftMaxSwap Cudd_ReadSiftMaxVar]
1906
1907******************************************************************************/
1908void
1909Cudd_SetSiftMaxVar(
1910  DdManager * dd,
1911  int  smv)
1912{
1913    dd->siftMaxVar = smv;
1914
1915} /* end of Cudd_SetSiftMaxVar */
1916
1917
1918/**Function********************************************************************
1919
1920  Synopsis    [Reads the siftMaxSwap parameter of the manager.]
1921
1922  Description [Reads the siftMaxSwap parameter of the manager. This
1923  parameter gives the maximum number of swaps that will be attempted
1924  for each invocation of sifting. The real number of swaps may exceed
1925  the set limit because the package will always complete the sifting
1926  of the variable that causes the limit to be reached.]
1927
1928  SideEffects [None]
1929
1930  SeeAlso     [Cudd_ReadSiftMaxVar Cudd_SetSiftMaxSwap]
1931
1932******************************************************************************/
1933int
1934Cudd_ReadSiftMaxSwap(
1935  DdManager * dd)
1936{
1937    return(dd->siftMaxSwap);
1938
1939} /* end of Cudd_ReadSiftMaxSwap */
1940
1941
1942/**Function********************************************************************
1943
1944  Synopsis    [Sets the siftMaxSwap parameter of the manager.]
1945
1946  Description [Sets the siftMaxSwap parameter of the manager. This
1947  parameter gives the maximum number of swaps that will be attempted
1948  for each invocation of sifting. The real number of swaps may exceed
1949  the set limit because the package will always complete the sifting
1950  of the variable that causes the limit to be reached.]
1951
1952  SideEffects [None]
1953
1954  SeeAlso     [Cudd_SetSiftMaxVar Cudd_ReadSiftMaxSwap]
1955
1956******************************************************************************/
1957void
1958Cudd_SetSiftMaxSwap(
1959  DdManager * dd,
1960  int  sms)
1961{
1962    dd->siftMaxSwap = sms;
1963
1964} /* end of Cudd_SetSiftMaxSwap */
1965
1966
1967/**Function********************************************************************
1968
1969  Synopsis    [Reads the maxGrowth parameter of the manager.]
1970
1971  Description [Reads the maxGrowth parameter of the manager.  This
1972  parameter determines how much the number of nodes can grow during
1973  sifting of a variable.  Overall, sifting never increases the size of
1974  the decision diagrams.  This parameter only refers to intermediate
1975  results.  A lower value will speed up sifting, possibly at the
1976  expense of quality.]
1977
1978  SideEffects [None]
1979
1980  SeeAlso     [Cudd_SetMaxGrowth Cudd_ReadMaxGrowthAlternate]
1981
1982******************************************************************************/
1983double
1984Cudd_ReadMaxGrowth(
1985  DdManager * dd)
1986{
1987    return(dd->maxGrowth);
1988
1989} /* end of Cudd_ReadMaxGrowth */
1990
1991
1992/**Function********************************************************************
1993
1994  Synopsis    [Sets the maxGrowth parameter of the manager.]
1995
1996  Description [Sets the maxGrowth parameter of the manager.  This
1997  parameter determines how much the number of nodes can grow during
1998  sifting of a variable.  Overall, sifting never increases the size of
1999  the decision diagrams.  This parameter only refers to intermediate
2000  results.  A lower value will speed up sifting, possibly at the
2001  expense of quality.]
2002
2003  SideEffects [None]
2004
2005  SeeAlso     [Cudd_ReadMaxGrowth Cudd_SetMaxGrowthAlternate]
2006
2007******************************************************************************/
2008void
2009Cudd_SetMaxGrowth(
2010  DdManager * dd,
2011  double mg)
2012{
2013    dd->maxGrowth = mg;
2014
2015} /* end of Cudd_SetMaxGrowth */
2016
2017
2018/**Function********************************************************************
2019
2020  Synopsis    [Reads the maxGrowthAlt parameter of the manager.]
2021
2022  Description [Reads the maxGrowthAlt parameter of the manager.  This
2023  parameter is analogous to the maxGrowth paramter, and is used every
2024  given number of reorderings instead of maxGrowth.  The number of
2025  reorderings is set with Cudd_SetReorderingCycle.  If the number of
2026  reorderings is 0 (default) maxGrowthAlt is never used.]
2027
2028  SideEffects [None]
2029
2030  SeeAlso     [Cudd_ReadMaxGrowth Cudd_SetMaxGrowthAlternate
2031  Cudd_SetReorderingCycle Cudd_ReadReorderingCycle]
2032
2033******************************************************************************/
2034double
2035Cudd_ReadMaxGrowthAlternate(
2036  DdManager * dd)
2037{
2038    return(dd->maxGrowthAlt);
2039
2040} /* end of Cudd_ReadMaxGrowthAlternate */
2041
2042
2043/**Function********************************************************************
2044
2045  Synopsis    [Sets the maxGrowthAlt parameter of the manager.]
2046
2047  Description [Sets the maxGrowthAlt parameter of the manager.  This
2048  parameter is analogous to the maxGrowth paramter, and is used every
2049  given number of reorderings instead of maxGrowth.  The number of
2050  reorderings is set with Cudd_SetReorderingCycle.  If the number of
2051  reorderings is 0 (default) maxGrowthAlt is never used.]
2052
2053  SideEffects [None]
2054
2055  SeeAlso     [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowth
2056  Cudd_SetReorderingCycle Cudd_ReadReorderingCycle]
2057
2058******************************************************************************/
2059void
2060Cudd_SetMaxGrowthAlternate(
2061  DdManager * dd,
2062  double mg)
2063{
2064    dd->maxGrowthAlt = mg;
2065
2066} /* end of Cudd_SetMaxGrowthAlternate */
2067
2068
2069/**Function********************************************************************
2070
2071  Synopsis    [Reads the reordCycle parameter of the manager.]
2072
2073  Description [Reads the reordCycle parameter of the manager.  This
2074  parameter determines how often the alternate threshold on maximum
2075  growth is used in reordering.]
2076
2077  SideEffects [None]
2078
2079  SeeAlso     [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowthAlternate
2080  Cudd_SetReorderingCycle]
2081
2082******************************************************************************/
2083int
2084Cudd_ReadReorderingCycle(
2085  DdManager * dd)
2086{
2087    return(dd->reordCycle);
2088
2089} /* end of Cudd_ReadReorderingCycle */
2090
2091
2092/**Function********************************************************************
2093
2094  Synopsis    [Sets the reordCycle parameter of the manager.]
2095
2096  Description [Sets the reordCycle parameter of the manager.  This
2097  parameter determines how often the alternate threshold on maximum
2098  growth is used in reordering.]
2099
2100  SideEffects [None]
2101
2102  SeeAlso     [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowthAlternate
2103  Cudd_ReadReorderingCycle]
2104
2105******************************************************************************/
2106void
2107Cudd_SetReorderingCycle(
2108  DdManager * dd,
2109  int cycle)
2110{
2111    dd->reordCycle = cycle;
2112
2113} /* end of Cudd_SetReorderingCycle */
2114
2115
2116/**Function********************************************************************
2117
2118  Synopsis    [Returns the variable group tree of the manager.]
2119
2120  Description []
2121
2122  SideEffects [None]
2123
2124  SeeAlso     [Cudd_SetTree Cudd_FreeTree Cudd_ReadZddTree]
2125
2126******************************************************************************/
2127MtrNode *
2128Cudd_ReadTree(
2129  DdManager * dd)
2130{
2131    return(dd->tree);
2132
2133} /* end of Cudd_ReadTree */
2134
2135
2136/**Function********************************************************************
2137
2138  Synopsis    [Sets the variable group tree of the manager.]
2139
2140  Description []
2141
2142  SideEffects [None]
2143
2144  SeeAlso     [Cudd_FreeTree Cudd_ReadTree Cudd_SetZddTree]
2145
2146******************************************************************************/
2147void
2148Cudd_SetTree(
2149  DdManager * dd,
2150  MtrNode * tree)
2151{
2152    if (dd->tree != NULL) {
2153        Mtr_FreeTree(dd->tree);
2154    }
2155    dd->tree = tree;
2156    if (tree == NULL) return;
2157
2158    fixVarTree(tree, dd->perm, dd->size);
2159    return;
2160
2161} /* end of Cudd_SetTree */
2162
2163
2164/**Function********************************************************************
2165
2166  Synopsis    [Frees the variable group tree of the manager.]
2167
2168  Description []
2169
2170  SideEffects [None]
2171
2172  SeeAlso     [Cudd_SetTree Cudd_ReadTree Cudd_FreeZddTree]
2173
2174******************************************************************************/
2175void
2176Cudd_FreeTree(
2177  DdManager * dd)
2178{
2179    if (dd->tree != NULL) {
2180        Mtr_FreeTree(dd->tree);
2181        dd->tree = NULL;
2182    }
2183    return;
2184
2185} /* end of Cudd_FreeTree */
2186
2187
2188/**Function********************************************************************
2189
2190  Synopsis    [Returns the variable group tree of the manager.]
2191
2192  Description []
2193
2194  SideEffects [None]
2195
2196  SeeAlso     [Cudd_SetZddTree Cudd_FreeZddTree Cudd_ReadTree]
2197
2198******************************************************************************/
2199MtrNode *
2200Cudd_ReadZddTree(
2201  DdManager * dd)
2202{
2203    return(dd->treeZ);
2204
2205} /* end of Cudd_ReadZddTree */
2206
2207
2208/**Function********************************************************************
2209
2210  Synopsis    [Sets the ZDD variable group tree of the manager.]
2211
2212  Description []
2213
2214  SideEffects [None]
2215
2216  SeeAlso     [Cudd_FreeZddTree Cudd_ReadZddTree Cudd_SetTree]
2217
2218******************************************************************************/
2219void
2220Cudd_SetZddTree(
2221  DdManager * dd,
2222  MtrNode * tree)
2223{
2224    if (dd->treeZ != NULL) {
2225        Mtr_FreeTree(dd->treeZ);
2226    }
2227    dd->treeZ = tree;
2228    if (tree == NULL) return;
2229
2230    fixVarTree(tree, dd->permZ, dd->sizeZ);
2231    return;
2232
2233} /* end of Cudd_SetZddTree */
2234
2235
2236/**Function********************************************************************
2237
2238  Synopsis    [Frees the variable group tree of the manager.]
2239
2240  Description []
2241
2242  SideEffects [None]
2243
2244  SeeAlso     [Cudd_SetZddTree Cudd_ReadZddTree Cudd_FreeTree]
2245
2246******************************************************************************/
2247void
2248Cudd_FreeZddTree(
2249  DdManager * dd)
2250{
2251    if (dd->treeZ != NULL) {
2252        Mtr_FreeTree(dd->treeZ);
2253        dd->treeZ = NULL;
2254    }
2255    return;
2256
2257} /* end of Cudd_FreeZddTree */
2258
2259
2260/**Function********************************************************************
2261
2262  Synopsis    [Returns the index of the node.]
2263
2264  Description [Returns the index of the node. The node pointer can be
2265  either regular or complemented.]
2266
2267  SideEffects [None]
2268
2269  SeeAlso [Cudd_ReadIndex]
2270
2271******************************************************************************/
2272unsigned int
2273Cudd_NodeReadIndex(
2274  DdNode * node)
2275{
2276    return((unsigned int) Cudd_Regular(node)->index);
2277
2278} /* end of Cudd_NodeReadIndex */
2279
2280
2281/**Function********************************************************************
2282
2283  Synopsis    [Returns the current position of the i-th variable in the
2284  order.]
2285
2286  Description [Returns the current position of the i-th variable in
2287  the order. If the index is CUDD_CONST_INDEX, returns
2288  CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns
2289  -1.]
2290
2291  SideEffects [None]
2292
2293  SeeAlso     [Cudd_ReadInvPerm Cudd_ReadPermZdd]
2294
2295******************************************************************************/
2296int
2297Cudd_ReadPerm(
2298  DdManager * dd,
2299  int  i)
2300{
2301    if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
2302    if (i < 0 || i >= dd->size) return(-1);
2303    return(dd->perm[i]);
2304
2305} /* end of Cudd_ReadPerm */
2306
2307
2308/**Function********************************************************************
2309
2310  Synopsis    [Returns the current position of the i-th ZDD variable in the
2311  order.]
2312
2313  Description [Returns the current position of the i-th ZDD variable
2314  in the order. If the index is CUDD_CONST_INDEX, returns
2315  CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns
2316  -1.]
2317
2318  SideEffects [None]
2319
2320  SeeAlso     [Cudd_ReadInvPermZdd Cudd_ReadPerm]
2321
2322******************************************************************************/
2323int
2324Cudd_ReadPermZdd(
2325  DdManager * dd,
2326  int  i)
2327{
2328    if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
2329    if (i < 0 || i >= dd->sizeZ) return(-1);
2330    return(dd->permZ[i]);
2331
2332} /* end of Cudd_ReadPermZdd */
2333
2334
2335/**Function********************************************************************
2336
2337  Synopsis    [Returns the index of the variable currently in the i-th
2338  position of the order.]
2339
2340  Description [Returns the index of the variable currently in the i-th
2341  position of the order. If the index is CUDD_CONST_INDEX, returns
2342  CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.]
2343
2344  SideEffects [None]
2345
2346  SeeAlso     [Cudd_ReadPerm Cudd_ReadInvPermZdd]
2347
2348******************************************************************************/
2349int
2350Cudd_ReadInvPerm(
2351  DdManager * dd,
2352  int  i)
2353{
2354    if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
2355    if (i < 0 || i >= dd->size) return(-1);
2356    return(dd->invperm[i]);
2357
2358} /* end of Cudd_ReadInvPerm */
2359
2360
2361/**Function********************************************************************
2362
2363  Synopsis    [Returns the index of the ZDD variable currently in the i-th
2364  position of the order.]
2365
2366  Description [Returns the index of the ZDD variable currently in the
2367  i-th position of the order. If the index is CUDD_CONST_INDEX, returns
2368  CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.]
2369
2370  SideEffects [None]
2371
2372  SeeAlso     [Cudd_ReadPerm Cudd_ReadInvPermZdd]
2373
2374******************************************************************************/
2375int
2376Cudd_ReadInvPermZdd(
2377  DdManager * dd,
2378  int  i)
2379{
2380    if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
2381    if (i < 0 || i >= dd->sizeZ) return(-1);
2382    return(dd->invpermZ[i]);
2383
2384} /* end of Cudd_ReadInvPermZdd */
2385
2386
2387/**Function********************************************************************
2388
2389  Synopsis    [Returns the i-th element of the vars array.]
2390
2391  Description [Returns the i-th element of the vars array if it falls
2392  within the array bounds; NULL otherwise. If i is the index of an
2393  existing variable, this function produces the same result as
2394  Cudd_bddIthVar. However, if the i-th var does not exist yet,
2395  Cudd_bddIthVar will create it, whereas Cudd_ReadVars will not.]
2396
2397  SideEffects [None]
2398
2399  SeeAlso     [Cudd_bddIthVar]
2400
2401******************************************************************************/
2402DdNode *
2403Cudd_ReadVars(
2404  DdManager * dd,
2405  int  i)
2406{
2407    if (i < 0 || i > dd->size) return(NULL);
2408    return(dd->vars[i]);
2409
2410} /* end of Cudd_ReadVars */
2411
2412
2413/**Function********************************************************************
2414
2415  Synopsis    [Reads the epsilon parameter of the manager.]
2416
2417  Description [Reads the epsilon parameter of the manager. The epsilon
2418  parameter control the comparison between floating point numbers.]
2419
2420  SideEffects [None]
2421
2422  SeeAlso     [Cudd_SetEpsilon]
2423
2424******************************************************************************/
2425CUDD_VALUE_TYPE
2426Cudd_ReadEpsilon(
2427  DdManager * dd)
2428{
2429    return(dd->epsilon);
2430
2431} /* end of Cudd_ReadEpsilon */
2432
2433
2434/**Function********************************************************************
2435
2436  Synopsis    [Sets the epsilon parameter of the manager to ep.]
2437
2438  Description [Sets the epsilon parameter of the manager to ep. The epsilon
2439  parameter control the comparison between floating point numbers.]
2440
2441  SideEffects [None]
2442
2443  SeeAlso     [Cudd_ReadEpsilon]
2444
2445******************************************************************************/
2446void
2447Cudd_SetEpsilon(
2448  DdManager * dd,
2449  CUDD_VALUE_TYPE  ep)
2450{
2451    dd->epsilon = ep;
2452
2453} /* end of Cudd_SetEpsilon */
2454
2455
2456/**Function********************************************************************
2457
2458  Synopsis    [Reads the groupcheck parameter of the manager.]
2459
2460  Description [Reads the groupcheck parameter of the manager. The
2461  groupcheck parameter determines the aggregation criterion in group
2462  sifting.]
2463
2464  SideEffects [None]
2465
2466  SeeAlso     [Cudd_SetGroupcheck]
2467
2468******************************************************************************/
2469Cudd_AggregationType
2470Cudd_ReadGroupcheck(
2471  DdManager * dd)
2472{
2473    return(dd->groupcheck);
2474
2475} /* end of Cudd_ReadGroupCheck */
2476
2477
2478/**Function********************************************************************
2479
2480  Synopsis    [Sets the parameter groupcheck of the manager to gc.]
2481
2482  Description [Sets the parameter groupcheck of the manager to gc. The
2483  groupcheck parameter determines the aggregation criterion in group
2484  sifting.]
2485
2486  SideEffects [None]
2487
2488  SeeAlso     [Cudd_ReadGroupCheck]
2489
2490******************************************************************************/
2491void
2492Cudd_SetGroupcheck(
2493  DdManager * dd,
2494  Cudd_AggregationType gc)
2495{
2496    dd->groupcheck = gc;
2497
2498} /* end of Cudd_SetGroupcheck */
2499
2500
2501/**Function********************************************************************
2502
2503  Synopsis    [Tells whether garbage collection is enabled.]
2504
2505  Description [Returns 1 if garbage collection is enabled; 0 otherwise.]
2506
2507  SideEffects [None]
2508
2509  SeeAlso     [Cudd_EnableGarbageCollection Cudd_DisableGarbageCollection]
2510
2511******************************************************************************/
2512int
2513Cudd_GarbageCollectionEnabled(
2514  DdManager * dd)
2515{
2516    return(dd->gcEnabled);
2517
2518} /* end of Cudd_GarbageCollectionEnabled */
2519
2520
2521/**Function********************************************************************
2522
2523  Synopsis    [Enables garbage collection.]
2524
2525  Description [Enables garbage collection. Garbage collection is
2526  initially enabled. Therefore it is necessary to call this function
2527  only if garbage collection has been explicitly disabled.]
2528
2529  SideEffects [None]
2530
2531  SeeAlso     [Cudd_DisableGarbageCollection Cudd_GarbageCollectionEnabled]
2532
2533******************************************************************************/
2534void
2535Cudd_EnableGarbageCollection(
2536  DdManager * dd)
2537{
2538    dd->gcEnabled = 1;
2539
2540} /* end of Cudd_EnableGarbageCollection */
2541
2542
2543/**Function********************************************************************
2544
2545  Synopsis    [Disables garbage collection.]
2546
2547  Description [Disables garbage collection. Garbage collection is
2548  initially enabled. This function may be called to disable it.
2549  However, garbage collection will still occur when a new node must be
2550  created and no memory is left, or when garbage collection is required
2551  for correctness. (E.g., before reordering.)]
2552
2553  SideEffects [None]
2554
2555  SeeAlso     [Cudd_EnableGarbageCollection Cudd_GarbageCollectionEnabled]
2556
2557******************************************************************************/
2558void
2559Cudd_DisableGarbageCollection(
2560  DdManager * dd)
2561{
2562    dd->gcEnabled = 0;
2563
2564} /* end of Cudd_DisableGarbageCollection */
2565
2566
2567/**Function********************************************************************
2568
2569  Synopsis    [Tells whether dead nodes are counted towards triggering
2570  reordering.]
2571
2572  Description [Tells whether dead nodes are counted towards triggering
2573  reordering. Returns 1 if dead nodes are counted; 0 otherwise.]
2574
2575  SideEffects [None]
2576
2577  SeeAlso     [Cudd_TurnOnCountDead Cudd_TurnOffCountDead]
2578
2579******************************************************************************/
2580int
2581Cudd_DeadAreCounted(
2582  DdManager * dd)
2583{
2584    return(dd->countDead == 0 ? 1 : 0);
2585
2586} /* end of Cudd_DeadAreCounted */
2587
2588
2589/**Function********************************************************************
2590
2591  Synopsis    [Causes the dead nodes to be counted towards triggering
2592  reordering.]
2593
2594  Description [Causes the dead nodes to be counted towards triggering
2595  reordering. This causes more frequent reorderings. By default dead
2596  nodes are not counted.]
2597
2598  SideEffects [Changes the manager.]
2599
2600  SeeAlso     [Cudd_TurnOffCountDead Cudd_DeadAreCounted]
2601
2602******************************************************************************/
2603void
2604Cudd_TurnOnCountDead(
2605  DdManager * dd)
2606{
2607    dd->countDead = 0;
2608
2609} /* end of Cudd_TurnOnCountDead */
2610
2611
2612/**Function********************************************************************
2613
2614  Synopsis    [Causes the dead nodes not to be counted towards triggering
2615  reordering.]
2616
2617  Description [Causes the dead nodes not to be counted towards
2618  triggering reordering. This causes less frequent reorderings. By
2619  default dead nodes are not counted. Therefore there is no need to
2620  call this function unless Cudd_TurnOnCountDead has been previously
2621  called.]
2622
2623  SideEffects [Changes the manager.]
2624
2625  SeeAlso     [Cudd_TurnOnCountDead Cudd_DeadAreCounted]
2626
2627******************************************************************************/
2628void
2629Cudd_TurnOffCountDead(
2630  DdManager * dd)
2631{
2632    dd->countDead = ~0;
2633
2634} /* end of Cudd_TurnOffCountDead */
2635
2636
2637/**Function********************************************************************
2638
2639  Synopsis    [Returns the current value of the recombination parameter used
2640  in group sifting.]
2641
2642  Description [Returns the current value of the recombination
2643  parameter used in group sifting. A larger (positive) value makes the
2644  aggregation of variables due to the second difference criterion more
2645  likely. A smaller (negative) value makes aggregation less likely.]
2646
2647  SideEffects [None]
2648
2649  SeeAlso     [Cudd_SetRecomb]
2650
2651******************************************************************************/
2652int
2653Cudd_ReadRecomb(
2654  DdManager * dd)
2655{
2656    return(dd->recomb);
2657
2658} /* end of Cudd_ReadRecomb */
2659
2660
2661/**Function********************************************************************
2662
2663  Synopsis    [Sets the value of the recombination parameter used in group
2664  sifting.]
2665
2666  Description [Sets the value of the recombination parameter used in
2667  group sifting. A larger (positive) value makes the aggregation of
2668  variables due to the second difference criterion more likely. A
2669  smaller (negative) value makes aggregation less likely. The default
2670  value is 0.]
2671
2672  SideEffects [Changes the manager.]
2673
2674  SeeAlso     [Cudd_ReadRecomb]
2675
2676******************************************************************************/
2677void
2678Cudd_SetRecomb(
2679  DdManager * dd,
2680  int  recomb)
2681{
2682    dd->recomb = recomb;
2683
2684} /* end of Cudd_SetRecomb */
2685
2686
2687/**Function********************************************************************
2688
2689  Synopsis    [Returns the current value of the symmviolation parameter used
2690  in group sifting.]
2691
2692  Description [Returns the current value of the symmviolation
2693  parameter. This parameter is used in group sifting to decide how
2694  many violations to the symmetry conditions <code>f10 = f01</code> or
2695  <code>f11 = f00</code> are tolerable when checking for aggregation
2696  due to extended symmetry. The value should be between 0 and 100. A
2697  small value causes fewer variables to be aggregated. The default
2698  value is 0.]
2699
2700  SideEffects [None]
2701
2702  SeeAlso     [Cudd_SetSymmviolation]
2703
2704******************************************************************************/
2705int
2706Cudd_ReadSymmviolation(
2707  DdManager * dd)
2708{
2709    return(dd->symmviolation);
2710
2711} /* end of Cudd_ReadSymmviolation */
2712
2713
2714/**Function********************************************************************
2715
2716  Synopsis    [Sets the value of the symmviolation parameter used
2717  in group sifting.]
2718
2719  Description [Sets the value of the symmviolation
2720  parameter. This parameter is used in group sifting to decide how
2721  many violations to the symmetry conditions <code>f10 = f01</code> or
2722  <code>f11 = f00</code> are tolerable when checking for aggregation
2723  due to extended symmetry. The value should be between 0 and 100. A
2724  small value causes fewer variables to be aggregated. The default
2725  value is 0.]
2726
2727  SideEffects [Changes the manager.]
2728
2729  SeeAlso     [Cudd_ReadSymmviolation]
2730
2731******************************************************************************/
2732void
2733Cudd_SetSymmviolation(
2734  DdManager * dd,
2735  int  symmviolation)
2736{
2737    dd->symmviolation = symmviolation;
2738
2739} /* end of Cudd_SetSymmviolation */
2740
2741
2742/**Function********************************************************************
2743
2744  Synopsis    [Returns the current value of the arcviolation parameter used
2745  in group sifting.]
2746
2747  Description [Returns the current value of the arcviolation
2748  parameter. This parameter is used in group sifting to decide how
2749  many arcs into <code>y</code> not coming from <code>x</code> are
2750  tolerable when checking for aggregation due to extended
2751  symmetry. The value should be between 0 and 100. A small value
2752  causes fewer variables to be aggregated. The default value is 0.]
2753
2754  SideEffects [None]
2755
2756  SeeAlso     [Cudd_SetArcviolation]
2757
2758******************************************************************************/
2759int
2760Cudd_ReadArcviolation(
2761  DdManager * dd)
2762{
2763    return(dd->arcviolation);
2764
2765} /* end of Cudd_ReadArcviolation */
2766
2767
2768/**Function********************************************************************
2769
2770  Synopsis    [Sets the value of the arcviolation parameter used
2771  in group sifting.]
2772
2773  Description [Sets the value of the arcviolation
2774  parameter. This parameter is used in group sifting to decide how
2775  many arcs into <code>y</code> not coming from <code>x</code> are
2776  tolerable when checking for aggregation due to extended
2777  symmetry. The value should be between 0 and 100. A small value
2778  causes fewer variables to be aggregated. The default value is 0.]
2779
2780  SideEffects [None]
2781
2782  SeeAlso     [Cudd_ReadArcviolation]
2783
2784******************************************************************************/
2785void
2786Cudd_SetArcviolation(
2787  DdManager * dd,
2788  int  arcviolation)
2789{
2790    dd->arcviolation = arcviolation;
2791
2792} /* end of Cudd_SetArcviolation */
2793
2794
2795/**Function********************************************************************
2796
2797  Synopsis    [Reads the current size of the population used by the
2798  genetic algorithm for reordering.]
2799
2800  Description [Reads the current size of the population used by the
2801  genetic algorithm for variable reordering. A larger population size will
2802  cause the genetic algorithm to take more time, but will generally
2803  produce better results. The default value is 0, in which case the
2804  package uses three times the number of variables as population size,
2805  with a maximum of 120.]
2806
2807  SideEffects [None]
2808
2809  SeeAlso     [Cudd_SetPopulationSize]
2810
2811******************************************************************************/
2812int
2813Cudd_ReadPopulationSize(
2814  DdManager * dd)
2815{
2816    return(dd->populationSize);
2817
2818} /* end of Cudd_ReadPopulationSize */
2819
2820
2821/**Function********************************************************************
2822
2823  Synopsis    [Sets the size of the population used by the
2824  genetic algorithm for reordering.]
2825
2826  Description [Sets the size of the population used by the
2827  genetic algorithm for variable reordering. A larger population size will
2828  cause the genetic algorithm to take more time, but will generally
2829  produce better results. The default value is 0, in which case the
2830  package uses three times the number of variables as population size,
2831  with a maximum of 120.]
2832
2833  SideEffects [Changes the manager.]
2834
2835  SeeAlso     [Cudd_ReadPopulationSize]
2836
2837******************************************************************************/
2838void
2839Cudd_SetPopulationSize(
2840  DdManager * dd,
2841  int  populationSize)
2842{
2843    dd->populationSize = populationSize;
2844
2845} /* end of Cudd_SetPopulationSize */
2846
2847
2848/**Function********************************************************************
2849
2850  Synopsis    [Reads the current number of crossovers used by the
2851  genetic algorithm for reordering.]
2852
2853  Description [Reads the current number of crossovers used by the
2854  genetic algorithm for variable reordering. A larger number of crossovers will
2855  cause the genetic algorithm to take more time, but will generally
2856  produce better results. The default value is 0, in which case the
2857  package uses three times the number of variables as number of crossovers,
2858  with a maximum of 60.]
2859
2860  SideEffects [None]
2861
2862  SeeAlso     [Cudd_SetNumberXovers]
2863
2864******************************************************************************/
2865int
2866Cudd_ReadNumberXovers(
2867  DdManager * dd)
2868{
2869    return(dd->numberXovers);
2870
2871} /* end of Cudd_ReadNumberXovers */
2872
2873
2874/**Function********************************************************************
2875
2876  Synopsis    [Sets the number of crossovers used by the
2877  genetic algorithm for reordering.]
2878
2879  Description [Sets the number of crossovers used by the genetic
2880  algorithm for variable reordering. A larger number of crossovers
2881  will cause the genetic algorithm to take more time, but will
2882  generally produce better results. The default value is 0, in which
2883  case the package uses three times the number of variables as number
2884  of crossovers, with a maximum of 60.]
2885
2886  SideEffects [None]
2887
2888  SeeAlso     [Cudd_ReadNumberXovers]
2889
2890******************************************************************************/
2891void
2892Cudd_SetNumberXovers(
2893  DdManager * dd,
2894  int  numberXovers)
2895{
2896    dd->numberXovers = numberXovers;
2897
2898} /* end of Cudd_SetNumberXovers */
2899
2900/**Function********************************************************************
2901
2902  Synopsis    [Returns the memory in use by the manager measured in bytes.]
2903
2904  Description []
2905
2906  SideEffects [None]
2907
2908  SeeAlso     []
2909
2910******************************************************************************/
2911unsigned long
2912Cudd_ReadMemoryInUse(
2913  DdManager * dd)
2914{
2915    return(dd->memused);
2916
2917} /* end of Cudd_ReadMemoryInUse */
2918
2919
2920/**Function********************************************************************
2921
2922  Synopsis    [Prints out statistics and settings for a CUDD manager.]
2923
2924  Description [Prints out statistics and settings for a CUDD manager.
2925  Returns 1 if successful; 0 otherwise.]
2926
2927  SideEffects [None]
2928
2929  SeeAlso     []
2930
2931******************************************************************************/
2932int
2933Cudd_PrintInfo(
2934  DdManager * dd,
2935  FILE * fp)
2936{
2937    int retval;
2938    Cudd_ReorderingType autoMethod, autoMethodZ;
2939
2940    /* Modifiable parameters. */
2941    retval = fprintf(fp,"**** CUDD modifiable parameters ****\n");
2942    if (retval == EOF) return(0);
2943    retval = fprintf(fp,"Hard limit for cache size: %u\n",
2944                     Cudd_ReadMaxCacheHard(dd));
2945    if (retval == EOF) return(0);
2946    retval = fprintf(fp,"Cache hit threshold for resizing: %u%%\n",
2947                     Cudd_ReadMinHit(dd));
2948    if (retval == EOF) return(0);
2949    retval = fprintf(fp,"Garbage collection enabled: %s\n",
2950                     Cudd_GarbageCollectionEnabled(dd) ? "yes" : "no");
2951    if (retval == EOF) return(0);
2952    retval = fprintf(fp,"Limit for fast unique table growth: %u\n",
2953                     Cudd_ReadLooseUpTo(dd));
2954    if (retval == EOF) return(0);
2955    retval = fprintf(fp,
2956                     "Maximum number of variables sifted per reordering: %d\n",
2957                     Cudd_ReadSiftMaxVar(dd));
2958    if (retval == EOF) return(0);
2959    retval = fprintf(fp,
2960                     "Maximum number of variable swaps per reordering: %d\n",
2961                     Cudd_ReadSiftMaxSwap(dd));
2962    if (retval == EOF) return(0);
2963    retval = fprintf(fp,"Maximum growth while sifting a variable: %g\n",
2964                     Cudd_ReadMaxGrowth(dd));
2965    if (retval == EOF) return(0);
2966    retval = fprintf(fp,"Dynamic reordering of BDDs enabled: %s\n",
2967                     Cudd_ReorderingStatus(dd,&autoMethod) ? "yes" : "no");
2968    if (retval == EOF) return(0);
2969    retval = fprintf(fp,"Default BDD reordering method: %d\n", autoMethod);
2970    if (retval == EOF) return(0);
2971    retval = fprintf(fp,"Dynamic reordering of ZDDs enabled: %s\n",
2972                     Cudd_ReorderingStatusZdd(dd,&autoMethodZ) ? "yes" : "no");
2973    if (retval == EOF) return(0);
2974    retval = fprintf(fp,"Default ZDD reordering method: %d\n", autoMethodZ);
2975    if (retval == EOF) return(0);
2976    retval = fprintf(fp,"Realignment of ZDDs to BDDs enabled: %s\n",
2977                     Cudd_zddRealignmentEnabled(dd) ? "yes" : "no");
2978    if (retval == EOF) return(0);
2979    retval = fprintf(fp,"Realignment of BDDs to ZDDs enabled: %s\n",
2980                     Cudd_bddRealignmentEnabled(dd) ? "yes" : "no");
2981    if (retval == EOF) return(0);
2982    retval = fprintf(fp,"Dead nodes counted in triggering reordering: %s\n",
2983                     Cudd_DeadAreCounted(dd) ? "yes" : "no");
2984    if (retval == EOF) return(0);
2985    retval = fprintf(fp,"Group checking criterion: %d\n",
2986                     Cudd_ReadGroupcheck(dd));
2987    if (retval == EOF) return(0);
2988    retval = fprintf(fp,"Recombination threshold: %d\n", Cudd_ReadRecomb(dd));
2989    if (retval == EOF) return(0);
2990    retval = fprintf(fp,"Symmetry violation threshold: %d\n",
2991                     Cudd_ReadSymmviolation(dd));
2992    if (retval == EOF) return(0);
2993    retval = fprintf(fp,"Arc violation threshold: %d\n",
2994                     Cudd_ReadArcviolation(dd));
2995    if (retval == EOF) return(0);
2996    retval = fprintf(fp,"GA population size: %d\n",
2997                     Cudd_ReadPopulationSize(dd));
2998    if (retval == EOF) return(0);
2999    retval = fprintf(fp,"Number of crossovers for GA: %d\n",
3000                     Cudd_ReadNumberXovers(dd));
3001    if (retval == EOF) return(0);
3002    retval = fprintf(fp,"Next reordering threshold: %u\n",
3003                     Cudd_ReadNextReordering(dd));
3004    if (retval == EOF) return(0);
3005
3006    /* Non-modifiable parameters. */
3007    retval = fprintf(fp,"**** CUDD non-modifiable parameters ****\n");
3008    if (retval == EOF) return(0);
3009    retval = fprintf(fp,"Memory in use: %lu\n", Cudd_ReadMemoryInUse(dd));
3010    if (retval == EOF) return(0);
3011    retval = fprintf(fp,"Peak number of nodes: %ld\n",
3012                     Cudd_ReadPeakNodeCount(dd));
3013    if (retval == EOF) return(0);
3014    retval = fprintf(fp,"Peak number of live nodes: %d\n",
3015                     Cudd_ReadPeakLiveNodeCount(dd));
3016    if (retval == EOF) return(0);
3017    retval = fprintf(fp,"Number of BDD variables: %d\n", dd->size);
3018    if (retval == EOF) return(0);
3019    retval = fprintf(fp,"Number of ZDD variables: %d\n", dd->sizeZ);
3020    if (retval == EOF) return(0);
3021    retval = fprintf(fp,"Number of cache entries: %u\n", dd->cacheSlots);
3022    if (retval == EOF) return(0);
3023    retval = fprintf(fp,"Number of cache look-ups: %.0f\n",
3024                     Cudd_ReadCacheLookUps(dd));
3025    if (retval == EOF) return(0);
3026    retval = fprintf(fp,"Number of cache hits: %.0f\n",
3027                     Cudd_ReadCacheHits(dd));
3028    if (retval == EOF) return(0);
3029    retval = fprintf(fp,"Number of cache insertions: %.0f\n",
3030                     dd->cacheinserts);
3031    if (retval == EOF) return(0);
3032    retval = fprintf(fp,"Number of cache collisions: %.0f\n",
3033                     dd->cachecollisions);
3034    if (retval == EOF) return(0);
3035    retval = fprintf(fp,"Number of cache deletions: %.0f\n",
3036                     dd->cachedeletions);
3037    if (retval == EOF) return(0);
3038    retval = cuddCacheProfile(dd,fp);
3039    if (retval == 0) return(0);
3040    retval = fprintf(fp,"Soft limit for cache size: %u\n",
3041                     Cudd_ReadMaxCache(dd));
3042    if (retval == EOF) return(0);
3043    retval = fprintf(fp,"Number of buckets in unique table: %u\n", dd->slots);
3044    if (retval == EOF) return(0);
3045    retval = fprintf(fp,"Used buckets in unique table: %.2f%% (expected %.2f%%)\n",
3046                     100.0 * Cudd_ReadUsedSlots(dd),
3047                     100.0 * Cudd_ExpectedUsedSlots(dd));
3048    if (retval == EOF) return(0);
3049#ifdef DD_UNIQUE_PROFILE
3050    retval = fprintf(fp,"Unique lookups: %.0f\n", dd->uniqueLookUps);
3051    if (retval == EOF) return(0);
3052    retval = fprintf(fp,"Unique links: %.0f (%g per lookup)\n",
3053            dd->uniqueLinks, dd->uniqueLinks / dd->uniqueLookUps);
3054    if (retval == EOF) return(0);
3055#endif
3056    retval = fprintf(fp,"Number of BDD and ADD nodes: %u\n", dd->keys);
3057    if (retval == EOF) return(0);
3058    retval = fprintf(fp,"Number of ZDD nodes: %u\n", dd->keysZ);
3059    if (retval == EOF) return(0);
3060    retval = fprintf(fp,"Number of dead BDD and ADD nodes: %u\n", dd->dead);
3061    if (retval == EOF) return(0);
3062    retval = fprintf(fp,"Number of dead ZDD nodes: %u\n", dd->deadZ);
3063    if (retval == EOF) return(0);
3064    retval = fprintf(fp,"Total number of nodes allocated: %.0f\n",
3065                     dd->allocated);
3066    if (retval == EOF) return(0);
3067    retval = fprintf(fp,"Total number of nodes reclaimed: %.0f\n",
3068                     dd->reclaimed);
3069    if (retval == EOF) return(0);
3070#if DD_STATS
3071    retval = fprintf(fp,"Nodes freed: %.0f\n", dd->nodesFreed);
3072    if (retval == EOF) return(0);
3073    retval = fprintf(fp,"Nodes dropped: %.0f\n", dd->nodesDropped);
3074    if (retval == EOF) return(0);
3075#endif
3076#if DD_COUNT
3077    retval = fprintf(fp,"Number of recursive calls: %.0f\n",
3078                     Cudd_ReadRecursiveCalls(dd));
3079    if (retval == EOF) return(0);
3080#endif
3081    retval = fprintf(fp,"Garbage collections so far: %d\n",
3082                     Cudd_ReadGarbageCollections(dd));
3083    if (retval == EOF) return(0);
3084    retval = fprintf(fp,"Time for garbage collection: %.2f sec\n",
3085                     ((double)Cudd_ReadGarbageCollectionTime(dd)/1000.0));
3086    if (retval == EOF) return(0);
3087    retval = fprintf(fp,"Reorderings so far: %d\n", dd->reorderings);
3088    if (retval == EOF) return(0);
3089    retval = fprintf(fp,"Time for reordering: %.2f sec\n",
3090                     ((double)Cudd_ReadReorderingTime(dd)/1000.0));
3091    if (retval == EOF) return(0);
3092#if DD_COUNT
3093    retval = fprintf(fp,"Node swaps in reordering: %.0f\n",
3094        Cudd_ReadSwapSteps(dd));
3095    if (retval == EOF) return(0);
3096#endif
3097
3098    return(1);
3099
3100} /* end of Cudd_PrintInfo */
3101
3102
3103/**Function********************************************************************
3104
3105  Synopsis    [Reports the peak number of nodes.]
3106
3107  Description [Reports the peak number of nodes. This number includes
3108  node on the free list. At the peak, the number of nodes on the free
3109  list is guaranteed to be less than DD_MEM_CHUNK.]
3110
3111  SideEffects [None]
3112
3113  SeeAlso     [Cudd_ReadNodeCount Cudd_PrintInfo]
3114
3115******************************************************************************/
3116long
3117Cudd_ReadPeakNodeCount(
3118  DdManager * dd)
3119{
3120    long count = 0;
3121    DdNodePtr *scan = dd->memoryList;
3122
3123    while (scan != NULL) {
3124        count += DD_MEM_CHUNK;
3125        scan = (DdNodePtr *) *scan;
3126    }
3127    return(count);
3128
3129} /* end of Cudd_ReadPeakNodeCount */
3130
3131
3132/**Function********************************************************************
3133
3134  Synopsis    [Reports the peak number of live nodes.]
3135
3136  Description [Reports the peak number of live nodes. This count is kept
3137  only if CUDD is compiled with DD_STATS defined. If DD_STATS is not
3138  defined, this function returns -1.]
3139
3140  SideEffects [None]
3141
3142  SeeAlso     [Cudd_ReadNodeCount Cudd_PrintInfo Cudd_ReadPeakNodeCount]
3143
3144******************************************************************************/
3145int
3146Cudd_ReadPeakLiveNodeCount(
3147  DdManager * dd)
3148{
3149    unsigned int live = dd->keys - dd->dead;
3150
3151    if (live > dd->peakLiveNodes) {
3152        dd->peakLiveNodes = live;
3153    }
3154    return((int)dd->peakLiveNodes);
3155
3156} /* end of Cudd_ReadPeakLiveNodeCount */
3157
3158
3159/**Function********************************************************************
3160
3161  Synopsis    [Reports the number of nodes in BDDs and ADDs.]
3162
3163  Description [Reports the number of live nodes in BDDs and ADDs. This
3164  number does not include the isolated projection functions and the
3165  unused constants. These nodes that are not counted are not part of
3166  the DDs manipulated by the application.]
3167
3168  SideEffects [None]
3169
3170  SeeAlso     [Cudd_ReadPeakNodeCount Cudd_zddReadNodeCount]
3171
3172******************************************************************************/
3173long
3174Cudd_ReadNodeCount(
3175  DdManager * dd)
3176{
3177    long count;
3178    int i;
3179
3180#ifndef DD_NO_DEATH_ROW
3181    cuddClearDeathRow(dd);
3182#endif
3183
3184    count = (long) (dd->keys - dd->dead);
3185
3186    /* Count isolated projection functions. Their number is subtracted
3187    ** from the node count because they are not part of the BDDs.
3188    */
3189    for (i=0; i < dd->size; i++) {
3190        if (dd->vars[i]->ref == 1) count--;
3191    }
3192    /* Subtract from the count the unused constants. */
3193    if (DD_ZERO(dd)->ref == 1) count--;
3194    if (DD_PLUS_INFINITY(dd)->ref == 1) count--;
3195    if (DD_MINUS_INFINITY(dd)->ref == 1) count--;
3196
3197    return(count);
3198
3199} /* end of Cudd_ReadNodeCount */
3200
3201
3202
3203/**Function********************************************************************
3204
3205  Synopsis    [Reports the number of nodes in ZDDs.]
3206
3207  Description [Reports the number of nodes in ZDDs. This
3208  number always includes the two constants 1 and 0.]
3209
3210  SideEffects [None]
3211
3212  SeeAlso     [Cudd_ReadPeakNodeCount Cudd_ReadNodeCount]
3213
3214******************************************************************************/
3215long
3216Cudd_zddReadNodeCount(
3217  DdManager * dd)
3218{
3219    return((long)(dd->keysZ - dd->deadZ + 2));
3220
3221} /* end of Cudd_zddReadNodeCount */
3222
3223
3224/**Function********************************************************************
3225
3226  Synopsis    [Adds a function to a hook.]
3227
3228  Description [Adds a function to a hook. A hook is a list of
3229  application-provided functions called on certain occasions by the
3230  package. Returns 1 if the function is successfully added; 2 if the
3231  function was already in the list; 0 otherwise.]
3232
3233  SideEffects [None]
3234
3235  SeeAlso     [Cudd_RemoveHook]
3236
3237******************************************************************************/
3238int
3239Cudd_AddHook(
3240  DdManager * dd,
3241  DD_HFP f,
3242  Cudd_HookType where)
3243{
3244    DdHook **hook, *nextHook, *newHook;
3245
3246    switch (where) {
3247    case CUDD_PRE_GC_HOOK:
3248        hook = &(dd->preGCHook);
3249        break;
3250    case CUDD_POST_GC_HOOK:
3251        hook = &(dd->postGCHook);
3252        break;
3253    case CUDD_PRE_REORDERING_HOOK:
3254        hook = &(dd->preReorderingHook);
3255        break;
3256    case CUDD_POST_REORDERING_HOOK:
3257        hook = &(dd->postReorderingHook);
3258        break;
3259    default:
3260        return(0);
3261    }
3262    /* Scan the list and find whether the function is already there.
3263    ** If so, just return. */
3264    nextHook = *hook;
3265    while (nextHook != NULL) {
3266        if (nextHook->f == f) {
3267            return(2);
3268        }
3269        hook = &(nextHook->next);
3270        nextHook = nextHook->next;
3271    }
3272    /* The function was not in the list. Create a new item and append it
3273    ** to the end of the list. */
3274    newHook = ALLOC(DdHook,1);
3275    if (newHook == NULL) {
3276        dd->errorCode = CUDD_MEMORY_OUT;
3277        return(0);
3278    }
3279    newHook->next = NULL;
3280    newHook->f = f;
3281    *hook = newHook;
3282    return(1);
3283
3284} /* end of Cudd_AddHook */
3285
3286
3287/**Function********************************************************************
3288
3289  Synopsis    [Removes a function from a hook.]
3290
3291  Description [Removes a function from a hook. A hook is a list of
3292  application-provided functions called on certain occasions by the
3293  package. Returns 1 if successful; 0 the function was not in the list.]
3294
3295  SideEffects [None]
3296
3297  SeeAlso     [Cudd_AddHook]
3298
3299******************************************************************************/
3300int
3301Cudd_RemoveHook(
3302  DdManager * dd,
3303  DD_HFP f,
3304  Cudd_HookType where)
3305{
3306    DdHook **hook, *nextHook;
3307
3308    switch (where) {
3309    case CUDD_PRE_GC_HOOK:
3310        hook = &(dd->preGCHook);
3311        break;
3312    case CUDD_POST_GC_HOOK:
3313        hook = &(dd->postGCHook);
3314        break;
3315    case CUDD_PRE_REORDERING_HOOK:
3316        hook = &(dd->preReorderingHook);
3317        break;
3318    case CUDD_POST_REORDERING_HOOK:
3319        hook = &(dd->postReorderingHook);
3320        break;
3321    default:
3322        return(0);
3323    }
3324    nextHook = *hook;
3325    while (nextHook != NULL) {
3326        if (nextHook->f == f) {
3327            *hook = nextHook->next;
3328            FREE(nextHook);
3329            return(1);
3330        }
3331        hook = &(nextHook->next);
3332        nextHook = nextHook->next;
3333    }
3334
3335    return(0);
3336
3337} /* end of Cudd_RemoveHook */
3338
3339
3340/**Function********************************************************************
3341
3342  Synopsis    [Checks whether a function is in a hook.]
3343
3344  Description [Checks whether a function is in a hook. A hook is a list of
3345  application-provided functions called on certain occasions by the
3346  package. Returns 1 if the function is found; 0 otherwise.]
3347
3348  SideEffects [None]
3349
3350  SeeAlso     [Cudd_AddHook Cudd_RemoveHook]
3351
3352******************************************************************************/
3353int
3354Cudd_IsInHook(
3355  DdManager * dd,
3356  DD_HFP f,
3357  Cudd_HookType where)
3358{
3359    DdHook *hook;
3360
3361    switch (where) {
3362    case CUDD_PRE_GC_HOOK:
3363        hook = dd->preGCHook;
3364        break;
3365    case CUDD_POST_GC_HOOK:
3366        hook = dd->postGCHook;
3367        break;
3368    case CUDD_PRE_REORDERING_HOOK:
3369        hook = dd->preReorderingHook;
3370        break;
3371    case CUDD_POST_REORDERING_HOOK:
3372        hook = dd->postReorderingHook;
3373        break;
3374    default:
3375        return(0);
3376    }
3377    /* Scan the list and find whether the function is already there. */
3378    while (hook != NULL) {
3379        if (hook->f == f) {
3380            return(1);
3381        }
3382        hook = hook->next;
3383    }
3384    return(0);
3385
3386} /* end of Cudd_IsInHook */
3387
3388
3389/**Function********************************************************************
3390
3391  Synopsis    [Sample hook function to call before reordering.]
3392
3393  Description [Sample hook function to call before reordering.
3394  Prints on the manager's stdout reordering method and initial size.
3395  Returns 1 if successful; 0 otherwise.]
3396
3397  SideEffects [None]
3398
3399  SeeAlso     [Cudd_StdPostReordHook]
3400
3401******************************************************************************/
3402int
3403Cudd_StdPreReordHook(
3404  DdManager *dd,
3405  const char *str,
3406  void *data)
3407{
3408    Cudd_ReorderingType method = (Cudd_ReorderingType) (ptruint) data;
3409    int retval;
3410
3411    retval = fprintf(dd->out,"%s reordering with ", str);
3412    if (retval == EOF) return(0);
3413    switch (method) {
3414    case CUDD_REORDER_SIFT_CONVERGE:
3415    case CUDD_REORDER_SYMM_SIFT_CONV:
3416    case CUDD_REORDER_GROUP_SIFT_CONV:
3417    case CUDD_REORDER_WINDOW2_CONV:
3418    case CUDD_REORDER_WINDOW3_CONV:
3419    case CUDD_REORDER_WINDOW4_CONV:
3420    case CUDD_REORDER_LINEAR_CONVERGE:
3421        retval = fprintf(dd->out,"converging ");
3422        if (retval == EOF) return(0);
3423        break;
3424    default:
3425        break;
3426    }
3427    switch (method) {
3428    case CUDD_REORDER_RANDOM:
3429    case CUDD_REORDER_RANDOM_PIVOT:
3430        retval = fprintf(dd->out,"random");
3431        break;
3432    case CUDD_REORDER_SIFT:
3433    case CUDD_REORDER_SIFT_CONVERGE:
3434        retval = fprintf(dd->out,"sifting");
3435        break;
3436    case CUDD_REORDER_SYMM_SIFT:
3437    case CUDD_REORDER_SYMM_SIFT_CONV:
3438        retval = fprintf(dd->out,"symmetric sifting");
3439        break;
3440    case CUDD_REORDER_LAZY_SIFT:
3441        retval = fprintf(dd->out,"lazy sifting");
3442        break;
3443    case CUDD_REORDER_GROUP_SIFT:
3444    case CUDD_REORDER_GROUP_SIFT_CONV:
3445        retval = fprintf(dd->out,"group sifting");
3446        break;
3447    case CUDD_REORDER_WINDOW2:
3448    case CUDD_REORDER_WINDOW3:
3449    case CUDD_REORDER_WINDOW4:
3450    case CUDD_REORDER_WINDOW2_CONV:
3451    case CUDD_REORDER_WINDOW3_CONV:
3452    case CUDD_REORDER_WINDOW4_CONV:
3453        retval = fprintf(dd->out,"window");
3454        break;
3455    case CUDD_REORDER_ANNEALING:
3456        retval = fprintf(dd->out,"annealing");
3457        break;
3458    case CUDD_REORDER_GENETIC:
3459        retval = fprintf(dd->out,"genetic");
3460        break;
3461    case CUDD_REORDER_LINEAR:
3462    case CUDD_REORDER_LINEAR_CONVERGE:
3463        retval = fprintf(dd->out,"linear sifting");
3464        break;
3465    case CUDD_REORDER_EXACT:
3466        retval = fprintf(dd->out,"exact");
3467        break;
3468    default:
3469        return(0);
3470    }
3471    if (retval == EOF) return(0);
3472
3473    retval = fprintf(dd->out,": from %ld to ... ", strcmp(str, "BDD") == 0 ?
3474                     Cudd_ReadNodeCount(dd) : Cudd_zddReadNodeCount(dd));
3475    if (retval == EOF) return(0);
3476    fflush(dd->out);
3477    return(1);
3478
3479} /* end of Cudd_StdPreReordHook */
3480
3481
3482/**Function********************************************************************
3483
3484  Synopsis    [Sample hook function to call after reordering.]
3485
3486  Description [Sample hook function to call after reordering.
3487  Prints on the manager's stdout final size and reordering time.
3488  Returns 1 if successful; 0 otherwise.]
3489
3490  SideEffects [None]
3491
3492  SeeAlso     [Cudd_StdPreReordHook]
3493
3494******************************************************************************/
3495int
3496Cudd_StdPostReordHook(
3497  DdManager *dd,
3498  const char *str,
3499  void *data)
3500{
3501    long initialTime = (long) data;
3502    int retval;
3503    long finalTime = util_cpu_time();
3504    double totalTimeSec = (double)(finalTime - initialTime) / 1000.0;
3505
3506    retval = fprintf(dd->out,"%ld nodes in %g sec\n", strcmp(str, "BDD") == 0 ?
3507                     Cudd_ReadNodeCount(dd) : Cudd_zddReadNodeCount(dd),
3508                     totalTimeSec);
3509    if (retval == EOF) return(0);
3510    retval = fflush(dd->out);
3511    if (retval == EOF) return(0);
3512    return(1);
3513
3514} /* end of Cudd_StdPostReordHook */
3515
3516
3517/**Function********************************************************************
3518
3519  Synopsis    [Enables reporting of reordering stats.]
3520
3521  Description [Enables reporting of reordering stats.
3522  Returns 1 if successful; 0 otherwise.]
3523
3524  SideEffects [Installs functions in the pre-reordering and post-reordering
3525  hooks.]
3526
3527  SeeAlso     [Cudd_DisableReorderingReporting Cudd_ReorderingReporting]
3528
3529******************************************************************************/
3530int
3531Cudd_EnableReorderingReporting(
3532  DdManager *dd)
3533{
3534    if (!Cudd_AddHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) {
3535        return(0);
3536    }
3537    if (!Cudd_AddHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) {
3538        return(0);
3539    }
3540    return(1);
3541
3542} /* end of Cudd_EnableReorderingReporting */
3543
3544
3545/**Function********************************************************************
3546
3547  Synopsis    [Disables reporting of reordering stats.]
3548
3549  Description [Disables reporting of reordering stats.
3550  Returns 1 if successful; 0 otherwise.]
3551
3552  SideEffects [Removes functions from the pre-reordering and post-reordering
3553  hooks.]
3554
3555  SeeAlso     [Cudd_EnableReorderingReporting Cudd_ReorderingReporting]
3556
3557******************************************************************************/
3558int
3559Cudd_DisableReorderingReporting(
3560  DdManager *dd)
3561{
3562    if (!Cudd_RemoveHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) {
3563        return(0);
3564    }
3565    if (!Cudd_RemoveHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) {
3566        return(0);
3567    }
3568    return(1);
3569
3570} /* end of Cudd_DisableReorderingReporting */
3571
3572
3573/**Function********************************************************************
3574
3575  Synopsis    [Returns 1 if reporting of reordering stats is enabled.]
3576
3577  Description [Returns 1 if reporting of reordering stats is enabled;
3578  0 otherwise.]
3579
3580  SideEffects [none]
3581
3582  SeeAlso     [Cudd_EnableReorderingReporting Cudd_DisableReorderingReporting]
3583
3584******************************************************************************/
3585int
3586Cudd_ReorderingReporting(
3587  DdManager *dd)
3588{
3589    return(Cudd_IsInHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK));
3590
3591} /* end of Cudd_ReorderingReporting */
3592
3593
3594/**Function********************************************************************
3595
3596  Synopsis    [Returns the code of the last error.]
3597
3598  Description [Returns the code of the last error. The error codes are
3599  defined in cudd.h.]
3600
3601  SideEffects [None]
3602
3603  SeeAlso     [Cudd_ClearErrorCode]
3604
3605******************************************************************************/
3606Cudd_ErrorType
3607Cudd_ReadErrorCode(
3608  DdManager *dd)
3609{
3610    return(dd->errorCode);
3611
3612} /* end of Cudd_ReadErrorCode */
3613
3614
3615/**Function********************************************************************
3616
3617  Synopsis    [Clear the error code of a manager.]
3618
3619  Description []
3620
3621  SideEffects [None]
3622
3623  SeeAlso     [Cudd_ReadErrorCode]
3624
3625******************************************************************************/
3626void
3627Cudd_ClearErrorCode(
3628  DdManager *dd)
3629{
3630    dd->errorCode = CUDD_NO_ERROR;
3631
3632} /* end of Cudd_ClearErrorCode */
3633
3634
3635/**Function********************************************************************
3636
3637  Synopsis    [Reads the stdout of a manager.]
3638
3639  Description [Reads the stdout of a manager. This is the file pointer to
3640  which messages normally going to stdout are written. It is initialized
3641  to stdout. Cudd_SetStdout allows the application to redirect it.]
3642
3643  SideEffects [None]
3644
3645  SeeAlso     [Cudd_SetStdout Cudd_ReadStderr]
3646
3647******************************************************************************/
3648FILE *
3649Cudd_ReadStdout(
3650  DdManager *dd)
3651{
3652    return(dd->out);
3653
3654} /* end of Cudd_ReadStdout */
3655
3656
3657/**Function********************************************************************
3658
3659  Synopsis    [Sets the stdout of a manager.]
3660
3661  Description []
3662
3663  SideEffects [None]
3664
3665  SeeAlso     [Cudd_ReadStdout Cudd_SetStderr]
3666
3667******************************************************************************/
3668void
3669Cudd_SetStdout(
3670  DdManager *dd,
3671  FILE *fp)
3672{
3673    dd->out = fp;
3674
3675} /* end of Cudd_SetStdout */
3676
3677
3678/**Function********************************************************************
3679
3680  Synopsis    [Reads the stderr of a manager.]
3681
3682  Description [Reads the stderr of a manager. This is the file pointer to
3683  which messages normally going to stderr are written. It is initialized
3684  to stderr. Cudd_SetStderr allows the application to redirect it.]
3685
3686  SideEffects [None]
3687
3688  SeeAlso     [Cudd_SetStderr Cudd_ReadStdout]
3689
3690******************************************************************************/
3691FILE *
3692Cudd_ReadStderr(
3693  DdManager *dd)
3694{
3695    return(dd->err);
3696
3697} /* end of Cudd_ReadStderr */
3698
3699
3700/**Function********************************************************************
3701
3702  Synopsis    [Sets the stderr of a manager.]
3703
3704  Description []
3705
3706  SideEffects [None]
3707
3708  SeeAlso     [Cudd_ReadStderr Cudd_SetStdout]
3709
3710******************************************************************************/
3711void
3712Cudd_SetStderr(
3713  DdManager *dd,
3714  FILE *fp)
3715{
3716    dd->err = fp;
3717
3718} /* end of Cudd_SetStderr */
3719
3720
3721/**Function********************************************************************
3722
3723  Synopsis    [Returns the threshold for the next dynamic reordering.]
3724
3725  Description [Returns the threshold for the next dynamic reordering.
3726  The threshold is in terms of number of nodes and is in effect only
3727  if reordering is enabled. The count does not include the dead nodes,
3728  unless the countDead parameter of the manager has been changed from
3729  its default setting.]
3730
3731  SideEffects [None]
3732
3733  SeeAlso     [Cudd_SetNextReordering]
3734
3735******************************************************************************/
3736unsigned int
3737Cudd_ReadNextReordering(
3738  DdManager *dd)
3739{
3740    return(dd->nextDyn);
3741
3742} /* end of Cudd_ReadNextReordering */
3743
3744
3745/**Function********************************************************************
3746
3747  Synopsis    [Sets the threshold for the next dynamic reordering.]
3748
3749  Description [Sets the threshold for the next dynamic reordering.
3750  The threshold is in terms of number of nodes and is in effect only
3751  if reordering is enabled. The count does not include the dead nodes,
3752  unless the countDead parameter of the manager has been changed from
3753  its default setting.]
3754
3755  SideEffects [None]
3756
3757  SeeAlso     [Cudd_ReadNextReordering]
3758
3759******************************************************************************/
3760void
3761Cudd_SetNextReordering(
3762  DdManager *dd,
3763  unsigned int next)
3764{
3765    dd->nextDyn = next;
3766
3767} /* end of Cudd_SetNextReordering */
3768
3769
3770/**Function********************************************************************
3771
3772  Synopsis    [Reads the number of elementary reordering steps.]
3773
3774  Description []
3775
3776  SideEffects [none]
3777
3778  SeeAlso     []
3779
3780******************************************************************************/
3781double
3782Cudd_ReadSwapSteps(
3783  DdManager *dd)
3784{
3785#ifdef DD_COUNT
3786    return(dd->swapSteps);
3787#else
3788    return(-1);
3789#endif
3790
3791} /* end of Cudd_ReadSwapSteps */
3792
3793
3794/**Function********************************************************************
3795
3796  Synopsis    [Reads the maximum allowed number of live nodes.]
3797
3798  Description [Reads the maximum allowed number of live nodes. When this
3799  number is exceeded, the package returns NULL.]
3800
3801  SideEffects [none]
3802
3803  SeeAlso     [Cudd_SetMaxLive]
3804
3805******************************************************************************/
3806unsigned int
3807Cudd_ReadMaxLive(
3808  DdManager *dd)
3809{
3810    return(dd->maxLive);
3811
3812} /* end of Cudd_ReadMaxLive */
3813
3814
3815/**Function********************************************************************
3816
3817  Synopsis    [Sets the maximum allowed number of live nodes.]
3818
3819  Description [Sets the maximum allowed number of live nodes. When this
3820  number is exceeded, the package returns NULL.]
3821
3822  SideEffects [none]
3823
3824  SeeAlso     [Cudd_ReadMaxLive]
3825
3826******************************************************************************/
3827void
3828Cudd_SetMaxLive(
3829  DdManager *dd,
3830  unsigned int maxLive)
3831{
3832    dd->maxLive = maxLive;
3833
3834} /* end of Cudd_SetMaxLive */
3835
3836
3837/**Function********************************************************************
3838
3839  Synopsis    [Reads the maximum allowed memory.]
3840
3841  Description [Reads the maximum allowed memory. When this
3842  number is exceeded, the package returns NULL.]
3843
3844  SideEffects [none]
3845
3846  SeeAlso     [Cudd_SetMaxMemory]
3847
3848******************************************************************************/
3849unsigned long
3850Cudd_ReadMaxMemory(
3851  DdManager *dd)
3852{
3853    return(dd->maxmemhard);
3854
3855} /* end of Cudd_ReadMaxMemory */
3856
3857
3858/**Function********************************************************************
3859
3860  Synopsis    [Sets the maximum allowed memory.]
3861
3862  Description [Sets the maximum allowed memory. When this
3863  number is exceeded, the package returns NULL.]
3864
3865  SideEffects [none]
3866
3867  SeeAlso     [Cudd_ReadMaxMemory]
3868
3869******************************************************************************/
3870void
3871Cudd_SetMaxMemory(
3872  DdManager *dd,
3873  unsigned long maxMemory)
3874{
3875    dd->maxmemhard = maxMemory;
3876
3877} /* end of Cudd_SetMaxMemory */
3878
3879
3880/**Function********************************************************************
3881
3882  Synopsis    [Prevents sifting of a variable.]
3883
3884  Description [This function sets a flag to prevent sifting of a
3885  variable.  Returns 1 if successful; 0 otherwise (i.e., invalid
3886  variable index).]
3887
3888  SideEffects [Changes the "bindVar" flag in DdSubtable.]
3889
3890  SeeAlso     [Cudd_bddUnbindVar]
3891
3892******************************************************************************/
3893int
3894Cudd_bddBindVar(
3895  DdManager *dd /* manager */,
3896  int index /* variable index */)
3897{
3898    if (index >= dd->size || index < 0) return(0);
3899    dd->subtables[dd->perm[index]].bindVar = 1;
3900    return(1);
3901
3902} /* end of Cudd_bddBindVar */
3903
3904
3905/**Function********************************************************************
3906
3907  Synopsis    [Allows the sifting of a variable.]
3908
3909  Description [This function resets the flag that prevents the sifting
3910  of a variable. In successive variable reorderings, the variable will
3911  NOT be skipped, that is, sifted.  Initially all variables can be
3912  sifted. It is necessary to call this function only to re-enable
3913  sifting after a call to Cudd_bddBindVar. Returns 1 if successful; 0
3914  otherwise (i.e., invalid variable index).]
3915
3916  SideEffects [Changes the "bindVar" flag in DdSubtable.]
3917
3918  SeeAlso     [Cudd_bddBindVar]
3919
3920******************************************************************************/
3921int
3922Cudd_bddUnbindVar(
3923  DdManager *dd /* manager */,
3924  int index /* variable index */)
3925{
3926    if (index >= dd->size || index < 0) return(0);
3927    dd->subtables[dd->perm[index]].bindVar = 0;
3928    return(1);
3929
3930} /* end of Cudd_bddUnbindVar */
3931
3932
3933/**Function********************************************************************
3934
3935  Synopsis    [Tells whether a variable can be sifted.]
3936
3937  Description [This function returns 1 if a variable is enabled for
3938  sifting.  Initially all variables can be sifted. This function returns
3939  0 only if there has been a previous call to Cudd_bddBindVar for that
3940  variable not followed by a call to Cudd_bddUnbindVar. The function returns
3941  0 also in the case in which the index of the variable is out of bounds.]
3942
3943  SideEffects [none]
3944
3945  SeeAlso     [Cudd_bddBindVar Cudd_bddUnbindVar]
3946
3947******************************************************************************/
3948int
3949Cudd_bddVarIsBound(
3950  DdManager *dd /* manager */,
3951  int index /* variable index */)
3952{
3953    if (index >= dd->size || index < 0) return(0);
3954    return(dd->subtables[dd->perm[index]].bindVar);
3955
3956} /* end of Cudd_bddVarIsBound */
3957
3958
3959/**Function********************************************************************
3960
3961  Synopsis    [Sets a variable type to primary input.]
3962
3963  Description [Sets a variable type to primary input.  The variable type is
3964  used by lazy sifting.  Returns 1 if successful; 0 otherwise.]
3965
3966  SideEffects [modifies the manager]
3967
3968  SeeAlso     [Cudd_bddSetPsVar Cudd_bddSetNsVar Cudd_bddIsPiVar]
3969
3970******************************************************************************/
3971int
3972Cudd_bddSetPiVar(
3973  DdManager *dd /* manager */,
3974  int index /* variable index */)
3975{
3976    if (index >= dd->size || index < 0) return (0);
3977    dd->subtables[dd->perm[index]].varType = CUDD_VAR_PRIMARY_INPUT;
3978    return(1);
3979
3980} /* end of Cudd_bddSetPiVar */
3981
3982
3983/**Function********************************************************************
3984
3985  Synopsis    [Sets a variable type to present state.]
3986
3987  Description [Sets a variable type to present state.  The variable type is
3988  used by lazy sifting.  Returns 1 if successful; 0 otherwise.]
3989
3990  SideEffects [modifies the manager]
3991
3992  SeeAlso     [Cudd_bddSetPiVar Cudd_bddSetNsVar Cudd_bddIsPsVar]
3993
3994******************************************************************************/
3995int
3996Cudd_bddSetPsVar(
3997  DdManager *dd /* manager */,
3998  int index /* variable index */)
3999{
4000    if (index >= dd->size || index < 0) return (0);
4001    dd->subtables[dd->perm[index]].varType = CUDD_VAR_PRESENT_STATE;
4002    return(1);
4003
4004} /* end of Cudd_bddSetPsVar */
4005
4006
4007/**Function********************************************************************
4008
4009  Synopsis    [Sets a variable type to next state.]
4010
4011  Description [Sets a variable type to next state.  The variable type is
4012  used by lazy sifting.  Returns 1 if successful; 0 otherwise.]
4013
4014  SideEffects [modifies the manager]
4015
4016  SeeAlso     [Cudd_bddSetPiVar Cudd_bddSetPsVar Cudd_bddIsNsVar]
4017
4018******************************************************************************/
4019int
4020Cudd_bddSetNsVar(
4021  DdManager *dd /* manager */,
4022  int index /* variable index */)
4023{
4024    if (index >= dd->size || index < 0) return (0);
4025    dd->subtables[dd->perm[index]].varType = CUDD_VAR_NEXT_STATE;
4026    return(1);
4027
4028} /* end of Cudd_bddSetNsVar */
4029
4030
4031/**Function********************************************************************
4032
4033  Synopsis    [Checks whether a variable is primary input.]
4034
4035  Description [Checks whether a variable is primary input.  Returns 1 if
4036  the variable's type is primary input; 0 if the variable exists but is
4037  not a primary input; -1 if the variable does not exist.]
4038
4039  SideEffects [none]
4040
4041  SeeAlso     [Cudd_bddSetPiVar Cudd_bddIsPsVar Cudd_bddIsNsVar]
4042
4043******************************************************************************/
4044int
4045Cudd_bddIsPiVar(
4046  DdManager *dd /* manager */,
4047  int index /* variable index */)
4048{
4049    if (index >= dd->size || index < 0) return -1;
4050    return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_PRIMARY_INPUT);
4051
4052} /* end of Cudd_bddIsPiVar */
4053
4054
4055/**Function********************************************************************
4056
4057  Synopsis    [Checks whether a variable is present state.]
4058
4059  Description [Checks whether a variable is present state.  Returns 1 if
4060  the variable's type is present state; 0 if the variable exists but is
4061  not a present state; -1 if the variable does not exist.]
4062
4063  SideEffects [none]
4064
4065  SeeAlso     [Cudd_bddSetPsVar Cudd_bddIsPiVar Cudd_bddIsNsVar]
4066
4067******************************************************************************/
4068int
4069Cudd_bddIsPsVar(
4070  DdManager *dd,
4071  int index)
4072{
4073    if (index >= dd->size || index < 0) return -1;
4074    return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_PRESENT_STATE);
4075
4076} /* end of Cudd_bddIsPsVar */
4077
4078
4079/**Function********************************************************************
4080
4081  Synopsis    [Checks whether a variable is next state.]
4082
4083  Description [Checks whether a variable is next state.  Returns 1 if
4084  the variable's type is present state; 0 if the variable exists but is
4085  not a present state; -1 if the variable does not exist.]
4086
4087  SideEffects [none]
4088
4089  SeeAlso     [Cudd_bddSetNsVar Cudd_bddIsPiVar Cudd_bddIsPsVar]
4090
4091******************************************************************************/
4092int
4093Cudd_bddIsNsVar(
4094  DdManager *dd,
4095  int index)
4096{
4097    if (index >= dd->size || index < 0) return -1;
4098    return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_NEXT_STATE);
4099
4100} /* end of Cudd_bddIsNsVar */
4101
4102
4103/**Function********************************************************************
4104
4105  Synopsis    [Sets a corresponding pair index for a given index.]
4106
4107  Description [Sets a corresponding pair index for a given index.
4108  These pair indices are present and next state variable.  Returns 1 if
4109  successful; 0 otherwise.]
4110
4111  SideEffects [modifies the manager]
4112
4113  SeeAlso     [Cudd_bddReadPairIndex]
4114
4115******************************************************************************/
4116int
4117Cudd_bddSetPairIndex(
4118  DdManager *dd /* manager */,
4119  int index /* variable index */,
4120  int pairIndex /* corresponding variable index */)
4121{
4122    if (index >= dd->size || index < 0) return(0);
4123    dd->subtables[dd->perm[index]].pairIndex = pairIndex;
4124    return(1);
4125
4126} /* end of Cudd_bddSetPairIndex */
4127
4128
4129/**Function********************************************************************
4130
4131  Synopsis    [Reads a corresponding pair index for a given index.]
4132
4133  Description [Reads a corresponding pair index for a given index.
4134  These pair indices are present and next state variable.  Returns the
4135  corresponding variable index if the variable exists; -1 otherwise.]
4136
4137  SideEffects [modifies the manager]
4138
4139  SeeAlso     [Cudd_bddSetPairIndex]
4140
4141******************************************************************************/
4142int
4143Cudd_bddReadPairIndex(
4144  DdManager *dd,
4145  int index)
4146{
4147    if (index >= dd->size || index < 0) return -1;
4148    return dd->subtables[dd->perm[index]].pairIndex;
4149
4150} /* end of Cudd_bddReadPairIndex */
4151
4152
4153/**Function********************************************************************
4154
4155  Synopsis    [Sets a variable to be grouped.]
4156
4157  Description [Sets a variable to be grouped. This function is used for
4158  lazy sifting.  Returns 1 if successful; 0 otherwise.]
4159
4160  SideEffects [modifies the manager]
4161
4162  SeeAlso     [Cudd_bddSetVarHardGroup Cudd_bddResetVarToBeGrouped]
4163
4164******************************************************************************/
4165int
4166Cudd_bddSetVarToBeGrouped(
4167  DdManager *dd,
4168  int index)
4169{
4170    if (index >= dd->size || index < 0) return(0);
4171    if (dd->subtables[dd->perm[index]].varToBeGrouped <= CUDD_LAZY_SOFT_GROUP) {
4172        dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_SOFT_GROUP;
4173    }
4174    return(1);
4175
4176} /* end of Cudd_bddSetVarToBeGrouped */
4177
4178
4179/**Function********************************************************************
4180
4181  Synopsis    [Sets a variable to be a hard group.]
4182
4183  Description [Sets a variable to be a hard group.  This function is used
4184  for lazy sifting.  Returns 1 if successful; 0 otherwise.]
4185
4186  SideEffects [modifies the manager]
4187
4188  SeeAlso     [Cudd_bddSetVarToBeGrouped Cudd_bddResetVarToBeGrouped
4189  Cudd_bddIsVarHardGroup]
4190
4191******************************************************************************/
4192int
4193Cudd_bddSetVarHardGroup(
4194  DdManager *dd,
4195  int index)
4196{
4197    if (index >= dd->size || index < 0) return(0);
4198    dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_HARD_GROUP;
4199    return(1);
4200
4201} /* end of Cudd_bddSetVarHardGrouped */
4202
4203
4204/**Function********************************************************************
4205
4206  Synopsis    [Resets a variable not to be grouped.]
4207
4208  Description [Resets a variable not to be grouped.  This function is
4209  used for lazy sifting.  Returns 1 if successful; 0 otherwise.]
4210
4211  SideEffects [modifies the manager]
4212
4213  SeeAlso     [Cudd_bddSetVarToBeGrouped Cudd_bddSetVarHardGroup]
4214
4215******************************************************************************/
4216int
4217Cudd_bddResetVarToBeGrouped(
4218  DdManager *dd,
4219  int index)
4220{
4221    if (index >= dd->size || index < 0) return(0);
4222    if (dd->subtables[dd->perm[index]].varToBeGrouped <=
4223        CUDD_LAZY_SOFT_GROUP) {
4224        dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_NONE;
4225    }
4226    return(1);
4227
4228} /* end of Cudd_bddResetVarToBeGrouped */
4229
4230
4231/**Function********************************************************************
4232
4233  Synopsis    [Checks whether a variable is set to be grouped.]
4234
4235  Description [Checks whether a variable is set to be grouped. This
4236  function is used for lazy sifting.]
4237
4238  SideEffects [none]
4239
4240  SeeAlso     []
4241
4242******************************************************************************/
4243int
4244Cudd_bddIsVarToBeGrouped(
4245  DdManager *dd,
4246  int index)
4247{
4248    if (index >= dd->size || index < 0) return(-1);
4249    if (dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_UNGROUP)
4250        return(0);
4251    else
4252        return(dd->subtables[dd->perm[index]].varToBeGrouped);
4253
4254} /* end of Cudd_bddIsVarToBeGrouped */
4255
4256
4257/**Function********************************************************************
4258
4259  Synopsis    [Sets a variable to be ungrouped.]
4260
4261  Description [Sets a variable to be ungrouped. This function is used
4262  for lazy sifting.  Returns 1 if successful; 0 otherwise.]
4263
4264  SideEffects [modifies the manager]
4265
4266  SeeAlso     [Cudd_bddIsVarToBeUngrouped]
4267
4268******************************************************************************/
4269int
4270Cudd_bddSetVarToBeUngrouped(
4271  DdManager *dd,
4272  int index)
4273{
4274    if (index >= dd->size || index < 0) return(0);
4275    dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_UNGROUP;
4276    return(1);
4277
4278} /* end of Cudd_bddSetVarToBeGrouped */
4279
4280
4281/**Function********************************************************************
4282
4283  Synopsis    [Checks whether a variable is set to be ungrouped.]
4284
4285  Description [Checks whether a variable is set to be ungrouped. This
4286  function is used for lazy sifting.  Returns 1 if the variable is marked
4287  to be ungrouped; 0 if the variable exists, but it is not marked to be
4288  ungrouped; -1 if the variable does not exist.]
4289
4290  SideEffects [none]
4291
4292  SeeAlso     [Cudd_bddSetVarToBeUngrouped]
4293
4294******************************************************************************/
4295int
4296Cudd_bddIsVarToBeUngrouped(
4297  DdManager *dd,
4298  int index)
4299{
4300    if (index >= dd->size || index < 0) return(-1);
4301    return dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_UNGROUP;
4302
4303} /* end of Cudd_bddIsVarToBeGrouped */
4304
4305
4306/**Function********************************************************************
4307
4308  Synopsis    [Checks whether a variable is set to be in a hard group.]
4309
4310  Description [Checks whether a variable is set to be in a hard group.  This
4311  function is used for lazy sifting.  Returns 1 if the variable is marked
4312  to be in a hard group; 0 if the variable exists, but it is not marked to be
4313  in a hard group; -1 if the variable does not exist.]
4314
4315  SideEffects [none]
4316
4317  SeeAlso     [Cudd_bddSetVarHardGroup]
4318
4319******************************************************************************/
4320int
4321Cudd_bddIsVarHardGroup(
4322  DdManager *dd,
4323  int index)
4324{
4325    if (index >= dd->size || index < 0) return(-1);
4326    if (dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_HARD_GROUP)
4327        return(1);
4328    return(0);
4329
4330} /* end of Cudd_bddIsVarToBeGrouped */
4331
4332
4333/*---------------------------------------------------------------------------*/
4334/* Definition of internal functions                                          */
4335/*---------------------------------------------------------------------------*/
4336
4337/*---------------------------------------------------------------------------*/
4338/* Definition of static functions                                            */
4339/*---------------------------------------------------------------------------*/
4340
4341
4342/**Function********************************************************************
4343
4344  Synopsis    [Fixes a variable group tree.]
4345
4346  Description []
4347
4348  SideEffects [Changes the variable group tree.]
4349
4350  SeeAlso     []
4351
4352******************************************************************************/
4353static void
4354fixVarTree(
4355  MtrNode * treenode,
4356  int * perm,
4357  int  size)
4358{
4359    treenode->index = treenode->low;
4360    treenode->low = ((int) treenode->index < size) ?
4361        perm[treenode->index] : treenode->index;
4362    if (treenode->child != NULL)
4363        fixVarTree(treenode->child, perm, size);
4364    if (treenode->younger != NULL)
4365        fixVarTree(treenode->younger, perm, size);
4366    return;
4367
4368} /* end of fixVarTree */
4369
4370
4371/**Function********************************************************************
4372
4373  Synopsis    [Adds multiplicity groups to a ZDD variable group tree.]
4374
4375  Description [Adds multiplicity groups to a ZDD variable group tree.
4376  Returns 1 if successful; 0 otherwise. This function creates the groups
4377  for set of ZDD variables (whose cardinality is given by parameter
4378  multiplicity) that are created for each BDD variable in
4379  Cudd_zddVarsFromBddVars. The crux of the matter is to determine the index
4380  each new group. (The index of the first variable in the group.)
4381  We first build all the groups for the children of a node, and then deal
4382  with the ZDD variables that are directly attached to the node. The problem
4383  for these is that the tree itself does not provide information on their
4384  position inside the group. While we deal with the children of the node,
4385  therefore, we keep track of all the positions they occupy. The remaining
4386  positions in the tree can be freely used. Also, we keep track of all the
4387  variables placed in the children. All the remaining variables are directly
4388  attached to the group. We can then place any pair of variables not yet
4389  grouped in any pair of available positions in the node.]
4390
4391  SideEffects [Changes the variable group tree.]
4392
4393  SeeAlso     [Cudd_zddVarsFromBddVars]
4394
4395******************************************************************************/
4396static int
4397addMultiplicityGroups(
4398  DdManager *dd /* manager */,
4399  MtrNode *treenode /* current tree node */,
4400  int multiplicity /* how many ZDD vars per BDD var */,
4401  char *vmask /* variable pairs for which a group has been already built */,
4402  char *lmask /* levels for which a group has already been built*/)
4403{
4404    int startV, stopV, startL;
4405    int i, j;
4406    MtrNode *auxnode = treenode;
4407
4408    while (auxnode != NULL) {
4409        if (auxnode->child != NULL) {
4410            addMultiplicityGroups(dd,auxnode->child,multiplicity,vmask,lmask);
4411        }
4412        /* Build remaining groups. */
4413        startV = dd->permZ[auxnode->index] / multiplicity;
4414        startL = auxnode->low / multiplicity;
4415        stopV = startV + auxnode->size / multiplicity;
4416        /* Walk down vmask starting at startV and build missing groups. */
4417        for (i = startV, j = startL; i < stopV; i++) {
4418            if (vmask[i] == 0) {
4419                MtrNode *node;
4420                while (lmask[j] == 1) j++;
4421                node = Mtr_MakeGroup(auxnode, j * multiplicity, multiplicity,
4422                                     MTR_FIXED);
4423                if (node == NULL) {
4424                    return(0);
4425                }
4426                node->index = dd->invpermZ[i * multiplicity];
4427                vmask[i] = 1;
4428                lmask[j] = 1;
4429            }
4430        }
4431        auxnode = auxnode->younger;
4432    }
4433    return(1);
4434
4435} /* end of addMultiplicityGroups */
4436
Note: See TracBrowser for help on using the repository browser.