cudd package abstract (Internal)

Internal data structures of the CUDD package.


Cudd_AddHook()
Adds a function to a hook.
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_BddToCubeArray()
Builds a positional array from the BDD of a cube.
Cudd_BiasedOverApprox()
Extracts a dense superset from a BDD with the biased underapproximation method.
Cudd_BiasedUnderApprox()
Extracts a dense subset from a BDD with the biased underapproximation method.
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_CountPathsToNonZero()
Counts the number of paths to a non-zero terminal of a DD.
Cudd_CountPath()
Counts the number of paths of a DD.
Cudd_CubeArrayToBdd()
Builds the BDD of a cube from a positional array.
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_DelayedDerefBdd()
Decreases the reference count of BDD node n.
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_DumpBlifBody()
Writes a blif body representing the argument BDDs.
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_EpdCountMinterm()
Counts the number of minterms of a DD with extended precision.
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_ExpectedUsedSlots()
Computes the expected fraction of used slots in the unique table.
Cudd_E()
Returns the else child of an internal node.
Cudd_FindEssential()
Finds the essential variables of a DD.
Cudd_FindTwoLiteralClauses()
Finds the two literal clauses of a DD.
Cudd_FirstCube()
Finds the first cube of a decision diagram.
Cudd_FirstNode()
Finds the first node of a decision diagram.
Cudd_FirstPrime()
Finds the first prime of a Boolean function.
Cudd_ForeachCube()
Iterates over the cubes of a decision diagram.
Cudd_ForeachNode()
Iterates over the nodes of a decision diagram.
Cudd_ForeachPrime()
Iterates over the primes of a Boolean function.
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_IsInHook()
Checks whether a function is in a hook.
Cudd_IsNonConstant()
Returns 1 if a DD node is not constant.
Cudd_IterDerefBdd()
Decreases the reference count of BDD node n.
Cudd_LargestCube()
Finds a largest cube in a DD.
Cudd_MakeBddFromZddCover()
Converts a ZDD cover to a BDD graph.
Cudd_MakeTreeNode()
Creates a new variable group.
Cudd_MakeZddTreeNode()
Creates a new ZDD variable group.
Cudd_MinHammingDist()
Returns the minimum Hamming distance between f and minterm.
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_NextPrime()
Generates the next prime of a Boolean function.
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_PrintTwoLiteralClauses()
Prints the two literal clauses of a DD.
Cudd_PrintVersion()
Prints the package version number.
Cudd_PrioritySelect()
Selects pairs from R using a priority function.
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_ReadIthClause()
Accesses the i-th clause of a DD.
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()
Returns the soft limit for the cache size.
Cudd_ReadMaxGrowthAlternate()
Reads the maxGrowthAlt parameter of the manager.
Cudd_ReadMaxGrowth()
Reads the maxGrowth parameter of the manager.
Cudd_ReadMaxLive()
Reads the maximum allowed number of live nodes.
Cudd_ReadMaxMemory()
Reads the maximum allowed memory.
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 rate that causes resizinig of the computed table.
Cudd_ReadMinusInfinity()
Reads the minus-infinity constant from the manager.
Cudd_ReadNextReordering()
Returns the threshold for the next dynamic reordering.
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_ReadPeakLiveNodeCount()
Reports the peak number of live nodes.
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_ReadRecursiveCalls()
Returns the number of recursive calls.
Cudd_ReadReorderingCycle()
Reads the reordCycle parameter of the manager.
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_ReadStderr()
Reads the stderr of a manager.
Cudd_ReadStdout()
Reads the stdout of a manager.
Cudd_ReadSwapSteps()
Reads the number of elementary reordering steps.
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 the remapping underapproximation method.
Cudd_RemapUnderApprox()
Extracts a dense subset from a BDD with the remapping underapproximation method.
Cudd_RemoveHook()
Removes a function from a hook.
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_SetMaxGrowthAlternate()
Sets the maxGrowthAlt parameter of the manager.
Cudd_SetMaxGrowth()
Sets the maxGrowth parameter of the manager.
Cudd_SetMaxLive()
Sets the maximum allowed number of live nodes.
Cudd_SetMaxMemory()
Sets the maximum allowed memory.
Cudd_SetMinHit()
Sets the hit rate that causes resizinig of the computed table.
Cudd_SetNextReordering()
Sets the threshold for the next dynamic reordering.
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_SetReorderingCycle()
Sets the reordCycle parameter of the manager.
Cudd_SetSiftMaxSwap()
Sets the siftMaxSwap parameter of the manager.
Cudd_SetSiftMaxVar()
Sets the siftMaxVar parameter of the manager.
Cudd_SetStderr()
Sets the stderr of a manager.
Cudd_SetStdout()
Sets the stdout of a 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_SetVarMap()
Registers a variable mapping with 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_SubsetWithMaskVars()
Extracts a subset from a BDD.
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_SupportIndex()
Finds the variables on which a DD depends.
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_VectorSupportIndex()
Finds the variables on which a set of DDs depends.
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_addApply()
Applies op to the corresponding discriminants of f and 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_addGeneralVectorCompose()
Composes an ADD with a vector of ADDs.
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_addLog()
Natural logarithm of an ADD.
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_addMonadicApply()
Applies op to the discriminants of f.
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_addOuterSum()
Takes the minimum of a matrix and the outer sum of two vectors.
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_bddAndAbstractLimit()
Takes the AND of two BDDs and simultaneously abstracts the variables in cube. Returns NULL if too many nodes are required.
Cudd_bddAndAbstract()
Takes the AND of two BDDs and simultaneously abstracts the variables in cube.
Cudd_bddAndLimit()
Computes the conjunction of two BDDs f and g. Returns NULL if too many nodes are required.
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_bddBindVar()
Prevents sifting of a variable.
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_bddClosestCube()
Finds a cube of f at minimum Hamming distance from 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_bddIsNsVar()
Checks whether a variable is next state.
Cudd_bddIsPiVar()
Checks whether a variable is primary input.
Cudd_bddIsPsVar()
Checks whether a variable is present state.
Cudd_bddIsVarEssential()
Determines whether a given variable is essential with a given phase in a BDD.
Cudd_bddIsVarHardGroup()
Checks whether a variable is set to be in a hard group.
Cudd_bddIsVarToBeGrouped()
Checks whether a variable is set to be grouped.
Cudd_bddIsVarToBeUngrouped()
Checks whether a variable is set to be ungrouped.
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_bddLeqUnless()
Tells whether f is less than of equal to G unless D is 1.
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_bddMakePrime()
Expands cube to a prime implicant of f.
Cudd_bddMinimize()
Finds a small BDD that agrees with f over c.
Cudd_bddNPAnd()
Computes f non-polluting-and g.
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_bddPrintCover()
Prints a sum of prime implicants of a BDD.
Cudd_bddReadPairIndex()
Reads a corresponding pair index for a given index.
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_bddResetVarToBeGrouped()
Resets a variable not to be grouped.
Cudd_bddRestrict()
BDD restrict according to Coudert and Madre's algorithm (ICCAD90).
Cudd_bddSetNsVar()
Sets a variable type to next state.
Cudd_bddSetPairIndex()
Sets a corresponding pair index for a given index.
Cudd_bddSetPiVar()
Sets a variable type to primary input.
Cudd_bddSetPsVar()
Sets a variable type to present state.
Cudd_bddSetVarHardGroup()
Sets a variable to be a hard group.
Cudd_bddSetVarToBeGrouped()
Sets a variable to be grouped.
Cudd_bddSetVarToBeUngrouped()
Sets a variable to be ungrouped.
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_bddUnbindVar()
Allows the sifting of a variable.
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_bddVarIsBound()
Tells whether a variable can be sifted.
Cudd_bddVarIsDependent()
Checks whether a variable is dependent on others in a function.
Cudd_bddVarMap()
Remaps the variables of a BDD using the default variable map.
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_tlcInfoFree()
Frees a DdTlcInfo Structure.
Cudd_zddChange()
Substitutes a variable with its complement in a ZDD.
Cudd_zddComplement()
Computes a complement cover for a ZDD node.
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_zddCoverPathToString()
Converts a path of a ZDD representing a cover to a string.
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_zddFirstPath()
Finds the first path of a ZDD.
Cudd_zddForeachPath()
Iterates over the paths of a ZDD.
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_zddNextPath()
Generates the next path of a ZDD.
Cudd_zddPortFromBdd()
Converts a BDD into a ZDD.
Cudd_zddPortToBdd()
Converts a ZDD into a BDD.
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_zddPrintMinterm()
Prints a disjoint sum of product form for a ZDD.
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.
cuddAddApplyRecur()
Performs the recursive step of Cudd_addApply.
cuddAddBddDoPattern()
Performs the recursive step for Cudd_addBddPattern.
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).
cuddAddMonadicApplyRecur()
Performs the recursive step of Cudd_addMonadicApply.
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.
cuddAdjust()
Enforces DD_MINUS_INF_VAL <= x <= DD_PLUS_INF_VAL.
cuddAllocNode()
Fast storage allocation for DdNodes in the table.
cuddAnnealing()
Get new variable-order by simulated annealing algorithm.
cuddBddAlignToZdd()
Reorders BDD variables according to the order of the ZDD 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.
cuddBddClosestCube()
Performs the recursive step of Cudd_bddClosestCube.
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.
cuddBddMakePrime()
Performs the recursive step of Cudd_bddMakePrime.
cuddBddNPAndRecur()
Implements the recursive step of Cudd_bddAnd.
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.
cuddBiasedUnderApprox()
Applies the biased remapping underappoximation algorithm.
cuddCProjectionRecur()
Performs the recursive step of Cudd_CProjection.
cuddCacheFlush()
Flushes the cache.
cuddCacheInsert1()
Inserts a result in the cache for a function with two operands.
cuddCacheInsert2()
Inserts a result in the cache for a function with two operands.
cuddCacheInsert()
Inserts a result in the cache.
cuddCacheLookup1Zdd()
Looks up in the cache for the result of op applied to f.
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.
cuddCacheLookup2()
Looks up in the cache for the result of op applied to f and g.
cuddCacheLookupZdd()
Looks up in the cache for the result of op applied to f, g, and h.
cuddCacheLookup()
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.
cuddCheckCube()
Checks whether g is the BDD of a cube.
cuddClean()
Clears the 4 least significant bits of a pointer.
cuddClearDeathRow()
Clears the death row.
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.
cuddConstantLookup()
Looks up in the cache for the result of op applied to f, g, and h.
cuddDeallocMove()
Adds node to the head of the free list.
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.
cuddGarbageCollect()
Performs garbage collection on the unique tables.
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.
cuddInitLinear()
Initializes the linear transform 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.
cuddIsInDeathRow()
Checks whether a node is in the death row.
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.
cuddLinearInPlace()
Linearly combines two adjacent variables.
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.
cuddMakeBddFromZddCover()
Converts a ZDD cover to a BDD graph.
cuddNextHigh()
Finds the next subtable with a larger index.
cuddNextLow()
Finds the next subtable with a smaller index.
cuddNodeArray()
Recursively collects all the nodes of a DD in an array.
cuddPrintNode()
Prints out information on a node.
cuddPrintVarGroups()
Prints the variable groups as a parenthesized list.
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.
cuddRehash()
Rehashes a unique subtable.
cuddRemapUnderApprox()
Applies the remapping underappoximation algorithm.
cuddResizeLinear()
Resizes the linear transform matrix.
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.
cuddShrinkDeathRow()
Shrinks the death row.
cuddShrinkSubtable()
Shrinks a subtable.
cuddSifting()
Implementation of Rudell's sifting algorithm.
cuddSlowTableGrowth()
Adjusts parameters of a table to slow down its growth.
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.
cuddTimesInDeathRow()
Counts how many times a node is in the death row.
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.
cuddUniqueInterIVO()
Wrapper for cuddUniqueInter that is independent of variable ordering.
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.
cuddUpdateInteractionMatrix()
Updates the interaction matrix.
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.
cuddZddComplement()
Computes a complement of a ZDD node.
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.
cuddZddGetNegVarIndex()
Returns the index of negative ZDD variable.
cuddZddGetNegVarLevel()
Returns the level of negative ZDD variable.
cuddZddGetNodeIVO()
Wrapper for cuddUniqueInterZdd that is independent of variable ordering.
cuddZddGetNode()
Wrapper for cuddUniqueInterZdd.
cuddZddGetPosVarIndex()
Returns the index of positive ZDD variable.
cuddZddGetPosVarLevel()
Returns the level of positive ZDD variable.
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.
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.
statLine()
Outputs a line of stats.

Generated automatically by extdoc on 20050517