cuddAddAbs.c

Quantification functions for ADDs.

cuddAddApply.c

Apply functions for ADDs and their operators.

cuddAddFind.c

Functions to find maximum and minimum in an ADD and to extract the i-th bit.

cuddAddInv.c

Function to compute the scalar inverse of an ADD.

cuddAddIte.c

ADD ITE function and satellites.

cuddAddNeg.c

Function to compute the negation of an ADD.

cuddAddWalsh.c

Functions that generate Walsh matrices and residue functions in ADD form.

cuddAndAbs.c

Combined AND and existential abstraction for BDDs

cuddAnneal.c

Reordering of DDs based on simulated annealing

cuddApa.c

Arbitrary precision arithmetic functions.

cuddAPI.c

Application interface functions.

cuddApprox.c

Procedures to approximate a given BDD.

cuddBddAbs.c

Quantification functions for BDDs.

cuddBddCorr.c

Correlation between BDDs.

cuddBddIte.c

BDD ITE function and satellites.

cuddBridge.c

Translation from BDD to ADD and vice versa and transfer between different managers.

cuddCache.c

Functions for cache insertion and lookup.

cuddCheck.c

Functions to check consistency of data structures.

cuddClip.c

Clipping functions.

cuddCof.c

Cofactoring functions.

cuddCompose.c

Functional composition and variable permutation of DDs.

cuddDecomp.c

Functions for BDD decomposition.

cuddEssent.c

Functions for the detection of essential variables.

cuddExact.c

Functions for exact variable reordering.

cuddExport.c

Export functions.

cuddGenCof.c

Generalized cofactors for BDDs and ADDs.

cuddGenetic.c

Genetic algorithm for variable reordering.

cuddGroup.c

Functions for group sifting.

cuddHarwell.c

Function to read a matrix in Harwell format.

cuddInit.c

Functions to initialize and shut down the DD manager.

cuddInteract.c

Functions to manipulate the variable interaction matrix.

cuddLCache.c

Functions for local caches.

cuddLevelQ.c

Procedure to manage level queues.

cuddLinear.c

Functions for DD reduction by linear transformations.

cuddLiteral.c

Functions for manipulation of literal sets represented by BDDs.

cuddMatMult.c

Matrix multiplication functions.

cuddPriority.c

Priority functions.

cuddRead.c

Functions to read in a matrix

cuddRef.c

Functions that manipulate the reference counts.

cuddReorder.c

Functions for dynamic variable reordering.

cuddSat.c

Functions for the solution of satisfiability related problems.

cuddSign.c

Computation of signatures.

cuddSolve.c

Boolean equation solver and related functions.

cuddSplit.c

Returns a subset of minterms from a boolean function.

cuddSubsetHB.c

Procedure to subset the given BDD by choosing the heavier branches.

cuddSubsetSP.c

Procedure to subset the given BDD choosing the shortest paths (largest cubes) in the BDD.

cuddSymmetry.c

Functions for symmetry-based variable reordering.

cuddTable.c

Unique table management functions.

cuddUtil.c

Utility functions.

cuddWindow.c

Functions for variable reordering by window permutation.

cuddZddCount.c

Procedures to count the number of minterms of a ZDD.

cuddZddFuncs.c

Functions to manipulate covers represented as ZDDs.

cuddZddGroup.c

Functions for ZDD group sifting.

cuddZddIsop.c

Functions to find irredundant SOP covers as ZDDs from BDDs.

cuddZddLin.c

Procedures for dynamic variable ordering of ZDDs.

cuddZddMisc.c

Miscellaneous utility functions for ZDDs.

cuddZddPort.c

Functions that translate BDDs to ZDDs.

cuddZddReord.c

Procedures for dynamic variable ordering of ZDDs.

cuddZddSetop.c

Set operations on ZDDs.

cuddZddSymm.c

Functions for symmetry-based ZDD variable reordering.

cuddZddUtil.c

Utility functions for ZDDs.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_addExistAbstract()
• Cudd_addUnivAbstract()
• Cudd_addOrAbstract()

• cuddAddExistAbstractRecur()
• cuddAddUnivAbstractRecur()
• cuddAddOrAbstractRecur()

• addCheckPositiveCube()

Cudd_addExistAbstract()

Existentially Abstracts all the variables in cube from f.

Cudd_addUnivAbstract()

Universally Abstracts all the variables in cube from f.

Cudd_addOrAbstract()

Disjunctively abstracts all the variables in cube from the 0-1 ADD f.

cuddAddExistAbstractRecur()

Performs the recursive step of Cudd_addExistAbstract.

cuddAddUnivAbstractRecur()

Performs the recursive step of Cudd_addUnivAbstract.

cuddAddOrAbstractRecur()

Performs the recursive step of Cudd_addOrAbstract.

addCheckPositiveCube()

Checks whether cube is an ADD representing the product of positive literals.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_addApply()
• Cudd_addMonadicApply()
• Cudd_addPlus()
• Cudd_addTimes()
• Cudd_addThreshold()
• Cudd_addSetNZ()
• Cudd_addDivide()
• Cudd_addMinus()
• Cudd_addMinimum()
• Cudd_addMaximum()
• Cudd_addOneZeroMaximum()
• Cudd_addDiff()
• Cudd_addAgreement()
• Cudd_addOr()
• Cudd_addNand()
• Cudd_addNor()
• Cudd_addXor()
• Cudd_addXnor()

• cuddAddApplyRecur()
• cuddAddMonadicApplyRecur()

Cudd_addApply()

Applies op to the corresponding discriminants of f and g.

Cudd_addPlus()

Integer and floating point addition.

Cudd_addTimes()

Integer and floating point multiplication.

Cudd_addThreshold()

f if f>=g; 0 if f<g.

Cudd_addSetNZ()

This operator sets f to the value of g wherever g != 0.

Cudd_addDivide()

Integer and floating point division.

Cudd_addMinus()

Integer and floating point subtraction.

Cudd_addMinimum()

Integer and floating point min.

Cudd_addMaximum()

Integer and floating point max.

Cudd_addOneZeroMaximum()

Returns 1 if f > g and 0 otherwise.

Cudd_addDiff()

Returns plusinfinity if f=g; returns min(f,g) if f!=g.

Cudd_addAgreement()

f if f==g; background if f!=g.

Cudd_addOr()

Disjunction of two 0-1 ADDs.

Cudd_addNand()

NAND of two 0-1 ADDs.

Cudd_addNor()

NOR of two 0-1 ADDs.

Cudd_addXor()

XOR of two 0-1 ADDs.

Cudd_addXnor()

XNOR of two 0-1 ADDs.

Cudd_addMonadicApply()

Applies op to the discriminants of f.

Cudd_addLog()

Natural logarithm of an ADD.

cuddAddApplyRecur()

Performs the recursive step of Cudd_addApply.

cuddAddMonadicApplyRecur()

Performs the recursive step of Cudd_addMonadicApply.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_addFindMax()
• Cudd_addFindMin()
• Cudd_addIthBit()

• addDoIthBit()

Cudd_addFindMax()

Finds the maximum discriminant of f.

Cudd_addFindMin()

Finds the minimum discriminant of f.

Cudd_addIthBit()

Extracts the i-th bit from an ADD.

addDoIthBit()

Performs the recursive step for Cudd_addIthBit.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_addScalarInverse()

• cuddAddScalarInverseRecur()

Cudd_addScalarInverse()

Computes the scalar inverse of an ADD.

cuddAddScalarInverseRecur()

Performs the recursive step of addScalarInverse.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_addIte()
• Cudd_addIteConstant()
• Cudd_addEvalConst()
• Cudd_addCmpl()
• Cudd_addLeq()

• cuddAddIteRecur()
• cuddAddCmplRecur()

• addVarToConst()

Cudd_addIte()

Implements ITE(f,g,h).

Cudd_addIteConstant()

Implements ITEconstant for ADDs.

Cudd_addEvalConst()

Checks whether ADD g is constant whenever ADD f is 1.

Cudd_addCmpl()

Computes the complement of an ADD a la C language.

Cudd_addLeq()

Determines whether f is less than or equal to g.

cuddAddIteRecur()

Implements the recursive step of Cudd_addIte(f,g,h).

cuddAddCmplRecur()

Performs the recursive step of Cudd_addCmpl.

addVarToConst()

Replaces variables with constants if possible (part of canonical form).

By: Fabio Somenzi, Balakrishna Kumthekar

External procedures included in this module:

• Cudd_addNegate()
• Cudd_addRoundOff()

• cuddAddNegateRecur()
• cuddAddRoundOffRecur()

Cudd_addNegate()

Computes the additive inverse of an ADD.

Cudd_addRoundOff()

Rounds off the discriminants of an ADD.

cuddAddNegateRecur()

Implements the recursive step of Cudd_addNegate.

cuddAddRoundOffRecur()

Implements the recursive step of Cudd_addRoundOff.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_addWalsh()
• Cudd_addResidue()

• addWalshInt()

Cudd_addWalsh()

Generates a Walsh matrix in ADD form.

Cudd_addResidue()

Builds an ADD for the residue modulo m of an n-bit number.

addWalshInt()

Implements the recursive step of Cudd_addWalsh.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_bddAndAbstract()
• Cudd_bddAndAbstractLimit()

• cuddBddAndAbstractRecur()

Cudd_bddAndAbstract()

Takes the AND of two BDDs and simultaneously abstracts the variables in cube.

Cudd_bddAndAbstractLimit()

Takes the AND of two BDDs and simultaneously abstracts the variables in cube. Returns NULL if too many nodes are required.

cuddBddAndAbstractRecur()

Takes the AND of two BDDs and simultaneously abstracts the variables in cube.

By: Jae-Young Jang, Jorgen Sivesind

Internal procedures included in this file:

• cuddAnnealing()

• stopping_criterion()
• random_generator()
• ddExchange()
• ddJumpingAux()
• ddJumpingUp()
• ddJumpingDown()
• siftBackwardProb()
• copyOrder()
• restoreOrder()

cuddAnnealing()

Get new variable-order by simulated annealing algorithm.

stopping_criterion()

Checks termination condition.

random_generator()

Random number generator.

ddExchange()

This function is for exchanging two variables, x and y.

ddJumpingAux()

Moves a variable to a specified position.

ddJumpingUp()

This function is for jumping up.

ddJumpingDown()

This function is for jumping down.

siftBackwardProb()

Returns the DD to the best position encountered during sifting if there was improvement.

copyOrder()

Copies the current variable order to array.

restoreOrder()

Restores the variable order in array by a series of sifts up.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_ApaNumberOfDigits()
• Cudd_NewApaNumber()
• Cudd_ApaCopy()
• Cudd_ApaAdd()
• Cudd_ApaSubtract()
• Cudd_ApaShortDivision()
• Cudd_ApaIntDivision()
• Cudd_ApaShiftRight()
• Cudd_ApaSetToLiteral()
• Cudd_ApaPowerOfTwo()
• Cudd_ApaCompare()
• Cudd_ApaCompareRatios()
• Cudd_ApaPrintHex()
• Cudd_ApaPrintDecimal()
• Cudd_ApaPrintExponential()
• Cudd_ApaCountMinterm()
• Cudd_ApaPrintMinterm()
• Cudd_ApaPrintMintermExp()
• Cudd_ApaPrintDensity()

• cuddApaCountMintermAux()
• cuddApaStCountfree()

Cudd_ApaNumberOfDigits()

Finds the number of digits for an arbitrary precision integer.

Cudd_NewApaNumber()

Allocates memory for an arbitrary precision integer.

Cudd_ApaCopy()

Makes a copy of an arbitrary precision integer.

Cudd_ApaAdd()

Adds two arbitrary precision integers.

Cudd_ApaSubtract()

Subtracts two arbitrary precision integers.

Cudd_ApaShortDivision()

Divides an arbitrary precision integer by a digit.

Cudd_ApaIntDivision()

Divides an arbitrary precision integer by an integer.

Cudd_ApaShiftRight()

Shifts right an arbitrary precision integer by one binary place.

Cudd_ApaSetToLiteral()

Sets an arbitrary precision integer to a one-digit literal.

Cudd_ApaPowerOfTwo()

Sets an arbitrary precision integer to a power of two.

Cudd_ApaCompare()

Compares two arbitrary precision integers.

Cudd_ApaCompareRatios()

Compares the ratios of two arbitrary precision integers to two unsigned ints.

Cudd_ApaPrintHex()

Prints an arbitrary precision integer in hexadecimal format.

Cudd_ApaPrintDecimal()

Prints an arbitrary precision integer in decimal format.

Cudd_ApaPrintExponential()

Prints an arbitrary precision integer in exponential format.

Cudd_ApaCountMinterm()

Counts the number of minterms of a DD.

Cudd_ApaPrintMinterm()

Prints the number of minterms of a BDD or ADD using arbitrary precision arithmetic.

Cudd_ApaPrintMintermExp()

Prints the number of minterms of a BDD or ADD in exponential format using arbitrary precision arithmetic.

Cudd_ApaPrintDensity()

Prints the density of a BDD or ADD using arbitrary precision arithmetic.

cuddApaCountMintermAux()

Performs the recursive step of Cudd_ApaCountMinterm.

cuddApaStCountfree()

Frees the memory used to store the minterm counts recorded in the visited table.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_addNewVar()
• Cudd_addNewVarAtLevel()
• Cudd_bddNewVar()
• Cudd_bddNewVarAtLevel()
• Cudd_addIthVar()
• Cudd_bddIthVar()
• Cudd_zddIthVar()
• Cudd_zddVarsFromBddVars()
• Cudd_addConst()
• Cudd_IsNonConstant()
• Cudd_ReadStartTime()
• Cudd_ReadElapsedTime()
• Cudd_SetStartTime()
• Cudd_ResetStartTime()
• Cudd_ReadTimeLimit()
• Cudd_SetTimeLimit()
• Cudd_UpdateTimeLimit()
• Cudd_IncreaseTimeLimit()
• Cudd_UnsetTimeLimit()
• Cudd_TimeLimited()
• Cudd_AutodynEnable()
• Cudd_AutodynDisable()
• Cudd_ReorderingStatus()
• Cudd_AutodynEnableZdd()
• Cudd_AutodynDisableZdd()
• Cudd_ReorderingStatusZdd()
• Cudd_zddRealignmentEnabled()
• Cudd_zddRealignEnable()
• Cudd_zddRealignDisable()
• Cudd_bddRealignmentEnabled()
• Cudd_bddRealignEnable()
• Cudd_bddRealignDisable()
• Cudd_ReadOne()
• Cudd_ReadZddOne()
• Cudd_ReadZero()
• Cudd_ReadLogicZero()
• Cudd_ReadPlusInfinity()
• Cudd_ReadMinusInfinity()
• Cudd_ReadBackground()
• Cudd_SetBackground()
• Cudd_ReadCacheSlots()
• Cudd_ReadCacheUsedSlots()
• Cudd_ReadCacheLookUps()
• Cudd_ReadCacheHits()
• Cudd_ReadMinHit()
• Cudd_SetMinHit()
• Cudd_ReadLooseUpTo()
• Cudd_SetLooseUpTo()
• Cudd_ReadMaxCache()
• Cudd_ReadMaxCacheHard()
• Cudd_SetMaxCacheHard()
• Cudd_ReadSize()
• Cudd_ReadSlots()
• Cudd_ReadUsedSlots()
• Cudd_ExpectedUsedSlots()
• Cudd_ReadKeys()
• Cudd_ReadDead()
• Cudd_ReadMinDead()
• Cudd_ReadReorderings()
• Cudd_ReadMaxReorderings()
• Cudd_SetMaxReorderings()
• Cudd_ReadReorderingTime()
• Cudd_ReadGarbageCollections()
• Cudd_ReadGarbageCollectionTime()
• Cudd_ReadNodesFreed()
• Cudd_ReadNodesDropped()
• Cudd_ReadUniqueLookUps()
• Cudd_ReadUniqueLinks()
• Cudd_ReadSiftMaxVar()
• Cudd_SetSiftMaxVar()
• Cudd_ReadMaxGrowth()
• Cudd_SetMaxGrowth()
• Cudd_ReadMaxGrowthAlternate()
• Cudd_SetMaxGrowthAlternate()
• Cudd_ReadReorderingCycle()
• Cudd_SetReorderingCycle()
• Cudd_ReadTree()
• Cudd_SetTree()
• Cudd_FreeTree()
• Cudd_ReadZddTree()
• Cudd_SetZddTree()
• Cudd_FreeZddTree()
• Cudd_NodeReadIndex()
• Cudd_ReadPerm()
• Cudd_ReadInvPerm()
• Cudd_ReadVars()
• Cudd_ReadEpsilon()
• Cudd_SetEpsilon()
• Cudd_ReadGroupCheck()
• Cudd_SetGroupcheck()
• Cudd_GarbageCollectionEnabled()
• Cudd_EnableGarbageCollection()
• Cudd_DisableGarbageCollection()
• Cudd_DeadAreCounted()
• Cudd_TurnOnCountDead()
• Cudd_TurnOffCountDead()
• Cudd_ReadRecomb()
• Cudd_SetRecomb()
• Cudd_ReadSymmviolation()
• Cudd_SetSymmviolation()
• Cudd_ReadArcviolation()
• Cudd_SetArcviolation()
• Cudd_ReadPopulationSize()
• Cudd_SetPopulationSize()
• Cudd_ReadNumberXovers()
• Cudd_SetNumberXovers()
• Cudd_ReadOrderRandomization()
• Cudd_SetOrderRandomization()
• Cudd_ReadMemoryInUse()
• Cudd_PrintInfo()
• Cudd_ReadPeakNodeCount()
• Cudd_ReadPeakLiveNodeCount()
• Cudd_ReadNodeCount()
• Cudd_zddReadNodeCount()
• Cudd_AddHook()
• Cudd_RemoveHook()
• Cudd_IsInHook()
• Cudd_StdPreReordHook()
• Cudd_StdPostReordHook()
• Cudd_EnableReorderingReporting()
• Cudd_DisableReorderingReporting()
• Cudd_ReorderingReporting()
• Cudd_PrintGroupedOrder()
• Cudd_EnableOrderingMonitoring()
• Cudd_DisableOrderingMonitoring()
• Cudd_OrderingMonitoring()
• Cudd_ReadErrorCode()
• Cudd_ClearErrorCode()
• Cudd_ReadStdout()
• Cudd_SetStdout()
• Cudd_ReadStderr()
• Cudd_SetStderr()
• Cudd_ReadNextReordering()
• Cudd_SetNextReordering()
• Cudd_ReadSwapSteps()
• Cudd_ReadMaxLive()
• Cudd_SetMaxLive()
• Cudd_ReadMaxMemory()
• Cudd_SetMaxMemory()
• Cudd_bddBindVar()
• Cudd_bddUnbindVar()
• Cudd_bddVarIsBound()
• Cudd_bddSetPiVar()
• Cudd_bddSetPsVar()
• Cudd_bddSetNsVar()
• Cudd_bddIsPiVar()
• Cudd_bddIsPsVar()
• Cudd_bddIsNsVar()
• Cudd_bddSetPairIndex()
• Cudd_bddReadPairIndex()
• Cudd_bddSetVarToBeGrouped()
• Cudd_bddSetVarHardGroup()
• Cudd_bddResetVarToBeGrouped()
• Cudd_bddIsVarToBeGrouped()
• Cudd_bddSetVarToBeUngrouped()
• Cudd_bddIsVarToBeUngrouped()
• Cudd_bddIsVarHardGroup()

• fixVarTree()

Cudd_addNewVar()

Returns a new ADD variable.

Cudd_addNewVarAtLevel()

Returns a new ADD variable at a specified level.

Cudd_bddNewVar()

Returns a new BDD variable.

Cudd_bddNewVarAtLevel()

Returns a new BDD variable at a specified level.

Cudd_addIthVar()

Returns the ADD variable with index i.

Cudd_bddIthVar()

Returns the BDD variable with index i.

Cudd_zddIthVar()

Returns the ZDD variable with index i.

Cudd_zddVarsFromBddVars()

Creates one or more ZDD variables for each BDD variable.

Cudd_addConst()

Returns the ADD for constant c.

Cudd_IsNonConstant()

Returns 1 if a DD node is not constant.

Cudd_ReadStartTime()

Returns the start time of the manager.

Cudd_ReadElapsedTime()

Returns the time elapsed since the start time of the manager.

Cudd_SetStartTime()

Sets the start time of the manager.

Cudd_ResetStartTime()

Resets the start time of the manager.

Cudd_ReadTimeLimit()

Returns the time limit for the manager.

Cudd_SetTimeLimit()

Sets the time limit for the manager.

Cudd_UpdateTimeLimit()

Updates the time limit for the manager.

Cudd_IncreaseTimeLimit()

Increases the time limit for the manager.

Cudd_UnsetTimeLimit()

Unsets the time limit for the manager.

Cudd_TimeLimited()

Returns true if the time limit for the manager is set.

Cudd_AutodynEnable()

Enables automatic dynamic reordering of BDDs and ADDs.

Cudd_AutodynDisable()

Disables automatic dynamic reordering.

Cudd_ReorderingStatus()

Reports the status of automatic dynamic reordering of BDDs and ADDs.

Cudd_AutodynEnableZdd()

Enables automatic dynamic reordering of ZDDs.

Cudd_AutodynDisableZdd()

Disables automatic dynamic reordering of ZDDs.

Cudd_ReorderingStatusZdd()

Reports the status of automatic dynamic reordering of ZDDs.

Cudd_zddRealignmentEnabled()

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

Cudd_zddRealignEnable()

Enables realignment of ZDD order to BDD order.

Cudd_zddRealignDisable()

Disables realignment of ZDD order to BDD order.

Cudd_bddRealignmentEnabled()

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

Cudd_bddRealignEnable()

Enables realignment of BDD order to ZDD order.

Cudd_bddRealignDisable()

Disables realignment of ZDD order to BDD order.

Cudd_ReadOne()

Returns the one constant of the manager.

Cudd_ReadZddOne()

Returns the ZDD for the constant 1 function.

Cudd_ReadZero()

Returns the zero constant of the manager.

Cudd_ReadLogicZero()

Returns the logic zero constant of the manager.

Cudd_ReadPlusInfinity()

Reads the plus-infinity constant from the manager.

Cudd_ReadMinusInfinity()

Reads the minus-infinity constant from the manager.

Cudd_ReadBackground()

Reads the background constant of the manager.

Cudd_SetBackground()

Sets the background constant of the manager.

Cudd_ReadCacheSlots()

Reads the number of slots in the cache.

Cudd_ReadCacheUsedSlots()

Reads the fraction of used slots in the cache.

Cudd_ReadCacheLookUps()

Returns the number of cache look-ups.

Cudd_ReadCacheHits()

Returns the number of cache hits.

Cudd_ReadRecursiveCalls()

Returns the number of recursive calls.

Cudd_ReadMinHit()

Reads the hit rate that causes resizinig of the computed table.

Cudd_SetMinHit()

Sets the hit rate that causes resizinig of the computed table.

Cudd_ReadLooseUpTo()

Reads the looseUpTo parameter of the manager.

Cudd_SetLooseUpTo()

Sets the looseUpTo parameter of the manager.

Cudd_ReadMaxCache()

Returns the soft limit for the cache size.

Cudd_ReadMaxCacheHard()

Reads the maxCacheHard parameter of the manager.

Cudd_SetMaxCacheHard()

Sets the maxCacheHard parameter of the manager.

Cudd_ReadSize()

Returns the number of BDD variables in existance.

Cudd_ReadZddSize()

Returns the number of ZDD variables in existance.

Cudd_ReadSlots()

Returns the total number of slots of the unique table.

Cudd_ReadUsedSlots()

Reads the fraction of used slots in the unique table.

Cudd_ExpectedUsedSlots()

Computes the expected fraction of used slots in the unique table.

Cudd_ReadKeys()

Returns the number of nodes in the unique table.

Cudd_ReadDead()

Returns the number of dead nodes in the unique table.

Cudd_ReadMinDead()

Reads the minDead parameter of the manager.

Cudd_ReadReorderings()

Returns the number of times reordering has occurred.

Cudd_ReadMaxReorderings()

Returns the maximum number of times reordering may be invoked.

Cudd_SetMaxReorderings()

Sets the maximum number of times reordering may be invoked.

Cudd_ReadReorderingTime()

Returns the time spent in reordering.

Cudd_ReadGarbageCollections()

Returns the number of times garbage collection has occurred.

Cudd_ReadGarbageCollectionTime()

Returns the time spent in garbage collection.

Cudd_ReadNodesFreed()

Returns the number of nodes freed.

Cudd_ReadNodesDropped()

Returns the number of nodes dropped.

Cudd_ReadUniqueLookUps()

Returns the number of look-ups in the unique table.

Cudd_ReadUniqueLinks()

Returns the number of links followed in the unique table.

Cudd_ReadSiftMaxVar()

Reads the siftMaxVar parameter of the manager.

Cudd_SetSiftMaxVar()

Sets the siftMaxVar parameter of the manager.

Cudd_ReadSiftMaxSwap()

Reads the siftMaxSwap parameter of the manager.

Cudd_SetSiftMaxSwap()

Sets the siftMaxSwap parameter of the manager.

Cudd_ReadMaxGrowth()

Reads the maxGrowth parameter of the manager.

Cudd_SetMaxGrowth()

Sets the maxGrowth parameter of the manager.

Cudd_ReadMaxGrowthAlternate()

Reads the maxGrowthAlt parameter of the manager.

Cudd_SetMaxGrowthAlternate()

Sets the maxGrowthAlt parameter of the manager.

Cudd_ReadReorderingCycle()

Reads the reordCycle parameter of the manager.

Cudd_SetReorderingCycle()

Sets the reordCycle parameter of the manager.

Cudd_ReadTree()

Returns the variable group tree of the manager.

Cudd_SetTree()

Sets the variable group tree of the manager.

Cudd_FreeTree()

Frees the variable group tree of the manager.

Cudd_ReadZddTree()

Returns the variable group tree of the manager.

Cudd_SetZddTree()

Sets the ZDD variable group tree of the manager.

Cudd_FreeZddTree()

Frees the variable group tree of the manager.

Cudd_NodeReadIndex()

Returns the index of the node.

Cudd_ReadPerm()

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

Cudd_ReadPermZdd()

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

Cudd_ReadInvPerm()

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

Cudd_ReadInvPermZdd()

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

Cudd_ReadVars()

Returns the i-th element of the vars array.

Cudd_ReadEpsilon()

Reads the epsilon parameter of the manager.

Cudd_SetEpsilon()

Sets the epsilon parameter of the manager to ep.

Cudd_ReadGroupcheck()

Reads the groupcheck parameter of the manager.

Cudd_SetGroupcheck()

Sets the parameter groupcheck of the manager to gc.

Cudd_GarbageCollectionEnabled()

Tells whether garbage collection is enabled.

Cudd_EnableGarbageCollection()

Enables garbage collection.

Cudd_DisableGarbageCollection()

Disables garbage collection.

Cudd_DeadAreCounted()

Tells whether dead nodes are counted towards triggering reordering.

Cudd_TurnOnCountDead()

Causes the dead nodes to be counted towards triggering reordering.

Cudd_TurnOffCountDead()

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

Cudd_ReadRecomb()

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

Cudd_SetRecomb()

Sets the value of the recombination parameter used in group sifting.

Cudd_ReadSymmviolation()

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

Cudd_SetSymmviolation()

Sets the value of the symmviolation parameter used in group sifting.

Cudd_ReadArcviolation()

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

Cudd_SetArcviolation()

Sets the value of the arcviolation parameter used in group sifting.

Cudd_ReadPopulationSize()

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

Cudd_SetPopulationSize()

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

Cudd_ReadNumberXovers()

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

Cudd_SetNumberXovers()

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

Cudd_ReadOrderRandomization()

Returns the order randomization factor.

Cudd_SetOrderRandomization()

Sets the order randomization factor.

Cudd_ReadMemoryInUse()

Returns the memory in use by the manager measured in bytes.

Cudd_PrintInfo()

Prints out statistics and settings for a CUDD manager.

Cudd_ReadPeakNodeCount()

Reports the peak number of nodes.

Cudd_ReadPeakLiveNodeCount()

Reports the peak number of live nodes.

Cudd_ReadNodeCount()

Reports the number of nodes in BDDs and ADDs.

Cudd_zddReadNodeCount()

Reports the number of nodes in ZDDs.

Cudd_AddHook()

Adds a function to a hook.

Cudd_RemoveHook()

Removes a function from a hook.

Cudd_IsInHook()

Checks whether a function is in a hook.

Cudd_StdPreReordHook()

Sample hook function to call before reordering.

Cudd_StdPostReordHook()

Sample hook function to call after reordering.

Cudd_EnableReorderingReporting()

Enables reporting of reordering stats.

Cudd_DisableReorderingReporting()

Disables reporting of reordering stats.

Cudd_ReorderingReporting()

Returns 1 if reporting of reordering stats is enabled.

Cudd_PrintGroupedOrder()

Hook function to print the current variable order.

Cudd_EnableOrderingMonitoring()

Enables monitoring of ordering.

Cudd_DisableOrderingMonitoring()

Disables monitoring of ordering.

Cudd_OrderingMonitoring()

Returns 1 if monitoring of ordering is enabled.

Cudd_ReadErrorCode()

Returns the code of the last error.

Cudd_ClearErrorCode()

Clear the error code of a manager.

Cudd_ReadStdout()

Reads the stdout of a manager.

Cudd_SetStdout()

Sets the stdout of a manager.

Cudd_ReadStderr()

Reads the stderr of a manager.

Cudd_SetStderr()

Sets the stderr of a manager.

Cudd_ReadNextReordering()

Returns the threshold for the next dynamic reordering.

Cudd_SetNextReordering()

Sets the threshold for the next dynamic reordering.

Cudd_ReadSwapSteps()

Reads the number of elementary reordering steps.

Cudd_ReadMaxLive()

Reads the maximum allowed number of live nodes.

Cudd_SetMaxLive()

Sets the maximum allowed number of live nodes.

Cudd_ReadMaxMemory()

Reads the maximum allowed memory.

Cudd_SetMaxMemory()

Sets the maximum allowed memory.

Cudd_bddBindVar()

Prevents sifting of a variable.

Cudd_bddUnbindVar()

Allows the sifting of a variable.

Cudd_bddVarIsBound()

Tells whether a variable can be sifted.

Cudd_bddSetPiVar()

Sets a variable type to primary input.

Cudd_bddSetPsVar()

Sets a variable type to present state.

Cudd_bddSetNsVar()

Sets a variable type to next state.

Cudd_bddIsPiVar()

Checks whether a variable is primary input.

Cudd_bddIsPsVar()

Checks whether a variable is present state.

Cudd_bddIsNsVar()

Checks whether a variable is next state.

Cudd_bddSetPairIndex()

Sets a corresponding pair index for a given index.

Cudd_bddReadPairIndex()

Reads a corresponding pair index for a given index.

Cudd_bddSetVarToBeGrouped()

Sets a variable to be grouped.

Cudd_bddSetVarHardGroup()

Sets a variable to be a hard group.

Cudd_bddResetVarToBeGrouped()

Resets a variable not to be grouped.

Cudd_bddIsVarToBeGrouped()

Checks whether a variable is set to be grouped.

Cudd_bddSetVarToBeUngrouped()

Sets a variable to be ungrouped.

Cudd_bddIsVarToBeUngrouped()

Checks whether a variable is set to be ungrouped.

Cudd_bddIsVarHardGroup()

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

fixVarTree()

Fixes a variable group tree.

addMultiplicityGroups()

Adds multiplicity groups to a ZDD variable group tree.

By: Fabio Somenzi

External procedures provided by this module:

• Cudd_UnderApprox()
• Cudd_OverApprox()
• Cudd_RemapUnderApprox()
• Cudd_RemapOverApprox()
• Cudd_BiasedUnderApprox()
• Cudd_BiasedOverApprox()

• cuddUnderApprox()
• cuddRemapUnderApprox()
• cuddBiasedUnderApprox()

• updateParity()
• gatherInfoAux()
• gatherInfo()
• computeSavings()
• updateRefs()
• UAmarkNodes()
• UAbuildSubset()
• RAmarkNodes()
• BAmarkNodes()
• RAbuildSubset()
• BAapplyBias()

See AlsocuddSubsetHB.c cuddSubsetSP.c cuddGenCof.c

Cudd_UnderApprox()

Extracts a dense subset from a BDD with Shiple's underapproximation method.

Cudd_OverApprox()

Extracts a dense superset from a BDD with Shiple's underapproximation method.

Cudd_RemapUnderApprox()

Extracts a dense subset from a BDD with the remapping underapproximation method.

Cudd_RemapOverApprox()

Extracts a dense superset from a BDD with the remapping underapproximation method.

Cudd_BiasedUnderApprox()

Extracts a dense subset from a BDD with the biased underapproximation method.

Cudd_BiasedOverApprox()

Extracts a dense superset from a BDD with the biased underapproximation method.

cuddUnderApprox()

Applies Tom Shiple's underappoximation algorithm.

cuddRemapUnderApprox()

Applies the remapping underappoximation algorithm.

cuddBiasedUnderApprox()

Applies the biased remapping underappoximation algorithm.

updateParity()

Recursively update the parity of the paths reaching a node.

gatherInfoAux()

Recursively counts minterms and computes reference counts of each node in the BDD.

gatherInfo()

Gathers information about each node.

computeSavings()

Counts the nodes that would be eliminated if a given node were replaced by zero.

updateRefs()

Update function reference counts.

UAmarkNodes()

Marks nodes for replacement by zero.

UAbuildSubset()

Builds the subset BDD.

RAmarkNodes()

Marks nodes for remapping.

BAmarkNodes()

Marks nodes for remapping.

RAbuildSubset()

Builds the subset BDD for cuddRemapUnderApprox.

BAapplyBias()

Finds don't care nodes.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_bddExistAbstract()
• Cudd_bddExistAbstractLimit()
• Cudd_bddXorExistAbstract()
• Cudd_bddUnivAbstract()
• Cudd_bddBooleanDiff()
• Cudd_bddVarIsDependent()

• cuddBddExistAbstractRecur()
• cuddBddXorExistAbstractRecur()
• cuddBddBooleanDiffRecur()

• bddCheckPositiveCube()

Cudd_bddExistAbstract()

Existentially abstracts all the variables in cube from f.

Cudd_bddExistAbstractLimit()

Existentially abstracts all the variables in cube from f.

Cudd_bddXorExistAbstract()

Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube.

Cudd_bddUnivAbstract()

Universally abstracts all the variables in cube from f.

Cudd_bddBooleanDiff()

Computes the boolean difference of f with respect to x.

Cudd_bddVarIsDependent()

Checks whether a variable is dependent on others in a function.

cuddBddExistAbstractRecur()

Performs the recursive steps of Cudd_bddExistAbstract.

cuddBddXorExistAbstractRecur()

Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube.

cuddBddBooleanDiffRecur()

Performs the recursive steps of Cudd_bddBoleanDiff.

bddCheckPositiveCube()

Checks whether cube is an BDD representing the product of positive literals.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_bddCorrelation()
• Cudd_bddCorrelationWeights()

• bddCorrelationAux()
• bddCorrelationWeightsAux()
• CorrelCompare()
• CorrelHash()
• CorrelCleanUp()

Cudd_bddCorrelation()

Computes the correlation of f and g.

Cudd_bddCorrelationWeights()

Computes the correlation of f and g for given input probabilities.

bddCorrelationAux()

Performs the recursive step of Cudd_bddCorrelation.

bddCorrelationWeightsAux()

Performs the recursive step of Cudd_bddCorrelationWeigths.

CorrelCompare()

Compares two hash table entries.

CorrelHash()

Hashes a hash table entry.

CorrelCleanUp()

Frees memory associated with hash table.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_bddIte()
• Cudd_bddIteLimit()
• Cudd_bddIteConstant()
• Cudd_bddIntersect()
• Cudd_bddAnd()
• Cudd_bddAndLimit()
• Cudd_bddOr()
• Cudd_bddOrLimit()
• Cudd_bddNand()
• Cudd_bddNor()
• Cudd_bddXor()
• Cudd_bddXnor()
• Cudd_bddXnorLimit()
• Cudd_bddLeq()

• cuddBddIteRecur()
• cuddBddIntersectRecur()
• cuddBddAndRecur()
• cuddBddXorRecur()

• bddVarToConst()
• bddVarToCanonical()
• bddVarToCanonicalSimple()

Cudd_bddIte()

Implements ITE(f,g,h).

Cudd_bddIteLimit()

Implements ITE(f,g,h). Returns NULL if too many nodes are required.

Cudd_bddIteConstant()

Implements ITEconstant(f,g,h).

Cudd_bddIntersect()

Returns a function included in the intersection of f and g.

Cudd_bddAnd()

Computes the conjunction of two BDDs f and g.

Cudd_bddAndLimit()

Computes the conjunction of two BDDs f and g. Returns NULL if too many nodes are required.

Cudd_bddOr()

Computes the disjunction of two BDDs f and g.

Cudd_bddOrLimit()

Computes the disjunction of two BDDs f and g. Returns NULL if too many nodes are required.

Cudd_bddNand()

Computes the NAND of two BDDs f and g.

Cudd_bddNor()

Computes the NOR of two BDDs f and g.

Cudd_bddXor()

Computes the exclusive OR of two BDDs f and g.

Cudd_bddXnor()

Computes the exclusive NOR of two BDDs f and g.

Cudd_bddXnorLimit()

Computes the exclusive NOR of two BDDs f and g. Returns NULL if too many nodes are required.

Cudd_bddLeq()

Determines whether f is less than or equal to g.

cuddBddIteRecur()

Implements the recursive step of Cudd_bddIte.

cuddBddIntersectRecur()

Implements the recursive step of Cudd_bddIntersect.

cuddBddAndRecur()

Implements the recursive step of Cudd_bddAnd.

cuddBddXorRecur()

Implements the recursive step of Cudd_bddXor.

bddVarToConst()

Replaces variables with constants if possible.

bddVarToCanonical()

Picks unique member from equiv expressions.

bddVarToCanonicalSimple()

Picks unique member from equiv expressions.

By: Fabio Somenzi

External procedures included in this file:

• Cudd_addBddThreshold()
• Cudd_addBddStrictThreshold()
• Cudd_addBddInterval()
• Cudd_addBddIthBit()
• Cudd_BddToAdd()
• Cudd_addBddPattern()
• Cudd_bddTransfer()

• cuddBddTransfer()
• cuddAddBddDoPattern()

• addBddDoThreshold()
• addBddDoStrictThreshold()
• addBddDoInterval()
• addBddDoIthBit()
• ddBddToAddRecur()
• cuddBddTransferRecur()

Cudd_addBddThreshold()

Converts an ADD to a BDD.

Cudd_addBddStrictThreshold()

Converts an ADD to a BDD.

Cudd_addBddInterval()

Converts an ADD to a BDD.

Cudd_addBddIthBit()

Converts an ADD to a BDD by extracting the i-th bit from the leaves.

Cudd_BddToAdd()

Converts a BDD to a 0-1 ADD.

Cudd_addBddPattern()

Converts an ADD to a BDD.

Cudd_bddTransfer()

Convert a BDD from a manager to another one.

cuddBddTransfer()

Convert a BDD from a manager to another one.

cuddAddBddDoPattern()

Performs the recursive step for Cudd_addBddPattern.

addBddDoThreshold()

Performs the recursive step for Cudd_addBddThreshold.

addBddDoStrictThreshold()

Performs the recursive step for Cudd_addBddStrictThreshold.

addBddDoInterval()

Performs the recursive step for Cudd_addBddInterval.

addBddDoIthBit()

Performs the recursive step for Cudd_addBddIthBit.

ddBddToAddRecur()

Performs the recursive step for Cudd_BddToAdd.

cuddBddTransferRecur()

Performs the recursive step of Cudd_bddTransfer.

By: Fabio Somenzi

Internal procedures included in this module:

• cuddInitCache()
• cuddCacheInsert()
• cuddCacheInsert2()
• cuddCacheLookup()
• cuddCacheLookupZdd()
• cuddCacheLookup2()
• cuddCacheLookup2Zdd()
• cuddConstantLookup()
• cuddCacheProfile()
• cuddCacheResize()
• cuddCacheFlush()
• cuddComputeFloorLog2()

cuddInitCache()

Initializes the computed table.

cuddCacheInsert()

Inserts a result in the cache for a function with three operands.

cuddCacheInsert2()

Inserts a result in the cache for a function with two operands.

cuddCacheInsert1()

Inserts a result in the cache for a function with two operands.

cuddCacheLookup()

Looks up in the cache for the result of op applied to f, g, and h.

cuddCacheLookupZdd()

Looks up in the cache for the result of op applied to f, g, and h.

cuddCacheLookup2()

Looks up in the cache for the result of op applied to f and g.

cuddCacheLookup1()

Looks up in the cache for the result of op applied to f.

cuddCacheLookup2Zdd()

Looks up in the cache for the result of op applied to f and g.

cuddCacheLookup1Zdd()

Looks up in the cache for the result of op applied to f.

cuddConstantLookup()

Looks up in the cache for the result of op applied to f, g, and h.

cuddCacheProfile()

Computes and prints a profile of the cache usage.

cuddCacheResize()

Resizes the cache.

cuddCacheFlush()

Flushes the cache.

cuddComputeFloorLog2()

Returns the floor of the logarithm to the base 2.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_DebugCheck()
• Cudd_CheckKeys()

• cuddHeapProfile()
• cuddPrintNode()
• cuddPrintVarGroups()

• debugFindParent()

Cudd_DebugCheck()

Checks for inconsistencies in the DD heap.

Cudd_CheckKeys()

Checks for several conditions that should not occur.

cuddHeapProfile()

Prints information about the heap.

cuddPrintNode()

Prints out information on a node.

cuddPrintVarGroups()

Prints the variable groups as a parenthesized list.

debugFindParent()

Searches the subtables above node for its parents.

debugCheckParent()

Reports an error if a (dead) node has a non-dead parent.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_bddClippingAnd()
• Cudd_bddClippingAndAbstract()

• cuddBddClippingAnd()
• cuddBddClippingAndAbstract()

• cuddBddClippingAndRecur()
• cuddBddClipAndAbsRecur()

Cudd_bddClippingAnd()

Approximates the conjunction of two BDDs f and g.

Cudd_bddClippingAndAbstract()

Approximates the conjunction of two BDDs f and g and simultaneously abstracts the variables in cube.

cuddBddClippingAnd()

Approximates the conjunction of two BDDs f and g.

cuddBddClippingAndAbstract()

Approximates the conjunction of two BDDs f and g and simultaneously abstracts the variables in cube.

cuddBddClippingAndRecur()

Implements the recursive step of Cudd_bddClippingAnd.

cuddBddClipAndAbsRecur()

Approximates the AND of two BDDs and simultaneously abstracts the variables in cube.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_Cofactor()
• Cudd_CheckCube()

• cuddGetBranches()
• cuddCofactorRecur()

Cudd_Cofactor()

Computes the cofactor of f with respect to g.

Cudd_CheckCube()

Checks whether g is the BDD of a cube.

cuddGetBranches()

Computes the children of g.

cuddCofactorRecur()

Performs the recursive step of Cudd_Cofactor.

By: Fabio Somenzi and Kavita Ravi

External procedures included in this module:

• Cudd_bddCompose()
• Cudd_addCompose()
• Cudd_addPermute()
• Cudd_addSwapVariables()
• Cudd_bddPermute()
• Cudd_bddVarMap()
• Cudd_SetVarMap()
• Cudd_bddSwapVariables()
• Cudd_bddAdjPermuteX()
• Cudd_addVectorCompose()
• Cudd_addGeneralVectorCompose()
• Cudd_addNonSimCompose()
• Cudd_bddVectorCompose()

• cuddBddComposeRecur()
• cuddAddComposeRecur()

• cuddAddPermuteRecur()
• cuddBddPermuteRecur()
• cuddBddVarMapRecur()
• cuddAddVectorComposeRecur()
• cuddAddGeneralVectorComposeRecur()
• cuddAddNonSimComposeRecur()
• cuddBddVectorComposeRecur()
• ddIsIthAddVar()
• ddIsIthAddVarPair()

Cudd_bddCompose()

Substitutes g for x_v in the BDD for f.

Cudd_addCompose()

Substitutes g for x_v in the ADD for f.

Cudd_addPermute()

Permutes the variables of an ADD.

Cudd_addSwapVariables()

Swaps two sets of variables of the same size (x and y) in the ADD f.

Cudd_bddPermute()

Permutes the variables of a BDD.

Cudd_bddVarMap()

Remaps the variables of a BDD using the default variable map.

Cudd_SetVarMap()

Registers a variable mapping with the manager.

Cudd_bddSwapVariables()

Swaps two sets of variables of the same size (x and y) in the BDD f.

Cudd_bddAdjPermuteX()

Rearranges a set of variables in the BDD B.

Cudd_addVectorCompose()

Composes an ADD with a vector of 0-1 ADDs.

Cudd_addGeneralVectorCompose()

Composes an ADD with a vector of ADDs.

Cudd_addNonSimCompose()

Composes an ADD with a vector of 0-1 ADDs.

Cudd_bddVectorCompose()

Composes a BDD with a vector of BDDs.

cuddBddComposeRecur()

Performs the recursive step of Cudd_bddCompose.

cuddAddComposeRecur()

Performs the recursive step of Cudd_addCompose.

cuddAddPermuteRecur()

Implements the recursive step of Cudd_addPermute.

cuddBddPermuteRecur()

Implements the recursive step of Cudd_bddPermute.

cuddBddVarMapRecur()

Implements the recursive step of Cudd_bddVarMap.

cuddAddVectorComposeRecur()

Performs the recursive step of Cudd_addVectorCompose.

cuddAddGeneralVectorComposeRecur()

Performs the recursive step of Cudd_addGeneralVectorCompose.

cuddAddNonSimComposeRecur()

Performs the recursive step of Cudd_addNonSimCompose.

cuddBddVectorComposeRecur()

Performs the recursive step of Cudd_bddVectorCompose.

()

Comparison of a function to the i-th ADD variable.

()

Comparison of a pair of functions to the i-th ADD variable.

By: Kavita Ravi, Fabio Somenzi

External procedures included in this file:

• Cudd_bddApproxConjDecomp()
• Cudd_bddApproxDisjDecomp()
• Cudd_bddIterConjDecomp()
• Cudd_bddIterDisjDecomp()
• Cudd_bddGenConjDecomp()
• Cudd_bddGenDisjDecomp()
• Cudd_bddVarConjDecomp()
• Cudd_bddVarDisjDecomp()

• cuddConjunctsAux()
• CreateBotDist()
• BuildConjuncts()
• ConjunctsFree()

Cudd_bddApproxConjDecomp()

Performs two-way conjunctive decomposition of a BDD.

Cudd_bddApproxDisjDecomp()

Performs two-way disjunctive decomposition of a BDD.

Cudd_bddIterConjDecomp()

Performs two-way conjunctive decomposition of a BDD.

Cudd_bddIterDisjDecomp()

Performs two-way disjunctive decomposition of a BDD.

Cudd_bddGenConjDecomp()

Performs two-way conjunctive decomposition of a BDD.

Cudd_bddGenDisjDecomp()

Performs two-way disjunctive decomposition of a BDD.

Cudd_bddVarConjDecomp()

Performs two-way conjunctive decomposition of a BDD.

Cudd_bddVarDisjDecomp()

Performs two-way disjunctive decomposition of a BDD.

CreateBotDist()

Get longest distance of node from constant.

CountMinterms()

Count the number of minterms of each node ina a BDD and store it in a hash table.

ConjunctsFree()

Free factors structure

PairInTables()

Check whether the given pair is in the tables.

CheckTablesCacheAndReturn()

Check the tables for the existence of pair and return one combination, cache the result.

PickOnePair()

Check the tables for the existence of pair and return one combination, store in cache.

CheckInTables()

Check if the two pairs exist in the table, If any of the conjuncts do exist, store in the cache and return the corresponding pair.

ZeroCase()

If one child is zero, do explicitly what Restrict does or better

BuildConjuncts()

Builds the conjuncts recursively, bottom up.

cuddConjunctsAux()

Procedure to compute two conjunctive factors of f and place in *c1 and *c2.

By: Fabio Somenzi

External procedures included in this file:

• Cudd_FindEssential()
• Cudd_bddIsVarEssential()
• Cudd_FindTwoLiteralClauses()
• Cudd_ReadIthClause()
• Cudd_PrintTwoLiteralClauses()
• Cudd_tlcInfoFree()

• ddFindEssentialRecur()
• ddFindTwoLiteralClausesRecur()
• computeClauses()
• computeClausesWithUniverse()
• emptyClauseSet()
• sentinelp()
• equalp()
• beforep()
• oneliteralp()
• impliedp()
• bitVectorAlloc()
• bitVectorClear()
• bitVectorFree()
• bitVectorRead()
• bitVectorSet()
• tlcInfoAlloc()

Cudd_FindEssential()

Finds the essential variables of a DD.

Cudd_bddIsVarEssential()

Determines whether a given variable is essential with a given phase in a BDD.

Cudd_FindTwoLiteralClauses()

Finds the two literal clauses of a DD.

Cudd_ReadIthClause()

Accesses the i-th clause of a DD.

Cudd_PrintTwoLiteralClauses()

Prints the two literal clauses of a DD.

Cudd_tlcInfoFree()

Frees a DdTlcInfo Structure.

ddFindEssentialRecur()

Implements the recursive step of Cudd_FindEssential.

ddFindTwoLiteralClausesRecur()

Implements the recursive step of Cudd_FindTwoLiteralClauses.

computeClauses()

Computes the two-literal clauses for a node.

computeClausesWithUniverse()

Computes the two-literal clauses for a node.

emptyClauseSet()

Returns an enpty set of clauses.

sentinelp()

Returns true iff the argument is the sentinel clause.

equalp()

Returns true iff the two arguments are identical clauses.

beforep()

Returns true iff the first argument precedes the second in the clause order.

oneliteralp()

Returns true iff the argument is a one-literal clause.

impliedp()

Returns true iff either literal of a clause is in a set of literals.

bitVectorAlloc()

Allocates a bit vector.

()

Clears a bit vector.

bitVectorFree()

Frees a bit vector.

()

Returns the i-th entry of a bit vector.

()

Sets the i-th entry of a bit vector to a value.

tlcInfoAlloc()

Allocates a DdTlcInfo Structure.

By: Cheng Hua, Fabio Somenzi

External procedures included in this file:

• cuddExact()

• getMaxBinomial()
• gcd()
• getMatrix()
• freeMatrix()
• getLevelKeys()
• ddShuffle()
• ddSiftUp()
• updateUB()
• ddCountRoots()
• ddClearGlobal()
• computeLB()
• updateEntry()
• pushDown()
• initSymmInfo()

cuddExact()

Exact variable ordering algorithm.

getMaxBinomial()

Returns the maximum value of (n choose k) for a given n.

gcd()

Returns the gcd of two integers.

getMatrix()

Allocates a two-dimensional matrix of ints.

freeMatrix()

Frees a two-dimensional matrix allocated by getMatrix.

getLevelKeys()

Returns the number of nodes at one level of a unique table.

ddShuffle()

Reorders variables according to a given permutation.

ddSiftUp()

Moves one variable up.

updateUB()

Updates the upper bound and saves the best order seen so far.

ddCountRoots()

Counts the number of roots.

ddClearGlobal()

Scans the DD and clears the LSB of the next pointers.

computeLB()

Computes a lower bound on the size of a BDD.

updateEntry()

Updates entry for a subset.

pushDown()

Pushes a variable in the order down to position "level."

initSymmInfo()

Gathers symmetry information.

checkSymmInfo()

Check symmetry condition.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_DumpBlif()
• Cudd_DumpBlifBody()
• Cudd_DumpDot()
• Cudd_DumpDaVinci()
• Cudd_DumpDDcal()
• Cudd_DumpFactoredForm()

• ddDoDumpBlif()
• ddDoDumpDaVinci()
• ddDoDumpDDcal()
• ddDoDumpFactoredForm()

Cudd_DumpBlif()

Writes a blif file representing the argument BDDs.

Cudd_DumpBlifBody()

Writes a blif body representing the argument BDDs.

Cudd_DumpDot()

Writes a dot file representing the argument DDs.

Cudd_DumpDaVinci()

Writes a daVinci file representing the argument BDDs.

Cudd_DumpDDcal()

Writes a DDcal file representing the argument BDDs.

Cudd_DumpFactoredForm()

Writes factored forms representing the argument BDDs.

ddDoDumpBlif()

Performs the recursive step of Cudd_DumpBlif.

ddDoDumpDaVinci()

Performs the recursive step of Cudd_DumpDaVinci.

ddDoDumpDDcal()

Performs the recursive step of Cudd_DumpDDcal.

ddDoDumpFactoredForm()

Performs the recursive step of Cudd_DumpFactoredForm.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_bddConstrain()
• Cudd_bddRestrict()
• Cudd_bddNPAnd()
• Cudd_addConstrain()
• Cudd_bddConstrainDecomp()
• Cudd_addRestrict()
• Cudd_bddCharToVect()
• Cudd_bddLICompaction()
• Cudd_bddSqueeze()
• Cudd_bddMinimize()
• Cudd_SubsetCompress()
• Cudd_SupersetCompress()

• cuddBddConstrainRecur()
• cuddBddRestrictRecur()
• cuddBddNPAndRecur()
• cuddAddConstrainRecur()
• cuddAddRestrictRecur()
• cuddBddLICompaction()

• cuddBddConstrainDecomp()
• cuddBddCharToVect()
• cuddBddLICMarkEdges()
• cuddBddLICBuildResult()
• MarkCacheHash()
• MarkCacheCompare()
• MarkCacheCleanUp()
• cuddBddSqueeze()

Cudd_bddConstrain()

Computes f constrain c.

Cudd_bddRestrict()

BDD restrict according to Coudert and Madre's algorithm (ICCAD90).

Cudd_bddNPAnd()

Computes f non-polluting-and g.

Cudd_addConstrain()

Computes f constrain c for ADDs.

Cudd_bddConstrainDecomp()

BDD conjunctive decomposition as in McMillan's CAV96 paper.

Cudd_addRestrict()

ADD restrict according to Coudert and Madre's algorithm (ICCAD90).

Cudd_bddCharToVect()

Computes a vector whose image equals a non-zero function.

Cudd_bddLICompaction()

Performs safe minimization of a BDD.

Cudd_bddSqueeze()

Finds a small BDD in a function interval.

Cudd_bddMinimize()

Finds a small BDD that agrees with f over c.

Cudd_SubsetCompress()

Find a dense subset of BDD f.

Cudd_SupersetCompress()

Find a dense superset of BDD f.

cuddBddConstrainRecur()

Performs the recursive step of Cudd_bddConstrain.

cuddBddRestrictRecur()

Performs the recursive step of Cudd_bddRestrict.

cuddBddNPAndRecur()

Implements the recursive step of Cudd_bddAnd.

cuddAddConstrainRecur()

Performs the recursive step of Cudd_addConstrain.

cuddAddRestrictRecur()

Performs the recursive step of Cudd_addRestrict.

cuddBddLICompaction()

Performs safe minimization of a BDD.

cuddBddConstrainDecomp()

Performs the recursive step of Cudd_bddConstrainDecomp.

cuddBddCharToVect()

Performs the recursive step of Cudd_bddCharToVect.

cuddBddLICMarkEdges()

Performs the edge marking step of Cudd_bddLICompaction.

cuddBddLICBuildResult()

Builds the result of Cudd_bddLICompaction.

MarkCacheHash()

Hash function for the computed table of cuddBddLICMarkEdges.

MarkCacheCompare()

Comparison function for the computed table of cuddBddLICMarkEdges.

MarkCacheCleanUp()

Frees memory associated with computed table of cuddBddLICMarkEdges.

cuddBddSqueeze()

Performs the recursive step of Cudd_bddSqueeze.

By: Curt Musfeldt, Alan Shuler, Fabio Somenzi

Internal procedures included in this file:

• cuddGa()

• make_random()
• sift_up()
• build_dd()
• largest()
• rand_int()
• array_hash()
• array_compare()
• find_best()
• find_average_fitness()
• PMX()
• roulette()

cuddGa()

Genetic algorithm for DD reordering.

make_random()

Generates the random sequences for the initial population.

sift_up()

Moves one variable up.

build_dd()

Builds a DD from a given order.

largest()

Finds the largest DD in the population.

rand_int()

Generates a random number between 0 and the integer a.

array_hash()

Hash function for the computed table.

array_compare()

Comparison function for the computed table.

find_best()

Returns the index of the fittest individual.

()

Returns the average fitness of the population.

PMX()

Performs the crossover between two parents.

roulette()

Selects two parents with the roulette wheel method.

By: Shipra Panda, Fabio Somenzi

External procedures included in this file:

• Cudd_MakeTreeNode()

• cuddTreeSifting()

• ddTreeSiftingAux()
• ddCountInternalMtrNodes()
• ddReorderChildren()
• ddFindNodeHiLo()
• ddUniqueCompareGroup()
• ddGroupSifting()
• ddCreateGroup()
• ddGroupSiftingAux()
• ddGroupSiftingUp()
• ddGroupSiftingDown()
• ddGroupMove()
• ddGroupMoveBackward()
• ddGroupSiftingBackward()
• ddMergeGroups()
• ddDissolveGroup()
• ddNoCheck()
• ddSecDiffCheck()
• ddExtSymmCheck()
• ddVarGroupCheck()
• ddSetVarHandled()
• ddResetVarHandled()
• ddIsVarHandled()
• ddFixTree()

Cudd_MakeTreeNode()

Creates a new variable group.

cuddTreeSifting()

Tree sifting algorithm.

ddTreeSiftingAux()

Visits the group tree and reorders each group.

ddCountInternalMtrNodes()

Counts the number of internal nodes of the group tree.

ddReorderChildren()

Reorders the children of a group tree node according to the options.

ddFindNodeHiLo()

Finds the lower and upper bounds of the group represented by treenode.

ddUniqueCompareGroup()

Comparison function used by qsort.

ddGroupSifting()

Sifts from treenode->low to treenode->high.

ddCreateGroup()

Creates a group encompassing variables from x to y in the DD table.

ddGroupSiftingAux()

Sifts one variable up and down until it has taken all positions. Checks for aggregation.

ddGroupSiftingUp()

Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much.

ddGroupSiftingDown()

Sifts down a variable until it reaches position xHigh.

ddGroupMove()

Swaps two groups and records the move.

ddGroupMoveBackward()

Undoes the swap two groups.

ddGroupSiftingBackward()

Determines the best position for a variables and returns it there.

ddMergeGroups()

Merges groups in the DD table.

ddDissolveGroup()

Dissolves a group in the DD table.

ddNoCheck()

Pretends to check two variables for aggregation.

ddSecDiffCheck()

Checks two variables for aggregation.

ddExtSymmCheck()

Checks for extended symmetry of x and y.

ddVarGroupCheck()

Checks for grouping of x and y.

ddSetVarHandled()

Sets a variable to already handled.

ddResetVarHandled()

Resets a variable to be processed.

ddIsVarHandled()

Checks whether a variables is already handled.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_addHarwell()

Cudd_addHarwell()

Reads in a matrix in the format of the Harwell-Boeing benchmark suite.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_Init()
• Cudd_Quit()

• cuddZddInitUniv()
• cuddZddFreeUniv()

Cudd_Init()

Creates a new DD manager.

Cudd_Quit()

Deletes resources associated with a DD manager.

cuddZddInitUniv()

Initializes the ZDD universe.

cuddZddFreeUniv()

Frees the ZDD universe.

By: Fabio Somenzi

Internal procedures included in this file:

• cuddSetInteract()
• cuddTestInteract()
• cuddInitInteract()

• ddSuppInteract()
• ddClearLocal()
• ddUpdateInteract()
• ddClearGlobal()

The computation of the interaction matrix is done with a series of depth-first searches. The searches start from those nodes that have only external references. The matrix is stored as a packed array of bits; since it is symmetric, only the upper triangle is kept in memory. As a final remark, we note that there may be variables that do interact, but that for a given variable order have no arc connecting their layers when they are adjacent. For instance, in ite(a,b,c) with the order a

cuddSetInteract()

Set interaction matrix entries.

cuddTestInteract()

Test interaction matrix entries.

cuddInitInteract()

Initializes the interaction matrix.

ddSuppInteract()

Find the support of f.

ddClearLocal()

Performs a DFS from f, clearing the LSB of the then pointers.

ddUpdateInteract()

Marks as interacting all pairs of variables that appear in support.

ddClearGlobal()

Scans the DD and clears the LSB of the next pointers.

By: Fabio Somenzi

Internal procedures included in this module:

• cuddLocalCacheInit()
• cuddLocalCacheQuit()
• cuddLocalCacheInsert()
• cuddLocalCacheLookup()
• cuddLocalCacheClearDead()
• cuddLocalCacheClearAll()
• cuddLocalCacheProfile()
• cuddHashTableInit()
• cuddHashTableQuit()
• cuddHashTableGenericQuit()
• cuddHashTableInsert()
• cuddHashTableLookup()
• cuddHashTableGenericInsert()
• cuddHashTableGenericLookup()
• cuddHashTableInsert2()
• cuddHashTableLookup2()
• cuddHashTableInsert3()
• cuddHashTableLookup3()

• cuddLocalCacheResize()
• ddLCHash()
• cuddLocalCacheAddToList()
• cuddLocalCacheRemoveFromList()
• cuddHashTableResize()
• cuddHashTableAlloc()

cuddLocalCacheInit()

Initializes a local computed table.

cuddLocalCacheQuit()

Shuts down a local computed table.

cuddLocalCacheInsert()

Inserts a result in a local cache.

cuddLocalCacheLookup()

Looks up in a local cache.

cuddLocalCacheClearDead()

Clears the dead entries of the local caches of a manager.

cuddLocalCacheClearAll()

Clears the local caches of a manager.

cuddLocalCacheProfile()

Computes and prints a profile of a local cache usage.

cuddHashTableInit()

Initializes a hash table.

cuddHashTableQuit()

Shuts down a hash table.

cuddHashTableGenericQuit()

Shuts down a hash table.

cuddHashTableInsert()

Inserts an item in a hash table.

cuddHashTableLookup()

Looks up a key in a hash table.

cuddHashTableInsert1()

Inserts an item in a hash table.

cuddHashTableLookup1()

Looks up a key consisting of one pointer in a hash table.

cuddHashTableGenericInsert()

Inserts an item in a hash table.

cuddHashTableGenericLookup()

Looks up a key consisting of one pointer in a hash table.

cuddHashTableInsert2()

Inserts an item in a hash table.

cuddHashTableLookup2()

Looks up a key consisting of two pointers in a hash table.

cuddHashTableInsert3()

Inserts an item in a hash table.

cuddHashTableLookup3()

Looks up a key consisting of three pointers in a hash table.

cuddLocalCacheResize()

Resizes a local cache.

()

Computes the hash value for a local cache.

cuddLocalCacheAddToList()

Inserts a local cache in the manager list.

cuddLocalCacheRemoveFromList()

Removes a local cache from the manager list.

cuddHashTableResize()

Resizes a hash table.

()

Fast storage allocation for items in a hash table.

By: Fabio Somenzi

The functions in this file allow an application to easily manipulate a queue where nodes are prioritized by level. The emphasis is on efficiency. Therefore, the queue items can have variable size. If the application does not need to attach information to the nodes, it can declare the queue items to be of type DdQueueItem. Otherwise, it can declare them to be of a structure type such that the first three fields are data pointers. The third pointer points to the node. The first two pointers are used by the level queue functions. The remaining fields are initialized to 0 when a new item is created, and are then left to the exclusive use of the application. On the DEC Alphas the three pointers must be 32-bit pointers when CUDD is compiled with 32-bit pointers. The level queue functions make sure that each node appears at most once in the queue. They do so by keeping a hash table where the node is used as key. Queue items are recycled via a free list for efficiency. Internal procedures provided by this module:

• cuddLevelQueueInit()
• cuddLevelQueueQuit()
• cuddLevelQueueEnqueue()
• cuddLevelQueueDequeue()

• hashLookup()
• hashInsert()
• hashDelete()
• hashResize()

cuddLevelQueueInit()

Initializes a level queue.

cuddLevelQueueQuit()

Shuts down a level queue.

cuddLevelQueueEnqueue()

Inserts a new key in a level queue.

cuddLevelQueueFirst()

Inserts the first key in a level queue.

cuddLevelQueueDequeue()

Remove an item from the front of a level queue.

hashLookup()

Looks up a key in the hash table of a level queue.

hashInsert()

Inserts an item in the hash table of a level queue.

hashDelete()

Removes an item from the hash table of a level queue.

hashResize()

Resizes the hash table of a level queue.

By: Fabio Somenzi

Internal procedures included in this module:

• cuddLinearAndSifting()
• cuddLinearInPlace()
• cuddUpdateInteractionMatrix()
• cuddInitLinear()
• cuddResizeLinear()

• ddLinearUniqueCompare()
• ddLinearAndSiftingAux()
• ddLinearAndSiftingUp()
• ddLinearAndSiftingDown()
• ddLinearAndSiftingBackward()
• ddUndoMoves()
• cuddXorLinear()

Cudd_PrintLinear()

Prints the linear transform matrix.

Cudd_ReadLinear()

Reads an entry of the linear transform matrix.

cuddLinearAndSifting()

BDD reduction based on combination of sifting and linear transformations.

cuddLinearInPlace()

Linearly combines two adjacent variables.

cuddUpdateInteractionMatrix()

Updates the interaction matrix.

cuddInitLinear()

Initializes the linear transform matrix.

cuddResizeLinear()

Resizes the linear transform matrix.

ddLinearUniqueCompare()

Comparison function used by qsort.

ddLinearAndSiftingAux()

Given xLow <= x <= xHigh moves x up and down between the boundaries.

ddLinearAndSiftingUp()

Sifts a variable up and applies linear transformations.

ddLinearAndSiftingDown()

Sifts a variable down and applies linear transformations.

ddLinearAndSiftingBackward()

Given a set of moves, returns the DD heap to the order giving the minimum size.

ddUndoMoves()

Given a set of moves, returns the DD heap to the order in effect before the moves.

cuddXorLinear()

XORs two rows of the linear transform matrix.

By: Fabio Somenzi

External procedures included in this file:

• Cudd_bddLiteralSetIntersection()

• cuddBddLiteralSetIntersectionRecur()

Cudd_bddLiteralSetIntersection()

Computes the intesection of two sets of literals represented as BDDs.

cuddBddLiteralSetIntersectionRecur()

Performs the recursive step of Cudd_bddLiteralSetIntersection.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_addMatrixMultiply()
• Cudd_addTimesPlus()
• Cudd_addTriangle()
• Cudd_addOuterSum()

• addMMRecur()
• addTriangleRecur()
• cuddAddOuterSumRecur()

Cudd_addMatrixMultiply()

Calculates the product of two matrices represented as ADDs.

Cudd_addTimesPlus()

Calculates the product of two matrices represented as ADDs.

Cudd_addTriangle()

Performs the triangulation step for the shortest path computation.

Cudd_addOuterSum()

Takes the minimum of a matrix and the outer sum of two vectors.

addMMRecur()

Performs the recursive step of Cudd_addMatrixMultiply.

addTriangleRecur()

Performs the recursive step of Cudd_addTriangle.

cuddAddOuterSumRecur()

Performs the recursive step of Cudd_addOuterSum.

By: Fabio Somenzi

External procedures included in this file:

• Cudd_PrioritySelect()
• Cudd_Xgty()
• Cudd_Xeqy()
• Cudd_addXeqy()
• Cudd_Dxygtdxz()
• Cudd_Dxygtdyz()
• Cudd_Inequality()
• Cudd_Disequality()
• Cudd_bddInterval()
• Cudd_CProjection()
• Cudd_addHamming()
• Cudd_MinHammingDist()
• Cudd_bddClosestCube()

• cuddCProjectionRecur()
• cuddBddClosestCube()

• cuddMinHammingDistRecur()
• separateCube()
• createResult()

Cudd_PrioritySelect()

Selects pairs from R using a priority function.

Cudd_Xgty()

Generates a BDD for the function x > y.

Cudd_Xeqy()

Generates a BDD for the function x==y.

Cudd_addXeqy()

Generates an ADD for the function x==y.

Cudd_Dxygtdxz()

Generates a BDD for the function d(x,y) > d(x,z).

Cudd_Dxygtdyz()

Generates a BDD for the function d(x,y) > d(y,z).

Cudd_Inequality()

Generates a BDD for the function x - y ≥ c.

Cudd_Disequality()

Generates a BDD for the function x - y != c.

Cudd_bddInterval()

Generates a BDD for the function lowerB ≤ x ≤ upperB.

Cudd_CProjection()

Computes the compatible projection of R w.r.t. cube Y.

Cudd_addHamming()

Computes the Hamming distance ADD.

Cudd_MinHammingDist()

Returns the minimum Hamming distance between f and minterm.

Cudd_bddClosestCube()

Finds a cube of f at minimum Hamming distance from g.

cuddCProjectionRecur()

Performs the recursive step of Cudd_CProjection.

cuddBddClosestCube()

Performs the recursive step of Cudd_bddClosestCube.

cuddMinHammingDistRecur()

Performs the recursive step of Cudd_MinHammingDist.

separateCube()

Separates cube from distance.

createResult()

Builds a result for cache storage.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_addRead()
• Cudd_bddRead()

See Alsocudd_addHarwell.c

Cudd_addRead()

Reads in a sparse matrix.

Cudd_bddRead()

Reads in a graph (without labels) given as a list of arcs.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_Ref()
• Cudd_RecursiveDeref()
• Cudd_IterDerefBdd()
• Cudd_DelayedDerefBdd()
• Cudd_RecursiveDerefZdd()
• Cudd_Deref()
• Cudd_CheckZeroRef()

• cuddReclaim()
• cuddReclaimZdd()
• cuddClearDeathRow()
• cuddShrinkDeathRow()
• cuddIsInDeathRow()
• cuddTimesInDeathRow()

Cudd_Ref()

Increases the reference count of a node, if it is not saturated.

Cudd_RecursiveDeref()

Decreases the reference count of node n.

Cudd_IterDerefBdd()

Decreases the reference count of BDD node n.

Cudd_DelayedDerefBdd()

Decreases the reference count of BDD node n.

Cudd_RecursiveDerefZdd()

Decreases the reference count of ZDD node n.

Cudd_Deref()

Decreases the reference count of node.

Cudd_CheckZeroRef()

Checks the unique table for nodes with non-zero reference counts.

cuddReclaim()

Brings children of a dead node back.

cuddReclaimZdd()

Brings children of a dead ZDD node back.

cuddShrinkDeathRow()

Shrinks the death row.

cuddClearDeathRow()

Clears the death row.

cuddIsInDeathRow()

Checks whether a node is in the death row.

cuddTimesInDeathRow()

Counts how many times a node is in the death row.

By: Shipra Panda, Bernard Plessier, Fabio Somenzi

External procedures included in this file:

• Cudd_ReduceHeap()
• Cudd_ShuffleHeap()

• cuddDynamicAllocNode()
• cuddSifting()
• cuddSwapping()
• cuddNextHigh()
• cuddNextLow()
• cuddSwapInPlace()
• cuddBddAlignToZdd()

• ddUniqueCompare()
• ddSwapAny()
• ddSiftingAux()
• ddSiftingUp()
• ddSiftingDown()
• ddSiftingBackward()
• ddReorderPreprocess()
• ddReorderPostprocess()
• ddShuffle()
• ddSiftUp()
• bddFixTree()

Cudd_ReduceHeap()

Main dynamic reordering routine.

Cudd_ShuffleHeap()

Reorders variables according to given permutation.

cuddDynamicAllocNode()

Dynamically allocates a Node.

cuddSifting()

Implementation of Rudell's sifting algorithm.

cuddSwapping()

Reorders variables by a sequence of (non-adjacent) swaps.

cuddNextHigh()

Finds the next subtable with a larger index.

cuddNextLow()

Finds the next subtable with a smaller index.

cuddSwapInPlace()

Swaps two adjacent variables.

cuddBddAlignToZdd()

Reorders BDD variables according to the order of the ZDD variables.

ddUniqueCompare()

Comparison function used by qsort.

ddSwapAny()

Swaps any two variables.

ddSiftingAux()

Given xLow <= x <= xHigh moves x up and down between the boundaries.

ddSiftingUp()

Sifts a variable up.

ddSiftingDown()

Sifts a variable down.

ddSiftingBackward()

Given a set of moves, returns the DD heap to the position giving the minimum size.

ddReorderPreprocess()

Prepares the DD heap for dynamic reordering.

ddReorderPostprocess()

Cleans up at the end of reordering.

ddShuffle()

Reorders variables according to a given permutation.

ddSiftUp()

Moves one variable up.

bddFixTree()

Fixes the BDD variable group tree after a shuffle.

ddUpdateMtrTree()

Updates the BDD variable group tree before a shuffle.

ddCheckPermuation()

Checks the BDD variable group tree before a shuffle.

By: Seh-Woong Jeong, Fabio Somenzi

External procedures included in this file:

• Cudd_Eval()
• Cudd_ShortestPath()
• Cudd_LargestCube()
• Cudd_ShortestLength()
• Cudd_Decreasing()
• Cudd_Increasing()
• Cudd_EquivDC()
• Cudd_bddLeqUnless()
• Cudd_EqualSupNorm()
• Cudd_bddMakePrime()
• Cudd_bddMaximallyExpand()
• Cudd_bddLargestPrimeUnate()

• cuddBddMakePrime()

• freePathPair()
• getShortest()
• getPath()
• getLargest()
• getCube()
• ddBddMaximallyExpand()
• ddShortestPathUnate()

Cudd_Eval()

Returns the value of a DD for a given variable assignment.

Cudd_ShortestPath()

Finds a shortest path in a DD.

Cudd_LargestCube()

Finds a largest cube in a DD.

Cudd_ShortestLength()

Find the length of the shortest path(s) in a DD.

Cudd_Decreasing()

Determines whether a BDD is negative unate in a variable.

Cudd_Increasing()

Determines whether a BDD is positive unate in a variable.

Cudd_EquivDC()

Tells whether F and G are identical wherever D is 0.

Cudd_bddLeqUnless()

Tells whether f is less than of equal to G unless D is 1.

Cudd_EqualSupNorm()

Compares two ADDs for equality within tolerance.

Cudd_bddMakePrime()

Expands cube to a prime implicant of f.

Cudd_bddMaximallyExpand()

Expands lb to prime implicants of (f and ub).

Cudd_bddLargestPrimeUnate()

Find a largest prime of a unate function.

cuddBddMakePrime()

Performs the recursive step of Cudd_bddMakePrime.

freePathPair()

Frees the entries of the visited symbol table.

getShortest()

Finds the length of the shortest path(s) in a DD.

getPath()

Build a BDD for a shortest path of f.

getLargest()

Finds the size of the largest cube(s) in a DD.

getCube()

Build a BDD for a largest cube of f.

ddBddMaximallyExpand()

Performs the recursive step of Cudd_bddMaximallyExpand.

ddBddShortestPathUnate()

Performs shortest path computation on a unate function.

ddGetLargestCubeUnate()

Extracts largest prime of a unate function.

By: Fabio Somenzi

External procedures included in this module:

• Cudd_CofMinterm();

• ddCofMintermAux()

Cudd_CofMinterm()

Computes the fraction of minterms in the on-set of all the positive cofactors of a BDD or ADD.

ddCofMintermAux()

Recursive Step for Cudd_CofMinterm function.

By: Balakrishna Kumthekar

External functions included in this modoule:

• Cudd_SolveEqn()
• Cudd_VerifySol()

• cuddSolveEqnRecur()
• cuddVerifySol()

Cudd_SolveEqn()

Implements the solution of F(x,y) = 0.

Cudd_VerifySol()

Checks the solution of F(x,y) = 0.

cuddSolveEqnRecur()

Implements the recursive step of Cudd_SolveEqn.

cuddVerifySol()

Implements the recursive step of Cudd_VerifySol.

By: Balakrishna Kumthekar

External functions included in this modoule:

• Cudd_SplitSet()

• cuddSplitSetRecur() Static functions included in this module:
  • selectMintermsFromUniverse()
  • mintermsFromUniverse()
  • bddAnnotateMintermCount()

  Cudd_SplitSet()

  Returns m minterms from a BDD.

  cuddSplitSetRecur()

  Implements the recursive step of Cudd_SplitSet.

  selectMintermsFromUniverse()

  This function prepares an array of variables which have not been encountered so far when traversing the procedure cuddSplitSetRecur.

  mintermsFromUniverse()

  Recursive procedure to extract n mintems from constant 1.

  bddAnnotateMintermCount()

  Annotates every node in the BDD node with its minterm count.

  ---

  cuddSubsetHB.c

  Procedure to subset the given BDD by choosing the heavier branches.

  By: Kavita Ravi

  External procedures provided by this module:

  • Cudd_SubsetHeavyBranch()
  • Cudd_SupersetHeavyBranch()
  Internal procedures included in this module:
  • cuddSubsetHeavyBranch()
  Static procedures included in this module:
  • ResizeCountMintermPages();
  • ResizeNodeDataPages()
  • ResizeCountNodePages()
  • SubsetCountMintermAux()
  • SubsetCountMinterm()
  • SubsetCountNodesAux()
  • SubsetCountNodes()
  • BuildSubsetBdd()

  See AlsocuddSubsetSP.c

  Cudd_SubsetHeavyBranch()

  Extracts a dense subset from a BDD with the heavy branch heuristic.

  Cudd_SupersetHeavyBranch()

  Extracts a dense superset from a BDD with the heavy branch heuristic.

  cuddSubsetHeavyBranch()

  The main procedure that returns a subset by choosing the heavier branch in the BDD.

  ResizeNodeDataPages()

  Resize the number of pages allocated to store the node data.

  ResizeCountMintermPages()

  Resize the number of pages allocated to store the minterm counts.

  ResizeCountNodePages()

  Resize the number of pages allocated to store the node counts.

  SubsetCountMintermAux()

  Recursively counts minterms of each node in the DAG.

  SubsetCountMinterm()

  Counts minterms of each node in the DAG

  SubsetCountNodesAux()

  Recursively counts the number of nodes under the dag. Also counts the number of nodes under the lighter child of this node.

  SubsetCountNodes()

  Counts the nodes under the current node and its lighter child

  StoreNodes()

  Procedure to recursively store nodes that are retained in the subset.

  BuildSubsetBdd()

  Builds the subset BDD using the heavy branch method.

  ---

  cuddSubsetSP.c

  Procedure to subset the given BDD choosing the shortest paths (largest cubes) in the BDD.

  By: Kavita Ravi

  External procedures included in this module:

  • Cudd_SubsetShortPaths()
  • Cudd_SupersetShortPaths()
  Internal procedures included in this module:
  • cuddSubsetShortPaths()
  Static procedures included in this module:
  • BuildSubsetBdd()
  • CreatePathTable()
  • AssessPathLength()
  • CreateTopDist()
  • CreateBotDist()
  • ResizeNodeDistPages()
  • ResizeQueuePages()
  • stPathTableDdFree()

  See AlsocuddSubsetHB.c

  Cudd_SubsetShortPaths()

  Extracts a dense subset from a BDD with the shortest paths heuristic.

  Cudd_SupersetShortPaths()

  Extracts a dense superset from a BDD with the shortest paths heuristic.

  cuddSubsetShortPaths()

  The outermost procedure to return a subset of the given BDD with the shortest path lengths.

  ResizeNodeDistPages()

  Resize the number of pages allocated to store the distances related to each node.

  ResizeQueuePages()

  Resize the number of pages allocated to store nodes in the BFS traversal of the Bdd .

  CreateTopDist()

  Labels each node with its shortest distance from the root

  CreateBotDist()

  Labels each node with the shortest distance from the constant.

  CreatePathTable()

  The outer procedure to label each node with its shortest distance from the root and constant

  AssessPathLength()

  Chooses the maximum allowable path length of nodes under the threshold.

  BuildSubsetBdd()

  Builds the BDD with nodes labeled with path length less than or equal to maxpath

  stPathTableDdFree()

  Procedure to free te result dds stored in the NodeDist pages.

  ---

  cuddSymmetry.c

  Functions for symmetry-based variable reordering.

  By: Shipra Panda, Fabio Somenzi

  External procedures included in this file:

  • Cudd_SymmProfile()
  Internal procedures included in this module:
  • cuddSymmCheck()
  • cuddSymmSifting()
  • cuddSymmSiftingConv()
  Static procedures included in this module:
  • ddSymmUniqueCompare()
  • ddSymmSiftingAux()
  • ddSymmSiftingConvAux()
  • ddSymmSiftingUp()
  • ddSymmSiftingDown()
  • ddSymmGroupMove()
  • ddSymmGroupMoveBackward()
  • ddSymmSiftingBackward()
  • ddSymmSummary()

  Cudd_SymmProfile()

  Prints statistics on symmetric variables.

  cuddSymmCheck()

  Checks for symmetry of x and y.

  cuddSymmSifting()

  Symmetric sifting algorithm.

  cuddSymmSiftingConv()

  Symmetric sifting to convergence algorithm.

  ddSymmUniqueCompare()

  Comparison function used by qsort.

  ddSymmSiftingAux()

  Given xLow <= x <= xHigh moves x up and down between the boundaries.

  ddSymmSiftingConvAux()

  Given xLow <= x <= xHigh moves x up and down between the boundaries.

  ddSymmSiftingUp()

  Moves x up until either it reaches the bound (xLow) or the size of the DD heap increases too much.

  ddSymmSiftingDown()

  Moves x down until either it reaches the bound (xHigh) or the size of the DD heap increases too much.

  ddSymmGroupMove()

  Swaps two groups.

  ddSymmGroupMoveBackward()

  Undoes the swap of two groups.

  ddSymmSiftingBackward()

  Given a set of moves, returns the DD heap to the position giving the minimum size.

  ddSymmSummary()

  Counts numbers of symmetric variables and symmetry groups.

  ---

  cuddTable.c

  Unique table management functions.

  By: Fabio Somenzi

  External procedures included in this module:

  • Cudd_Prime()
  • Cudd_Reserve()
  Internal procedures included in this module:
  • cuddAllocNode()
  • cuddInitTable()
  • cuddFreeTable()
  • cuddGarbageCollect()
  • cuddZddGetNode()
  • cuddZddGetNodeIVO()
  • cuddUniqueInter()
  • cuddUniqueInterIVO()
  • cuddUniqueInterZdd()
  • cuddUniqueConst()
  • cuddRehash()
  • cuddShrinkSubtable()
  • cuddInsertSubtables()
  • cuddDestroySubtables()
  • cuddResizeTableZdd()
  • cuddSlowTableGrowth()
  Static procedures included in this module:
  • ddRehashZdd()
  • ddResizeTable()
  • cuddFindParent()
  • cuddOrderedInsert()
  • cuddOrderedThread()
  • cuddRotateLeft()
  • cuddRotateRight()
  • cuddDoRebalance()
  • cuddCheckCollisionOrdering()

  Cudd_Prime()

  Returns the next prime >= p.

  Cudd_Reserve()

  Expand manager without creating variables.

  cuddAllocNode()

  Fast storage allocation for DdNodes in the table.

  cuddInitTable()

  Creates and initializes the unique table.

  cuddFreeTable()

  Frees the resources associated to a unique table.

  cuddGarbageCollect()

  Performs garbage collection on the unique tables.

  cuddZddGetNode()

  Wrapper for cuddUniqueInterZdd.

  cuddZddGetNodeIVO()

  Wrapper for cuddUniqueInterZdd that is independent of variable ordering.

  cuddUniqueInter()

  Checks the unique table for the existence of an internal node.

  cuddUniqueInterIVO()

  Wrapper for cuddUniqueInter that is independent of variable ordering.

  cuddUniqueInterZdd()

  Checks the unique table for the existence of an internal ZDD node.

  cuddUniqueConst()

  Checks the unique table for the existence of a constant node.

  cuddRehash()

  Rehashes a unique subtable.

  cuddShrinkSubtable()

  Shrinks a subtable.

  cuddInsertSubtables()

  Inserts n new subtables in a unique table at level.

  cuddDestroySubtables()

  Destroys the n most recently created subtables in a unique table.

  cuddResizeTableZdd()

  Increases the number of ZDD subtables in a unique table so that it meets or exceeds index.

  cuddSlowTableGrowth()

  Adjusts parameters of a table to slow down its growth.

  ddRehashZdd()

  Rehashes a ZDD unique subtable.

  ddResizeTable()

  Increases the number of subtables in a unique table so that it meets or exceeds index.

  cuddFindParent()

  Searches the subtables above node for a parent.

  ()

  Adjusts the values of table limits.

  cuddOrderedInsert()

  Inserts a DdNode in a red/black search tree.

  cuddOrderedThread()

  Threads all the nodes of a search tree into a linear list.

  ()

  Performs the left rotation for red/black trees.

  ()

  Performs the right rotation for red/black trees.

  cuddDoRebalance()

  Rebalances a red/black tree.

  ddPatchTree()

  Fixes a variable tree after the insertion of new subtables.

  cuddCheckCollisionOrdering()

  Checks whether a collision list is ordered.

  ddReportRefMess()

  Reports problem in garbage collection.

  ---

  cuddUtil.c

  Utility functions.

  By: Fabio Somenzi

  External procedures included in this module:

  • Cudd_PrintMinterm()
  • Cudd_bddPrintCover()
  • Cudd_PrintDebug()
  • Cudd_DagSize()
  • Cudd_EstimateCofactor()
  • Cudd_EstimateCofactorSimple()
  • Cudd_SharingSize()
  • Cudd_CountMinterm()
  • Cudd_EpdCountMinterm()
  • Cudd_CountPath()
  • Cudd_CountPathsToNonZero()
  • Cudd_SupportIndices()
  • Cudd_Support()
  • Cudd_SupportIndex()
  • Cudd_SupportSize()
  • Cudd_VectorSupportIndices()
  • Cudd_VectorSupport()
  • Cudd_VectorSupportIndex()
  • Cudd_VectorSupportSize()
  • Cudd_ClassifySupport()
  • Cudd_CountLeaves()
  • Cudd_bddPickOneCube()
  • Cudd_bddPickOneMinterm()
  • Cudd_bddPickArbitraryMinterms()
  • Cudd_SubsetWithMaskVars()
  • Cudd_FirstCube()
  • Cudd_NextCube()
  • Cudd_bddComputeCube()
  • Cudd_addComputeCube()
  • Cudd_FirstNode()
  • Cudd_NextNode()
  • Cudd_GenFree()
  • Cudd_IsGenEmpty()
  • Cudd_IndicesToCube()
  • Cudd_PrintVersion()
  • Cudd_AverageDistance()
  • Cudd_Random()
  • Cudd_Srandom()
  • Cudd_Density()
  Internal procedures included in this module:
  • cuddP()
  • cuddStCountfree()
  • cuddCollectNodes()
  • cuddNodeArray()
  Static procedures included in this module:
  • dp2()
  • ddPrintMintermAux()
  • ddDagInt()
  • ddCountMintermAux()
  • ddEpdCountMintermAux()
  • ddCountPathAux()
  • ddSupportStep()
  • ddClearFlag()
  • ddLeavesInt()
  • ddPickArbitraryMinterms()
  • ddPickRepresentativeCube()
  • ddEpdFree()
  • ddFindSupport()
  • ddClearVars()
  • indexCompare()

  Cudd_PrintMinterm()

  Prints a disjoint sum of products.

  Cudd_bddPrintCover()

  Prints a sum of prime implicants of a BDD.

  Cudd_PrintDebug()

  Prints to the standard output a DD and its statistics.

  Cudd_DagSize()

  Counts the number of nodes in a DD.

  Cudd_EstimateCofactor()

  Estimates the number of nodes in a cofactor of a DD.

  Cudd_EstimateCofactorSimple()

  Estimates the number of nodes in a cofactor of a DD.

  Cudd_SharingSize()

  Counts the number of nodes in an array of DDs.

  Cudd_CountMinterm()

  Counts the number of minterms of a DD.

  Cudd_CountPath()

  Counts the number of paths of a DD.

  Cudd_EpdCountMinterm()

  Counts the number of minterms of a DD with extended precision.

  Cudd_CountPathsToNonZero()

  Counts the number of paths to a non-zero terminal of a DD.

  Cudd_SupportIndices()

  Finds the variables on which a DD depends.

  Cudd_Support()

  Finds the variables on which a DD depends.

  Cudd_SupportIndex()

  Finds the variables on which a DD depends.

  Cudd_SupportSize()

  Counts the variables on which a DD depends.

  Cudd_VectorSupportIndices()

  Finds the variables on which a set of DDs depends.

  Cudd_VectorSupport()

  Finds the variables on which a set of DDs depends.

  Cudd_VectorSupportIndex()

  Finds the variables on which a set of DDs depends.

  Cudd_VectorSupportSize()

  Counts the variables on which a set of DDs depends.

  Cudd_ClassifySupport()

  Classifies the variables in the support of two DDs.

  Cudd_CountLeaves()

  Counts the number of leaves in a DD.

  Cudd_bddPickOneCube()

  Picks one on-set cube randomly from the given DD.

  Cudd_bddPickOneMinterm()

  Picks one on-set minterm randomly from the given DD.

  Cudd_bddPickArbitraryMinterms()

  Picks k on-set minterms evenly distributed from given DD.

  Cudd_SubsetWithMaskVars()

  Extracts a subset from a BDD.

  Cudd_FirstCube()

  Finds the first cube of a decision diagram.

  Cudd_NextCube()

  Generates the next cube of a decision diagram onset.

  Cudd_FirstPrime()

  Finds the first prime of a Boolean function.

  Cudd_NextPrime()

  Generates the next prime of a Boolean function.

  Cudd_bddComputeCube()

  Computes the cube of an array of BDD variables.

  Cudd_addComputeCube()

  Computes the cube of an array of ADD variables.

  Cudd_CubeArrayToBdd()

  Builds the BDD of a cube from a positional array.

  Cudd_BddToCubeArray()

  Builds a positional array from the BDD of a cube.

  Cudd_FirstNode()

  Finds the first node of a decision diagram.

  Cudd_NextNode()

  Finds the next node of a decision diagram.

  Cudd_GenFree()

  Frees a CUDD generator.

  Cudd_IsGenEmpty()

  Queries the status of a generator.

  Cudd_IndicesToCube()

  Builds a cube of BDD variables from an array of indices.

  Cudd_PrintVersion()

  Prints the package version number.

  Cudd_AverageDistance()

  Computes the average distance between adjacent nodes.

  Cudd_Random()

  Portable random number generator.

  Cudd_Srandom()

  Initializer for the portable random number generator.

  Cudd_Density()

  Computes the density of a BDD or ADD.

  Cudd_OutOfMem()

  Warns that a memory allocation failed.

  cuddP()

  Prints a DD to the standard output. One line per node is printed.

  cuddStCountfree()

  Frees the memory used to store the minterm counts recorded in the visited table.

  cuddCollectNodes()

  Recursively collects all the nodes of a DD in a symbol table.

  cuddNodeArray()

  Recursively collects all the nodes of a DD in an array.

  dp2()

  Performs the recursive step of cuddP.

  ddPrintMintermAux()

  Performs the recursive step of Cudd_PrintMinterm.

  ddDagInt()

  Performs the recursive step of Cudd_DagSize.

  cuddNodeArrayRecur()

  Performs the recursive step of cuddNodeArray.

  cuddEstimateCofactor()

  Performs the recursive step of Cudd_CofactorEstimate.

  cuddUniqueLookup()

  Checks the unique table for the existence of an internal node.

  cuddEstimateCofactorSimple()

  Performs the recursive step of Cudd_CofactorEstimateSimple.

  ddCountMintermAux()

  Performs the recursive step of Cudd_CountMinterm.

  ddCountPathAux()

  Performs the recursive step of Cudd_CountPath.

  ddEpdCountMintermAux()

  Performs the recursive step of Cudd_EpdCountMinterm.

  ddCountPathsToNonZero()

  Performs the recursive step of Cudd_CountPathsToNonZero.

  ddSupportStep()

  Performs the recursive step of Cudd_Support.

  ddClearFlag()

  Performs a DFS from f, clearing the LSB of the next pointers.

  ddLeavesInt()

  Performs the recursive step of Cudd_CountLeaves.

  ddPickArbitraryMinterms()

  Performs the recursive step of Cudd_bddPickArbitraryMinterms.

  ddPickRepresentativeCube()

  Finds a representative cube of a BDD.

  ddEpdFree()

  Frees the memory used to store the minterm counts recorded in the visited table.

  ddFindSupport()

  Recursively find the support of f.

  ddClearVars()

  Clears visited flags for variables.

  indexCompare()

  Compares indices for qsort.

  ---

  cuddWindow.c

  Functions for variable reordering by window permutation.

  By: Fabio Somenzi

  Internal procedures included in this module:

  • cuddWindowReorder()
  Static procedures included in this module:
  • ddWindow2()
  • ddWindowConv2()
  • ddPermuteWindow3()
  • ddWindow3()
  • ddWindowConv3()
  • ddPermuteWindow4()
  • ddWindow4()
  • ddWindowConv4()

  cuddWindowReorder()

  Reorders by applying the method of the sliding window.

  ddWindow2()

  Reorders by applying a sliding window of width 2.

  ddWindowConv2()

  Reorders by repeatedly applying a sliding window of width 2.

  ddPermuteWindow3()

  Tries all the permutations of the three variables between x and x+2 and retains the best.

  ddWindow3()

  Reorders by applying a sliding window of width 3.

  ddWindowConv3()

  Reorders by repeatedly applying a sliding window of width 3.

  ddPermuteWindow4()

  Tries all the permutations of the four variables between w and w+3 and retains the best.

  ddWindow4()

  Reorders by applying a sliding window of width 4.

  ddWindowConv4()

  Reorders by repeatedly applying a sliding window of width 4.

  ---

  cuddZddCount.c

  Procedures to count the number of minterms of a ZDD.

  By: Hyong-Kyoon Shin, In-Ho Moon

  External procedures included in this module:

  • Cudd_zddCount();
  • Cudd_zddCountDouble();
  Internal procedures included in this module:
  Static procedures included in this module:
  • cuddZddCountStep();
  • cuddZddCountDoubleStep();
  • st_zdd_count_dbl_free()
  • st_zdd_countfree()

  Cudd_zddCount()

  Counts the number of minterms in a ZDD.

  Cudd_zddCountDouble()

  Counts the number of minterms of a ZDD.

  cuddZddCountStep()

  Performs the recursive step of Cudd_zddCount.

  cuddZddCountDoubleStep()

  Performs the recursive step of Cudd_zddCountDouble.

  st_zdd_countfree()

  Frees the memory associated with the computed table of Cudd_zddCount.

  st_zdd_count_dbl_free()

  Frees the memory associated with the computed table of Cudd_zddCountDouble.

  ---

  cuddZddFuncs.c

  Functions to manipulate covers represented as ZDDs.

  By: In-Ho Moon

  External procedures included in this module:

  • Cudd_zddProduct();
  • Cudd_zddUnateProduct();
  • Cudd_zddWeakDiv();
  • Cudd_zddWeakDivF();
  • Cudd_zddDivide();
  • Cudd_zddDivideF();
  • Cudd_zddComplement();
  Internal procedures included in this module:
  • cuddZddProduct();
  • cuddZddUnateProduct();
  • cuddZddWeakDiv();
  • cuddZddWeakDivF();
  • cuddZddDivide();
  • cuddZddDivideF();
  • cuddZddGetCofactors3()
  • cuddZddGetCofactors2()
  • cuddZddComplement();
  • cuddZddGetPosVarIndex();
  • cuddZddGetNegVarIndex();
  • cuddZddGetPosVarLevel();
  • cuddZddGetNegVarLevel();
  Static procedures included in this module:

  Cudd_zddProduct()

  Computes the product of two covers represented by ZDDs.

  Cudd_zddUnateProduct()

  Computes the product of two unate covers.

  Cudd_zddWeakDiv()

  Applies weak division to two covers.

  Cudd_zddDivide()

  Computes the quotient of two unate covers.

  Cudd_zddWeakDivF()

  Modified version of Cudd_zddWeakDiv.

  Cudd_zddDivideF()

  Modified version of Cudd_zddDivide.

  Cudd_zddComplement()

  Computes a complement cover for a ZDD node.

  cuddZddProduct()

  Performs the recursive step of Cudd_zddProduct.

  cuddZddUnateProduct()

  Performs the recursive step of Cudd_zddUnateProduct.

  cuddZddWeakDiv()

  Performs the recursive step of Cudd_zddWeakDiv.

  cuddZddWeakDivF()

  Performs the recursive step of Cudd_zddWeakDivF.

  cuddZddDivide()

  Performs the recursive step of Cudd_zddDivide.

  cuddZddDivideF()

  Performs the recursive step of Cudd_zddDivideF.

  cuddZddGetCofactors3()

  Computes the three-way decomposition of f w.r.t. v.

  cuddZddGetCofactors2()

  Computes the two-way decomposition of f w.r.t. v.

  cuddZddComplement()

  Computes a complement of a ZDD node.

  cuddZddGetPosVarIndex()

  Returns the index of positive ZDD variable.

  cuddZddGetNegVarIndex()

  Returns the index of negative ZDD variable.

  cuddZddGetPosVarLevel()

  Returns the level of positive ZDD variable.

  cuddZddGetNegVarLevel()

  Returns the level of negative ZDD variable.

  ---

  cuddZddGroup.c

  Functions for ZDD group sifting.

  By: Fabio Somenzi

  External procedures included in this file:

  • Cudd_MakeZddTreeNode()
  Internal procedures included in this file:
  • cuddZddTreeSifting()
  Static procedures included in this module:
  • zddTreeSiftingAux()
  • zddCountInternalMtrNodes()
  • zddReorderChildren()
  • zddFindNodeHiLo()
  • zddUniqueCompareGroup()
  • zddGroupSifting()
  • zddGroupSiftingAux()
  • zddGroupSiftingUp()
  • zddGroupSiftingDown()
  • zddGroupMove()
  • zddGroupMoveBackward()
  • zddGroupSiftingBackward()
  • zddMergeGroups()

  Cudd_MakeZddTreeNode()

  Creates a new ZDD variable group.

  cuddZddTreeSifting()

  Tree sifting algorithm for ZDDs.

  zddTreeSiftingAux()

  Visits the group tree and reorders each group.

  zddCountInternalMtrNodes()

  Counts the number of internal nodes of the group tree.

  zddReorderChildren()

  Reorders the children of a group tree node according to the options.

  zddFindNodeHiLo()

  Finds the lower and upper bounds of the group represented by treenode.

  zddUniqueCompareGroup()

  Comparison function used by qsort.

  zddGroupSifting()

  Sifts from treenode->low to treenode->high.

  zddGroupSiftingAux()

  Sifts one variable up and down until it has taken all positions. Checks for aggregation.

  zddGroupSiftingUp()

  Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much.

  zddGroupSiftingDown()

  Sifts down a variable until it reaches position xHigh.

  zddGroupMove()

  Swaps two groups and records the move.

  zddGroupMoveBackward()

  Undoes the swap two groups.

  zddGroupSiftingBackward()

  Determines the best position for a variables and returns it there.

  zddMergeGroups()

  Merges groups in the DD table.

  ---

  cuddZddIsop.c

  Functions to find irredundant SOP covers as ZDDs from BDDs.

  By: In-Ho Moon

  External procedures included in this module:

  • Cudd_bddIsop()
  • Cudd_zddIsop()
  • Cudd_MakeBddFromZddCover()
  Internal procedures included in this module:
  • cuddBddIsop()
  • cuddZddIsop()
  • cuddMakeBddFromZddCover()
  Static procedures included in this module:

  Cudd_zddIsop()

  Computes an ISOP in ZDD form from BDDs.

  Cudd_bddIsop()

  Computes a BDD in the interval between L and U with a simple sum-of-product cover.

  Cudd_MakeBddFromZddCover()

  Converts a ZDD cover to a BDD.

  cuddZddIsop()

  Performs the recursive step of Cudd_zddIsop.

  cuddBddIsop()

  Performs the recursive step of Cudd_bddIsop.

  cuddMakeBddFromZddCover()

  Converts a ZDD cover to a BDD.

  ---

  cuddZddLin.c

  Procedures for dynamic variable ordering of ZDDs.

  By: Fabio Somenzi

  Internal procedures included in this module:

  • cuddZddLinearSifting()
  Static procedures included in this module:
  • cuddZddLinearInPlace()
  • cuddZddLinerAux()
  • cuddZddLinearUp()
  • cuddZddLinearDown()
  • cuddZddLinearBackward()
  • cuddZddUndoMoves()

  See AlsocuddLinear.c cuddZddReord.c

  cuddZddLinearSifting()

  Implementation of the linear sifting algorithm for ZDDs.

  cuddZddLinearInPlace()

  Linearly combines two adjacent variables.

  cuddZddLinearAux()

  Given xLow <= x <= xHigh moves x up and down between the boundaries.

  cuddZddLinearUp()

  Sifts a variable up applying the XOR transformation.

  cuddZddLinearDown()

  Sifts a variable down and applies the XOR transformation.

  cuddZddLinearBackward()

  Given a set of moves, returns the ZDD heap to the position giving the minimum size.

  cuddZddUndoMoves()

  Given a set of moves, returns the ZDD heap to the order in effect before the moves.

  ---

  cuddZddMisc.c

  Miscellaneous utility functions for ZDDs.

  By: Hyong-Kyoon Shin, In-Ho Moon

  External procedures included in this module:

  • Cudd_zddDagSize()
  • Cudd_zddCountMinterm()
  • Cudd_zddPrintSubtable()
  Internal procedures included in this module:
  Static procedures included in this module:
  • cuddZddDagInt()

  Cudd_zddDagSize()

  Counts the number of nodes in a ZDD.

  Cudd_zddCountMinterm()

  Counts the number of minterms of a ZDD.

  Cudd_zddPrintSubtable()

  Prints the ZDD table.

  cuddZddDagInt()

  Performs the recursive step of Cudd_zddDagSize.

  ---

  cuddZddPort.c

  Functions that translate BDDs to ZDDs.

  By: Hyong-kyoon Shin, In-Ho Moon

  External procedures included in this module:

  • Cudd_zddPortFromBdd()
  • Cudd_zddPortToBdd()
  Internal procedures included in this module:
  Static procedures included in this module:
  • zddPortFromBddStep()
  • zddPortToBddStep()

  Cudd_zddPortFromBdd()

  Converts a BDD into a ZDD.

  Cudd_zddPortToBdd()

  Converts a ZDD into a BDD.

  zddPortFromBddStep()

  Performs the recursive step of Cudd_zddPortFromBdd.

  zddPortToBddStep()

  Performs the recursive step of Cudd_zddPortToBdd.

  ---

  cuddZddReord.c

  Procedures for dynamic variable ordering of ZDDs.

  By: Hyong-Kyoon Shin, In-Ho Moon

  External procedures included in this module:

  • Cudd_zddReduceHeap()
  • Cudd_zddShuffleHeap()
  Internal procedures included in this module:
  • cuddZddAlignToBdd()
  • cuddZddNextHigh()
  • cuddZddNextLow()
  • cuddZddUniqueCompare()
  • cuddZddSwapInPlace()
  • cuddZddSwapping()
  • cuddZddSifting()
  Static procedures included in this module:
  • zddSwapAny()
  • cuddZddSiftingAux()
  • cuddZddSiftingUp()
  • cuddZddSiftingDown()
  • cuddZddSiftingBackward()
  • zddReorderPreprocess()
  • zddReorderPostprocess()
  • zddShuffle()
  • zddSiftUp()

  Cudd_zddReduceHeap()

  Main dynamic reordering routine for ZDDs.

  Cudd_zddShuffleHeap()

  Reorders ZDD variables according to given permutation.

  cuddZddAlignToBdd()

  Reorders ZDD variables according to the order of the BDD variables.

  cuddZddNextHigh()

  Finds the next subtable with a larger index.

  cuddZddNextLow()

  Finds the next subtable with a smaller index.

  cuddZddUniqueCompare()

  Comparison function used by qsort.

  cuddZddSwapInPlace()

  Swaps two adjacent variables.

  cuddZddSwapping()

  Reorders variables by a sequence of (non-adjacent) swaps.

  cuddZddSifting()

  Implementation of Rudell's sifting algorithm.

  zddSwapAny()

  Swaps any two variables.

  cuddZddSiftingAux()

  Given xLow <= x <= xHigh moves x up and down between the boundaries.

  cuddZddSiftingUp()

  Sifts a variable up.

  cuddZddSiftingDown()

  Sifts a variable down.

  cuddZddSiftingBackward()

  Given a set of moves, returns the ZDD heap to the position giving the minimum size.

  zddReorderPreprocess()

  Prepares the ZDD heap for dynamic reordering.

  zddReorderPostprocess()

  Shrinks almost empty ZDD subtables at the end of reordering to guarantee that they have a reasonable load factor.

  zddShuffle()

  Reorders ZDD variables according to a given permutation.

  zddSiftUp()

  Moves one ZDD variable up.

  zddFixTree()

  Fixes the ZDD variable group tree after a shuffle.

  ---

  cuddZddSetop.c

  Set operations on ZDDs.

  By: Hyong-Kyoon Shin, In-Ho Moon

  External procedures included in this module:

  • Cudd_zddIte()
  • Cudd_zddUnion()
  • Cudd_zddIntersect()
  • Cudd_zddDiff()
  • Cudd_zddDiffConst()
  • Cudd_zddSubset1()
  • Cudd_zddSubset0()
  • Cudd_zddChange()
  Internal procedures included in this module:
  • cuddZddIte()
  • cuddZddUnion()
  • cuddZddIntersect()
  • cuddZddDiff()
  • cuddZddChangeAux()
  • cuddZddSubset1()
  • cuddZddSubset0()
  Static procedures included in this module:
  • zdd_subset1_aux()
  • zdd_subset0_aux()
  • zddVarToConst()

  Cudd_zddIte()

  Computes the ITE of three ZDDs.

  Cudd_zddUnion()

  Computes the union of two ZDDs.

  Cudd_zddIntersect()

  Computes the intersection of two ZDDs.

  Cudd_zddDiff()

  Computes the difference of two ZDDs.

  Cudd_zddDiffConst()

  Performs the inclusion test for ZDDs (P implies Q).

  Cudd_zddSubset1()

  Computes the positive cofactor of a ZDD w.r.t. a variable.

  Cudd_zddSubset0()

  Computes the negative cofactor of a ZDD w.r.t. a variable.

  Cudd_zddChange()

  Substitutes a variable with its complement in a ZDD.

  cuddZddIte()

  Performs the recursive step of Cudd_zddIte.

  cuddZddUnion()

  Performs the recursive step of Cudd_zddUnion.

  cuddZddIntersect()

  Performs the recursive step of Cudd_zddIntersect.

  cuddZddDiff()

  Performs the recursive step of Cudd_zddDiff.

  cuddZddChangeAux()

  Performs the recursive step of Cudd_zddChange.

  cuddZddSubset1()

  Computes the positive cofactor of a ZDD w.r.t. a variable.

  cuddZddSubset0()

  Computes the negative cofactor of a ZDD w.r.t. a variable.

  cuddZddChange()

  Substitutes a variable with its complement in a ZDD.

  zdd_subset1_aux()

  Performs the recursive step of Cudd_zddSubset1.

  zdd_subset0_aux()

  Performs the recursive step of Cudd_zddSubset0.

  zddVarToConst()

  Replaces variables with constants if possible (part of canonical form).

  ---

  cuddZddSymm.c

  Functions for symmetry-based ZDD variable reordering.

  By: Hyong-Kyoon Shin, In-Ho Moon

  External procedures included in this module:

  • Cudd_zddSymmProfile()
  Internal procedures included in this module:
  • cuddZddSymmCheck()
  • cuddZddSymmSifting()
  • cuddZddSymmSiftingConv()
  Static procedures included in this module:
  • cuddZddUniqueCompare()
  • cuddZddSymmSiftingAux()
  • cuddZddSymmSiftingConvAux()
  • cuddZddSymmSifting_up()
  • cuddZddSymmSifting_down()
  • zdd_group_move()
  • cuddZddSymmSiftingBackward()
  • zdd_group_move_backward()

  See AlsocuddSymmetry.c

  Cudd_zddSymmProfile()

  Prints statistics on symmetric ZDD variables.

  cuddZddSymmCheck()

  Checks for symmetry of x and y.

  cuddZddSymmSifting()

  Symmetric sifting algorithm for ZDDs.

  cuddZddSymmSiftingConv()

  Symmetric sifting to convergence algorithm for ZDDs.

  cuddZddSymmSiftingAux()

  Given x_low <= x <= x_high moves x up and down between the boundaries.

  cuddZddSymmSiftingConvAux()

  Given x_low <= x <= x_high moves x up and down between the boundaries.

  cuddZddSymmSifting_up()

  Moves x up until either it reaches the bound (x_low) or the size of the ZDD heap increases too much.

  cuddZddSymmSifting_down()

  Moves x down until either it reaches the bound (x_high) or the size of the ZDD heap increases too much.

  cuddZddSymmSiftingBackward()

  Given a set of moves, returns the ZDD heap to the position giving the minimum size.

  zdd_group_move()

  Swaps two groups.

  zdd_group_move_backward()

  Undoes the swap of two groups.

  cuddZddSymmSummary()

  Counts numbers of symmetric variables and symmetry groups.

  ---

  cuddZddUtil.c

  Utility functions for ZDDs.

  By: Hyong-Kyoon Shin, In-Ho Moon, Fabio Somenzi

  External procedures included in this module:

  • Cudd_zddPrintMinterm()
  • Cudd_zddPrintCover()
  • Cudd_zddPrintDebug()
  • Cudd_zddFirstPath()
  • Cudd_zddNextPath()
  • Cudd_zddCoverPathToString()
  • Cudd_zddSupport()
  • Cudd_zddDumpDot()
  Internal procedures included in this module:
  • cuddZddP()
  Static procedures included in this module:
  • zp2()
  • zdd_print_minterm_aux()
  • zddPrintCoverAux()
  • zddSupportStep()
  • zddClearFlag()

  Cudd_zddPrintMinterm()

  Prints a disjoint sum of product form for a ZDD.

  Cudd_zddPrintCover()

  Prints a sum of products from a ZDD representing a cover.

  Cudd_zddPrintDebug()

  Prints to the standard output a ZDD and its statistics.

  Cudd_zddFirstPath()

  Finds the first path of a ZDD.

  Cudd_zddNextPath()

  Generates the next path of a ZDD.

  Cudd_zddCoverPathToString()

  Converts a path of a ZDD representing a cover to a string.

  Cudd_zddSupport()

  Finds the variables on which a ZDD depends.

  Cudd_zddDumpDot()

  Writes a dot file representing the argument ZDDs.

  cuddZddP()

  Prints a ZDD to the standard output. One line per node is printed.

  zp2()

  Performs the recursive step of cuddZddP.

  zdd_print_minterm_aux()

  Performs the recursive step of Cudd_zddPrintMinterm.

  zddPrintCoverAux()

  Performs the recursive step of Cudd_zddPrintCover.

  zddSupportStep()

  Performs the recursive step of Cudd_zddSupport.

  zddClearFlag()

  Performs a DFS from f, clearing the LSB of the next pointers.

  ---

  Last updated on 20120204 17h33