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