cudd package abstract

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