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_CheckCube()
Checks whether g is the BDD of a cube.
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_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_DisableOrderingMonitoring()
Disables monitoring of ordering.
Cudd_DisableReorderingReporting()
Disables reporting of reordering stats.
Cudd_Disequality()
Generates a BDD for the function x - y != c.
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_EnableOrderingMonitoring()
Enables monitoring of ordering.
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_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_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_IncreaseTimeLimit()
Increases the time limit for the manager.
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_Inequality()
Generates a BDD for the function x - y ≥ c.
Cudd_Init()
Creates a new DD manager.
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.
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_OrderingMonitoring()
Returns 1 if monitoring of ordering is enabled.
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_PrintGroupedOrder()
Hook function to print the current variable order.
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_ReadElapsedTime()
Returns the time elapsed since the start time of the manager.
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_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_ReadMaxReorderings()
Returns the maximum number of times reordering may be invoked.
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_ReadOrderRandomization()
Returns the order randomization factor.
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_ReadStartTime()
Returns the start time of the manager.
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_ReadTimeLimit()
Returns the time limit for the manager.
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_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_Reserve()
Expand manager without creating variables.
Cudd_ResetStartTime()
Resets the start time of the manager.
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_SetMaxReorderings()
Sets the maximum number of times reordering may be invoked.
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_SetOrderRandomization()
Sets the order randomization factor.
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_SetStartTime()
Sets the start time 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_SetTimeLimit()
Sets the time limit for the manager.
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_SupportIndices()
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_TimeLimited()
Returns true if the time limit for the manager is set.
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_UnderApprox()
Extracts a dense subset from a BDD with Shiple's underapproximation method.
Cudd_UnsetTimeLimit()
Unsets the time limit for the manager.
Cudd_UpdateTimeLimit()
Updates the time limit for the manager.
Cudd_VectorSupportIndex()
Finds the variables on which a set of DDs depends.
Cudd_VectorSupportIndices()
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_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_bddExistAbstractLimit()
Existentially abstracts all the variables in cube from f.
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_bddInterval()
Generates a BDD for the function lowerB ≤ x ≤ upperB.
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-product cover.
Cudd_bddIteConstant()
Implements ITEconstant(f,g,h).
Cudd_bddIteLimit()
Implements ITE(f,g,h). Returns NULL if too many nodes are required.
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_bddLargestPrimeUnate()
Find a largest prime of a unate function.
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_bddMaximallyExpand()
Expands lb to prime implicants of (f and ub).
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_bddOrLimit()
Computes the disjunction 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_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_bddXnorLimit()
Computes the exclusive NOR of two BDDs f and g. Returns NULL if too many nodes are required.
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_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_zddSupport()
Finds the variables on which a ZDD depends.
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.

Last updated on 20120204 17h33