cudd package abstract

AssessPathLength(): Chooses the maximum allowable path length of nodes under the threshold.
BAapplyBias(): Finds don't care nodes.
BAmarkNodes(): Marks nodes for remapping.
BuildConjuncts(): Builds the conjuncts recursively, bottom up.
BuildSubsetBdd(): Builds the BDD with nodes labeled with path length less than or equal to maxpath
BuildSubsetBdd(): Builds the subset BDD using the heavy branch method.
CheckInTables(): Check if the two pairs exist in the table, If any of the conjuncts do exist, store in the cache and return the corresponding pair.
CheckTablesCacheAndReturn(): Check the tables for the existence of pair and return one combination, cache the result.
ConjunctsFree(): Free factors structure
CorrelCleanUp(): Frees memory associated with hash table.
CorrelCompare(): Compares two hash table entries.
CorrelHash(): Hashes a hash table entry.
CountMinterms(): Count the number of minterms of each node ina a BDD and store it in a hash table.
CreateBotDist(): Get longest distance of node from constant.
CreateBotDist(): Labels each node with the shortest distance from the constant.
CreatePathTable(): The outer procedure to label each node with its shortest distance from the root and constant
CreateTopDist(): Labels each node with its shortest distance from the root
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_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_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_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_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 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_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_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_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_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_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_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-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_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.
MarkCacheCleanUp(): Frees memory associated with computed table of cuddBddLICMarkEdges.
MarkCacheCompare(): Comparison function for the computed table of cuddBddLICMarkEdges.
MarkCacheHash(): Hash function for the computed table of cuddBddLICMarkEdges.
PMX(): Performs the crossover between two parents.
PairInTables(): Check whether the given pair is in the tables.
PickOnePair(): Check the tables for the existence of pair and return one combination, store in cache.
RAbuildSubset(): Builds the subset BDD for cuddRemapUnderApprox.
RAmarkNodes(): Marks nodes for remapping.
ResizeCountMintermPages(): Resize the number of pages allocated to store the minterm counts.
ResizeCountNodePages(): Resize the number of pages allocated to store the node counts.
ResizeNodeDataPages(): Resize the number of pages allocated to store the node data.
ResizeNodeDistPages(): Resize the number of pages allocated to store the distances related to each node.
ResizeQueuePages(): Resize the number of pages allocated to store nodes in the BFS traversal of the Bdd .
StoreNodes(): Procedure to recursively store nodes that are retained in the subset.
SubsetCountMintermAux(): Recursively counts minterms of each node in the DAG.
SubsetCountMinterm(): Counts minterms of each node in the DAG
SubsetCountNodesAux(): Recursively counts the number of nodes under the dag. Also counts the number of nodes under the lighter child of this node.
SubsetCountNodes(): Counts the nodes under the current node and its lighter child
UAbuildSubset(): Builds the subset BDD.
UAmarkNodes(): Marks nodes for replacement by zero.
ZeroCase(): If one child is zero, do explicitly what Restrict does or better
addBddDoInterval(): Performs the recursive step for Cudd_addBddInterval.
addBddDoIthBit(): Performs the recursive step for Cudd_addBddIthBit.
addBddDoStrictThreshold(): Performs the recursive step for Cudd_addBddStrictThreshold.
addBddDoThreshold(): Performs the recursive step for Cudd_addBddThreshold.
addCheckPositiveCube(): Checks whether cube is an ADD representing the product of positive literals.
addDoIthBit(): Performs the recursive step for Cudd_addIthBit.
addMMRecur(): Performs the recursive step of Cudd_addMatrixMultiply.
addMultiplicityGroups(): Adds multiplicity groups to a ZDD variable group tree.
addTriangleRecur(): Performs the recursive step of Cudd_addTriangle.
addVarToConst(): Replaces variables with constants if possible (part of canonical form).
addWalshInt(): Implements the recursive step of Cudd_addWalsh.
array_compare(): Comparison function for the computed table.
array_hash(): Hash function for the computed table.
bddAnnotateMintermCount(): Annotates every node in the BDD node with its minterm count.
bddCheckPositiveCube(): Checks whether cube is an BDD representing the product of positive literals.
bddCorrelationAux(): Performs the recursive step of Cudd_bddCorrelation.
bddCorrelationWeightsAux(): Performs the recursive step of Cudd_bddCorrelationWeigths.
bddFixTree(): Fixes the BDD variable group tree after a shuffle.
bddVarToCanonicalSimple(): Picks unique member from equiv expressions.
bddVarToCanonical(): Picks unique member from equiv expressions.
bddVarToConst(): Replaces variables with constants if possible.
beforep(): Returns true iff the first argument precedes the second in the clause order.
bitVectorAlloc(): Allocates a bit vector.
bitVectorClear(): Clears a bit vector.
bitVectorFree(): Frees a bit vector.
bitVectorRead(): Returns the i-th entry of a bit vector.
bitVectorSet(): Sets the i-th entry of a bit vector to a value.
build_dd(): Builds a DD from a given order.
checkSymmInfo(): Check symmetry condition.
computeClausesWithUniverse(): Computes the two-literal clauses for a node.
computeClauses(): Computes the two-literal clauses for a node.
computeLB(): Computes a lower bound on the size of a BDD.
computeSavings(): Counts the nodes that would be eliminated if a given node were replaced by zero.
copyOrder(): Copies the current variable order to array.
createResult(): Builds a result for cache storage.
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.
cuddAddGeneralVectorComposeRecur(): Performs the recursive step of Cudd_addGeneralVectorCompose.
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.
cuddAddNonSimComposeRecur(): Performs the recursive step of Cudd_addNonSimCompose.
cuddAddOrAbstractRecur(): Performs the recursive step of Cudd_addOrAbstract.
cuddAddOuterSumRecur(): Performs the recursive step of Cudd_addOuterSum.
cuddAddPermuteRecur(): Implements the recursive step of Cudd_addPermute.
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.
cuddAddVectorComposeRecur(): Performs the recursive step of Cudd_addVectorCompose.
cuddAllocNode(): Fast storage allocation for DdNodes in the table.
cuddAnnealing(): Get new variable-order by simulated annealing algorithm.
cuddApaCountMintermAux(): Performs the recursive step of Cudd_ApaCountMinterm.
cuddApaStCountfree(): Frees the memory used to store the minterm counts recorded in the visited table.
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.
cuddBddCharToVect(): Performs the recursive step of Cudd_bddCharToVect.
cuddBddClipAndAbsRecur(): Approximates the AND of two BDDs and simultaneously abstracts the variables in cube.
cuddBddClippingAndAbstract(): Approximates the conjunction of two BDDs f and g and simultaneously abstracts the variables in cube.
cuddBddClippingAndRecur(): Implements the recursive step of Cudd_bddClippingAnd.
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.
cuddBddConstrainDecomp(): Performs the recursive step of Cudd_bddConstrainDecomp.
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.
cuddBddLICBuildResult(): Builds the result of Cudd_bddLICompaction.
cuddBddLICMarkEdges(): Performs the edge marking step of Cudd_bddLICompaction.
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.
cuddBddPermuteRecur(): Implements the recursive step of Cudd_bddPermute.
cuddBddRestrictRecur(): Performs the recursive step of Cudd_bddRestrict.
cuddBddSqueeze(): Performs the recursive step of Cudd_bddSqueeze.
cuddBddTransferRecur(): Performs the recursive step of Cudd_bddTransfer.
cuddBddTransfer(): Convert a BDD from a manager to another one.
cuddBddVarMapRecur(): Implements the recursive step of Cudd_bddVarMap.
cuddBddVectorComposeRecur(): Performs the recursive step of Cudd_bddVectorCompose.
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.
cuddCheckCollisionOrdering(): Checks whether a collision list is ordered.
cuddCheckCube(): Checks whether g is the BDD of a cube.
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.
cuddConjunctsAux(): Procedure to compute two conjunctive factors of f and place in *c1 and *c2.
cuddConstantLookup(): Looks up in the cache for the result of op applied to f, g, and h.
cuddDestroySubtables(): Destroys the n most recently created subtables in a unique table.
cuddDoRebalance(): Rebalances a red/black tree.
cuddDynamicAllocNode(): Dynamically allocates a Node.
cuddEstimateCofactorSimple(): Performs the recursive step of Cudd_CofactorEstimateSimple.
cuddEstimateCofactor(): Performs the recursive step of Cudd_CofactorEstimate.
cuddExact(): Exact variable ordering algorithm.
cuddFindParent(): Searches the subtables above node for a parent.
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.
cuddHashTableAlloc(): Fast storage allocation for items in a hash table.
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.
cuddHashTableResize(): Resizes a hash table.
cuddHeapProfile(): Prints information about the heap.
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.
cuddIsInDeathRow(): Checks whether a node is in the death row.
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.
cuddLocalCacheAddToList(): Inserts a local cache in the manager list.
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.
cuddLocalCacheRemoveFromList(): Removes a local cache from the manager list.
cuddLocalCacheResize(): Resizes a local cache.
cuddMakeBddFromZddCover(): Converts a ZDD cover to a BDD graph.
cuddMinHammingDistRecur(): Performs the recursive step of Cudd_MinHammingDist.
cuddNextHigh(): Finds the next subtable with a larger index.
cuddNextLow(): Finds the next subtable with a smaller index.
cuddNodeArrayRecur(): Performs the recursive step of cuddNodeArray.
cuddNodeArray(): Recursively collects all the nodes of a DD in an array.
cuddOrderedInsert(): Inserts a DdNode in a red/black search tree.
cuddOrderedThread(): Threads all the nodes of a search tree into a linear list.
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.
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.
cuddRotateLeft(): Performs the left rotation for red/black trees.
cuddRotateRight(): Performs the right rotation for red/black trees.
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.
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.
cuddUniqueLookup(): Checks the unique table for the existence of an internal node.
cuddUpdateInteractionMatrix(): Updates the interaction matrix.
cuddVerifySol(): Implements the recursive step of Cudd_VerifySol.
cuddWindowReorder(): Reorders by applying the method of the sliding window.
cuddXorLinear(): XORs two rows of the linear transform matrix.
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.
cuddZddCountDoubleStep(): Performs the recursive step of Cudd_zddCountDouble.
cuddZddCountStep(): Performs the recursive step of Cudd_zddCount.
cuddZddDagInt(): Performs the recursive step of Cudd_zddDagSize.
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.
cuddZddLinearAux(): Given xLow <= x <= xHigh moves x up and down between the boundaries.
cuddZddLinearBackward(): Given a set of moves, returns the ZDD heap to the position giving the minimum size.
cuddZddLinearDown(): Sifts a variable down and applies the XOR transformation.
cuddZddLinearInPlace(): Linearly combines two adjacent variables.
cuddZddLinearSifting(): Implementation of the linear sifting algorithm for ZDDs.
cuddZddLinearUp(): Sifts a variable up applying the XOR transformation.
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.
cuddZddSiftingAux(): Given xLow <= x <= xHigh moves x up and down between the boundaries.
cuddZddSiftingBackward(): Given a set of moves, returns the ZDD heap to the position giving the minimum size.
cuddZddSiftingDown(): Sifts a variable down.
cuddZddSiftingUp(): Sifts a variable up.
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.
cuddZddSymmSiftingAux(): Given x_low <= x <= x_high moves x up and down between the boundaries.
cuddZddSymmSiftingBackward(): Given a set of moves, returns the ZDD heap to the position giving the minimum size.
cuddZddSymmSiftingConvAux(): Given x_low <= x <= x_high moves x up and down between the boundaries.
cuddZddSymmSiftingConv(): Symmetric sifting to convergence algorithm for ZDDs.
cuddZddSymmSifting_down(): Moves x down until either it reaches the bound (x_high) or the size of the ZDD heap increases too much.
cuddZddSymmSifting_up(): Moves x up until either it reaches the bound (x_low) or the size of the ZDD heap increases too much.
cuddZddSymmSifting(): Symmetric sifting algorithm for ZDDs.
cuddZddSymmSummary(): Counts numbers of symmetric variables and symmetry groups.
cuddZddTreeSifting(): Tree sifting algorithm for ZDDs.
cuddZddUnateProduct(): Performs the recursive step of Cudd_zddUnateProduct.
cuddZddUndoMoves(): Given a set of moves, returns the ZDD heap to the order in effect before the moves.
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.
ddBddToAddRecur(): Performs the recursive step for Cudd_BddToAdd.
ddCheckPermuation(): Checks the BDD variable group tree before a shuffle.
ddClearFlag(): Performs a DFS from f, clearing the LSB of the next pointers.
ddClearGlobal(): Scans the DD and clears the LSB of the next pointers.
ddClearGlobal(): Scans the DD and clears the LSB of the next pointers.
ddClearLocal(): Performs a DFS from f, clearing the LSB of the then pointers.
ddCofMintermAux(): Recursive Step for Cudd_CofMinterm function.
ddCountInternalMtrNodes(): Counts the number of internal nodes of the group tree.
ddCountMintermAux(): Performs the recursive step of Cudd_CountMinterm.
ddCountPathAux(): Performs the recursive step of Cudd_CountPath.
ddCountPathsToNonZero(): Performs the recursive step of Cudd_CountPathsToNonZero.
ddCountRoots(): Counts the number of roots.
ddCreateGroup(): Creates a group encompassing variables from x to y in the DD table.
ddDagInt(): Performs the recursive step of Cudd_DagSize.
ddDissolveGroup(): Dissolves a group in the DD table.
ddDoDumpBlif(): Performs the recursive step of Cudd_DumpBlif.
ddDoDumpDDcal(): Performs the recursive step of Cudd_DumpDDcal.
ddDoDumpDaVinci(): Performs the recursive step of Cudd_DumpDaVinci.
ddDoDumpFactoredForm(): Performs the recursive step of Cudd_DumpFactoredForm.
ddEpdCountMintermAux(): Performs the recursive step of Cudd_EpdCountMinterm.
ddEpdFree(): Frees the memory used to store the minterm counts recorded in the visited table.
ddExchange(): This function is for exchanging two variables, x and y.
ddExtSymmCheck(): Checks for extended symmetry of x and y.
ddFindEssentialRecur(): Implements the recursive step of Cudd_FindEssential.
ddFindNodeHiLo(): Finds the lower and upper bounds of the group represented by treenode.
ddFindTwoLiteralClausesRecur(): Implements the recursive step of Cudd_FindTwoLiteralClauses.
ddFixLimits(): Adjusts the values of table limits.
ddGroupMoveBackward(): Undoes the swap two groups.
ddGroupMove(): Swaps two groups and records the move.
ddGroupSiftingAux(): Sifts one variable up and down until it has taken all positions. Checks for aggregation.
ddGroupSiftingBackward(): Determines the best position for a variables and returns it there.
ddGroupSiftingDown(): Sifts down a variable until it reaches position xHigh.
ddGroupSiftingUp(): Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much.
ddGroupSifting(): Sifts from treenode->low to treenode->high.
ddIsIthAddVarPair(): Comparison of a pair of functions to the i-th ADD variable.
ddIsIthAddVar(): Comparison of a function to the i-th ADD variable.
ddIsVarHandled(): Checks whether a variables is already handled.
ddJumpingAux(): Moves a variable to a specified position.
ddJumpingDown(): This function is for jumping down.
ddJumpingUp(): This function is for jumping up.
ddLCHash(): Computes the hash value for a local cache.
ddLeavesInt(): Performs the recursive step of Cudd_CountLeaves.
ddLinearAndSiftingAux(): Given xLow <= x <= xHigh moves x up and down between the boundaries.
ddLinearAndSiftingBackward(): Given a set of moves, returns the DD heap to the order giving the minimum size.
ddLinearAndSiftingDown(): Sifts a variable down and applies linear transformations.
ddLinearAndSiftingUp(): Sifts a variable up and applies linear transformations.
ddLinearUniqueCompare(): Comparison function used by qsort.
ddMergeGroups(): Merges groups in the DD table.
ddNoCheck(): Pretends to check two variables for aggregation.
ddPatchTree(): Fixes a variable tree after the insertion of new subtables.
ddPermuteWindow3(): Tries all the permutations of the three variables between x and x+2 and retains the best.
ddPermuteWindow4(): Tries all the permutations of the four variables between w and w+3 and retains the best.
ddPickArbitraryMinterms(): Performs the recursive step of Cudd_bddPickArbitraryMinterms.
ddPickRepresentativeCube(): Finds a representative cube of a BDD.
ddPrintMintermAux(): Performs the recursive step of Cudd_PrintMinterm.
ddRehashZdd(): Rehashes a ZDD unique subtable.
ddReorderChildren(): Reorders the children of a group tree node according to the options.
ddReorderPostprocess(): Cleans up at the end of reordering.
ddReorderPreprocess(): Prepares the DD heap for dynamic reordering.
ddReportRefMess(): Reports problem in garbage collection.
ddResetVarHandled(): Resets a variable to be processed.
ddResizeTable(): Increases the number of subtables in a unique table so that it meets or exceeds index.
ddSecDiffCheck(): Checks two variables for aggregation.
ddSetVarHandled(): Sets a variable to already handled.
ddShuffle(): Reorders variables according to a given permutation.
ddShuffle(): Reorders variables according to a given permutation.
ddSiftUp(): Moves one variable up.
ddSiftUp(): Moves one variable up.
ddSiftingAux(): Given xLow <= x <= xHigh moves x up and down between the boundaries.
ddSiftingBackward(): Given a set of moves, returns the DD heap to the position giving the minimum size.
ddSiftingDown(): Sifts a variable down.
ddSiftingUp(): Sifts a variable up.
ddSuppInteract(): Find the support of f.
ddSupportStep(): Performs the recursive step of Cudd_Support.
ddSwapAny(): Swaps any two variables.
ddSymmGroupMoveBackward(): Undoes the swap of two groups.
ddSymmGroupMove(): Swaps two groups.
ddSymmSiftingAux(): Given xLow <= x <= xHigh moves x up and down between the boundaries.
ddSymmSiftingBackward(): Given a set of moves, returns the DD heap to the position giving the minimum size.
ddSymmSiftingConvAux(): Given xLow <= x <= xHigh moves x up and down between the boundaries.
ddSymmSiftingDown(): Moves x down until either it reaches the bound (xHigh) or the size of the DD heap increases too much.
ddSymmSiftingUp(): Moves x up until either it reaches the bound (xLow) or the size of the DD heap increases too much.
ddSymmSummary(): Counts numbers of symmetric variables and symmetry groups.
ddSymmUniqueCompare(): Comparison function used by qsort.
ddTreeSiftingAux(): Visits the group tree and reorders each group.
ddUndoMoves(): Given a set of moves, returns the DD heap to the order in effect before the moves.
ddUniqueCompareGroup(): Comparison function used by qsort.
ddUniqueCompare(): Comparison function used by qsort.
ddUpdateInteract(): Marks as interacting all pairs of variables that appear in support.
ddUpdateMtrTree(): Updates the BDD variable group tree before a shuffle.
ddVarGroupCheck(): Checks for grouping of x and y.
ddWindow2(): Reorders by applying a sliding window of width 2.
ddWindow3(): Reorders by applying a sliding window of width 3.
ddWindow4(): Reorders by applying a sliding window of width 4.
ddWindowConv2(): Reorders by repeatedly applying a sliding window of width 2.
ddWindowConv3(): Reorders by repeatedly applying a sliding window of width 3.
ddWindowConv4(): Reorders by repeatedly applying a sliding window of width 4.
debugCheckParent(): Reports an error if a (dead) node has a non-dead parent.
debugFindParent(): Searches the subtables above node for its parents.
dp2(): Performs the recursive step of cuddP.
emptyClauseSet(): Returns an enpty set of clauses.
equalp(): Returns true iff the two arguments are identical clauses.
find_average_fitness(): Returns the average fitness of the population.
find_best(): Returns the index of the fittest individual.
fixVarTree(): Fixes a variable group tree.
freeMatrix(): Frees a two-dimensional matrix allocated by getMatrix.
freePathPair(): Frees the entries of the visited symbol table.
gatherInfoAux(): Recursively counts minterms and computes reference counts of each node in the BDD.
gatherInfo(): Gathers information about each node.
gcd(): Returns the gcd of two integers.
getCube(): Build a BDD for a largest cube of f.
getLargest(): Finds the size of the largest cube(s) in a DD.
getLevelKeys(): Returns the number of nodes at one level of a unique table.
getMatrix(): Allocates a two-dimensional matrix of ints.
getMaxBinomial(): Returns the maximum value of (n choose k) for a given n.
getPath(): Build a BDD for a shortest path of f.
getShortest(): Finds the length of the shortest path(s) in a DD.
hashDelete(): Removes an item from the hash table of a level queue.
hashInsert(): Inserts an item in the hash table of a level queue.
hashLookup(): Looks up a key in the hash table of a level queue.
hashResize(): Resizes the hash table of a level queue.
impliedp(): Returns true iff either literal of a clause is in a set of literals.
initSymmInfo(): Gathers symmetry information.
largest(): Finds the largest DD in the population.
make_random(): Generates the random sequences for the initial population.
mintermsFromUniverse(): Recursive procedure to extract n mintems from constant 1.
oneliteralp(): Returns true iff the argument is a one-literal clause.
pushDown(): Pushes a variable in the order down to position "level."
rand_int(): Generates a random number between 0 and the integer a.
random_generator(): Random number generator.
restoreOrder(): Restores the variable order in array by a series of sifts up.
roulette(): Selects two parents with the roulette wheel method.
selectMintermsFromUniverse(): This function prepares an array of variables which have not been encountered so far when traversing the procedure cuddSplitSetRecur.
sentinelp(): Returns true iff the argument is the sentinel clause.
separateCube(): Separates cube from distance.
siftBackwardProb(): Returns the DD to the best position encountered during sifting if there was improvement.
sift_up(): Moves one variable up.
stPathTableDdFree(): Procedure to free te result dds stored in the NodeDist pages.
st_zdd_count_dbl_free(): Frees the memory associated with the computed table of Cudd_zddCountDouble.
st_zdd_countfree(): Frees the memory associated with the computed table of Cudd_zddCount.
stopping_criterion(): Checks termination condition.
tlcInfoAlloc(): Allocates a DdTlcInfo Structure.
updateEntry(): Updates entry for a subset.
updateParity(): Recursively update the parity of the paths reaching a node.
updateRefs(): Update function reference counts.
updateUB(): Updates the upper bound and saves the best order seen so far.
zddCountInternalMtrNodes(): Counts the number of internal nodes of the group tree.
zddFindNodeHiLo(): Finds the lower and upper bounds of the group represented by treenode.
zddFixTree(): Fixes the ZDD variable group tree after a shuffle.
zddGroupMoveBackward(): Undoes the swap two groups.
zddGroupMove(): Swaps two groups and records the move.
zddGroupSiftingAux(): Sifts one variable up and down until it has taken all positions. Checks for aggregation.
zddGroupSiftingBackward(): Determines the best position for a variables and returns it there.
zddGroupSiftingDown(): Sifts down a variable until it reaches position xHigh.
zddGroupSiftingUp(): Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much.
zddGroupSifting(): Sifts from treenode->low to treenode->high.
zddMergeGroups(): Merges groups in the DD table.
zddPortFromBddStep(): Performs the recursive step of Cudd_zddPortFromBdd.
zddPortToBddStep(): Performs the recursive step of Cudd_zddPortToBdd.
zddPrintCoverAux(): Performs the recursive step of Cudd_zddPrintCover.
zddReorderChildren(): Reorders the children of a group tree node according to the options.
zddReorderPostprocess(): Shrinks almost empty ZDD subtables at the end of reordering to guarantee that they have a reasonable load factor.
zddReorderPreprocess(): Prepares the ZDD heap for dynamic reordering.
zddShuffle(): Reorders ZDD variables according to a given permutation.
zddSiftUp(): Moves one ZDD variable up.
zddSwapAny(): Swaps any two variables.
zddTreeSiftingAux(): Visits the group tree and reorders each group.
zddUniqueCompareGroup(): Comparison function used by qsort.
zddVarToConst(): Replaces variables with constants if possible (part of canonical form).
zdd_group_move_backward(): Undoes the swap of two groups.
zdd_group_move(): Swaps two groups.
zdd_print_minterm_aux(): Performs the recursive step of Cudd_zddPrintMinterm.
zdd_subset0_aux(): Performs the recursive step of Cudd_zddSubset0.
zdd_subset1_aux(): Performs the recursive step of Cudd_zddSubset1.
zp2(): Performs the recursive step of cuddZddP.
(): Adds node to the head of the free list.
(): Adds node to the head of the free list.
(): Clears the 4 least significant bits of a pointer.
(): Complements a DD if a condition is true.
(): Complements a DD.
(): Computes hash function for keys of three operands.
(): Computes hash function for keys of two operands.
(): Computes the absolute value of a number.
(): Computes the maximum of two numbers.
(): Computes the minimum of two numbers.
(): Decreases the reference count of a node, if it is not saturated.
(): Enforces DD_MINUS_INF_VAL <= x <= DD_PLUS_INF_VAL.
(): Extract the least significant digit of a double digit.
(): Extract the most significant digit of a double digit.
(): Finds the current position of ZDD variable index in the order.
(): Finds the current position of variable index in the order.
(): Hash function for the cache for functions with two operands.
(): Hash function for the cache.
(): Hash function for the table of a level queue.
(): Hash function for the unique table.
(): Increases the reference count of a node, if it is not saturated.
(): Iterates over the cubes of a decision diagram.
(): Iterates over the nodes of a decision diagram.
(): Iterates over the paths of a ZDD.
(): Iterates over the primes of a Boolean function.
(): Outputs a line of stats.
(): Returns 1 if a pointer is complemented.
(): Returns 1 if the absolute value of the difference of the two arguments x and y is less than e.
(): Returns 1 if the node is a constant node.
(): Returns 1 if the node is a constant node.
(): Returns the arithmetic 0 constant node.
(): Returns the complemented version of a pointer.
(): Returns the constant 1 node.
(): Returns the current position in the order of variable index.
(): Returns the else child of an internal node.
(): Returns the else child of an internal node.
(): Returns the minus infinity constant node.
(): Returns the plus infinity constant node.
(): Returns the regular version of a pointer.
(): Returns the then child of an internal node.
(): Returns the then child of an internal node.
(): Returns the value of a constant node.
(): Returns the value of a constant node.
(): Saturating decrement operator.
(): Saturating increment operator.

Last updated on 20090220 23h06