cudd package abstract (Internal)

Internal data structures of the CUDD package.


Cudd_ApaAdd()
Adds two arbitrary precision integers.
Cudd_ApaCompareRatios()
Compares the ratios of two arbitrary precision integers to two unsigned ints.
Cudd_ApaCompare()
Compares two arbitrary precision integers.
Cudd_ApaCopy()
Makes a copy of an arbitrary precision integer.
Cudd_ApaCountMinterm()
Counts the number of minterms of a DD.
Cudd_ApaIntDivision()
Divides an arbitrary precision integer by an integer.
Cudd_ApaNumberOfDigits()
Finds the number of digits for an arbitrary precision integer.
Cudd_ApaPowerOfTwo()
Sets an arbitrary precision integer to a power of two.
Cudd_ApaPrintDecimal()
Prints an arbitrary precision integer in decimal format.
Cudd_ApaPrintDensity()
Prints the density of a BDD or ADD using arbitrary precision arithmetic.
Cudd_ApaPrintExponential()
Prints an arbitrary precision integer in exponential format.
Cudd_ApaPrintHex()
Prints an arbitrary precision integer in hexadecimal format.
Cudd_ApaPrintMintermExp()
Prints the number of minterms of a BDD or ADD in exponential format using arbitrary precision arithmetic.
Cudd_ApaPrintMinterm()
Prints the number of minterms of a BDD or ADD using arbitrary precision arithmetic.
Cudd_ApaSetToLiteral()
Sets an arbitrary precision integer to a one-digit literal.
Cudd_ApaShiftRight()
Shifts right an arbitrary precision integer by one binary place.
Cudd_ApaShortDivision()
Divides an arbitrary precision integer by a digit.
Cudd_ApaSubtract()
Subtracts two arbitrary precision integers.
Cudd_AutodynDisableZdd()
Disables automatic dynamic reordering of ZDDs.
Cudd_AutodynDisable()
Disables automatic dynamic reordering.
Cudd_AutodynEnableZdd()
Enables automatic dynamic reordering of ZDDs.
Cudd_AutodynEnable()
Enables automatic dynamic reordering of BDDs and ADDs.
Cudd_AverageDistance()
Computes the average distance between adjacent nodes.
Cudd_BddToAdd()
Converts a BDD to a 0-1 ADD.
Cudd_CProjection()
Computes the compatible projection of R w.r.t. cube Y.
Cudd_CheckKeys()
Checks for several conditions that should not occur.
Cudd_CheckZeroRef()
Checks the unique table for nodes with non-zero reference counts.
Cudd_ClassifySupport()
Classifies the variables in the support of two DDs.
Cudd_ClearErrorCode()
Clear the error code of a manager.
Cudd_CofMinterm()
Computes the fraction of minterms in the on-set of all the positive cofactors of a BDD or ADD.
Cudd_Cofactor()
Computes the cofactor of f with respect to g.
Cudd_Complement()
Returns the complemented version of a pointer.
Cudd_CountLeaves()
Counts the number of leaves in a DD.
Cudd_CountMinterm()
Counts the number of minterms of a DD.
Cudd_CountPath()
Counts the number of paths of a DD.
Cudd_DagSize()
Counts the number of nodes in a DD.
Cudd_DeadAreCounted()
Tells whether dead nodes are counted towards triggering reordering.
Cudd_DebugCheck()
Checks for inconsistencies in the DD heap.
Cudd_Decreasing()
Determines whether a BDD is negative unate in a variable.
Cudd_Density()
Computes the density of a BDD or ADD.
Cudd_Deref()
Decreases the reference count of node.
Cudd_DisableGarbageCollection()
Disables garbage collection.
Cudd_DisableReorderingReporting()
Disables reporting of reordering stats.
Cudd_DumpBlif()
Writes a blif file representing the argument BDDs.
Cudd_DumpDDcal()
Writes a DDcal file representing the argument BDDs.
Cudd_DumpDaVinci()
Writes a daVinci file representing the argument BDDs.
Cudd_DumpDot()
Writes a dot file representing the argument DDs.
Cudd_DumpFactoredForm()
Writes factored forms representing the argument BDDs.
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_EnableGarbageCollection()
Enables garbage collection.
Cudd_EnableReorderingReporting()
Enables reporting of reordering stats.
Cudd_EqualSupNorm()
Compares two ADDs for equality within tolerance.
Cudd_EquivDC()
Tells whether F and G are identical wherever D is 0.
Cudd_EstimateCofactorSimple()
Estimates the number of nodes in a cofactor of a DD.
Cudd_EstimateCofactor()
Estimates the number of nodes in a cofactor of a DD.
Cudd_Eval()
Returns the value of a DD for a given variable assignment.
Cudd_E()
Returns the else child of an internal node.
Cudd_FindEssential()
Finds the essential variables of a DD.
Cudd_FirstCube()
Finds the first cube of a decision diagram.
Cudd_FirstNode()
Finds the first node of a decision diagram.
Cudd_ForeachCube()
Iterates over the cubes of a decision diagram.
Cudd_ForeachNode()
Iterates over the nodes of a decision diagram.
Cudd_FreeTree()
Frees the variable group tree of the manager.
Cudd_FreeZddTree()
Frees the variable group tree of the manager.
Cudd_GarbageCollectionEnabled()
Tells whether garbage collection is enabled.
Cudd_GenFree()
Frees a CUDD generator.
Cudd_Increasing()
Determines whether a BDD is positive unate in a variable.
Cudd_IndicesToCube()
Builds a cube of BDD variables from an array of indices.
Cudd_Init()
Creates a new DD manager.
Cudd_IsComplement()
Returns 1 if a pointer is complemented.
Cudd_IsConstant()
Returns 1 if the node is a constant node.
Cudd_IsGenEmpty()
Queries the status of a generator.
Cudd_IterDerefBdd()
Decreases the reference count of BDD node n.
Cudd_LargestCube()
Finds a largest cube in a DD.
Cudd_MakeTreeNode()
Creates a new variable group.
Cudd_MakeZddTreeNode()
Creates a new ZDD variable group.
Cudd_NewApaNumber()
Allocates memory for an arbitrary precision integer.
Cudd_NextCube()
Generates the next cube of a decision diagram onset.
Cudd_NextNode()
Finds the next node of a decision diagram.
Cudd_NodeReadIndex()
Returns the index of the node.
Cudd_NotCond()
Complements a DD if a condition is true.
Cudd_Not()
Complements a DD.
Cudd_OutOfMem()
Warns that a memory allocation failed.
Cudd_OverApprox()
Extracts a dense superset from a BDD with Shiple's underapproximation method.
Cudd_Prime()
Returns the next prime >= p.
Cudd_PrintDebug()
Prints to the standard output a DD and its statistics.
Cudd_PrintInfo()
Prints out statistics and settings for a CUDD manager.
Cudd_PrintLinear()
Prints the linear transform matrix.
Cudd_PrintMinterm()
Prints a disjoint sum of products.
Cudd_PrintVersion()
Prints the package version number.
Cudd_Quit()
Deletes resources associated with a DD manager.
Cudd_Random()
Portable random number generator.
Cudd_ReadArcviolation()
Returns the current value of the arcviolation parameter used in group sifting.
Cudd_ReadBackground()
Reads the background constant of the manager.
Cudd_ReadCacheHits()
Returns the number of cache hits.
Cudd_ReadCacheLookUps()
Returns the number of cache look-ups.
Cudd_ReadCacheSlots()
Reads the number of slots in the cache.
Cudd_ReadCacheUsedSlots()
Reads the fraction of used slots in the cache.
Cudd_ReadDead()
Returns the number of dead nodes in the unique table.
Cudd_ReadEpsilon()
Reads the epsilon parameter of the manager.
Cudd_ReadErrorCode()
Returns the code of the last error.
Cudd_ReadGarbageCollectionTime()
Returns the time spent in garbage collection.
Cudd_ReadGarbageCollections()
Returns the number of times garbage collection has occurred.
Cudd_ReadGroupcheck()
Reads the groupcheck parameter of the manager.
Cudd_ReadIndex()
Returns the current position in the order of variable index.
Cudd_ReadInvPermZdd()
Returns the index of the ZDD variable currently in the i-th position of the order.
Cudd_ReadInvPerm()
Returns the index of the variable currently in the i-th position of the order.
Cudd_ReadKeys()
Returns the number of nodes in the unique table.
Cudd_ReadLinear()
Reads an entry of the linear transform matrix.
Cudd_ReadLogicZero()
Returns the logic zero constant of the manager.
Cudd_ReadLooseUpTo()
Reads the looseUpTo parameter of the manager.
Cudd_ReadMaxCacheHard()
Reads the maxCacheHard parameter of the manager.
Cudd_ReadMaxCache()
Reads the maxCache parameter of the manager.
Cudd_ReadMaxGrowth()
Reads the maxGrowth parameter of the manager.
Cudd_ReadMemoryInUse()
Returns the memory in use by the manager measured in bytes.
Cudd_ReadMinDead()
Reads the minDead parameter of the manager.
Cudd_ReadMinHit()
Reads the hit ratio that causes resizinig of the computed table.
Cudd_ReadMinusInfinity()
Reads the minus-infinity constant from the manager.
Cudd_ReadNodeCount()
Reports the number of nodes in BDDs and ADDs.
Cudd_ReadNodesDropped()
Returns the number of nodes dropped.
Cudd_ReadNodesFreed()
Returns the number of nodes freed.
Cudd_ReadNumberXovers()
Reads the current number of crossovers used by the genetic algorithm for reordering.
Cudd_ReadOne()
Returns the one constant of the manager.
Cudd_ReadPeakNodeCount()
Reports the peak number of nodes.
Cudd_ReadPermZdd()
Returns the current position of the i-th ZDD variable in the order.
Cudd_ReadPerm()
Returns the current position of the i-th variable in the order.
Cudd_ReadPlusInfinity()
Reads the plus-infinity constant from the manager.
Cudd_ReadPopulationSize()
Reads the current size of the population used by the genetic algorithm for reordering.
Cudd_ReadRecomb()
Returns the current value of the recombination parameter used in group sifting.
Cudd_ReadReorderingTime()
Returns the time spent in reordering.
Cudd_ReadReorderings()
Returns the number of times reordering has occurred.
Cudd_ReadSiftMaxSwap()
Reads the siftMaxSwap parameter of the manager.
Cudd_ReadSiftMaxVar()
Reads the siftMaxVar parameter of the manager.
Cudd_ReadSize()
Returns the number of BDD variables in existance.
Cudd_ReadSlots()
Returns the total number of slots of the unique table.
Cudd_ReadSymmviolation()
Returns the current value of the symmviolation parameter used in group sifting.
Cudd_ReadTree()
Returns the variable group tree of the manager.
Cudd_ReadUniqueLinks()
Returns the number of links followed in the unique table.
Cudd_ReadUniqueLookUps()
Returns the number of look-ups in the unique table.
Cudd_ReadUsedSlots()
Reads the fraction of used slots in the unique table.
Cudd_ReadVars()
Returns the i-th element of the vars array.
Cudd_ReadZddOne()
Returns the ZDD for the constant 1 function.
Cudd_ReadZddSize()
Returns the number of ZDD variables in existance.
Cudd_ReadZddTree()
Returns the variable group tree of the manager.
Cudd_ReadZero()
Returns the zero constant of the manager.
Cudd_RecursiveDerefZdd()
Decreases the reference count of ZDD node n.
Cudd_RecursiveDeref()
Decreases the reference count of node n.
Cudd_ReduceHeap()
Main dynamic reordering routine.
Cudd_Ref()
Increases the reference count of a node, if it is not saturated.
Cudd_Regular()
Returns the regular version of a pointer.
Cudd_RemapOverApprox()
Extracts a dense superset from a BDD with Shiple's underapproximation method.
Cudd_RemapUnderApprox()
Extracts a dense subset from a BDD with remapping underapproximation method.
Cudd_ReorderingReporting()
Returns 1 if reporting of reordering stats is enabled.
Cudd_ReorderingStatusZdd()
Reports the status of automatic dynamic reordering of ZDDs.
Cudd_ReorderingStatus()
Reports the status of automatic dynamic reordering of BDDs and ADDs.
Cudd_SetArcviolation()
Sets the value of the arcviolation parameter used in group sifting.
Cudd_SetBackground()
Sets the background constant of the manager.
Cudd_SetEpsilon()
Sets the epsilon parameter of the manager to ep.
Cudd_SetGroupcheck()
Sets the parameter groupcheck of the manager to gc.
Cudd_SetLooseUpTo()
Sets the looseUpTo parameter of the manager.
Cudd_SetMaxCacheHard()
Sets the maxCacheHard parameter of the manager.
Cudd_SetMaxCache()
Sets the maxCache parameter of the manager.
Cudd_SetMaxGrowth()
Sets the maxGrowth parameter of the manager.
Cudd_SetMinHit()
Sets the hit ratio that causes resizinig of the computed table.
Cudd_SetNumberXovers()
Sets the number of crossovers used by the genetic algorithm for reordering.
Cudd_SetPopulationSize()
Sets the size of the population used by the genetic algorithm for reordering.
Cudd_SetRecomb()
Sets the value of the recombination parameter used in group sifting.
Cudd_SetSiftMaxSwap()
Sets the siftMaxSwap parameter of the manager.
Cudd_SetSiftMaxVar()
Sets the siftMaxVar parameter of the manager.
Cudd_SetSymmviolation()
Sets the value of the symmviolation parameter used in group sifting.
Cudd_SetTree()
Sets the variable group tree of the manager.
Cudd_SetZddTree()
Sets the ZDD variable group tree of the manager.
Cudd_SharingSize()
Counts the number of nodes in an array of DDs.
Cudd_ShortestLength()
Find the length of the shortest path(s) in a DD.
Cudd_ShortestPath()
Finds a shortest path in a DD.
Cudd_ShuffleHeap()
Reorders variables according to given permutation.
Cudd_SolveEqn()
Implements the solution of F(x,y) = 0.
Cudd_SplitSet()
Returns m minterms from a BDD.
Cudd_Srandom()
Initializer for the portable random number generator.
Cudd_StdPostReordHook()
Sample hook function to call after reordering.
Cudd_StdPreReordHook()
Sample hook function to call before reordering.
Cudd_SubsetCompress()
Find a dense subset of BDD f.
Cudd_SubsetHeavyBranch()
Extracts a dense subset from a BDD with the heavy branch heuristic.
Cudd_SubsetShortPaths()
Extracts a dense subset from a BDD with the shortest paths heuristic.
Cudd_SupersetCompress()
Find a dense superset of BDD f.
Cudd_SupersetHeavyBranch()
Extracts a dense superset from a BDD with the heavy branch heuristic.
Cudd_SupersetShortPaths()
Extracts a dense superset from a BDD with the shortest paths heuristic.
Cudd_SupportSize()
Counts the variables on which a DD depends.
Cudd_Support()
Finds the variables on which a DD depends.
Cudd_SymmProfile()
Prints statistics on symmetric variables.
Cudd_TurnOffCountDead()
Causes the dead nodes not to be counted towards triggering reordering.
Cudd_TurnOnCountDead()
Causes the dead nodes to be counted towards triggering reordering.
Cudd_T()
Returns the then child of an internal node.
Cudd_UnderApprox()
Extracts a dense subset from a BDD with Shiple's underapproximation method.
Cudd_VectorSupportSize()
Counts the variables on which a set of DDs depends.
Cudd_VectorSupport()
Finds the variables on which a set of DDs depends.
Cudd_VerifySol()
Checks the solution of F(x,y) = 0.
Cudd_V()
Returns the value of a constant node.
Cudd_Xeqy()
Generates a BDD for the function x==y.
Cudd_Xgty()
Generates a BDD for the function x > y.
Cudd_addAgreement()
f if f==g; background if f!=g.
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_addBddPattern()
Converts an ADD to a BDD.
Cudd_addBddStrictThreshold()
Converts an ADD to a BDD.
Cudd_addBddThreshold()
Converts an ADD to a BDD.
Cudd_addCmpl()
Computes the complement of an ADD a la C language.
Cudd_addCompose()
Substitutes g for x_v in the ADD for f.
Cudd_addComputeCube()
Computes the cube of an array of ADD variables.
Cudd_addConstrain()
Computes f constrain c for ADDs.
Cudd_addConst()
Returns the ADD for constant c.
Cudd_addDiff()
Returns plusinfinity if f=g; returns min(f,g) if f!=g.
Cudd_addDivide()
Integer and floating point division.
Cudd_addEvalConst()
Checks whether ADD g is constant whenever ADD f is 1.
Cudd_addExistAbstract()
Existentially Abstracts all the variables in cube from f.
Cudd_addFindMax()
Finds the maximum discriminant of f.
Cudd_addFindMin()
Finds the minimum discriminant of f.
Cudd_addHamming()
Computes the Hamming distance ADD.
Cudd_addHarwell()
Reads in a matrix in the format of the Harwell-Boeing benchmark suite.
Cudd_addIteConstant()
Implements ITEconstant for ADDs.
Cudd_addIte()
Implements ITE(f,g,h).
Cudd_addIthBit()
Extracts the i-th bit from an ADD.
Cudd_addIthVar()
Returns the ADD variable with index i.
Cudd_addLeq()
Determines whether f is less than or equal to g.
Cudd_addMatrixMultiply()
Calculates the product of two matrices represented as ADDs.
Cudd_addMaximum()
Integer and floating point max.
Cudd_addMinimum()
Integer and floating point min.
Cudd_addMinus()
Integer and floating point subtraction.
Cudd_addNand()
NAND of two 0-1 ADDs.
Cudd_addNegate()
Computes the additive inverse of an ADD.
Cudd_addNewVarAtLevel()
Returns a new ADD variable at a specified level.
Cudd_addNewVar()
Returns a new ADD variable.
Cudd_addNonSimCompose()
Composes an ADD with a vector of 0-1 ADDs.
Cudd_addNor()
NOR of two 0-1 ADDs.
Cudd_addOneZeroMaximum()
Returns 1 if f > g and 0 otherwise.
Cudd_addOrAbstract()
Disjunctively abstracts all the variables in cube from the 0-1 ADD f.
Cudd_addOr()
Disjunction of two 0-1 ADDs.
Cudd_addPermute()
Permutes the variables of an ADD.
Cudd_addPlus()
Integer and floating point addition.
Cudd_addRead()
Reads in a sparse matrix.
Cudd_addResidue()
Builds an ADD for the residue modulo m of an n-bit number.
Cudd_addRestrict()
ADD restrict according to Coudert and Madre's algorithm (ICCAD90).
Cudd_addRoundOff()
Rounds off the discriminants of an ADD.
Cudd_addScalarInverse()
Computes the scalar inverse of an ADD.
Cudd_addSetNZ()
This operator sets f to the value of g wherever g != 0.
Cudd_addSwapVariables()
Swaps two sets of variables of the same size (x and y) in the ADD f.
Cudd_addThreshold()
f if f>=g; 0 if f<g.
Cudd_addTimesPlus()
Calculates the product of two matrices represented as ADDs.
Cudd_addTimes()
Integer and floating point multiplication.
Cudd_addTriangle()
Performs the triangulation step for the shortest path computation.
Cudd_addUnivAbstract()
Universally Abstracts all the variables in cube from f.
Cudd_addVectorCompose()
Composes an ADD with a vector of 0-1 ADDs.
Cudd_addWalsh()
Generates a Walsh matrix in ADD form.
Cudd_addXeqy()
Generates an ADD for the function x==y.
Cudd_addXnor()
XNOR of two 0-1 ADDs.
Cudd_addXor()
XOR of two 0-1 ADDs.
Cudd_bddAdjPermuteX()
Rearranges a set of variables in the BDD B.
Cudd_bddAndAbstract()
Takes the AND of two BDDs and simultaneously abstracts the variables in cube.
Cudd_bddAnd()
Computes the conjunction of two BDDs f and g.
Cudd_bddApproxConjDecomp()
Performs two-way conjunctive decomposition of a BDD.
Cudd_bddApproxDisjDecomp()
Performs two-way disjunctive decomposition of a BDD.
Cudd_bddBooleanDiff()
Computes the boolean difference of f with respect to x.
Cudd_bddCharToVect()
Computes a vector whose image equals a non-zero function.
Cudd_bddClippingAndAbstract()
Approximates the conjunction of two BDDs f and g and simultaneously abstracts the variables in cube.
Cudd_bddClippingAnd()
Approximates the conjunction of two BDDs f and g.
Cudd_bddCompose()
Substitutes g for x_v in the BDD for f.
Cudd_bddComputeCube()
Computes the cube of an array of BDD variables.
Cudd_bddConstrainDecomp()
BDD conjunctive decomposition as in McMillan's CAV96 paper.
Cudd_bddConstrain()
Computes f constrain c.
Cudd_bddCorrelationWeights()
Computes the correlation of f and g for given input probabilities.
Cudd_bddCorrelation()
Computes the correlation of f and g.
Cudd_bddExistAbstract()
Existentially abstracts all the variables in cube from f.
Cudd_bddGenConjDecomp()
Performs two-way conjunctive decomposition of a BDD.
Cudd_bddGenDisjDecomp()
Performs two-way disjunctive decomposition of a BDD.
Cudd_bddIntersect()
Returns a function included in the intersection of f and g.
Cudd_bddIsVarEssential()
Determines whether a given variable is essential with a given phase in a BDD.
Cudd_bddIsop()
Computes a BDD in the interval between L and U with a simple sum-of-produuct cover.
Cudd_bddIteConstant()
Implements ITEconstant(f,g,h).
Cudd_bddIterConjDecomp()
Performs two-way conjunctive decomposition of a BDD.
Cudd_bddIterDisjDecomp()
Performs two-way disjunctive decomposition of a BDD.
Cudd_bddIte()
Implements ITE(f,g,h).
Cudd_bddIthVar()
Returns the BDD variable with index i.
Cudd_bddLICompaction()
Performs safe minimization of a BDD.
Cudd_bddLeq()
Determines whether f is less than or equal to g.
Cudd_bddLiteralSetIntersection()
Computes the intesection of two sets of literals represented as BDDs.
Cudd_bddMinimize()
Finds a small BDD that agrees with f over c.
Cudd_bddNand()
Computes the NAND of two BDDs f and g.
Cudd_bddNewVarAtLevel()
Returns a new BDD variable at a specified level.
Cudd_bddNewVar()
Returns a new BDD variable.
Cudd_bddNor()
Computes the NOR of two BDDs f and g.
Cudd_bddOr()
Computes the disjunction of two BDDs f and g.
Cudd_bddPermute()
Permutes the variables of a BDD.
Cudd_bddPickArbitraryMinterms()
Picks k on-set minterms evenly distributed from given 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_bddRead()
Reads in a graph (without labels) given as a list of arcs.
Cudd_bddRealignDisable()
Disables realignment of ZDD order to BDD order.
Cudd_bddRealignEnable()
Enables realignment of BDD order to ZDD order.
Cudd_bddRealignmentEnabled()
Tells whether the realignment of BDD order to ZDD order is enabled.
Cudd_bddRestrict()
BDD restrict according to Coudert and Madre's algorithm (ICCAD90).
Cudd_bddSqueeze()
Finds a small BDD in a function interval.
Cudd_bddSwapVariables()
Swaps two sets of variables of the same size (x and y) in the BDD f.
Cudd_bddTransfer()
Convert a BDD from a manager to another one.
Cudd_bddUnivAbstract()
Universally abstracts all the variables in cube from f.
Cudd_bddVarConjDecomp()
Performs two-way conjunctive decomposition of a BDD.
Cudd_bddVarDisjDecomp()
Performs two-way disjunctive decomposition of a BDD.
Cudd_bddVarIsDependent()
Checks whether a variable is dependent on others in a function.
Cudd_bddVectorCompose()
Composes a BDD with a vector of BDDs.
Cudd_bddXnor()
Computes the exclusive NOR of two BDDs f and g.
Cudd_bddXorExistAbstract()
Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube.
Cudd_bddXor()
Computes the exclusive OR of two BDDs f and g.
Cudd_zddChange()
Substitutes a variable with its complement in a ZDD.
Cudd_zddCountDouble()
Counts the number of minterms of a ZDD.
Cudd_zddCountMinterm()
Counts the number of minterms of a ZDD.
Cudd_zddCount()
Counts the number of minterms in a ZDD.
Cudd_zddDagSize()
Counts the number of nodes in a ZDD.
Cudd_zddDiffConst()
Performs the inclusion test for ZDDs (P implies Q).
Cudd_zddDiff()
Computes the difference of two ZDDs.
Cudd_zddDivideF()
Modified version of Cudd_zddDivide.
Cudd_zddDivide()
Computes the quotient of two unate covers.
Cudd_zddDumpDot()
Writes a dot file representing the argument ZDDs.
Cudd_zddIntersect()
Computes the intersection of two ZDDs.
Cudd_zddIsop()
Computes an ISOP in ZDD form from BDDs.
Cudd_zddIte()
Computes the ITE of three ZDDs.
Cudd_zddIthVar()
Returns the ZDD variable with index i.
Cudd_zddPortFromBdd()
Converts a BDD into a ZDD.
Cudd_zddPortToBdd()
Converts a ZDD into a BDD.
Cudd_zddPrintDebug()
Prints to the standard output a ZDD and its statistics.
Cudd_zddPrintMinterm()
Cudd_zddPrintSubtable()
Prints the ZDD table.
Cudd_zddProduct()
Computes the product of two covers represented by ZDDs.
Cudd_zddReadNodeCount()
Reports the number of nodes in ZDDs.
Cudd_zddRealignDisable()
Disables realignment of ZDD order to BDD order.
Cudd_zddRealignEnable()
Enables realignment of ZDD order to BDD order.
Cudd_zddRealignmentEnabled()
Tells whether the realignment of ZDD order to BDD order is enabled.
Cudd_zddReduceHeap()
Main dynamic reordering routine for ZDDs.
Cudd_zddShuffleHeap()
Reorders ZDD variables according to given permutation.
Cudd_zddSubset0()
Computes the negative cofactor of a ZDD w.r.t. a variable.
Cudd_zddSubset1()
Computes the positive cofactor of a ZDD w.r.t. a variable.
Cudd_zddSymmProfile()
Prints statistics on symmetric ZDD variables.
Cudd_zddUnateProduct()
Computes the product of two unate covers.
Cudd_zddUnion()
Computes the union of two ZDDs.
Cudd_zddVarsFromBddVars()
Creates one or more ZDD variables for each BDD variable.
Cudd_zddWeakDivF()
Modified version of Cudd_zddWeakDiv.
Cudd_zddWeakDiv()
Applies weak division to two covers.
DD_LSDIGIT()
Extract the least significant digit of a double digit.
DD_MINUS_INFINITY()
Returns the minus infinity constant node.
DD_MSDIGIT()
Extract the most significant digit of a double digit.
DD_ONE()
Returns the constant 1 node.
DD_PLUS_INFINITY()
Returns the plus infinity constant node.
DD_ZERO()
Returns the arithmetic 0 constant node.
cuddAddCmplRecur()
Performs the recursive step of Cudd_addCmpl.
cuddAddComposeRecur()
Performs the recursive step of Cudd_addCompose.
cuddAddConstrainRecur()
Performs the recursive step of Cudd_addConstrain.
cuddAddExistAbstractRecur()
Performs the recursive step of Cudd_addExistAbstract.
cuddAddIteRecur()
Implements the recursive step of Cudd_addIte(f,g,h).
cuddAddNegateRecur()
Implements the recursive step of Cudd_addNegate.
cuddAddOrAbstractRecur()
Performs the recursive step of Cudd_addOrAbstract.
cuddAddRestrictRecur()
Performs the recursive step of Cudd_addRestrict.
cuddAddRoundOffRecur()
Implements the recursive step of Cudd_addRoundOff.
cuddAddScalarInverseRecur()
Performs the recursive step of addScalarInverse.
cuddAddUnivAbstractRecur()
Performs the recursive step of Cudd_addUnivAbstract.
cuddAllocNode()
Fast storage allocation for DdNodes in the table.
cuddAnnealing()
Get new variable-order by simulated annealing algorithm.
cuddBddAlignToZdd()
Reorders ZDD variables according to the order of the BDD variables.
cuddBddAndAbstractRecur()
Takes the AND of two BDDs and simultaneously abstracts the variables in cube.
cuddBddAndRecur()
Implements the recursive step of Cudd_bddAnd.
cuddBddBooleanDiffRecur()
Performs the recursive steps of Cudd_bddBoleanDiff.
cuddBddClippingAndAbstract()
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.
cuddBddComposeRecur()
Performs the recursive step of Cudd_bddCompose.
cuddBddConstrainRecur()
Performs the recursive step of Cudd_bddConstrain.
cuddBddExistAbstractRecur()
Performs the recursive steps of Cudd_bddExistAbstract.
cuddBddIntersectRecur()
Implements the recursive step of Cudd_bddIntersect.
cuddBddIsop()
Performs the recursive step of Cudd_bddIsop.
cuddBddIteRecur()
Implements the recursive step of Cudd_bddIte.
cuddBddLICompaction()
Performs safe minimization of a BDD.
cuddBddLiteralSetIntersectionRecur()
Performs the recursive step of Cudd_bddLiteralSetIntersection.
cuddBddRestrictRecur()
Performs the recursive step of Cudd_bddRestrict.
cuddBddTransfer()
Convert a BDD from a manager to another one.
cuddBddXorExistAbstractRecur()
Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube.
cuddBddXorRecur()
Implements the recursive step of Cudd_bddXor.
cuddCProjectionRecur()
Performs the recursive step of Cudd_CProjection.
cuddCacheFlush()
Flushes the cache.
cuddCacheProfile()
Computes and prints a profile of the cache usage.
cuddCacheResize()
Resizes the cache.
cuddCheckCube()
Checks whether g is the BDD of a cube.
cuddCofactorRecur()
Performs the recursive step of Cudd_Cofactor.
cuddCollectNodes()
Recursively collects all the nodes of a DD in a symbol table.
cuddComputeFloorLog2()
Returns the floor of the logarithm to the base 2.
cuddDeallocNode()
Adds node to the head of the free list.
cuddDeref()
Decreases the reference count of a node, if it is not saturated.
cuddDestroySubtables()
Destroys the n most recently created subtables in a unique table.
cuddDynamicAllocNode()
Dynamically allocates a Node.
cuddExact()
Exact variable ordering algorithm.
cuddE()
Returns the else child of an internal node.
cuddFreeTable()
Frees the resources associated to a unique table.
cuddGarbageCollectZdd()
Performs garbage collection on a ZDD unique table.
cuddGarbageCollect()
Performs garbage collection on a unique table.
cuddGa()
Genetic algorithm for DD reordering.
cuddGetBranches()
Computes the children of g.
cuddHashTableInit()
Initializes a hash table.
cuddHashTableInsert1()
Inserts an item in a hash table.
cuddHashTableInsert2()
Inserts an item in a hash table.
cuddHashTableInsert3()
Inserts an item in a hash table.
cuddHashTableInsert()
Inserts an item in a hash table.
cuddHashTableLookup1()
Looks up a key consisting of one pointer in a hash table.
cuddHashTableLookup2()
Looks up a key consisting of two pointers in a hash table.
cuddHashTableLookup3()
Looks up a key consisting of three pointers in a hash table.
cuddHashTableLookup()
Looks up a key in a hash table.
cuddHashTableQuit()
Shuts down a hash table.
cuddHeapProfile()
Prints information about the heap.
cuddIZ()
Finds the current position of ZDD variable index in the order.
cuddInitCache()
Initializes the computed table.
cuddInitInteract()
Initializes the interaction matrix.
cuddInitTable()
Creates and initializes the unique table.
cuddInsertSubtables()
Inserts n new subtables in a unique table at level.
cuddIsConstant()
Returns 1 if the node is a constant node.
cuddI()
Finds the current position of variable index in the order.
cuddLevelQueueDequeue()
Remove an item from the front of a level queue.
cuddLevelQueueEnqueue()
Inserts a new key in a level queue.
cuddLevelQueueInit()
Initializes a level queue.
cuddLevelQueueQuit()
Shuts down a level queue.
cuddLinearAndSifting()
BDD reduction based on combination of sifting and linear transformations.
cuddLocalCacheClearAll()
Clears the local caches of a manager.
cuddLocalCacheClearDead()
Clears the dead entries of the local caches of a manager.
cuddLocalCacheInit()
Initializes a local computed table.
cuddLocalCacheInsert()
Inserts a result in a local cache.
cuddLocalCacheLookup()
Looks up in a local cache.
cuddLocalCacheProfile()
Computes and prints a profile of a local cache usage.
cuddLocalCacheQuit()
Shuts down a local computed table.
cuddNextHigh()
Finds the next subtable with a larger index.
cuddNextLow()
Finds the next subtable with a smaller index.
cuddPrintNode()
Prints out information on a node.
cuddP()
Prints a DD to the standard output. One line per node is printed.
cuddReclaimZdd()
Brings children of a dead ZDD node back.
cuddReclaim()
Brings children of a dead node back.
cuddRef()
Increases the reference count of a node, if it is not saturated.
cuddRemapUnderApprox()
Applies the remapping underappoximation algorithm.
cuddResizeTableZdd()
Increases the number of ZDD subtables in a unique table so that it meets or exceeds index.
cuddSatDec()
Saturating decrement operator.
cuddSatInc()
Saturating increment operator.
cuddSetInteract()
Set interaction matrix entries.
cuddSifting()
Implementation of Rudell's sifting algorithm.
cuddSolveEqnRecur()
Implements the recursive step of Cudd_SolveEqn.
cuddSplitSetRecur()
Implements the recursive step of Cudd_SplitSet.
cuddStCountfree()
Frees the memory used to store the minterm counts recorded in the visited table.
cuddSubsetHeavyBranch()
The main procedure that returns a subset by choosing the heavier branch in the BDD.
cuddSubsetShortPaths()
The outermost procedure to return a subset of the given BDD with the shortest path lengths.
cuddSwapInPlace()
Swaps two adjacent variables.
cuddSwapping()
Reorders variables by a sequence of (non-adjacent) swaps.
cuddSymmCheck()
Checks for symmetry of x and y.
cuddSymmSiftingConv()
Symmetric sifting to convergence algorithm.
cuddSymmSifting()
Symmetric sifting algorithm.
cuddTestInteract()
Test interaction matrix entries.
cuddTreeSifting()
Tree sifting algorithm.
cuddT()
Returns the then child of an internal node.
cuddUnderApprox()
Applies Tom Shiple's underappoximation algorithm.
cuddUniqueConst()
Checks the unique table for the existence of a constant node.
cuddUniqueInterZdd()
Checks the unique table for the existence of an internal ZDD node.
cuddUniqueInter()
Checks the unique table for the existence of an internal node.
cuddVerifySol()
Implements the recursive step of Cudd_VerifySol.
cuddV()
Returns the value of a constant node.
cuddWindowReorder()
Reorders by applying the method of the sliding window.
cuddZddAlignToBdd()
Reorders ZDD variables according to the order of the BDD variables.
cuddZddChangeAux()
Performs the recursive step of Cudd_zddChange.
cuddZddChange()
Substitutes a variable with its complement in a ZDD.
cuddZddDiff()
Performs the recursive step of Cudd_zddDiff.
cuddZddDivideF()
Performs the recursive step of Cudd_zddDivideF.
cuddZddDivide()
Performs the recursive step of Cudd_zddDivide.
cuddZddFreeUniv()
Frees the ZDD universe.
cuddZddGetCofactors2()
Computes the two-way decomposition of f w.r.t. v.
cuddZddGetCofactors3()
Computes the three-way decomposition of f w.r.t. v.
cuddZddGetNodeIVO()
Wrapper for cuddUniqueInterZdd that is independent of variable ordering.
cuddZddGetNode()
Wrapper for cuddUniqueInterZdd.
cuddZddInitUniv()
Initializes the ZDD universe.
cuddZddIntersect()
Performs the recursive step of Cudd_zddIntersect.
cuddZddIsop()
Performs the recursive step of Cudd_zddIsop.
cuddZddIte()
Performs the recursive step of Cudd_zddIte.
cuddZddLinearInPlace()
Linearly combines two adjacent variables.
cuddZddLinearSifting()
Implementation of the linear sifting algorithm for ZDDs.
cuddZddNextHigh()
Finds the next subtable with a larger index.
cuddZddNextLow()
Finds the next subtable with a smaller index.
cuddZddProduct()
Performs the recursive step of Cudd_zddProduct.
cuddZddP()
Prints a ZDD to the standard output. One line per node is printed.
cuddZddSifting()
Implementation of Rudell's sifting algorithm.
cuddZddSubset0()
Computes the negative cofactor of a ZDD w.r.t. a variable.
cuddZddSubset1()
Computes the positive cofactor of a ZDD w.r.t. a variable.
cuddZddSwapInPlace()
Swaps two adjacent variables.
cuddZddSwapping()
Reorders variables by a sequence of (non-adjacent) swaps.
cuddZddSymmCheck()
Checks for symmetry of x and y.
cuddZddSymmSiftingConv()
Symmetric sifting to convergence algorithm for ZDDs.
cuddZddSymmSifting()
Symmetric sifting algorithm for ZDDs.
cuddZddTreeSifting()
Tree sifting algorithm for ZDDs.
cuddZddUnateProduct()
Performs the recursive step of Cudd_zddUnateProduct.
cuddZddUnion()
Performs the recursive step of Cudd_zddUnion.
cuddZddUniqueCompare()
Comparison function used by qsort.
cuddZddWeakDivF()
Performs the recursive step of Cudd_zddWeakDivF.
cuddZddWeakDiv()
Performs the recursive step of Cudd_zddWeakDiv.
ddAbs()
Computes the absolute value of a number.
ddCHash2()
Hash function for the cache for functions with two operands.
ddCHash()
Hash function for the cache.
ddEqualVal()
Returns 1 if the absolute value of the difference of the two arguments x and y is less than e.
ddHash()
Hash function for the unique table.
ddLCHash2()
Computes hash function for keys of two operands.
ddLCHash3()
Computes hash function for keys of three operands.
ddMax()
Computes the maximum of two numbers.
ddMin()
Computes the minimum of two numbers.
lqHash()
Hash function for the table of a level queue.
()
Adds a function to a hook.
()
Applies op to the corresponding discriminants of f and g.
()
Checks whether a function is in a hook.
()
Enforces DD_MINUS_INF_VAL <= x <= DD_PLUS_INF_VAL.
()
Inserts a result in the cache for a function with two operands.
()
Inserts a result in the cache for a function with two operands.
()
Inserts a result in the cache.
()
Looks up in the cache for the result of op applied to f and g.
()
Looks up in the cache for the result of op applied to f and g.
()
Looks up in the cache for the result of op applied to f, g, and h.
()
Looks up in the cache for the result of op applied to f, g, and h.
()
Looks up in the cache for the result of op applied to f, g, and h.
()
Looks up in the cache for the result of op applied to f.
()
Looks up in the cache for the result of op applied to f.
()
Performs the recursive step of Cudd_addApply.
()
Removes a function from a hook.
()
Selects pairs from R using a priority function.
()
Sifts down a variable until it reaches position xHigh.
()
Sifts from treenode->low to treenode->high.
()
Sifts one variable up and down until it has taken all positions. Checks for aggregation.
()
Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much.

Generated automatically by extdoc on 980512