source: vis_dev/glu-2.3/src/cuBdd/cuddAPI.c @ 91

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

library glu 2.3

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.59 2009/02/19 16:14:14 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        unsigned 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        unsigned 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 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",
2970                     (int) autoMethod);
2971    if (retval == EOF) return(0);
2972    retval = fprintf(fp,"Dynamic reordering of ZDDs enabled: %s\n",
2973                     Cudd_ReorderingStatusZdd(dd,&autoMethodZ) ? "yes" : "no");
2974    if (retval == EOF) return(0);
2975    retval = fprintf(fp,"Default ZDD reordering method: %d\n",
2976                     (int) autoMethodZ);
2977    if (retval == EOF) return(0);
2978    retval = fprintf(fp,"Realignment of ZDDs to BDDs enabled: %s\n",
2979                     Cudd_zddRealignmentEnabled(dd) ? "yes" : "no");
2980    if (retval == EOF) return(0);
2981    retval = fprintf(fp,"Realignment of BDDs to ZDDs enabled: %s\n",
2982                     Cudd_bddRealignmentEnabled(dd) ? "yes" : "no");
2983    if (retval == EOF) return(0);
2984    retval = fprintf(fp,"Dead nodes counted in triggering reordering: %s\n",
2985                     Cudd_DeadAreCounted(dd) ? "yes" : "no");
2986    if (retval == EOF) return(0);
2987    retval = fprintf(fp,"Group checking criterion: %d\n",
2988                     (int) Cudd_ReadGroupcheck(dd));
2989    if (retval == EOF) return(0);
2990    retval = fprintf(fp,"Recombination threshold: %d\n", Cudd_ReadRecomb(dd));
2991    if (retval == EOF) return(0);
2992    retval = fprintf(fp,"Symmetry violation threshold: %d\n",
2993                     Cudd_ReadSymmviolation(dd));
2994    if (retval == EOF) return(0);
2995    retval = fprintf(fp,"Arc violation threshold: %d\n",
2996                     Cudd_ReadArcviolation(dd));
2997    if (retval == EOF) return(0);
2998    retval = fprintf(fp,"GA population size: %d\n",
2999                     Cudd_ReadPopulationSize(dd));
3000    if (retval == EOF) return(0);
3001    retval = fprintf(fp,"Number of crossovers for GA: %d\n",
3002                     Cudd_ReadNumberXovers(dd));
3003    if (retval == EOF) return(0);
3004    retval = fprintf(fp,"Next reordering threshold: %u\n",
3005                     Cudd_ReadNextReordering(dd));
3006    if (retval == EOF) return(0);
3007
3008    /* Non-modifiable parameters. */
3009    retval = fprintf(fp,"**** CUDD non-modifiable parameters ****\n");
3010    if (retval == EOF) return(0);
3011    retval = fprintf(fp,"Memory in use: %lu\n", Cudd_ReadMemoryInUse(dd));
3012    if (retval == EOF) return(0);
3013    retval = fprintf(fp,"Peak number of nodes: %ld\n",
3014                     Cudd_ReadPeakNodeCount(dd));
3015    if (retval == EOF) return(0);
3016    retval = fprintf(fp,"Peak number of live nodes: %d\n",
3017                     Cudd_ReadPeakLiveNodeCount(dd));
3018    if (retval == EOF) return(0);
3019    retval = fprintf(fp,"Number of BDD variables: %d\n", dd->size);
3020    if (retval == EOF) return(0);
3021    retval = fprintf(fp,"Number of ZDD variables: %d\n", dd->sizeZ);
3022    if (retval == EOF) return(0);
3023    retval = fprintf(fp,"Number of cache entries: %u\n", dd->cacheSlots);
3024    if (retval == EOF) return(0);
3025    retval = fprintf(fp,"Number of cache look-ups: %.0f\n",
3026                     Cudd_ReadCacheLookUps(dd));
3027    if (retval == EOF) return(0);
3028    retval = fprintf(fp,"Number of cache hits: %.0f\n",
3029                     Cudd_ReadCacheHits(dd));
3030    if (retval == EOF) return(0);
3031    retval = fprintf(fp,"Number of cache insertions: %.0f\n",
3032                     dd->cacheinserts);
3033    if (retval == EOF) return(0);
3034    retval = fprintf(fp,"Number of cache collisions: %.0f\n",
3035                     dd->cachecollisions);
3036    if (retval == EOF) return(0);
3037    retval = fprintf(fp,"Number of cache deletions: %.0f\n",
3038                     dd->cachedeletions);
3039    if (retval == EOF) return(0);
3040    retval = cuddCacheProfile(dd,fp);
3041    if (retval == 0) return(0);
3042    retval = fprintf(fp,"Soft limit for cache size: %u\n",
3043                     Cudd_ReadMaxCache(dd));
3044    if (retval == EOF) return(0);
3045    retval = fprintf(fp,"Number of buckets in unique table: %u\n", dd->slots);
3046    if (retval == EOF) return(0);
3047    retval = fprintf(fp,"Used buckets in unique table: %.2f%% (expected %.2f%%)\n",
3048                     100.0 * Cudd_ReadUsedSlots(dd),
3049                     100.0 * Cudd_ExpectedUsedSlots(dd));
3050    if (retval == EOF) return(0);
3051#ifdef DD_UNIQUE_PROFILE
3052    retval = fprintf(fp,"Unique lookups: %.0f\n", dd->uniqueLookUps);
3053    if (retval == EOF) return(0);
3054    retval = fprintf(fp,"Unique links: %.0f (%g per lookup)\n",
3055            dd->uniqueLinks, dd->uniqueLinks / dd->uniqueLookUps);
3056    if (retval == EOF) return(0);
3057#endif
3058    retval = fprintf(fp,"Number of BDD and ADD nodes: %u\n", dd->keys);
3059    if (retval == EOF) return(0);
3060    retval = fprintf(fp,"Number of ZDD nodes: %u\n", dd->keysZ);
3061    if (retval == EOF) return(0);
3062    retval = fprintf(fp,"Number of dead BDD and ADD nodes: %u\n", dd->dead);
3063    if (retval == EOF) return(0);
3064    retval = fprintf(fp,"Number of dead ZDD nodes: %u\n", dd->deadZ);
3065    if (retval == EOF) return(0);
3066    retval = fprintf(fp,"Total number of nodes allocated: %.0f\n",
3067                     dd->allocated);
3068    if (retval == EOF) return(0);
3069    retval = fprintf(fp,"Total number of nodes reclaimed: %.0f\n",
3070                     dd->reclaimed);
3071    if (retval == EOF) return(0);
3072#ifdef DD_STATS
3073    retval = fprintf(fp,"Nodes freed: %.0f\n", dd->nodesFreed);
3074    if (retval == EOF) return(0);
3075    retval = fprintf(fp,"Nodes dropped: %.0f\n", dd->nodesDropped);
3076    if (retval == EOF) return(0);
3077#endif
3078#ifdef DD_COUNT
3079    retval = fprintf(fp,"Number of recursive calls: %.0f\n",
3080                     Cudd_ReadRecursiveCalls(dd));
3081    if (retval == EOF) return(0);
3082#endif
3083    retval = fprintf(fp,"Garbage collections so far: %d\n",
3084                     Cudd_ReadGarbageCollections(dd));
3085    if (retval == EOF) return(0);
3086    retval = fprintf(fp,"Time for garbage collection: %.2f sec\n",
3087                     ((double)Cudd_ReadGarbageCollectionTime(dd)/1000.0));
3088    if (retval == EOF) return(0);
3089    retval = fprintf(fp,"Reorderings so far: %d\n", dd->reorderings);
3090    if (retval == EOF) return(0);
3091    retval = fprintf(fp,"Time for reordering: %.2f sec\n",
3092                     ((double)Cudd_ReadReorderingTime(dd)/1000.0));
3093    if (retval == EOF) return(0);
3094#ifdef DD_COUNT
3095    retval = fprintf(fp,"Node swaps in reordering: %.0f\n",
3096        Cudd_ReadSwapSteps(dd));
3097    if (retval == EOF) return(0);
3098#endif
3099
3100    return(1);
3101
3102} /* end of Cudd_PrintInfo */
3103
3104
3105/**Function********************************************************************
3106
3107  Synopsis    [Reports the peak number of nodes.]
3108
3109  Description [Reports the peak number of nodes. This number includes
3110  node on the free list. At the peak, the number of nodes on the free
3111  list is guaranteed to be less than DD_MEM_CHUNK.]
3112
3113  SideEffects [None]
3114
3115  SeeAlso     [Cudd_ReadNodeCount Cudd_PrintInfo]
3116
3117******************************************************************************/
3118long
3119Cudd_ReadPeakNodeCount(
3120  DdManager * dd)
3121{
3122    long count = 0;
3123    DdNodePtr *scan = dd->memoryList;
3124
3125    while (scan != NULL) {
3126        count += DD_MEM_CHUNK;
3127        scan = (DdNodePtr *) *scan;
3128    }
3129    return(count);
3130
3131} /* end of Cudd_ReadPeakNodeCount */
3132
3133
3134/**Function********************************************************************
3135
3136  Synopsis    [Reports the peak number of live nodes.]
3137
3138  Description [Reports the peak number of live nodes. This count is kept
3139  only if CUDD is compiled with DD_STATS defined. If DD_STATS is not
3140  defined, this function returns -1.]
3141
3142  SideEffects [None]
3143
3144  SeeAlso     [Cudd_ReadNodeCount Cudd_PrintInfo Cudd_ReadPeakNodeCount]
3145
3146******************************************************************************/
3147int
3148Cudd_ReadPeakLiveNodeCount(
3149  DdManager * dd)
3150{
3151    unsigned int live = dd->keys - dd->dead;
3152
3153    if (live > dd->peakLiveNodes) {
3154        dd->peakLiveNodes = live;
3155    }
3156    return((int)dd->peakLiveNodes);
3157
3158} /* end of Cudd_ReadPeakLiveNodeCount */
3159
3160
3161/**Function********************************************************************
3162
3163  Synopsis    [Reports the number of nodes in BDDs and ADDs.]
3164
3165  Description [Reports the number of live nodes in BDDs and ADDs. This
3166  number does not include the isolated projection functions and the
3167  unused constants. These nodes that are not counted are not part of
3168  the DDs manipulated by the application.]
3169
3170  SideEffects [None]
3171
3172  SeeAlso     [Cudd_ReadPeakNodeCount Cudd_zddReadNodeCount]
3173
3174******************************************************************************/
3175long
3176Cudd_ReadNodeCount(
3177  DdManager * dd)
3178{
3179    long count;
3180    int i;
3181
3182#ifndef DD_NO_DEATH_ROW
3183    cuddClearDeathRow(dd);
3184#endif
3185
3186    count = (long) (dd->keys - dd->dead);
3187
3188    /* Count isolated projection functions. Their number is subtracted
3189    ** from the node count because they are not part of the BDDs.
3190    */
3191    for (i=0; i < dd->size; i++) {
3192        if (dd->vars[i]->ref == 1) count--;
3193    }
3194    /* Subtract from the count the unused constants. */
3195    if (DD_ZERO(dd)->ref == 1) count--;
3196    if (DD_PLUS_INFINITY(dd)->ref == 1) count--;
3197    if (DD_MINUS_INFINITY(dd)->ref == 1) count--;
3198
3199    return(count);
3200
3201} /* end of Cudd_ReadNodeCount */
3202
3203
3204
3205/**Function********************************************************************
3206
3207  Synopsis    [Reports the number of nodes in ZDDs.]
3208
3209  Description [Reports the number of nodes in ZDDs. This
3210  number always includes the two constants 1 and 0.]
3211
3212  SideEffects [None]
3213
3214  SeeAlso     [Cudd_ReadPeakNodeCount Cudd_ReadNodeCount]
3215
3216******************************************************************************/
3217long
3218Cudd_zddReadNodeCount(
3219  DdManager * dd)
3220{
3221    return((long)(dd->keysZ - dd->deadZ + 2));
3222
3223} /* end of Cudd_zddReadNodeCount */
3224
3225
3226/**Function********************************************************************
3227
3228  Synopsis    [Adds a function to a hook.]
3229
3230  Description [Adds a function to a hook. A hook is a list of
3231  application-provided functions called on certain occasions by the
3232  package. Returns 1 if the function is successfully added; 2 if the
3233  function was already in the list; 0 otherwise.]
3234
3235  SideEffects [None]
3236
3237  SeeAlso     [Cudd_RemoveHook]
3238
3239******************************************************************************/
3240int
3241Cudd_AddHook(
3242  DdManager * dd,
3243  DD_HFP f,
3244  Cudd_HookType where)
3245{
3246    DdHook **hook, *nextHook, *newHook;
3247
3248    switch (where) {
3249    case CUDD_PRE_GC_HOOK:
3250        hook = &(dd->preGCHook);
3251        break;
3252    case CUDD_POST_GC_HOOK:
3253        hook = &(dd->postGCHook);
3254        break;
3255    case CUDD_PRE_REORDERING_HOOK:
3256        hook = &(dd->preReorderingHook);
3257        break;
3258    case CUDD_POST_REORDERING_HOOK:
3259        hook = &(dd->postReorderingHook);
3260        break;
3261    default:
3262        return(0);
3263    }
3264    /* Scan the list and find whether the function is already there.
3265    ** If so, just return. */
3266    nextHook = *hook;
3267    while (nextHook != NULL) {
3268        if (nextHook->f == f) {
3269            return(2);
3270        }
3271        hook = &(nextHook->next);
3272        nextHook = nextHook->next;
3273    }
3274    /* The function was not in the list. Create a new item and append it
3275    ** to the end of the list. */
3276    newHook = ALLOC(DdHook,1);
3277    if (newHook == NULL) {
3278        dd->errorCode = CUDD_MEMORY_OUT;
3279        return(0);
3280    }
3281    newHook->next = NULL;
3282    newHook->f = f;
3283    *hook = newHook;
3284    return(1);
3285
3286} /* end of Cudd_AddHook */
3287
3288
3289/**Function********************************************************************
3290
3291  Synopsis    [Removes a function from a hook.]
3292
3293  Description [Removes a function from a hook. A hook is a list of
3294  application-provided functions called on certain occasions by the
3295  package. Returns 1 if successful; 0 the function was not in the list.]
3296
3297  SideEffects [None]
3298
3299  SeeAlso     [Cudd_AddHook]
3300
3301******************************************************************************/
3302int
3303Cudd_RemoveHook(
3304  DdManager * dd,
3305  DD_HFP f,
3306  Cudd_HookType where)
3307{
3308    DdHook **hook, *nextHook;
3309
3310    switch (where) {
3311    case CUDD_PRE_GC_HOOK:
3312        hook = &(dd->preGCHook);
3313        break;
3314    case CUDD_POST_GC_HOOK:
3315        hook = &(dd->postGCHook);
3316        break;
3317    case CUDD_PRE_REORDERING_HOOK:
3318        hook = &(dd->preReorderingHook);
3319        break;
3320    case CUDD_POST_REORDERING_HOOK:
3321        hook = &(dd->postReorderingHook);
3322        break;
3323    default:
3324        return(0);
3325    }
3326    nextHook = *hook;
3327    while (nextHook != NULL) {
3328        if (nextHook->f == f) {
3329            *hook = nextHook->next;
3330            FREE(nextHook);
3331            return(1);
3332        }
3333        hook = &(nextHook->next);
3334        nextHook = nextHook->next;
3335    }
3336
3337    return(0);
3338
3339} /* end of Cudd_RemoveHook */
3340
3341
3342/**Function********************************************************************
3343
3344  Synopsis    [Checks whether a function is in a hook.]
3345
3346  Description [Checks whether a function is in a hook. A hook is a list of
3347  application-provided functions called on certain occasions by the
3348  package. Returns 1 if the function is found; 0 otherwise.]
3349
3350  SideEffects [None]
3351
3352  SeeAlso     [Cudd_AddHook Cudd_RemoveHook]
3353
3354******************************************************************************/
3355int
3356Cudd_IsInHook(
3357  DdManager * dd,
3358  DD_HFP f,
3359  Cudd_HookType where)
3360{
3361    DdHook *hook;
3362
3363    switch (where) {
3364    case CUDD_PRE_GC_HOOK:
3365        hook = dd->preGCHook;
3366        break;
3367    case CUDD_POST_GC_HOOK:
3368        hook = dd->postGCHook;
3369        break;
3370    case CUDD_PRE_REORDERING_HOOK:
3371        hook = dd->preReorderingHook;
3372        break;
3373    case CUDD_POST_REORDERING_HOOK:
3374        hook = dd->postReorderingHook;
3375        break;
3376    default:
3377        return(0);
3378    }
3379    /* Scan the list and find whether the function is already there. */
3380    while (hook != NULL) {
3381        if (hook->f == f) {
3382            return(1);
3383        }
3384        hook = hook->next;
3385    }
3386    return(0);
3387
3388} /* end of Cudd_IsInHook */
3389
3390
3391/**Function********************************************************************
3392
3393  Synopsis    [Sample hook function to call before reordering.]
3394
3395  Description [Sample hook function to call before reordering.
3396  Prints on the manager's stdout reordering method and initial size.
3397  Returns 1 if successful; 0 otherwise.]
3398
3399  SideEffects [None]
3400
3401  SeeAlso     [Cudd_StdPostReordHook]
3402
3403******************************************************************************/
3404int
3405Cudd_StdPreReordHook(
3406  DdManager *dd,
3407  const char *str,
3408  void *data)
3409{
3410    Cudd_ReorderingType method = (Cudd_ReorderingType) (ptruint) data;
3411    int retval;
3412
3413    retval = fprintf(dd->out,"%s reordering with ", str);
3414    if (retval == EOF) return(0);
3415    switch (method) {
3416    case CUDD_REORDER_SIFT_CONVERGE:
3417    case CUDD_REORDER_SYMM_SIFT_CONV:
3418    case CUDD_REORDER_GROUP_SIFT_CONV:
3419    case CUDD_REORDER_WINDOW2_CONV:
3420    case CUDD_REORDER_WINDOW3_CONV:
3421    case CUDD_REORDER_WINDOW4_CONV:
3422    case CUDD_REORDER_LINEAR_CONVERGE:
3423        retval = fprintf(dd->out,"converging ");
3424        if (retval == EOF) return(0);
3425        break;
3426    default:
3427        break;
3428    }
3429    switch (method) {
3430    case CUDD_REORDER_RANDOM:
3431    case CUDD_REORDER_RANDOM_PIVOT:
3432        retval = fprintf(dd->out,"random");
3433        break;
3434    case CUDD_REORDER_SIFT:
3435    case CUDD_REORDER_SIFT_CONVERGE:
3436        retval = fprintf(dd->out,"sifting");
3437        break;
3438    case CUDD_REORDER_SYMM_SIFT:
3439    case CUDD_REORDER_SYMM_SIFT_CONV:
3440        retval = fprintf(dd->out,"symmetric sifting");
3441        break;
3442    case CUDD_REORDER_LAZY_SIFT:
3443        retval = fprintf(dd->out,"lazy sifting");
3444        break;
3445    case CUDD_REORDER_GROUP_SIFT:
3446    case CUDD_REORDER_GROUP_SIFT_CONV:
3447        retval = fprintf(dd->out,"group sifting");
3448        break;
3449    case CUDD_REORDER_WINDOW2:
3450    case CUDD_REORDER_WINDOW3:
3451    case CUDD_REORDER_WINDOW4:
3452    case CUDD_REORDER_WINDOW2_CONV:
3453    case CUDD_REORDER_WINDOW3_CONV:
3454    case CUDD_REORDER_WINDOW4_CONV:
3455        retval = fprintf(dd->out,"window");
3456        break;
3457    case CUDD_REORDER_ANNEALING:
3458        retval = fprintf(dd->out,"annealing");
3459        break;
3460    case CUDD_REORDER_GENETIC:
3461        retval = fprintf(dd->out,"genetic");
3462        break;
3463    case CUDD_REORDER_LINEAR:
3464    case CUDD_REORDER_LINEAR_CONVERGE:
3465        retval = fprintf(dd->out,"linear sifting");
3466        break;
3467    case CUDD_REORDER_EXACT:
3468        retval = fprintf(dd->out,"exact");
3469        break;
3470    default:
3471        return(0);
3472    }
3473    if (retval == EOF) return(0);
3474
3475    retval = fprintf(dd->out,": from %ld to ... ", strcmp(str, "BDD") == 0 ?
3476                     Cudd_ReadNodeCount(dd) : Cudd_zddReadNodeCount(dd));
3477    if (retval == EOF) return(0);
3478    fflush(dd->out);
3479    return(1);
3480
3481} /* end of Cudd_StdPreReordHook */
3482
3483
3484/**Function********************************************************************
3485
3486  Synopsis    [Sample hook function to call after reordering.]
3487
3488  Description [Sample hook function to call after reordering.
3489  Prints on the manager's stdout final size and reordering time.
3490  Returns 1 if successful; 0 otherwise.]
3491
3492  SideEffects [None]
3493
3494  SeeAlso     [Cudd_StdPreReordHook]
3495
3496******************************************************************************/
3497int
3498Cudd_StdPostReordHook(
3499  DdManager *dd,
3500  const char *str,
3501  void *data)
3502{
3503    long initialTime = (long) data;
3504    int retval;
3505    long finalTime = util_cpu_time();
3506    double totalTimeSec = (double)(finalTime - initialTime) / 1000.0;
3507
3508    retval = fprintf(dd->out,"%ld nodes in %g sec\n", strcmp(str, "BDD") == 0 ?
3509                     Cudd_ReadNodeCount(dd) : Cudd_zddReadNodeCount(dd),
3510                     totalTimeSec);
3511    if (retval == EOF) return(0);
3512    retval = fflush(dd->out);
3513    if (retval == EOF) return(0);
3514    return(1);
3515
3516} /* end of Cudd_StdPostReordHook */
3517
3518
3519/**Function********************************************************************
3520
3521  Synopsis    [Enables reporting of reordering stats.]
3522
3523  Description [Enables reporting of reordering stats.
3524  Returns 1 if successful; 0 otherwise.]
3525
3526  SideEffects [Installs functions in the pre-reordering and post-reordering
3527  hooks.]
3528
3529  SeeAlso     [Cudd_DisableReorderingReporting Cudd_ReorderingReporting]
3530
3531******************************************************************************/
3532int
3533Cudd_EnableReorderingReporting(
3534  DdManager *dd)
3535{
3536    if (!Cudd_AddHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) {
3537        return(0);
3538    }
3539    if (!Cudd_AddHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) {
3540        return(0);
3541    }
3542    return(1);
3543
3544} /* end of Cudd_EnableReorderingReporting */
3545
3546
3547/**Function********************************************************************
3548
3549  Synopsis    [Disables reporting of reordering stats.]
3550
3551  Description [Disables reporting of reordering stats.
3552  Returns 1 if successful; 0 otherwise.]
3553
3554  SideEffects [Removes functions from the pre-reordering and post-reordering
3555  hooks.]
3556
3557  SeeAlso     [Cudd_EnableReorderingReporting Cudd_ReorderingReporting]
3558
3559******************************************************************************/
3560int
3561Cudd_DisableReorderingReporting(
3562  DdManager *dd)
3563{
3564    if (!Cudd_RemoveHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) {
3565        return(0);
3566    }
3567    if (!Cudd_RemoveHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) {
3568        return(0);
3569    }
3570    return(1);
3571
3572} /* end of Cudd_DisableReorderingReporting */
3573
3574
3575/**Function********************************************************************
3576
3577  Synopsis    [Returns 1 if reporting of reordering stats is enabled.]
3578
3579  Description [Returns 1 if reporting of reordering stats is enabled;
3580  0 otherwise.]
3581
3582  SideEffects [none]
3583
3584  SeeAlso     [Cudd_EnableReorderingReporting Cudd_DisableReorderingReporting]
3585
3586******************************************************************************/
3587int
3588Cudd_ReorderingReporting(
3589  DdManager *dd)
3590{
3591    return(Cudd_IsInHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK));
3592
3593} /* end of Cudd_ReorderingReporting */
3594
3595
3596/**Function********************************************************************
3597
3598  Synopsis    [Returns the code of the last error.]
3599
3600  Description [Returns the code of the last error. The error codes are
3601  defined in cudd.h.]
3602
3603  SideEffects [None]
3604
3605  SeeAlso     [Cudd_ClearErrorCode]
3606
3607******************************************************************************/
3608Cudd_ErrorType
3609Cudd_ReadErrorCode(
3610  DdManager *dd)
3611{
3612    return(dd->errorCode);
3613
3614} /* end of Cudd_ReadErrorCode */
3615
3616
3617/**Function********************************************************************
3618
3619  Synopsis    [Clear the error code of a manager.]
3620
3621  Description []
3622
3623  SideEffects [None]
3624
3625  SeeAlso     [Cudd_ReadErrorCode]
3626
3627******************************************************************************/
3628void
3629Cudd_ClearErrorCode(
3630  DdManager *dd)
3631{
3632    dd->errorCode = CUDD_NO_ERROR;
3633
3634} /* end of Cudd_ClearErrorCode */
3635
3636
3637/**Function********************************************************************
3638
3639  Synopsis    [Reads the stdout of a manager.]
3640
3641  Description [Reads the stdout of a manager. This is the file pointer to
3642  which messages normally going to stdout are written. It is initialized
3643  to stdout. Cudd_SetStdout allows the application to redirect it.]
3644
3645  SideEffects [None]
3646
3647  SeeAlso     [Cudd_SetStdout Cudd_ReadStderr]
3648
3649******************************************************************************/
3650FILE *
3651Cudd_ReadStdout(
3652  DdManager *dd)
3653{
3654    return(dd->out);
3655
3656} /* end of Cudd_ReadStdout */
3657
3658
3659/**Function********************************************************************
3660
3661  Synopsis    [Sets the stdout of a manager.]
3662
3663  Description []
3664
3665  SideEffects [None]
3666
3667  SeeAlso     [Cudd_ReadStdout Cudd_SetStderr]
3668
3669******************************************************************************/
3670void
3671Cudd_SetStdout(
3672  DdManager *dd,
3673  FILE *fp)
3674{
3675    dd->out = fp;
3676
3677} /* end of Cudd_SetStdout */
3678
3679
3680/**Function********************************************************************
3681
3682  Synopsis    [Reads the stderr of a manager.]
3683
3684  Description [Reads the stderr of a manager. This is the file pointer to
3685  which messages normally going to stderr are written. It is initialized
3686  to stderr. Cudd_SetStderr allows the application to redirect it.]
3687
3688  SideEffects [None]
3689
3690  SeeAlso     [Cudd_SetStderr Cudd_ReadStdout]
3691
3692******************************************************************************/
3693FILE *
3694Cudd_ReadStderr(
3695  DdManager *dd)
3696{
3697    return(dd->err);
3698
3699} /* end of Cudd_ReadStderr */
3700
3701
3702/**Function********************************************************************
3703
3704  Synopsis    [Sets the stderr of a manager.]
3705
3706  Description []
3707
3708  SideEffects [None]
3709
3710  SeeAlso     [Cudd_ReadStderr Cudd_SetStdout]
3711
3712******************************************************************************/
3713void
3714Cudd_SetStderr(
3715  DdManager *dd,
3716  FILE *fp)
3717{
3718    dd->err = fp;
3719
3720} /* end of Cudd_SetStderr */
3721
3722
3723/**Function********************************************************************
3724
3725  Synopsis    [Returns the threshold for the next dynamic reordering.]
3726
3727  Description [Returns the threshold for the next dynamic reordering.
3728  The threshold is in terms of number of nodes and is in effect only
3729  if reordering is enabled. The count does not include the dead nodes,
3730  unless the countDead parameter of the manager has been changed from
3731  its default setting.]
3732
3733  SideEffects [None]
3734
3735  SeeAlso     [Cudd_SetNextReordering]
3736
3737******************************************************************************/
3738unsigned int
3739Cudd_ReadNextReordering(
3740  DdManager *dd)
3741{
3742    return(dd->nextDyn);
3743
3744} /* end of Cudd_ReadNextReordering */
3745
3746
3747/**Function********************************************************************
3748
3749  Synopsis    [Sets the threshold for the next dynamic reordering.]
3750
3751  Description [Sets the threshold for the next dynamic reordering.
3752  The threshold is in terms of number of nodes and is in effect only
3753  if reordering is enabled. The count does not include the dead nodes,
3754  unless the countDead parameter of the manager has been changed from
3755  its default setting.]
3756
3757  SideEffects [None]
3758
3759  SeeAlso     [Cudd_ReadNextReordering]
3760
3761******************************************************************************/
3762void
3763Cudd_SetNextReordering(
3764  DdManager *dd,
3765  unsigned int next)
3766{
3767    dd->nextDyn = next;
3768
3769} /* end of Cudd_SetNextReordering */
3770
3771
3772/**Function********************************************************************
3773
3774  Synopsis    [Reads the number of elementary reordering steps.]
3775
3776  Description []
3777
3778  SideEffects [none]
3779
3780  SeeAlso     []
3781
3782******************************************************************************/
3783double
3784Cudd_ReadSwapSteps(
3785  DdManager *dd)
3786{
3787#ifdef DD_COUNT
3788    return(dd->swapSteps);
3789#else
3790    return(-1);
3791#endif
3792
3793} /* end of Cudd_ReadSwapSteps */
3794
3795
3796/**Function********************************************************************
3797
3798  Synopsis    [Reads the maximum allowed number of live nodes.]
3799
3800  Description [Reads the maximum allowed number of live nodes. When this
3801  number is exceeded, the package returns NULL.]
3802
3803  SideEffects [none]
3804
3805  SeeAlso     [Cudd_SetMaxLive]
3806
3807******************************************************************************/
3808unsigned int
3809Cudd_ReadMaxLive(
3810  DdManager *dd)
3811{
3812    return(dd->maxLive);
3813
3814} /* end of Cudd_ReadMaxLive */
3815
3816
3817/**Function********************************************************************
3818
3819  Synopsis    [Sets the maximum allowed number of live nodes.]
3820
3821  Description [Sets the maximum allowed number of live nodes. When this
3822  number is exceeded, the package returns NULL.]
3823
3824  SideEffects [none]
3825
3826  SeeAlso     [Cudd_ReadMaxLive]
3827
3828******************************************************************************/
3829void
3830Cudd_SetMaxLive(
3831  DdManager *dd,
3832  unsigned int maxLive)
3833{
3834    dd->maxLive = maxLive;
3835
3836} /* end of Cudd_SetMaxLive */
3837
3838
3839/**Function********************************************************************
3840
3841  Synopsis    [Reads the maximum allowed memory.]
3842
3843  Description [Reads the maximum allowed memory. When this
3844  number is exceeded, the package returns NULL.]
3845
3846  SideEffects [none]
3847
3848  SeeAlso     [Cudd_SetMaxMemory]
3849
3850******************************************************************************/
3851unsigned long
3852Cudd_ReadMaxMemory(
3853  DdManager *dd)
3854{
3855    return(dd->maxmemhard);
3856
3857} /* end of Cudd_ReadMaxMemory */
3858
3859
3860/**Function********************************************************************
3861
3862  Synopsis    [Sets the maximum allowed memory.]
3863
3864  Description [Sets the maximum allowed memory. When this
3865  number is exceeded, the package returns NULL.]
3866
3867  SideEffects [none]
3868
3869  SeeAlso     [Cudd_ReadMaxMemory]
3870
3871******************************************************************************/
3872void
3873Cudd_SetMaxMemory(
3874  DdManager *dd,
3875  unsigned long maxMemory)
3876{
3877    dd->maxmemhard = maxMemory;
3878
3879} /* end of Cudd_SetMaxMemory */
3880
3881
3882/**Function********************************************************************
3883
3884  Synopsis    [Prevents sifting of a variable.]
3885
3886  Description [This function sets a flag to prevent sifting of a
3887  variable.  Returns 1 if successful; 0 otherwise (i.e., invalid
3888  variable index).]
3889
3890  SideEffects [Changes the "bindVar" flag in DdSubtable.]
3891
3892  SeeAlso     [Cudd_bddUnbindVar]
3893
3894******************************************************************************/
3895int
3896Cudd_bddBindVar(
3897  DdManager *dd /* manager */,
3898  int index /* variable index */)
3899{
3900    if (index >= dd->size || index < 0) return(0);
3901    dd->subtables[dd->perm[index]].bindVar = 1;
3902    return(1);
3903
3904} /* end of Cudd_bddBindVar */
3905
3906
3907/**Function********************************************************************
3908
3909  Synopsis    [Allows the sifting of a variable.]
3910
3911  Description [This function resets the flag that prevents the sifting
3912  of a variable. In successive variable reorderings, the variable will
3913  NOT be skipped, that is, sifted.  Initially all variables can be
3914  sifted. It is necessary to call this function only to re-enable
3915  sifting after a call to Cudd_bddBindVar. Returns 1 if successful; 0
3916  otherwise (i.e., invalid variable index).]
3917
3918  SideEffects [Changes the "bindVar" flag in DdSubtable.]
3919
3920  SeeAlso     [Cudd_bddBindVar]
3921
3922******************************************************************************/
3923int
3924Cudd_bddUnbindVar(
3925  DdManager *dd /* manager */,
3926  int index /* variable index */)
3927{
3928    if (index >= dd->size || index < 0) return(0);
3929    dd->subtables[dd->perm[index]].bindVar = 0;
3930    return(1);
3931
3932} /* end of Cudd_bddUnbindVar */
3933
3934
3935/**Function********************************************************************
3936
3937  Synopsis    [Tells whether a variable can be sifted.]
3938
3939  Description [This function returns 1 if a variable is enabled for
3940  sifting.  Initially all variables can be sifted. This function returns
3941  0 only if there has been a previous call to Cudd_bddBindVar for that
3942  variable not followed by a call to Cudd_bddUnbindVar. The function returns
3943  0 also in the case in which the index of the variable is out of bounds.]
3944
3945  SideEffects [none]
3946
3947  SeeAlso     [Cudd_bddBindVar Cudd_bddUnbindVar]
3948
3949******************************************************************************/
3950int
3951Cudd_bddVarIsBound(
3952  DdManager *dd /* manager */,
3953  int index /* variable index */)
3954{
3955    if (index >= dd->size || index < 0) return(0);
3956    return(dd->subtables[dd->perm[index]].bindVar);
3957
3958} /* end of Cudd_bddVarIsBound */
3959
3960
3961/**Function********************************************************************
3962
3963  Synopsis    [Sets a variable type to primary input.]
3964
3965  Description [Sets a variable type to primary input.  The variable type is
3966  used by lazy sifting.  Returns 1 if successful; 0 otherwise.]
3967
3968  SideEffects [modifies the manager]
3969
3970  SeeAlso     [Cudd_bddSetPsVar Cudd_bddSetNsVar Cudd_bddIsPiVar]
3971
3972******************************************************************************/
3973int
3974Cudd_bddSetPiVar(
3975  DdManager *dd /* manager */,
3976  int index /* variable index */)
3977{
3978    if (index >= dd->size || index < 0) return (0);
3979    dd->subtables[dd->perm[index]].varType = CUDD_VAR_PRIMARY_INPUT;
3980    return(1);
3981
3982} /* end of Cudd_bddSetPiVar */
3983
3984
3985/**Function********************************************************************
3986
3987  Synopsis    [Sets a variable type to present state.]
3988
3989  Description [Sets a variable type to present state.  The variable type is
3990  used by lazy sifting.  Returns 1 if successful; 0 otherwise.]
3991
3992  SideEffects [modifies the manager]
3993
3994  SeeAlso     [Cudd_bddSetPiVar Cudd_bddSetNsVar Cudd_bddIsPsVar]
3995
3996******************************************************************************/
3997int
3998Cudd_bddSetPsVar(
3999  DdManager *dd /* manager */,
4000  int index /* variable index */)
4001{
4002    if (index >= dd->size || index < 0) return (0);
4003    dd->subtables[dd->perm[index]].varType = CUDD_VAR_PRESENT_STATE;
4004    return(1);
4005
4006} /* end of Cudd_bddSetPsVar */
4007
4008
4009/**Function********************************************************************
4010
4011  Synopsis    [Sets a variable type to next state.]
4012
4013  Description [Sets a variable type to next state.  The variable type is
4014  used by lazy sifting.  Returns 1 if successful; 0 otherwise.]
4015
4016  SideEffects [modifies the manager]
4017
4018  SeeAlso     [Cudd_bddSetPiVar Cudd_bddSetPsVar Cudd_bddIsNsVar]
4019
4020******************************************************************************/
4021int
4022Cudd_bddSetNsVar(
4023  DdManager *dd /* manager */,
4024  int index /* variable index */)
4025{
4026    if (index >= dd->size || index < 0) return (0);
4027    dd->subtables[dd->perm[index]].varType = CUDD_VAR_NEXT_STATE;
4028    return(1);
4029
4030} /* end of Cudd_bddSetNsVar */
4031
4032
4033/**Function********************************************************************
4034
4035  Synopsis    [Checks whether a variable is primary input.]
4036
4037  Description [Checks whether a variable is primary input.  Returns 1 if
4038  the variable's type is primary input; 0 if the variable exists but is
4039  not a primary input; -1 if the variable does not exist.]
4040
4041  SideEffects [none]
4042
4043  SeeAlso     [Cudd_bddSetPiVar Cudd_bddIsPsVar Cudd_bddIsNsVar]
4044
4045******************************************************************************/
4046int
4047Cudd_bddIsPiVar(
4048  DdManager *dd /* manager */,
4049  int index /* variable index */)
4050{
4051    if (index >= dd->size || index < 0) return -1;
4052    return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_PRIMARY_INPUT);
4053
4054} /* end of Cudd_bddIsPiVar */
4055
4056
4057/**Function********************************************************************
4058
4059  Synopsis    [Checks whether a variable is present state.]
4060
4061  Description [Checks whether a variable is present state.  Returns 1 if
4062  the variable's type is present state; 0 if the variable exists but is
4063  not a present state; -1 if the variable does not exist.]
4064
4065  SideEffects [none]
4066
4067  SeeAlso     [Cudd_bddSetPsVar Cudd_bddIsPiVar Cudd_bddIsNsVar]
4068
4069******************************************************************************/
4070int
4071Cudd_bddIsPsVar(
4072  DdManager *dd,
4073  int index)
4074{
4075    if (index >= dd->size || index < 0) return -1;
4076    return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_PRESENT_STATE);
4077
4078} /* end of Cudd_bddIsPsVar */
4079
4080
4081/**Function********************************************************************
4082
4083  Synopsis    [Checks whether a variable is next state.]
4084
4085  Description [Checks whether a variable is next state.  Returns 1 if
4086  the variable's type is present state; 0 if the variable exists but is
4087  not a present state; -1 if the variable does not exist.]
4088
4089  SideEffects [none]
4090
4091  SeeAlso     [Cudd_bddSetNsVar Cudd_bddIsPiVar Cudd_bddIsPsVar]
4092
4093******************************************************************************/
4094int
4095Cudd_bddIsNsVar(
4096  DdManager *dd,
4097  int index)
4098{
4099    if (index >= dd->size || index < 0) return -1;
4100    return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_NEXT_STATE);
4101
4102} /* end of Cudd_bddIsNsVar */
4103
4104
4105/**Function********************************************************************
4106
4107  Synopsis    [Sets a corresponding pair index for a given index.]
4108
4109  Description [Sets a corresponding pair index for a given index.
4110  These pair indices are present and next state variable.  Returns 1 if
4111  successful; 0 otherwise.]
4112
4113  SideEffects [modifies the manager]
4114
4115  SeeAlso     [Cudd_bddReadPairIndex]
4116
4117******************************************************************************/
4118int
4119Cudd_bddSetPairIndex(
4120  DdManager *dd /* manager */,
4121  int index /* variable index */,
4122  int pairIndex /* corresponding variable index */)
4123{
4124    if (index >= dd->size || index < 0) return(0);
4125    dd->subtables[dd->perm[index]].pairIndex = pairIndex;
4126    return(1);
4127
4128} /* end of Cudd_bddSetPairIndex */
4129
4130
4131/**Function********************************************************************
4132
4133  Synopsis    [Reads a corresponding pair index for a given index.]
4134
4135  Description [Reads a corresponding pair index for a given index.
4136  These pair indices are present and next state variable.  Returns the
4137  corresponding variable index if the variable exists; -1 otherwise.]
4138
4139  SideEffects [modifies the manager]
4140
4141  SeeAlso     [Cudd_bddSetPairIndex]
4142
4143******************************************************************************/
4144int
4145Cudd_bddReadPairIndex(
4146  DdManager *dd,
4147  int index)
4148{
4149    if (index >= dd->size || index < 0) return -1;
4150    return dd->subtables[dd->perm[index]].pairIndex;
4151
4152} /* end of Cudd_bddReadPairIndex */
4153
4154
4155/**Function********************************************************************
4156
4157  Synopsis    [Sets a variable to be grouped.]
4158
4159  Description [Sets a variable to be grouped. This function is used for
4160  lazy sifting.  Returns 1 if successful; 0 otherwise.]
4161
4162  SideEffects [modifies the manager]
4163
4164  SeeAlso     [Cudd_bddSetVarHardGroup Cudd_bddResetVarToBeGrouped]
4165
4166******************************************************************************/
4167int
4168Cudd_bddSetVarToBeGrouped(
4169  DdManager *dd,
4170  int index)
4171{
4172    if (index >= dd->size || index < 0) return(0);
4173    if (dd->subtables[dd->perm[index]].varToBeGrouped <= CUDD_LAZY_SOFT_GROUP) {
4174        dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_SOFT_GROUP;
4175    }
4176    return(1);
4177
4178} /* end of Cudd_bddSetVarToBeGrouped */
4179
4180
4181/**Function********************************************************************
4182
4183  Synopsis    [Sets a variable to be a hard group.]
4184
4185  Description [Sets a variable to be a hard group.  This function is used
4186  for lazy sifting.  Returns 1 if successful; 0 otherwise.]
4187
4188  SideEffects [modifies the manager]
4189
4190  SeeAlso     [Cudd_bddSetVarToBeGrouped Cudd_bddResetVarToBeGrouped
4191  Cudd_bddIsVarHardGroup]
4192
4193******************************************************************************/
4194int
4195Cudd_bddSetVarHardGroup(
4196  DdManager *dd,
4197  int index)
4198{
4199    if (index >= dd->size || index < 0) return(0);
4200    dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_HARD_GROUP;
4201    return(1);
4202
4203} /* end of Cudd_bddSetVarHardGrouped */
4204
4205
4206/**Function********************************************************************
4207
4208  Synopsis    [Resets a variable not to be grouped.]
4209
4210  Description [Resets a variable not to be grouped.  This function is
4211  used for lazy sifting.  Returns 1 if successful; 0 otherwise.]
4212
4213  SideEffects [modifies the manager]
4214
4215  SeeAlso     [Cudd_bddSetVarToBeGrouped Cudd_bddSetVarHardGroup]
4216
4217******************************************************************************/
4218int
4219Cudd_bddResetVarToBeGrouped(
4220  DdManager *dd,
4221  int index)
4222{
4223    if (index >= dd->size || index < 0) return(0);
4224    if (dd->subtables[dd->perm[index]].varToBeGrouped <=
4225        CUDD_LAZY_SOFT_GROUP) {
4226        dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_NONE;
4227    }
4228    return(1);
4229
4230} /* end of Cudd_bddResetVarToBeGrouped */
4231
4232
4233/**Function********************************************************************
4234
4235  Synopsis    [Checks whether a variable is set to be grouped.]
4236
4237  Description [Checks whether a variable is set to be grouped. This
4238  function is used for lazy sifting.]
4239
4240  SideEffects [none]
4241
4242  SeeAlso     []
4243
4244******************************************************************************/
4245int
4246Cudd_bddIsVarToBeGrouped(
4247  DdManager *dd,
4248  int index)
4249{
4250    if (index >= dd->size || index < 0) return(-1);
4251    if (dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_UNGROUP)
4252        return(0);
4253    else
4254        return(dd->subtables[dd->perm[index]].varToBeGrouped);
4255
4256} /* end of Cudd_bddIsVarToBeGrouped */
4257
4258
4259/**Function********************************************************************
4260
4261  Synopsis    [Sets a variable to be ungrouped.]
4262
4263  Description [Sets a variable to be ungrouped. This function is used
4264  for lazy sifting.  Returns 1 if successful; 0 otherwise.]
4265
4266  SideEffects [modifies the manager]
4267
4268  SeeAlso     [Cudd_bddIsVarToBeUngrouped]
4269
4270******************************************************************************/
4271int
4272Cudd_bddSetVarToBeUngrouped(
4273  DdManager *dd,
4274  int index)
4275{
4276    if (index >= dd->size || index < 0) return(0);
4277    dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_UNGROUP;
4278    return(1);
4279
4280} /* end of Cudd_bddSetVarToBeGrouped */
4281
4282
4283/**Function********************************************************************
4284
4285  Synopsis    [Checks whether a variable is set to be ungrouped.]
4286
4287  Description [Checks whether a variable is set to be ungrouped. This
4288  function is used for lazy sifting.  Returns 1 if the variable is marked
4289  to be ungrouped; 0 if the variable exists, but it is not marked to be
4290  ungrouped; -1 if the variable does not exist.]
4291
4292  SideEffects [none]
4293
4294  SeeAlso     [Cudd_bddSetVarToBeUngrouped]
4295
4296******************************************************************************/
4297int
4298Cudd_bddIsVarToBeUngrouped(
4299  DdManager *dd,
4300  int index)
4301{
4302    if (index >= dd->size || index < 0) return(-1);
4303    return dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_UNGROUP;
4304
4305} /* end of Cudd_bddIsVarToBeGrouped */
4306
4307
4308/**Function********************************************************************
4309
4310  Synopsis    [Checks whether a variable is set to be in a hard group.]
4311
4312  Description [Checks whether a variable is set to be in a hard group.  This
4313  function is used for lazy sifting.  Returns 1 if the variable is marked
4314  to be in a hard group; 0 if the variable exists, but it is not marked to be
4315  in a hard group; -1 if the variable does not exist.]
4316
4317  SideEffects [none]
4318
4319  SeeAlso     [Cudd_bddSetVarHardGroup]
4320
4321******************************************************************************/
4322int
4323Cudd_bddIsVarHardGroup(
4324  DdManager *dd,
4325  int index)
4326{
4327    if (index >= dd->size || index < 0) return(-1);
4328    if (dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_HARD_GROUP)
4329        return(1);
4330    return(0);
4331
4332} /* end of Cudd_bddIsVarToBeGrouped */
4333
4334
4335/*---------------------------------------------------------------------------*/
4336/* Definition of internal functions                                          */
4337/*---------------------------------------------------------------------------*/
4338
4339/*---------------------------------------------------------------------------*/
4340/* Definition of static functions                                            */
4341/*---------------------------------------------------------------------------*/
4342
4343
4344/**Function********************************************************************
4345
4346  Synopsis    [Fixes a variable group tree.]
4347
4348  Description []
4349
4350  SideEffects [Changes the variable group tree.]
4351
4352  SeeAlso     []
4353
4354******************************************************************************/
4355static void
4356fixVarTree(
4357  MtrNode * treenode,
4358  int * perm,
4359  int  size)
4360{
4361    treenode->index = treenode->low;
4362    treenode->low = ((int) treenode->index < size) ?
4363        perm[treenode->index] : treenode->index;
4364    if (treenode->child != NULL)
4365        fixVarTree(treenode->child, perm, size);
4366    if (treenode->younger != NULL)
4367        fixVarTree(treenode->younger, perm, size);
4368    return;
4369
4370} /* end of fixVarTree */
4371
4372
4373/**Function********************************************************************
4374
4375  Synopsis    [Adds multiplicity groups to a ZDD variable group tree.]
4376
4377  Description [Adds multiplicity groups to a ZDD variable group tree.
4378  Returns 1 if successful; 0 otherwise. This function creates the groups
4379  for set of ZDD variables (whose cardinality is given by parameter
4380  multiplicity) that are created for each BDD variable in
4381  Cudd_zddVarsFromBddVars. The crux of the matter is to determine the index
4382  each new group. (The index of the first variable in the group.)
4383  We first build all the groups for the children of a node, and then deal
4384  with the ZDD variables that are directly attached to the node. The problem
4385  for these is that the tree itself does not provide information on their
4386  position inside the group. While we deal with the children of the node,
4387  therefore, we keep track of all the positions they occupy. The remaining
4388  positions in the tree can be freely used. Also, we keep track of all the
4389  variables placed in the children. All the remaining variables are directly
4390  attached to the group. We can then place any pair of variables not yet
4391  grouped in any pair of available positions in the node.]
4392
4393  SideEffects [Changes the variable group tree.]
4394
4395  SeeAlso     [Cudd_zddVarsFromBddVars]
4396
4397******************************************************************************/
4398static int
4399addMultiplicityGroups(
4400  DdManager *dd /* manager */,
4401  MtrNode *treenode /* current tree node */,
4402  int multiplicity /* how many ZDD vars per BDD var */,
4403  char *vmask /* variable pairs for which a group has been already built */,
4404  char *lmask /* levels for which a group has already been built*/)
4405{
4406    int startV, stopV, startL;
4407    int i, j;
4408    MtrNode *auxnode = treenode;
4409
4410    while (auxnode != NULL) {
4411        if (auxnode->child != NULL) {
4412            addMultiplicityGroups(dd,auxnode->child,multiplicity,vmask,lmask);
4413        }
4414        /* Build remaining groups. */
4415        startV = dd->permZ[auxnode->index] / multiplicity;
4416        startL = auxnode->low / multiplicity;
4417        stopV = startV + auxnode->size / multiplicity;
4418        /* Walk down vmask starting at startV and build missing groups. */
4419        for (i = startV, j = startL; i < stopV; i++) {
4420            if (vmask[i] == 0) {
4421                MtrNode *node;
4422                while (lmask[j] == 1) j++;
4423                node = Mtr_MakeGroup(auxnode, j * multiplicity, multiplicity,
4424                                     MTR_FIXED);
4425                if (node == NULL) {
4426                    return(0);
4427                }
4428                node->index = dd->invpermZ[i * multiplicity];
4429                vmask[i] = 1;
4430                lmask[j] = 1;
4431            }
4432        }
4433        auxnode = auxnode->younger;
4434    }
4435    return(1);
4436
4437} /* end of addMultiplicityGroups */
Note: See TracBrowser for help on using the repository browser.