DdApaDigit
Cudd_ApaAdd(
int digits,
DdApaNumber a,
DdApaNumber b,
DdApaNumber sum
)
 Adds two arbitrary precision integers. Returns the carry out of the most significant digit.
 Side Effects The result of the sum is stored in parameter
sum
.
int
Cudd_ApaCompareRatios(
int digitsFirst,
DdApaNumber firstNum,
unsigned int firstDen,
int digitsSecond,
DdApaNumber secondNum,
unsigned int secondDen
)
 Compares the ratios of two arbitrary precision integers to two unsigned ints. Returns 1 if the first number is larger; 0 if they are equal; 1 if the second number is larger.
 Side Effects None
int
Cudd_ApaCompare(
int digitsFirst,
DdApaNumber first,
int digitsSecond,
DdApaNumber second
)
 Compares two arbitrary precision integers. Returns 1 if the first number is larger; 0 if they are equal; 1 if the second number is larger.
 Side Effects None
void
Cudd_ApaCopy(
int digits,
DdApaNumber source,
DdApaNumber dest
)
 Makes a copy of an arbitrary precision integer.
 Side Effects Changes parameter
dest
.
DdApaNumber
Cudd_ApaCountMinterm(
DdManager * manager,
DdNode * node,
int nvars,
int * digits
)
 Counts the number of minterms of a DD. The function is assumed to depend on nvars variables. The minterm count is represented as an arbitrary precision unsigned integer, to allow for any number of variables CUDD supports. Returns a pointer to the array representing the number of minterms of the function rooted at node if successful; NULL otherwise.
 Side Effects The number of digits of the result is returned in parameter
digits
.
 See Also
Cudd_CountMinterm
unsigned int
Cudd_ApaIntDivision(
int digits,
DdApaNumber dividend,
unsigned int divisor,
DdApaNumber quotient
)
 Divides an arbitrary precision integer by a 32bit unsigned integer. Returns the remainder of the division. This procedure relies on the assumption that the number of bits of a DdApaDigit plus the number of bits of an unsigned int is less the number of bits of the mantissa of a double. This guarantees that the product of a DdApaDigit and an unsigned int can be represented without loss of precision by a double. On machines where this assumption is not satisfied, this procedure will malfunction.
 Side Effects The quotient is returned in parameter
quotient
.
 See Also
Cudd_ApaShortDivision
int
Cudd_ApaNumberOfDigits(
int binaryDigits
)
 Finds the number of digits for an arbitrary precision integer given the maximum number of binary digits. The number of binary digits should be positive. Returns the number of digits if successful; 0 otherwise.
 Side Effects None
void
Cudd_ApaPowerOfTwo(
int digits,
DdApaNumber number,
int power
)
 Sets an arbitrary precision integer to a power of two. If the power of two is too large to be represented, the number is set to 0.
 Side Effects The result is returned in parameter
number
.
int
Cudd_ApaPrintDecimal(
FILE * fp,
int digits,
DdApaNumber number
)
 Prints an arbitrary precision integer in decimal format. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
Cudd_ApaPrintHex
Cudd_ApaPrintExponential
int
Cudd_ApaPrintDensity(
FILE * fp,
DdManager * dd,
DdNode * node,
int nvars
)
 Prints the density of a BDD or ADD using arbitrary precision arithmetic. Returns 1 if successful; 0 otherwise.
 Side Effects None
int
Cudd_ApaPrintExponential(
FILE * fp,
int digits,
DdApaNumber number,
int precision
)
 Prints an arbitrary precision integer in exponential format. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
Cudd_ApaPrintHex
Cudd_ApaPrintDecimal
int
Cudd_ApaPrintHex(
FILE * fp,
int digits,
DdApaNumber number
)
 Prints an arbitrary precision integer in hexadecimal format. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
Cudd_ApaPrintDecimal
Cudd_ApaPrintExponential
int
Cudd_ApaPrintMintermExp(
FILE * fp,
DdManager * dd,
DdNode * node,
int nvars,
int precision
)
 Prints the number of minterms of a BDD or ADD in exponential format using arbitrary precision arithmetic. Parameter precision controls the number of signficant digits printed. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
Cudd_ApaPrintMinterm
int
Cudd_ApaPrintMinterm(
FILE * fp,
DdManager * dd,
DdNode * node,
int nvars
)
 Prints the number of minterms of a BDD or ADD using arbitrary precision arithmetic. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
Cudd_ApaPrintMintermExp
void
Cudd_ApaSetToLiteral(
int digits,
DdApaNumber number,
DdApaDigit literal
)
 Sets an arbitrary precision integer to a onedigit literal.
 Side Effects The result is returned in parameter
number
.
void
Cudd_ApaShiftRight(
int digits,
DdApaDigit in,
DdApaNumber a,
DdApaNumber b
)
 Shifts right an arbitrary precision integer by one binary place. The most significant binary digit of the result is taken from parameter
in
.
 Side Effects The result is returned in parameter
b
.
DdApaDigit
Cudd_ApaShortDivision(
int digits,
DdApaNumber dividend,
DdApaDigit divisor,
DdApaNumber quotient
)
 Divides an arbitrary precision integer by a digit.
 Side Effects The quotient is returned in parameter
quotient
.
DdApaDigit
Cudd_ApaSubtract(
int digits,
DdApaNumber a,
DdApaNumber b,
DdApaNumber diff
)
 Subtracts two arbitrary precision integers. Returns the borrow out of the most significant digit.
 Side Effects The result of the subtraction is stored in parameter
diff
.
void
Cudd_AutodynDisableZdd(
DdManager * unique
)
 Disables automatic dynamic reordering of ZDDs.
 Side Effects None
 See Also
Cudd_AutodynEnableZdd
Cudd_ReorderingStatusZdd
Cudd_AutodynDisable
void
Cudd_AutodynDisable(
DdManager * unique
)
 Disables automatic dynamic reordering.
 Side Effects None
 See Also
Cudd_AutodynEnable
Cudd_ReorderingStatus
Cudd_AutodynDisableZdd
void
Cudd_AutodynEnableZdd(
DdManager * unique,
Cudd_ReorderingType method
)
 Enables automatic dynamic reordering of ZDDs. Parameter method is used to determine the method used for reordering ZDDs. If CUDD_REORDER_SAME is passed, the method is unchanged.
 Side Effects None
 See Also
Cudd_AutodynDisableZdd
Cudd_ReorderingStatusZdd
Cudd_AutodynEnable
void
Cudd_AutodynEnable(
DdManager * unique,
Cudd_ReorderingType method
)
 Enables automatic dynamic reordering of BDDs and ADDs. Parameter method is used to determine the method used for reordering. If CUDD_REORDER_SAME is passed, the method is unchanged.
 Side Effects None
 See Also
Cudd_AutodynDisable
Cudd_ReorderingStatus
Cudd_AutodynEnableZdd
double
Cudd_AverageDistance(
DdManager * dd
)
 Computes the average distance between adjacent nodes in the manager. Adjacent nodes are node pairs such that the second node is the then child, else child, or next node in the collision list.
 Side Effects None
DdNode *
Cudd_BddToAdd(
DdManager * dd,
DdNode * B
)
 Converts a BDD to a 01 ADD. Returns a pointer to the resulting ADD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addBddPattern
Cudd_addBddThreshold
Cudd_addBddInterval
Cudd_addBddStrictThreshold
DdNode *
Cudd_CProjection(
DdManager * dd,
DdNode * R,
DdNode * Y
)
 Computes the compatible projection of relation R with respect to cube Y. Returns a pointer to the cprojection if successful; NULL otherwise. For a comparison between Cudd_CProjection and Cudd_PrioritySelect, see the documentation of the latter.
 Side Effects None
 See Also
Cudd_PrioritySelect
int
Cudd_CheckKeys(
DdManager * table
)
 Checks for the following conditions:
 Wrong sizes of subtables.
 Wrong number of keys found in unique subtable.
 Wrong number of dead found in unique subtable.
 Wrong number of keys found in the constant table
 Wrong number of dead found in the constant table
 Wrong number of total slots found
 Wrong number of maximum keys found
 Wrong number of total dead found
Reports the average length of nonempty lists. Returns the number of subtables for which the number of keys is wrong.
 Side Effects None
 See Also
Cudd_DebugCheck
int
Cudd_CheckZeroRef(
DdManager * manager
)
 Checks the unique table for nodes with nonzero reference counts. It is normally called before Cudd_Quit to make sure that there are no memory leaks due to missing Cudd_RecursiveDeref's. Takes into account that reference counts may saturate and that the basic constants and the projection functions are referenced by the manager. Returns the number of nodes with nonzero reference count. (Except for the cases mentioned above.)
 Side Effects None
int
Cudd_ClassifySupport(
DdManager * dd, manager
DdNode * f, first DD
DdNode * g, second DD
DdNode ** common, cube of shared variables
DdNode ** onlyF, cube of variables only in f
DdNode ** onlyG cube of variables only in g
)
 Classifies the variables in the support of two DDs
f
and g
, depending on whther they appear in both DDs, only in f
, or only in g
. Returns 1 successful; 0 otherwise.
 Side Effects The cubes of the three classes of variables are returned as side effects.
 See Also
Cudd_Support
Cudd_VectorSupport
void
Cudd_ClearErrorCode(
DdManager * dd
)
 Clear the error code of a manager.
 Side Effects None
 See Also
Cudd_ReadErrorCode
double *
Cudd_CofMinterm(
DdManager * dd,
DdNode * node
)
 Computes the fraction of minterms in the onset of all the positive cofactors of DD. Returns the pointer to an array of doubles if successful; NULL otherwise. The array hs as many positions as there are BDD variables in the manager plus one. The last position of the array contains the fraction of the minterms in the ONset of the function represented by the BDD or ADD. The other positions of the array hold the variable signatures.
 Side Effects None
DdNode *
Cudd_Cofactor(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Computes the cofactor of f with respect to g; g must be the BDD or the ADD of a cube. Returns a pointer to the cofactor if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddConstrain
Cudd_bddRestrict
Cudd_Complement(
node
)
 Returns the complemented version of a pointer.
 Side Effects none
 See Also
Cudd_Regular
Cudd_IsComplement
int
Cudd_CountLeaves(
DdNode * node
)
 Counts the number of leaves in a DD. Returns the number of leaves in the DD rooted at node if successful; CUDD_OUT_OF_MEM otherwise.
 Side Effects None
 See Also
Cudd_PrintDebug
double
Cudd_CountMinterm(
DdManager * manager,
DdNode * node,
int nvars
)
 Counts the number of minterms of a DD. The function is assumed to depend on nvars variables. The minterm count is represented as a double, to allow for a larger number of variables. Returns the number of minterms of the function rooted at node if successful; (double) CUDD_OUT_OF_MEM otherwise.
 Side Effects None
 See Also
Cudd_PrintDebug
Cudd_CountPath
double
Cudd_CountPath(
DdNode * node
)
 Counts the number of paths of a DD. Paths to all terminal nodes are counted. The path count is represented as a double, to allow for a larger number of variables. Returns the number of paths of the function rooted at node.
 Side Effects None
 See Also
Cudd_CountMinterm
int
Cudd_DagSize(
DdNode * node
)
 Counts the number of nodes in a DD. Returns the number of nodes in the graph rooted at node.
 Side Effects None
 See Also
Cudd_SharingSize
Cudd_PrintDebug
int
Cudd_DeadAreCounted(
DdManager * dd
)
 Tells whether dead nodes are counted towards triggering reordering. Returns 1 if dead nodes are counted; 0 otherwise.
 Side Effects None
 See Also
Cudd_TurnOnCountDead
Cudd_TurnOffCountDead
int
Cudd_DebugCheck(
DdManager * table
)
 Checks for inconsistencies in the DD heap:
 node has illegal index
 live node has dead children
 node has illegal Then or Else pointers
 BDD/ADD node has identical children
 ZDD node has zero then child
 wrong number of total nodes
 wrong number of dead nodes
 ref count error at node
Returns 0 if no inconsistencies are found; DD_OUT_OF_MEM if there is not enough memory; 1 otherwise.
 Side Effects None
 See Also
Cudd_CheckKeys
DdNode *
Cudd_Decreasing(
DdManager * dd,
DdNode * f,
int i
)
 Determines whether the function represented by BDD f is negative unate (monotonic decreasing) in variable i. Returns the constant one is f is unate and the (logical) constant zero if it is not. This function does not generate any new nodes.
 Side Effects None
 See Also
Cudd_Increasing
double
Cudd_Density(
DdManager * dd, manager
DdNode * f, function whose density is sought
int nvars size of the support of f
)
 Computes the density of a BDD or ADD. The density is the ratio of the number of minterms to the number of nodes. If 0 is passed as number of variables, the number of variables existing in the manager is used. Returns the density if successful; (double) CUDD_OUT_OF_MEM otherwise.
 Side Effects None
 See Also
Cudd_CountMinterm
Cudd_DagSize
void
Cudd_Deref(
DdNode * node
)
 Decreases the reference count of node. It is primarily used in recursive procedures to decrease the ref count of a result node before returning it. This accomplishes the goal of removing the protection applied by a previous Cudd_Ref.
 Side Effects None
 See Also
Cudd_RecursiveDeref
Cudd_RecursiveDerefZdd
Cudd_Ref
void
Cudd_DisableGarbageCollection(
DdManager * dd
)
 Disables garbage collection. Garbage collection is initially enabled. This function may be called to disable it. However, garbage collection will still occur when a new node must be created and no memory is left, or when garbage collection is required for correctness. (E.g., before reordering.)
 Side Effects None
 See Also
Cudd_EnableGarbageCollection
Cudd_GarbageCollectionEnabled
int
Cudd_DisableReorderingReporting(
DdManager * dd
)
 Disables reporting of reordering stats. Returns 1 if successful; 0 otherwise.
 Side Effects Removes functions from the prereordering and postreordering hooks.
 See Also
Cudd_EnableReorderingReporting
Cudd_ReorderingReporting
int
Cudd_DumpBlif(
DdManager * dd, manager
int n, number of output nodes to be dumped
DdNode ** f, array of output nodes to be dumped
char ** inames, array of input names (or NULL)
char ** onames, array of output names (or NULL)
char * mname, model name (or NULL)
FILE * fp pointer to the dump file
)
 Writes a blif file representing the argument BDDs as a network of multiplexers. One multiplexer is written for each BDD node. It returns 1 in case of success; 0 otherwise (e.g., outofmemory, file system full, or an ADD with constants different from 0 and 1). Cudd_DumpBlif does not close the file: This is the caller responsibility. Cudd_DumpBlif uses a minimal unique subset of the hexadecimal address of a node as name for it. If the argument inames is nonnull, it is assumed to hold the pointers to the names of the inputs. Similarly for onames.
 Side Effects None
 See Also
Cudd_DumpDot
Cudd_PrintDebug
int
Cudd_DumpDDcal(
DdManager * dd, manager
int n, number of output nodes to be dumped
DdNode ** f, array of output nodes to be dumped
char ** inames, array of input names (or NULL)
char ** onames, array of output names (or NULL)
FILE * fp pointer to the dump file
)
 Writes a DDcal file representing the argument BDDs. It returns 1 in case of success; 0 otherwise (e.g., outofmemory or file system full). Cudd_DumpDDcal does not close the file: This is the caller responsibility. Cudd_DumpDDcal uses a minimal unique subset of the hexadecimal address of a node as name for it. If the argument inames is nonnull, it is assumed to hold the pointers to the names of the inputs. Similarly for onames.
 Side Effects None
 See Also
Cudd_DumpDot
Cudd_PrintDebug
Cudd_DumpBlif
Cudd_DumpDaVinci
int
Cudd_DumpDaVinci(
DdManager * dd, manager
int n, number of output nodes to be dumped
DdNode ** f, array of output nodes to be dumped
char ** inames, array of input names (or NULL)
char ** onames, array of output names (or NULL)
FILE * fp pointer to the dump file
)
 Writes a daVinci file representing the argument BDDs. It returns 1 in case of success; 0 otherwise (e.g., outofmemory or file system full). Cudd_DumpDaVinci does not close the file: This is the caller responsibility. Cudd_DumpDaVinci uses a minimal unique subset of the hexadecimal address of a node as name for it. If the argument inames is nonnull, it is assumed to hold the pointers to the names of the inputs. Similarly for onames.
 Side Effects None
 See Also
Cudd_DumpDot
Cudd_PrintDebug
Cudd_DumpBlif
int
Cudd_DumpDot(
DdManager * dd, manager
int n, number of output nodes to be dumped
DdNode ** f, array of output nodes to be dumped
char ** inames, array of input names (or NULL)
char ** onames, array of output names (or NULL)
FILE * fp pointer to the dump file
)
 Writes a file representing the argument DDs in a format suitable for the graph drawing program dot. It returns 1 in case of success; 0 otherwise (e.g., outofmemory, file system full). Cudd_DumpDot does not close the file: This is the caller responsibility. Cudd_DumpDot uses a minimal unique subset of the hexadecimal address of a node as name for it. If the argument inames is nonnull, it is assumed to hold the pointers to the names of the inputs. Similarly for onames. Cudd_DumpDot uses the following convention to draw arcs:
 solid line: THEN arcs;
 dotted line: complement arcs;
 dashed line: regular ELSE arcs.
The dot options are chosen so that the drawing fits on a lettersize sheet.
 Side Effects None
 See Also
Cudd_DumpBlif
Cudd_PrintDebug
int
Cudd_DumpFactoredForm(
DdManager * dd, manager
int n, number of output nodes to be dumped
DdNode ** f, array of output nodes to be dumped
char ** inames, array of input names (or NULL)
char ** onames, array of output names (or NULL)
FILE * fp pointer to the dump file
)
 Writes factored forms representing the argument BDDs. The format of the factored form is the one used in the genlib files for technology mapping in sis. It returns 1 in case of success; 0 otherwise (e.g., file system full). Cudd_DumpFactoredForm does not close the file: This is the caller responsibility. Caution must be exercised because a factored form may be exponentially larger than the argument BDD. If the argument inames is nonnull, it is assumed to hold the pointers to the names of the inputs. Similarly for onames.
 Side Effects None
 See Also
Cudd_DumpDot
Cudd_PrintDebug
Cudd_DumpBlif
Cudd_DumpDaVinci
Cudd_DumpDDcal
DdNode *
Cudd_Dxygtdxz(
DdManager * dd, DD manager
int N, number of x, y, and z variables
DdNode ** x, array of x variables
DdNode ** y, array of y variables
DdNode ** z array of z variables
)
 This function generates a BDD for the function d(x,y) > d(x,z); x, y, and z are Nbit numbers, x[0] x[1] ... x[N1], y[0] y[1] ... y[N1], and z[0] z[1] ... z[N1], with 0 the most significant bit. The distance d(x,y) is defined as: sum_{i=0}^{N1}(x_i  y_i cdot 2^{Ni1}). The BDD is built bottomup. It has 7*N3 internal nodes, if the variables are ordered as follows: x[0] y[0] z[0] x[1] y[1] z[1] ... x[N1] y[N1] z[N1].
 Side Effects None
 See Also
Cudd_PrioritySelect
Cudd_Dxygtdyz
Cudd_Xgty
Cudd_bddAdjPermuteX
DdNode *
Cudd_Dxygtdyz(
DdManager * dd, DD manager
int N, number of x, y, and z variables
DdNode ** x, array of x variables
DdNode ** y, array of y variables
DdNode ** z array of z variables
)
 This function generates a BDD for the function d(x,y) > d(y,z); x, y, and z are Nbit numbers, x[0] x[1] ... x[N1], y[0] y[1] ... y[N1], and z[0] z[1] ... z[N1], with 0 the most significant bit. The distance d(x,y) is defined as: sum_{i=0}^{N1}(x_i  y_i cdot 2^{Ni1}). The BDD is built bottomup. It has 7*N3 internal nodes, if the variables are ordered as follows: x[0] y[0] z[0] x[1] y[1] z[1] ... x[N1] y[N1] z[N1].
 Side Effects None
 See Also
Cudd_PrioritySelect
Cudd_Dxygtdxz
Cudd_Xgty
Cudd_bddAdjPermuteX
void
Cudd_EnableGarbageCollection(
DdManager * dd
)
 Enables garbage collection. Garbage collection is initially enabled. Therefore it is necessary to call this function only if garbage collection has been explicitly disabled.
 Side Effects None
 See Also
Cudd_DisableGarbageCollection
Cudd_GarbageCollectionEnabled
int
Cudd_EnableReorderingReporting(
DdManager * dd
)
 Enables reporting of reordering stats. Returns 1 if successful; 0 otherwise.
 Side Effects Installs functions in the prereordering and postreordering hooks.
 See Also
Cudd_DisableReorderingReporting
Cudd_ReorderingReporting
int
Cudd_EqualSupNorm(
DdManager * dd, manager
DdNode * f, first ADD
DdNode * g, second ADD
CUDD_VALUE_TYPE tolerance, maximum allowed difference
int pr verbosity level
)
 Compares two ADDs for equality within tolerance. Two ADDs are reported to be equal if the maximum difference between them (the sup norm of their difference) is less than or equal to the tolerance parameter. Returns 1 if the two ADDs are equal (within tolerance); 0 otherwise. If parameter
pr
is positive the first failure is reported to the standard output.
 Side Effects None
int
Cudd_EquivDC(
DdManager * dd,
DdNode * F,
DdNode * G,
DdNode * D
)
 Tells whether F and G are identical wherever D is 0. F and G are either two ADDs or two BDDs. D is either a 01 ADD or a BDD. The function returns 1 if F and G are equivalent, and 0 otherwise. No new nodes are created.
 Side Effects None
int
Cudd_EstimateCofactorSimple(
DdNode * node,
int i
)
 Estimates the number of nodes in a cofactor of a DD. Returns an estimate of the number of nodes in the positive cofactor of the graph rooted at node with respect to the variable whose index is i. This procedure implements with minor changes the algorithm of Cabodi et al. (ICCAD96). It does not allocate any memory, it does not change the state of the manager, and it is fast. However, it has been observed to overestimate the size of the cofactor by as much as a factor of 2.
 Side Effects None
 See Also
Cudd_DagSize
int
Cudd_EstimateCofactor(
DdManager * dd,
DdNode * f,
int i,
int phase 1: positive; 0: negative
)
 Estimates the number of nodes in a cofactor of a DD. Returns an estimate of the number of nodes in a cofactor of the graph rooted at node with respect to the variable whose index is i. In case of failure, returns CUDD_OUT_OF_MEM. This function uses a refinement of the algorithm of Cabodi et al. (ICCAD96). The refinement allows the procedure to account for part of the recombination that may occur in the part of the cofactor above the cofactoring variable. This procedure does no create any new node. It does keep a small table of results; therefore itmay run out of memory. If this is a concern, one should use Cudd_EstimateCofactorSimple, which is faster, does not allocate any memory, but is less accurate.
 Side Effects None
 See Also
Cudd_DagSize
Cudd_EstimateCofactorSimple
DdNode *
Cudd_Eval(
DdManager * dd,
DdNode * f,
int * inputs
)
 Finds the value of a DD for a given variable assignment. The variable assignment is passed in an array of int's, that should specify a zero or a one for each variable in the support of the function. Returns a pointer to a constant node. No new nodes are produced.
 Side Effects None
 See Also
Cudd_bddLeq
Cudd_addEvalConst
Cudd_E(
node
)
 Returns the else child of an internal node. If
node
is a constant node, the result is unpredictable.
 Side Effects none
 See Also
Cudd_T
Cudd_V
DdNode *
Cudd_FindEssential(
DdManager * dd,
DdNode * f
)
 Returns the cube of the essential variables. A positive literal means that the variable must be set to 1 for the function to be 1. A negative literal means that the variable must be set to 0 for the function to be 1. Returns a pointer to the cube BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddIsVarEssential
DdGen *
Cudd_FirstCube(
DdManager * dd,
DdNode * f,
int ** cube,
CUDD_VALUE_TYPE * value
)
 Defines an iterator on the onset of a decision diagram and finds its first cube. Returns a generator that contains the information necessary to continue the enumeration if successful; NULL otherwise.
A cube is represented as an array of literals, which are integers in {0, 1, 2}; 0 represents a complemented literal, 1 represents an uncomplemented literal, and 2 stands for don't care. The enumeration produces a disjoint cover of the function associated with the diagram. The size of the array equals the number of variables in the manager at the time Cudd_FirstCube is called.
For each cube, a value is also returned. This value is always 1 for a BDD, while it may be different from 1 for an ADD. For BDDs, the offset is the set of cubes whose value is the logical zero. For ADDs, the offset is the set of cubes whose value is the background value. The cubes of the offset are not enumerated.
 Side Effects The first cube and its value are returned as side effects.
 See Also
Cudd_ForeachCube
Cudd_NextCube
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_FirstNode
DdGen *
Cudd_FirstNode(
DdManager * dd,
DdNode * f,
DdNode ** node
)
 Defines an iterator on the nodes of a decision diagram and finds its first node. Returns a generator that contains the information necessary to continue the enumeration if successful; NULL otherwise.
 Side Effects The first node is returned as a side effect.
 See Also
Cudd_ForeachNode
Cudd_NextNode
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_FirstCube
Cudd_ForeachCube(
manager,
f,
gen,
cube,
value
)
 Iterates over the cubes of a decision diagram f.
 DdManager *manager;
 DdNode *f;
 DdGen *gen;
 int **cube;
 CUDD_VALUE_TYPE *value;
Cudd_ForeachCube allocates and frees the generator. Therefore the application should not try to do that. Also, the cube is freed at the end of Cudd_ForeachCube and hence is not available outside of the loop. CAUTION: It is assumed that dynamic reordering will not occur while there are open generators. It is the user's responsibility to make sure that dynamic reordering does not occur. As long as new nodes are not created during generation, and dynamic reordering is not called explicitly, dynamic reordering will not occur. Alternatively, it is sufficient to disable dynamic reordering. It is a mistake to dispose of a diagram on which generation is ongoing.
 Side Effects none
 See Also
Cudd_ForeachNode
Cudd_FirstCube
Cudd_NextCube
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_AutodynDisable
Cudd_ForeachNode(
manager,
f,
gen,
node
)
 Iterates over the nodes of a decision diagram f.
 DdManager *manager;
 DdNode *f;
 DdGen *gen;
 DdNode **node;
The nodes are returned in a seemingly random order. Cudd_ForeachCube allocates and frees the generator. Therefore the application should not try to do that. CAUTION: It is assumed that dynamic reordering will not occur while there are open generators. It is the user's responsibility to make sure that dynamic reordering does not occur. As long as new nodes are not created during generation, and dynamic reordering is not called explicitly, dynamic reordering will not occur. Alternatively, it is sufficient to disable dynamic reordering. It is a mistake to dispose of a diagram on which generation is ongoing.
 Side Effects none
 See Also
Cudd_ForeachCube
Cudd_FirstNode
Cudd_NextNode
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_AutodynDisable
void
Cudd_FreeTree(
DdManager * dd
)
 Frees the variable group tree of the manager.
 Side Effects None
 See Also
Cudd_SetTree
Cudd_ReadTree
Cudd_FreeZddTree
void
Cudd_FreeZddTree(
DdManager * dd
)
 Frees the variable group tree of the manager.
 Side Effects None
 See Also
Cudd_SetZddTree
Cudd_ReadZddTree
Cudd_FreeTree
int
Cudd_GarbageCollectionEnabled(
DdManager * dd
)
 Returns 1 if garbage collection is enabled; 0 otherwise.
 Side Effects None
 See Also
Cudd_EnableGarbageCollection
Cudd_DisableGarbageCollection
int
Cudd_GenFree(
DdGen * gen
)
 Frees a CUDD generator. Always returns 0, so that it can be used in mislike foreach constructs.
 Side Effects None
 See Also
Cudd_ForeachCube
Cudd_ForeachNode
Cudd_FirstCube
Cudd_NextCube
Cudd_FirstNode
Cudd_NextNode
Cudd_IsGenEmpty
DdNode *
Cudd_Increasing(
DdManager * dd,
DdNode * f,
int i
)
 Determines whether the function represented by BDD f is positive unate (monotonic decreasing) in variable i. It is based on Cudd_Decreasing and the fact that f is monotonic increasing in i if and only if its complement is monotonic decreasing in i.
 Side Effects None
 See Also
Cudd_Decreasing
DdNode *
Cudd_IndicesToCube(
DdManager * dd,
int * array,
int n
)
 Builds a cube of BDD variables from an array of indices. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddComputeCube
DdManager *
Cudd_Init(
unsigned int numVars, initial number of BDD variables (i.e., subtables)
unsigned int numVarsZ, initial number of ZDD variables (i.e., subtables)
unsigned int numSlots, initial size of the unique tables
unsigned int cacheSize, initial size of the cache
unsigned long maxMemory target maximum memory occupation
)
 Creates a new DD manager, initializes the table, the basic constants and the projection functions. If maxMemory is 0, Cudd_Init decides suitable values for the maximum size of the cache and for the limit for fast unique table growth based on the available memory. Returns a pointer to the manager if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_Quit
Cudd_IsComplement(
node
)
 Returns 1 if a pointer is complemented.
 Side Effects none
 See Also
Cudd_Regular
Cudd_Complement
Cudd_IsConstant(
node
)
 Returns 1 if the node is a constant node (rather than an internal node). All constant nodes have the same index (CUDD_MAXINDEX). The pointer passed to Cudd_IsConstant may be either regular or complemented.
 Side Effects none
int
Cudd_IsGenEmpty(
DdGen * gen
)
 Queries the status of a generator. Returns 1 if the generator is empty or NULL; 0 otherswise.
 Side Effects None
 See Also
Cudd_ForeachCube
Cudd_ForeachNode
Cudd_FirstCube
Cudd_NextCube
Cudd_FirstNode
Cudd_NextNode
Cudd_GenFree
void
Cudd_IterDerefBdd(
DdManager * table,
DdNode * n
)
 Decreases the reference count of node n. If n dies, recursively decreases the reference counts of its children. It is used to dispose of a BDD that is no longer needed. It is more efficient than Cudd_RecursiveDeref, but it cannot be used on ADDs. The greater efficiency comes from being able to assume that no constant node will ever die as a result of a call to this procedure.
 Side Effects None
 See Also
Cudd_RecursiveDeref
DdNode *
Cudd_LargestCube(
DdManager * manager,
DdNode * f,
int * length
)
 Finds a largest cube in a DD. f is the DD we want to get the largest cube for. The problem is translated into the one of finding a shortest path in f, when both THEN and ELSE arcs are assumed to have unit length. This yields a largest cube in the disjoint cover corresponding to the DD. Therefore, it is not necessarily the largest implicant of f. Returns the largest cube as a BDD.
 Side Effects The number of literals of the cube is returned in length.
 See Also
Cudd_ShortestPath
MtrNode *
Cudd_MakeTreeNode(
DdManager * dd, manager
unsigned int low, index of the first group variable
unsigned int size, number of variables in the group
unsigned int type MTR_DEFAULT or MTR_FIXED
)
 Creates a new variable group. The group starts at variable and contains size variables. The parameter low is the index of the first variable. If the variable already exists, its current position in the order is known to the manager. If the variable does not exist yet, the position is assumed to be the same as the index. The group tree is created if it does not exist yet. Returns a pointer to the group if successful; NULL otherwise.
 Side Effects The variable tree is changed.
 See Also
Cudd_MakeZddTreeNode
MtrNode *
Cudd_MakeZddTreeNode(
DdManager * dd, manager
unsigned int low, index of the first group variable
unsigned int size, number of variables in the group
unsigned int type MTR_DEFAULT or MTR_FIXED
)
 Creates a new ZDD variable group. The group starts at variable and contains size variables. The parameter low is the index of the first variable. If the variable already exists, its current position in the order is known to the manager. If the variable does not exist yet, the position is assumed to be the same as the index. The group tree is created if it does not exist yet. Returns a pointer to the group if successful; NULL otherwise.
 Side Effects The ZDD variable tree is changed.
 See Also
Cudd_MakeTreeNode
DdApaNumber
Cudd_NewApaNumber(
int digits
)
 Allocates memory for an arbitrary precision integer. Returns a pointer to the allocated memory if successful; NULL otherwise.
 Side Effects None
int
Cudd_NextCube(
DdGen * gen,
int ** cube,
CUDD_VALUE_TYPE * value
)
 Generates the next cube of a decision diagram onset, using generator gen. Returns 0 if the enumeration is completed; 1 otherwise.
 Side Effects The cube and its value are returned as side effects. The generator is modified.
 See Also
Cudd_ForeachCube
Cudd_FirstCube
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_NextNode
int
Cudd_NextNode(
DdGen * gen,
DdNode ** node
)
 Finds the node of a decision diagram, using generator gen. Returns 0 if the enumeration is completed; 1 otherwise.
 Side Effects The next node is returned as a side effect.
 See Also
Cudd_ForeachNode
Cudd_FirstNode
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_NextCube
unsigned int
Cudd_NodeReadIndex(
DdNode * node
)
 Returns the index of the node. The node pointer can be either regular or complemented.
 Side Effects None
 See Also
Cudd_ReadIndex
Cudd_NotCond(
node,
c
)
 Complements a DD if condition c is true; c should be either 0 or 1, because it is used directly (for efficiency). If in doubt on the values c may take, use "(c) ? Cudd_Not(node) : node".
 Side Effects none
 See Also
Cudd_Not
Cudd_Not(
node
)
 Complements a DD by flipping the complement attribute of the pointer (the least significant bit).
 Side Effects none
 See Also
Cudd_NotCond
void
Cudd_OutOfMem(
long size size of the allocation that failed
)
 Warns that a memory allocation failed. This function can be used as replacement of MMout_of_memory to prevent the safe_mem functions of the util package from exiting when malloc returns NULL. One possible use is in case of discretionary allocations; for instance, the allocation of memory to enlarge the computed table.
 Side Effects None
DdNode *
Cudd_OverApprox(
DdManager * dd, manager
DdNode * f, function to be superset
int numVars, number of variables in the support of f
int threshold, when to stop approximation
int safe, enforce safe approximation
double quality minimum improvement for accepted changes
)
 Extracts a dense superset from a BDD. The procedure is identical to the underapproximation procedure except for the fact that it works on the complement of the given function. Extracting the subset of the complement function is equivalent to extracting the superset of the function. Returns a pointer to the BDD of the superset if successful. NULL if intermediate result causes the procedure to run out of memory. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.
 Side Effects None
 See Also
Cudd_SupersetHeavyBranch
Cudd_SupersetShortPaths
Cudd_ReadSize
unsigned int
Cudd_Prime(
unsigned int p
)
 Returns the next prime >= p.
 Side Effects None
int
Cudd_PrintDebug(
DdManager * dd,
DdNode * f,
int n,
int pr
)
 Prints to the standard output a DD and its statistics. The statistics include the number of nodes, the number of leaves, and the number of minterms. (The number of minterms is the number of assignments to the variables that cause the function to be different from the logical zero (for BDDs) and from the background value (for ADDs.) The statistics are printed if pr > 0. Specifically:
 pr = 0 : prints nothing
 pr = 1 : prints counts of nodes and minterms
 pr = 2 : prints counts + disjoint sum of product
 pr = 3 : prints counts + list of nodes
 pr > 3 : prints counts + disjoint sum of product + list of nodes
Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
Cudd_DagSize
Cudd_CountLeaves
Cudd_CountMinterm
Cudd_PrintMinterm
int
Cudd_PrintInfo(
DdManager * dd,
FILE * fp
)
 Prints out statistics and settings for a CUDD manager. Returns 1 if successful; 0 otherwise.
 Side Effects None
int
Cudd_PrintLinear(
DdManager * table
)
 Prints the linear transform matrix. Returns 1 in case of success; 0 otherwise.
 Side Effects none
int
Cudd_PrintMinterm(
DdManager * manager,
DdNode * node
)
 Prints a disjoint sum of product cover for the function rooted at node. Each product corresponds to a path from node a leaf node different from the logical zero, and different from the background value. Uses the standard output. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
Cudd_PrintDebug
void
Cudd_PrintVersion(
FILE * fp
)
 Prints the package version number.
 Side Effects None
void
Cudd_Quit(
DdManager * unique
)
 Deletes resources associated with a DD manager and resets the global statistical counters. (Otherwise, another manaqger subsequently created would inherit the stats of this one.)
 Side Effects None
 See Also
Cudd_Init
long
Cudd_Random(
)
 Portable number generator based on ran2 from "Numerical Recipes in C." It is a long period (> 2 * 10^18) random number generator of L'Ecuyer with BaysDurham shuffle. Returns a long integer uniformly distributed between 0 and 2147483561 (inclusive of the endpoint values). The ranom generator can be explicitly initialized by calling Cudd_Srandom. If no explicit initialization is performed, then the seed 1 is assumed.
 Side Effects None
 See Also
Cudd_Srandom
int
Cudd_ReadArcviolation(
DdManager * dd
)
 Returns the current value of the arcviolation parameter. This parameter is used in group sifting to decide how many arcs into
y
not coming from x
are tolerable when checking for aggregation due to extended symmetry. The value should be between 0 and 100. A small value causes fewer variables to be aggregated. The default value is 0.
 Side Effects None
 See Also
Cudd_SetArcviolation
DdNode *
Cudd_ReadBackground(
DdManager * dd
)
 Reads the background constant of the manager.
 Side Effects None
double
Cudd_ReadCacheHits(
DdManager * dd
)
 Returns the number of cache hits.
 Side Effects None
 See Also
Cudd_ReadCacheLookUps
double
Cudd_ReadCacheLookUps(
DdManager * dd
)
 Returns the number of cache lookups.
 Side Effects None
 See Also
Cudd_ReadCacheHits
unsigned int
Cudd_ReadCacheSlots(
DdManager * dd
)
 Reads the number of slots in the cache.
 Side Effects None
 See Also
Cudd_ReadCacheUsedSlots
double
Cudd_ReadCacheUsedSlots(
DdManager * dd
)
 Reads the fraction of used slots in the cache. The unused slots are those in which no valid data is stored. Garbage collection, variable reordering, and cache resizing may cause used slots to become unused.
 Side Effects None
 See Also
Cudd_ReadCacheSlots
unsigned int
Cudd_ReadDead(
DdManager * dd
)
 Returns the number of dead nodes in the unique table.
 Side Effects None
 See Also
Cudd_ReadKeys
CUDD_VALUE_TYPE
Cudd_ReadEpsilon(
DdManager * dd
)
 Reads the epsilon parameter of the manager. The epsilon parameter control the comparison between floating point numbers.
 Side Effects None
 See Also
Cudd_SetEpsilon
Cudd_ErrorType
Cudd_ReadErrorCode(
DdManager * dd
)
 Returns the code of the last error. The error codes are defined in cudd.h.
 Side Effects None
 See Also
Cudd_ClearErrorCode
long
Cudd_ReadGarbageCollectionTime(
DdManager * dd
)
 Returns the number of milliseconds spent doing garbage collection since the manager was initialized.
 Side Effects None
 See Also
Cudd_ReadGarbageCollections
int
Cudd_ReadGarbageCollections(
DdManager * dd
)
 Returns the number of times garbage collection has occurred in the manager. The number includes both the calls from reordering procedures and those caused by requests to create new nodes.
 Side Effects None
 See Also
Cudd_ReadGarbageCollectionTime
Cudd_AggregationType
Cudd_ReadGroupcheck(
DdManager * dd
)
 Reads the groupcheck parameter of the manager. The groupcheck parameter determines the aggregation criterion in group sifting.
 Side Effects None
 See Also
Cudd_SetGroupcheck
Cudd_ReadIndex(
dd,
index
)
 Returns the current position in the order of variable index. This macro is obsolete and is kept for compatibility. New applications should use Cudd_ReadPerm instead.
 Side Effects none
 See Also
Cudd_ReadPerm
int
Cudd_ReadInvPermZdd(
DdManager * dd,
int i
)
 Returns the index of the ZDD variable currently in the ith position of the order. If the index is CUDD_MAXINDEX, returns CUDD_MAXINDEX; otherwise, if the index is out of bounds returns 1.
 Side Effects None
 See Also
Cudd_ReadPerm
Cudd_ReadInvPermZdd
int
Cudd_ReadInvPerm(
DdManager * dd,
int i
)
 Returns the index of the variable currently in the ith position of the order. If the index is CUDD_MAXINDEX, returns CUDD_MAXINDEX; otherwise, if the index is out of bounds returns 1.
 Side Effects None
 See Also
Cudd_ReadPerm
Cudd_ReadInvPermZdd
unsigned int
Cudd_ReadKeys(
DdManager * dd
)
 Returns the total number of nodes currently in the unique table, including the dead nodes.
 Side Effects None
 See Also
Cudd_ReadDead
int
Cudd_ReadLinear(
DdManager * table, CUDD manager
int x, row index
int y column index
)
 Reads an entry of the linear transform matrix.
 Side Effects none
DdNode *
Cudd_ReadLogicZero(
DdManager * dd
)
 Returns the zero constant of the manager. The logic zero constant is the complement of the one constant, and is distinct from the arithmetic zero.
 Side Effects None
 See Also
Cudd_ReadOne
Cudd_ReadZero
unsigned int
Cudd_ReadLooseUpTo(
DdManager * dd
)
 Reads the looseUpTo parameter of the manager.
 Side Effects None
 See Also
Cudd_SetLooseUpTo
Cudd_ReadMinHit
Cudd_ReadMinDead
unsigned int
Cudd_ReadMaxCacheHard(
DdManager * dd
)
 Reads the maxCacheHard parameter of the manager.
 Side Effects None
 See Also
Cudd_SetMaxCacheHard
Cudd_ReadMaxCache
unsigned int
Cudd_ReadMaxCache(
DdManager * dd
)
 Reads the maxCache parameter of the manager.
 Side Effects None
 See Also
Cudd_SetMaxCache
Cudd_ReadMaxCache
double
Cudd_ReadMaxGrowth(
DdManager * dd
)
 Reads the maxGrowth parameter of the manager. This parameter determines how much the number of nodes can grow during sifting of a variable. Overall, sifting never increases the size of the decision diagrams. This parameter only refers to intermediate results. A lower value will speed up sifting, possibly at the expense of quality.
 Side Effects None
 See Also
Cudd_SetMaxGrowth
long
Cudd_ReadMemoryInUse(
DdManager * dd
)
 Returns the memory in use by the manager measured in bytes.
 Side Effects None
unsigned int
Cudd_ReadMinDead(
DdManager * dd
)
 Reads the minDead parameter of the manager. The minDead parameter is used by the package to decide whether to collect garbage or resize a subtable of the unique table when the subtable becomes too full. The application can indirectly control the value of minDead by setting the looseUpTo parameter.
 Side Effects None
 See Also
Cudd_ReadDead
Cudd_ReadLooseUpTo
Cudd_SetLooseUpTo
unsigned int
Cudd_ReadMinHit(
DdManager * dd
)
 Reads the hit ratio that causes resizinig of the computed table.
 Side Effects None
 See Also
Cudd_SetMinHit
DdNode *
Cudd_ReadMinusInfinity(
DdManager * dd
)
 Reads the minusinfinity constant from the manager.
 Side Effects None
long
Cudd_ReadNodeCount(
DdManager * dd
)
 Reports the number of nodes in BDDs and ADDs. This number does not include the isolated projection functions and the unused constants. These nodes that are not counted are not part of the DDs manipulated by the application.
 Side Effects None
 See Also
Cudd_ReadPeakNodeCount
Cudd_zddReadNodeCount
double
Cudd_ReadNodesDropped(
DdManager * dd
)
 Returns the number of nodes killed by dereferencing if the keeping of this statistic is enabled; 1 otherwise. This statistic is enabled only if the package is compiled with DD_STATS defined.
 Side Effects None
 See Also
Cudd_ReadNodesFreed
double
Cudd_ReadNodesFreed(
DdManager * dd
)
 Returns the number of nodes returned to the free list if the keeping of this statistic is enabled; 1 otherwise. This statistic is enabled only if the package is compiled with DD_STATS defined.
 Side Effects None
 See Also
Cudd_ReadNodesDropped
int
Cudd_ReadNumberXovers(
DdManager * dd
)
 Reads the current number of crossovers used by the genetic algorithm for variable reordering. A larger number of crossovers will cause the genetic algorithm to take more time, but will generally produce better results. The default value is 0, in which case the package uses three times the number of variables as number of crossovers, with a maximum of 60.
 Side Effects None
 See Also
Cudd_SetNumberXovers
DdNode *
Cudd_ReadOne(
DdManager * dd
)
 Returns the one constant of the manager. The one constant is common to ADDs and BDDs.
 Side Effects None
 See Also
Cudd_ReadZero
Cudd_ReadLogicZero
Cudd_ReadZddOne
long
Cudd_ReadPeakNodeCount(
DdManager * dd
)
 Reports the peak number of nodes. This number includes node on the free list. At the peak, the number of nodes on the free list is guaranteed to be less than DD_MEM_CHUNK.
 Side Effects None
 See Also
Cudd_ReadNodeCount
Cudd_PrintInfo
int
Cudd_ReadPermZdd(
DdManager * dd,
int i
)
 Returns the current position of the ith ZDD variable in the order. If the index is CUDD_MAXINDEX, returns CUDD_MAXINDEX; otherwise, if the index is out of bounds returns 1.
 Side Effects None
 See Also
Cudd_ReadInvPermZdd
Cudd_ReadPerm
int
Cudd_ReadPerm(
DdManager * dd,
int i
)
 Returns the current position of the ith variable in the order. If the index is CUDD_MAXINDEX, returns CUDD_MAXINDEX; otherwise, if the index is out of bounds returns 1.
 Side Effects None
 See Also
Cudd_ReadInvPerm
Cudd_ReadPermZdd
DdNode *
Cudd_ReadPlusInfinity(
DdManager * dd
)
 Reads the plusinfinity constant from the manager.
 Side Effects None
int
Cudd_ReadPopulationSize(
DdManager * dd
)
 Reads the current size of the population used by the genetic algorithm for variable reordering. A larger population size will cause the genetic algorithm to take more time, but will generally produce better results. The default value is 0, in which case the package uses three times the number of variables as population size, with a maximum of 120.
 Side Effects None
 See Also
Cudd_SetPopulationSize
int
Cudd_ReadRecomb(
DdManager * dd
)
 Returns the current value of the recombination parameter used in group sifting. A larger (positive) value makes the aggregation of variables due to the second difference criterion more likely. A smaller (negative) value makes aggregation less likely.
 Side Effects None
 See Also
Cudd_SetRecomb
long
Cudd_ReadReorderingTime(
DdManager * dd
)
 Returns the number of milliseconds spent reordering variables since the manager was initialized. The time spent in collecting garbage before reordering is included.
 Side Effects None
 See Also
Cudd_ReadReorderings
int
Cudd_ReadReorderings(
DdManager * dd
)
 Returns the number of times reordering has occurred in the manager. The number includes both the calls to Cudd_ReduceHeap from the application program and those automatically performed by the package. However, calls that do not even initiate reordering are not counted. A call may not initiate reordering if there are fewer than minsize live nodes in the manager, or if CUDD_REORDER_NONE is specified as reordering method. The calls to Cudd_ShuffleHeap are not counted.
 Side Effects None
 See Also
Cudd_ReduceHeap
Cudd_ReadReorderingTime
int
Cudd_ReadSiftMaxSwap(
DdManager * dd
)
 Reads the siftMaxSwap parameter of the manager. This parameter gives the maximum number of swaps that will be attempted for each invocation of sifting. The real number of swaps may exceed the set limit because the package will always complete the sifting of the variable that causes the limit to be reached.
 Side Effects None
 See Also
Cudd_ReadSiftMaxVar
Cudd_SetSiftMaxSwap
int
Cudd_ReadSiftMaxVar(
DdManager * dd
)
 Reads the siftMaxVar parameter of the manager. This parameter gives the maximum number of variables that will be sifted for each invocation of sifting.
 Side Effects None
 See Also
Cudd_ReadSiftMaxSwap
Cudd_SetSiftMaxVar
int
Cudd_ReadSize(
DdManager * dd
)
 Returns the number of BDD variables in existance.
 Side Effects None
 See Also
Cudd_ReadZddSize
unsigned int
Cudd_ReadSlots(
DdManager * dd
)
 Returns the total number of slots of the unique table. This number ismainly for diagnostic purposes.
 Side Effects None
int
Cudd_ReadSymmviolation(
DdManager * dd
)
 Returns the current value of the symmviolation parameter. This parameter is used in group sifting to decide how many violations to the symmetry conditions
f10 = f01
or f11 = f00
are tolerable when checking for aggregation due to extended symmetry. The value should be between 0 and 100. A small value causes fewer variables to be aggregated. The default value is 0.
 Side Effects None
 See Also
Cudd_SetSymmviolation
MtrNode *
Cudd_ReadTree(
DdManager * dd
)
 Returns the variable group tree of the manager.
 Side Effects None
 See Also
Cudd_SetTree
Cudd_FreeTree
Cudd_ReadZddTree
double
Cudd_ReadUniqueLinks(
DdManager * dd
)
 Returns the number of links followed during lookups in the unique table if the keeping of this statistic is enabled; 1 otherwise. If an item is found in the first position of its collision list, the number of links followed is taken to be 0. If it is in second position, the number of links is 1, and so on. This statistic is enabled only if the package is compiled with DD_UNIQUE_PROFILE defined.
 Side Effects None
 See Also
Cudd_ReadUniqueLookUps
double
Cudd_ReadUniqueLookUps(
DdManager * dd
)
 Returns the number of lookups in the unique table if the keeping of this statistic is enabled; 1 otherwise. This statistic is enabled only if the package is compiled with DD_UNIQUE_PROFILE defined.
 Side Effects None
 See Also
Cudd_ReadUniqueLinks
double
Cudd_ReadUsedSlots(
DdManager * dd
)
 Reads the fraction of used slots in the unique table. The unused slots are those in which no valid data is stored. Garbage collection, variable reordering, and subtable resizing may cause used slots to become unused.
 Side Effects None
 See Also
Cudd_ReadSlots
DdNode *
Cudd_ReadVars(
DdManager * dd,
int i
)
 Returns the ith element of the vars array if it falls within the array bounds; NULL otherwise. If i is the index of an existing variable, this function produces the same result as Cudd_bddIthVar. However, if the ith var does not exist yet, Cudd_bddIthVar will create it, whereas Cudd_ReadVars will not.
 Side Effects None
 See Also
Cudd_bddIthVar
DdNode *
Cudd_ReadZddOne(
DdManager * dd,
int i
)
 Returns the ZDD for the constant 1 function. The representation of the constant 1 function as a ZDD depends on how many variables it (nominally) depends on. The index of the topmost variable in the support is given as argument
i
.
 Side Effects None
 See Also
Cudd_ReadOne
int
Cudd_ReadZddSize(
DdManager * dd
)
 Returns the number of ZDD variables in existance.
 Side Effects None
 See Also
Cudd_ReadSize
MtrNode *
Cudd_ReadZddTree(
DdManager * dd
)
 Returns the variable group tree of the manager.
 Side Effects None
 See Also
Cudd_SetZddTree
Cudd_FreeZddTree
Cudd_ReadTree
DdNode *
Cudd_ReadZero(
DdManager * dd
)
 Returns the zero constant of the manager. The zero constant is the arithmetic zero, rather than the logic zero. The latter is the complement of the one constant.
 Side Effects None
 See Also
Cudd_ReadOne
Cudd_ReadLogicZero
void
Cudd_RecursiveDerefZdd(
DdManager * table,
DdNode * n
)
 Decreases the reference count of ZDD node n. If n dies, recursively decreases the reference counts of its children. It is used to dispose of a ZDD that is no longer needed.
 Side Effects None
 See Also
Cudd_Deref
Cudd_Ref
Cudd_RecursiveDeref
void
Cudd_RecursiveDeref(
DdManager * table,
DdNode * n
)
 Decreases the reference count of node n. If n dies, recursively decreases the reference counts of its children. It is used to dispose of a DD that is no longer needed.
 Side Effects None
 See Also
Cudd_Deref
Cudd_Ref
Cudd_RecursiveDerefZdd
int
Cudd_ReduceHeap(
DdManager * table, DD manager
Cudd_ReorderingType heuristic, method used for reordering
int minsize bound below which no reordering occurs
)
 Main dynamic reordering routine. Calls one of the possible reordering procedures:
 Swapping
 Sifting
 Symmetric Sifting
 Group Sifting
 Window Permutation
 Simulated Annealing
 Genetic Algorithm
 Dynamic Programming (exact)
For sifting, symmetric sifting, group sifting, and window permutation it is possible to request reordering to convergence. The core of all methods is the reordering procedure cuddSwapInPlace() which swaps two adjacent variables and is based on Rudell's paper. Returns 1 in case of success; 0 otherwise. In the case of symmetric sifting (with and without convergence) returns 1 plus the number of symmetric variables, in case of success.
 Side Effects Changes the variable order for all diagrams and clears the cache.
void
Cudd_Ref(
DdNode * n
)
 Increases the reference count of a node, if it is not saturated.
 Side Effects None
 See Also
Cudd_RecursiveDeref
Cudd_Deref
Cudd_Regular(
node
)
 Returns the regular version of a pointer.
 Side Effects none
 See Also
Cudd_Complement
Cudd_IsComplement
DdNode *
Cudd_RemapOverApprox(
DdManager * dd, manager
DdNode * f, function to be superset
int numVars, number of variables in the support of f
int threshold, when to stop approximation
double quality minimum improvement for accepted changes
)
 Extracts a dense superset from a BDD. The procedure is identical to the underapproximation procedure except for the fact that it works on the complement of the given function. Extracting the subset of the complement function is equivalent to extracting the superset of the function. Returns a pointer to the BDD of the superset if successful. NULL if intermediate result causes the procedure to run out of memory. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.
 Side Effects None
 See Also
Cudd_SupersetHeavyBranch
Cudd_SupersetShortPaths
Cudd_ReadSize
DdNode *
Cudd_RemapUnderApprox(
DdManager * dd, manager
DdNode * f, function to be subset
int numVars, number of variables in the support of f
int threshold, when to stop approximation
double quality minimum improvement for accepted changes
)
 Extracts a dense subset from a BDD. This procedure uses a remapping technique and density as the cost function. Returns a pointer to the BDD of the subset if successful. NULL if the procedure runs out of memory. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will cause overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.
 Side Effects None
 See Also
Cudd_SubsetShortPaths
Cudd_SubsetHeavyBranch
Cudd_UnderApprox
Cudd_ReadSize
int
Cudd_ReorderingReporting(
DdManager * dd
)
 Returns 1 if reporting of reordering stats is enabled; 0 otherwise.
 Side Effects none
 See Also
Cudd_EnableReorderingReporting
Cudd_DisableReorderingReporting
int
Cudd_ReorderingStatusZdd(
DdManager * unique,
Cudd_ReorderingType * method
)
 Reports the status of automatic dynamic reordering of ZDDs. Parameter method is set to the ZDD reordering method currently selected. Returns 1 if automatic reordering is enabled; 0 otherwise.
 Side Effects Parameter method is set to the ZDD reordering method currently selected.
 See Also
Cudd_AutodynEnableZdd
Cudd_AutodynDisableZdd
Cudd_ReorderingStatus
int
Cudd_ReorderingStatus(
DdManager * unique,
Cudd_ReorderingType * method
)
 Reports the status of automatic dynamic reordering of BDDs and ADDs. Parameter method is set to the reordering method currently selected. Returns 1 if automatic reordering is enabled; 0 otherwise.
 Side Effects Parameter method is set to the reordering method currently selected.
 See Also
Cudd_AutodynEnable
Cudd_AutodynDisable
Cudd_ReorderingStatusZdd
void
Cudd_SetArcviolation(
DdManager * dd,
int arcviolation
)
 Sets the value of the arcviolation parameter. This parameter is used in group sifting to decide how many arcs into
y
not coming from x
are tolerable when checking for aggregation due to extended symmetry. The value should be between 0 and 100. A small value causes fewer variables to be aggregated. The default value is 0.
 Side Effects None
 See Also
Cudd_ReadArcviolation
void
Cudd_SetBackground(
DdManager * dd,
DdNode * bck
)
 Sets the background constant of the manager. It assumes that the DdNode pointer bck is already referenced.
 Side Effects None
void
Cudd_SetEpsilon(
DdManager * dd,
CUDD_VALUE_TYPE ep
)
 Sets the epsilon parameter of the manager to ep. The epsilon parameter control the comparison between floating point numbers.
 Side Effects None
 See Also
Cudd_ReadEpsilon
void
Cudd_SetGroupcheck(
DdManager * dd,
Cudd_AggregationType gc
)
 Sets the parameter groupcheck of the manager to gc. The groupcheck parameter determines the aggregation criterion in group sifting.
 Side Effects None
 See Also
Cudd_ReadGroupCheck
void
Cudd_SetLooseUpTo(
DdManager * dd,
unsigned int lut
)
 Sets the looseUpTo parameter of the manager. This parameter of the manager controls the threshold beyond which no fast growth of the unique table is allowed. The threshold is given as a number of slots. If the value passed to this function is 0, the function determines a suitable value based on the available memory.
 Side Effects None
 See Also
Cudd_ReadLooseUpTo
Cudd_SetMinHit
void
Cudd_SetMaxCacheHard(
DdManager * dd,
unsigned int mc
)
 Sets the maxCacheHard parameter of the manager. The cache cannot grow larger than maxCacheHard entries. This parameter allows an application to control the tradeoff of memory versus speed. If the value passed to this function is 0, the function determines a suitable maximum cache size based on the available memory.
 Side Effects None
 See Also
Cudd_ReadMaxCacheHard
Cudd_SetMaxCache
void
Cudd_SetMaxCache(
DdManager * dd,
unsigned int mc
)
 Sets the maxCache parameter of the manager. This parameter is normally automatically determined by the package based on the total number of nodes and the parameter maxCacheHard. Applications should normally change maxCacheHard rather than maxCache if they want to explicitly control the tradeoff of memory versus speed.
 Side Effects None
 See Also
Cudd_ReadMaxCache
Cudd_SetMaxCacheHard
void
Cudd_SetMaxGrowth(
DdManager * dd,
double mg
)
 Sets the maxGrowth parameter of the manager. This parameter determines how much the number of nodes can grow during sifting of a variable. Overall, sifting never increases the size of the decision diagrams. This parameter only refers to intermediate results. A lower value will speed up sifting, possibly at the expense of quality.
 Side Effects None
 See Also
Cudd_ReadMaxGrowth
void
Cudd_SetMinHit(
DdManager * dd,
unsigned int hr
)
 Sets the minHit parameter of the manager. This parameter controls the resizing of the computed table. If the hit ratio is larger than the specified value, and the cache is not already too large, then its size is doubled.
 Side Effects None
 See Also
Cudd_ReadMinHit
void
Cudd_SetNumberXovers(
DdManager * dd,
int numberXovers
)
 Sets the number of crossovers used by the genetic algorithm for variable reordering. A larger number of crossovers will cause the genetic algorithm to take more time, but will generally produce better results. The default value is 0, in which case the package uses three times the number of variables as number of crossovers, with a maximum of 60.
 Side Effects None
 See Also
Cudd_ReadNumberXovers
void
Cudd_SetPopulationSize(
DdManager * dd,
int populationSize
)
 Sets the size of the population used by the genetic algorithm for variable reordering. A larger population size will cause the genetic algorithm to take more time, but will generally produce better results. The default value is 0, in which case the package uses three times the number of variables as population size, with a maximum of 120.
 Side Effects Changes the manager.
 See Also
Cudd_ReadPopulationSize
void
Cudd_SetRecomb(
DdManager * dd,
int recomb
)
 Sets the value of the recombination parameter used in group sifting. A larger (positive) value makes the aggregation of variables due to the second difference criterion more likely. A smaller (negative) value makes aggregation less likely. The default value is 0.
 Side Effects Changes the manager.
 See Also
Cudd_ReadRecomb
void
Cudd_SetSiftMaxSwap(
DdManager * dd,
int sms
)
 Sets the siftMaxSwap parameter of the manager. This parameter gives the maximum number of swaps that will be attempted for each invocation of sifting. The real number of swaps may exceed the set limit because the package will always complete the sifting of the variable that causes the limit to be reached.
 Side Effects None
 See Also
Cudd_SetSiftMaxVar
Cudd_ReadSiftMaxSwap
void
Cudd_SetSiftMaxVar(
DdManager * dd,
int smv
)
 Sets the siftMaxVar parameter of the manager. This parameter gives the maximum number of variables that will be sifted for each invocation of sifting.
 Side Effects None
 See Also
Cudd_SetSiftMaxSwap
Cudd_ReadSiftMaxVar
void
Cudd_SetSymmviolation(
DdManager * dd,
int symmviolation
)
 Sets the value of the symmviolation parameter. This parameter is used in group sifting to decide how many violations to the symmetry conditions
f10 = f01
or f11 = f00
are tolerable when checking for aggregation due to extended symmetry. The value should be between 0 and 100. A small value causes fewer variables to be aggregated. The default value is 0.
 Side Effects Changes the manager.
 See Also
Cudd_ReadSymmviolation
void
Cudd_SetTree(
DdManager * dd,
MtrNode * tree
)
 Sets the variable group tree of the manager.
 Side Effects None
 See Also
Cudd_FreeTree
Cudd_ReadTree
Cudd_SetZddTree
void
Cudd_SetZddTree(
DdManager * dd,
MtrNode * tree
)
 Sets the ZDD variable group tree of the manager.
 Side Effects None
 See Also
Cudd_FreeZddTree
Cudd_ReadZddTree
Cudd_SetTree
int
Cudd_SharingSize(
DdNode ** nodeArray,
int n
)
 Counts the number of nodes in an array of DDs. Shared nodes are counted only once. Returns the total number of nodes.
 Side Effects None
 See Also
Cudd_DagSize
int
Cudd_ShortestLength(
DdManager * manager,
DdNode * f,
int * weight
)
 Find the length of the shortest path(s) in a DD. f is the DD we want to get the shortest path for; weight[i] is the weight of the THEN edge coming from the node whose index is i. All ELSE edges have 0 weight. Returns the length of the shortest path(s) if successful; CUDD_OUT_OF_MEM otherwise.
 Side Effects None
 See Also
Cudd_ShortestPath
DdNode *
Cudd_ShortestPath(
DdManager * manager,
DdNode * f,
int * weight,
int * support,
int * length
)
 Finds a shortest path in a DD. f is the DD we want to get the shortest path for; weight[i] is the weight of the THEN arc coming from the node whose index is i. If weight is NULL, then unit weights are assumed for all THEN arcs. All ELSE arcs have 0 weight. If nonNULL, both weight and support should point to arrays with at least as many entries as there are variables in the manager. Returns the shortest path as the BDD of a cube.
 Side Effects support contains on return the true support of f. If support is NULL on entry, then Cudd_ShortestPath does not compute the true support info. length contains the length of the path.
 See Also
Cudd_ShortestLength
Cudd_LargestCube
int
Cudd_ShuffleHeap(
DdManager * table, DD manager
int * permutation required variable permutation
)
 Reorders variables according to given permutation. The ith entry of the permutation array contains the index of the variable that should be brought to the ith level. The size of the array should be equal or greater to the number of variables currently in use. Returns 1 in case of success; 0 otherwise.
 Side Effects Changes the variable order for all diagrams and clears the cache.
 See Also
Cudd_ReduceHeap
DdNode *
Cudd_SolveEqn(
DdManager * bdd,
DdNode * F, the lefthand side of the equation
DdNode * Y, the cube of the y variables
DdNode ** G, the array of solutions (return parameter)
int ** yIndex, index of y variables
int n numbers of unknowns
)
 Implements the solution for F(x,y) = 0. The return value is the consistency condition. The y variables are the unknowns and the remaining variables are the parameters. Returns the consistency condition if successful; NULL otherwise. Cudd_SolveEqn allocates an array and fills it with the indices of the unknowns. This array is used by Cudd_VerifySol.
 Side Effects The solution is returned in G; the indices of the y variables are returned in yIndex.
 See Also
Cudd_VerifySol
DdNode *
Cudd_SplitSet(
DdManager * manager,
DdNode * S,
DdNode ** xVars,
int n,
double m
)
 Returns
m
minterms from a BDD whose support has n
variables at most. The procedure tries to create as few extra nodes as possible. The function represented by S
depends on at most n
of the variables in xVars
. Returns a BDD with m
minterms of the onset of S if successful; NULL otherwise.
 Side Effects None
void
Cudd_Srandom(
long seed
)
 Initializer for the portable number generator based on ran2 in "Numerical Recipes in C." The input is the seed for the generator. If it is negative, its absolute value is taken as seed. If it is 0, then 1 is taken as seed. The initialized sets up the two recurrences used to generate a longperiod stream, and sets up the shuffle table.
 Side Effects None
 See Also
Cudd_Random
int
Cudd_StdPostReordHook(
DdManager * dd,
void * data
)
 Sample hook function to call after reordering. Prints on stdout final size and reordering time. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
Cudd_StdPreReordHook
int
Cudd_StdPreReordHook(
DdManager * dd,
void * data
)
 Sample hook function to call before reordering. Prints on stdout reordering method and initial size. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
Cudd_StdPostReordHook
DdNode *
Cudd_SubsetCompress(
DdManager * dd, manager
DdNode * f, BDD whose subset is sought
int nvars, number of variables in the support of f
int threshold maximum number of nodes in the subset
)
 Finds a dense subset of BDD
f
. Density is the ratio of number of minterms to number of nodes. Uses several techniques in series. It is more expensive than other subsetting procedures, but often produces better results. See Cudd_SubsetShortPaths for a description of the threshold and nvars parameters. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_SubsetRemap
Cudd_SubsetShortPaths
Cudd_SubsetHeavyBranch
Cudd_bddSqueeze
DdNode *
Cudd_SubsetHeavyBranch(
DdManager * dd, manager
DdNode * f, function to be subset
int numVars, number of variables in the support of f
int threshold maximum number of nodes in the subset
)
 Extracts a dense subset from a BDD. This procedure builds a subset by throwing away one of the children of each node, starting from the root, until the result is small enough. The child that is eliminated from the result is the one that contributes the fewer minterms. Returns a pointer to the BDD of the subset if successful. NULL if the procedure runs out of memory. The parameter numVars is the maximum number of variables to be used in minterm calculation and node count calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.
 Side Effects None
 See Also
Cudd_SubsetShortPaths
Cudd_SupersetHeavyBranch
Cudd_ReadSize
DdNode *
Cudd_SubsetShortPaths(
DdManager * dd, manager
DdNode * f, function to be subset
int numVars, number of variables in the support of f
int threshold, maximum number of nodes in the subset
int hardlimit flag: 1 if threshold is a hard limit
)
 Extracts a dense subset from a BDD. This procedure tries to preserve the shortest paths of the input BDD, because they give many minterms and contribute few nodes. This procedure may increase the number of nodes in trying to create the subset or reduce the number of nodes due to recombination as compared to the original BDD. Hence the threshold may not be strictly adhered to. In practice, recombination overshadows the increase in the number of nodes and results in small BDDs as compared to the threshold. The hardlimit specifies whether threshold needs to be strictly adhered to. If it is set to 1, the procedure ensures that result is never larger than the specified limit but may be considerably less than the threshold. Returns a pointer to the BDD for the subset if successful; NULL otherwise. The value for numVars should be as close as possible to the size of the support of f for better efficiency. However, it is safe to pass the value returned by Cudd_ReadSize for numVars. If 0 is passed, then the value returned by Cudd_ReadSize is used.
 Side Effects None
 See Also
Cudd_SupersetShortPaths
Cudd_SubsetHeavyBranch
Cudd_ReadSize
DdNode *
Cudd_SupersetCompress(
DdManager * dd, manager
DdNode * f, BDD whose superset is sought
int nvars, number of variables in the support of f
int threshold maximum number of nodes in the superset
)
 Finds a dense superset of BDD
f
. Density is the ratio of number of minterms to number of nodes. Uses several techniques in series. It is more expensive than other supersetting procedures, but often produces better results. See Cudd_SupersetShortPaths for a description of the threshold and nvars parameters. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_SubsetCompress
Cudd_SupersetRemap
Cudd_SupersetShortPaths
Cudd_SupersetHeavyBranch
Cudd_bddSqueeze
DdNode *
Cudd_SupersetHeavyBranch(
DdManager * dd, manager
DdNode * f, function to be superset
int numVars, number of variables in the support of f
int threshold maximum number of nodes in the superset
)
 Extracts a dense superset from a BDD. The procedure is identical to the subset procedure except for the fact that it receives the complement of the given function. Extracting the subset of the complement function is equivalent to extracting the superset of the function. This procedure builds a superset by throwing away one of the children of each node starting from the root of the complement function, until the result is small enough. The child that is eliminated from the result is the one that contributes the fewer minterms. Returns a pointer to the BDD of the superset if successful. NULL if intermediate result causes the procedure to run out of memory. The parameter numVars is the maximum number of variables to be used in minterm calculation and node count calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.
 Side Effects None
 See Also
Cudd_SubsetHeavyBranch
Cudd_SupersetShortPaths
Cudd_ReadSize
DdNode *
Cudd_SupersetShortPaths(
DdManager * dd, manager
DdNode * f, function to be superset
int numVars, number of variables in the support of f
int threshold, maximum number of nodes in the subset
int hardlimit flag: 1 if threshold is a hard limit
)
 Extracts a dense superset from a BDD. The procedure is identical to the subset procedure except for the fact that it receives the complement of the given function. Extracting the subset of the complement function is equivalent to extracting the superset of the function. This procedure tries to preserve the shortest paths of the complement BDD, because they give many minterms and contribute few nodes. This procedure may increase the number of nodes in trying to create the superset or reduce the number of nodes due to recombination as compared to the original BDD. Hence the threshold may not be strictly adhered to. In practice, recombination overshadows the increase in the number of nodes and results in small BDDs as compared to the threshold. The hardlimit specifies whether threshold needs to be strictly adhered to. If it is set to 1, the procedure ensures that result is never larger than the specified limit but may be considerably less than the threshold. Returns a pointer to the BDD for the superset if successful; NULL otherwise. The value for numVars should be as close as possible to the size of the support of f for better efficiency. However, it is safe to pass the value returned by Cudd_ReadSize for numVar. If 0 is passed, then the value returned by Cudd_ReadSize is used.
 Side Effects None
 See Also
Cudd_SubsetShortPaths
Cudd_SupersetHeavyBranch
Cudd_ReadSize
int
Cudd_SupportSize(
DdManager * dd, manager
DdNode * f DD whose support size is sought
)
 Counts the variables on which a DD depends. Returns the number of the variables if successful; CUDD_OUT_OF_MEM otherwise.
 Side Effects None
 See Also
Cudd_Support
DdNode *
Cudd_Support(
DdManager * dd, manager
DdNode * f DD whose support is sought
)
 Finds the variables on which a DD depends. Returns a BDD consisting of the product of the variables if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_VectorSupport
Cudd_ClassifySupport
void
Cudd_SymmProfile(
DdManager * table,
int lower,
int upper
)
 Prints statistics on symmetric variables.
 Side Effects None
void
Cudd_TurnOffCountDead(
DdManager * dd
)
 Causes the dead nodes not to be counted towards triggering reordering. This causes less frequent reorderings. By default dead nodes are not counted. Therefore there is no need to call this function unless Cudd_TurnOnCountDead has been previously called.
 Side Effects Changes the manager.
 See Also
Cudd_TurnOnCountDead
Cudd_DeadAreCounted
void
Cudd_TurnOnCountDead(
DdManager * dd
)
 Causes the dead nodes to be counted towards triggering reordering. This causes more frequent reorderings. By default dead nodes are not counted.
 Side Effects Changes the manager.
 See Also
Cudd_TurnOffCountDead
Cudd_DeadAreCounted
Cudd_T(
node
)
 Returns the then child of an internal node. If
node
is a constant node, the result is unpredictable.
 Side Effects none
 See Also
Cudd_E
Cudd_V
DdNode *
Cudd_UnderApprox(
DdManager * dd, manager
DdNode * f, function to be subset
int numVars, number of variables in the support of f
int threshold, when to stop approximation
int safe, enforce safe approximation
double quality minimum improvement for accepted changes
)
 Extracts a dense subset from a BDD. This procedure uses a variant of Tom Shiple's underapproximation method. The main difference from the original method is that density is used as cost function. Returns a pointer to the BDD of the subset if successful. NULL if the procedure runs out of memory. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will cause overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.
 Side Effects None
 See Also
Cudd_SubsetShortPaths
Cudd_SubsetHeavyBranch
Cudd_ReadSize
int
Cudd_VectorSupportSize(
DdManager * dd, manager
DdNode ** F, array of DDs whose support is sought
int n size of the array
)
 Counts the variables on which a set of DDs depends. The set must contain either BDDs and ADDs, or ZDDs. Returns the number of the variables if successful; CUDD_OUT_OF_MEM otherwise.
 Side Effects None
 See Also
Cudd_VectorSupport
Cudd_SupportSize
DdNode *
Cudd_VectorSupport(
DdManager * dd, manager
DdNode ** F, array of DDs whose support is sought
int n size of the array
)
 Finds the variables on which a set of DDs depends. The set must contain either BDDs and ADDs, or ZDDs. Returns a BDD consisting of the product of the variables if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_Support
Cudd_ClassifySupport
DdNode *
Cudd_VerifySol(
DdManager * bdd,
DdNode * F, the lefthand side of the equation
DdNode ** G, the array of solutions
int * yIndex, index of y variables
int n numbers of unknowns
)
 Checks the solution of F(x,y) = 0. This procedure substitutes the solution components for the unknowns of F and returns the resulting BDD for F.
 Side Effects Frees the memory pointed by yIndex.
 See Also
Cudd_SolveEqn
Cudd_V(
node
)
 Returns the value of a constant node. If
node
is an internal node, the result is unpredictable.
 Side Effects none
 See Also
Cudd_T
Cudd_E
DdNode *
Cudd_Xeqy(
DdManager * dd, DD manager
int N, number of x and y variables
DdNode ** x, array of x variables
DdNode ** y array of y variables
)
 This function generates a BDD for the function x==y. Both x and y are Nbit numbers, x[0] x[1] ... x[N1] and y[0] y[1] ... y[N1], with 0 the most significant bit. The BDD is built bottomup. It has 3*N1 internal nodes, if the variables are ordered as follows: x[0] y[0] x[1] y[1] ... x[N1] y[N1].
 Side Effects None
 See Also
Cudd_addXeqy
DdNode *
Cudd_Xgty(
DdManager * dd, DD manager
int N, number of x and y variables
DdNode ** z, array of z variables: unused
DdNode ** x, array of x variables
DdNode ** y array of y variables
)
 This function generates a BDD for the function x > y. Both x and y are Nbit numbers, x[0] x[1] ... x[N1] and y[0] y[1] ... y[N1], with 0 the most significant bit. The BDD is built bottomup. It has 3*N1 internal nodes, if the variables are ordered as follows: x[0] y[0] x[1] y[1] ... x[N1] y[N1]. Argument z is not used by Cudd_Xgty: it is included to make it callcompatible to Cudd_Dxygtdxz and Cudd_Dxygtdyz.
 Side Effects None
 See Also
Cudd_PrioritySelect
Cudd_Dxygtdxz
Cudd_Dxygtdyz
DdNode *
Cudd_addAgreement(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
 Returns NULL if not a terminal case; f op g otherwise, where f op g is f if f==g; background if f!=g.
 Side Effects None
 See Also
Cudd_addApply
DdNode *
Cudd_addBddInterval(
DdManager * dd,
DdNode * f,
CUDD_VALUE_TYPE lower,
CUDD_VALUE_TYPE upper
)
 Converts an ADD to a BDD by replacing all discriminants greater than or equal to lower and less than or equal to upper with 1, and all other discriminants with 0. Returns a pointer to the resulting BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addBddThreshold
Cudd_addBddStrictThreshold
Cudd_addBddPattern
Cudd_BddToAdd
DdNode *
Cudd_addBddIthBit(
DdManager * dd,
DdNode * f,
int bit
)
 Converts an ADD to a BDD by replacing all discriminants whose ith bit is equal to 1 with 1, and all other discriminants with 0. The ith bit refers to the integer representation of the leaf value. If the value is has a fractional part, it is ignored. Repeated calls to this procedure allow one to transform an integervalued ADD into an array of BDDs, one for each bit of the leaf values. Returns a pointer to the resulting BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addBddInterval
Cudd_addBddPattern
Cudd_BddToAdd
DdNode *
Cudd_addBddPattern(
DdManager * dd,
DdNode * f
)
 Converts an ADD to a BDD by replacing all discriminants different from 0 with 1. Returns a pointer to the resulting BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_BddToAdd
Cudd_addBddThreshold
Cudd_addBddInterval
Cudd_addBddStrictThreshold
DdNode *
Cudd_addBddStrictThreshold(
DdManager * dd,
DdNode * f,
CUDD_VALUE_TYPE value
)
 Converts an ADD to a BDD by replacing all discriminants STRICTLY greater than value with 1, and all other discriminants with 0. Returns a pointer to the resulting BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addBddInterval
Cudd_addBddPattern
Cudd_BddToAdd
Cudd_addBddThreshold
DdNode *
Cudd_addBddThreshold(
DdManager * dd,
DdNode * f,
CUDD_VALUE_TYPE value
)
 Converts an ADD to a BDD by replacing all discriminants greater than or equal to value with 1, and all other discriminants with 0. Returns a pointer to the resulting BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addBddInterval
Cudd_addBddPattern
Cudd_BddToAdd
Cudd_addBddStrictThreshold
DdNode *
Cudd_addCmpl(
DdManager * dd,
DdNode * f
)
 Computes the complement of an ADD a la C language: The complement of 0 is 1 and the complement of everything else is 0. Returns a pointer to the resulting ADD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addNegate
DdNode *
Cudd_addCompose(
DdManager * dd,
DdNode * f,
DdNode * g,
int v
)
 Substitutes g for x_v in the ADD for f. v is the index of the variable to be substituted. g must be a 01 ADD. Cudd_bddCompose passes the corresponding projection function to the recursive procedure, so that the cache may be used. Returns the composed ADD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddCompose
DdNode *
Cudd_addComputeCube(
DdManager * dd,
DdNode ** vars,
int * phase,
int n
)
 Computes the cube of an array of ADD variables. If nonnull, the phase argument indicates which literal of each variable should appear in the cube. If phase[i] is nonzero, then the positive literal is used. If phase is NULL, the cube is positive unate. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects none
 See Also
Cudd_bddComputeCube
DdNode *
Cudd_addConstrain(
DdManager * dd,
DdNode * f,
DdNode * c
)
 Computes f constrain c (f @ c), for f an ADD and c a 01 ADD. List of special cases:
 F @ 0 = 0
 F @ 1 = F
 0 @ c = 0
 1 @ c = 1
 F @ F = 1
Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddConstrain
DdNode *
Cudd_addConst(
DdManager * dd,
CUDD_VALUE_TYPE c
)
 Retrieves the ADD for constant c if it already exists, or creates a new ADD. Returns a pointer to the ADD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addNewVar
Cudd_addIthVar
DdNode *
Cudd_addDiff(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
 Returns NULL if not a terminal case; f op g otherwise, where f op g is plusinfinity if f=g; min(f,g) if f!=g.
 Side Effects None
 See Also
Cudd_addApply
DdNode *
Cudd_addDivide(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
 Integer and floating point division. Returns NULL if not a terminal case; f / g otherwise.
 Side Effects None
 See Also
Cudd_addApply
DdNode *
Cudd_addEvalConst(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Checks whether ADD g is constant whenever ADD f is 1. f must be a 01 ADD. Returns a pointer to the resulting ADD (which may or may not be constant) or DD_NON_CONSTANT. If f is identically 0, the check is assumed to be successful, and the background value is returned. No new nodes are created.
 Side Effects None
 See Also
Cudd_addIteConstant
Cudd_addLeq
DdNode *
Cudd_addExistAbstract(
DdManager * manager,
DdNode * f,
DdNode * cube
)
 Abstracts all the variables in cube from f by summing over all possible values taken by the variables. Returns the abstracted ADD.
 Side Effects None
 See Also
Cudd_addUnivAbstract
Cudd_bddExistAbstract
Cudd_addOrAbstract
DdNode *
Cudd_addFindMax(
DdManager * dd,
DdNode * f
)
 Returns a pointer to a constant ADD.
 Side Effects None
DdNode *
Cudd_addFindMin(
DdManager * dd,
DdNode * f
)
 Returns a pointer to a constant ADD.
 Side Effects None
DdNode *
Cudd_addHamming(
DdManager * dd,
DdNode ** xVars,
DdNode ** yVars,
int nVars
)
 Computes the Hamming distance ADD. Returns an ADD that gives the Hamming distance between its two arguments if successful; NULL otherwise. The two vectors xVars and yVars identify the variables that form the two arguments.
 Side Effects None
int
Cudd_addHarwell(
FILE * fp, pointer to the input file
DdManager * dd, DD manager
DdNode ** E, characteristic function of the graph
DdNode *** x, array of row variables
DdNode *** y, array of column variables
DdNode *** xn, array of complemented row variables
DdNode *** yn_, array of complemented column variables
int * nx, number or row variables
int * ny, number or column variables
int * m, number of rows
int * n, number of columns
int bx, first index of row variables
int sx, step of row variables
int by, first index of column variables
int sy, step of column variables
int pr verbosity level
)
 Reads in a matrix in the format of the HarwellBoeing benchmark suite. The variables are ordered as follows:
x[0] y[0] x[1] y[1] ...
0 is the most significant bit. On input, nx and ny hold the numbers of row and column variables already in existence. On output, they hold the numbers of row and column variables actually used by the matrix. m and n are set to the numbers of rows and columns of the matrix. Their values on input are immaterial. Returns 1 on success; 0 otherwise. The ADD for the sparse matrix is returned in E, and its reference count is > 0.
 Side Effects None
 See Also
Cudd_addRead
Cudd_bddRead
DdNode *
Cudd_addIteConstant(
DdManager * dd,
DdNode * f,
DdNode * g,
DdNode * h
)
 Implements ITEconstant for ADDs. f must be a 01 ADD. Returns a pointer to the resulting ADD (which may or may not be constant) or DD_NON_CONSTANT. No new nodes are created. This function can be used, for instance, to check that g has a constant value (specified by h) whenever f is 1. If the constant value is unknown, then one should use Cudd_addEvalConst.
 Side Effects None
 See Also
Cudd_addIte
Cudd_addEvalConst
Cudd_bddIteConstant
DdNode *
Cudd_addIte(
DdManager * dd,
DdNode * f,
DdNode * g,
DdNode * h
)
 Implements ITE(f,g,h). This procedure assumes that f is a 01 ADD. Returns a pointer to the resulting ADD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddIte
Cudd_addIteConstant
Cudd_addApply
DdNode *
Cudd_addIthBit(
DdManager * dd,
DdNode * f,
int bit
)
 Produces an ADD from another ADD by replacing all discriminants whose ith bit is equal to 1 with 1, and all other discriminants with 0. The ith bit refers to the integer representation of the leaf value. If the value is has a fractional part, it is ignored. Repeated calls to this procedure allow one to transform an integervalued ADD into an array of ADDs, one for each bit of the leaf values. Returns a pointer to the resulting ADD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addBddIthBit
DdNode *
Cudd_addIthVar(
DdManager * dd,
int i
)
 Retrieves the ADD variable with index i if it already exists, or creates a new ADD variable. Returns a pointer to the variable if successful; NULL otherwise. An ADD variable differs from a BDD variable because it points to the arithmetic zero, instead of having a complement pointer to 1.
 Side Effects None
 See Also
Cudd_addNewVar
Cudd_bddIthVar
Cudd_addConst
Cudd_addNewVarAtLevel
int
Cudd_addLeq(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Returns 1 if f is less than or equal to g; 0 otherwise. No new nodes are created. This procedure works for arbitrary ADDs. For 01 ADDs Cudd_addEvalConst is more efficient.
 Side Effects None
 See Also
Cudd_addIteConstant
Cudd_addEvalConst
Cudd_bddLeq
DdNode *
Cudd_addMatrixMultiply(
DdManager * dd,
DdNode * A,
DdNode * B,
DdNode ** z,
int nz
)
 Calculates the product of two matrices, A and B, represented as ADDs. This procedure implements the quasiring multiplication algorithm. A is assumed to depend on varibles x (rows) and z (columns). B is assumed to depend on varibles z (rows) and y (columns). The product of A and B then depends on x (rows) and y (columns). Only the z variables have to be explicitly identified; they are the "summation" variables. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addTimesPlus
Cudd_addTriangle
Cudd_bddAndAbstract
DdNode *
Cudd_addMaximum(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
 Integer and floating point max for Cudd_addApply. Returns NULL if not a terminal case; max(f,g) otherwise.
 Side Effects None
 See Also
Cudd_addApply
DdNode *
Cudd_addMinimum(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
 Integer and floating point min for Cudd_addApply. Returns NULL if not a terminal case; min(f,g) otherwise.
 Side Effects None
 See Also
Cudd_addApply
DdNode *
Cudd_addMinus(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
 Integer and floating point subtraction. Returns NULL if not a terminal case; f  g otherwise.
 Side Effects None
 See Also
Cudd_addApply
DdNode *
Cudd_addNand(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
 NAND of two 01 ADDs. Returns NULL if not a terminal case; f NAND g otherwise.
 Side Effects None
 See Also
Cudd_addApply
DdNode *
Cudd_addNegate(
DdManager * dd,
DdNode * f
)
 Computes the additive inverse of an ADD. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addCmpl
DdNode *
Cudd_addNewVarAtLevel(
DdManager * dd,
int level
)
 Creates a new ADD variable. The new variable has an index equal to the largest previous index plus 1 and is positioned at the specified level in the order. Returns a pointer to the new variable if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addNewVar
Cudd_addIthVar
Cudd_bddNewVarAtLevel
DdNode *
Cudd_addNewVar(
DdManager * dd
)
 Creates a new ADD variable. The new variable has an index equal to the largest previous index plus 1. Returns a pointer to the new variable if successful; NULL otherwise. An ADD variable differs from a BDD variable because it points to the arithmetic zero, instead of having a complement pointer to 1.
 Side Effects None
 See Also
Cudd_bddNewVar
Cudd_addIthVar
Cudd_addConst
Cudd_addNewVarAtLevel
DdNode *
Cudd_addNonSimCompose(
DdManager * dd,
DdNode * f,
DdNode ** vector
)
 Given a vector of 01 ADDs, creates a new ADD by substituting the 01 ADDs for the variables of the ADD f. There should be an entry in vector for each variable in the manager. This function implements nonsimultaneous composition. If any of the functions being composed depends on any of the variables being substituted, then the result depends on the order of composition, which in turn depends on the variable order: The variables farther from the roots in the order are substituted first. Returns a pointer to the resulting ADD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addVectorCompose
Cudd_addPermute
Cudd_addCompose
DdNode *
Cudd_addNor(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
 NOR of two 01 ADDs. Returns NULL if not a terminal case; f NOR g otherwise.
 Side Effects None
 See Also
Cudd_addApply
DdNode *
Cudd_addOneZeroMaximum(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
 Returns 1 if f > g (both should be terminal cases) and 0 otherwise. Used in conjunction with Cudd_addApply. Returns NULL if not a terminal case.
 Side Effects None
 See Also
Cudd_addApply
DdNode *
Cudd_addOrAbstract(
DdManager * manager,
DdNode * f,
DdNode * cube
)
 Abstracts all the variables in cube from the 01 ADD f by taking the disjunction over all possible values taken by the variables. Returns the abstracted ADD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addUnivAbstract
Cudd_addExistAbstract
DdNode *
Cudd_addOr(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
 Disjunction of two 01 ADDs. Returns NULL if not a terminal case; f OR g otherwise.
 Side Effects None
 See Also
Cudd_addApply
DdNode *
Cudd_addPermute(
DdManager * manager,
DdNode * node,
int * permut
)
 Given a permutation in array permut, creates a new ADD with permuted variables. There should be an entry in array permut for each variable in the manager. The ith entry of permut holds the index of the variable that is to substitute the ith variable. Returns a pointer to the resulting ADD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddPermute
Cudd_addSwapVariables
DdNode *
Cudd_addPlus(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
 Integer and floating point addition. Returns NULL if not a terminal case; f+g otherwise.
 Side Effects None
 See Also
Cudd_addApply
int
Cudd_addRead(
FILE * fp, input file pointer
DdManager * dd, DD manager
DdNode ** E, characteristic function of the graph
DdNode *** x, array of row variables
DdNode *** y, array of column variables
DdNode *** xn, array of complemented row variables
DdNode *** yn_, array of complemented column variables
int * nx, number or row variables
int * ny, number or column variables
int * m, number of rows
int * n, number of columns
int bx, first index of row variables
int sx, step of row variables
int by, first index of column variables
int sy step of column variables
)
 Reads in a sparse matrix specified in a simple format. The first line of the input contains the numbers of rows and columns. The remaining lines contain the elements of the matrix, one per line. Given a background value (specified by the background field of the manager), only the values different from it are explicitly listed. Each foreground element is described by two integers, i.e., the row and column number, and a real number, i.e., the value.
Cudd_addRead produces an ADD that depends on two sets of variables: x and y. The x variables (x[0] ... x[nx1]) encode the row index and the y variables (y[0] ... y[ny1]) encode the column index. x[0] and y[0] are the most significant bits in the indices. The variables may already exist or may be created by the function. The index of x[i] is bx+i*sx, and the index of y[i] is by+i*sy.
On input, nx and ny hold the numbers of row and column variables already in existence. On output, they hold the numbers of row and column variables actually used by the matrix. When Cudd_addRead creates the variable arrays, the index of x[i] is bx+i*sx, and the index of y[i] is by+i*sy. When some variables already exist Cudd_addRead expects the indices of the existing x variables to be bx+i*sx, and the indices of the existing y variables to be by+i*sy.
m and n are set to the numbers of rows and columns of the matrix. Their values on input are immaterial. The ADD for the sparse matrix is returned in E, and its reference count is > 0. Cudd_addRead returns 1 in case of success; 0 otherwise.
 Side Effects nx and ny are set to the numbers of row and column variables. m and n are set to the numbers of rows and columns. x and y are possibly extended to represent the array of row and column variables. Similarly for xn and yn_, which hold on return from Cudd_addRead the complements of the row and column variables.
 See Also
Cudd_addHarwell
Cudd_bddRead
DdNode *
Cudd_addResidue(
DdManager * dd, manager
int n, number of bits
int m, modulus
int options, options
int top index of top variable
)
 Builds an ADD for the residue modulo m of an nbit number. The modulus must be at least 2, and the number of bits at least 1. Parameter options specifies whether the MSB should be on top or the LSB; and whther the number whose residue is computed is in two's complement notation or not. The macro CUDD_RESIDUE_DEFAULT specifies LSB on top and unsigned number. The macro CUDD_RESIDUE_MSB specifies MSB on top, and the macro CUDD_RESIDUE_TC specifies two's complement residue. To request MSB on top and two's complement residue simultaneously, one can OR the two macros: CUDD_RESIDUE_MSB  CUDD_RESIDUE_TC. Cudd_addResidue returns a pointer to the resulting ADD if successful; NULL otherwise.
 Side Effects None
DdNode *
Cudd_addRestrict(
DdManager * dd,
DdNode * f,
DdNode * c
)
 ADD restrict according to Coudert and Madre's algorithm (ICCAD90). Returns the restricted ADD if successful; otherwise NULL. If application of restrict results in an ADD larger than the input ADD, the input ADD is returned.
 Side Effects None
 See Also
Cudd_addConstrain
Cudd_bddRestrict
DdNode *
Cudd_addRoundOff(
DdManager * dd,
DdNode * f,
int N
)
 Rounds off the discriminants of an ADD. The discriminants are rounded off to N digits after the decimal. Returns a pointer to the result ADD if successful; NULL otherwise.
 Side Effects None
DdNode *
Cudd_addScalarInverse(
DdManager * dd,
DdNode * f,
DdNode * epsilon
)
 Computes an n ADD where the discriminants are the multiplicative inverses of the corresponding discriminants of the argument ADD. Returns a pointer to the resulting ADD in case of success. Returns NULL if any discriminants smaller than epsilon is encountered.
 Side Effects None
DdNode *
Cudd_addSetNZ(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
 This operator sets f to the value of g wherever g != 0. Returns NULL if not a terminal case; f op g otherwise.
 Side Effects None
 See Also
Cudd_addApply
DdNode *
Cudd_addSwapVariables(
DdManager * dd,
DdNode * f,
DdNode ** x,
DdNode ** y,
int n
)
 Swaps two sets of variables of the same size (x and y) in the ADD f. The size is given by n. The two sets of variables are assumed to be disjoint. Returns a pointer to the resulting ADD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addPermute
Cudd_bddSwapVariables
DdNode *
Cudd_addThreshold(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
 Threshold operator for Apply (f if f >=g; 0 if f<g). Returns NULL if not a terminal case; f op g otherwise.
 Side Effects None
 See Also
Cudd_addApply
DdNode *
Cudd_addTimesPlus(
DdManager * dd,
DdNode * A,
DdNode * B,
DdNode ** z,
int nz
)
 Calculates the product of two matrices, A and B, represented as ADDs, using the CMU matrix by matrix multiplication procedure by Clarke et al.. Matrix A has x's as row variables and z's as column variables, while matrix B has z's as row variables and y's as column variables. Returns the pointer to the result if successful; NULL otherwise. The resulting matrix has x's as row variables and y's as column variables.
 Side Effects None
 See Also
Cudd_addMatrixMultiply
DdNode *
Cudd_addTimes(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
 Integer and floating point multiplication. Returns NULL if not a terminal case; f * g otherwise.
 Side Effects None
 See Also
Cudd_addApply
DdNode *
Cudd_addTriangle(
DdManager * dd,
DdNode * f,
DdNode * g,
DdNode ** z,
int nz
)
 Implements the semiring multiplication algorithm used in the triangulation step for the shortest path computation. f is assumed to depend on varibles x (rows) and z (columns). g is assumed to depend on varibles z (rows) and y (columns). The product of f and g then depends on x (rows) and y (columns). Only the z variables have to be explicitly identified; they are the "abstraction" variables. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addMatrixMultiply
Cudd_bddAndAbstract
DdNode *
Cudd_addUnivAbstract(
DdManager * manager,
DdNode * f,
DdNode * cube
)
 Abstracts all the variables in cube from f by taking the product over all possible values taken by the variable. Returns the abstracted ADD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addExistAbstract
Cudd_bddUnivAbstract
Cudd_addOrAbstract
DdNode *
Cudd_addVectorCompose(
DdManager * dd,
DdNode * f,
DdNode ** vector
)
 Given a vector of 01 ADDs, creates a new ADD by substituting the 01 ADDs for the variables of the ADD f. There should be an entry in vector for each variable in the manager. If no substitution is sought for a given variable, the corresponding projection function should be specified in the vector. This function implements simultaneous composition. Returns a pointer to the resulting ADD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addNonSimCompose
Cudd_addPermute
Cudd_addCompose
Cudd_bddVectorCompose
DdNode *
Cudd_addWalsh(
DdManager * dd,
DdNode ** x,
DdNode ** y,
int n
)
 Generates a Walsh matrix in ADD form. Returns a pointer to the matrixi if successful; NULL otherwise.
 Side Effects None
DdNode *
Cudd_addXeqy(
DdManager * dd, DD manager
int N, number of x and y variables
DdNode ** x, array of x variables
DdNode ** y array of y variables
)
 This function generates an ADD for the function x==y. Both x and y are Nbit numbers, x[0] x[1] ... x[N1] and y[0] y[1] ... y[N1], with 0 the most significant bit. The ADD is built bottomup. It has 3*N1 internal nodes, if the variables are ordered as follows: x[0] y[0] x[1] y[1] ... x[N1] y[N1].
 Side Effects None
 See Also
Cudd_Xeqy
DdNode *
Cudd_addXnor(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
 XNOR of two 01 ADDs. Returns NULL if not a terminal case; f XNOR g otherwise.
 Side Effects None
 See Also
Cudd_addApply
DdNode *
Cudd_addXor(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
 XOR of two 01 ADDs. Returns NULL if not a terminal case; f XOR g otherwise.
 Side Effects None
 See Also
Cudd_addApply
DdNode *
Cudd_bddAdjPermuteX(
DdManager * dd,
DdNode * B,
DdNode ** x,
int n
)
 Rearranges a set of variables in the BDD B. The size of the set is given by n. This procedure is intended for the `randomization' of the priority functions. Returns a pointer to the BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddPermute
Cudd_bddSwapVariables
Cudd_Dxygtdxz
Cudd_Dxygtdyz
Cudd_PrioritySelect
DdNode *
Cudd_bddAndAbstract(
DdManager * manager,
DdNode * f,
DdNode * g,
DdNode * cube
)
 Takes the AND of two BDDs and simultaneously abstracts the variables in cube. The variables are existentially abstracted. Returns a pointer to the result is successful; NULL otherwise. Cudd_bddAndAbstract implements the semiring matrix multiplication algorithm for the boolean semiring.
 Side Effects None
 See Also
Cudd_addMatrixMultiply
Cudd_addTriangle
Cudd_bddAnd
DdNode *
Cudd_bddAnd(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Computes the conjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.
 Side Effects None
 See Also
Cudd_bddIte
Cudd_addApply
Cudd_bddAndAbstract
Cudd_bddIntersect
Cudd_bddOr
Cudd_bddNand
Cudd_bddNor
Cudd_bddXor
Cudd_bddXnor
int
Cudd_bddApproxConjDecomp(
DdManager * dd, manager
DdNode * f, function to be decomposed
DdNode *** conjuncts address of the first factor
)
 Performs twoway conjunctive decomposition of a BDD. This procedure owes its name to the use of supersetting to obtain an initial factor of the given function. Returns the number of conjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise. The conjuncts produced by this procedure tend to be imbalanced.
 Side Effects The factors are returned in an array as side effects. The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the conjuncts are already referenced. If the function returns 0, the array for the conjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.
 See Also
Cudd_bddApproxDisjDecomp
Cudd_bddIterConjDecomp
Cudd_bddGenConjDecomp
Cudd_bddVarConjDecomp
Cudd_RemapOverApprox
Cudd_bddSqueeze
Cudd_bddLICompaction
int
Cudd_bddApproxDisjDecomp(
DdManager * dd, manager
DdNode * f, function to be decomposed
DdNode *** disjuncts address of the array of the disjuncts
)
 Performs twoway disjunctive decomposition of a BDD. Returns the number of disjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise. The disjuncts produced by this procedure tend to be imbalanced.
 Side Effects The two disjuncts are returned in an array as side effects. The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the disjuncts are already referenced. If the function returns 0, the array for the disjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.
 See Also
Cudd_bddApproxConjDecomp
Cudd_bddIterDisjDecomp
Cudd_bddGenDisjDecomp
Cudd_bddVarDisjDecomp
DdNode *
Cudd_bddBooleanDiff(
DdManager * manager,
DdNode * f,
int x
)
 Computes the boolean difference of f with respect to the variable with index x. Returns the BDD of the boolean difference if successful; NULL otherwise.
 Side Effects None
DdNode **
Cudd_bddCharToVect(
DdManager * dd,
DdNode * f
)
 Computes a vector of BDDs whose image equals a nonzero function. The result depends on the variable order. The ith component of the vector depends only on the first i variables in the order. Each BDD in the vector is not larger than the BDD of the given characteristic function. This function is based on the description of chartovect in "Verification of Sequential Machines Using Boolean Functional Vectors" by O. Coudert, C. Berthet and J. C. Madre. Returns a pointer to an array containing the result if successful; NULL otherwise. The size of the array equals the number of variables in the manager. The components of the solution have their reference counts already incremented (unlike the results of most other functions in the package.
 Side Effects None
 See Also
Cudd_bddConstrain
DdNode *
Cudd_bddClippingAndAbstract(
DdManager * dd, manager
DdNode * f, first conjunct
DdNode * g, second conjunct
DdNode * cube, cube of variables to be abstracted
int maxDepth, maximum recursion depth
int direction under (0) or over (1) approximation
)
 Approximates the conjunction of two BDDs f and g and simultaneously abstracts the variables in cube. The variables are existentially abstracted. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.
 Side Effects None
 See Also
Cudd_bddAndAbstract
Cudd_bddClippingAnd
DdNode *
Cudd_bddClippingAnd(
DdManager * dd, manager
DdNode * f, first conjunct
DdNode * g, second conjunct
int maxDepth, maximum recursion depth
int direction under (0) or over (1) approximation
)
 Approximates the conjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.
 Side Effects None
 See Also
Cudd_bddAnd
DdNode *
Cudd_bddCompose(
DdManager * dd,
DdNode * f,
DdNode * g,
int v
)
 Substitutes g for x_v in the BDD for f. v is the index of the variable to be substituted. Cudd_bddCompose passes the corresponding projection function to the recursive procedure, so that the cache may be used. Returns the composed BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addCompose
DdNode *
Cudd_bddComputeCube(
DdManager * dd,
DdNode ** vars,
int * phase,
int n
)
 Computes the cube of an array of BDD variables. If nonnull, the phase argument indicates which literal of each variable should appear in the cube. If phase[i] is nonzero, then the positive literal is used. If phase is NULL, the cube is positive unate. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addComputeCube
Cudd_IndicesToCube
DdNode **
Cudd_bddConstrainDecomp(
DdManager * dd,
DdNode * f
)
 BDD conjunctive decomposition as in McMillan's CAV96 paper. The decomposition is canonical only for a given variable order. If canonicity is required, variable ordering must be disabled after the decomposition has been computed. Returns an array with one entry for each BDD variable in the manager if successful; otherwise NULL. The components of the solution have their reference counts already incremented (unlike the results of most other functions in the package.
 Side Effects None
 See Also
Cudd_bddConstrain
Cudd_bddExistAbstract
DdNode *
Cudd_bddConstrain(
DdManager * dd,
DdNode * f,
DdNode * c
)
 Computes f constrain c (f @ c). Uses a canonical form: (f' @ c) = ( f @ c)'. (Note: this is not true for c.) List of special cases:
 F @ 0 = 0
 F @ 1 = F
 0 @ c = 0
 1 @ c = 1
 F @ F = 1
 F @ F'= 0
Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddRestrict
Cudd_addConstrain
double
Cudd_bddCorrelationWeights(
DdManager * manager,
DdNode * f,
DdNode * g,
double * prob
)
 Computes the correlation of f and g for given input probabilities. On input, prob[i] is supposed to contain the probability of the ith input variable to be 1. If f == g, their correlation is 1. If f == g', their correlation is 0. Returns the probability that f and g have the same value. If it runs out of memory, returns (double)CUDD_OUT_OF_MEM. The correlation of f and the constant one gives the probability of f.
 Side Effects None
 See Also
Cudd_bddCorrelation
double
Cudd_bddCorrelation(
DdManager * manager,
DdNode * f,
DdNode * g
)
 Computes the correlation of f and g. If f == g, their correlation is 1. If f == g', their correlation is 0. Returns the fraction of minterms in the ONset of the EXNOR of f and g. If it runs out of memory, returns (double)CUDD_OUT_OF_MEM.
 Side Effects None
 See Also
Cudd_bddCorrelationWeights
DdNode *
Cudd_bddExistAbstract(
DdManager * manager,
DdNode * f,
DdNode * cube
)
 Existentially abstracts all the variables in cube from f. Returns the abstracted BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddUnivAbstract
Cudd_addExistAbstract
int
Cudd_bddGenConjDecomp(
DdManager * dd, manager
DdNode * f, function to be decomposed
DdNode *** conjuncts address of the array of conjuncts
)
 Performs twoway conjunctive decomposition of a BDD. This procedure owes its name to the fact tht it generalizes the decomposition based on the cofactors with respect to one variable. Returns the number of conjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise. The conjuncts produced by this procedure tend to be balanced.
 Side Effects The two factors are returned in an array as side effects. The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the conjuncts are already referenced. If the function returns 0, the array for the conjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.
 See Also
Cudd_bddGenDisjDecomp
Cudd_bddApproxConjDecomp
Cudd_bddIterConjDecomp
Cudd_bddVarConjDecomp
int
Cudd_bddGenDisjDecomp(
DdManager * dd, manager
DdNode * f, function to be decomposed
DdNode *** disjuncts address of the array of the disjuncts
)
 Performs twoway disjunctive decomposition of a BDD. Returns the number of disjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise. The disjuncts produced by this procedure tend to be balanced.
 Side Effects The two disjuncts are returned in an array as side effects. The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the disjuncts are already referenced. If the function returns 0, the array for the disjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.
 See Also
Cudd_bddGenConjDecomp
Cudd_bddApproxDisjDecomp
Cudd_bddIterDisjDecomp
Cudd_bddVarDisjDecomp
DdNode *
Cudd_bddIntersect(
DdManager * dd, manager
DdNode * f, first operand
DdNode * g second operand
)
 Computes a function included in the intersection of f and g. (That is, a witness that the intersection is not empty.) Cudd_bddIntersect tries to build as few new nodes as possible. If the only result of interest is whether f and g intersect, Cudd_bddLeq should be used instead.
 Side Effects None
 See Also
Cudd_bddLeq
Cudd_bddIteConstant
int
Cudd_bddIsVarEssential(
DdManager * manager,
DdNode * f,
int id,
int phase
)
 Determines whether a given variable is essential with a given phase in a BDD. Uses Cudd_bddIteConstant. Returns 1 if phase == 1 and f>x_id, or if phase == 0 and f>x_id'.
 Side Effects None
 See Also
Cudd_FindEssential
DdNode *
Cudd_bddIsop(
DdManager * dd,
DdNode * L,
DdNode * U
)
 Computes a BDD in the interval between L and U with a simple sumofproduuct cover. This procedure is similar to Cudd_zddIsop, but it does not return the ZDD for the cover. Returns a pointer to the BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_zddIsop
DdNode *
Cudd_bddIteConstant(
DdManager * dd,
DdNode * f,
DdNode * g,
DdNode * h
)
 Implements ITEconstant(f,g,h). Returns a pointer to the resulting BDD (which may or may not be constant) or DD_NON_CONSTANT. No new nodes are created.
 Side Effects None
 See Also
Cudd_bddIte
Cudd_bddIntersect
Cudd_bddLeq
Cudd_addIteConstant
int
Cudd_bddIterConjDecomp(
DdManager * dd, manager
DdNode * f, function to be decomposed
DdNode *** conjuncts address of the array of conjuncts
)
 Performs twoway conjunctive decomposition of a BDD. This procedure owes its name to the iterated use of supersetting to obtain a factor of the given function. Returns the number of conjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise. The conjuncts produced by this procedure tend to be imbalanced.
 Side Effects The factors are returned in an array as side effects. The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the conjuncts are already referenced. If the function returns 0, the array for the conjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.
 See Also
Cudd_bddIterDisjDecomp
Cudd_bddApproxConjDecomp
Cudd_bddGenConjDecomp
Cudd_bddVarConjDecomp
Cudd_RemapOverApprox
Cudd_bddSqueeze
Cudd_bddLICompaction
int
Cudd_bddIterDisjDecomp(
DdManager * dd, manager
DdNode * f, function to be decomposed
DdNode *** disjuncts address of the array of the disjuncts
)
 Performs twoway disjunctive decomposition of a BDD. Returns the number of disjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise. The disjuncts produced by this procedure tend to be imbalanced.
 Side Effects The two disjuncts are returned in an array as side effects. The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the disjuncts are already referenced. If the function returns 0, the array for the disjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.
 See Also
Cudd_bddIterConjDecomp
Cudd_bddApproxDisjDecomp
Cudd_bddGenDisjDecomp
Cudd_bddVarDisjDecomp
DdNode *
Cudd_bddIte(
DdManager * dd,
DdNode * f,
DdNode * g,
DdNode * h
)
 Implements ITE(f,g,h). Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.
 Side Effects None
 See Also
Cudd_addIte
Cudd_bddIteConstant
Cudd_bddIntersect
DdNode *
Cudd_bddIthVar(
DdManager * dd,
int i
)
 Retrieves the BDD variable with index i if it already exists, or creates a new BDD variable. Returns a pointer to the variable if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddNewVar
Cudd_addIthVar
Cudd_bddNewVarAtLevel
DdNode *
Cudd_bddLICompaction(
DdManager * dd, manager
DdNode * f, function to be minimized
DdNode * c constraint (care set)
)
 Performs safe minimization of a BDD. Given the BDD
f
of a function to be minimized and a BDD c
representing the care set, Cudd_bddLICompaction produces the BDD of a function that agrees with f
wherever c
is 1. Safe minimization means that the size of the result is guaranteed not to exceed the size of f
. This function is based on the DAC97 paper by Hong et al.. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddRestrict
int
Cudd_bddLeq(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Returns 1 if f is less than or equal to g; 0 otherwise. No new nodes are created.
 Side Effects None
 See Also
Cudd_bddIteConstant
Cudd_addEvalConst
DdNode *
Cudd_bddLiteralSetIntersection(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Computes the intesection of two sets of literals represented as BDDs. Each set is represented as a cube of the literals in the set. The empty set is represented by the constant 1. No variable can be simultaneously present in both phases in a set. Returns a pointer to the BDD representing the intersected sets, if successful; NULL otherwise.
 Side Effects None
DdNode *
Cudd_bddMinimize(
DdManager * dd,
DdNode * f,
DdNode * c
)
 Finds a small BDD that agrees with
f
over c
. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddRestrict
Cudd_bddLICompaction
Cudd_bddSqueeze
DdNode *
Cudd_bddNand(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Computes the NAND of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.
 Side Effects None
 See Also
Cudd_bddIte
Cudd_addApply
Cudd_bddAnd
Cudd_bddOr
Cudd_bddNor
Cudd_bddXor
Cudd_bddXnor
DdNode *
Cudd_bddNewVarAtLevel(
DdManager * dd,
int level
)
 Creates a new BDD variable. The new variable has an index equal to the largest previous index plus 1 and is positioned at the specified level in the order. Returns a pointer to the new variable if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddNewVar
Cudd_bddIthVar
Cudd_addNewVarAtLevel
DdNode *
Cudd_bddNewVar(
DdManager * dd
)
 Creates a new BDD variable. The new variable has an index equal to the largest previous index plus 1. Returns a pointer to the new variable if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addNewVar
Cudd_bddIthVar
Cudd_bddNewVarAtLevel
DdNode *
Cudd_bddNor(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Computes the NOR of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.
 Side Effects None
 See Also
Cudd_bddIte
Cudd_addApply
Cudd_bddAnd
Cudd_bddOr
Cudd_bddNand
Cudd_bddXor
Cudd_bddXnor
DdNode *
Cudd_bddOr(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Computes the disjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.
 Side Effects None
 See Also
Cudd_bddIte
Cudd_addApply
Cudd_bddAnd
Cudd_bddNand
Cudd_bddNor
Cudd_bddXor
Cudd_bddXnor
DdNode *
Cudd_bddPermute(
DdManager * manager,
DdNode * node,
int * permut
)
 Given a permutation in array permut, creates a new BDD with permuted variables. There should be an entry in array permut for each variable in the manager. The ith entry of permut holds the index of the variable that is to substitute the ith variable. Returns a pointer to the resulting BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addPermute
Cudd_bddSwapVariables
DdNode **
Cudd_bddPickArbitraryMinterms(
DdManager * dd, manager
DdNode * f, function from which to pick one minterm
DdNode ** vars, array of variables
int n, size of vars
int k number of minterms to find
)
 Picks k onset minterms evenly distributed from given DD. The minterms are in terms of
vars
. The array vars
should contain at least all variables in the support of f
; if this condition is not met the minterms built by this procedure may not be contained in f
. Builds a BDD for the minterms and returns a pointer to it if successful; NULL otherwise. There are three reasons why the procedure may fail:  It may run out of memory;
 the function
f
may be the constant 0;  the minterms may not be contained in
f
.
 Side Effects None
 See Also
Cudd_bddPickOneMinterm
Cudd_bddPickOneCube
int
Cudd_bddPickOneCube(
DdManager * ddm,
DdNode * node,
char * string
)
 Picks one onset cube randomly from the given DD. The cube is written into an array of characters. The array must have at least as many entries as there are variables. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
Cudd_bddPickOneMinterm
DdNode *
Cudd_bddPickOneMinterm(
DdManager * dd, manager
DdNode * f, function from which to pick one minterm
DdNode ** vars, array of variables
int n size of vars
)
 Picks one onset minterm randomly from the given DD. The minterm is in terms of
vars
. The array vars
should contain at least all variables in the support of f
; if this condition is not met the minterm built by this procedure may not be contained in f
. Builds a BDD for the minterm and returns a pointer to it if successful; NULL otherwise. There are three reasons why the procedure may fail:  It may run out of memory;
 the function
f
may be the constant 0;  the minterm may not be contained in
f
.
 Side Effects None
 See Also
Cudd_bddPickOneCube
int
Cudd_bddRead(
FILE * fp, input file pointer
DdManager * dd, DD manager
DdNode ** E, characteristic function of the graph
DdNode *** x, array of row variables
DdNode *** y, array of column variables
int * nx, number or row variables
int * ny, number or column variables
int * m, number of rows
int * n, number of columns
int bx, first index of row variables
int sx, step of row variables
int by, first index of column variables
int sy step of column variables
)
 Reads in a graph (without labels) given as an adjacency matrix. The first line of the input contains the numbers of rows and columns of the adjacency matrix. The remaining lines contain the arcs of the graph, one per line. Each arc is described by two integers, i.e., the row and column number, or the indices of the two endpoints. Cudd_bddRead produces a BDD that depends on two sets of variables: x and y. The x variables (x[0] ... x[nx1]) encode the row index and the y variables (y[0] ... y[ny1]) encode the column index. x[0] and y[0] are the most significant bits in the indices. The variables may already exist or may be created by the function. The index of x[i] is bx+i*sx, and the index of y[i] is by+i*sy.
On input, nx and ny hold the numbers of row and column variables already in existence. On output, they hold the numbers of row and column variables actually used by the matrix. When Cudd_bddRead creates the variable arrays, the index of x[i] is bx+i*sx, and the index of y[i] is by+i*sy. When some variables already exist, Cudd_bddRead expects the indices of the existing x variables to be bx+i*sx, and the indices of the existing y variables to be by+i*sy.
m and n are set to the numbers of rows and columns of the matrix. Their values on input are immaterial. The BDD for the graph is returned in E, and its reference count is > 0. Cudd_bddRead returns 1 in case of success; 0 otherwise.
 Side Effects nx and ny are set to the numbers of row and column variables. m and n are set to the numbers of rows and columns. x and y are possibly extended to represent the array of row and column variables.
 See Also
Cudd_addHarwell
Cudd_addRead
void
Cudd_bddRealignDisable(
DdManager * unique
)
 Disables realignment of ZDD order to BDD order.
 Side Effects None
 See Also
Cudd_bddRealignEnable
Cudd_bddRealignmentEnabled
Cudd_zddRealignEnable
Cudd_zddRealignmentEnabled
void
Cudd_bddRealignEnable(
DdManager * unique
)
 Enables realignment of the BDD variable order to the ZDD variable order after the ZDDs have been reordered. The number of ZDD variables must be a multiple of the number of BDD variables for realignment to make sense. If this condition is not met, Cudd_zddReduceHeap will return 0. Let
M
be the ratio of the two numbers. For the purpose of realignment, the ZDD variables from M*i
to (M+1)*i1
are reagarded as corresponding to BDD variable i
. Realignment is initially disabled.
 Side Effects None
 See Also
Cudd_zddReduceHeap
Cudd_bddRealignDisable
Cudd_bddRealignmentEnabled
Cudd_zddRealignDisable
Cudd_zddRealignmentEnabled
int
Cudd_bddRealignmentEnabled(
DdManager * unique
)
 Returns 1 if the realignment of BDD order to ZDD order is enabled; 0 otherwise.
 Side Effects None
 See Also
Cudd_bddRealignEnable
Cudd_bddRealignDisable
Cudd_zddRealignEnable
Cudd_zddRealignDisable
DdNode *
Cudd_bddRestrict(
DdManager * dd,
DdNode * f,
DdNode * c
)
 BDD restrict according to Coudert and Madre's algorithm (ICCAD90). Returns the restricted BDD if successful; otherwise NULL. If application of restrict results in a BDD larger than the input BDD, the input BDD is returned.
 Side Effects None
 See Also
Cudd_bddConstrain
Cudd_addRestrict
DdNode *
Cudd_bddSqueeze(
DdManager * dd, manager
DdNode * l, lower bound
DdNode * u upper bound
)
 Finds a small BDD in a function interval. Given BDDs
l
and u
, representing the lower bound and upper bound of a function interval, Cudd_bddSqueeze produces the BDD of a function within the interval with a small BDD. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddRestrict
Cudd_bddLICompaction
DdNode *
Cudd_bddSwapVariables(
DdManager * dd,
DdNode * f,
DdNode ** x,
DdNode ** y,
int n
)
 Swaps two sets of variables of the same size (x and y) in the BDD f. The size is given by n. The two sets of variables are assumed to be disjoint. Returns a pointer to the resulting BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddPermute
Cudd_addSwapVariables
DdNode *
Cudd_bddTransfer(
DdManager * ddSource,
DdManager * ddDestination,
DdNode * f
)
 Convert a BDD from a manager to another one. Returns a pointer to the BDD in the destination manager if successful; NULL otherwise.
 Side Effects None
DdNode *
Cudd_bddUnivAbstract(
DdManager * manager,
DdNode * f,
DdNode * cube
)
 Universally abstracts all the variables in cube from f. Returns the abstracted BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddExistAbstract
Cudd_addUnivAbstract
int
Cudd_bddVarConjDecomp(
DdManager * dd, manager
DdNode * f, function to be decomposed
DdNode *** conjuncts address of the array of conjuncts
)
 Conjunctively decomposes one BDD according to a variable. If
f
is the function of the BDD and x
is the variable, the decomposition is (f+x)(f+x')
. The variable is chosen so as to balance the sizes of the two conjuncts and to keep them small. Returns the number of conjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise.
 Side Effects The two factors are returned in an array as side effects. The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the conjuncts are already referenced. If the function returns 0, the array for the conjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.
 See Also
Cudd_bddVarDisjDecomp
Cudd_bddGenConjDecomp
Cudd_bddApproxConjDecomp
Cudd_bddIterConjDecomp
int
Cudd_bddVarDisjDecomp(
DdManager * dd, manager
DdNode * f, function to be decomposed
DdNode *** disjuncts address of the array of the disjuncts
)
 Performs twoway disjunctive decomposition of a BDD according to a variable. If
f
is the function of the BDD and x
is the variable, the decomposition is f*x + f*x'
. The variable is chosen so as to balance the sizes of the two disjuncts and to keep them small. Returns the number of disjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise.
 Side Effects The two disjuncts are returned in an array as side effects. The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the disjuncts are already referenced. If the function returns 0, the array for the disjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.
 See Also
Cudd_bddVarConjDecomp
Cudd_bddApproxDisjDecomp
Cudd_bddIterDisjDecomp
Cudd_bddGenDisjDecomp
int
Cudd_bddVarIsDependent(
DdManager * dd,
DdNode * f,
DdNode * var variable
)
 Checks whether a variable is dependent on others in a function. Returns 1 if the variable is dependent; 0 otherwise. No new nodes are created.
 Side Effects None
DdNode *
Cudd_bddVectorCompose(
DdManager * dd,
DdNode * f,
DdNode ** vector
)
 Given a vector of BDDs, creates a new BDD by substituting the BDDs for the variables of the BDD f. There should be an entry in vector for each variable in the manager. If no substitution is sought for a given variable, the corresponding projection function should be specified in the vector. This function implements simultaneous composition. Returns a pointer to the resulting BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddPermute
Cudd_bddCompose
Cudd_addVectorCompose
DdNode *
Cudd_bddXnor(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Computes the exclusive NOR of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.
 Side Effects None
 See Also
Cudd_bddIte
Cudd_addApply
Cudd_bddAnd
Cudd_bddOr
Cudd_bddNand
Cudd_bddNor
Cudd_bddXor
DdNode *
Cudd_bddXorExistAbstract(
DdManager * manager,
DdNode * f,
DdNode * g,
DdNode * cube
)
 Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube. The variables are existentially abstracted. Returns a pointer to the result is successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddUnivAbstract
Cudd_bddExistAbstract
Cudd_bddAndAbstract
DdNode *
Cudd_bddXor(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Computes the exclusive OR of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.
 Side Effects None
 See Also
Cudd_bddIte
Cudd_addApply
Cudd_bddAnd
Cudd_bddOr
Cudd_bddNand
Cudd_bddNor
Cudd_bddXnor
DdNode *
Cudd_zddChange(
DdManager * dd,
DdNode * P,
int var
)
 Substitutes a variable with its complement in a ZDD. returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
double
Cudd_zddCountDouble(
DdManager * zdd,
DdNode * P
)
 Counts the number of minterms of a ZDD. The result is returned as a double. If the procedure runs out of memory, it returns CUDD_OUT_OF_MEM. This procedure is used in Cudd_zddCountMinterm.
 Side Effects None
 See Also
Cudd_zddCountMinterm
Cudd_zddCount
double
Cudd_zddCountMinterm(
DdManager * zdd,
DdNode * node,
int path
)
 Counts the number of minterms of the ZDD rooted at
node
. This procedure takes a parameter path
that specifies how many variables are in the support of the function.
 Side Effects None
 See Also
Cudd_zddCountDouble
int
Cudd_zddCount(
DdManager * zdd,
DdNode * P
)
 Returns an integer representing the number of minterms in a ZDD.
 Side Effects None
 See Also
Cudd_zddCountDouble
int
Cudd_zddDagSize(
DdNode * p_node
)
 Counts the number of nodes in a ZDD. This function duplicates Cudd_DagSize and is only retained for compatibility.
 Side Effects None
 See Also
Cudd_DagSize
DdNode *
Cudd_zddDiffConst(
DdManager * zdd,
DdNode * P,
DdNode * Q
)
 Inclusion test for ZDDs (P implies Q). No new nodes are generated by this procedure. Returns empty if true; a valid pointer different from empty or DD_NON_CONSTANT otherwise.
 Side Effects None
 See Also
Cudd_zddDiff
DdNode *
Cudd_zddDiff(
DdManager * dd,
DdNode * P,
DdNode * Q
)
 Computes the difference of two ZDDs. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_zddDiffConst
DdNode *
Cudd_zddDivideF(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Modified version of Cudd_zddDivide. This function may disappear in future releases.
 Side Effects None
DdNode *
Cudd_zddDivide(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Computes the quotient of two unate covers represented by ZDDs. Unate covers use one ZDD variable for each BDD variable. Returns a pointer to the resulting ZDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_zddWeakDiv
int
Cudd_zddDumpDot(
DdManager * dd, manager
int n, number of output nodes to be dumped
DdNode ** f, array of output nodes to be dumped
char ** inames, array of input names (or NULL)
char ** onames, array of output names (or NULL)
FILE * fp pointer to the dump file
)
 Writes a file representing the argument ZDDs in a format suitable for the graph drawing program dot. It returns 1 in case of success; 0 otherwise (e.g., outofmemory, file system full). Cudd_zddDumpDot does not close the file: This is the caller responsibility. Cudd_zddDumpDot uses a minimal unique subset of the hexadecimal address of a node as name for it. If the argument inames is nonnull, it is assumed to hold the pointers to the names of the inputs. Similarly for onames. Cudd_zddDumpDot uses the following convention to draw arcs:
 solid line: THEN arcs;
 dashed line: ELSE arcs.
The dot options are chosen so that the drawing fits on a lettersize sheet.
 Side Effects None
 See Also
Cudd_DumpDot
Cudd_zddPrintDebug
DdNode *
Cudd_zddIntersect(
DdManager * dd,
DdNode * P,
DdNode * Q
)
 Computes the intersection of two ZDDs. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
DdNode *
Cudd_zddIsop(
DdManager * dd,
DdNode * L,
DdNode * U,
DdNode ** zdd_I
)
 Computes an irredundant sum of products (ISOP) in ZDD form from BDDs. The two BDDs L and U represent the lower bound and the upper bound, respectively, of the function. The ISOP uses two ZDD variables for each BDD variable: One for the positive literal, and one for the negative literal. These two variables should be adjacent in the ZDD order. The two ZDD variables corresponding to BDD variable
i
should have indices 2i
and 2i+1
. The result of this procedure depends on the variable order. If successful, Cudd_zddIsop returns the BDD for the function chosen from the interval. The ZDD representing the irredundant cover is returned as a side effect in zdd_I. In case of failure, NULL is returned.
 Side Effects zdd_I holds the pointer to the ZDD for the ISOP on successful return.
 See Also
Cudd_bddIsop
Cudd_zddVarsFromBddVars
DdNode *
Cudd_zddIte(
DdManager * dd,
DdNode * f,
DdNode * g,
DdNode * h
)
 Computes the ITE of three ZDDs. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
DdNode *
Cudd_zddIthVar(
DdManager * dd,
int i
)
 Retrieves the ZDD variable with index i if it already exists, or creates a new ZDD variable. Returns a pointer to the variable if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddIthVar
Cudd_addIthVar
DdNode *
Cudd_zddPortFromBdd(
DdManager * dd,
DdNode * B
)
 Converts a BDD into a ZDD. This function assumes that there is a onetoone correspondence between the BDD variables and the ZDD variables, and that the variable order is the same for both types of variables. These conditions are established if the ZDD variables are created by one call to Cudd_zddVarsFromBddVars with multiplicity = 1. Returns a pointer to the resulting ZDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_zddVarsFromBddVars
DdNode *
Cudd_zddPortToBdd(
DdManager * dd,
DdNode * f
)
 Converts a ZDD into a BDD. Returns a pointer to the resulting ZDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_zddPortFromBdd
int
Cudd_zddPrintDebug(
DdManager * zdd,
DdNode * f,
int n,
int pr
)
 Prints to the standard output a DD and its statistics. The statistics include the number of nodes and the number of minterms. (The number of minterms is also the number of combinations in the set.) The statistics are printed if pr > 0. Specifically:
 pr = 0 : prints nothing
 pr = 1 : prints counts of nodes and minterms
 pr = 2 : prints counts + disjoint sum of product
 pr = 3 : prints counts + list of nodes
 pr > 3 : prints counts + disjoint sum of product + list of nodes
Returns 1 if successful; 0 otherwise.
 Side Effects None
int
Cudd_zddPrintMinterm(
DdManager * zdd,
DdNode * node
)

 Side Effects None
 See Also
Cudd_zddPrintDebug
void
Cudd_zddPrintSubtable(
DdManager * table
)
 Prints the ZDD table for debugging purposes.
 Side Effects None
DdNode *
Cudd_zddProduct(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Computes the product of two covers represented by ZDDs. The result is also a ZDD. Returns a pointer to the result if successful; NULL otherwise. The covers on which Cudd_zddProduct operates use two ZDD variables for each function variable (one ZDD variable for each literal of the variable). Those two ZDD variables should be adjacent in the order.
 Side Effects None
 See Also
Cudd_zddUnateProduct
long
Cudd_zddReadNodeCount(
DdManager * dd
)
 Reports the number of nodes in ZDDs. This number always includes the two constants 1 and 0.
 Side Effects None
 See Also
Cudd_ReadPeakNodeCount
Cudd_ReadNodeCount
void
Cudd_zddRealignDisable(
DdManager * unique
)
 Disables realignment of ZDD order to BDD order.
 Side Effects None
 See Also
Cudd_zddRealignEnable
Cudd_zddRealignmentEnabled
Cudd_bddRealignEnable
Cudd_bddRealignmentEnabled
void
Cudd_zddRealignEnable(
DdManager * unique
)
 Enables realignment of the ZDD variable order to the BDD variable order after the BDDs and ADDs have been reordered. The number of ZDD variables must be a multiple of the number of BDD variables for realignment to make sense. If this condition is not met, Cudd_ReduceHeap will return 0. Let
M
be the ratio of the two numbers. For the purpose of realignment, the ZDD variables from M*i
to (M+1)*i1
are reagarded as corresponding to BDD variable i
. Realignment is initially disabled.
 Side Effects None
 See Also
Cudd_ReduceHeap
Cudd_zddRealignDisable
Cudd_zddRealignmentEnabled
Cudd_bddRealignDisable
Cudd_bddRealignmentEnabled
int
Cudd_zddRealignmentEnabled(
DdManager * unique
)
 Returns 1 if the realignment of ZDD order to BDD order is enabled; 0 otherwise.
 Side Effects None
 See Also
Cudd_zddRealignEnable
Cudd_zddRealignDisable
Cudd_bddRealignEnable
Cudd_bddRealignDisable
int
Cudd_zddReduceHeap(
DdManager * table, DD manager
Cudd_ReorderingType heuristic, method used for reordering
int minsize bound below which no reordering occurs
)
 Main dynamic reordering routine for ZDDs. Calls one of the possible reordering procedures:
 Swapping
 Sifting
 Symmetric Sifting
For sifting and symmetric sifting it is possible to request reordering to convergence. The core of all methods is the reordering procedure cuddZddSwapInPlace() which swaps two adjacent variables. Returns 1 in case of success; 0 otherwise. In the case of symmetric sifting (with and without convergence) returns 1 plus the number of symmetric variables, in case of success.
 Side Effects Changes the variable order for all ZDDs and clears the cache.
int
Cudd_zddShuffleHeap(
DdManager * table, DD manager
int * permutation required variable permutation
)
 Reorders ZDD variables according to given permutation. The ith entry of the permutation array contains the index of the variable that should be brought to the ith level. The size of the array should be equal or greater to the number of variables currently in use. Returns 1 in case of success; 0 otherwise.
 Side Effects Changes the ZDD variable order for all diagrams and clears the cache.
 See Also
Cudd_zddReduceHeap
DdNode *
Cudd_zddSubset0(
DdManager * dd,
DdNode * P,
int var
)
 Computes the negative cofactor of a ZDD w.r.t. a variable. In terms of combinations, the result is the set of all combinations in which the variable is negated. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_zddSubset1
DdNode *
Cudd_zddSubset1(
DdManager * dd,
DdNode * P,
int var
)
 Computes the positive cofactor of a ZDD w.r.t. a variable. In terms of combinations, the result is the set of all combinations in which the variable is asserted. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_zddSubset0
void
Cudd_zddSymmProfile(
DdManager * table,
int lower,
int upper
)
 Prints statistics on symmetric ZDD variables.
 Side Effects None
DdNode *
Cudd_zddUnateProduct(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Computes the product of two unate covers represented as ZDDs. Unate covers use one ZDD variable for each BDD variable. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_zddProduct
DdNode *
Cudd_zddUnion(
DdManager * dd,
DdNode * P,
DdNode * Q
)
 Computes the union of two ZDDs. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
int
Cudd_zddVarsFromBddVars(
DdManager * dd, DD manager
int multiplicity how many ZDD variables are created for each BDD variable
)
 Creates one or more ZDD variables for each BDD variable. If some ZDD variables already exist, only the missing variables are created. Parameter multiplicity allows the caller to control how many variables are created for each BDD variable in existence. For instance, if ZDDs are used to represent covers, two ZDD variables are required for each BDD variable. The order of the BDD variables is transferred to the ZDD variables. If a variable group tree exists for the BDD variables, a corresponding ZDD variable group tree is created by expanding the BDD variable tree. In any case, the ZDD variables derived from the same BDD variable are merged in a ZDD variable group. If a ZDD variable group tree exists, it is freed. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
Cudd_bddNewVar
Cudd_bddIthVar
Cudd_bddNewVarAtLevel
DdNode *
Cudd_zddWeakDivF(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Modified version of Cudd_zddWeakDiv. This function may disappear in future releases.
 Side Effects None
 See Also
Cudd_zddWeakDiv
DdNode *
Cudd_zddWeakDiv(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Applies weak division to two ZDDs representing two covers. Returns a pointer to the ZDD representing the result if successful; NULL otherwise. The result of weak division depends on the variable order. The covers on which Cudd_zddWeakDiv operates use two ZDD variables for each function variable (one ZDD variable for each literal of the variable). Those two ZDD variables should be adjacent in the order.
 Side Effects None
 See Also
Cudd_zddDivide
DD_LSDIGIT(
x
)
 Extract the least significant digit of a double digit. Used in the manipulation of arbitrary precision integers.
 Side Effects None
 See Also
DD_MSDIGIT
DD_MINUS_INFINITY(
dd
)
 Returns the minus infinity constant node.
 Side Effects none
 See Also
DD_ONE
DD_ZERO
DD_PLUS_INFINITY
DD_MSDIGIT(
x
)
 Extract the most significant digit of a double digit. Used in the manipulation of arbitrary precision integers.
 Side Effects None
 See Also
DD_LSDIGIT
DD_ONE(
dd
)
 Returns the constant 1 node.
 Side Effects none
 See Also
DD_ZERO
DD_PLUS_INFINITY
DD_MINUS_INFINITY
DD_PLUS_INFINITY(
dd
)
 Returns the plus infinity constant node.
 Side Effects none
 See Also
DD_ONE
DD_ZERO
DD_MINUS_INFINITY
DD_ZERO(
dd
)
 Returns the arithmetic 0 constant node. This is different from the logical zero. The latter is obtained by Cudd_Not(DD_ONE(dd)).
 Side Effects none
 See Also
DD_ONE
Cudd_Not
DD_PLUS_INFINITY
DD_MINUS_INFINITY
DdNode *
cuddAddCmplRecur(
DdManager * dd,
DdNode * f
)
 Performs the recursive step of Cudd_addCmpl. Returns a pointer to the resulting ADD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addCmpl
DdNode *
cuddAddComposeRecur(
DdManager * dd,
DdNode * f,
DdNode * g,
DdNode * proj
)
 Performs the recursive step of Cudd_addCompose. Returns the composed BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addCompose
DdNode *
cuddAddConstrainRecur(
DdManager * dd,
DdNode * f,
DdNode * c
)
 Performs the recursive step of Cudd_addConstrain. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addConstrain
DdNode *
cuddAddExistAbstractRecur(
DdManager * manager,
DdNode * f,
DdNode * cube
)
 Performs the recursive step of Cudd_addExistAbstract. Returns the ADD obtained by abstracting the variables of cube from f, if successful; NULL otherwise.
 Side Effects None
DdNode *
cuddAddIteRecur(
DdManager * dd,
DdNode * f,
DdNode * g,
DdNode * h
)
 Implements the recursive step of Cudd_addIte(f,g,h). Returns a pointer to the resulting ADD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addIte
DdNode *
cuddAddNegateRecur(
DdManager * dd,
DdNode * f
)
 Implements the recursive step of Cudd_addNegate. Returns a pointer to the result.
 Side Effects None
DdNode *
cuddAddOrAbstractRecur(
DdManager * manager,
DdNode * f,
DdNode * cube
)
 Performs the recursive step of Cudd_addOrAbstract. Returns the ADD obtained by abstracting the variables of cube from f, if successful; NULL otherwise.
 Side Effects None
DdNode *
cuddAddRestrictRecur(
DdManager * dd,
DdNode * f,
DdNode * c
)
 Performs the recursive step of Cudd_addRestrict. Returns the restricted ADD if successful; otherwise NULL.
 Side Effects None
 See Also
Cudd_addRestrict
DdNode *
cuddAddRoundOffRecur(
DdManager * dd,
DdNode * f,
double trunc
)
 Implements the recursive step of Cudd_addRoundOff. Returns a pointer to the result.
 Side Effects None
DdNode *
cuddAddScalarInverseRecur(
DdManager * dd,
DdNode * f,
DdNode * epsilon
)
 Returns a pointer to the resulting ADD in case of success. Returns NULL if any discriminants smaller than epsilon is encountered.
 Side Effects None
DdNode *
cuddAddUnivAbstractRecur(
DdManager * manager,
DdNode * f,
DdNode * cube
)
 Performs the recursive step of Cudd_addUnivAbstract. Returns the ADD obtained by abstracting the variables of cube from f, if successful; NULL otherwise.
 Side Effects None
DdNode *
cuddAllocNode(
DdManager * unique
)
 Fast storage allocation for DdNodes in the table. The first 4 bytes of a chunk contain a pointer to the next block; the rest contains DD_MEM_CHUNK spaces for DdNodes. Returns a pointer to a new node if successful; NULL is memory is full.
 Side Effects None
 See Also
cuddDynamicAllocNode
int
cuddAnnealing(
DdManager * table,
int lower,
int upper
)
 Get x, y by random selection. Choose either exchange or jump randomly. In case of jump, choose between jump_up and jump_down randomly. Do exchange or jump and get optimal case. Loop until there is no improvement or temperature reaches minimum. Returns 1 in case of success; 0 otherwise.
 Side Effects None
int
cuddBddAlignToZdd(
DdManager * table DD manager
)
 Reorders BDD variables according to the order of the ZDD variables. This function can be called at the end of ZDD reordering to insure that the order of the BDD variables is consistent with the order of the ZDD variables. The number of ZDD variables must be a multiple of the number of BDD variables. Let
M
be the ratio of the two numbers. cuddBddAlignToZdd then considers the ZDD variables from M*i
to (M+1)*i1
as corresponding to BDD variable i
. This function should be normally called from Cudd_zddReduceHeap, which clears the cache. Returns 1 in case of success; 0 otherwise.
 Side Effects Changes the BDD variable order for all diagrams and performs garbage collection of the BDD unique table.
 See Also
Cudd_ShuffleHeap
Cudd_zddReduceHeap
DdNode *
cuddBddAndAbstractRecur(
DdManager * manager,
DdNode * f,
DdNode * g,
DdNode * cube
)
 Takes the AND of two BDDs and simultaneously abstracts the variables in cube. The variables are existentially abstracted. Returns a pointer to the result is successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddAndAbstract
DdNode *
cuddBddAndRecur(
DdManager * manager,
DdNode * f,
DdNode * g
)
 Implements the recursive step of Cudd_bddAnd by taking the conjunction of two BDDs. Returns a pointer to the result is successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddAnd
DdNode *
cuddBddBooleanDiffRecur(
DdManager * manager,
DdNode * f,
DdNode * var
)
 Performs the recursive steps of Cudd_bddBoleanDiff. Returns the BDD obtained by XORing the cofactors of f with respect to var if successful; NULL otherwise. Exploits the fact that dF/dx = dF'/dx.
 Side Effects None
DdNode *
cuddBddClippingAndAbstract(
DdManager * dd, manager
DdNode * f, first conjunct
DdNode * g, second conjunct
DdNode * cube, cube of variables to be abstracted
int maxDepth, maximum recursion depth
int direction under (0) or over (1) approximation
)
 Approximates the conjunction of two BDDs f and g and simultaneously abstracts the variables in cube. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.
 Side Effects None
 See Also
Cudd_bddClippingAndAbstract
DdNode *
cuddBddClippingAnd(
DdManager * dd, manager
DdNode * f, first conjunct
DdNode * g, second conjunct
int maxDepth, maximum recursion depth
int direction under (0) or over (1) approximation
)
 Approximates the conjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.
 Side Effects None
 See Also
Cudd_bddClippingAnd
DdNode *
cuddBddComposeRecur(
DdManager * dd,
DdNode * f,
DdNode * g,
DdNode * proj
)
 Performs the recursive step of Cudd_bddCompose. Exploits the fact that the composition of f' with g produces the complement of the composition of f with g to better utilize the cache. Returns the composed BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddCompose
DdNode *
cuddBddConstrainRecur(
DdManager * dd,
DdNode * f,
DdNode * c
)
 Performs the recursive step of Cudd_bddConstrain. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddConstrain
DdNode *
cuddBddExistAbstractRecur(
DdManager * manager,
DdNode * f,
DdNode * cube
)
 Performs the recursive steps of Cudd_bddExistAbstract. Returns the BDD obtained by abstracting the variables of cube from f if successful; NULL otherwise. It is also used by Cudd_bddUnivAbstract.
 Side Effects None
 See Also
Cudd_bddExistAbstract
Cudd_bddUnivAbstract
DdNode *
cuddBddIntersectRecur(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Implements the recursive step of Cudd_bddIntersect.
 Side Effects None
 See Also
Cudd_bddIntersect
DdNode *
cuddBddIsop(
DdManager * dd,
DdNode * L,
DdNode * U
)
 Performs the recursive step of Cudd_bddIsop.
 Side Effects None
 See Also
Cudd_bddIsop
DdNode *
cuddBddIteRecur(
DdManager * dd,
DdNode * f,
DdNode * g,
DdNode * h
)
 Implements the recursive step of Cudd_bddIte. Returns a pointer to the resulting BDD. NULL if the intermediate result blows up or if reordering occurs.
 Side Effects None
DdNode *
cuddBddLICompaction(
DdManager * dd, manager
DdNode * f, function to be minimized
DdNode * c constraint (care set)
)
 Performs safe minimization of a BDD. Given the BDD
f
of a function to be minimized and a BDD c
representing the care set, Cudd_bddLICompaction produces the BDD of a function that agrees with f
wherever c
is 1. Safe minimization means that the size of the result is guaranteed not to exceed the size of f
. This function is based on the DAC97 paper by Hong et al.. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddLICompaction
DdNode *
cuddBddLiteralSetIntersectionRecur(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Performs the recursive step of Cudd_bddLiteralSetIntersection. Scans the cubes for common variables, and checks whether they agree in phase. Returns a pointer to the resulting cube if successful; NULL otherwise.
 Side Effects None
DdNode *
cuddBddRestrictRecur(
DdManager * dd,
DdNode * f,
DdNode * c
)
 Performs the recursive step of Cudd_bddRestrict. Returns the restricted BDD if successful; otherwise NULL.
 Side Effects None
 See Also
Cudd_bddRestrict
DdNode *
cuddBddTransfer(
DdManager * ddS,
DdManager * ddD,
DdNode * f
)
 Convert a BDD from a manager to another one. Returns a pointer to the BDD in the destination manager if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddTransfer
DdNode *
cuddBddXorExistAbstractRecur(
DdManager * manager,
DdNode * f,
DdNode * g,
DdNode * cube
)
 Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube. The variables are existentially abstracted. Returns a pointer to the result is successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddAndAbstract
DdNode *
cuddBddXorRecur(
DdManager * manager,
DdNode * f,
DdNode * g
)
 Implements the recursive step of Cudd_bddXor by taking the exclusive OR of two BDDs. Returns a pointer to the result is successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_bddXor
DdNode *
cuddCProjectionRecur(
DdManager * dd,
DdNode * R,
DdNode * Y,
DdNode * Ysupp
)
 Performs the recursive step of Cudd_CProjection. Returns the projection if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_CProjection
void
cuddCacheFlush(
DdManager * table
)
 Flushes the cache.
 Side Effects None
int
cuddCacheProfile(
DdManager * table,
FILE * fp
)
 Computes and prints a profile of the cache usage. Returns 1 if successful; 0 otherwise.
 Side Effects None
void
cuddCacheResize(
DdManager * table
)
 Resizes the cache.
 Side Effects None
int
cuddCheckCube(
DdManager * dd,
DdNode * g
)
 Checks whether g is the BDD of a cube. Returns 1 in case of success; 0 otherwise. The constant 1 is a valid cube, but all other constant functions cause cuddCheckCube to return 0.
 Side Effects None
DdNode *
cuddCofactorRecur(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Performs the recursive step of Cudd_Cofactor. Returns a pointer to the cofactor if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_Cofactor
int
cuddCollectNodes(
DdNode * f,
st_table * visited
)
 Traverses the BDD f and collects all its nodes in a symbol table. f is assumed to be a regular pointer and cuddCollectNodes guarantees this assumption in the recursive calls. Returns 1 in case of success; 0 otherwise.
 Side Effects None
int
cuddComputeFloorLog2(
unsigned int value
)
 Returns the floor of the logarithm to the base 2. The input value is assumed to be greater than 0.
 Side Effects None
cuddDeallocNode(
unique,
node
)
 Adds node to the head of the free list. Does not deallocate memory chunks that become free. This function is also used by the dynamic reordering functions.
 Side Effects None
 See Also
cuddAllocNode
cuddDynamicAllocNode
cuddDeref(
n
)
 Decreases the reference count of node. It is primarily used in recursive procedures to decrease the ref count of a result node before returning it. This accomplishes the goal of removing the protection applied by a previous cuddRef. This being a macro, it is faster than Cudd_Deref, but it cannot be used in constructs like cuddDeref(a = b()).
 Side Effects none
 See Also
Cudd_Deref
int
cuddDestroySubtables(
DdManager * unique,
int n
)
 Destroys the n most recently created subtables in a unique table. n should be positive. The subtables should not contain any live nodes, except the (isolated) projection function. The projection functions are freed. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
cuddInsertSubtables
DdNode *
cuddDynamicAllocNode(
DdManager * table
)
 Dynamically allocates a Node. This procedure is similar to cuddAllocNode in Cudd_Table.c, but it does not attempt garbage collection, because during reordering there are no dead nodes. Returns a pointer to a new node if successful; NULL is memory is full.
 Side Effects None
 See Also
cuddAllocNode
int
cuddExact(
DdManager * table,
int lower,
int upper
)
 Exact variable ordering algorithm. Finds an optimum order for the variables between lower and upper. Returns 1 if successful; 0 otherwise.
 Side Effects None
cuddE(
node
)
 Returns the else child of an internal node. If
node
is a constant node, the result is unpredictable. The pointer passed to cuddE must be regular.
 Side Effects none
 See Also
Cudd_E
void
cuddFreeTable(
DdManager * unique
)
 Frees the resources associated to a unique table.
 Side Effects None
 See Also
cuddInitTable
int
cuddGarbageCollectZdd(
DdManager * unique,
int clearCache
)
 Performs garbage collection on a ZDD unique table. If clearCache is 0, the cache is not cleared. This should only be specified if the cache has been cleared right before calling cuddGarbageCollectZdd. (As in the case of dynamic reordering.) Returns the total number of deleted nodes.
 Side Effects None
 See Also
cuddGarbageCollect
int
cuddGarbageCollect(
DdManager * unique,
int clearCache
)
 Performs garbage collection on a unique table. If clearCache is 0, the cache is not cleared. This should only be specified if the cache has been cleared right before calling cuddGarbageCollect. (As in the case of dynamic reordering.) Returns the total number of deleted nodes.
 Side Effects None
 See Also
cuddGarbageCollectZdd
int
cuddGa(
DdManager * table, manager
int lower, lowest level to be reordered
int upper highest level to be reorderded
)
 Genetic algorithm for DD reordering. The two children of a crossover will be stored in storedd[popsize
 Side Effects None
void
cuddGetBranches(
DdNode * g,
DdNode ** g1,
DdNode ** g0
)
 Computes the children of g.
 Side Effects None
DdHashTable *
cuddHashTableInit(
DdManager * manager,
unsigned int keySize,
unsigned int initSize
)
 Initializes a hash table. Returns a pointer to the new table if successful; NULL otherwise.
 Side Effects None
 See Also
cuddHashTableQuit
int
cuddHashTableInsert1(
DdHashTable * hash,
DdNode * f,
DdNode * value,
ptrint count
)
 Inserts an item in a hash table when the key is one pointer. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
cuddHashTableInsert
cuddHashTableInsert2
cuddHashTableInsert3
cuddHashTableLookup1
int
cuddHashTableInsert2(
DdHashTable * hash,
DdNode * f,
DdNode * g,
DdNode * value,
ptrint count
)
 Inserts an item in a hash table when the key is composed of two pointers. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
cuddHashTableInsert
cuddHashTableInsert1
cuddHashTableInsert3
cuddHashTableLookup2
int
cuddHashTableInsert3(
DdHashTable * hash,
DdNode * f,
DdNode * g,
DdNode * h,
DdNode * value,
ptrint count
)
 Inserts an item in a hash table when the key is composed of three pointers. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
cuddHashTableInsert
cuddHashTableInsert1
cuddHashTableInsert2
cuddHashTableLookup3
int
cuddHashTableInsert(
DdHashTable * hash,
DdNodePtr * key,
DdNode * value,
ptrint count
)
 Inserts an item in a hash table when the key has more than three pointers. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
[cuddHashTableInsert1
cuddHashTableInsert2
cuddHashTableInsert3
cuddHashTableLookup
DdNode *
cuddHashTableLookup1(
DdHashTable * hash,
DdNode * f
)
 Looks up a key consisting of one pointer in a hash table. Returns the value associated to the key if there is an entry for the given key in the table; NULL otherwise. If the entry is present, its reference counter is decremented if not saturated. If the counter reaches 0, the value of the entry is dereferenced, and the entry is returned to the free list.
 Side Effects None
 See Also
cuddHashTableLookup
cuddHashTableLookup2
cuddHashTableLookup3
cuddHashTableInsert1
DdNode *
cuddHashTableLookup2(
DdHashTable * hash,
DdNode * f,
DdNode * g
)
 Looks up a key consisting of two pointer in a hash table. Returns the value associated to the key if there is an entry for the given key in the table; NULL otherwise. If the entry is present, its reference counter is decremented if not saturated. If the counter reaches 0, the value of the entry is dereferenced, and the entry is returned to the free list.
 Side Effects None
 See Also
cuddHashTableLookup
cuddHashTableLookup1
cuddHashTableLookup3
cuddHashTableInsert2
DdNode *
cuddHashTableLookup3(
DdHashTable * hash,
DdNode * f,
DdNode * g,
DdNode * h
)
 Looks up a key consisting of three pointers in a hash table. Returns the value associated to the key if there is an entry for the given key in the table; NULL otherwise. If the entry is present, its reference counter is decremented if not saturated. If the counter reaches 0, the value of the entry is dereferenced, and the entry is returned to the free list.
 Side Effects None
 See Also
cuddHashTableLookup
cuddHashTableLookup1
cuddHashTableLookup2
cuddHashTableInsert3
DdNode *
cuddHashTableLookup(
DdHashTable * hash,
DdNodePtr * key
)
 Looks up a key consisting of more than three pointers in a hash table. Returns the value associated to the key if there is an entry for the given key in the table; NULL otherwise. If the entry is present, its reference counter is decremented if not saturated. If the counter reaches 0, the value of the entry is dereferenced, and the entry is returned to the free list.
 Side Effects None
 See Also
cuddHashTableLookup1
cuddHashTableLookup2
cuddHashTableLookup3
cuddHashTableInsert
void
cuddHashTableQuit(
DdHashTable * hash
)
 Shuts down a hash table, dereferencing all the values.
 Side Effects None
 See Also
cuddHashTableInit
int
cuddHeapProfile(
DdManager * dd
)
 Prints to stdout the number of live nodes for each level of the DD heap that contains at least one live node. It also prints a summary containing:
 total number of tables;
 number of tables with live nodes;
 table with the largest number of live nodes;
 number of nodes in that table.
If more than one table contains the maximum number of live nodes, only the one of lowest index is reported. Returns 1 in case of success and 0 otherwise.
 Side Effects None
cuddIZ(
dd,
index
)
 Finds the current position of ZDD variable index in the order. This macro duplicates the functionality of Cudd_ReadPermZdd, but it does not check for outofbounds indices and it is more efficient.
 Side Effects none
 See Also
Cudd_ReadPermZdd
int
cuddInitCache(
DdManager * unique, unique table
unsigned int cacheSize, initial size of the cache
unsigned int maxCacheSize cache size beyond which no resizing occurs
)
 Initializes the computed table. It is called by Cudd_Init. Returns 1 in case of success; 0 otherwise.
 Side Effects None
 See Also
Cudd_Init
int
cuddInitInteract(
DdManager * table
)
 Initializes the interaction matrix. The interaction matrix is implemented as a bit vector storing the upper triangle of the symmetric interaction matrix. The bit vector is kept in an array of long integers. The computation is based on a series of depthfirst searches, one for each root of the DAG. Two flags are needed: The local visited flag uses the LSB of the then pointer. The global visited flag uses the LSB of the next pointer. Returns 1 if successful; 0 otherwise.
 Side Effects None
DdManager *
cuddInitTable(
unsigned int numVars, Initial number of BDD variables (and subtables)
unsigned int numVarsZ, Initial number of ZDD variables (and subtables)
unsigned int numSlots Initial size of the BDD subtables
)
 Creates and initializes the unique table. Returns a pointer to the table if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_Init
cuddFreeTable
int
cuddInsertSubtables(
DdManager * unique,
int n,
int level
)
 Inserts n new subtables in a unique table at level. The number n should be positive, and level should be an existing level. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
cuddDestroySubtables
cuddIsConstant(
node
)
 Returns 1 if the node is a constant node (rather than an internal node). All constant nodes have the same index (CUDD_MAXINDEX). The pointer passed to cuddIsConstant must be regular.
 Side Effects none
 See Also
Cudd_IsConstant
cuddI(
dd,
index
)
 Finds the current position of variable index in the order. This macro duplicates the functionality of Cudd_ReadPerm, but it does not check for outofbounds indices and it is more efficient.
 Side Effects none
 See Also
Cudd_ReadPerm
void
cuddLevelQueueDequeue(
DdLevelQueue * queue,
int level
)
 Remove an item from the front of a level queue.
 Side Effects None
 See Also
cuddLevelQueueEnqueue
void *
cuddLevelQueueEnqueue(
DdLevelQueue * queue, level queue
void * key, key to be enqueued
int level level at which to insert
)
 Inserts a new key in a level queue. A new entry is created in the queue only if the node is not already enqueued. Returns a pointer to the queue item if successful; NULL otherwise.
 Side Effects None
 See Also
cuddLevelQueueInit
cuddLevelQueueDequeue
DdLevelQueue *
cuddLevelQueueInit(
int levels, number of levels
int itemSize, size of the item
int numBuckets initial number of hash buckets
)
 Initializes a level queue. A level queue is a queue where inserts are based on the levels of the nodes. Within each level the policy is FIFO. Level queues are useful in traversing a BDD topdown. Queue items are kept in a free list when dequeued for efficiency. Returns a pointer to the new queue if successful; NULL otherwise.
 Side Effects None
 See Also
cuddLevelQueueQuit
cuddLevelQueueEnqueue
cuddLevelQueueDequeue
void
cuddLevelQueueQuit(
DdLevelQueue * queue
)
 Shuts down a level queue and releases all the associated memory.
 Side Effects None
 See Also
cuddLevelQueueInit
int
cuddLinearAndSifting(
DdManager * table,
int lower,
int upper
)
 BDD reduction based on combination of sifting and linear transformations. Assumes that no dead nodes are present.
 Order all the variables according to the number of entries in each unique table.
 Sift the variable up and down, remembering each time the total size of the DD heap. At each position, linear transformation of the two adjacent variables is tried and is accepted if it reduces the size of the DD.
 Select the best permutation.
 Repeat 3 and 4 for all variables.
Returns 1 if successful; 0 otherwise.
 Side Effects None
void
cuddLocalCacheClearAll(
DdManager * manager
)
 Clears the local caches of a manager. Used before reordering.
 Side Effects None
void
cuddLocalCacheClearDead(
DdManager * manager
)
 Clears the dead entries of the local caches of a manager. Used during garbage collection.
 Side Effects None
DdLocalCache *
cuddLocalCacheInit(
DdManager * manager, manager
unsigned int keySize, size of the key (number of operands)
unsigned int cacheSize, Initial size of the cache
unsigned int maxCacheSize Size of the cache beyond which no resizing occurs
)
 Initializes a computed table. Returns a pointer the the new local cache in case of success; NULL otherwise.
 Side Effects None
 See Also
cuddInitCache
void
cuddLocalCacheInsert(
DdLocalCache * cache,
DdNodePtr * key,
DdNode * value
)
 Inserts a result in a local cache.
 Side Effects None
DdNode *
cuddLocalCacheLookup(
DdLocalCache * cache,
DdNodePtr * key
)
 Looks up in a local cache. Returns the result if found; it returns NULL if no result is found.
 Side Effects None
int
cuddLocalCacheProfile(
DdLocalCache * cache
)
 Computes and prints a profile of a local cache usage. Returns 1 if successful; 0 otherwise.
 Side Effects None
void
cuddLocalCacheQuit(
DdLocalCache * cache cache to be shut down
)
 Initializes the computed table. It is called by Cudd_Init. Returns a pointer the the new local cache in case of success; NULL otherwise.
 Side Effects None
 See Also
cuddLocalCacheInit
int
cuddNextHigh(
DdManager * table,
int x
)
 Finds the next subtable with a larger index. Returns the index.
 Side Effects None
 See Also
cuddNextLow
int
cuddNextLow(
DdManager * table,
int x
)
 Finds the next subtable with a smaller index. Returns the index.
 Side Effects None
 See Also
cuddNextHigh
void
cuddPrintNode(
DdNode * f
)
 Prints out information on a node.
 Side Effects None
int
cuddP(
DdManager * dd,
DdNode * f
)
 Prints a DD to the standard output. One line per node is printed. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
Cudd_PrintDebug
void
cuddReclaimZdd(
DdManager * table,
DdNode * n
)
 Brings children of a dead ZDD node back.
 Side Effects None
 See Also
cuddReclaim
void
cuddReclaim(
DdManager * table,
DdNode * n
)
 Brings children of a dead node back.
 Side Effects None
 See Also
cuddReclaimZdd
cuddRef(
n
)
 Increases the reference count of a node, if it is not saturated. This being a macro, it is faster than Cudd_Ref, but it cannot be used in constructs like cuddRef(a = b()).
 Side Effects none
 See Also
Cudd_Ref
DdNode *
cuddRemapUnderApprox(
DdManager * dd, DD manager
DdNode * f, current DD
int numVars, maximum number of variables
int threshold, threshold under which approximation stops
double quality minimum improvement for accepted changes
)
 Applies the remapping underappoximation algorithm. Proceeds in three phases:
 collect information on each node in the BDD; this is done via DFS.
 traverse the BDD in topdown fashion and compute for each node whether remapping increases density.
 traverse the BDD via DFS and actually perform the elimination.
Returns the approximated BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_RemapUnderApprox
int
cuddResizeTableZdd(
DdManager * unique,
int index
)
 Increases the number of ZDD subtables in a unique table so that it meets or exceeds index. When new ZDD variables are created, it is possible to preserve the functions unchanged, or it is possible to preserve the covers unchanged, but not both. cuddResizeTableZdd preserves the covers. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
ddResizeTable
cuddSatDec(
x
)
 Saturating decrement operator.
 Side Effects none
 See Also
cuddSatInc
cuddSatInc(
x
)
 Saturating increment operator.
 Side Effects none
 See Also
cuddSatDec
void
cuddSetInteract(
DdManager * table,
int x,
int y
)
 Given a pair of variables 0 <= x < y < table>size, sets the corresponding bit of the interaction matrix to 1.
 Side Effects None
int
cuddSifting(
DdManager * table,
int lower,
int upper
)
 Implementation of Rudell's sifting algorithm. Assumes that no dead nodes are present.
 Order all the variables according to the number of entries in each unique table.
 Sift the variable up and down, remembering each time the total size of the DD heap.
 Select the best permutation.
 Repeat 3 and 4 for all variables.
Returns 1 if successful; 0 otherwise.
 Side Effects None
DdNode *
cuddSolveEqnRecur(
DdManager * bdd,
DdNode * F, the lefthand side of the equation
DdNode * Y, the cube of remaining y variables
DdNode ** G, the array of solutions
int n, number of unknowns
int * yIndex, array holding the y variable indices
int i level of recursion
)
 Implements the recursive step of Cudd_SolveEqn. Returns NULL if the intermediate solution blows up or reordering occurs. The parametric solutions are stored in the array G.
 Side Effects none
 See Also
Cudd_SolveEqn
Cudd_VerifySol
DdNode*
cuddSplitSetRecur(
DdManager * manager,
st_table * mtable,
int * varSeen,
DdNode * p,
double n,
double max,
int index
)
 Implements the recursive step of Cudd_SplitSet. The procedure recursively traverses the BDD and checks to see if any node satisfies the minterm requirements as specified by 'n'. At any node X, n is compared to the number of minterms in the onset of X's children. If either of the child nodes have exactly n minterms, then that node is returned; else, if n is greater than the onset of one of the child nodes, that node is retained and the difference in the number of minterms is extracted from the other child. In case n minterms can be extracted from constant 1, the algorithm returns the result with at most log(n) nodes.
 Side Effects The array 'varSeen' is updated at every recursive call to set the variables traversed by the procedure.
enum st_retval
cuddStCountfree(
char * key,
char * value,
char * arg
)
 Frees the memory used to store the minterm counts recorded in the visited table. Returns ST_CONTINUE.
 Side Effects None
DdNode *
cuddSubsetHeavyBranch(
DdManager * dd, DD manager
DdNode * f, current DD
int numVars, maximum number of variables
int threshold threshold size for the subset
)
 Here a subset BDD is built by throwing away one of the children. Starting at root, annotate each node with the number of minterms (in terms of the total number of variables specified  numVars), number of nodes taken by the DAG rooted at this node and number of additional nodes taken by the child that has the lesser minterms. The child with the lower number of minterms is thrown away and a dyanmic count of the nodes of the subset is kept. Once the threshold is reached the subset is returned to the calling procedure.
 Side Effects None
 See Also
Cudd_SubsetHeavyBranch
DdNode *
cuddSubsetShortPaths(
DdManager * dd, DD manager
DdNode * f, function to be subset
int numVars, total number of variables in consideration
int threshold, maximum number of nodes allowed in the subset
int hardlimit flag determining whether thershold should be respected strictly
)
 The outermost procedure to return a subset of the given BDD with the largest cubes. The path lengths are calculated, the maximum allowable path length is determined and the number of nodes of this path length that can be used to build a subset. If the threshold is larger than the size of the original BDD, the original BDD is returned.
 Side Effects None
 See Also
Cudd_SubsetShortPaths
int
cuddSwapInPlace(
DdManager * table,
int x,
int y
)
 Swaps two adjacent variables. It assumes that no dead nodes are present on entry to this procedure. The procedure then guarantees that no dead nodes will be present when it terminates. cuddSwapInPlace assumes that x < y. Returns the number of keys in the table if successful; 0 otherwise.
 Side Effects None
int
cuddSwapping(
DdManager * table,
int lower,
int upper,
Cudd_ReorderingType heuristic
)
 Implementation of Plessier's algorithm that reorders variables by a sequence of (nonadjacent) swaps.
 Select two variables (RANDOM or HEURISTIC).
 Permute these variables.
 If the nodes have decreased accept the permutation.
 Otherwise reconstruct the original heap.
 Loop.
Returns 1 in case of success; 0 otherwise.
 Side Effects None
int
cuddSymmCheck(
DdManager * table,
int x,
int y
)
 Checks for symmetry of x and y. Ignores projection functions, unless they are isolated. Returns 1 in case of symmetry; 0 otherwise.
 Side Effects None
int
cuddSymmSiftingConv(
DdManager * table,
int lower,
int upper
)
 Symmetric sifting to convergence algorithm. Assumes that no dead nodes are present.
 Order all the variables according to the number of entries in each unique subtable.
 Sift the variable up and down, remembering each time the total size of the DD heap and grouping variables that are symmetric.
 Select the best permutation.
 Repeat 3 and 4 for all variables.
 Repeat 14 until no further improvement.
Returns 1 plus the number of symmetric variables if successful; 0 otherwise.
 Side Effects None
 See Also
cuddSymmSifting
int
cuddSymmSifting(
DdManager * table,
int lower,
int upper
)
 Symmetric sifting algorithm. Assumes that no dead nodes are present.
 Order all the variables according to the number of entries in each unique subtable.
 Sift the variable up and down, remembering each time the total size of the DD heap and grouping variables that are symmetric.
 Select the best permutation.
 Repeat 3 and 4 for all variables.
Returns 1 plus the number of symmetric variables if successful; 0 otherwise.
 Side Effects None
 See Also
cuddSymmSiftingConv
int
cuddTestInteract(
DdManager * table,
int x,
int y
)
 Given a pair of variables 0 <= x < y < table>size, tests whether the corresponding bit of the interaction matrix is 1. Returns the value of the bit.
 Side Effects None
int
cuddTreeSifting(
DdManager * table, DD table
Cudd_ReorderingType method reordering method for the groups of leaves
)
 Tree sifting algorithm. Assumes that a tree representing a group hierarchy is passed as a parameter. It then reorders each group in postorder fashion by calling ddTreeSiftingAux. Assumes that no dead nodes are present. Returns 1 if successful; 0 otherwise.
 Side Effects None
cuddT(
node
)
 Returns the then child of an internal node. If
node
is a constant node, the result is unpredictable. The pointer passed to cuddT must be regular.
 Side Effects none
 See Also
Cudd_T
DdNode *
cuddUnderApprox(
DdManager * dd, DD manager
DdNode * f, current DD
int numVars, maximum number of variables
int threshold, threshold under which approximation stops
int safe, enforce safe approximation
double quality minimum improvement for accepted changes
)
 Applies Tom Shiple's underappoximation algorithm. Proceeds in three phases:
 collect information on each node in the BDD; this is done via DFS.
 traverse the BDD in topdown fashion and compute for each node whether its elimination increases density.
 traverse the BDD via DFS and actually perform the elimination.
Returns the approximated BDD if successful; NULL otherwise.
 Side Effects None
 See Also
Cudd_UnderApprox
DdNode *
cuddUniqueConst(
DdManager * unique,
CUDD_VALUE_TYPE value
)
 Checks the unique table for the existence of a constant node. If it does not exist, it creates a new one. Does not modify the reference count of whatever is returned. A newly created internal node comes back with a reference count 0. Returns a pointer to the new node.
 Side Effects None
DdNode *
cuddUniqueInterZdd(
DdManager * unique,
int index,
DdNode * T,
DdNode * E
)
 Checks the unique table for the existence of an internal ZDD node. If it does not exist, it creates a new one. Does not modify the reference count of whatever is returned. A newly created internal node comes back with a reference count 0. For a newly created node, increments the reference counts of what T and E point to. Returns a pointer to the new node if successful; NULL if memory is exhausted or if reordering took place.
 Side Effects None
 See Also
cuddUniqueInter
DdNode *
cuddUniqueInter(
DdManager * unique,
int index,
DdNode * T,
DdNode * E
)
 Checks the unique table for the existence of an internal node. If it does not exist, it creates a new one. Does not modify the reference count of whatever is returned. A newly created internal node comes back with a reference count 0. For a newly created node, increments the reference counts of what T and E point to. Returns a pointer to the new node if successful; NULL if memory is exhausted or if reordering took place.
 Side Effects None
 See Also
cuddUniqueInterZdd
DdNode *
cuddVerifySol(
DdManager * bdd,
DdNode * F, the lefthand side of the equation
DdNode ** G, the array of solutions
int * yIndex, array holding the y variable indices
int n number of unknowns
)
 Implements the recursive step of Cudd_VerifySol.
 Side Effects none
 See Also
Cudd_VerifySol
cuddV(
node
)
 Returns the value of a constant node. If
node
is an internal node, the result is unpredictable. The pointer passed to cuddV must be regular.
 Side Effects none
 See Also
Cudd_V
int
cuddWindowReorder(
DdManager * table, DD table
int low, lowest index to reorder
int high, highest index to reorder
Cudd_ReorderingType submethod window reordering option
)
 Reorders by applying the method of the sliding window. Tries all possible permutations to the variables in a window that slides from low to high. The size of the window is determined by submethod. Assumes that no dead nodes are present. Returns 1 in case of success; 0 otherwise.
 Side Effects None
int
cuddZddAlignToBdd(
DdManager * table DD manager
)
 Reorders ZDD variables according to the order of the BDD variables. This function can be called at the end of BDD reordering to insure that the order of the ZDD variables is consistent with the order of the BDD variables. The number of ZDD variables must be a multiple of the number of BDD variables. Let
M
be the ratio of the two numbers. cuddZddAlignToBdd then considers the ZDD variables from M*i
to (M+1)*i1
as corresponding to BDD variable i
. This function should be normally called from Cudd_ReduceHeap, which clears the cache. Returns 1 in case of success; 0 otherwise.
 Side Effects Changes the ZDD variable order for all diagrams and performs garbage collection of the ZDD unique table.
 See Also
Cudd_zddShuffleHeap
Cudd_ReduceHeap
DdNode *
cuddZddChangeAux(
DdManager * zdd,
DdNode * P,
DdNode * zvar
)
 Performs the recursive step of Cudd_zddChange.
 Side Effects None
DdNode *
cuddZddChange(
DdManager * dd,
DdNode * P,
int var
)
 Substitutes a variable with its complement in a ZDD. returns a pointer to the result if successful; NULL otherwise. cuddZddChange performs the same function as Cudd_zddChange, but does not restart if reordering has taken place. Therefore it can be called from within a recursive procedure.
 Side Effects None
 See Also
Cudd_zddChange
DdNode *
cuddZddDiff(
DdManager * zdd,
DdNode * P,
DdNode * Q
)
 Performs the recursive step of Cudd_zddDiff.
 Side Effects None
DdNode *
cuddZddDivideF(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Performs the recursive step of Cudd_zddDivideF.
 Side Effects None
 See Also
Cudd_zddDivideF
DdNode *
cuddZddDivide(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Performs the recursive step of Cudd_zddDivide.
 Side Effects None
 See Also
Cudd_zddDivide
void
cuddZddFreeUniv(
DdManager * zdd
)
 Frees the ZDD universe.
 Side Effects None
 See Also
cuddZddInitUniv
int
cuddZddGetCofactors2(
DdManager * dd,
DdNode * f,
int v,
DdNode ** f1,
DdNode ** f0
)
 Computes the twoway decomposition of f w.r.t. v.
 Side Effects The results are returned in f1 and f0.
 See Also
cuddZddGetCofactors3
int
cuddZddGetCofactors3(
DdManager * dd,
DdNode * f,
int v,
DdNode ** f1,
DdNode ** f0,
DdNode ** fd
)
 Computes the threeway decomposition of function f (represented by a ZDD) wit respect to variable v.
 Side Effects The results are returned in f1, f0, and fd.
 See Also
cuddZddGetCofactors2
DdNode *
cuddZddGetNodeIVO(
DdManager * dd,
int index,
DdNode * g,
DdNode * h
)
 Wrapper for cuddUniqueInterZdd that is independent of variable ordering (IVO). This function does not require parameter index to precede the indices of the top nodes of g and h in the variable order. Returns a pointer to the result node under normal conditions; NULL if reordering occurred or memory was exhausted.
 Side Effects None
 See Also
cuddZddGetNode
cuddZddIsop
DdNode *
cuddZddGetNode(
DdManager * zdd,
int id,
DdNode * T,
DdNode * E
)
 Wrapper for cuddUniqueInterZdd, which applies the ZDD reduction rule. Returns a pointer to the result node under normal conditions; NULL if reordering occurred or memory was exhausted.
 Side Effects None
 See Also
cuddUniqueInterZdd
int
cuddZddInitUniv(
DdManager * zdd
)
 Initializes the ZDD universe. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
cuddZddFreeUniv
DdNode *
cuddZddIntersect(
DdManager * zdd,
DdNode * P,
DdNode * Q
)
 Performs the recursive step of Cudd_zddIntersect.
 Side Effects None
DdNode *
cuddZddIsop(
DdManager * dd,
DdNode * L,
DdNode * U,
DdNode ** zdd_I
)
 Performs the recursive step of Cudd_zddIsop.
 Side Effects None
 See Also
Cudd_zddIsop
DdNode *
cuddZddIte(
DdManager * dd,
DdNode * f,
DdNode * g,
DdNode * h
)
 Performs the recursive step of Cudd_zddIte.
 Side Effects None
int
cuddZddLinearInPlace(
DdManager * table,
int x,
int y
)
 Linearly combines two adjacent variables. It assumes that no dead nodes are present on entry to this procedure. The procedure then guarantees that no dead nodes will be present when it terminates. cuddZddLinearInPlace assumes that x < y. Returns the number of keys in the table if successful; 0 otherwise.
 Side Effects None
 See Also
cuddZddSwapInPlace
cuddLinearInPlace
int
cuddZddLinearSifting(
DdManager * table,
int lower,
int upper
)
 Implementation of the linear sifting algorithm for ZDDs. Assumes that no dead nodes are present.
 Order all the variables according to the number of entries in each unique table.
 Sift the variable up and down and applies the XOR transformation, remembering each time the total size of the DD heap.
 Select the best permutation.
 Repeat 3 and 4 for all variables.
Returns 1 if successful; 0 otherwise.
 Side Effects None
int
cuddZddNextHigh(
DdManager * table,
int x
)
 Finds the next subtable with a larger index. Returns the index.
 Side Effects None
int
cuddZddNextLow(
DdManager * table,
int x
)
 Finds the next subtable with a smaller index. Returns the index.
 Side Effects None
DdNode *
cuddZddProduct(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Performs the recursive step of Cudd_zddProduct.
 Side Effects None
 See Also
Cudd_zddProduct
int
cuddZddP(
DdManager * zdd,
DdNode * f
)
 Prints a ZDD to the standard output. One line per node is printed. Returns 1 if successful; 0 otherwise.
 Side Effects None
 See Also
Cudd_zddPrintDebug
int
cuddZddSifting(
DdManager * table,
int lower,
int upper
)
 Implementation of Rudell's sifting algorithm. Assumes that no dead nodes are present.
 Order all the variables according to the number of entries in each unique table.
 Sift the variable up and down, remembering each time the total size of the DD heap.
 Select the best permutation.
 Repeat 3 and 4 for all variables.
Returns 1 if successful; 0 otherwise.
 Side Effects None
DdNode *
cuddZddSubset0(
DdManager * dd,
DdNode * P,
int var
)
 Computes the negative cofactor of a ZDD w.r.t. a variable. In terms of combinations, the result is the set of all combinations in which the variable is negated. Returns a pointer to the result if successful; NULL otherwise. cuddZddSubset0 performs the same function as Cudd_zddSubset0, but does not restart if reordering has taken place. Therefore it can be called from within a recursive procedure.
 Side Effects None
 See Also
cuddZddSubset1
Cudd_zddSubset0
DdNode *
cuddZddSubset1(
DdManager * dd,
DdNode * P,
int var
)
 Computes the positive cofactor of a ZDD w.r.t. a variable. In terms of combinations, the result is the set of all combinations in which the variable is asserted. Returns a pointer to the result if successful; NULL otherwise. cuddZddSubset1 performs the same function as Cudd_zddSubset1, but does not restart if reordering has taken place. Therefore it can be called from within a recursive procedure.
 Side Effects None
 See Also
cuddZddSubset0
Cudd_zddSubset1
int
cuddZddSwapInPlace(
DdManager * table,
int x,
int y
)
 Swaps two adjacent variables. It assumes that no dead nodes are present on entry to this procedure. The procedure then guarantees that no dead nodes will be present when it terminates. cuddZddSwapInPlace assumes that x < y. Returns the number of keys in the table if successful; 0 otherwise.
 Side Effects None
int
cuddZddSwapping(
DdManager * table,
int lower,
int upper,
Cudd_ReorderingType heuristic
)
 Implementation of Plessier's algorithm that reorders variables by a sequence of (nonadjacent) swaps.
 Select two variables (RANDOM or HEURISTIC).
 Permute these variables.
 If the nodes have decreased accept the permutation.
 Otherwise reconstruct the original heap.
 Loop.
Returns 1 in case of success; 0 otherwise.
 Side Effects None
int
cuddZddSymmCheck(
DdManager * table,
int x,
int y
)
 Checks for symmetry of x and y. Ignores projection functions, unless they are isolated. Returns 1 in case of symmetry; 0 otherwise.
 Side Effects None
int
cuddZddSymmSiftingConv(
DdManager * table,
int lower,
int upper
)
 Symmetric sifting to convergence algorithm for ZDDs. Assumes that no dead nodes are present.
 Order all the variables according to the number of entries in each unique subtable.
 Sift the variable up and down, remembering each time the total size of the ZDD heap and grouping variables that are symmetric.
 Select the best permutation.
 Repeat 3 and 4 for all variables.
 Repeat 14 until no further improvement.
Returns 1 plus the number of symmetric variables if successful; 0 otherwise.
 Side Effects None
 See Also
cuddZddSymmSifting
int
cuddZddSymmSifting(
DdManager * table,
int lower,
int upper
)
 Symmetric sifting algorithm. Assumes that no dead nodes are present.
 Order all the variables according to the number of entries in each unique subtable.
 Sift the variable up and down, remembering each time the total size of the ZDD heap and grouping variables that are symmetric.
 Select the best permutation.
 Repeat 3 and 4 for all variables.
Returns 1 plus the number of symmetric variables if successful; 0 otherwise.
 Side Effects None
 See Also
cuddZddSymmSiftingConv
int
cuddZddTreeSifting(
DdManager * table, DD table
Cudd_ReorderingType method reordering method for the groups of leaves
)
 Tree sifting algorithm for ZDDs. Assumes that a tree representing a group hierarchy is passed as a parameter. It then reorders each group in postorder fashion by calling zddTreeSiftingAux. Assumes that no dead nodes are present. Returns 1 if successful; 0 otherwise.
 Side Effects None
DdNode *
cuddZddUnateProduct(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Performs the recursive step of Cudd_zddUnateProduct.
 Side Effects None
 See Also
Cudd_zddUnateProduct
DdNode *
cuddZddUnion(
DdManager * zdd,
DdNode * P,
DdNode * Q
)
 Performs the recursive step of Cudd_zddUnion.
 Side Effects None
int
cuddZddUniqueCompare(
int * ptr_x,
int * ptr_y
)
 Comparison function used by qsort to order the variables according to the number of keys in the subtables. Returns the difference in number of keys between the two variables being compared.
 Side Effects None
DdNode *
cuddZddWeakDivF(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Performs the recursive step of Cudd_zddWeakDivF.
 Side Effects None
 See Also
Cudd_zddWeakDivF
DdNode *
cuddZddWeakDiv(
DdManager * dd,
DdNode * f,
DdNode * g
)
 Performs the recursive step of Cudd_zddWeakDiv.
 Side Effects None
 See Also
Cudd_zddWeakDiv
ddAbs(
x
)
 Computes the absolute value of a number.
 Side Effects none
ddCHash2(
o,
f,
g,
s
)
 Hash function for the cache for functions with two operands.
 Side Effects none
 See Also
ddHash
ddCHash
ddCHash(
o,
f,
g,
h,
s
)
 Hash function for the cache.
 Side Effects none
 See Also
ddHash
ddCHash2
ddEqualVal(
x,
y,
e
)
 Returns 1 if the absolute value of the difference of the two arguments x and y is less than e.
 Side Effects none
ddHash(
f,
g,
s
)
 Hash function for the unique table.
 Side Effects none
 See Also
ddCHash
ddCHash2
ddLCHash2(
f,
g,
shift
)
 Computes hash function for keys of two operands.
 Side Effects None
 See Also
ddLCHash3
ddLCHash
ddLCHash3(
f,
g,
h,
shift
)
 Computes hash function for keys of three operands.
 Side Effects None
 See Also
ddLCHash2
ddLCHash
ddMax(
x,
y
)
 Computes the maximum of two numbers.
 Side Effects none
 See Also
ddMin
ddMin(
x,
y
)
 Computes the minimum of two numbers.
 Side Effects none
 See Also
ddMax
lqHash(
key,
shift
)
 Hash function for the table of a level queue.
 Side Effects None
 See Also
hashInsert
hashLookup
hashDelete
(
)
 Adds a function to a hook. A hook is a list of applicationprovided functions called on certain occasions by the package. Returns 1 if the function is successfully added; 2 if the function was already in the list; 0 otherwise.
 Side Effects None
 See Also
Cudd_RemoveHook
(
)
 Applies op to the corresponding discriminants of f and g. Returns a pointer to the result if succssful; NULL otherwise.
 Side Effects None
 See Also
Cudd_addPlus
Cudd_addTimes
Cudd_addThreshold
Cudd_addSetNZ
Cudd_addDivide
Cudd_addMinus
Cudd_addMinimum
Cudd_addMaximum
Cudd_addOneZeroMaximum
Cudd_addDiff
Cudd_addAgreement
Cudd_addOr
Cudd_addNand
Cudd_addNor
Cudd_addXor
Cudd_addXnor
(
)
 Checks whether a function is in a hook. A hook is a list of applicationprovided functions called on certain occasions by the package. Returns 1 if the function is found; 0 otherwise.
 Side Effects None
 See Also
Cudd_AddHook
Cudd_RemoveHook
(
)
 Enforces DD_MINUS_INF_VAL <= x <= DD_PLUS_INF_VAL. Furthermore, if x <= DD_MINUS_INF_VAL/2, x is set to DD_MINUS_INF_VAL. Similarly, if DD_PLUS_INF_VAL/2 <= x, x is set to DD_PLUS_INF_VAL. Normally this macro is a NOOP. However, if HAVE_IEEE_754 is not defined, it makes sure that a value does not get larger than infinity in absolute value, and once it gets to infinity, stays there. If the value overflows before this macro is applied, no recovery is possible.
 Side Effects none
(
)
 Inserts a result in the cache for a function with two operands.
 Side Effects None
 See Also
cuddCacheInsert
cuddCacheInsert1
(
)
 Inserts a result in the cache for a function with two operands.
 Side Effects None
 See Also
cuddCacheInsert
cuddCacheInsert2
(
)
 Inserts a result in the cache.
 Side Effects None
 See Also
cuddCacheInsert2
cuddCacheInsert1
(
)
 Returns the result if found; it returns NULL if no result is found.
 Side Effects None
 See Also
cuddCacheLookupZdd
cuddCacheLookup1Zdd
(
)
 Returns the result if found; it returns NULL if no result is found.
 Side Effects None
 See Also
cuddCacheLookup
cuddCacheLookup1
(
)
 Looks up in the cache for the result of op applied to f, g, and h. Assumes that the calling procedure (e.g., Cudd_bddIteConstant) is only interested in whether the result is constant or not. Returns the result if found (possibly DD_NON_CONSTANT); otherwise it returns NULL.
 Side Effects None
 See Also
cuddCacheLookup
(
)
 Returns the result if found; it returns NULL if no result is found.
 Side Effects None
 See Also
cuddCacheLookup2Zdd
cuddCacheLookup1Zdd
(
)
 Returns the result if found; it returns NULL if no result is found.
 Side Effects None
 See Also
cuddCacheLookup2
cuddCacheLookup1
(
)
 Returns the result if found; it returns NULL if no result is found.
 Side Effects None
 See Also
cuddCacheLookupZdd
cuddCacheLookup2Zdd
(
)
 Returns the result if found; it returns NULL if no result is found.
 Side Effects None
 See Also
cuddCacheLookup
cuddCacheLookup2
(
)
 Performs the recursive step of Cudd_addApply. Returns a pointer to the result if successful; NULL otherwise.
 Side Effects None
(
)
 Removes a function from a hook. A hook is a list of applicationprovided functions called on certain occasions by the package. Returns 1 if successful; 0 the function was not in the list.
 Side Effects None
 See Also
Cudd_AddHook
(
)
 Selects pairs from a relation R(x,y) (given as a BDD) in such a way that a given x appears in one pair only. Uses a priority function to determine which y should be paired to a given x. Cudd_PrioritySelect returns a pointer to the selected function if successful; NULL otherwise. Three of the argumentsx, y, and zare vectors of BDD variables. The first two are the variables on which R depends. The third vectore is a vector of auxiliary variables, used during the computation. This vector is optional. If a NULL value is passed instead, Cudd_PrioritySelect will create the working variables on the fly. The sizes of x and y (and z if it is not NULL) should equal n. The priority function Pi can be passed as a BDD, or can be built by Cudd_PrioritySelect. If NULL is passed instead of a DdNode *, parameter Pifunc is used by Cudd_PrioritySelect to build a BDD for the priority function. (Pifunc is a pointer to a C function.) If Pi is not NULL, then Pifunc is ignored. Pifunc should have the same interface as the standard priority functions (e.g., Cudd_Dxygtdxz). Cudd_PrioritySelect and Cudd_CProjection can sometimes be used interchangeably. Specifically, calling Cudd_PrioritySelect with Cudd_Xgty as Pifunc produces the same result as calling Cudd_CProjection with the allzero minterm as reference minterm. However, depending on the application, one or the other may be preferable:
 When extracting representatives from an equivalence relation, Cudd_CProjection has the advantage of nor requiring the auxiliary variables.
 When computing matchings in general bipartite graphs, Cudd_PrioritySelect normally obtains better results because it can use more powerful matching schemes (e.g., Cudd_Dxygtdxz).
 Side Effects If called with z == NULL, will create new variables in the manager.
 See Also
Cudd_Dxygtdxz
Cudd_Dxygtdyz
Cudd_Xgty
Cudd_bddAdjPermuteX
Cudd_CProjection
(
)
 Sifts down a variable until it reaches position xHigh. Assumes that x is the bottom of a group (or a singleton). Records all the moves. Returns 1 in case of success; 0 otherwise.
 Side Effects None
(
)
 Sifts from treenode>low to treenode>high. If croupcheck == CUDD_GROUP_CHECK7, it checks for group creation at the end of the initial sifting. If a group is created, it is then sifted again. After sifting one variable, the group that contains it is dissolved. Returns 1 in case of success; 0 otherwise.
 Side Effects None
(
)
 Sifts one variable up and down until it has taken all positions. Checks for aggregation. There may be at most two sweeps, even if the group grows. Assumes that x is either an isolated variable, or it is the bottom of a group. All groups may not have been found. The variable being moved is returned to the best position seen during sifting. Returns 1 in case of success; 0 otherwise.
 Side Effects None
(
)
 Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much. Assumes that y is the top of a group (or a singleton). Checks y for aggregation to the adjacent variables. Records all the moves that are appended to the list of moves received as input and returned as a side effect. Returns 1 in case of success; 0 otherwise.
 Side Effects None