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