cuddAPI.c 128 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9
/**CFile***********************************************************************

  FileName    [cuddAPI.c]

  PackageName [cudd]

  Synopsis    [Application interface functions.]

  Description [External procedures included in this module:
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80
                <ul>
                <li> Cudd_addNewVar()
                <li> Cudd_addNewVarAtLevel()
                <li> Cudd_bddNewVar()
                <li> Cudd_bddNewVarAtLevel()
                <li> Cudd_addIthVar()
                <li> Cudd_bddIthVar()
                <li> Cudd_zddIthVar()
                <li> Cudd_zddVarsFromBddVars()
                <li> Cudd_addConst()
                <li> Cudd_IsNonConstant()
                <li> Cudd_AutodynEnable()
                <li> Cudd_AutodynDisable()
                <li> Cudd_ReorderingStatus()
                <li> Cudd_AutodynEnableZdd()
                <li> Cudd_AutodynDisableZdd()
                <li> Cudd_ReorderingStatusZdd()
                <li> Cudd_zddRealignmentEnabled()
                <li> Cudd_zddRealignEnable()
                <li> Cudd_zddRealignDisable()
                <li> Cudd_bddRealignmentEnabled()
                <li> Cudd_bddRealignEnable()
                <li> Cudd_bddRealignDisable()
                <li> Cudd_ReadOne()
                <li> Cudd_ReadZddOne()
                <li> Cudd_ReadZero()
                <li> Cudd_ReadLogicZero()
                <li> Cudd_ReadPlusInfinity()
                <li> Cudd_ReadMinusInfinity()
                <li> Cudd_ReadBackground()
                <li> Cudd_SetBackground()
                <li> Cudd_ReadCacheSlots()
                <li> Cudd_ReadCacheUsedSlots()
                <li> Cudd_ReadCacheLookUps()
                <li> Cudd_ReadCacheHits()
                <li> Cudd_ReadMinHit()
                <li> Cudd_SetMinHit()
                <li> Cudd_ReadLooseUpTo()
                <li> Cudd_SetLooseUpTo()
                <li> Cudd_ReadMaxCache()
                <li> Cudd_ReadMaxCacheHard()
                <li> Cudd_SetMaxCacheHard()
                <li> Cudd_ReadSize()
                <li> Cudd_ReadSlots()
                <li> Cudd_ReadUsedSlots()
                <li> Cudd_ExpectedUsedSlots()
                <li> Cudd_ReadKeys()
                <li> Cudd_ReadDead()
                <li> Cudd_ReadMinDead()
                <li> Cudd_ReadReorderings()
                <li> Cudd_ReadReorderingTime()
                <li> Cudd_ReadGarbageCollections()
                <li> Cudd_ReadGarbageCollectionTime()
                <li> Cudd_ReadNodesFreed()
                <li> Cudd_ReadNodesDropped()
                <li> Cudd_ReadUniqueLookUps()
                <li> Cudd_ReadUniqueLinks()
                <li> Cudd_ReadSiftMaxVar()
                <li> Cudd_SetSiftMaxVar()
                <li> Cudd_ReadMaxGrowth()
                <li> Cudd_SetMaxGrowth()
                <li> Cudd_ReadMaxGrowthAlternate()
                <li> Cudd_SetMaxGrowthAlternate()
                <li> Cudd_ReadReorderingCycle()
                <li> Cudd_SetReorderingCycle()
                <li> Cudd_ReadTree()
                <li> Cudd_SetTree()
                <li> Cudd_FreeTree()
                <li> Cudd_ReadZddTree()
                <li> Cudd_SetZddTree()
                <li> Cudd_FreeZddTree()
Alan Mishchenko committed
81
                <li> Cudd_NodeReadIndex()
82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154
                <li> Cudd_ReadPerm()
                <li> Cudd_ReadInvPerm()
                <li> Cudd_ReadVars()
                <li> Cudd_ReadEpsilon()
                <li> Cudd_SetEpsilon()
                <li> Cudd_ReadGroupCheck()
                <li> Cudd_SetGroupcheck()
                <li> Cudd_GarbageCollectionEnabled()
                <li> Cudd_EnableGarbageCollection()
                <li> Cudd_DisableGarbageCollection()
                <li> Cudd_DeadAreCounted()
                <li> Cudd_TurnOnCountDead()
                <li> Cudd_TurnOffCountDead()
                <li> Cudd_ReadRecomb()
                <li> Cudd_SetRecomb()
                <li> Cudd_ReadSymmviolation()
                <li> Cudd_SetSymmviolation()
                <li> Cudd_ReadArcviolation()
                <li> Cudd_SetArcviolation()
                <li> Cudd_ReadPopulationSize()
                <li> Cudd_SetPopulationSize()
                <li> Cudd_ReadNumberXovers()
                <li> Cudd_SetNumberXovers()
                <li> Cudd_ReadMemoryInUse()
                <li> Cudd_PrintInfo()
                <li> Cudd_ReadPeakNodeCount()
                <li> Cudd_ReadPeakLiveNodeCount()
                <li> Cudd_ReadNodeCount()
                <li> Cudd_zddReadNodeCount()
                <li> Cudd_AddHook()
                <li> Cudd_RemoveHook()
                <li> Cudd_IsInHook()
                <li> Cudd_StdPreReordHook()
                <li> Cudd_StdPostReordHook()
                <li> Cudd_EnableReorderingReporting()
                <li> Cudd_DisableReorderingReporting()
                <li> Cudd_ReorderingReporting()
                <li> Cudd_ReadErrorCode()
                <li> Cudd_ClearErrorCode()
                <li> Cudd_ReadStdout()
                <li> Cudd_SetStdout()
                <li> Cudd_ReadStderr()
                <li> Cudd_SetStderr()
                <li> Cudd_ReadNextReordering()
                <li> Cudd_SetNextReordering()
                <li> Cudd_ReadSwapSteps()
                <li> Cudd_ReadMaxLive()
                <li> Cudd_SetMaxLive()
                <li> Cudd_ReadMaxMemory()
                <li> Cudd_SetMaxMemory()
                <li> Cudd_bddBindVar()
                <li> Cudd_bddUnbindVar()
                <li> Cudd_bddVarIsBound()
                <li> Cudd_bddSetPiVar()
                <li> Cudd_bddSetPsVar()
                <li> Cudd_bddSetNsVar()
                <li> Cudd_bddIsPiVar()
                <li> Cudd_bddIsPsVar()
                <li> Cudd_bddIsNsVar()
                <li> Cudd_bddSetPairIndex()
                <li> Cudd_bddReadPairIndex()
                <li> Cudd_bddSetVarToBeGrouped()
                <li> Cudd_bddSetVarHardGroup()
                <li> Cudd_bddResetVarToBeGrouped()
                <li> Cudd_bddIsVarToBeGrouped()
                <li> Cudd_bddSetVarToBeUngrouped()
                <li> Cudd_bddIsVarToBeUngrouped()
                <li> Cudd_bddIsVarHardGroup()
                </ul>
              Static procedures included in this module:
                <ul>
                <li> fixVarTree()
                </ul>]
Alan Mishchenko committed
155 156 157 158 159

  SeeAlso     []

  Author      [Fabio Somenzi]

160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190
  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado

  All rights reserved.

  Redistribution and use in source and binary forms, with or without
  modification, are permitted provided that the following conditions
  are met:

  Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

  Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

  Neither the name of the University of Colorado nor the names of its
  contributors may be used to endorse or promote products derived from
  this software without specific prior written permission.

  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  POSSIBILITY OF SUCH DAMAGE.]
Alan Mishchenko committed
191 192 193

******************************************************************************/

194
#include "misc/util/util_hack.h"
195
#include "cuddInt.h"
Alan Mishchenko committed
196

197 198 199
ABC_NAMESPACE_IMPL_START


200

Alan Mishchenko committed
201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217
/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
218
static char rcsid[] DD_UNUSED = "$Id: cuddAPI.c,v 1.59 2009/02/19 16:14:14 fabio Exp $";
Alan Mishchenko committed
219 220 221 222 223 224 225 226 227 228 229 230
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

231 232
static void fixVarTree (MtrNode *treenode, int *perm, int size);
static int addMultiplicityGroups (DdManager *dd, MtrNode *treenode, int multiplicity, char *vmask, char *lmask);
Alan Mishchenko committed
233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265

/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [Returns a new ADD variable.]

  Description [Creates a new ADD variable.  The new variable has an
  index equal to the largest previous index plus 1.  Returns a
  pointer to the new variable if successful; NULL otherwise.
  An ADD variable differs from a BDD variable because it points to the
  arithmetic zero, instead of having a complement pointer to 1. ]

  SideEffects [None]

  SeeAlso     [Cudd_bddNewVar Cudd_addIthVar Cudd_addConst
  Cudd_addNewVarAtLevel]

******************************************************************************/
DdNode *
Cudd_addNewVar(
  DdManager * dd)
{
    DdNode *res;

    if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
    do {
266 267
        dd->reordered = 0;
        res = cuddUniqueInter(dd,dd->size,DD_ONE(dd),DD_ZERO(dd));
Alan Mishchenko committed
268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299
    } while (dd->reordered == 1);

    return(res);

} /* end of Cudd_addNewVar */


/**Function********************************************************************

  Synopsis    [Returns a new ADD variable at a specified level.]

  Description [Creates a new ADD variable.  The new variable has an
  index equal to the largest previous index plus 1 and is positioned at
  the specified level in the order.  Returns a pointer to the new
  variable if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addNewVar Cudd_addIthVar Cudd_bddNewVarAtLevel]

******************************************************************************/
DdNode *
Cudd_addNewVarAtLevel(
  DdManager * dd,
  int  level)
{
    DdNode *res;

    if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
    if (level >= dd->size) return(Cudd_addIthVar(dd,level));
    if (!cuddInsertSubtables(dd,1,level)) return(NULL);
    do {
300 301
        dd->reordered = 0;
        res = cuddUniqueInter(dd,dd->size - 1,DD_ONE(dd),DD_ZERO(dd));
Alan Mishchenko committed
302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391
    } while (dd->reordered == 1);

    return(res);

} /* end of Cudd_addNewVarAtLevel */


/**Function********************************************************************

  Synopsis    [Returns a new BDD variable.]

  Description [Creates a new BDD variable.  The new variable has an
  index equal to the largest previous index plus 1.  Returns a
  pointer to the new variable if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addNewVar Cudd_bddIthVar Cudd_bddNewVarAtLevel]

******************************************************************************/
DdNode *
Cudd_bddNewVar(
  DdManager * dd)
{
    DdNode *res;

    if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
    res = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one));

    return(res);

} /* end of Cudd_bddNewVar */


/**Function********************************************************************

  Synopsis    [Returns a new BDD variable at a specified level.]

  Description [Creates a new BDD variable.  The new variable has an
  index equal to the largest previous index plus 1 and is positioned at
  the specified level in the order.  Returns a pointer to the new
  variable if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddNewVar Cudd_bddIthVar Cudd_addNewVarAtLevel]

******************************************************************************/
DdNode *
Cudd_bddNewVarAtLevel(
  DdManager * dd,
  int  level)
{
    DdNode *res;

    if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
    if (level >= dd->size) return(Cudd_bddIthVar(dd,level));
    if (!cuddInsertSubtables(dd,1,level)) return(NULL);
    res = dd->vars[dd->size - 1];

    return(res);

} /* end of Cudd_bddNewVarAtLevel */


/**Function********************************************************************

  Synopsis    [Returns the ADD variable with index i.]

  Description [Retrieves the ADD variable with index i if it already
  exists, or creates a new ADD variable.  Returns a pointer to the
  variable if successful; NULL otherwise.  An ADD variable differs from
  a BDD variable because it points to the arithmetic zero, instead of
  having a complement pointer to 1. ]

  SideEffects [None]

  SeeAlso     [Cudd_addNewVar Cudd_bddIthVar Cudd_addConst
  Cudd_addNewVarAtLevel]

******************************************************************************/
DdNode *
Cudd_addIthVar(
  DdManager * dd,
  int  i)
{
    DdNode *res;

    if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL);
    do {
392 393
        dd->reordered = 0;
        res = cuddUniqueInter(dd,i,DD_ONE(dd),DD_ZERO(dd));
Alan Mishchenko committed
394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423
    } while (dd->reordered == 1);

    return(res);

} /* end of Cudd_addIthVar */


/**Function********************************************************************

  Synopsis    [Returns the BDD variable with index i.]

  Description [Retrieves the BDD variable with index i if it already
  exists, or creates a new BDD variable.  Returns a pointer to the
  variable if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddNewVar Cudd_addIthVar Cudd_bddNewVarAtLevel
  Cudd_ReadVars]

******************************************************************************/
DdNode *
Cudd_bddIthVar(
  DdManager * dd,
  int  i)
{
    DdNode *res;

    if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL);
    if (i < dd->size) {
424
        res = dd->vars[i];
Alan Mishchenko committed
425
    } else {
426
        res = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
Alan Mishchenko committed
427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467
    }

    return(res);

} /* end of Cudd_bddIthVar */


/**Function********************************************************************

  Synopsis    [Returns the ZDD variable with index i.]

  Description [Retrieves the ZDD variable with index i if it already
  exists, or creates a new ZDD variable.  Returns a pointer to the
  variable if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddIthVar Cudd_addIthVar]

******************************************************************************/
DdNode *
Cudd_zddIthVar(
  DdManager * dd,
  int  i)
{
    DdNode *res;
    DdNode *zvar;
    DdNode *lower;
    int j;

    if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL);

    /* The i-th variable function has the following structure:
    ** at the level corresponding to index i there is a node whose "then"
    ** child points to the universe, and whose "else" child points to zero.
    ** Above that level there are nodes with identical children.
    */

    /* First we build the node at the level of index i. */
    lower = (i < dd->sizeZ - 1) ? dd->univ[dd->permZ[i]+1] : DD_ONE(dd);
    do {
468 469
        dd->reordered = 0;
        zvar = cuddUniqueInterZdd(dd, i, lower, DD_ZERO(dd));
Alan Mishchenko committed
470 471 472
    } while (dd->reordered == 1);

    if (zvar == NULL)
473
        return(NULL);
Alan Mishchenko committed
474 475 476 477
    cuddRef(zvar);

    /* Now we add the "filler" nodes above the level of index i. */
    for (j = dd->permZ[i] - 1; j >= 0; j--) {
478 479 480 481 482 483 484 485 486
        do {
            dd->reordered = 0;
            res = cuddUniqueInterZdd(dd, dd->invpermZ[j], zvar, zvar);
        } while (dd->reordered == 1);
        if (res == NULL) {
            Cudd_RecursiveDerefZdd(dd,zvar);
            return(NULL);
        }
        cuddRef(res);
Alan Mishchenko committed
487
        Cudd_RecursiveDerefZdd(dd,zvar);
488
        zvar = res;
Alan Mishchenko committed
489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530
    }
    cuddDeref(zvar);
    return(zvar);

} /* end of Cudd_zddIthVar */


/**Function********************************************************************

  Synopsis    [Creates one or more ZDD variables for each BDD variable.]

  Description [Creates one or more ZDD variables for each BDD
  variable.  If some ZDD variables already exist, only the missing
  variables are created.  Parameter multiplicity allows the caller to
  control how many variables are created for each BDD variable in
  existence. For instance, if ZDDs are used to represent covers, two
  ZDD variables are required for each BDD variable.  The order of the
  BDD variables is transferred to the ZDD variables. If a variable
  group tree exists for the BDD variables, a corresponding ZDD
  variable group tree is created by expanding the BDD variable
  tree. In any case, the ZDD variables derived from the same BDD
  variable are merged in a ZDD variable group. If a ZDD variable group
  tree exists, it is freed. Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddNewVar Cudd_bddIthVar Cudd_bddNewVarAtLevel]

******************************************************************************/
int
Cudd_zddVarsFromBddVars(
  DdManager * dd /* DD manager */,
  int multiplicity /* how many ZDD variables are created for each BDD variable */)
{
    int res;
    int i, j;
    int allnew;
    int *permutation;

    if (multiplicity < 1) return(0);
    allnew = dd->sizeZ == 0;
    if (dd->size * multiplicity > dd->sizeZ) {
531 532
        res = cuddResizeTableZdd(dd,dd->size * multiplicity - 1);
        if (res == 0) return(0);
Alan Mishchenko committed
533 534 535
    }
    /* Impose the order of the BDD variables to the ZDD variables. */
    if (allnew) {
536 537 538 539 540 541 542 543 544 545
        for (i = 0; i < dd->size; i++) {
            for (j = 0; j < multiplicity; j++) {
                dd->permZ[i * multiplicity + j] =
                    dd->perm[i] * multiplicity + j;
                dd->invpermZ[dd->permZ[i * multiplicity + j]] =
                    i * multiplicity + j;
            }
        }
        for (i = 0; i < dd->sizeZ; i++) {
            dd->univ[i]->index = dd->invpermZ[i];
Alan Mishchenko committed
546 547
        }
    } else {
548 549 550 551
        permutation = ABC_ALLOC(int,dd->sizeZ);
        if (permutation == NULL) {
            dd->errorCode = CUDD_MEMORY_OUT;
            return(0);
Alan Mishchenko committed
552
        }
553 554 555 556 557 558 559 560 561 562 563 564
        for (i = 0; i < dd->size; i++) {
            for (j = 0; j < multiplicity; j++) {
                permutation[i * multiplicity + j] =
                    dd->invperm[i] * multiplicity + j;
            }
        }
        for (i = dd->size * multiplicity; i < dd->sizeZ; i++) {
            permutation[i] = i;
        }
        res = Cudd_zddShuffleHeap(dd, permutation);
        ABC_FREE(permutation);
        if (res == 0) return(0);
Alan Mishchenko committed
565 566 567
    }
    /* Copy and expand the variable group tree if it exists. */
    if (dd->treeZ != NULL) {
568
        Cudd_FreeZddTree(dd);
Alan Mishchenko committed
569 570
    }
    if (dd->tree != NULL) {
571 572
        dd->treeZ = Mtr_CopyTree(dd->tree, multiplicity);
        if (dd->treeZ == NULL) return(0);
Alan Mishchenko committed
573
    } else if (multiplicity > 1) {
574 575 576
        dd->treeZ = Mtr_InitGroupTree(0, dd->sizeZ);
        if (dd->treeZ == NULL) return(0);
        dd->treeZ->index = dd->invpermZ[0];
Alan Mishchenko committed
577 578 579 580
    }
    /* Create groups for the ZDD variables derived from the same BDD variable.
    */
    if (multiplicity > 1) {
581
        char *vmask, *lmask;
Alan Mishchenko committed
582

583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599
        vmask = ABC_ALLOC(char, dd->size);
        if (vmask == NULL) {
            dd->errorCode = CUDD_MEMORY_OUT;
            return(0);
        }
        lmask =  ABC_ALLOC(char, dd->size);
        if (lmask == NULL) {
            dd->errorCode = CUDD_MEMORY_OUT;
            return(0);
        }
        for (i = 0; i < dd->size; i++) {
            vmask[i] = lmask[i] = 0;
        }
        res = addMultiplicityGroups(dd,dd->treeZ,multiplicity,vmask,lmask);
        ABC_FREE(vmask);
        ABC_FREE(lmask);
        if (res == 0) return(0);
Alan Mishchenko committed
600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674
    }
    return(1);

} /* end of Cudd_zddVarsFromBddVars */


/**Function********************************************************************

  Synopsis    [Returns the ADD for constant c.]

  Description [Retrieves the ADD for constant c if it already
  exists, or creates a new ADD.  Returns a pointer to the
  ADD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addNewVar Cudd_addIthVar]

******************************************************************************/
DdNode *
Cudd_addConst(
  DdManager * dd,
  CUDD_VALUE_TYPE  c)
{
    return(cuddUniqueConst(dd,c));

} /* end of Cudd_addConst */


/**Function********************************************************************

  Synopsis    [Returns 1 if a DD node is not constant.]

  Description [Returns 1 if a DD node is not constant. This function is
  useful to test the results of Cudd_bddIteConstant, Cudd_addIteConstant,
  Cudd_addEvalConst. These results may be a special value signifying
  non-constant. In the other cases the macro Cudd_IsConstant can be used.]

  SideEffects [None]

  SeeAlso     [Cudd_IsConstant Cudd_bddIteConstant Cudd_addIteConstant
  Cudd_addEvalConst]

******************************************************************************/
int
Cudd_IsNonConstant(
  DdNode *f)
{
    return(f == DD_NON_CONSTANT || !Cudd_IsConstant(f));

} /* end of Cudd_IsNonConstant */


/**Function********************************************************************

  Synopsis    [Enables automatic dynamic reordering of BDDs and ADDs.]

  Description [Enables automatic dynamic reordering of BDDs and
  ADDs. Parameter method is used to determine the method used for
  reordering. If CUDD_REORDER_SAME is passed, the method is
  unchanged.]

  SideEffects [None]

  SeeAlso     [Cudd_AutodynDisable Cudd_ReorderingStatus
  Cudd_AutodynEnableZdd]

******************************************************************************/
void
Cudd_AutodynEnable(
  DdManager * unique,
  Cudd_ReorderingType  method)
{
    unique->autoDyn = 1;
    if (method != CUDD_REORDER_SAME) {
675
        unique->autoMethod = method;
Alan Mishchenko committed
676 677 678 679 680 681 682 683 684
    }
#ifndef DD_NO_DEATH_ROW
    /* If reordering is enabled, using the death row causes too many
    ** invocations. Hence, we shrink the death row to just one entry.
    */
    cuddClearDeathRow(unique);
    unique->deathRowDepth = 1;
    unique->deadMask = unique->deathRowDepth - 1;
    if ((unsigned) unique->nextDead > unique->deadMask) {
685
        unique->nextDead = 0;
Alan Mishchenko committed
686
    }
Alan Mishchenko committed
687
    unique->deathRow = ABC_REALLOC(DdNodePtr, unique->deathRow,
688
        unique->deathRowDepth);
Alan Mishchenko committed
689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765
#endif
    return;

} /* end of Cudd_AutodynEnable */


/**Function********************************************************************

  Synopsis    [Disables automatic dynamic reordering.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_AutodynEnable Cudd_ReorderingStatus
  Cudd_AutodynDisableZdd]

******************************************************************************/
void
Cudd_AutodynDisable(
  DdManager * unique)
{
    unique->autoDyn = 0;
    return;

} /* end of Cudd_AutodynDisable */


/**Function********************************************************************

  Synopsis    [Reports the status of automatic dynamic reordering of BDDs
  and ADDs.]

  Description [Reports the status of automatic dynamic reordering of
  BDDs and ADDs. Parameter method is set to the reordering method
  currently selected. Returns 1 if automatic reordering is enabled; 0
  otherwise.]

  SideEffects [Parameter method is set to the reordering method currently
  selected.]

  SeeAlso     [Cudd_AutodynEnable Cudd_AutodynDisable
  Cudd_ReorderingStatusZdd]

******************************************************************************/
int
Cudd_ReorderingStatus(
  DdManager * unique,
  Cudd_ReorderingType * method)
{
    *method = unique->autoMethod;
    return(unique->autoDyn);

} /* end of Cudd_ReorderingStatus */


/**Function********************************************************************

  Synopsis    [Enables automatic dynamic reordering of ZDDs.]

  Description [Enables automatic dynamic reordering of ZDDs. Parameter
  method is used to determine the method used for reordering ZDDs. If
  CUDD_REORDER_SAME is passed, the method is unchanged.]

  SideEffects [None]

  SeeAlso     [Cudd_AutodynDisableZdd Cudd_ReorderingStatusZdd
  Cudd_AutodynEnable]

******************************************************************************/
void
Cudd_AutodynEnableZdd(
  DdManager * unique,
  Cudd_ReorderingType method)
{
    unique->autoDynZ = 1;
    if (method != CUDD_REORDER_SAME) {
766
        unique->autoMethodZ = method;
Alan Mishchenko committed
767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014
    }
    return;

} /* end of Cudd_AutodynEnableZdd */


/**Function********************************************************************

  Synopsis    [Disables automatic dynamic reordering of ZDDs.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_AutodynEnableZdd Cudd_ReorderingStatusZdd
  Cudd_AutodynDisable]

******************************************************************************/
void
Cudd_AutodynDisableZdd(
  DdManager * unique)
{
    unique->autoDynZ = 0;
    return;

} /* end of Cudd_AutodynDisableZdd */


/**Function********************************************************************

  Synopsis    [Reports the status of automatic dynamic reordering of ZDDs.]

  Description [Reports the status of automatic dynamic reordering of
  ZDDs. Parameter method is set to the ZDD reordering method currently
  selected. Returns 1 if automatic reordering is enabled; 0
  otherwise.]

  SideEffects [Parameter method is set to the ZDD reordering method currently
  selected.]

  SeeAlso     [Cudd_AutodynEnableZdd Cudd_AutodynDisableZdd
  Cudd_ReorderingStatus]

******************************************************************************/
int
Cudd_ReorderingStatusZdd(
  DdManager * unique,
  Cudd_ReorderingType * method)
{
    *method = unique->autoMethodZ;
    return(unique->autoDynZ);

} /* end of Cudd_ReorderingStatusZdd */


/**Function********************************************************************

  Synopsis    [Tells whether the realignment of ZDD order to BDD order is
  enabled.]

  Description [Returns 1 if the realignment of ZDD order to BDD order is
  enabled; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_zddRealignEnable Cudd_zddRealignDisable
  Cudd_bddRealignEnable Cudd_bddRealignDisable]

******************************************************************************/
int
Cudd_zddRealignmentEnabled(
  DdManager * unique)
{
    return(unique->realign);

} /* end of Cudd_zddRealignmentEnabled */


/**Function********************************************************************

  Synopsis    [Enables realignment of ZDD order to BDD order.]

  Description [Enables realignment of the ZDD variable order to the
  BDD variable order after the BDDs and ADDs have been reordered.  The
  number of ZDD variables must be a multiple of the number of BDD
  variables for realignment to make sense. If this condition is not met,
  Cudd_ReduceHeap will return 0. Let <code>M</code> be the
  ratio of the two numbers. For the purpose of realignment, the ZDD
  variables from <code>M*i</code> to <code>(M+1)*i-1</code> are
  reagarded as corresponding to BDD variable <code>i</code>. Realignment
  is initially disabled.]

  SideEffects [None]

  SeeAlso     [Cudd_ReduceHeap Cudd_zddRealignDisable
  Cudd_zddRealignmentEnabled Cudd_bddRealignDisable
  Cudd_bddRealignmentEnabled]

******************************************************************************/
void
Cudd_zddRealignEnable(
  DdManager * unique)
{
    unique->realign = 1;
    return;

} /* end of Cudd_zddRealignEnable */


/**Function********************************************************************

  Synopsis    [Disables realignment of ZDD order to BDD order.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_zddRealignEnable Cudd_zddRealignmentEnabled
  Cudd_bddRealignEnable Cudd_bddRealignmentEnabled]

******************************************************************************/
void
Cudd_zddRealignDisable(
  DdManager * unique)
{
    unique->realign = 0;
    return;

} /* end of Cudd_zddRealignDisable */


/**Function********************************************************************

  Synopsis    [Tells whether the realignment of BDD order to ZDD order is
  enabled.]

  Description [Returns 1 if the realignment of BDD order to ZDD order is
  enabled; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddRealignEnable Cudd_bddRealignDisable
  Cudd_zddRealignEnable Cudd_zddRealignDisable]

******************************************************************************/
int
Cudd_bddRealignmentEnabled(
  DdManager * unique)
{
    return(unique->realignZ);

} /* end of Cudd_bddRealignmentEnabled */


/**Function********************************************************************

  Synopsis    [Enables realignment of BDD order to ZDD order.]

  Description [Enables realignment of the BDD variable order to the
  ZDD variable order after the ZDDs have been reordered.  The
  number of ZDD variables must be a multiple of the number of BDD
  variables for realignment to make sense. If this condition is not met,
  Cudd_zddReduceHeap will return 0. Let <code>M</code> be the
  ratio of the two numbers. For the purpose of realignment, the ZDD
  variables from <code>M*i</code> to <code>(M+1)*i-1</code> are
  reagarded as corresponding to BDD variable <code>i</code>. Realignment
  is initially disabled.]

  SideEffects [None]

  SeeAlso     [Cudd_zddReduceHeap Cudd_bddRealignDisable
  Cudd_bddRealignmentEnabled Cudd_zddRealignDisable
  Cudd_zddRealignmentEnabled]

******************************************************************************/
void
Cudd_bddRealignEnable(
  DdManager * unique)
{
    unique->realignZ = 1;
    return;

} /* end of Cudd_bddRealignEnable */


/**Function********************************************************************

  Synopsis    [Disables realignment of ZDD order to BDD order.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_bddRealignEnable Cudd_bddRealignmentEnabled
  Cudd_zddRealignEnable Cudd_zddRealignmentEnabled]

******************************************************************************/
void
Cudd_bddRealignDisable(
  DdManager * unique)
{
    unique->realignZ = 0;
    return;

} /* end of Cudd_bddRealignDisable */


/**Function********************************************************************

  Synopsis    [Returns the one constant of the manager.]

  Description [Returns the one constant of the manager. The one
  constant is common to ADDs and BDDs.]

  SideEffects [None]

  SeeAlso [Cudd_ReadZero Cudd_ReadLogicZero Cudd_ReadZddOne]

******************************************************************************/
DdNode *
Cudd_ReadOne(
  DdManager * dd)
{
    return(dd->one);

} /* end of Cudd_ReadOne */


/**Function********************************************************************

  Synopsis    [Returns the ZDD for the constant 1 function.]

  Description [Returns the ZDD for the constant 1 function.
  The representation of the constant 1 function as a ZDD depends on
  how many variables it (nominally) depends on. The index of the
  topmost variable in the support is given as argument <code>i</code>.]

  SideEffects [None]

  SeeAlso [Cudd_ReadOne]

******************************************************************************/
DdNode *
Cudd_ReadZddOne(
  DdManager * dd,
  int  i)
{
    if (i < 0)
1015
        return(NULL);
Alan Mishchenko committed
1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183
    return(i < dd->sizeZ ? dd->univ[i] : DD_ONE(dd));

} /* end of Cudd_ReadZddOne */



/**Function********************************************************************

  Synopsis    [Returns the zero constant of the manager.]

  Description [Returns the zero constant of the manager. The zero
  constant is the arithmetic zero, rather than the logic zero. The
  latter is the complement of the one constant.]

  SideEffects [None]

  SeeAlso [Cudd_ReadOne Cudd_ReadLogicZero]

******************************************************************************/
DdNode *
Cudd_ReadZero(
  DdManager * dd)
{
    return(DD_ZERO(dd));

} /* end of Cudd_ReadZero */


/**Function********************************************************************

  Synopsis    [Returns the logic zero constant of the manager.]

  Description [Returns the zero constant of the manager. The logic zero
  constant is the complement of the one constant, and is distinct from
  the arithmetic zero.]

  SideEffects [None]

  SeeAlso [Cudd_ReadOne Cudd_ReadZero]

******************************************************************************/
DdNode *
Cudd_ReadLogicZero(
  DdManager * dd)
{
    return(Cudd_Not(DD_ONE(dd)));

} /* end of Cudd_ReadLogicZero */


/**Function********************************************************************

  Synopsis    [Reads the plus-infinity constant from the manager.]

  Description []

  SideEffects [None]

******************************************************************************/
DdNode *
Cudd_ReadPlusInfinity(
  DdManager * dd)
{
    return(dd->plusinfinity);

} /* end of Cudd_ReadPlusInfinity */


/**Function********************************************************************

  Synopsis    [Reads the minus-infinity constant from the manager.]

  Description []

  SideEffects [None]

******************************************************************************/
DdNode *
Cudd_ReadMinusInfinity(
  DdManager * dd)
{
    return(dd->minusinfinity);

} /* end of Cudd_ReadMinusInfinity */


/**Function********************************************************************

  Synopsis    [Reads the background constant of the manager.]

  Description []

  SideEffects [None]

******************************************************************************/
DdNode *
Cudd_ReadBackground(
  DdManager * dd)
{
    return(dd->background);

} /* end of Cudd_ReadBackground */


/**Function********************************************************************

  Synopsis    [Sets the background constant of the manager.]

  Description [Sets the background constant of the manager. It assumes
  that the DdNode pointer bck is already referenced.]

  SideEffects [None]

******************************************************************************/
void
Cudd_SetBackground(
  DdManager * dd,
  DdNode * bck)
{
    dd->background = bck;

} /* end of Cudd_SetBackground */


/**Function********************************************************************

  Synopsis    [Reads the number of slots in the cache.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_ReadCacheUsedSlots]

******************************************************************************/
unsigned int
Cudd_ReadCacheSlots(
  DdManager * dd)
{
    return(dd->cacheSlots);

} /* end of Cudd_ReadCacheSlots */


/**Function********************************************************************

  Synopsis    [Reads the fraction of used slots in the cache.]

  Description [Reads the fraction of used slots in the cache. The unused
  slots are those in which no valid data is stored. Garbage collection,
  variable reordering, and cache resizing may cause used slots to become
  unused.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadCacheSlots]

******************************************************************************/
double
Cudd_ReadCacheUsedSlots(
  DdManager * dd)
{
    unsigned long used = 0;
    int slots = dd->cacheSlots;
    DdCache *cache = dd->cache;
    int i;

    for (i = 0; i < slots; i++) {
1184
        used += cache[i].h != 0;
Alan Mishchenko committed
1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207
    }

    return((double)used / (double) dd->cacheSlots);

} /* end of Cudd_ReadCacheUsedSlots */


/**Function********************************************************************

  Synopsis    [Returns the number of cache look-ups.]

  Description [Returns the number of cache look-ups.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadCacheHits]

******************************************************************************/
double
Cudd_ReadCacheLookUps(
  DdManager * dd)
{
    return(dd->cacheHits + dd->cacheMisses +
1208
           dd->totCachehits + dd->totCacheMisses);
Alan Mishchenko committed
1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349

} /* end of Cudd_ReadCacheLookUps */


/**Function********************************************************************

  Synopsis    [Returns the number of cache hits.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_ReadCacheLookUps]

******************************************************************************/
double
Cudd_ReadCacheHits(
  DdManager * dd)
{
    return(dd->cacheHits + dd->totCachehits);

} /* end of Cudd_ReadCacheHits */


/**Function********************************************************************

  Synopsis    [Returns the number of recursive calls.]

  Description [Returns the number of recursive calls if the package is
  compiled with DD_COUNT defined.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
double
Cudd_ReadRecursiveCalls(
  DdManager * dd)
{
#ifdef DD_COUNT
    return(dd->recursiveCalls);
#else
    return(-1.0);
#endif

} /* end of Cudd_ReadRecursiveCalls */



/**Function********************************************************************

  Synopsis    [Reads the hit rate that causes resizinig of the computed
  table.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_SetMinHit]

******************************************************************************/
unsigned int
Cudd_ReadMinHit(
  DdManager * dd)
{
    /* Internally, the package manipulates the ratio of hits to
    ** misses instead of the ratio of hits to accesses. */
    return((unsigned int) (0.5 + 100 * dd->minHit / (1 + dd->minHit)));

} /* end of Cudd_ReadMinHit */


/**Function********************************************************************

  Synopsis    [Sets the hit rate that causes resizinig of the computed
  table.]

  Description [Sets the minHit parameter of the manager. This
  parameter controls the resizing of the computed table. If the hit
  rate is larger than the specified value, and the cache is not
  already too large, then its size is doubled.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadMinHit]

******************************************************************************/
void
Cudd_SetMinHit(
  DdManager * dd,
  unsigned int hr)
{
    /* Internally, the package manipulates the ratio of hits to
    ** misses instead of the ratio of hits to accesses. */
    dd->minHit = (double) hr / (100.0 - (double) hr);

} /* end of Cudd_SetMinHit */


/**Function********************************************************************

  Synopsis    [Reads the looseUpTo parameter of the manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_SetLooseUpTo Cudd_ReadMinHit Cudd_ReadMinDead]

******************************************************************************/
unsigned int
Cudd_ReadLooseUpTo(
  DdManager * dd)
{
    return(dd->looseUpTo);

} /* end of Cudd_ReadLooseUpTo */


/**Function********************************************************************

  Synopsis    [Sets the looseUpTo parameter of the manager.]

  Description [Sets the looseUpTo parameter of the manager. This
  parameter of the manager controls the threshold beyond which no fast
  growth of the unique table is allowed. The threshold is given as a
  number of slots. If the value passed to this function is 0, the
  function determines a suitable value based on the available memory.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadLooseUpTo Cudd_SetMinHit]

******************************************************************************/
void
Cudd_SetLooseUpTo(
  DdManager * dd,
  unsigned int lut)
{
    if (lut == 0) {
1350 1351 1352
        unsigned long datalimit = getSoftDataLimit();
        lut = (unsigned int) (datalimit / (sizeof(DdNode) *
                                           DD_MAX_LOOSE_FRACTION));
Alan Mishchenko committed
1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391 1392 1393 1394 1395 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 1407 1408 1409 1410 1411 1412 1413 1414 1415 1416 1417 1418 1419
    }
    dd->looseUpTo = lut;

} /* end of Cudd_SetLooseUpTo */


/**Function********************************************************************

  Synopsis    [Returns the soft limit for the cache size.]

  Description [Returns the soft limit for the cache size. The soft limit]

  SideEffects [None]

  SeeAlso     [Cudd_ReadMaxCache]

******************************************************************************/
unsigned int
Cudd_ReadMaxCache(
  DdManager * dd)
{
    return(2 * dd->cacheSlots + dd->cacheSlack);

} /* end of Cudd_ReadMaxCache */


/**Function********************************************************************

  Synopsis    [Reads the maxCacheHard parameter of the manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_SetMaxCacheHard Cudd_ReadMaxCache]

******************************************************************************/
unsigned int
Cudd_ReadMaxCacheHard(
  DdManager * dd)
{
    return(dd->maxCacheHard);

} /* end of Cudd_ReadMaxCache */


/**Function********************************************************************

  Synopsis    [Sets the maxCacheHard parameter of the manager.]

  Description [Sets the maxCacheHard parameter of the manager. The
  cache cannot grow larger than maxCacheHard entries. This parameter
  allows an application to control the trade-off of memory versus
  speed. If the value passed to this function is 0, the function
  determines a suitable maximum cache size based on the available memory.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadMaxCacheHard Cudd_SetMaxCache]

******************************************************************************/
void
Cudd_SetMaxCacheHard(
  DdManager * dd,
  unsigned int mc)
{
    if (mc == 0) {
1420 1421 1422
        unsigned long datalimit = getSoftDataLimit();
        mc = (unsigned int) (datalimit / (sizeof(DdCache) *
                                          DD_MAX_CACHE_FRACTION));
Alan Mishchenko committed
1423 1424 1425 1426 1427 1428 1429 1430 1431 1432 1433 1434 1435 1436 1437 1438 1439 1440 1441 1442 1443 1444 1445 1446 1447 1448 1449 1450 1451 1452 1453 1454 1455 1456 1457 1458 1459 1460 1461 1462 1463 1464 1465 1466 1467 1468 1469 1470 1471 1472 1473 1474 1475 1476 1477 1478 1479 1480 1481 1482 1483 1484 1485 1486 1487 1488 1489 1490 1491 1492 1493 1494 1495 1496 1497 1498 1499 1500 1501 1502 1503 1504 1505 1506 1507 1508 1509 1510 1511 1512 1513 1514 1515
    }
    dd->maxCacheHard = mc;

} /* end of Cudd_SetMaxCacheHard */


/**Function********************************************************************

  Synopsis    [Returns the number of BDD variables in existance.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_ReadZddSize]

******************************************************************************/
int
Cudd_ReadSize(
  DdManager * dd)
{
    return(dd->size);

} /* end of Cudd_ReadSize */


/**Function********************************************************************

  Synopsis    [Returns the number of ZDD variables in existance.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_ReadSize]

******************************************************************************/
int
Cudd_ReadZddSize(
  DdManager * dd)
{
    return(dd->sizeZ);

} /* end of Cudd_ReadZddSize */


/**Function********************************************************************

  Synopsis    [Returns the total number of slots of the unique table.]

  Description [Returns the total number of slots of the unique table.
  This number ismainly for diagnostic purposes.]

  SideEffects [None]

******************************************************************************/
unsigned int
Cudd_ReadSlots(
  DdManager * dd)
{
    return(dd->slots);

} /* end of Cudd_ReadSlots */


/**Function********************************************************************

  Synopsis    [Reads the fraction of used slots in the unique table.]

  Description [Reads the fraction of used slots in the unique
  table. The unused slots are those in which no valid data is
  stored. Garbage collection, variable reordering, and subtable
  resizing may cause used slots to become unused.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadSlots]

******************************************************************************/
double
Cudd_ReadUsedSlots(
  DdManager * dd)
{
    unsigned long used = 0;
    int i, j;
    int size = dd->size;
    DdNodePtr *nodelist;
    DdSubtable *subtable;
    DdNode *node;
    DdNode *sentinel = &(dd->sentinel);

    /* Scan each BDD/ADD subtable. */
    for (i = 0; i < size; i++) {
1516 1517 1518 1519 1520 1521 1522
        subtable = &(dd->subtables[i]);
        nodelist = subtable->nodelist;
        for (j = 0; (unsigned) j < subtable->slots; j++) {
            node = nodelist[j];
            if (node != sentinel) {
                used++;
            }
Alan Mishchenko committed
1523 1524 1525 1526 1527 1528 1529
        }
    }

    /* Scan the ZDD subtables. */
    size = dd->sizeZ;

    for (i = 0; i < size; i++) {
1530 1531 1532 1533 1534 1535 1536
        subtable = &(dd->subtableZ[i]);
        nodelist = subtable->nodelist;
        for (j = 0; (unsigned) j < subtable->slots; j++) {
            node = nodelist[j];
            if (node != NULL) {
                used++;
            }
Alan Mishchenko committed
1537 1538 1539 1540 1541 1542 1543
        }
    }

    /* Constant table. */
    subtable = &(dd->constants);
    nodelist = subtable->nodelist;
    for (j = 0; (unsigned) j < subtable->slots; j++) {
1544 1545 1546 1547
        node = nodelist[j];
        if (node != NULL) {
            used++;
        }
Alan Mishchenko committed
1548 1549 1550 1551 1552 1553 1554 1555 1556 1557 1558 1559 1560 1561 1562 1563 1564 1565 1566 1567 1568 1569 1570 1571 1572 1573 1574 1575 1576 1577 1578 1579 1580 1581
    }

    return((double)used / (double) dd->slots);

} /* end of Cudd_ReadUsedSlots */


/**Function********************************************************************

  Synopsis    [Computes the expected fraction of used slots in the unique
  table.]

  Description [Computes the fraction of slots in the unique table that
  should be in use. This expected value is based on the assumption
  that the hash function distributes the keys randomly; it can be
  compared with the result of Cudd_ReadUsedSlots to monitor the
  performance of the unique table hash function.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadSlots Cudd_ReadUsedSlots]

******************************************************************************/
double
Cudd_ExpectedUsedSlots(
  DdManager * dd)
{
    int i;
    int size = dd->size;
    DdSubtable *subtable;
    double empty = 0.0;

    /* To each subtable we apply the corollary to Theorem 8.5 (occupancy
    ** distribution) from Sedgewick and Flajolet's Analysis of Algorithms.
1582
    ** The corollary says that for a table with M buckets and a load ratio
Alan Mishchenko committed
1583 1584 1585 1586 1587 1588
    ** of r, the expected number of empty buckets is asymptotically given
    ** by M * exp(-r).
    */

    /* Scan each BDD/ADD subtable. */
    for (i = 0; i < size; i++) {
1589 1590 1591
        subtable = &(dd->subtables[i]);
        empty += (double) subtable->slots *
            exp(-(double) subtable->keys / (double) subtable->slots);
Alan Mishchenko committed
1592 1593 1594 1595 1596 1597
    }

    /* Scan the ZDD subtables. */
    size = dd->sizeZ;

    for (i = 0; i < size; i++) {
1598 1599 1600
        subtable = &(dd->subtableZ[i]);
        empty += (double) subtable->slots *
            exp(-(double) subtable->keys / (double) subtable->slots);
Alan Mishchenko committed
1601 1602 1603 1604 1605
    }

    /* Constant table. */
    subtable = &(dd->constants);
    empty += (double) subtable->slots *
1606
        exp(-(double) subtable->keys / (double) subtable->slots);
Alan Mishchenko committed
1607 1608 1609 1610 1611 1612 1613 1614 1615 1616 1617 1618 1619 1620 1621 1622 1623 1624 1625 1626 1627 1628 1629 1630 1631 1632 1633 1634 1635 1636 1637 1638 1639 1640 1641 1642 1643 1644 1645 1646 1647 1648 1649 1650 1651 1652 1653 1654 1655 1656 1657 1658 1659 1660 1661 1662 1663 1664 1665 1666 1667 1668 1669 1670 1671 1672 1673 1674 1675 1676 1677 1678 1679 1680 1681 1682 1683 1684 1685 1686 1687 1688 1689 1690 1691 1692 1693 1694 1695 1696 1697 1698 1699 1700 1701 1702 1703 1704 1705 1706 1707 1708 1709 1710 1711 1712 1713 1714 1715 1716 1717 1718 1719 1720 1721 1722 1723 1724 1725 1726 1727 1728 1729 1730 1731 1732 1733 1734 1735 1736 1737 1738 1739 1740 1741 1742 1743 1744 1745 1746 1747 1748 1749 1750 1751 1752 1753 1754 1755 1756 1757 1758 1759 1760 1761 1762 1763 1764 1765 1766 1767 1768 1769 1770 1771 1772 1773

    return(1.0 - empty / (double) dd->slots);

} /* end of Cudd_ExpectedUsedSlots */


/**Function********************************************************************

  Synopsis    [Returns the number of nodes in the unique table.]

  Description [Returns the total number of nodes currently in the unique
  table, including the dead nodes.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadDead]

******************************************************************************/
unsigned int
Cudd_ReadKeys(
  DdManager * dd)
{
    return(dd->keys);

} /* end of Cudd_ReadKeys */


/**Function********************************************************************

  Synopsis    [Returns the number of dead nodes in the unique table.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_ReadKeys]

******************************************************************************/
unsigned int
Cudd_ReadDead(
  DdManager * dd)
{
    return(dd->dead);

} /* end of Cudd_ReadDead */


/**Function********************************************************************

  Synopsis    [Reads the minDead parameter of the manager.]

  Description [Reads the minDead parameter of the manager. The minDead
  parameter is used by the package to decide whether to collect garbage
  or resize a subtable of the unique table when the subtable becomes
  too full. The application can indirectly control the value of minDead
  by setting the looseUpTo parameter.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadDead Cudd_ReadLooseUpTo Cudd_SetLooseUpTo]

******************************************************************************/
unsigned int
Cudd_ReadMinDead(
  DdManager * dd)
{
    return(dd->minDead);

} /* end of Cudd_ReadMinDead */


/**Function********************************************************************

  Synopsis    [Returns the number of times reordering has occurred.]

  Description [Returns the number of times reordering has occurred in the
  manager. The number includes both the calls to Cudd_ReduceHeap from
  the application program and those automatically performed by the
  package. However, calls that do not even initiate reordering are not
  counted. A call may not initiate reordering if there are fewer than
  minsize live nodes in the manager, or if CUDD_REORDER_NONE is specified
  as reordering method. The calls to Cudd_ShuffleHeap are not counted.]

  SideEffects [None]

  SeeAlso [Cudd_ReduceHeap Cudd_ReadReorderingTime]

******************************************************************************/
int
Cudd_ReadReorderings(
  DdManager * dd)
{
    return(dd->reorderings);

} /* end of Cudd_ReadReorderings */


/**Function********************************************************************

  Synopsis    [Returns the time spent in reordering.]

  Description [Returns the number of milliseconds spent reordering
  variables since the manager was initialized. The time spent in collecting
  garbage before reordering is included.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadReorderings]

******************************************************************************/
long
Cudd_ReadReorderingTime(
  DdManager * dd)
{
    return(dd->reordTime);

} /* end of Cudd_ReadReorderingTime */


/**Function********************************************************************

  Synopsis    [Returns the number of times garbage collection has occurred.]

  Description [Returns the number of times garbage collection has
  occurred in the manager. The number includes both the calls from
  reordering procedures and those caused by requests to create new
  nodes.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadGarbageCollectionTime]

******************************************************************************/
int
Cudd_ReadGarbageCollections(
  DdManager * dd)
{
    return(dd->garbageCollections);

} /* end of Cudd_ReadGarbageCollections */


/**Function********************************************************************

  Synopsis    [Returns the time spent in garbage collection.]

  Description [Returns the number of milliseconds spent doing garbage
  collection since the manager was initialized.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadGarbageCollections]

******************************************************************************/
long
Cudd_ReadGarbageCollectionTime(
  DdManager * dd)
{
    return(dd->GCTime);

} /* end of Cudd_ReadGarbageCollectionTime */


/**Function********************************************************************

  Synopsis    [Returns the number of nodes freed.]

1774
  Description [Returns the number of nodes returned to the free list if the
Alan Mishchenko committed
1775 1776 1777 1778 1779 1780 1781 1782 1783 1784 1785 1786 1787 1788 1789 1790 1791 1792 1793 1794 1795 1796 1797 1798 1799 1800 1801 1802 1803 1804 1805 1806 1807 1808 1809 1810 1811 1812 1813 1814 1815 1816 1817 1818 1819 1820 1821 1822 1823 1824 1825 1826 1827 1828 1829 1830 1831 1832 1833 1834 1835 1836 1837 1838 1839 1840 1841 1842 1843 1844 1845 1846 1847 1848 1849 1850 1851 1852 1853 1854 1855 1856 1857 1858 1859 1860 1861 1862 1863 1864 1865 1866 1867 1868 1869 1870 1871 1872 1873 1874 1875 1876 1877 1878 1879 1880 1881 1882 1883 1884 1885 1886 1887 1888 1889 1890 1891 1892 1893 1894 1895 1896 1897 1898 1899 1900 1901 1902 1903 1904 1905 1906 1907 1908 1909 1910 1911 1912 1913 1914 1915 1916 1917 1918 1919 1920 1921 1922 1923 1924 1925 1926 1927 1928 1929 1930 1931 1932 1933 1934 1935 1936 1937 1938 1939 1940 1941 1942 1943 1944 1945 1946 1947 1948 1949 1950 1951 1952 1953 1954 1955 1956 1957 1958 1959 1960 1961 1962 1963 1964 1965 1966 1967 1968 1969 1970 1971 1972 1973 1974 1975 1976 1977 1978 1979 1980 1981 1982 1983 1984 1985 1986 1987 1988 1989 1990 1991 1992 1993 1994 1995 1996 1997 1998 1999 2000 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018 2019 2020 2021 2022 2023 2024 2025 2026 2027 2028 2029 2030 2031 2032 2033 2034 2035 2036 2037 2038 2039 2040 2041 2042 2043 2044 2045 2046 2047 2048 2049 2050 2051 2052 2053 2054 2055 2056 2057 2058 2059 2060 2061 2062 2063 2064 2065 2066 2067 2068 2069 2070 2071 2072 2073 2074 2075 2076 2077 2078 2079 2080 2081 2082 2083 2084 2085 2086 2087 2088 2089 2090 2091 2092 2093 2094 2095 2096 2097 2098 2099 2100 2101 2102 2103 2104 2105 2106 2107 2108 2109 2110 2111 2112 2113 2114 2115 2116 2117 2118 2119 2120 2121 2122 2123 2124 2125 2126 2127 2128 2129 2130 2131 2132 2133 2134 2135 2136 2137 2138 2139 2140 2141 2142 2143 2144 2145 2146 2147 2148 2149 2150 2151 2152 2153 2154 2155 2156
  keeping of this statistic is enabled; -1 otherwise. This statistic is
  enabled only if the package is compiled with DD_STATS defined.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadNodesDropped]

******************************************************************************/
double
Cudd_ReadNodesFreed(
  DdManager * dd)
{
#ifdef DD_STATS
    return(dd->nodesFreed);
#else
    return(-1.0);
#endif

} /* end of Cudd_ReadNodesFreed */


/**Function********************************************************************

  Synopsis    [Returns the number of nodes dropped.]

  Description [Returns the number of nodes killed by dereferencing if the
  keeping of this statistic is enabled; -1 otherwise. This statistic is
  enabled only if the package is compiled with DD_STATS defined.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadNodesFreed]

******************************************************************************/
double
Cudd_ReadNodesDropped(
  DdManager * dd)
{
#ifdef DD_STATS
    return(dd->nodesDropped);
#else
    return(-1.0);
#endif

} /* end of Cudd_ReadNodesDropped */


/**Function********************************************************************

  Synopsis    [Returns the number of look-ups in the unique table.]

  Description [Returns the number of look-ups in the unique table if the
  keeping of this statistic is enabled; -1 otherwise. This statistic is
  enabled only if the package is compiled with DD_UNIQUE_PROFILE defined.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadUniqueLinks]

******************************************************************************/
double
Cudd_ReadUniqueLookUps(
  DdManager * dd)
{
#ifdef DD_UNIQUE_PROFILE
    return(dd->uniqueLookUps);
#else
    return(-1.0);
#endif

} /* end of Cudd_ReadUniqueLookUps */


/**Function********************************************************************

  Synopsis    [Returns the number of links followed in the unique table.]

  Description [Returns the number of links followed during look-ups in the
  unique table if the keeping of this statistic is enabled; -1 otherwise.
  If an item is found in the first position of its collision list, the
  number of links followed is taken to be 0. If it is in second position,
  the number of links is 1, and so on. This statistic is enabled only if
  the package is compiled with DD_UNIQUE_PROFILE defined.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadUniqueLookUps]

******************************************************************************/
double
Cudd_ReadUniqueLinks(
  DdManager * dd)
{
#ifdef DD_UNIQUE_PROFILE
    return(dd->uniqueLinks);
#else
    return(-1.0);
#endif

} /* end of Cudd_ReadUniqueLinks */


/**Function********************************************************************

  Synopsis    [Reads the siftMaxVar parameter of the manager.]

  Description [Reads the siftMaxVar parameter of the manager. This
  parameter gives the maximum number of variables that will be sifted
  for each invocation of sifting.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadSiftMaxSwap Cudd_SetSiftMaxVar]

******************************************************************************/
int
Cudd_ReadSiftMaxVar(
  DdManager * dd)
{
    return(dd->siftMaxVar);

} /* end of Cudd_ReadSiftMaxVar */


/**Function********************************************************************

  Synopsis    [Sets the siftMaxVar parameter of the manager.]

  Description [Sets the siftMaxVar parameter of the manager. This
  parameter gives the maximum number of variables that will be sifted
  for each invocation of sifting.]

  SideEffects [None]

  SeeAlso     [Cudd_SetSiftMaxSwap Cudd_ReadSiftMaxVar]

******************************************************************************/
void
Cudd_SetSiftMaxVar(
  DdManager * dd,
  int  smv)
{
    dd->siftMaxVar = smv;

} /* end of Cudd_SetSiftMaxVar */


/**Function********************************************************************

  Synopsis    [Reads the siftMaxSwap parameter of the manager.]

  Description [Reads the siftMaxSwap parameter of the manager. This
  parameter gives the maximum number of swaps that will be attempted
  for each invocation of sifting. The real number of swaps may exceed
  the set limit because the package will always complete the sifting
  of the variable that causes the limit to be reached.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadSiftMaxVar Cudd_SetSiftMaxSwap]

******************************************************************************/
int
Cudd_ReadSiftMaxSwap(
  DdManager * dd)
{
    return(dd->siftMaxSwap);

} /* end of Cudd_ReadSiftMaxSwap */


/**Function********************************************************************

  Synopsis    [Sets the siftMaxSwap parameter of the manager.]

  Description [Sets the siftMaxSwap parameter of the manager. This
  parameter gives the maximum number of swaps that will be attempted
  for each invocation of sifting. The real number of swaps may exceed
  the set limit because the package will always complete the sifting
  of the variable that causes the limit to be reached.]

  SideEffects [None]

  SeeAlso     [Cudd_SetSiftMaxVar Cudd_ReadSiftMaxSwap]

******************************************************************************/
void
Cudd_SetSiftMaxSwap(
  DdManager * dd,
  int  sms)
{
    dd->siftMaxSwap = sms;

} /* end of Cudd_SetSiftMaxSwap */


/**Function********************************************************************

  Synopsis    [Reads the maxGrowth parameter of the manager.]

  Description [Reads the maxGrowth parameter of the manager.  This
  parameter determines how much the number of nodes can grow during
  sifting of a variable.  Overall, sifting never increases the size of
  the decision diagrams.  This parameter only refers to intermediate
  results.  A lower value will speed up sifting, possibly at the
  expense of quality.]

  SideEffects [None]

  SeeAlso     [Cudd_SetMaxGrowth Cudd_ReadMaxGrowthAlternate]

******************************************************************************/
double
Cudd_ReadMaxGrowth(
  DdManager * dd)
{
    return(dd->maxGrowth);

} /* end of Cudd_ReadMaxGrowth */


/**Function********************************************************************

  Synopsis    [Sets the maxGrowth parameter of the manager.]

  Description [Sets the maxGrowth parameter of the manager.  This
  parameter determines how much the number of nodes can grow during
  sifting of a variable.  Overall, sifting never increases the size of
  the decision diagrams.  This parameter only refers to intermediate
  results.  A lower value will speed up sifting, possibly at the
  expense of quality.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadMaxGrowth Cudd_SetMaxGrowthAlternate]

******************************************************************************/
void
Cudd_SetMaxGrowth(
  DdManager * dd,
  double mg)
{
    dd->maxGrowth = mg;

} /* end of Cudd_SetMaxGrowth */


/**Function********************************************************************

  Synopsis    [Reads the maxGrowthAlt parameter of the manager.]

  Description [Reads the maxGrowthAlt parameter of the manager.  This
  parameter is analogous to the maxGrowth paramter, and is used every
  given number of reorderings instead of maxGrowth.  The number of
  reorderings is set with Cudd_SetReorderingCycle.  If the number of
  reorderings is 0 (default) maxGrowthAlt is never used.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadMaxGrowth Cudd_SetMaxGrowthAlternate
  Cudd_SetReorderingCycle Cudd_ReadReorderingCycle]

******************************************************************************/
double
Cudd_ReadMaxGrowthAlternate(
  DdManager * dd)
{
    return(dd->maxGrowthAlt);

} /* end of Cudd_ReadMaxGrowthAlternate */


/**Function********************************************************************

  Synopsis    [Sets the maxGrowthAlt parameter of the manager.]

  Description [Sets the maxGrowthAlt parameter of the manager.  This
  parameter is analogous to the maxGrowth paramter, and is used every
  given number of reorderings instead of maxGrowth.  The number of
  reorderings is set with Cudd_SetReorderingCycle.  If the number of
  reorderings is 0 (default) maxGrowthAlt is never used.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowth
  Cudd_SetReorderingCycle Cudd_ReadReorderingCycle]

******************************************************************************/
void
Cudd_SetMaxGrowthAlternate(
  DdManager * dd,
  double mg)
{
    dd->maxGrowthAlt = mg;

} /* end of Cudd_SetMaxGrowthAlternate */


/**Function********************************************************************

  Synopsis    [Reads the reordCycle parameter of the manager.]

  Description [Reads the reordCycle parameter of the manager.  This
  parameter determines how often the alternate threshold on maximum
  growth is used in reordering.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowthAlternate
  Cudd_SetReorderingCycle]

******************************************************************************/
int
Cudd_ReadReorderingCycle(
  DdManager * dd)
{
    return(dd->reordCycle);

} /* end of Cudd_ReadReorderingCycle */


/**Function********************************************************************

  Synopsis    [Sets the reordCycle parameter of the manager.]

  Description [Sets the reordCycle parameter of the manager.  This
  parameter determines how often the alternate threshold on maximum
  growth is used in reordering.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowthAlternate
  Cudd_ReadReorderingCycle]

******************************************************************************/
void
Cudd_SetReorderingCycle(
  DdManager * dd,
  int cycle)
{
    dd->reordCycle = cycle;

} /* end of Cudd_SetReorderingCycle */


/**Function********************************************************************

  Synopsis    [Returns the variable group tree of the manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_SetTree Cudd_FreeTree Cudd_ReadZddTree]

******************************************************************************/
MtrNode *
Cudd_ReadTree(
  DdManager * dd)
{
    return(dd->tree);

} /* end of Cudd_ReadTree */


/**Function********************************************************************

  Synopsis    [Sets the variable group tree of the manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_FreeTree Cudd_ReadTree Cudd_SetZddTree]

******************************************************************************/
void
Cudd_SetTree(
  DdManager * dd,
  MtrNode * tree)
{
    if (dd->tree != NULL) {
2157
        Mtr_FreeTree(dd->tree);
Alan Mishchenko committed
2158 2159 2160 2161 2162 2163 2164 2165 2166 2167 2168 2169 2170 2171 2172 2173 2174 2175 2176 2177 2178 2179 2180 2181 2182 2183
    }
    dd->tree = tree;
    if (tree == NULL) return;

    fixVarTree(tree, dd->perm, dd->size);
    return;

} /* end of Cudd_SetTree */


/**Function********************************************************************

  Synopsis    [Frees the variable group tree of the manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_SetTree Cudd_ReadTree Cudd_FreeZddTree]

******************************************************************************/
void
Cudd_FreeTree(
  DdManager * dd)
{
    if (dd->tree != NULL) {
2184 2185
        Mtr_FreeTree(dd->tree);
        dd->tree = NULL;
Alan Mishchenko committed
2186 2187 2188 2189 2190 2191 2192 2193 2194 2195 2196 2197 2198 2199 2200 2201 2202 2203 2204 2205 2206 2207 2208 2209 2210 2211 2212 2213 2214 2215 2216 2217 2218 2219 2220 2221 2222 2223 2224 2225 2226 2227 2228
    }
    return;

} /* end of Cudd_FreeTree */


/**Function********************************************************************

  Synopsis    [Returns the variable group tree of the manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_SetZddTree Cudd_FreeZddTree Cudd_ReadTree]

******************************************************************************/
MtrNode *
Cudd_ReadZddTree(
  DdManager * dd)
{
    return(dd->treeZ);

} /* end of Cudd_ReadZddTree */


/**Function********************************************************************

  Synopsis    [Sets the ZDD variable group tree of the manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_FreeZddTree Cudd_ReadZddTree Cudd_SetTree]

******************************************************************************/
void
Cudd_SetZddTree(
  DdManager * dd,
  MtrNode * tree)
{
    if (dd->treeZ != NULL) {
2229
        Mtr_FreeTree(dd->treeZ);
Alan Mishchenko committed
2230 2231 2232 2233 2234 2235 2236 2237 2238 2239 2240 2241 2242 2243 2244 2245 2246 2247 2248 2249 2250 2251 2252 2253 2254 2255
    }
    dd->treeZ = tree;
    if (tree == NULL) return;

    fixVarTree(tree, dd->permZ, dd->sizeZ);
    return;

} /* end of Cudd_SetZddTree */


/**Function********************************************************************

  Synopsis    [Frees the variable group tree of the manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_SetZddTree Cudd_ReadZddTree Cudd_FreeTree]

******************************************************************************/
void
Cudd_FreeZddTree(
  DdManager * dd)
{
    if (dd->treeZ != NULL) {
2256 2257
        Mtr_FreeTree(dd->treeZ);
        dd->treeZ = NULL;
Alan Mishchenko committed
2258 2259 2260 2261 2262 2263 2264 2265 2266 2267 2268 2269 2270 2271 2272 2273 2274 2275 2276 2277 2278 2279 2280 2281 2282 2283 2284 2285 2286 2287 2288 2289 2290 2291 2292 2293 2294 2295 2296 2297 2298 2299 2300 2301 2302 2303 2304 2305 2306 2307 2308 2309 2310 2311 2312 2313 2314 2315 2316 2317 2318 2319 2320 2321 2322 2323 2324 2325 2326 2327 2328 2329 2330 2331 2332 2333 2334 2335 2336 2337 2338 2339 2340 2341 2342 2343 2344 2345 2346 2347 2348 2349 2350 2351 2352 2353 2354 2355 2356 2357 2358 2359 2360 2361 2362 2363 2364 2365 2366 2367 2368 2369 2370 2371 2372 2373 2374 2375 2376 2377 2378 2379 2380 2381 2382 2383 2384 2385 2386 2387 2388 2389 2390 2391 2392 2393 2394 2395 2396 2397 2398 2399 2400 2401 2402 2403 2404 2405 2406 2407 2408 2409 2410 2411 2412 2413 2414 2415 2416 2417 2418 2419 2420 2421 2422 2423 2424 2425 2426 2427 2428 2429 2430 2431 2432 2433 2434 2435 2436 2437 2438 2439 2440 2441 2442 2443 2444 2445 2446 2447 2448 2449 2450 2451 2452 2453 2454 2455 2456 2457 2458 2459 2460 2461 2462 2463 2464 2465 2466 2467 2468 2469 2470 2471 2472 2473 2474 2475 2476 2477 2478 2479 2480 2481 2482 2483 2484 2485 2486 2487 2488 2489 2490 2491 2492 2493 2494 2495 2496 2497 2498 2499 2500 2501 2502 2503 2504 2505 2506 2507 2508 2509 2510 2511 2512 2513 2514 2515 2516 2517 2518 2519 2520 2521 2522 2523 2524 2525 2526 2527 2528 2529 2530 2531 2532 2533 2534 2535 2536 2537 2538 2539 2540 2541 2542 2543 2544 2545 2546 2547 2548 2549 2550 2551 2552 2553 2554 2555 2556 2557 2558 2559 2560 2561 2562 2563 2564 2565 2566 2567 2568 2569 2570 2571 2572 2573 2574 2575 2576 2577 2578 2579 2580 2581 2582 2583 2584 2585 2586 2587 2588 2589 2590 2591 2592 2593 2594 2595 2596 2597 2598 2599 2600 2601 2602 2603 2604 2605 2606 2607 2608 2609 2610 2611 2612 2613 2614 2615 2616 2617 2618 2619 2620 2621 2622 2623 2624 2625 2626 2627 2628 2629 2630 2631 2632 2633 2634 2635 2636 2637 2638 2639 2640 2641 2642 2643 2644 2645 2646 2647 2648 2649 2650 2651 2652 2653 2654 2655 2656 2657 2658 2659 2660 2661 2662 2663 2664 2665 2666 2667 2668 2669 2670 2671 2672 2673 2674 2675 2676 2677 2678 2679 2680 2681 2682 2683 2684 2685 2686 2687 2688 2689 2690 2691 2692 2693 2694 2695 2696 2697 2698 2699 2700 2701 2702 2703 2704 2705 2706 2707 2708 2709 2710 2711 2712 2713 2714 2715 2716 2717 2718 2719 2720 2721 2722 2723 2724 2725 2726 2727 2728 2729 2730 2731 2732 2733 2734 2735 2736 2737 2738 2739 2740 2741 2742 2743 2744 2745 2746 2747 2748 2749 2750 2751 2752 2753 2754 2755 2756 2757 2758 2759 2760 2761 2762 2763 2764 2765 2766 2767 2768 2769 2770 2771 2772 2773 2774 2775 2776 2777 2778 2779 2780 2781 2782 2783 2784 2785 2786 2787 2788 2789 2790 2791 2792 2793 2794 2795 2796 2797 2798 2799 2800 2801 2802 2803 2804 2805 2806 2807 2808 2809 2810 2811 2812 2813 2814 2815 2816 2817 2818 2819 2820 2821 2822 2823 2824 2825 2826 2827 2828 2829 2830 2831 2832 2833 2834 2835 2836 2837 2838 2839 2840 2841 2842 2843 2844 2845 2846 2847 2848 2849 2850 2851 2852 2853 2854 2855 2856 2857 2858 2859 2860 2861 2862 2863 2864 2865 2866 2867 2868 2869 2870 2871 2872 2873 2874 2875 2876 2877 2878 2879 2880 2881 2882 2883 2884 2885 2886 2887 2888 2889 2890 2891 2892 2893 2894 2895 2896 2897 2898 2899 2900 2901 2902 2903 2904 2905 2906 2907 2908 2909 2910 2911 2912 2913 2914
    }
    return;

} /* end of Cudd_FreeZddTree */


/**Function********************************************************************

  Synopsis    [Returns the index of the node.]

  Description [Returns the index of the node. The node pointer can be
  either regular or complemented.]

  SideEffects [None]

  SeeAlso [Cudd_ReadIndex]

******************************************************************************/
unsigned int
Cudd_NodeReadIndex(
  DdNode * node)
{
    return((unsigned int) Cudd_Regular(node)->index);

} /* end of Cudd_NodeReadIndex */


/**Function********************************************************************

  Synopsis    [Returns the current position of the i-th variable in the
  order.]

  Description [Returns the current position of the i-th variable in
  the order. If the index is CUDD_CONST_INDEX, returns
  CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns
  -1.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadInvPerm Cudd_ReadPermZdd]

******************************************************************************/
int
Cudd_ReadPerm(
  DdManager * dd,
  int  i)
{
    if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
    if (i < 0 || i >= dd->size) return(-1);
    return(dd->perm[i]);

} /* end of Cudd_ReadPerm */


/**Function********************************************************************

  Synopsis    [Returns the current position of the i-th ZDD variable in the
  order.]

  Description [Returns the current position of the i-th ZDD variable
  in the order. If the index is CUDD_CONST_INDEX, returns
  CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns
  -1.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadInvPermZdd Cudd_ReadPerm]

******************************************************************************/
int
Cudd_ReadPermZdd(
  DdManager * dd,
  int  i)
{
    if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
    if (i < 0 || i >= dd->sizeZ) return(-1);
    return(dd->permZ[i]);

} /* end of Cudd_ReadPermZdd */


/**Function********************************************************************

  Synopsis    [Returns the index of the variable currently in the i-th
  position of the order.]

  Description [Returns the index of the variable currently in the i-th
  position of the order. If the index is CUDD_CONST_INDEX, returns
  CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadPerm Cudd_ReadInvPermZdd]

******************************************************************************/
int
Cudd_ReadInvPerm(
  DdManager * dd,
  int  i)
{
    if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
    if (i < 0 || i >= dd->size) return(-1);
    return(dd->invperm[i]);

} /* end of Cudd_ReadInvPerm */


/**Function********************************************************************

  Synopsis    [Returns the index of the ZDD variable currently in the i-th
  position of the order.]

  Description [Returns the index of the ZDD variable currently in the
  i-th position of the order. If the index is CUDD_CONST_INDEX, returns
  CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadPerm Cudd_ReadInvPermZdd]

******************************************************************************/
int
Cudd_ReadInvPermZdd(
  DdManager * dd,
  int  i)
{
    if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
    if (i < 0 || i >= dd->sizeZ) return(-1);
    return(dd->invpermZ[i]);

} /* end of Cudd_ReadInvPermZdd */


/**Function********************************************************************

  Synopsis    [Returns the i-th element of the vars array.]

  Description [Returns the i-th element of the vars array if it falls
  within the array bounds; NULL otherwise. If i is the index of an
  existing variable, this function produces the same result as
  Cudd_bddIthVar. However, if the i-th var does not exist yet,
  Cudd_bddIthVar will create it, whereas Cudd_ReadVars will not.]

  SideEffects [None]

  SeeAlso     [Cudd_bddIthVar]

******************************************************************************/
DdNode *
Cudd_ReadVars(
  DdManager * dd,
  int  i)
{
    if (i < 0 || i > dd->size) return(NULL);
    return(dd->vars[i]);

} /* end of Cudd_ReadVars */


/**Function********************************************************************

  Synopsis    [Reads the epsilon parameter of the manager.]

  Description [Reads the epsilon parameter of the manager. The epsilon
  parameter control the comparison between floating point numbers.]

  SideEffects [None]

  SeeAlso     [Cudd_SetEpsilon]

******************************************************************************/
CUDD_VALUE_TYPE
Cudd_ReadEpsilon(
  DdManager * dd)
{
    return(dd->epsilon);

} /* end of Cudd_ReadEpsilon */


/**Function********************************************************************

  Synopsis    [Sets the epsilon parameter of the manager to ep.]

  Description [Sets the epsilon parameter of the manager to ep. The epsilon
  parameter control the comparison between floating point numbers.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadEpsilon]

******************************************************************************/
void
Cudd_SetEpsilon(
  DdManager * dd,
  CUDD_VALUE_TYPE  ep)
{
    dd->epsilon = ep;

} /* end of Cudd_SetEpsilon */


/**Function********************************************************************

  Synopsis    [Reads the groupcheck parameter of the manager.]

  Description [Reads the groupcheck parameter of the manager. The
  groupcheck parameter determines the aggregation criterion in group
  sifting.]

  SideEffects [None]

  SeeAlso     [Cudd_SetGroupcheck]

******************************************************************************/
Cudd_AggregationType
Cudd_ReadGroupcheck(
  DdManager * dd)
{
    return(dd->groupcheck);

} /* end of Cudd_ReadGroupCheck */


/**Function********************************************************************

  Synopsis    [Sets the parameter groupcheck of the manager to gc.]

  Description [Sets the parameter groupcheck of the manager to gc. The
  groupcheck parameter determines the aggregation criterion in group
  sifting.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadGroupCheck]

******************************************************************************/
void
Cudd_SetGroupcheck(
  DdManager * dd,
  Cudd_AggregationType gc)
{
    dd->groupcheck = gc;

} /* end of Cudd_SetGroupcheck */


/**Function********************************************************************

  Synopsis    [Tells whether garbage collection is enabled.]

  Description [Returns 1 if garbage collection is enabled; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_EnableGarbageCollection Cudd_DisableGarbageCollection]

******************************************************************************/
int
Cudd_GarbageCollectionEnabled(
  DdManager * dd)
{
    return(dd->gcEnabled);

} /* end of Cudd_GarbageCollectionEnabled */


/**Function********************************************************************

  Synopsis    [Enables garbage collection.]

  Description [Enables garbage collection. Garbage collection is
  initially enabled. Therefore it is necessary to call this function
  only if garbage collection has been explicitly disabled.]

  SideEffects [None]

  SeeAlso     [Cudd_DisableGarbageCollection Cudd_GarbageCollectionEnabled]

******************************************************************************/
void
Cudd_EnableGarbageCollection(
  DdManager * dd)
{
    dd->gcEnabled = 1;

} /* end of Cudd_EnableGarbageCollection */


/**Function********************************************************************

  Synopsis    [Disables garbage collection.]

  Description [Disables garbage collection. Garbage collection is
  initially enabled. This function may be called to disable it.
  However, garbage collection will still occur when a new node must be
  created and no memory is left, or when garbage collection is required
  for correctness. (E.g., before reordering.)]

  SideEffects [None]

  SeeAlso     [Cudd_EnableGarbageCollection Cudd_GarbageCollectionEnabled]

******************************************************************************/
void
Cudd_DisableGarbageCollection(
  DdManager * dd)
{
    dd->gcEnabled = 0;

} /* end of Cudd_DisableGarbageCollection */


/**Function********************************************************************

  Synopsis    [Tells whether dead nodes are counted towards triggering
  reordering.]

  Description [Tells whether dead nodes are counted towards triggering
  reordering. Returns 1 if dead nodes are counted; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_TurnOnCountDead Cudd_TurnOffCountDead]

******************************************************************************/
int
Cudd_DeadAreCounted(
  DdManager * dd)
{
    return(dd->countDead == 0 ? 1 : 0);

} /* end of Cudd_DeadAreCounted */


/**Function********************************************************************

  Synopsis    [Causes the dead nodes to be counted towards triggering
  reordering.]

  Description [Causes the dead nodes to be counted towards triggering
  reordering. This causes more frequent reorderings. By default dead
  nodes are not counted.]

  SideEffects [Changes the manager.]

  SeeAlso     [Cudd_TurnOffCountDead Cudd_DeadAreCounted]

******************************************************************************/
void
Cudd_TurnOnCountDead(
  DdManager * dd)
{
    dd->countDead = 0;

} /* end of Cudd_TurnOnCountDead */


/**Function********************************************************************

  Synopsis    [Causes the dead nodes not to be counted towards triggering
  reordering.]

  Description [Causes the dead nodes not to be counted towards
  triggering reordering. This causes less frequent reorderings. By
  default dead nodes are not counted. Therefore there is no need to
  call this function unless Cudd_TurnOnCountDead has been previously
  called.]

  SideEffects [Changes the manager.]

  SeeAlso     [Cudd_TurnOnCountDead Cudd_DeadAreCounted]

******************************************************************************/
void
Cudd_TurnOffCountDead(
  DdManager * dd)
{
    dd->countDead = ~0;

} /* end of Cudd_TurnOffCountDead */


/**Function********************************************************************

  Synopsis    [Returns the current value of the recombination parameter used
  in group sifting.]

  Description [Returns the current value of the recombination
  parameter used in group sifting. A larger (positive) value makes the
  aggregation of variables due to the second difference criterion more
  likely. A smaller (negative) value makes aggregation less likely.]

  SideEffects [None]

  SeeAlso     [Cudd_SetRecomb]

******************************************************************************/
int
Cudd_ReadRecomb(
  DdManager * dd)
{
    return(dd->recomb);

} /* end of Cudd_ReadRecomb */


/**Function********************************************************************

  Synopsis    [Sets the value of the recombination parameter used in group
  sifting.]

  Description [Sets the value of the recombination parameter used in
  group sifting. A larger (positive) value makes the aggregation of
  variables due to the second difference criterion more likely. A
  smaller (negative) value makes aggregation less likely. The default
  value is 0.]

  SideEffects [Changes the manager.]

  SeeAlso     [Cudd_ReadRecomb]

******************************************************************************/
void
Cudd_SetRecomb(
  DdManager * dd,
  int  recomb)
{
    dd->recomb = recomb;

} /* end of Cudd_SetRecomb */


/**Function********************************************************************

  Synopsis    [Returns the current value of the symmviolation parameter used
  in group sifting.]

  Description [Returns the current value of the symmviolation
  parameter. This parameter is used in group sifting to decide how
  many violations to the symmetry conditions <code>f10 = f01</code> or
  <code>f11 = f00</code> are tolerable when checking for aggregation
  due to extended symmetry. The value should be between 0 and 100. A
  small value causes fewer variables to be aggregated. The default
  value is 0.]

  SideEffects [None]

  SeeAlso     [Cudd_SetSymmviolation]

******************************************************************************/
int
Cudd_ReadSymmviolation(
  DdManager * dd)
{
    return(dd->symmviolation);

} /* end of Cudd_ReadSymmviolation */


/**Function********************************************************************

  Synopsis    [Sets the value of the symmviolation parameter used
  in group sifting.]

  Description [Sets the value of the symmviolation
  parameter. This parameter is used in group sifting to decide how
  many violations to the symmetry conditions <code>f10 = f01</code> or
  <code>f11 = f00</code> are tolerable when checking for aggregation
  due to extended symmetry. The value should be between 0 and 100. A
  small value causes fewer variables to be aggregated. The default
  value is 0.]

  SideEffects [Changes the manager.]

  SeeAlso     [Cudd_ReadSymmviolation]

******************************************************************************/
void
Cudd_SetSymmviolation(
  DdManager * dd,
  int  symmviolation)
{
    dd->symmviolation = symmviolation;

} /* end of Cudd_SetSymmviolation */


/**Function********************************************************************

  Synopsis    [Returns the current value of the arcviolation parameter used
  in group sifting.]

  Description [Returns the current value of the arcviolation
  parameter. This parameter is used in group sifting to decide how
  many arcs into <code>y</code> not coming from <code>x</code> are
  tolerable when checking for aggregation due to extended
  symmetry. The value should be between 0 and 100. A small value
  causes fewer variables to be aggregated. The default value is 0.]

  SideEffects [None]

  SeeAlso     [Cudd_SetArcviolation]

******************************************************************************/
int
Cudd_ReadArcviolation(
  DdManager * dd)
{
    return(dd->arcviolation);

} /* end of Cudd_ReadArcviolation */


/**Function********************************************************************

  Synopsis    [Sets the value of the arcviolation parameter used
  in group sifting.]

  Description [Sets the value of the arcviolation
  parameter. This parameter is used in group sifting to decide how
  many arcs into <code>y</code> not coming from <code>x</code> are
  tolerable when checking for aggregation due to extended
  symmetry. The value should be between 0 and 100. A small value
  causes fewer variables to be aggregated. The default value is 0.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadArcviolation]

******************************************************************************/
void
Cudd_SetArcviolation(
  DdManager * dd,
  int  arcviolation)
{
    dd->arcviolation = arcviolation;

} /* end of Cudd_SetArcviolation */


/**Function********************************************************************

  Synopsis    [Reads the current size of the population used by the
  genetic algorithm for reordering.]

  Description [Reads the current size of the population used by the
  genetic algorithm for variable reordering. A larger population size will
  cause the genetic algorithm to take more time, but will generally
  produce better results. The default value is 0, in which case the
  package uses three times the number of variables as population size,
  with a maximum of 120.]

  SideEffects [None]

  SeeAlso     [Cudd_SetPopulationSize]

******************************************************************************/
int
Cudd_ReadPopulationSize(
  DdManager * dd)
{
    return(dd->populationSize);

} /* end of Cudd_ReadPopulationSize */


/**Function********************************************************************

  Synopsis    [Sets the size of the population used by the
  genetic algorithm for reordering.]

  Description [Sets the size of the population used by the
  genetic algorithm for variable reordering. A larger population size will
  cause the genetic algorithm to take more time, but will generally
  produce better results. The default value is 0, in which case the
  package uses three times the number of variables as population size,
  with a maximum of 120.]

  SideEffects [Changes the manager.]

  SeeAlso     [Cudd_ReadPopulationSize]

******************************************************************************/
void
Cudd_SetPopulationSize(
  DdManager * dd,
  int  populationSize)
{
    dd->populationSize = populationSize;

} /* end of Cudd_SetPopulationSize */


/**Function********************************************************************

  Synopsis    [Reads the current number of crossovers used by the
  genetic algorithm for reordering.]

  Description [Reads the current number of crossovers used by the
  genetic algorithm for variable reordering. A larger number of crossovers will
  cause the genetic algorithm to take more time, but will generally
  produce better results. The default value is 0, in which case the
  package uses three times the number of variables as number of crossovers,
  with a maximum of 60.]

  SideEffects [None]

  SeeAlso     [Cudd_SetNumberXovers]

******************************************************************************/
int
Cudd_ReadNumberXovers(
  DdManager * dd)
{
    return(dd->numberXovers);

} /* end of Cudd_ReadNumberXovers */


/**Function********************************************************************

  Synopsis    [Sets the number of crossovers used by the
  genetic algorithm for reordering.]

  Description [Sets the number of crossovers used by the genetic
  algorithm for variable reordering. A larger number of crossovers
  will cause the genetic algorithm to take more time, but will
  generally produce better results. The default value is 0, in which
  case the package uses three times the number of variables as number
  of crossovers, with a maximum of 60.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadNumberXovers]

******************************************************************************/
void
Cudd_SetNumberXovers(
  DdManager * dd,
  int  numberXovers)
{
    dd->numberXovers = numberXovers;

} /* end of Cudd_SetNumberXovers */

/**Function********************************************************************

  Synopsis    [Returns the memory in use by the manager measured in bytes.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
2915
unsigned long
Alan Mishchenko committed
2916 2917 2918 2919 2920 2921 2922 2923 2924 2925 2926 2927 2928 2929 2930 2931 2932 2933 2934 2935 2936 2937 2938 2939 2940 2941 2942 2943 2944 2945 2946 2947
Cudd_ReadMemoryInUse(
  DdManager * dd)
{
    return(dd->memused);

} /* end of Cudd_ReadMemoryInUse */


/**Function********************************************************************

  Synopsis    [Prints out statistics and settings for a CUDD manager.]

  Description [Prints out statistics and settings for a CUDD manager.
  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
int
Cudd_PrintInfo(
  DdManager * dd,
  FILE * fp)
{
    int retval;
    Cudd_ReorderingType autoMethod, autoMethodZ;

    /* Modifiable parameters. */
    retval = fprintf(fp,"**** CUDD modifiable parameters ****\n");
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Hard limit for cache size: %u\n",
2948
                     Cudd_ReadMaxCacheHard(dd));
Alan Mishchenko committed
2949 2950
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Cache hit threshold for resizing: %u%%\n",
2951
                     Cudd_ReadMinHit(dd));
Alan Mishchenko committed
2952 2953
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Garbage collection enabled: %s\n",
2954
                     Cudd_GarbageCollectionEnabled(dd) ? "yes" : "no");
Alan Mishchenko committed
2955 2956
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Limit for fast unique table growth: %u\n",
2957
                     Cudd_ReadLooseUpTo(dd));
Alan Mishchenko committed
2958 2959
    if (retval == EOF) return(0);
    retval = fprintf(fp,
2960 2961
                     "Maximum number of variables sifted per reordering: %d\n",
                     Cudd_ReadSiftMaxVar(dd));
Alan Mishchenko committed
2962 2963
    if (retval == EOF) return(0);
    retval = fprintf(fp,
2964 2965
                     "Maximum number of variable swaps per reordering: %d\n",
                     Cudd_ReadSiftMaxSwap(dd));
Alan Mishchenko committed
2966 2967
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Maximum growth while sifting a variable: %g\n",
2968
                     Cudd_ReadMaxGrowth(dd));
Alan Mishchenko committed
2969 2970
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Dynamic reordering of BDDs enabled: %s\n",
2971
                     Cudd_ReorderingStatus(dd,&autoMethod) ? "yes" : "no");
Alan Mishchenko committed
2972
    if (retval == EOF) return(0);
2973 2974
    retval = fprintf(fp,"Default BDD reordering method: %d\n",
                     (int) autoMethod);
Alan Mishchenko committed
2975 2976
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Dynamic reordering of ZDDs enabled: %s\n",
2977
                     Cudd_ReorderingStatusZdd(dd,&autoMethodZ) ? "yes" : "no");
Alan Mishchenko committed
2978
    if (retval == EOF) return(0);
2979 2980
    retval = fprintf(fp,"Default ZDD reordering method: %d\n",
                     (int) autoMethodZ);
Alan Mishchenko committed
2981 2982
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Realignment of ZDDs to BDDs enabled: %s\n",
2983
                     Cudd_zddRealignmentEnabled(dd) ? "yes" : "no");
Alan Mishchenko committed
2984 2985
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Realignment of BDDs to ZDDs enabled: %s\n",
2986
                     Cudd_bddRealignmentEnabled(dd) ? "yes" : "no");
Alan Mishchenko committed
2987 2988
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Dead nodes counted in triggering reordering: %s\n",
2989
                     Cudd_DeadAreCounted(dd) ? "yes" : "no");
Alan Mishchenko committed
2990 2991
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Group checking criterion: %d\n",
2992
                     (int) Cudd_ReadGroupcheck(dd));
Alan Mishchenko committed
2993 2994 2995 2996
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Recombination threshold: %d\n", Cudd_ReadRecomb(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Symmetry violation threshold: %d\n",
2997
                     Cudd_ReadSymmviolation(dd));
Alan Mishchenko committed
2998 2999
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Arc violation threshold: %d\n",
3000
                     Cudd_ReadArcviolation(dd));
Alan Mishchenko committed
3001 3002
    if (retval == EOF) return(0);
    retval = fprintf(fp,"GA population size: %d\n",
3003
                     Cudd_ReadPopulationSize(dd));
Alan Mishchenko committed
3004 3005
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of crossovers for GA: %d\n",
3006
                     Cudd_ReadNumberXovers(dd));
Alan Mishchenko committed
3007 3008
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Next reordering threshold: %u\n",
3009
                     Cudd_ReadNextReordering(dd));
Alan Mishchenko committed
3010 3011 3012 3013 3014
    if (retval == EOF) return(0);

    /* Non-modifiable parameters. */
    retval = fprintf(fp,"**** CUDD non-modifiable parameters ****\n");
    if (retval == EOF) return(0);
3015
    retval = fprintf(fp,"Memory in use: %lu\n", Cudd_ReadMemoryInUse(dd));
Alan Mishchenko committed
3016 3017
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Peak number of nodes: %ld\n",
3018
                     Cudd_ReadPeakNodeCount(dd));
Alan Mishchenko committed
3019 3020
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Peak number of live nodes: %d\n",
3021
                     Cudd_ReadPeakLiveNodeCount(dd));
Alan Mishchenko committed
3022 3023 3024 3025 3026 3027 3028 3029
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of BDD variables: %d\n", dd->size);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of ZDD variables: %d\n", dd->sizeZ);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of cache entries: %u\n", dd->cacheSlots);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of cache look-ups: %.0f\n",
3030
                     Cudd_ReadCacheLookUps(dd));
Alan Mishchenko committed
3031 3032
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of cache hits: %.0f\n",
3033
                     Cudd_ReadCacheHits(dd));
Alan Mishchenko committed
3034 3035
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of cache insertions: %.0f\n",
3036
                     dd->cacheinserts);
Alan Mishchenko committed
3037 3038
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of cache collisions: %.0f\n",
3039
                     dd->cachecollisions);
Alan Mishchenko committed
3040 3041
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of cache deletions: %.0f\n",
3042
                     dd->cachedeletions);
Alan Mishchenko committed
3043 3044 3045 3046
    if (retval == EOF) return(0);
    retval = cuddCacheProfile(dd,fp);
    if (retval == 0) return(0);
    retval = fprintf(fp,"Soft limit for cache size: %u\n",
3047
                     Cudd_ReadMaxCache(dd));
Alan Mishchenko committed
3048 3049 3050 3051
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of buckets in unique table: %u\n", dd->slots);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Used buckets in unique table: %.2f%% (expected %.2f%%)\n",
3052 3053
                     100.0 * Cudd_ReadUsedSlots(dd),
                     100.0 * Cudd_ExpectedUsedSlots(dd));
Alan Mishchenko committed
3054 3055 3056 3057 3058
    if (retval == EOF) return(0);
#ifdef DD_UNIQUE_PROFILE
    retval = fprintf(fp,"Unique lookups: %.0f\n", dd->uniqueLookUps);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Unique links: %.0f (%g per lookup)\n",
3059
            dd->uniqueLinks, dd->uniqueLinks / dd->uniqueLookUps);
Alan Mishchenko committed
3060 3061 3062 3063 3064 3065 3066 3067 3068 3069
    if (retval == EOF) return(0);
#endif
    retval = fprintf(fp,"Number of BDD and ADD nodes: %u\n", dd->keys);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of ZDD nodes: %u\n", dd->keysZ);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of dead BDD and ADD nodes: %u\n", dd->dead);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of dead ZDD nodes: %u\n", dd->deadZ);
    if (retval == EOF) return(0);
3070
    retval = fprintf(fp,"Total number of nodes allocated: %d\n", (int)dd->allocated);
Alan Mishchenko committed
3071 3072
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Total number of nodes reclaimed: %.0f\n",
3073
                     dd->reclaimed);
Alan Mishchenko committed
3074
    if (retval == EOF) return(0);
3075
#ifdef DD_STATS
Alan Mishchenko committed
3076 3077 3078 3079 3080
    retval = fprintf(fp,"Nodes freed: %.0f\n", dd->nodesFreed);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Nodes dropped: %.0f\n", dd->nodesDropped);
    if (retval == EOF) return(0);
#endif
3081
#ifdef DD_COUNT
Alan Mishchenko committed
3082
    retval = fprintf(fp,"Number of recursive calls: %.0f\n",
3083
                     Cudd_ReadRecursiveCalls(dd));
Alan Mishchenko committed
3084 3085 3086
    if (retval == EOF) return(0);
#endif
    retval = fprintf(fp,"Garbage collections so far: %d\n",
3087
                     Cudd_ReadGarbageCollections(dd));
Alan Mishchenko committed
3088 3089
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Time for garbage collection: %.2f sec\n",
3090
                     ((double)Cudd_ReadGarbageCollectionTime(dd)/1000.0));
Alan Mishchenko committed
3091 3092 3093 3094
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Reorderings so far: %d\n", dd->reorderings);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Time for reordering: %.2f sec\n",
3095
                     ((double)Cudd_ReadReorderingTime(dd)/1000.0));
Alan Mishchenko committed
3096
    if (retval == EOF) return(0);
3097
#ifdef DD_COUNT
Alan Mishchenko committed
3098
    retval = fprintf(fp,"Node swaps in reordering: %.0f\n",
3099
        Cudd_ReadSwapSteps(dd));
Alan Mishchenko committed
3100 3101 3102 3103 3104 3105 3106 3107 3108 3109 3110 3111 3112
    if (retval == EOF) return(0);
#endif

    return(1);

} /* end of Cudd_PrintInfo */


/**Function********************************************************************

  Synopsis    [Reports the peak number of nodes.]

  Description [Reports the peak number of nodes. This number includes
3113
  node on the free list. At the peak, the number of nodes on the free
Alan Mishchenko committed
3114 3115 3116 3117 3118 3119 3120 3121 3122 3123 3124 3125 3126 3127 3128
  list is guaranteed to be less than DD_MEM_CHUNK.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadNodeCount Cudd_PrintInfo]

******************************************************************************/
long
Cudd_ReadPeakNodeCount(
  DdManager * dd)
{
    long count = 0;
    DdNodePtr *scan = dd->memoryList;

    while (scan != NULL) {
3129 3130
        count += DD_MEM_CHUNK;
        scan = (DdNodePtr *) *scan;
Alan Mishchenko committed
3131 3132 3133 3134 3135 3136 3137 3138 3139 3140 3141 3142 3143 3144 3145 3146 3147 3148 3149 3150 3151 3152 3153 3154 3155 3156
    }
    return(count);

} /* end of Cudd_ReadPeakNodeCount */


/**Function********************************************************************

  Synopsis    [Reports the peak number of live nodes.]

  Description [Reports the peak number of live nodes. This count is kept
  only if CUDD is compiled with DD_STATS defined. If DD_STATS is not
  defined, this function returns -1.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadNodeCount Cudd_PrintInfo Cudd_ReadPeakNodeCount]

******************************************************************************/
int
Cudd_ReadPeakLiveNodeCount(
  DdManager * dd)
{
    unsigned int live = dd->keys - dd->dead;

    if (live > dd->peakLiveNodes) {
3157
        dd->peakLiveNodes = live;
Alan Mishchenko committed
3158 3159 3160 3161 3162 3163 3164 3165 3166 3167 3168 3169 3170 3171 3172 3173 3174 3175 3176 3177 3178 3179 3180 3181 3182 3183 3184 3185 3186 3187 3188
    }
    return((int)dd->peakLiveNodes);

} /* end of Cudd_ReadPeakLiveNodeCount */


/**Function********************************************************************

  Synopsis    [Reports the number of nodes in BDDs and ADDs.]

  Description [Reports the number of live nodes in BDDs and ADDs. This
  number does not include the isolated projection functions and the
  unused constants. These nodes that are not counted are not part of
  the DDs manipulated by the application.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadPeakNodeCount Cudd_zddReadNodeCount]

******************************************************************************/
long
Cudd_ReadNodeCount(
  DdManager * dd)
{
    long count;
    int i;

#ifndef DD_NO_DEATH_ROW
    cuddClearDeathRow(dd);
#endif

3189
    count = (long) (dd->keys - dd->dead);
Alan Mishchenko committed
3190 3191 3192 3193 3194

    /* Count isolated projection functions. Their number is subtracted
    ** from the node count because they are not part of the BDDs.
    */
    for (i=0; i < dd->size; i++) {
3195
        if (dd->vars[i]->ref == 1) count--;
Alan Mishchenko committed
3196 3197 3198 3199 3200 3201 3202 3203 3204 3205 3206 3207 3208 3209 3210 3211 3212 3213 3214 3215 3216 3217 3218 3219 3220 3221 3222 3223
    }
    /* Subtract from the count the unused constants. */
    if (DD_ZERO(dd)->ref == 1) count--;
    if (DD_PLUS_INFINITY(dd)->ref == 1) count--;
    if (DD_MINUS_INFINITY(dd)->ref == 1) count--;

    return(count);

} /* end of Cudd_ReadNodeCount */



/**Function********************************************************************

  Synopsis    [Reports the number of nodes in ZDDs.]

  Description [Reports the number of nodes in ZDDs. This
  number always includes the two constants 1 and 0.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadPeakNodeCount Cudd_ReadNodeCount]

******************************************************************************/
long
Cudd_zddReadNodeCount(
  DdManager * dd)
{
3224
    return((long)(dd->keysZ - dd->deadZ + 2));
Alan Mishchenko committed
3225 3226 3227 3228 3229 3230 3231 3232 3233 3234 3235 3236 3237 3238 3239 3240 3241 3242 3243 3244 3245

} /* end of Cudd_zddReadNodeCount */


/**Function********************************************************************

  Synopsis    [Adds a function to a hook.]

  Description [Adds a function to a hook. A hook is a list of
  application-provided functions called on certain occasions by the
  package. Returns 1 if the function is successfully added; 2 if the
  function was already in the list; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_RemoveHook]

******************************************************************************/
int
Cudd_AddHook(
  DdManager * dd,
3246
  DD_HFP f,
Alan Mishchenko committed
3247 3248 3249 3250 3251 3252
  Cudd_HookType where)
{
    DdHook **hook, *nextHook, *newHook;

    switch (where) {
    case CUDD_PRE_GC_HOOK:
3253 3254
        hook = &(dd->preGCHook);
        break;
Alan Mishchenko committed
3255
    case CUDD_POST_GC_HOOK:
3256 3257
        hook = &(dd->postGCHook);
        break;
Alan Mishchenko committed
3258
    case CUDD_PRE_REORDERING_HOOK:
3259 3260
        hook = &(dd->preReorderingHook);
        break;
Alan Mishchenko committed
3261
    case CUDD_POST_REORDERING_HOOK:
3262 3263
        hook = &(dd->postReorderingHook);
        break;
Alan Mishchenko committed
3264
    default:
3265
        return(0);
Alan Mishchenko committed
3266 3267 3268 3269 3270
    }
    /* Scan the list and find whether the function is already there.
    ** If so, just return. */
    nextHook = *hook;
    while (nextHook != NULL) {
3271 3272 3273 3274 3275
        if (nextHook->f == f) {
            return(2);
        }
        hook = &(nextHook->next);
        nextHook = nextHook->next;
Alan Mishchenko committed
3276 3277 3278
    }
    /* The function was not in the list. Create a new item and append it
    ** to the end of the list. */
Alan Mishchenko committed
3279
    newHook = ABC_ALLOC(DdHook,1);
Alan Mishchenko committed
3280
    if (newHook == NULL) {
3281 3282
        dd->errorCode = CUDD_MEMORY_OUT;
        return(0);
Alan Mishchenko committed
3283 3284 3285 3286 3287 3288 3289 3290 3291 3292 3293 3294 3295 3296 3297 3298 3299 3300 3301 3302 3303 3304 3305 3306 3307
    }
    newHook->next = NULL;
    newHook->f = f;
    *hook = newHook;
    return(1);

} /* end of Cudd_AddHook */


/**Function********************************************************************

  Synopsis    [Removes a function from a hook.]

  Description [Removes a function from a hook. A hook is a list of
  application-provided functions called on certain occasions by the
  package. Returns 1 if successful; 0 the function was not in the list.]

  SideEffects [None]

  SeeAlso     [Cudd_AddHook]

******************************************************************************/
int
Cudd_RemoveHook(
  DdManager * dd,
3308
  DD_HFP f,
Alan Mishchenko committed
3309 3310 3311 3312 3313 3314
  Cudd_HookType where)
{
    DdHook **hook, *nextHook;

    switch (where) {
    case CUDD_PRE_GC_HOOK:
3315 3316
        hook = &(dd->preGCHook);
        break;
Alan Mishchenko committed
3317
    case CUDD_POST_GC_HOOK:
3318 3319
        hook = &(dd->postGCHook);
        break;
Alan Mishchenko committed
3320
    case CUDD_PRE_REORDERING_HOOK:
3321 3322
        hook = &(dd->preReorderingHook);
        break;
Alan Mishchenko committed
3323
    case CUDD_POST_REORDERING_HOOK:
3324 3325
        hook = &(dd->postReorderingHook);
        break;
Alan Mishchenko committed
3326
    default:
3327
        return(0);
Alan Mishchenko committed
3328 3329 3330
    }
    nextHook = *hook;
    while (nextHook != NULL) {
3331 3332 3333 3334 3335 3336 3337
        if (nextHook->f == f) {
            *hook = nextHook->next;
            ABC_FREE(nextHook);
            return(1);
        }
        hook = &(nextHook->next);
        nextHook = nextHook->next;
Alan Mishchenko committed
3338 3339 3340 3341 3342 3343 3344 3345 3346 3347 3348 3349 3350 3351 3352 3353 3354 3355 3356 3357 3358 3359 3360
    }

    return(0);

} /* end of Cudd_RemoveHook */


/**Function********************************************************************

  Synopsis    [Checks whether a function is in a hook.]

  Description [Checks whether a function is in a hook. A hook is a list of
  application-provided functions called on certain occasions by the
  package. Returns 1 if the function is found; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_AddHook Cudd_RemoveHook]

******************************************************************************/
int
Cudd_IsInHook(
  DdManager * dd,
3361
  DD_HFP f,
Alan Mishchenko committed
3362 3363 3364 3365 3366 3367
  Cudd_HookType where)
{
    DdHook *hook;

    switch (where) {
    case CUDD_PRE_GC_HOOK:
3368 3369
        hook = dd->preGCHook;
        break;
Alan Mishchenko committed
3370
    case CUDD_POST_GC_HOOK:
3371 3372
        hook = dd->postGCHook;
        break;
Alan Mishchenko committed
3373
    case CUDD_PRE_REORDERING_HOOK:
3374 3375
        hook = dd->preReorderingHook;
        break;
Alan Mishchenko committed
3376
    case CUDD_POST_REORDERING_HOOK:
3377 3378
        hook = dd->postReorderingHook;
        break;
Alan Mishchenko committed
3379
    default:
3380
        return(0);
Alan Mishchenko committed
3381 3382 3383
    }
    /* Scan the list and find whether the function is already there. */
    while (hook != NULL) {
3384 3385 3386 3387
        if (hook->f == f) {
            return(1);
        }
        hook = hook->next;
Alan Mishchenko committed
3388 3389 3390 3391 3392 3393 3394 3395 3396 3397 3398 3399 3400 3401 3402 3403 3404 3405 3406 3407 3408 3409
    }
    return(0);

} /* end of Cudd_IsInHook */


/**Function********************************************************************

  Synopsis    [Sample hook function to call before reordering.]

  Description [Sample hook function to call before reordering.
  Prints on the manager's stdout reordering method and initial size.
  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_StdPostReordHook]

******************************************************************************/
int
Cudd_StdPreReordHook(
  DdManager *dd,
3410
  const char *str,
Alan Mishchenko committed
3411 3412 3413 3414 3415 3416 3417 3418 3419 3420 3421 3422 3423 3424 3425
  void *data)
{
    Cudd_ReorderingType method = (Cudd_ReorderingType) (ptruint) data;
    int retval;

    retval = fprintf(dd->out,"%s reordering with ", str);
    if (retval == EOF) return(0);
    switch (method) {
    case CUDD_REORDER_SIFT_CONVERGE:
    case CUDD_REORDER_SYMM_SIFT_CONV:
    case CUDD_REORDER_GROUP_SIFT_CONV:
    case CUDD_REORDER_WINDOW2_CONV:
    case CUDD_REORDER_WINDOW3_CONV:
    case CUDD_REORDER_WINDOW4_CONV:
    case CUDD_REORDER_LINEAR_CONVERGE:
3426 3427 3428
        retval = fprintf(dd->out,"converging ");
        if (retval == EOF) return(0);
        break;
Alan Mishchenko committed
3429
    default:
3430
        break;
Alan Mishchenko committed
3431 3432 3433 3434
    }
    switch (method) {
    case CUDD_REORDER_RANDOM:
    case CUDD_REORDER_RANDOM_PIVOT:
3435 3436
        retval = fprintf(dd->out,"random");
        break;
Alan Mishchenko committed
3437 3438
    case CUDD_REORDER_SIFT:
    case CUDD_REORDER_SIFT_CONVERGE:
3439 3440
        retval = fprintf(dd->out,"sifting");
        break;
Alan Mishchenko committed
3441 3442
    case CUDD_REORDER_SYMM_SIFT:
    case CUDD_REORDER_SYMM_SIFT_CONV:
3443 3444
        retval = fprintf(dd->out,"symmetric sifting");
        break;
Alan Mishchenko committed
3445
    case CUDD_REORDER_LAZY_SIFT:
3446 3447
        retval = fprintf(dd->out,"lazy sifting");
        break;
Alan Mishchenko committed
3448 3449
    case CUDD_REORDER_GROUP_SIFT:
    case CUDD_REORDER_GROUP_SIFT_CONV:
3450 3451
        retval = fprintf(dd->out,"group sifting");
        break;
Alan Mishchenko committed
3452 3453 3454 3455 3456 3457
    case CUDD_REORDER_WINDOW2:
    case CUDD_REORDER_WINDOW3:
    case CUDD_REORDER_WINDOW4:
    case CUDD_REORDER_WINDOW2_CONV:
    case CUDD_REORDER_WINDOW3_CONV:
    case CUDD_REORDER_WINDOW4_CONV:
3458 3459
        retval = fprintf(dd->out,"window");
        break;
Alan Mishchenko committed
3460
    case CUDD_REORDER_ANNEALING:
3461 3462
        retval = fprintf(dd->out,"annealing");
        break;
Alan Mishchenko committed
3463
    case CUDD_REORDER_GENETIC:
3464 3465
        retval = fprintf(dd->out,"genetic");
        break;
Alan Mishchenko committed
3466 3467
    case CUDD_REORDER_LINEAR:
    case CUDD_REORDER_LINEAR_CONVERGE:
3468 3469
        retval = fprintf(dd->out,"linear sifting");
        break;
Alan Mishchenko committed
3470
    case CUDD_REORDER_EXACT:
3471 3472
        retval = fprintf(dd->out,"exact");
        break;
Alan Mishchenko committed
3473
    default:
3474
        return(0);
Alan Mishchenko committed
3475 3476 3477 3478
    }
    if (retval == EOF) return(0);

    retval = fprintf(dd->out,": from %ld to ... ", strcmp(str, "BDD") == 0 ?
3479
                     Cudd_ReadNodeCount(dd) : Cudd_zddReadNodeCount(dd));
Alan Mishchenko committed
3480 3481 3482 3483 3484 3485 3486 3487 3488 3489 3490 3491 3492 3493 3494 3495 3496 3497 3498 3499 3500 3501 3502
    if (retval == EOF) return(0);
    fflush(dd->out);
    return(1);

} /* end of Cudd_StdPreReordHook */


/**Function********************************************************************

  Synopsis    [Sample hook function to call after reordering.]

  Description [Sample hook function to call after reordering.
  Prints on the manager's stdout final size and reordering time.
  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_StdPreReordHook]

******************************************************************************/
int
Cudd_StdPostReordHook(
  DdManager *dd,
3503
  const char *str,
Alan Mishchenko committed
3504 3505 3506 3507 3508 3509 3510 3511
  void *data)
{
    long initialTime = (long) data;
    int retval;
    long finalTime = util_cpu_time();
    double totalTimeSec = (double)(finalTime - initialTime) / 1000.0;

    retval = fprintf(dd->out,"%ld nodes in %g sec\n", strcmp(str, "BDD") == 0 ?
3512 3513
                     Cudd_ReadNodeCount(dd) : Cudd_zddReadNodeCount(dd),
                     totalTimeSec);
Alan Mishchenko committed
3514 3515 3516 3517 3518 3519 3520 3521 3522 3523 3524 3525 3526 3527 3528 3529 3530 3531 3532 3533 3534 3535 3536 3537 3538 3539
    if (retval == EOF) return(0);
    retval = fflush(dd->out);
    if (retval == EOF) return(0);
    return(1);

} /* end of Cudd_StdPostReordHook */


/**Function********************************************************************

  Synopsis    [Enables reporting of reordering stats.]

  Description [Enables reporting of reordering stats.
  Returns 1 if successful; 0 otherwise.]

  SideEffects [Installs functions in the pre-reordering and post-reordering
  hooks.]

  SeeAlso     [Cudd_DisableReorderingReporting Cudd_ReorderingReporting]

******************************************************************************/
int
Cudd_EnableReorderingReporting(
  DdManager *dd)
{
    if (!Cudd_AddHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) {
3540
        return(0);
Alan Mishchenko committed
3541 3542
    }
    if (!Cudd_AddHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) {
3543
        return(0);
Alan Mishchenko committed
3544 3545 3546 3547 3548 3549 3550 3551 3552 3553 3554 3555 3556 3557 3558 3559 3560 3561 3562 3563 3564 3565 3566 3567
    }
    return(1);

} /* end of Cudd_EnableReorderingReporting */


/**Function********************************************************************

  Synopsis    [Disables reporting of reordering stats.]

  Description [Disables reporting of reordering stats.
  Returns 1 if successful; 0 otherwise.]

  SideEffects [Removes functions from the pre-reordering and post-reordering
  hooks.]

  SeeAlso     [Cudd_EnableReorderingReporting Cudd_ReorderingReporting]

******************************************************************************/
int
Cudd_DisableReorderingReporting(
  DdManager *dd)
{
    if (!Cudd_RemoveHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) {
3568
        return(0);
Alan Mishchenko committed
3569 3570
    }
    if (!Cudd_RemoveHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) {
3571
        return(0);
Alan Mishchenko committed
3572 3573 3574 3575 3576 3577 3578 3579 3580 3581 3582 3583 3584 3585 3586 3587 3588 3589 3590 3591 3592 3593 3594 3595 3596 3597 3598 3599 3600 3601 3602 3603 3604 3605 3606 3607 3608 3609 3610 3611 3612 3613 3614 3615 3616 3617 3618 3619 3620 3621 3622 3623 3624 3625 3626 3627 3628 3629 3630 3631 3632 3633 3634 3635 3636 3637 3638 3639 3640 3641 3642 3643 3644 3645 3646 3647 3648 3649 3650 3651 3652 3653 3654 3655 3656 3657 3658 3659 3660 3661 3662 3663 3664 3665 3666 3667 3668 3669 3670 3671 3672 3673 3674 3675 3676 3677 3678 3679 3680 3681 3682 3683 3684 3685 3686 3687 3688 3689 3690 3691 3692 3693 3694 3695 3696 3697 3698 3699 3700 3701 3702 3703 3704 3705 3706 3707 3708 3709 3710 3711 3712 3713 3714 3715 3716 3717 3718 3719 3720 3721 3722 3723 3724 3725 3726 3727 3728 3729 3730 3731 3732 3733 3734 3735 3736 3737 3738 3739 3740 3741 3742 3743 3744 3745 3746 3747 3748 3749 3750 3751 3752 3753 3754 3755 3756 3757 3758 3759 3760 3761 3762 3763 3764 3765 3766 3767 3768 3769 3770 3771 3772 3773 3774 3775 3776 3777 3778 3779 3780 3781 3782 3783 3784 3785 3786 3787 3788 3789 3790 3791 3792 3793 3794 3795 3796 3797 3798 3799 3800 3801 3802 3803 3804 3805 3806 3807 3808 3809 3810 3811 3812 3813 3814 3815 3816 3817 3818 3819 3820 3821 3822 3823 3824 3825 3826 3827 3828 3829 3830 3831 3832 3833 3834 3835 3836 3837 3838 3839 3840 3841 3842 3843 3844 3845 3846 3847 3848 3849 3850 3851 3852 3853
    }
    return(1);

} /* end of Cudd_DisableReorderingReporting */


/**Function********************************************************************

  Synopsis    [Returns 1 if reporting of reordering stats is enabled.]

  Description [Returns 1 if reporting of reordering stats is enabled;
  0 otherwise.]

  SideEffects [none]

  SeeAlso     [Cudd_EnableReorderingReporting Cudd_DisableReorderingReporting]

******************************************************************************/
int
Cudd_ReorderingReporting(
  DdManager *dd)
{
    return(Cudd_IsInHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK));

} /* end of Cudd_ReorderingReporting */


/**Function********************************************************************

  Synopsis    [Returns the code of the last error.]

  Description [Returns the code of the last error. The error codes are
  defined in cudd.h.]

  SideEffects [None]

  SeeAlso     [Cudd_ClearErrorCode]

******************************************************************************/
Cudd_ErrorType
Cudd_ReadErrorCode(
  DdManager *dd)
{
    return(dd->errorCode);

} /* end of Cudd_ReadErrorCode */


/**Function********************************************************************

  Synopsis    [Clear the error code of a manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_ReadErrorCode]

******************************************************************************/
void
Cudd_ClearErrorCode(
  DdManager *dd)
{
    dd->errorCode = CUDD_NO_ERROR;

} /* end of Cudd_ClearErrorCode */


/**Function********************************************************************

  Synopsis    [Reads the stdout of a manager.]

  Description [Reads the stdout of a manager. This is the file pointer to
  which messages normally going to stdout are written. It is initialized
  to stdout. Cudd_SetStdout allows the application to redirect it.]

  SideEffects [None]

  SeeAlso     [Cudd_SetStdout Cudd_ReadStderr]

******************************************************************************/
FILE *
Cudd_ReadStdout(
  DdManager *dd)
{
    return(dd->out);

} /* end of Cudd_ReadStdout */


/**Function********************************************************************

  Synopsis    [Sets the stdout of a manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_ReadStdout Cudd_SetStderr]

******************************************************************************/
void
Cudd_SetStdout(
  DdManager *dd,
  FILE *fp)
{
    dd->out = fp;

} /* end of Cudd_SetStdout */


/**Function********************************************************************

  Synopsis    [Reads the stderr of a manager.]

  Description [Reads the stderr of a manager. This is the file pointer to
  which messages normally going to stderr are written. It is initialized
  to stderr. Cudd_SetStderr allows the application to redirect it.]

  SideEffects [None]

  SeeAlso     [Cudd_SetStderr Cudd_ReadStdout]

******************************************************************************/
FILE *
Cudd_ReadStderr(
  DdManager *dd)
{
    return(dd->err);

} /* end of Cudd_ReadStderr */


/**Function********************************************************************

  Synopsis    [Sets the stderr of a manager.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_ReadStderr Cudd_SetStdout]

******************************************************************************/
void
Cudd_SetStderr(
  DdManager *dd,
  FILE *fp)
{
    dd->err = fp;

} /* end of Cudd_SetStderr */


/**Function********************************************************************

  Synopsis    [Returns the threshold for the next dynamic reordering.]

  Description [Returns the threshold for the next dynamic reordering.
  The threshold is in terms of number of nodes and is in effect only
  if reordering is enabled. The count does not include the dead nodes,
  unless the countDead parameter of the manager has been changed from
  its default setting.]

  SideEffects [None]

  SeeAlso     [Cudd_SetNextReordering]

******************************************************************************/
unsigned int
Cudd_ReadNextReordering(
  DdManager *dd)
{
    return(dd->nextDyn);

} /* end of Cudd_ReadNextReordering */


/**Function********************************************************************

  Synopsis    [Sets the threshold for the next dynamic reordering.]

  Description [Sets the threshold for the next dynamic reordering.
  The threshold is in terms of number of nodes and is in effect only
  if reordering is enabled. The count does not include the dead nodes,
  unless the countDead parameter of the manager has been changed from
  its default setting.]

  SideEffects [None]

  SeeAlso     [Cudd_ReadNextReordering]

******************************************************************************/
void
Cudd_SetNextReordering(
  DdManager *dd,
  unsigned int next)
{
    dd->nextDyn = next;

} /* end of Cudd_SetNextReordering */


/**Function********************************************************************

  Synopsis    [Reads the number of elementary reordering steps.]

  Description []

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
double
Cudd_ReadSwapSteps(
  DdManager *dd)
{
#ifdef DD_COUNT
    return(dd->swapSteps);
#else
    return(-1);
#endif

} /* end of Cudd_ReadSwapSteps */


/**Function********************************************************************

  Synopsis    [Reads the maximum allowed number of live nodes.]

  Description [Reads the maximum allowed number of live nodes. When this
  number is exceeded, the package returns NULL.]

  SideEffects [none]

  SeeAlso     [Cudd_SetMaxLive]

******************************************************************************/
unsigned int
Cudd_ReadMaxLive(
  DdManager *dd)
{
    return(dd->maxLive);

} /* end of Cudd_ReadMaxLive */


/**Function********************************************************************

  Synopsis    [Sets the maximum allowed number of live nodes.]

  Description [Sets the maximum allowed number of live nodes. When this
  number is exceeded, the package returns NULL.]

  SideEffects [none]

  SeeAlso     [Cudd_ReadMaxLive]

******************************************************************************/
void
Cudd_SetMaxLive(
  DdManager *dd,
  unsigned int maxLive)
{
    dd->maxLive = maxLive;

} /* end of Cudd_SetMaxLive */


/**Function********************************************************************

  Synopsis    [Reads the maximum allowed memory.]

  Description [Reads the maximum allowed memory. When this
  number is exceeded, the package returns NULL.]

  SideEffects [none]

  SeeAlso     [Cudd_SetMaxMemory]

******************************************************************************/
3854
unsigned long
Alan Mishchenko committed
3855 3856 3857 3858 3859 3860 3861 3862 3863 3864 3865 3866 3867 3868 3869 3870 3871 3872 3873 3874 3875 3876 3877
Cudd_ReadMaxMemory(
  DdManager *dd)
{
    return(dd->maxmemhard);

} /* end of Cudd_ReadMaxMemory */


/**Function********************************************************************

  Synopsis    [Sets the maximum allowed memory.]

  Description [Sets the maximum allowed memory. When this
  number is exceeded, the package returns NULL.]

  SideEffects [none]

  SeeAlso     [Cudd_ReadMaxMemory]

******************************************************************************/
void
Cudd_SetMaxMemory(
  DdManager *dd,
3878
  unsigned long maxMemory)
Alan Mishchenko committed
3879 3880 3881 3882 3883 3884 3885 3886 3887 3888 3889 3890 3891 3892 3893 3894 3895 3896 3897 3898 3899 3900 3901 3902 3903 3904 3905 3906 3907 3908 3909 3910 3911 3912 3913 3914 3915 3916 3917 3918 3919 3920 3921 3922 3923 3924 3925 3926 3927 3928 3929 3930 3931 3932 3933 3934 3935 3936 3937 3938 3939 3940 3941 3942 3943 3944 3945 3946 3947 3948 3949 3950 3951 3952 3953 3954 3955 3956 3957 3958 3959 3960 3961 3962 3963 3964 3965 3966 3967 3968 3969 3970 3971 3972 3973 3974 3975 3976 3977 3978 3979 3980 3981 3982 3983 3984 3985 3986 3987 3988 3989 3990 3991 3992 3993 3994 3995 3996 3997 3998 3999 4000 4001 4002 4003 4004 4005 4006 4007 4008 4009 4010 4011 4012 4013 4014 4015 4016 4017 4018 4019 4020 4021 4022 4023 4024 4025 4026 4027 4028 4029 4030 4031 4032 4033 4034 4035 4036 4037 4038 4039 4040 4041 4042 4043 4044 4045 4046 4047 4048 4049 4050 4051 4052 4053 4054 4055 4056 4057 4058 4059 4060 4061 4062 4063 4064 4065 4066 4067 4068 4069 4070 4071 4072 4073 4074 4075 4076 4077 4078 4079 4080 4081 4082 4083 4084 4085 4086 4087 4088 4089 4090 4091 4092 4093 4094 4095 4096 4097 4098 4099 4100 4101 4102 4103 4104 4105 4106 4107 4108 4109 4110 4111 4112 4113 4114 4115 4116 4117 4118 4119 4120 4121 4122 4123 4124 4125 4126 4127 4128 4129 4130 4131 4132 4133 4134 4135 4136 4137 4138 4139 4140 4141 4142 4143 4144 4145 4146 4147 4148 4149 4150 4151 4152 4153 4154 4155 4156 4157 4158 4159 4160 4161 4162 4163 4164 4165 4166 4167 4168 4169 4170 4171 4172 4173 4174 4175 4176
{
    dd->maxmemhard = maxMemory;

} /* end of Cudd_SetMaxMemory */


/**Function********************************************************************

  Synopsis    [Prevents sifting of a variable.]

  Description [This function sets a flag to prevent sifting of a
  variable.  Returns 1 if successful; 0 otherwise (i.e., invalid
  variable index).]

  SideEffects [Changes the "bindVar" flag in DdSubtable.]

  SeeAlso     [Cudd_bddUnbindVar]

******************************************************************************/
int
Cudd_bddBindVar(
  DdManager *dd /* manager */,
  int index /* variable index */)
{
    if (index >= dd->size || index < 0) return(0);
    dd->subtables[dd->perm[index]].bindVar = 1;
    return(1);

} /* end of Cudd_bddBindVar */


/**Function********************************************************************

  Synopsis    [Allows the sifting of a variable.]

  Description [This function resets the flag that prevents the sifting
  of a variable. In successive variable reorderings, the variable will
  NOT be skipped, that is, sifted.  Initially all variables can be
  sifted. It is necessary to call this function only to re-enable
  sifting after a call to Cudd_bddBindVar. Returns 1 if successful; 0
  otherwise (i.e., invalid variable index).]

  SideEffects [Changes the "bindVar" flag in DdSubtable.]

  SeeAlso     [Cudd_bddBindVar]

******************************************************************************/
int
Cudd_bddUnbindVar(
  DdManager *dd /* manager */,
  int index /* variable index */)
{
    if (index >= dd->size || index < 0) return(0);
    dd->subtables[dd->perm[index]].bindVar = 0;
    return(1);

} /* end of Cudd_bddUnbindVar */


/**Function********************************************************************

  Synopsis    [Tells whether a variable can be sifted.]

  Description [This function returns 1 if a variable is enabled for
  sifting.  Initially all variables can be sifted. This function returns
  0 only if there has been a previous call to Cudd_bddBindVar for that
  variable not followed by a call to Cudd_bddUnbindVar. The function returns
  0 also in the case in which the index of the variable is out of bounds.]

  SideEffects [none]

  SeeAlso     [Cudd_bddBindVar Cudd_bddUnbindVar]

******************************************************************************/
int
Cudd_bddVarIsBound(
  DdManager *dd /* manager */,
  int index /* variable index */)
{
    if (index >= dd->size || index < 0) return(0);
    return(dd->subtables[dd->perm[index]].bindVar);

} /* end of Cudd_bddVarIsBound */


/**Function********************************************************************

  Synopsis    [Sets a variable type to primary input.]

  Description [Sets a variable type to primary input.  The variable type is
  used by lazy sifting.  Returns 1 if successful; 0 otherwise.]

  SideEffects [modifies the manager]

  SeeAlso     [Cudd_bddSetPsVar Cudd_bddSetNsVar Cudd_bddIsPiVar]

******************************************************************************/
int
Cudd_bddSetPiVar(
  DdManager *dd /* manager */,
  int index /* variable index */)
{
    if (index >= dd->size || index < 0) return (0);
    dd->subtables[dd->perm[index]].varType = CUDD_VAR_PRIMARY_INPUT;
    return(1);

} /* end of Cudd_bddSetPiVar */


/**Function********************************************************************

  Synopsis    [Sets a variable type to present state.]

  Description [Sets a variable type to present state.  The variable type is
  used by lazy sifting.  Returns 1 if successful; 0 otherwise.]

  SideEffects [modifies the manager]

  SeeAlso     [Cudd_bddSetPiVar Cudd_bddSetNsVar Cudd_bddIsPsVar]

******************************************************************************/
int
Cudd_bddSetPsVar(
  DdManager *dd /* manager */,
  int index /* variable index */)
{
    if (index >= dd->size || index < 0) return (0);
    dd->subtables[dd->perm[index]].varType = CUDD_VAR_PRESENT_STATE;
    return(1);

} /* end of Cudd_bddSetPsVar */


/**Function********************************************************************

  Synopsis    [Sets a variable type to next state.]

  Description [Sets a variable type to next state.  The variable type is
  used by lazy sifting.  Returns 1 if successful; 0 otherwise.]

  SideEffects [modifies the manager]

  SeeAlso     [Cudd_bddSetPiVar Cudd_bddSetPsVar Cudd_bddIsNsVar]

******************************************************************************/
int
Cudd_bddSetNsVar(
  DdManager *dd /* manager */,
  int index /* variable index */)
{
    if (index >= dd->size || index < 0) return (0);
    dd->subtables[dd->perm[index]].varType = CUDD_VAR_NEXT_STATE;
    return(1);

} /* end of Cudd_bddSetNsVar */


/**Function********************************************************************

  Synopsis    [Checks whether a variable is primary input.]

  Description [Checks whether a variable is primary input.  Returns 1 if
  the variable's type is primary input; 0 if the variable exists but is
  not a primary input; -1 if the variable does not exist.]

  SideEffects [none]

  SeeAlso     [Cudd_bddSetPiVar Cudd_bddIsPsVar Cudd_bddIsNsVar]

******************************************************************************/
int
Cudd_bddIsPiVar(
  DdManager *dd /* manager */,
  int index /* variable index */)
{
    if (index >= dd->size || index < 0) return -1;
    return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_PRIMARY_INPUT);

} /* end of Cudd_bddIsPiVar */


/**Function********************************************************************

  Synopsis    [Checks whether a variable is present state.]

  Description [Checks whether a variable is present state.  Returns 1 if
  the variable's type is present state; 0 if the variable exists but is
  not a present state; -1 if the variable does not exist.]

  SideEffects [none]

  SeeAlso     [Cudd_bddSetPsVar Cudd_bddIsPiVar Cudd_bddIsNsVar]

******************************************************************************/
int
Cudd_bddIsPsVar(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return -1;
    return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_PRESENT_STATE);

} /* end of Cudd_bddIsPsVar */


/**Function********************************************************************

  Synopsis    [Checks whether a variable is next state.]

  Description [Checks whether a variable is next state.  Returns 1 if
  the variable's type is present state; 0 if the variable exists but is
  not a present state; -1 if the variable does not exist.]

  SideEffects [none]

  SeeAlso     [Cudd_bddSetNsVar Cudd_bddIsPiVar Cudd_bddIsPsVar]

******************************************************************************/
int
Cudd_bddIsNsVar(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return -1;
    return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_NEXT_STATE);

} /* end of Cudd_bddIsNsVar */


/**Function********************************************************************

  Synopsis    [Sets a corresponding pair index for a given index.]

  Description [Sets a corresponding pair index for a given index.
  These pair indices are present and next state variable.  Returns 1 if
  successful; 0 otherwise.]

  SideEffects [modifies the manager]

  SeeAlso     [Cudd_bddReadPairIndex]

******************************************************************************/
int
Cudd_bddSetPairIndex(
  DdManager *dd /* manager */,
  int index /* variable index */,
  int pairIndex /* corresponding variable index */)
{
    if (index >= dd->size || index < 0) return(0);
    dd->subtables[dd->perm[index]].pairIndex = pairIndex;
    return(1);

} /* end of Cudd_bddSetPairIndex */


/**Function********************************************************************

  Synopsis    [Reads a corresponding pair index for a given index.]

  Description [Reads a corresponding pair index for a given index.
  These pair indices are present and next state variable.  Returns the
  corresponding variable index if the variable exists; -1 otherwise.]

  SideEffects [modifies the manager]

  SeeAlso     [Cudd_bddSetPairIndex]

******************************************************************************/
int
Cudd_bddReadPairIndex(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return -1;
    return dd->subtables[dd->perm[index]].pairIndex;

} /* end of Cudd_bddReadPairIndex */


/**Function********************************************************************

  Synopsis    [Sets a variable to be grouped.]

  Description [Sets a variable to be grouped. This function is used for
  lazy sifting.  Returns 1 if successful; 0 otherwise.]

  SideEffects [modifies the manager]

  SeeAlso     [Cudd_bddSetVarHardGroup Cudd_bddResetVarToBeGrouped]

******************************************************************************/
int
Cudd_bddSetVarToBeGrouped(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(0);
    if (dd->subtables[dd->perm[index]].varToBeGrouped <= CUDD_LAZY_SOFT_GROUP) {
4177
        dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_SOFT_GROUP;
Alan Mishchenko committed
4178 4179 4180 4181 4182 4183 4184 4185 4186 4187 4188 4189 4190 4191 4192 4193 4194 4195 4196 4197 4198 4199 4200 4201 4202 4203 4204 4205 4206 4207 4208 4209 4210 4211 4212 4213 4214 4215 4216 4217 4218 4219 4220 4221 4222 4223 4224 4225 4226 4227
    }
    return(1);

} /* end of Cudd_bddSetVarToBeGrouped */


/**Function********************************************************************

  Synopsis    [Sets a variable to be a hard group.]

  Description [Sets a variable to be a hard group.  This function is used
  for lazy sifting.  Returns 1 if successful; 0 otherwise.]

  SideEffects [modifies the manager]

  SeeAlso     [Cudd_bddSetVarToBeGrouped Cudd_bddResetVarToBeGrouped
  Cudd_bddIsVarHardGroup]

******************************************************************************/
int
Cudd_bddSetVarHardGroup(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(0);
    dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_HARD_GROUP;
    return(1);

} /* end of Cudd_bddSetVarHardGrouped */


/**Function********************************************************************

  Synopsis    [Resets a variable not to be grouped.]

  Description [Resets a variable not to be grouped.  This function is
  used for lazy sifting.  Returns 1 if successful; 0 otherwise.]

  SideEffects [modifies the manager]

  SeeAlso     [Cudd_bddSetVarToBeGrouped Cudd_bddSetVarHardGroup]

******************************************************************************/
int
Cudd_bddResetVarToBeGrouped(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(0);
    if (dd->subtables[dd->perm[index]].varToBeGrouped <=
4228 4229
        CUDD_LAZY_SOFT_GROUP) {
        dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_NONE;
Alan Mishchenko committed
4230 4231 4232 4233 4234 4235 4236 4237 4238 4239 4240 4241 4242 4243 4244 4245 4246 4247 4248 4249 4250 4251 4252 4253 4254
    }
    return(1);

} /* end of Cudd_bddResetVarToBeGrouped */


/**Function********************************************************************

  Synopsis    [Checks whether a variable is set to be grouped.]

  Description [Checks whether a variable is set to be grouped. This
  function is used for lazy sifting.]

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
int
Cudd_bddIsVarToBeGrouped(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(-1);
    if (dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_UNGROUP)
4255
        return(0);
Alan Mishchenko committed
4256
    else
4257
        return(dd->subtables[dd->perm[index]].varToBeGrouped);
Alan Mishchenko committed
4258 4259 4260 4261 4262 4263 4264 4265 4266 4267 4268 4269 4270 4271 4272 4273 4274 4275 4276 4277 4278 4279 4280 4281 4282 4283 4284 4285 4286 4287 4288 4289 4290 4291 4292 4293 4294 4295 4296 4297 4298 4299 4300 4301 4302 4303 4304 4305 4306 4307 4308 4309 4310 4311 4312 4313 4314 4315 4316 4317 4318 4319 4320 4321 4322 4323 4324 4325 4326 4327 4328 4329 4330 4331

} /* end of Cudd_bddIsVarToBeGrouped */


/**Function********************************************************************

  Synopsis    [Sets a variable to be ungrouped.]

  Description [Sets a variable to be ungrouped. This function is used
  for lazy sifting.  Returns 1 if successful; 0 otherwise.]

  SideEffects [modifies the manager]

  SeeAlso     [Cudd_bddIsVarToBeUngrouped]

******************************************************************************/
int
Cudd_bddSetVarToBeUngrouped(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(0);
    dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_UNGROUP;
    return(1);

} /* end of Cudd_bddSetVarToBeGrouped */


/**Function********************************************************************

  Synopsis    [Checks whether a variable is set to be ungrouped.]

  Description [Checks whether a variable is set to be ungrouped. This
  function is used for lazy sifting.  Returns 1 if the variable is marked
  to be ungrouped; 0 if the variable exists, but it is not marked to be
  ungrouped; -1 if the variable does not exist.]

  SideEffects [none]

  SeeAlso     [Cudd_bddSetVarToBeUngrouped]

******************************************************************************/
int
Cudd_bddIsVarToBeUngrouped(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(-1);
    return dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_UNGROUP;

} /* end of Cudd_bddIsVarToBeGrouped */


/**Function********************************************************************

  Synopsis    [Checks whether a variable is set to be in a hard group.]

  Description [Checks whether a variable is set to be in a hard group.  This
  function is used for lazy sifting.  Returns 1 if the variable is marked
  to be in a hard group; 0 if the variable exists, but it is not marked to be
  in a hard group; -1 if the variable does not exist.]

  SideEffects [none]

  SeeAlso     [Cudd_bddSetVarHardGroup]

******************************************************************************/
int
Cudd_bddIsVarHardGroup(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(-1);
    if (dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_HARD_GROUP)
4332
        return(1);
Alan Mishchenko committed
4333 4334 4335 4336 4337 4338 4339 4340 4341 4342 4343 4344 4345 4346 4347 4348 4349 4350 4351 4352 4353 4354 4355 4356 4357 4358 4359 4360 4361 4362 4363 4364 4365
    return(0);

} /* end of Cudd_bddIsVarToBeGrouped */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [Fixes a variable group tree.]

  Description []

  SideEffects [Changes the variable group tree.]

  SeeAlso     []

******************************************************************************/
static void
fixVarTree(
  MtrNode * treenode,
  int * perm,
  int  size)
{
    treenode->index = treenode->low;
    treenode->low = ((int) treenode->index < size) ?
4366
        perm[treenode->index] : treenode->index;
Alan Mishchenko committed
4367
    if (treenode->child != NULL)
4368
        fixVarTree(treenode->child, perm, size);
Alan Mishchenko committed
4369
    if (treenode->younger != NULL)
4370
        fixVarTree(treenode->younger, perm, size);
Alan Mishchenko committed
4371 4372 4373 4374 4375 4376 4377 4378 4379 4380 4381 4382 4383 4384 4385 4386 4387 4388 4389 4390 4391 4392 4393 4394 4395 4396 4397 4398 4399 4400 4401 4402 4403 4404 4405 4406 4407 4408 4409 4410 4411 4412 4413
    return;

} /* end of fixVarTree */


/**Function********************************************************************

  Synopsis    [Adds multiplicity groups to a ZDD variable group tree.]

  Description [Adds multiplicity groups to a ZDD variable group tree.
  Returns 1 if successful; 0 otherwise. This function creates the groups
  for set of ZDD variables (whose cardinality is given by parameter
  multiplicity) that are created for each BDD variable in
  Cudd_zddVarsFromBddVars. The crux of the matter is to determine the index
  each new group. (The index of the first variable in the group.)
  We first build all the groups for the children of a node, and then deal
  with the ZDD variables that are directly attached to the node. The problem
  for these is that the tree itself does not provide information on their
  position inside the group. While we deal with the children of the node,
  therefore, we keep track of all the positions they occupy. The remaining
  positions in the tree can be freely used. Also, we keep track of all the
  variables placed in the children. All the remaining variables are directly
  attached to the group. We can then place any pair of variables not yet
  grouped in any pair of available positions in the node.]

  SideEffects [Changes the variable group tree.]

  SeeAlso     [Cudd_zddVarsFromBddVars]

******************************************************************************/
static int
addMultiplicityGroups(
  DdManager *dd /* manager */,
  MtrNode *treenode /* current tree node */,
  int multiplicity /* how many ZDD vars per BDD var */,
  char *vmask /* variable pairs for which a group has been already built */,
  char *lmask /* levels for which a group has already been built*/)
{
    int startV, stopV, startL;
    int i, j;
    MtrNode *auxnode = treenode;

    while (auxnode != NULL) {
4414 4415
        if (auxnode->child != NULL) {
            addMultiplicityGroups(dd,auxnode->child,multiplicity,vmask,lmask);
Alan Mishchenko committed
4416
        }
4417 4418 4419 4420 4421 4422 4423 4424 4425 4426 4427 4428 4429 4430 4431 4432 4433 4434
        /* Build remaining groups. */
        startV = dd->permZ[auxnode->index] / multiplicity;
        startL = auxnode->low / multiplicity;
        stopV = startV + auxnode->size / multiplicity;
        /* Walk down vmask starting at startV and build missing groups. */
        for (i = startV, j = startL; i < stopV; i++) {
            if (vmask[i] == 0) {
                MtrNode *node;
                while (lmask[j] == 1) j++;
                node = Mtr_MakeGroup(auxnode, j * multiplicity, multiplicity,
                                     MTR_FIXED);
                if (node == NULL) {
                    return(0);
                }
                node->index = dd->invpermZ[i * multiplicity];
                vmask[i] = 1;
                lmask[j] = 1;
            }
Alan Mishchenko committed
4435
        }
4436
        auxnode = auxnode->younger;
Alan Mishchenko committed
4437 4438 4439 4440 4441
    }
    return(1);

} /* end of addMultiplicityGroups */

4442

4443 4444
ABC_NAMESPACE_IMPL_END