1 /**CFile***********************************************************************
7 Synopsis [Application interface functions.]
9 Description [External procedures included in this module:
12 <li> Cudd_addNewVarAtLevel()
14 <li> Cudd_bddNewVarAtLevel()
18 <li> Cudd_zddVarsFromBddVars()
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()
34 <li> Cudd_ReadZddOne()
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()
47 <li> Cudd_ReadLooseUpTo()
48 <li> Cudd_SetLooseUpTo()
49 <li> Cudd_ReadMaxCache()
50 <li> Cudd_ReadMaxCacheHard()
51 <li> Cudd_SetMaxCacheHard()
54 <li> Cudd_ReadUsedSlots()
55 <li> Cudd_ExpectedUsedSlots()
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()
78 <li> Cudd_ReadZddTree()
79 <li> Cudd_SetZddTree()
80 <li> Cudd_FreeZddTree()
81 <li> Cudd_NodeReadIndex()
83 <li> Cudd_ReadInvPerm()
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()
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()
112 <li> Cudd_RemoveHook()
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()
151 Static procedures included in this module:
158 Author [Fabio Somenzi]
160 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
164 Redistribution and use in source and binary forms, with or without
165 modification, are permitted provided that the following conditions
168 Redistributions of source code must retain the above copyright
169 notice, this list of conditions and the following disclaimer.
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.
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.
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.]
192 ******************************************************************************/
197 /*---------------------------------------------------------------------------*/
198 /* Constant declarations */
199 /*---------------------------------------------------------------------------*/
201 /*---------------------------------------------------------------------------*/
202 /* Stucture declarations */
203 /*---------------------------------------------------------------------------*/
205 /*---------------------------------------------------------------------------*/
206 /* Type declarations */
207 /*---------------------------------------------------------------------------*/
209 /*---------------------------------------------------------------------------*/
210 /* Variable declarations */
211 /*---------------------------------------------------------------------------*/
214 static char rcsid
[] DD_UNUSED
= "$Id: cuddAPI.c,v 1.59 2009/02/19 16:14:14 fabio Exp $";
217 /*---------------------------------------------------------------------------*/
218 /* Macro declarations */
219 /*---------------------------------------------------------------------------*/
221 /**AutomaticStart*************************************************************/
223 /*---------------------------------------------------------------------------*/
224 /* Static function prototypes */
225 /*---------------------------------------------------------------------------*/
227 static void fixVarTree (MtrNode
*treenode
, int *perm
, int size
);
228 static int addMultiplicityGroups (DdManager
*dd
, MtrNode
*treenode
, int multiplicity
, char *vmask
, char *lmask
);
230 /**AutomaticEnd***************************************************************/
233 /*---------------------------------------------------------------------------*/
234 /* Definition of exported functions */
235 /*---------------------------------------------------------------------------*/
238 /**Function********************************************************************
240 Synopsis [Returns a new ADD variable.]
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. ]
250 SeeAlso [Cudd_bddNewVar Cudd_addIthVar Cudd_addConst
251 Cudd_addNewVarAtLevel]
253 ******************************************************************************/
260 if ((unsigned int) dd
->size
>= CUDD_MAXINDEX
- 1) return(NULL
);
263 res
= cuddUniqueInter(dd
,dd
->size
,DD_ONE(dd
),DD_ZERO(dd
));
264 } while (dd
->reordered
== 1);
268 } /* end of Cudd_addNewVar */
271 /**Function********************************************************************
273 Synopsis [Returns a new ADD variable at a specified level.]
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.]
282 SeeAlso [Cudd_addNewVar Cudd_addIthVar Cudd_bddNewVarAtLevel]
284 ******************************************************************************/
286 Cudd_addNewVarAtLevel(
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
);
297 res
= cuddUniqueInter(dd
,dd
->size
- 1,DD_ONE(dd
),DD_ZERO(dd
));
298 } while (dd
->reordered
== 1);
302 } /* end of Cudd_addNewVarAtLevel */
305 /**Function********************************************************************
307 Synopsis [Returns a new BDD variable.]
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.]
315 SeeAlso [Cudd_addNewVar Cudd_bddIthVar Cudd_bddNewVarAtLevel]
317 ******************************************************************************/
324 if ((unsigned int) dd
->size
>= CUDD_MAXINDEX
- 1) return(NULL
);
325 res
= cuddUniqueInter(dd
,dd
->size
,dd
->one
,Cudd_Not(dd
->one
));
329 } /* end of Cudd_bddNewVar */
332 /**Function********************************************************************
334 Synopsis [Returns a new BDD variable at a specified level.]
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.]
343 SeeAlso [Cudd_bddNewVar Cudd_bddIthVar Cudd_addNewVarAtLevel]
345 ******************************************************************************/
347 Cudd_bddNewVarAtLevel(
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];
360 } /* end of Cudd_bddNewVarAtLevel */
363 /**Function********************************************************************
365 Synopsis [Returns the ADD variable with index i.]
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. ]
375 SeeAlso [Cudd_addNewVar Cudd_bddIthVar Cudd_addConst
376 Cudd_addNewVarAtLevel]
378 ******************************************************************************/
386 if ((unsigned int) i
>= CUDD_MAXINDEX
- 1) return(NULL
);
389 res
= cuddUniqueInter(dd
,i
,DD_ONE(dd
),DD_ZERO(dd
));
390 } while (dd
->reordered
== 1);
394 } /* end of Cudd_addIthVar */
397 /**Function********************************************************************
399 Synopsis [Returns the BDD variable with index i.]
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.]
407 SeeAlso [Cudd_bddNewVar Cudd_addIthVar Cudd_bddNewVarAtLevel
410 ******************************************************************************/
418 if ((unsigned int) i
>= CUDD_MAXINDEX
- 1) return(NULL
);
422 res
= cuddUniqueInter(dd
,i
,dd
->one
,Cudd_Not(dd
->one
));
427 } /* end of Cudd_bddIthVar */
430 /**Function********************************************************************
432 Synopsis [Returns the ZDD variable with index i.]
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.]
440 SeeAlso [Cudd_bddIthVar Cudd_addIthVar]
442 ******************************************************************************/
453 if ((unsigned int) i
>= CUDD_MAXINDEX
- 1) return(NULL
);
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.
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
);
465 zvar
= cuddUniqueInterZdd(dd
, i
, lower
, DD_ZERO(dd
));
466 } while (dd
->reordered
== 1);
472 /* Now we add the "filler" nodes above the level of index i. */
473 for (j
= dd
->permZ
[i
] - 1; j
>= 0; j
--) {
476 res
= cuddUniqueInterZdd(dd
, dd
->invpermZ
[j
], zvar
, zvar
);
477 } while (dd
->reordered
== 1);
479 Cudd_RecursiveDerefZdd(dd
,zvar
);
483 Cudd_RecursiveDerefZdd(dd
,zvar
);
489 } /* end of Cudd_zddIthVar */
492 /**Function********************************************************************
494 Synopsis [Creates one or more ZDD variables for each BDD variable.]
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.]
511 SeeAlso [Cudd_bddNewVar Cudd_bddIthVar Cudd_bddNewVarAtLevel]
513 ******************************************************************************/
515 Cudd_zddVarsFromBddVars(
516 DdManager
* dd
/* DD manager */,
517 int multiplicity
/* how many ZDD variables are created for each BDD variable */)
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);
530 /* Impose the order of the BDD variables to the ZDD variables. */
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
;
540 for (i
= 0; i
< dd
->sizeZ
; i
++) {
541 dd
->univ
[i
]->index
= dd
->invpermZ
[i
];
544 permutation
= ALLOC(int,dd
->sizeZ
);
545 if (permutation
== NULL
) {
546 dd
->errorCode
= CUDD_MEMORY_OUT
;
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
;
555 for (i
= dd
->size
* multiplicity
; i
< dd
->sizeZ
; i
++) {
558 res
= Cudd_zddShuffleHeap(dd
, permutation
);
560 if (res
== 0) return(0);
562 /* Copy and expand the variable group tree if it exists. */
563 if (dd
->treeZ
!= NULL
) {
564 Cudd_FreeZddTree(dd
);
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];
574 /* Create groups for the ZDD variables derived from the same BDD variable.
576 if (multiplicity
> 1) {
579 vmask
= ALLOC(char, dd
->size
);
581 dd
->errorCode
= CUDD_MEMORY_OUT
;
584 lmask
= ALLOC(char, dd
->size
);
586 dd
->errorCode
= CUDD_MEMORY_OUT
;
589 for (i
= 0; i
< dd
->size
; i
++) {
590 vmask
[i
] = lmask
[i
] = 0;
592 res
= addMultiplicityGroups(dd
,dd
->treeZ
,multiplicity
,vmask
,lmask
);
595 if (res
== 0) return(0);
599 } /* end of Cudd_zddVarsFromBddVars */
602 /**Function********************************************************************
604 Synopsis [Returns the ADD for constant c.]
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.]
612 SeeAlso [Cudd_addNewVar Cudd_addIthVar]
614 ******************************************************************************/
620 return(cuddUniqueConst(dd
,c
));
622 } /* end of Cudd_addConst */
625 /**Function********************************************************************
627 Synopsis [Returns 1 if a DD node is not constant.]
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.]
636 SeeAlso [Cudd_IsConstant Cudd_bddIteConstant Cudd_addIteConstant
639 ******************************************************************************/
644 return(f
== DD_NON_CONSTANT
|| !Cudd_IsConstant(f
));
646 } /* end of Cudd_IsNonConstant */
649 /**Function********************************************************************
651 Synopsis [Enables automatic dynamic reordering of BDDs and ADDs.]
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
660 SeeAlso [Cudd_AutodynDisable Cudd_ReorderingStatus
661 Cudd_AutodynEnableZdd]
663 ******************************************************************************/
667 Cudd_ReorderingType method
)
670 if (method
!= CUDD_REORDER_SAME
) {
671 unique
->autoMethod
= method
;
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.
677 cuddClearDeathRow(unique
);
678 unique
->deathRowDepth
= 1;
679 unique
->deadMask
= unique
->deathRowDepth
- 1;
680 if ((unsigned) unique
->nextDead
> unique
->deadMask
) {
681 unique
->nextDead
= 0;
683 unique
->deathRow
= REALLOC(DdNodePtr
, unique
->deathRow
,
684 unique
->deathRowDepth
);
688 } /* end of Cudd_AutodynEnable */
691 /**Function********************************************************************
693 Synopsis [Disables automatic dynamic reordering.]
699 SeeAlso [Cudd_AutodynEnable Cudd_ReorderingStatus
700 Cudd_AutodynDisableZdd]
702 ******************************************************************************/
710 } /* end of Cudd_AutodynDisable */
713 /**Function********************************************************************
715 Synopsis [Reports the status of automatic dynamic reordering of BDDs
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
723 SideEffects [Parameter method is set to the reordering method currently
726 SeeAlso [Cudd_AutodynEnable Cudd_AutodynDisable
727 Cudd_ReorderingStatusZdd]
729 ******************************************************************************/
731 Cudd_ReorderingStatus(
733 Cudd_ReorderingType
* method
)
735 *method
= unique
->autoMethod
;
736 return(unique
->autoDyn
);
738 } /* end of Cudd_ReorderingStatus */
741 /**Function********************************************************************
743 Synopsis [Enables automatic dynamic reordering of ZDDs.]
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.]
751 SeeAlso [Cudd_AutodynDisableZdd Cudd_ReorderingStatusZdd
754 ******************************************************************************/
756 Cudd_AutodynEnableZdd(
758 Cudd_ReorderingType method
)
760 unique
->autoDynZ
= 1;
761 if (method
!= CUDD_REORDER_SAME
) {
762 unique
->autoMethodZ
= method
;
766 } /* end of Cudd_AutodynEnableZdd */
769 /**Function********************************************************************
771 Synopsis [Disables automatic dynamic reordering of ZDDs.]
777 SeeAlso [Cudd_AutodynEnableZdd Cudd_ReorderingStatusZdd
780 ******************************************************************************/
782 Cudd_AutodynDisableZdd(
785 unique
->autoDynZ
= 0;
788 } /* end of Cudd_AutodynDisableZdd */
791 /**Function********************************************************************
793 Synopsis [Reports the status of automatic dynamic reordering of ZDDs.]
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
800 SideEffects [Parameter method is set to the ZDD reordering method currently
803 SeeAlso [Cudd_AutodynEnableZdd Cudd_AutodynDisableZdd
804 Cudd_ReorderingStatus]
806 ******************************************************************************/
808 Cudd_ReorderingStatusZdd(
810 Cudd_ReorderingType
* method
)
812 *method
= unique
->autoMethodZ
;
813 return(unique
->autoDynZ
);
815 } /* end of Cudd_ReorderingStatusZdd */
818 /**Function********************************************************************
820 Synopsis [Tells whether the realignment of ZDD order to BDD order is
823 Description [Returns 1 if the realignment of ZDD order to BDD order is
824 enabled; 0 otherwise.]
828 SeeAlso [Cudd_zddRealignEnable Cudd_zddRealignDisable
829 Cudd_bddRealignEnable Cudd_bddRealignDisable]
831 ******************************************************************************/
833 Cudd_zddRealignmentEnabled(
836 return(unique
->realign
);
838 } /* end of Cudd_zddRealignmentEnabled */
841 /**Function********************************************************************
843 Synopsis [Enables realignment of ZDD order to BDD order.]
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.]
857 SeeAlso [Cudd_ReduceHeap Cudd_zddRealignDisable
858 Cudd_zddRealignmentEnabled Cudd_bddRealignDisable
859 Cudd_bddRealignmentEnabled]
861 ******************************************************************************/
863 Cudd_zddRealignEnable(
869 } /* end of Cudd_zddRealignEnable */
872 /**Function********************************************************************
874 Synopsis [Disables realignment of ZDD order to BDD order.]
880 SeeAlso [Cudd_zddRealignEnable Cudd_zddRealignmentEnabled
881 Cudd_bddRealignEnable Cudd_bddRealignmentEnabled]
883 ******************************************************************************/
885 Cudd_zddRealignDisable(
891 } /* end of Cudd_zddRealignDisable */
894 /**Function********************************************************************
896 Synopsis [Tells whether the realignment of BDD order to ZDD order is
899 Description [Returns 1 if the realignment of BDD order to ZDD order is
900 enabled; 0 otherwise.]
904 SeeAlso [Cudd_bddRealignEnable Cudd_bddRealignDisable
905 Cudd_zddRealignEnable Cudd_zddRealignDisable]
907 ******************************************************************************/
909 Cudd_bddRealignmentEnabled(
912 return(unique
->realignZ
);
914 } /* end of Cudd_bddRealignmentEnabled */
917 /**Function********************************************************************
919 Synopsis [Enables realignment of BDD order to ZDD order.]
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.]
933 SeeAlso [Cudd_zddReduceHeap Cudd_bddRealignDisable
934 Cudd_bddRealignmentEnabled Cudd_zddRealignDisable
935 Cudd_zddRealignmentEnabled]
937 ******************************************************************************/
939 Cudd_bddRealignEnable(
942 unique
->realignZ
= 1;
945 } /* end of Cudd_bddRealignEnable */
948 /**Function********************************************************************
950 Synopsis [Disables realignment of ZDD order to BDD order.]
956 SeeAlso [Cudd_bddRealignEnable Cudd_bddRealignmentEnabled
957 Cudd_zddRealignEnable Cudd_zddRealignmentEnabled]
959 ******************************************************************************/
961 Cudd_bddRealignDisable(
964 unique
->realignZ
= 0;
967 } /* end of Cudd_bddRealignDisable */
970 /**Function********************************************************************
972 Synopsis [Returns the one constant of the manager.]
974 Description [Returns the one constant of the manager. The one
975 constant is common to ADDs and BDDs.]
979 SeeAlso [Cudd_ReadZero Cudd_ReadLogicZero Cudd_ReadZddOne]
981 ******************************************************************************/
988 } /* end of Cudd_ReadOne */
991 /**Function********************************************************************
993 Synopsis [Returns the ZDD for the constant 1 function.]
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>.]
1002 SeeAlso [Cudd_ReadOne]
1004 ******************************************************************************/
1012 return(i
< dd
->sizeZ
? dd
->univ
[i
] : DD_ONE(dd
));
1014 } /* end of Cudd_ReadZddOne */
1018 /**Function********************************************************************
1020 Synopsis [Returns the zero constant of the manager.]
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.]
1028 SeeAlso [Cudd_ReadOne Cudd_ReadLogicZero]
1030 ******************************************************************************/
1035 return(DD_ZERO(dd
));
1037 } /* end of Cudd_ReadZero */
1040 /**Function********************************************************************
1042 Synopsis [Returns the logic zero constant of the manager.]
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.]
1050 SeeAlso [Cudd_ReadOne Cudd_ReadZero]
1052 ******************************************************************************/
1057 return(Cudd_Not(DD_ONE(dd
)));
1059 } /* end of Cudd_ReadLogicZero */
1062 /**Function********************************************************************
1064 Synopsis [Reads the plus-infinity constant from the manager.]
1070 ******************************************************************************/
1072 Cudd_ReadPlusInfinity(
1075 return(dd
->plusinfinity
);
1077 } /* end of Cudd_ReadPlusInfinity */
1080 /**Function********************************************************************
1082 Synopsis [Reads the minus-infinity constant from the manager.]
1088 ******************************************************************************/
1090 Cudd_ReadMinusInfinity(
1093 return(dd
->minusinfinity
);
1095 } /* end of Cudd_ReadMinusInfinity */
1098 /**Function********************************************************************
1100 Synopsis [Reads the background constant of the manager.]
1106 ******************************************************************************/
1108 Cudd_ReadBackground(
1111 return(dd
->background
);
1113 } /* end of Cudd_ReadBackground */
1116 /**Function********************************************************************
1118 Synopsis [Sets the background constant of the manager.]
1120 Description [Sets the background constant of the manager. It assumes
1121 that the DdNode pointer bck is already referenced.]
1125 ******************************************************************************/
1131 dd
->background
= bck
;
1133 } /* end of Cudd_SetBackground */
1136 /**Function********************************************************************
1138 Synopsis [Reads the number of slots in the cache.]
1144 SeeAlso [Cudd_ReadCacheUsedSlots]
1146 ******************************************************************************/
1148 Cudd_ReadCacheSlots(
1151 return(dd
->cacheSlots
);
1153 } /* end of Cudd_ReadCacheSlots */
1156 /**Function********************************************************************
1158 Synopsis [Reads the fraction of used slots in the cache.]
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
1167 SeeAlso [Cudd_ReadCacheSlots]
1169 ******************************************************************************/
1171 Cudd_ReadCacheUsedSlots(
1174 unsigned long used
= 0;
1175 int slots
= dd
->cacheSlots
;
1176 DdCache
*cache
= dd
->cache
;
1179 for (i
= 0; i
< slots
; i
++) {
1180 used
+= cache
[i
].h
!= 0;
1183 return((double)used
/ (double) dd
->cacheSlots
);
1185 } /* end of Cudd_ReadCacheUsedSlots */
1188 /**Function********************************************************************
1190 Synopsis [Returns the number of cache look-ups.]
1192 Description [Returns the number of cache look-ups.]
1196 SeeAlso [Cudd_ReadCacheHits]
1198 ******************************************************************************/
1200 Cudd_ReadCacheLookUps(
1203 return(dd
->cacheHits
+ dd
->cacheMisses
+
1204 dd
->totCachehits
+ dd
->totCacheMisses
);
1206 } /* end of Cudd_ReadCacheLookUps */
1209 /**Function********************************************************************
1211 Synopsis [Returns the number of cache hits.]
1217 SeeAlso [Cudd_ReadCacheLookUps]
1219 ******************************************************************************/
1224 return(dd
->cacheHits
+ dd
->totCachehits
);
1226 } /* end of Cudd_ReadCacheHits */
1229 /**Function********************************************************************
1231 Synopsis [Returns the number of recursive calls.]
1233 Description [Returns the number of recursive calls if the package is
1234 compiled with DD_COUNT defined.]
1240 ******************************************************************************/
1242 Cudd_ReadRecursiveCalls(
1246 return(dd
->recursiveCalls
);
1251 } /* end of Cudd_ReadRecursiveCalls */
1255 /**Function********************************************************************
1257 Synopsis [Reads the hit rate that causes resizinig of the computed
1264 SeeAlso [Cudd_SetMinHit]
1266 ******************************************************************************/
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
)));
1275 } /* end of Cudd_ReadMinHit */
1278 /**Function********************************************************************
1280 Synopsis [Sets the hit rate that causes resizinig of the computed
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.]
1290 SeeAlso [Cudd_ReadMinHit]
1292 ******************************************************************************/
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
);
1302 } /* end of Cudd_SetMinHit */
1305 /**Function********************************************************************
1307 Synopsis [Reads the looseUpTo parameter of the manager.]
1313 SeeAlso [Cudd_SetLooseUpTo Cudd_ReadMinHit Cudd_ReadMinDead]
1315 ******************************************************************************/
1320 return(dd
->looseUpTo
);
1322 } /* end of Cudd_ReadLooseUpTo */
1325 /**Function********************************************************************
1327 Synopsis [Sets the looseUpTo parameter of the manager.]
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.]
1337 SeeAlso [Cudd_ReadLooseUpTo Cudd_SetMinHit]
1339 ******************************************************************************/
1346 unsigned long datalimit
= getSoftDataLimit();
1347 lut
= (unsigned int) (datalimit
/ (sizeof(DdNode
) *
1348 DD_MAX_LOOSE_FRACTION
));
1350 dd
->looseUpTo
= lut
;
1352 } /* end of Cudd_SetLooseUpTo */
1355 /**Function********************************************************************
1357 Synopsis [Returns the soft limit for the cache size.]
1359 Description [Returns the soft limit for the cache size. The soft limit]
1363 SeeAlso [Cudd_ReadMaxCache]
1365 ******************************************************************************/
1370 return(2 * dd
->cacheSlots
+ dd
->cacheSlack
);
1372 } /* end of Cudd_ReadMaxCache */
1375 /**Function********************************************************************
1377 Synopsis [Reads the maxCacheHard parameter of the manager.]
1383 SeeAlso [Cudd_SetMaxCacheHard Cudd_ReadMaxCache]
1385 ******************************************************************************/
1387 Cudd_ReadMaxCacheHard(
1390 return(dd
->maxCacheHard
);
1392 } /* end of Cudd_ReadMaxCache */
1395 /**Function********************************************************************
1397 Synopsis [Sets the maxCacheHard parameter of the manager.]
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.]
1407 SeeAlso [Cudd_ReadMaxCacheHard Cudd_SetMaxCache]
1409 ******************************************************************************/
1411 Cudd_SetMaxCacheHard(
1416 unsigned long datalimit
= getSoftDataLimit();
1417 mc
= (unsigned int) (datalimit
/ (sizeof(DdCache
) *
1418 DD_MAX_CACHE_FRACTION
));
1420 dd
->maxCacheHard
= mc
;
1422 } /* end of Cudd_SetMaxCacheHard */
1425 /**Function********************************************************************
1427 Synopsis [Returns the number of BDD variables in existance.]
1433 SeeAlso [Cudd_ReadZddSize]
1435 ******************************************************************************/
1442 } /* end of Cudd_ReadSize */
1445 /**Function********************************************************************
1447 Synopsis [Returns the number of ZDD variables in existance.]
1453 SeeAlso [Cudd_ReadSize]
1455 ******************************************************************************/
1462 } /* end of Cudd_ReadZddSize */
1465 /**Function********************************************************************
1467 Synopsis [Returns the total number of slots of the unique table.]
1469 Description [Returns the total number of slots of the unique table.
1470 This number ismainly for diagnostic purposes.]
1474 ******************************************************************************/
1481 } /* end of Cudd_ReadSlots */
1484 /**Function********************************************************************
1486 Synopsis [Reads the fraction of used slots in the unique table.]
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.]
1495 SeeAlso [Cudd_ReadSlots]
1497 ******************************************************************************/
1502 unsigned long used
= 0;
1504 int size
= dd
->size
;
1505 DdNodePtr
*nodelist
;
1506 DdSubtable
*subtable
;
1508 DdNode
*sentinel
= &(dd
->sentinel
);
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
++) {
1516 if (node
!= sentinel
) {
1522 /* Scan the ZDD subtables. */
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
++) {
1536 /* Constant table. */
1537 subtable
= &(dd
->constants
);
1538 nodelist
= subtable
->nodelist
;
1539 for (j
= 0; (unsigned) j
< subtable
->slots
; j
++) {
1546 return((double)used
/ (double) dd
->slots
);
1548 } /* end of Cudd_ReadUsedSlots */
1551 /**Function********************************************************************
1553 Synopsis [Computes the expected fraction of used slots in the unique
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.]
1564 SeeAlso [Cudd_ReadSlots Cudd_ReadUsedSlots]
1566 ******************************************************************************/
1568 Cudd_ExpectedUsedSlots(
1572 int size
= dd
->size
;
1573 DdSubtable
*subtable
;
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
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
);
1590 /* Scan the ZDD subtables. */
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
);
1599 /* Constant table. */
1600 subtable
= &(dd
->constants
);
1601 empty
+= (double) subtable
->slots
*
1602 exp(-(double) subtable
->keys
/ (double) subtable
->slots
);
1604 return(1.0 - empty
/ (double) dd
->slots
);
1606 } /* end of Cudd_ExpectedUsedSlots */
1609 /**Function********************************************************************
1611 Synopsis [Returns the number of nodes in the unique table.]
1613 Description [Returns the total number of nodes currently in the unique
1614 table, including the dead nodes.]
1618 SeeAlso [Cudd_ReadDead]
1620 ******************************************************************************/
1627 } /* end of Cudd_ReadKeys */
1630 /**Function********************************************************************
1632 Synopsis [Returns the number of dead nodes in the unique table.]
1638 SeeAlso [Cudd_ReadKeys]
1640 ******************************************************************************/
1647 } /* end of Cudd_ReadDead */
1650 /**Function********************************************************************
1652 Synopsis [Reads the minDead parameter of the manager.]
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.]
1662 SeeAlso [Cudd_ReadDead Cudd_ReadLooseUpTo Cudd_SetLooseUpTo]
1664 ******************************************************************************/
1669 return(dd
->minDead
);
1671 } /* end of Cudd_ReadMinDead */
1674 /**Function********************************************************************
1676 Synopsis [Returns the number of times reordering has occurred.]
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.]
1688 SeeAlso [Cudd_ReduceHeap Cudd_ReadReorderingTime]
1690 ******************************************************************************/
1692 Cudd_ReadReorderings(
1695 return(dd
->reorderings
);
1697 } /* end of Cudd_ReadReorderings */
1700 /**Function********************************************************************
1702 Synopsis [Returns the time spent in reordering.]
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.]
1710 SeeAlso [Cudd_ReadReorderings]
1712 ******************************************************************************/
1714 Cudd_ReadReorderingTime(
1717 return(dd
->reordTime
);
1719 } /* end of Cudd_ReadReorderingTime */
1722 /**Function********************************************************************
1724 Synopsis [Returns the number of times garbage collection has occurred.]
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
1733 SeeAlso [Cudd_ReadGarbageCollectionTime]
1735 ******************************************************************************/
1737 Cudd_ReadGarbageCollections(
1740 return(dd
->garbageCollections
);
1742 } /* end of Cudd_ReadGarbageCollections */
1745 /**Function********************************************************************
1747 Synopsis [Returns the time spent in garbage collection.]
1749 Description [Returns the number of milliseconds spent doing garbage
1750 collection since the manager was initialized.]
1754 SeeAlso [Cudd_ReadGarbageCollections]
1756 ******************************************************************************/
1758 Cudd_ReadGarbageCollectionTime(
1763 } /* end of Cudd_ReadGarbageCollectionTime */
1766 /**Function********************************************************************
1768 Synopsis [Returns the number of nodes freed.]
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.]
1776 SeeAlso [Cudd_ReadNodesDropped]
1778 ******************************************************************************/
1780 Cudd_ReadNodesFreed(
1784 return(dd
->nodesFreed
);
1789 } /* end of Cudd_ReadNodesFreed */
1792 /**Function********************************************************************
1794 Synopsis [Returns the number of nodes dropped.]
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.]
1802 SeeAlso [Cudd_ReadNodesFreed]
1804 ******************************************************************************/
1806 Cudd_ReadNodesDropped(
1810 return(dd
->nodesDropped
);
1815 } /* end of Cudd_ReadNodesDropped */
1818 /**Function********************************************************************
1820 Synopsis [Returns the number of look-ups in the unique table.]
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.]
1828 SeeAlso [Cudd_ReadUniqueLinks]
1830 ******************************************************************************/
1832 Cudd_ReadUniqueLookUps(
1835 #ifdef DD_UNIQUE_PROFILE
1836 return(dd
->uniqueLookUps
);
1841 } /* end of Cudd_ReadUniqueLookUps */
1844 /**Function********************************************************************
1846 Synopsis [Returns the number of links followed in the unique table.]
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.]
1857 SeeAlso [Cudd_ReadUniqueLookUps]
1859 ******************************************************************************/
1861 Cudd_ReadUniqueLinks(
1864 #ifdef DD_UNIQUE_PROFILE
1865 return(dd
->uniqueLinks
);
1870 } /* end of Cudd_ReadUniqueLinks */
1873 /**Function********************************************************************
1875 Synopsis [Reads the siftMaxVar parameter of the manager.]
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.]
1883 SeeAlso [Cudd_ReadSiftMaxSwap Cudd_SetSiftMaxVar]
1885 ******************************************************************************/
1887 Cudd_ReadSiftMaxVar(
1890 return(dd
->siftMaxVar
);
1892 } /* end of Cudd_ReadSiftMaxVar */
1895 /**Function********************************************************************
1897 Synopsis [Sets the siftMaxVar parameter of the manager.]
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.]
1905 SeeAlso [Cudd_SetSiftMaxSwap Cudd_ReadSiftMaxVar]
1907 ******************************************************************************/
1913 dd
->siftMaxVar
= smv
;
1915 } /* end of Cudd_SetSiftMaxVar */
1918 /**Function********************************************************************
1920 Synopsis [Reads the siftMaxSwap parameter of the manager.]
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.]
1930 SeeAlso [Cudd_ReadSiftMaxVar Cudd_SetSiftMaxSwap]
1932 ******************************************************************************/
1934 Cudd_ReadSiftMaxSwap(
1937 return(dd
->siftMaxSwap
);
1939 } /* end of Cudd_ReadSiftMaxSwap */
1942 /**Function********************************************************************
1944 Synopsis [Sets the siftMaxSwap parameter of the manager.]
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.]
1954 SeeAlso [Cudd_SetSiftMaxVar Cudd_ReadSiftMaxSwap]
1956 ******************************************************************************/
1958 Cudd_SetSiftMaxSwap(
1962 dd
->siftMaxSwap
= sms
;
1964 } /* end of Cudd_SetSiftMaxSwap */
1967 /**Function********************************************************************
1969 Synopsis [Reads the maxGrowth parameter of the manager.]
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.]
1980 SeeAlso [Cudd_SetMaxGrowth Cudd_ReadMaxGrowthAlternate]
1982 ******************************************************************************/
1987 return(dd
->maxGrowth
);
1989 } /* end of Cudd_ReadMaxGrowth */
1992 /**Function********************************************************************
1994 Synopsis [Sets the maxGrowth parameter of the manager.]
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.]
2005 SeeAlso [Cudd_ReadMaxGrowth Cudd_SetMaxGrowthAlternate]
2007 ******************************************************************************/
2015 } /* end of Cudd_SetMaxGrowth */
2018 /**Function********************************************************************
2020 Synopsis [Reads the maxGrowthAlt parameter of the manager.]
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.]
2030 SeeAlso [Cudd_ReadMaxGrowth Cudd_SetMaxGrowthAlternate
2031 Cudd_SetReorderingCycle Cudd_ReadReorderingCycle]
2033 ******************************************************************************/
2035 Cudd_ReadMaxGrowthAlternate(
2038 return(dd
->maxGrowthAlt
);
2040 } /* end of Cudd_ReadMaxGrowthAlternate */
2043 /**Function********************************************************************
2045 Synopsis [Sets the maxGrowthAlt parameter of the manager.]
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.]
2055 SeeAlso [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowth
2056 Cudd_SetReorderingCycle Cudd_ReadReorderingCycle]
2058 ******************************************************************************/
2060 Cudd_SetMaxGrowthAlternate(
2064 dd
->maxGrowthAlt
= mg
;
2066 } /* end of Cudd_SetMaxGrowthAlternate */
2069 /**Function********************************************************************
2071 Synopsis [Reads the reordCycle parameter of the manager.]
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.]
2079 SeeAlso [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowthAlternate
2080 Cudd_SetReorderingCycle]
2082 ******************************************************************************/
2084 Cudd_ReadReorderingCycle(
2087 return(dd
->reordCycle
);
2089 } /* end of Cudd_ReadReorderingCycle */
2092 /**Function********************************************************************
2094 Synopsis [Sets the reordCycle parameter of the manager.]
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.]
2102 SeeAlso [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowthAlternate
2103 Cudd_ReadReorderingCycle]
2105 ******************************************************************************/
2107 Cudd_SetReorderingCycle(
2111 dd
->reordCycle
= cycle
;
2113 } /* end of Cudd_SetReorderingCycle */
2116 /**Function********************************************************************
2118 Synopsis [Returns the variable group tree of the manager.]
2124 SeeAlso [Cudd_SetTree Cudd_FreeTree Cudd_ReadZddTree]
2126 ******************************************************************************/
2133 } /* end of Cudd_ReadTree */
2136 /**Function********************************************************************
2138 Synopsis [Sets the variable group tree of the manager.]
2144 SeeAlso [Cudd_FreeTree Cudd_ReadTree Cudd_SetZddTree]
2146 ******************************************************************************/
2152 if (dd
->tree
!= NULL
) {
2153 Mtr_FreeTree(dd
->tree
);
2156 if (tree
== NULL
) return;
2158 fixVarTree(tree
, dd
->perm
, dd
->size
);
2161 } /* end of Cudd_SetTree */
2164 /**Function********************************************************************
2166 Synopsis [Frees the variable group tree of the manager.]
2172 SeeAlso [Cudd_SetTree Cudd_ReadTree Cudd_FreeZddTree]
2174 ******************************************************************************/
2179 if (dd
->tree
!= NULL
) {
2180 Mtr_FreeTree(dd
->tree
);
2185 } /* end of Cudd_FreeTree */
2188 /**Function********************************************************************
2190 Synopsis [Returns the variable group tree of the manager.]
2196 SeeAlso [Cudd_SetZddTree Cudd_FreeZddTree Cudd_ReadTree]
2198 ******************************************************************************/
2205 } /* end of Cudd_ReadZddTree */
2208 /**Function********************************************************************
2210 Synopsis [Sets the ZDD variable group tree of the manager.]
2216 SeeAlso [Cudd_FreeZddTree Cudd_ReadZddTree Cudd_SetTree]
2218 ******************************************************************************/
2224 if (dd
->treeZ
!= NULL
) {
2225 Mtr_FreeTree(dd
->treeZ
);
2228 if (tree
== NULL
) return;
2230 fixVarTree(tree
, dd
->permZ
, dd
->sizeZ
);
2233 } /* end of Cudd_SetZddTree */
2236 /**Function********************************************************************
2238 Synopsis [Frees the variable group tree of the manager.]
2244 SeeAlso [Cudd_SetZddTree Cudd_ReadZddTree Cudd_FreeTree]
2246 ******************************************************************************/
2251 if (dd
->treeZ
!= NULL
) {
2252 Mtr_FreeTree(dd
->treeZ
);
2257 } /* end of Cudd_FreeZddTree */
2260 /**Function********************************************************************
2262 Synopsis [Returns the index of the node.]
2264 Description [Returns the index of the node. The node pointer can be
2265 either regular or complemented.]
2269 SeeAlso [Cudd_ReadIndex]
2271 ******************************************************************************/
2276 return((unsigned int) Cudd_Regular(node
)->index
);
2278 } /* end of Cudd_NodeReadIndex */
2281 /**Function********************************************************************
2283 Synopsis [Returns the current position of the i-th variable in the
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
2293 SeeAlso [Cudd_ReadInvPerm Cudd_ReadPermZdd]
2295 ******************************************************************************/
2301 if (i
== CUDD_CONST_INDEX
) return(CUDD_CONST_INDEX
);
2302 if (i
< 0 || i
>= dd
->size
) return(-1);
2303 return(dd
->perm
[i
]);
2305 } /* end of Cudd_ReadPerm */
2308 /**Function********************************************************************
2310 Synopsis [Returns the current position of the i-th ZDD variable in the
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
2320 SeeAlso [Cudd_ReadInvPermZdd Cudd_ReadPerm]
2322 ******************************************************************************/
2328 if (i
== CUDD_CONST_INDEX
) return(CUDD_CONST_INDEX
);
2329 if (i
< 0 || i
>= dd
->sizeZ
) return(-1);
2330 return(dd
->permZ
[i
]);
2332 } /* end of Cudd_ReadPermZdd */
2335 /**Function********************************************************************
2337 Synopsis [Returns the index of the variable currently in the i-th
2338 position of the order.]
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.]
2346 SeeAlso [Cudd_ReadPerm Cudd_ReadInvPermZdd]
2348 ******************************************************************************/
2354 if (i
== CUDD_CONST_INDEX
) return(CUDD_CONST_INDEX
);
2355 if (i
< 0 || i
>= dd
->size
) return(-1);
2356 return(dd
->invperm
[i
]);
2358 } /* end of Cudd_ReadInvPerm */
2361 /**Function********************************************************************
2363 Synopsis [Returns the index of the ZDD variable currently in the i-th
2364 position of the order.]
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.]
2372 SeeAlso [Cudd_ReadPerm Cudd_ReadInvPermZdd]
2374 ******************************************************************************/
2376 Cudd_ReadInvPermZdd(
2380 if (i
== CUDD_CONST_INDEX
) return(CUDD_CONST_INDEX
);
2381 if (i
< 0 || i
>= dd
->sizeZ
) return(-1);
2382 return(dd
->invpermZ
[i
]);
2384 } /* end of Cudd_ReadInvPermZdd */
2387 /**Function********************************************************************
2389 Synopsis [Returns the i-th element of the vars array.]
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.]
2399 SeeAlso [Cudd_bddIthVar]
2401 ******************************************************************************/
2407 if (i
< 0 || i
> dd
->size
) return(NULL
);
2408 return(dd
->vars
[i
]);
2410 } /* end of Cudd_ReadVars */
2413 /**Function********************************************************************
2415 Synopsis [Reads the epsilon parameter of the manager.]
2417 Description [Reads the epsilon parameter of the manager. The epsilon
2418 parameter control the comparison between floating point numbers.]
2422 SeeAlso [Cudd_SetEpsilon]
2424 ******************************************************************************/
2429 return(dd
->epsilon
);
2431 } /* end of Cudd_ReadEpsilon */
2434 /**Function********************************************************************
2436 Synopsis [Sets the epsilon parameter of the manager to ep.]
2438 Description [Sets the epsilon parameter of the manager to ep. The epsilon
2439 parameter control the comparison between floating point numbers.]
2443 SeeAlso [Cudd_ReadEpsilon]
2445 ******************************************************************************/
2453 } /* end of Cudd_SetEpsilon */
2456 /**Function********************************************************************
2458 Synopsis [Reads the groupcheck parameter of the manager.]
2460 Description [Reads the groupcheck parameter of the manager. The
2461 groupcheck parameter determines the aggregation criterion in group
2466 SeeAlso [Cudd_SetGroupcheck]
2468 ******************************************************************************/
2469 Cudd_AggregationType
2470 Cudd_ReadGroupcheck(
2473 return(dd
->groupcheck
);
2475 } /* end of Cudd_ReadGroupCheck */
2478 /**Function********************************************************************
2480 Synopsis [Sets the parameter groupcheck of the manager to gc.]
2482 Description [Sets the parameter groupcheck of the manager to gc. The
2483 groupcheck parameter determines the aggregation criterion in group
2488 SeeAlso [Cudd_ReadGroupCheck]
2490 ******************************************************************************/
2494 Cudd_AggregationType gc
)
2496 dd
->groupcheck
= gc
;
2498 } /* end of Cudd_SetGroupcheck */
2501 /**Function********************************************************************
2503 Synopsis [Tells whether garbage collection is enabled.]
2505 Description [Returns 1 if garbage collection is enabled; 0 otherwise.]
2509 SeeAlso [Cudd_EnableGarbageCollection Cudd_DisableGarbageCollection]
2511 ******************************************************************************/
2513 Cudd_GarbageCollectionEnabled(
2516 return(dd
->gcEnabled
);
2518 } /* end of Cudd_GarbageCollectionEnabled */
2521 /**Function********************************************************************
2523 Synopsis [Enables garbage collection.]
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.]
2531 SeeAlso [Cudd_DisableGarbageCollection Cudd_GarbageCollectionEnabled]
2533 ******************************************************************************/
2535 Cudd_EnableGarbageCollection(
2540 } /* end of Cudd_EnableGarbageCollection */
2543 /**Function********************************************************************
2545 Synopsis [Disables garbage collection.]
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.)]
2555 SeeAlso [Cudd_EnableGarbageCollection Cudd_GarbageCollectionEnabled]
2557 ******************************************************************************/
2559 Cudd_DisableGarbageCollection(
2564 } /* end of Cudd_DisableGarbageCollection */
2567 /**Function********************************************************************
2569 Synopsis [Tells whether dead nodes are counted towards triggering
2572 Description [Tells whether dead nodes are counted towards triggering
2573 reordering. Returns 1 if dead nodes are counted; 0 otherwise.]
2577 SeeAlso [Cudd_TurnOnCountDead Cudd_TurnOffCountDead]
2579 ******************************************************************************/
2581 Cudd_DeadAreCounted(
2584 return(dd
->countDead
== 0 ? 1 : 0);
2586 } /* end of Cudd_DeadAreCounted */
2589 /**Function********************************************************************
2591 Synopsis [Causes the dead nodes to be counted towards triggering
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.]
2598 SideEffects [Changes the manager.]
2600 SeeAlso [Cudd_TurnOffCountDead Cudd_DeadAreCounted]
2602 ******************************************************************************/
2604 Cudd_TurnOnCountDead(
2609 } /* end of Cudd_TurnOnCountDead */
2612 /**Function********************************************************************
2614 Synopsis [Causes the dead nodes not to be counted towards triggering
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
2623 SideEffects [Changes the manager.]
2625 SeeAlso [Cudd_TurnOnCountDead Cudd_DeadAreCounted]
2627 ******************************************************************************/
2629 Cudd_TurnOffCountDead(
2634 } /* end of Cudd_TurnOffCountDead */
2637 /**Function********************************************************************
2639 Synopsis [Returns the current value of the recombination parameter used
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.]
2649 SeeAlso [Cudd_SetRecomb]
2651 ******************************************************************************/
2658 } /* end of Cudd_ReadRecomb */
2661 /**Function********************************************************************
2663 Synopsis [Sets the value of the recombination parameter used in group
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
2672 SideEffects [Changes the manager.]
2674 SeeAlso [Cudd_ReadRecomb]
2676 ******************************************************************************/
2682 dd
->recomb
= recomb
;
2684 } /* end of Cudd_SetRecomb */
2687 /**Function********************************************************************
2689 Synopsis [Returns the current value of the symmviolation parameter used
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
2702 SeeAlso [Cudd_SetSymmviolation]
2704 ******************************************************************************/
2706 Cudd_ReadSymmviolation(
2709 return(dd
->symmviolation
);
2711 } /* end of Cudd_ReadSymmviolation */
2714 /**Function********************************************************************
2716 Synopsis [Sets the value of the symmviolation parameter used
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
2727 SideEffects [Changes the manager.]
2729 SeeAlso [Cudd_ReadSymmviolation]
2731 ******************************************************************************/
2733 Cudd_SetSymmviolation(
2737 dd
->symmviolation
= symmviolation
;
2739 } /* end of Cudd_SetSymmviolation */
2742 /**Function********************************************************************
2744 Synopsis [Returns the current value of the arcviolation parameter used
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.]
2756 SeeAlso [Cudd_SetArcviolation]
2758 ******************************************************************************/
2760 Cudd_ReadArcviolation(
2763 return(dd
->arcviolation
);
2765 } /* end of Cudd_ReadArcviolation */
2768 /**Function********************************************************************
2770 Synopsis [Sets the value of the arcviolation parameter used
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.]
2782 SeeAlso [Cudd_ReadArcviolation]
2784 ******************************************************************************/
2786 Cudd_SetArcviolation(
2790 dd
->arcviolation
= arcviolation
;
2792 } /* end of Cudd_SetArcviolation */
2795 /**Function********************************************************************
2797 Synopsis [Reads the current size of the population used by the
2798 genetic algorithm for reordering.]
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.]
2809 SeeAlso [Cudd_SetPopulationSize]
2811 ******************************************************************************/
2813 Cudd_ReadPopulationSize(
2816 return(dd
->populationSize
);
2818 } /* end of Cudd_ReadPopulationSize */
2821 /**Function********************************************************************
2823 Synopsis [Sets the size of the population used by the
2824 genetic algorithm for reordering.]
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.]
2833 SideEffects [Changes the manager.]
2835 SeeAlso [Cudd_ReadPopulationSize]
2837 ******************************************************************************/
2839 Cudd_SetPopulationSize(
2843 dd
->populationSize
= populationSize
;
2845 } /* end of Cudd_SetPopulationSize */
2848 /**Function********************************************************************
2850 Synopsis [Reads the current number of crossovers used by the
2851 genetic algorithm for reordering.]
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.]
2862 SeeAlso [Cudd_SetNumberXovers]
2864 ******************************************************************************/
2866 Cudd_ReadNumberXovers(
2869 return(dd
->numberXovers
);
2871 } /* end of Cudd_ReadNumberXovers */
2874 /**Function********************************************************************
2876 Synopsis [Sets the number of crossovers used by the
2877 genetic algorithm for reordering.]
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.]
2888 SeeAlso [Cudd_ReadNumberXovers]
2890 ******************************************************************************/
2892 Cudd_SetNumberXovers(
2896 dd
->numberXovers
= numberXovers
;
2898 } /* end of Cudd_SetNumberXovers */
2900 /**Function********************************************************************
2902 Synopsis [Returns the memory in use by the manager measured in bytes.]
2910 ******************************************************************************/
2912 Cudd_ReadMemoryInUse(
2915 return(dd
->memused
);
2917 } /* end of Cudd_ReadMemoryInUse */
2920 /**Function********************************************************************
2922 Synopsis [Prints out statistics and settings for a CUDD manager.]
2924 Description [Prints out statistics and settings for a CUDD manager.
2925 Returns 1 if successful; 0 otherwise.]
2931 ******************************************************************************/
2938 Cudd_ReorderingType autoMethod
, autoMethodZ
;
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",
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",
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);
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",
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);
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",
3068 if (retval
== EOF
) return(0);
3069 retval
= fprintf(fp
,"Total number of nodes reclaimed: %.0f\n",
3071 if (retval
== EOF
) return(0);
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);
3079 retval
= fprintf(fp
,"Number of recursive calls: %.0f\n",
3080 Cudd_ReadRecursiveCalls(dd
));
3081 if (retval
== EOF
) return(0);
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);
3095 retval
= fprintf(fp
,"Node swaps in reordering: %.0f\n",
3096 Cudd_ReadSwapSteps(dd
));
3097 if (retval
== EOF
) return(0);
3102 } /* end of Cudd_PrintInfo */
3105 /**Function********************************************************************
3107 Synopsis [Reports the peak number of nodes.]
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.]
3115 SeeAlso [Cudd_ReadNodeCount Cudd_PrintInfo]
3117 ******************************************************************************/
3119 Cudd_ReadPeakNodeCount(
3123 DdNodePtr
*scan
= dd
->memoryList
;
3125 while (scan
!= NULL
) {
3126 count
+= DD_MEM_CHUNK
;
3127 scan
= (DdNodePtr
*) *scan
;
3131 } /* end of Cudd_ReadPeakNodeCount */
3134 /**Function********************************************************************
3136 Synopsis [Reports the peak number of live nodes.]
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.]
3144 SeeAlso [Cudd_ReadNodeCount Cudd_PrintInfo Cudd_ReadPeakNodeCount]
3146 ******************************************************************************/
3148 Cudd_ReadPeakLiveNodeCount(
3151 unsigned int live
= dd
->keys
- dd
->dead
;
3153 if (live
> dd
->peakLiveNodes
) {
3154 dd
->peakLiveNodes
= live
;
3156 return((int)dd
->peakLiveNodes
);
3158 } /* end of Cudd_ReadPeakLiveNodeCount */
3161 /**Function********************************************************************
3163 Synopsis [Reports the number of nodes in BDDs and ADDs.]
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.]
3172 SeeAlso [Cudd_ReadPeakNodeCount Cudd_zddReadNodeCount]
3174 ******************************************************************************/
3182 #ifndef DD_NO_DEATH_ROW
3183 cuddClearDeathRow(dd
);
3186 count
= (long) (dd
->keys
- dd
->dead
);
3188 /* Count isolated projection functions. Their number is subtracted
3189 ** from the node count because they are not part of the BDDs.
3191 for (i
=0; i
< dd
->size
; i
++) {
3192 if (dd
->vars
[i
]->ref
== 1) count
--;
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
--;
3201 } /* end of Cudd_ReadNodeCount */
3205 /**Function********************************************************************
3207 Synopsis [Reports the number of nodes in ZDDs.]
3209 Description [Reports the number of nodes in ZDDs. This
3210 number always includes the two constants 1 and 0.]
3214 SeeAlso [Cudd_ReadPeakNodeCount Cudd_ReadNodeCount]
3216 ******************************************************************************/
3218 Cudd_zddReadNodeCount(
3221 return((long)(dd
->keysZ
- dd
->deadZ
+ 2));
3223 } /* end of Cudd_zddReadNodeCount */
3226 /**Function********************************************************************
3228 Synopsis [Adds a function to a hook.]
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.]
3237 SeeAlso [Cudd_RemoveHook]
3239 ******************************************************************************/
3244 Cudd_HookType where
)
3246 DdHook
**hook
, *nextHook
, *newHook
;
3249 case CUDD_PRE_GC_HOOK
:
3250 hook
= &(dd
->preGCHook
);
3252 case CUDD_POST_GC_HOOK
:
3253 hook
= &(dd
->postGCHook
);
3255 case CUDD_PRE_REORDERING_HOOK
:
3256 hook
= &(dd
->preReorderingHook
);
3258 case CUDD_POST_REORDERING_HOOK
:
3259 hook
= &(dd
->postReorderingHook
);
3264 /* Scan the list and find whether the function is already there.
3265 ** If so, just return. */
3267 while (nextHook
!= NULL
) {
3268 if (nextHook
->f
== f
) {
3271 hook
= &(nextHook
->next
);
3272 nextHook
= nextHook
->next
;
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
;
3281 newHook
->next
= NULL
;
3286 } /* end of Cudd_AddHook */
3289 /**Function********************************************************************
3291 Synopsis [Removes a function from a hook.]
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.]
3299 SeeAlso [Cudd_AddHook]
3301 ******************************************************************************/
3306 Cudd_HookType where
)
3308 DdHook
**hook
, *nextHook
;
3311 case CUDD_PRE_GC_HOOK
:
3312 hook
= &(dd
->preGCHook
);
3314 case CUDD_POST_GC_HOOK
:
3315 hook
= &(dd
->postGCHook
);
3317 case CUDD_PRE_REORDERING_HOOK
:
3318 hook
= &(dd
->preReorderingHook
);
3320 case CUDD_POST_REORDERING_HOOK
:
3321 hook
= &(dd
->postReorderingHook
);
3327 while (nextHook
!= NULL
) {
3328 if (nextHook
->f
== f
) {
3329 *hook
= nextHook
->next
;
3333 hook
= &(nextHook
->next
);
3334 nextHook
= nextHook
->next
;
3339 } /* end of Cudd_RemoveHook */
3342 /**Function********************************************************************
3344 Synopsis [Checks whether a function is in a hook.]
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.]
3352 SeeAlso [Cudd_AddHook Cudd_RemoveHook]
3354 ******************************************************************************/
3359 Cudd_HookType where
)
3364 case CUDD_PRE_GC_HOOK
:
3365 hook
= dd
->preGCHook
;
3367 case CUDD_POST_GC_HOOK
:
3368 hook
= dd
->postGCHook
;
3370 case CUDD_PRE_REORDERING_HOOK
:
3371 hook
= dd
->preReorderingHook
;
3373 case CUDD_POST_REORDERING_HOOK
:
3374 hook
= dd
->postReorderingHook
;
3379 /* Scan the list and find whether the function is already there. */
3380 while (hook
!= NULL
) {
3388 } /* end of Cudd_IsInHook */
3391 /**Function********************************************************************
3393 Synopsis [Sample hook function to call before reordering.]
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.]
3401 SeeAlso [Cudd_StdPostReordHook]
3403 ******************************************************************************/
3405 Cudd_StdPreReordHook(
3410 Cudd_ReorderingType method
= (Cudd_ReorderingType
) (ptruint
) data
;
3413 retval
= fprintf(dd
->out
,"%s reordering with ", str
);
3414 if (retval
== EOF
) return(0);
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);
3430 case CUDD_REORDER_RANDOM
:
3431 case CUDD_REORDER_RANDOM_PIVOT
:
3432 retval
= fprintf(dd
->out
,"random");
3434 case CUDD_REORDER_SIFT
:
3435 case CUDD_REORDER_SIFT_CONVERGE
:
3436 retval
= fprintf(dd
->out
,"sifting");
3438 case CUDD_REORDER_SYMM_SIFT
:
3439 case CUDD_REORDER_SYMM_SIFT_CONV
:
3440 retval
= fprintf(dd
->out
,"symmetric sifting");
3442 case CUDD_REORDER_LAZY_SIFT
:
3443 retval
= fprintf(dd
->out
,"lazy sifting");
3445 case CUDD_REORDER_GROUP_SIFT
:
3446 case CUDD_REORDER_GROUP_SIFT_CONV
:
3447 retval
= fprintf(dd
->out
,"group sifting");
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");
3457 case CUDD_REORDER_ANNEALING
:
3458 retval
= fprintf(dd
->out
,"annealing");
3460 case CUDD_REORDER_GENETIC
:
3461 retval
= fprintf(dd
->out
,"genetic");
3463 case CUDD_REORDER_LINEAR
:
3464 case CUDD_REORDER_LINEAR_CONVERGE
:
3465 retval
= fprintf(dd
->out
,"linear sifting");
3467 case CUDD_REORDER_EXACT
:
3468 retval
= fprintf(dd
->out
,"exact");
3473 if (retval
== EOF
) return(0);
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);
3481 } /* end of Cudd_StdPreReordHook */
3484 /**Function********************************************************************
3486 Synopsis [Sample hook function to call after reordering.]
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.]
3494 SeeAlso [Cudd_StdPreReordHook]
3496 ******************************************************************************/
3498 Cudd_StdPostReordHook(
3503 long initialTime
= (long) data
;
3505 long finalTime
= util_cpu_time();
3506 double totalTimeSec
= (double)(finalTime
- initialTime
) / 1000.0;
3508 retval
= fprintf(dd
->out
,"%ld nodes in %g sec\n", strcmp(str
, "BDD") == 0 ?
3509 Cudd_ReadNodeCount(dd
) : Cudd_zddReadNodeCount(dd
),
3511 if (retval
== EOF
) return(0);
3512 retval
= fflush(dd
->out
);
3513 if (retval
== EOF
) return(0);
3516 } /* end of Cudd_StdPostReordHook */
3519 /**Function********************************************************************
3521 Synopsis [Enables reporting of reordering stats.]
3523 Description [Enables reporting of reordering stats.
3524 Returns 1 if successful; 0 otherwise.]
3526 SideEffects [Installs functions in the pre-reordering and post-reordering
3529 SeeAlso [Cudd_DisableReorderingReporting Cudd_ReorderingReporting]
3531 ******************************************************************************/
3533 Cudd_EnableReorderingReporting(
3536 if (!Cudd_AddHook(dd
, Cudd_StdPreReordHook
, CUDD_PRE_REORDERING_HOOK
)) {
3539 if (!Cudd_AddHook(dd
, Cudd_StdPostReordHook
, CUDD_POST_REORDERING_HOOK
)) {
3544 } /* end of Cudd_EnableReorderingReporting */
3547 /**Function********************************************************************
3549 Synopsis [Disables reporting of reordering stats.]
3551 Description [Disables reporting of reordering stats.
3552 Returns 1 if successful; 0 otherwise.]
3554 SideEffects [Removes functions from the pre-reordering and post-reordering
3557 SeeAlso [Cudd_EnableReorderingReporting Cudd_ReorderingReporting]
3559 ******************************************************************************/
3561 Cudd_DisableReorderingReporting(
3564 if (!Cudd_RemoveHook(dd
, Cudd_StdPreReordHook
, CUDD_PRE_REORDERING_HOOK
)) {
3567 if (!Cudd_RemoveHook(dd
, Cudd_StdPostReordHook
, CUDD_POST_REORDERING_HOOK
)) {
3572 } /* end of Cudd_DisableReorderingReporting */
3575 /**Function********************************************************************
3577 Synopsis [Returns 1 if reporting of reordering stats is enabled.]
3579 Description [Returns 1 if reporting of reordering stats is enabled;
3584 SeeAlso [Cudd_EnableReorderingReporting Cudd_DisableReorderingReporting]
3586 ******************************************************************************/
3588 Cudd_ReorderingReporting(
3591 return(Cudd_IsInHook(dd
, Cudd_StdPreReordHook
, CUDD_PRE_REORDERING_HOOK
));
3593 } /* end of Cudd_ReorderingReporting */
3596 /**Function********************************************************************
3598 Synopsis [Returns the code of the last error.]
3600 Description [Returns the code of the last error. The error codes are
3605 SeeAlso [Cudd_ClearErrorCode]
3607 ******************************************************************************/
3612 return(dd
->errorCode
);
3614 } /* end of Cudd_ReadErrorCode */
3617 /**Function********************************************************************
3619 Synopsis [Clear the error code of a manager.]
3625 SeeAlso [Cudd_ReadErrorCode]
3627 ******************************************************************************/
3629 Cudd_ClearErrorCode(
3632 dd
->errorCode
= CUDD_NO_ERROR
;
3634 } /* end of Cudd_ClearErrorCode */
3637 /**Function********************************************************************
3639 Synopsis [Reads the stdout of a manager.]
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.]
3647 SeeAlso [Cudd_SetStdout Cudd_ReadStderr]
3649 ******************************************************************************/
3656 } /* end of Cudd_ReadStdout */
3659 /**Function********************************************************************
3661 Synopsis [Sets the stdout of a manager.]
3667 SeeAlso [Cudd_ReadStdout Cudd_SetStderr]
3669 ******************************************************************************/
3677 } /* end of Cudd_SetStdout */
3680 /**Function********************************************************************
3682 Synopsis [Reads the stderr of a manager.]
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.]
3690 SeeAlso [Cudd_SetStderr Cudd_ReadStdout]
3692 ******************************************************************************/
3699 } /* end of Cudd_ReadStderr */
3702 /**Function********************************************************************
3704 Synopsis [Sets the stderr of a manager.]
3710 SeeAlso [Cudd_ReadStderr Cudd_SetStdout]
3712 ******************************************************************************/
3720 } /* end of Cudd_SetStderr */
3723 /**Function********************************************************************
3725 Synopsis [Returns the threshold for the next dynamic reordering.]
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.]
3735 SeeAlso [Cudd_SetNextReordering]
3737 ******************************************************************************/
3739 Cudd_ReadNextReordering(
3742 return(dd
->nextDyn
);
3744 } /* end of Cudd_ReadNextReordering */
3747 /**Function********************************************************************
3749 Synopsis [Sets the threshold for the next dynamic reordering.]
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.]
3759 SeeAlso [Cudd_ReadNextReordering]
3761 ******************************************************************************/
3763 Cudd_SetNextReordering(
3769 } /* end of Cudd_SetNextReordering */
3772 /**Function********************************************************************
3774 Synopsis [Reads the number of elementary reordering steps.]
3782 ******************************************************************************/
3788 return(dd
->swapSteps
);
3793 } /* end of Cudd_ReadSwapSteps */
3796 /**Function********************************************************************
3798 Synopsis [Reads the maximum allowed number of live nodes.]
3800 Description [Reads the maximum allowed number of live nodes. When this
3801 number is exceeded, the package returns NULL.]
3805 SeeAlso [Cudd_SetMaxLive]
3807 ******************************************************************************/
3812 return(dd
->maxLive
);
3814 } /* end of Cudd_ReadMaxLive */
3817 /**Function********************************************************************
3819 Synopsis [Sets the maximum allowed number of live nodes.]
3821 Description [Sets the maximum allowed number of live nodes. When this
3822 number is exceeded, the package returns NULL.]
3826 SeeAlso [Cudd_ReadMaxLive]
3828 ******************************************************************************/
3832 unsigned int maxLive
)
3834 dd
->maxLive
= maxLive
;
3836 } /* end of Cudd_SetMaxLive */
3839 /**Function********************************************************************
3841 Synopsis [Reads the maximum allowed memory.]
3843 Description [Reads the maximum allowed memory. When this
3844 number is exceeded, the package returns NULL.]
3848 SeeAlso [Cudd_SetMaxMemory]
3850 ******************************************************************************/
3855 return(dd
->maxmemhard
);
3857 } /* end of Cudd_ReadMaxMemory */
3860 /**Function********************************************************************
3862 Synopsis [Sets the maximum allowed memory.]
3864 Description [Sets the maximum allowed memory. When this
3865 number is exceeded, the package returns NULL.]
3869 SeeAlso [Cudd_ReadMaxMemory]
3871 ******************************************************************************/
3875 unsigned long maxMemory
)
3877 dd
->maxmemhard
= maxMemory
;
3879 } /* end of Cudd_SetMaxMemory */
3882 /**Function********************************************************************
3884 Synopsis [Prevents sifting of a variable.]
3886 Description [This function sets a flag to prevent sifting of a
3887 variable. Returns 1 if successful; 0 otherwise (i.e., invalid
3890 SideEffects [Changes the "bindVar" flag in DdSubtable.]
3892 SeeAlso [Cudd_bddUnbindVar]
3894 ******************************************************************************/
3897 DdManager
*dd
/* manager */,
3898 int index
/* variable index */)
3900 if (index
>= dd
->size
|| index
< 0) return(0);
3901 dd
->subtables
[dd
->perm
[index
]].bindVar
= 1;
3904 } /* end of Cudd_bddBindVar */
3907 /**Function********************************************************************
3909 Synopsis [Allows the sifting of a variable.]
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).]
3918 SideEffects [Changes the "bindVar" flag in DdSubtable.]
3920 SeeAlso [Cudd_bddBindVar]
3922 ******************************************************************************/
3925 DdManager
*dd
/* manager */,
3926 int index
/* variable index */)
3928 if (index
>= dd
->size
|| index
< 0) return(0);
3929 dd
->subtables
[dd
->perm
[index
]].bindVar
= 0;
3932 } /* end of Cudd_bddUnbindVar */
3935 /**Function********************************************************************
3937 Synopsis [Tells whether a variable can be sifted.]
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.]
3947 SeeAlso [Cudd_bddBindVar Cudd_bddUnbindVar]
3949 ******************************************************************************/
3952 DdManager
*dd
/* manager */,
3953 int index
/* variable index */)
3955 if (index
>= dd
->size
|| index
< 0) return(0);
3956 return(dd
->subtables
[dd
->perm
[index
]].bindVar
);
3958 } /* end of Cudd_bddVarIsBound */
3961 /**Function********************************************************************
3963 Synopsis [Sets a variable type to primary input.]
3965 Description [Sets a variable type to primary input. The variable type is
3966 used by lazy sifting. Returns 1 if successful; 0 otherwise.]
3968 SideEffects [modifies the manager]
3970 SeeAlso [Cudd_bddSetPsVar Cudd_bddSetNsVar Cudd_bddIsPiVar]
3972 ******************************************************************************/
3975 DdManager
*dd
/* manager */,
3976 int index
/* variable index */)
3978 if (index
>= dd
->size
|| index
< 0) return (0);
3979 dd
->subtables
[dd
->perm
[index
]].varType
= CUDD_VAR_PRIMARY_INPUT
;
3982 } /* end of Cudd_bddSetPiVar */
3985 /**Function********************************************************************
3987 Synopsis [Sets a variable type to present state.]
3989 Description [Sets a variable type to present state. The variable type is
3990 used by lazy sifting. Returns 1 if successful; 0 otherwise.]
3992 SideEffects [modifies the manager]
3994 SeeAlso [Cudd_bddSetPiVar Cudd_bddSetNsVar Cudd_bddIsPsVar]
3996 ******************************************************************************/
3999 DdManager
*dd
/* manager */,
4000 int index
/* variable index */)
4002 if (index
>= dd
->size
|| index
< 0) return (0);
4003 dd
->subtables
[dd
->perm
[index
]].varType
= CUDD_VAR_PRESENT_STATE
;
4006 } /* end of Cudd_bddSetPsVar */
4009 /**Function********************************************************************
4011 Synopsis [Sets a variable type to next state.]
4013 Description [Sets a variable type to next state. The variable type is
4014 used by lazy sifting. Returns 1 if successful; 0 otherwise.]
4016 SideEffects [modifies the manager]
4018 SeeAlso [Cudd_bddSetPiVar Cudd_bddSetPsVar Cudd_bddIsNsVar]
4020 ******************************************************************************/
4023 DdManager
*dd
/* manager */,
4024 int index
/* variable index */)
4026 if (index
>= dd
->size
|| index
< 0) return (0);
4027 dd
->subtables
[dd
->perm
[index
]].varType
= CUDD_VAR_NEXT_STATE
;
4030 } /* end of Cudd_bddSetNsVar */
4033 /**Function********************************************************************
4035 Synopsis [Checks whether a variable is primary input.]
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.]
4043 SeeAlso [Cudd_bddSetPiVar Cudd_bddIsPsVar Cudd_bddIsNsVar]
4045 ******************************************************************************/
4048 DdManager
*dd
/* manager */,
4049 int index
/* variable index */)
4051 if (index
>= dd
->size
|| index
< 0) return -1;
4052 return (dd
->subtables
[dd
->perm
[index
]].varType
== CUDD_VAR_PRIMARY_INPUT
);
4054 } /* end of Cudd_bddIsPiVar */
4057 /**Function********************************************************************
4059 Synopsis [Checks whether a variable is present state.]
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.]
4067 SeeAlso [Cudd_bddSetPsVar Cudd_bddIsPiVar Cudd_bddIsNsVar]
4069 ******************************************************************************/
4075 if (index
>= dd
->size
|| index
< 0) return -1;
4076 return (dd
->subtables
[dd
->perm
[index
]].varType
== CUDD_VAR_PRESENT_STATE
);
4078 } /* end of Cudd_bddIsPsVar */
4081 /**Function********************************************************************
4083 Synopsis [Checks whether a variable is next state.]
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.]
4091 SeeAlso [Cudd_bddSetNsVar Cudd_bddIsPiVar Cudd_bddIsPsVar]
4093 ******************************************************************************/
4099 if (index
>= dd
->size
|| index
< 0) return -1;
4100 return (dd
->subtables
[dd
->perm
[index
]].varType
== CUDD_VAR_NEXT_STATE
);
4102 } /* end of Cudd_bddIsNsVar */
4105 /**Function********************************************************************
4107 Synopsis [Sets a corresponding pair index for a given index.]
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.]
4113 SideEffects [modifies the manager]
4115 SeeAlso [Cudd_bddReadPairIndex]
4117 ******************************************************************************/
4119 Cudd_bddSetPairIndex(
4120 DdManager
*dd
/* manager */,
4121 int index
/* variable index */,
4122 int pairIndex
/* corresponding variable index */)
4124 if (index
>= dd
->size
|| index
< 0) return(0);
4125 dd
->subtables
[dd
->perm
[index
]].pairIndex
= pairIndex
;
4128 } /* end of Cudd_bddSetPairIndex */
4131 /**Function********************************************************************
4133 Synopsis [Reads a corresponding pair index for a given index.]
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.]
4139 SideEffects [modifies the manager]
4141 SeeAlso [Cudd_bddSetPairIndex]
4143 ******************************************************************************/
4145 Cudd_bddReadPairIndex(
4149 if (index
>= dd
->size
|| index
< 0) return -1;
4150 return dd
->subtables
[dd
->perm
[index
]].pairIndex
;
4152 } /* end of Cudd_bddReadPairIndex */
4155 /**Function********************************************************************
4157 Synopsis [Sets a variable to be grouped.]
4159 Description [Sets a variable to be grouped. This function is used for
4160 lazy sifting. Returns 1 if successful; 0 otherwise.]
4162 SideEffects [modifies the manager]
4164 SeeAlso [Cudd_bddSetVarHardGroup Cudd_bddResetVarToBeGrouped]
4166 ******************************************************************************/
4168 Cudd_bddSetVarToBeGrouped(
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
;
4178 } /* end of Cudd_bddSetVarToBeGrouped */
4181 /**Function********************************************************************
4183 Synopsis [Sets a variable to be a hard group.]
4185 Description [Sets a variable to be a hard group. This function is used
4186 for lazy sifting. Returns 1 if successful; 0 otherwise.]
4188 SideEffects [modifies the manager]
4190 SeeAlso [Cudd_bddSetVarToBeGrouped Cudd_bddResetVarToBeGrouped
4191 Cudd_bddIsVarHardGroup]
4193 ******************************************************************************/
4195 Cudd_bddSetVarHardGroup(
4199 if (index
>= dd
->size
|| index
< 0) return(0);
4200 dd
->subtables
[dd
->perm
[index
]].varToBeGrouped
= CUDD_LAZY_HARD_GROUP
;
4203 } /* end of Cudd_bddSetVarHardGrouped */
4206 /**Function********************************************************************
4208 Synopsis [Resets a variable not to be grouped.]
4210 Description [Resets a variable not to be grouped. This function is
4211 used for lazy sifting. Returns 1 if successful; 0 otherwise.]
4213 SideEffects [modifies the manager]
4215 SeeAlso [Cudd_bddSetVarToBeGrouped Cudd_bddSetVarHardGroup]
4217 ******************************************************************************/
4219 Cudd_bddResetVarToBeGrouped(
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
;
4230 } /* end of Cudd_bddResetVarToBeGrouped */
4233 /**Function********************************************************************
4235 Synopsis [Checks whether a variable is set to be grouped.]
4237 Description [Checks whether a variable is set to be grouped. This
4238 function is used for lazy sifting.]
4244 ******************************************************************************/
4246 Cudd_bddIsVarToBeGrouped(
4250 if (index
>= dd
->size
|| index
< 0) return(-1);
4251 if (dd
->subtables
[dd
->perm
[index
]].varToBeGrouped
== CUDD_LAZY_UNGROUP
)
4254 return(dd
->subtables
[dd
->perm
[index
]].varToBeGrouped
);
4256 } /* end of Cudd_bddIsVarToBeGrouped */
4259 /**Function********************************************************************
4261 Synopsis [Sets a variable to be ungrouped.]
4263 Description [Sets a variable to be ungrouped. This function is used
4264 for lazy sifting. Returns 1 if successful; 0 otherwise.]
4266 SideEffects [modifies the manager]
4268 SeeAlso [Cudd_bddIsVarToBeUngrouped]
4270 ******************************************************************************/
4272 Cudd_bddSetVarToBeUngrouped(
4276 if (index
>= dd
->size
|| index
< 0) return(0);
4277 dd
->subtables
[dd
->perm
[index
]].varToBeGrouped
= CUDD_LAZY_UNGROUP
;
4280 } /* end of Cudd_bddSetVarToBeGrouped */
4283 /**Function********************************************************************
4285 Synopsis [Checks whether a variable is set to be ungrouped.]
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.]
4294 SeeAlso [Cudd_bddSetVarToBeUngrouped]
4296 ******************************************************************************/
4298 Cudd_bddIsVarToBeUngrouped(
4302 if (index
>= dd
->size
|| index
< 0) return(-1);
4303 return dd
->subtables
[dd
->perm
[index
]].varToBeGrouped
== CUDD_LAZY_UNGROUP
;
4305 } /* end of Cudd_bddIsVarToBeGrouped */
4308 /**Function********************************************************************
4310 Synopsis [Checks whether a variable is set to be in a hard group.]
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.]
4319 SeeAlso [Cudd_bddSetVarHardGroup]
4321 ******************************************************************************/
4323 Cudd_bddIsVarHardGroup(
4327 if (index
>= dd
->size
|| index
< 0) return(-1);
4328 if (dd
->subtables
[dd
->perm
[index
]].varToBeGrouped
== CUDD_LAZY_HARD_GROUP
)
4332 } /* end of Cudd_bddIsVarToBeGrouped */
4335 /*---------------------------------------------------------------------------*/
4336 /* Definition of internal functions */
4337 /*---------------------------------------------------------------------------*/
4339 /*---------------------------------------------------------------------------*/
4340 /* Definition of static functions */
4341 /*---------------------------------------------------------------------------*/
4344 /**Function********************************************************************
4346 Synopsis [Fixes a variable group tree.]
4350 SideEffects [Changes the variable group tree.]
4354 ******************************************************************************/
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
);
4370 } /* end of fixVarTree */
4373 /**Function********************************************************************
4375 Synopsis [Adds multiplicity groups to a ZDD variable group tree.]
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.]
4393 SideEffects [Changes the variable group tree.]
4395 SeeAlso [Cudd_zddVarsFromBddVars]
4397 ******************************************************************************/
4399 addMultiplicityGroups(
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*/)
4406 int startV
, stopV
, startL
;
4408 MtrNode
*auxnode
= treenode
;
4410 while (auxnode
!= NULL
) {
4411 if (auxnode
->child
!= NULL
) {
4412 addMultiplicityGroups(dd
,auxnode
->child
,multiplicity
,vmask
,lmask
);
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) {
4422 while (lmask
[j
] == 1) j
++;
4423 node
= Mtr_MakeGroup(auxnode
, j
* multiplicity
, multiplicity
,
4428 node
->index
= dd
->invpermZ
[i
* multiplicity
];
4433 auxnode
= auxnode
->younger
;
4437 } /* end of addMultiplicityGroups */