distr/cudd/cuddAPI.c

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