if not a terminal case; f NAND g otherwise.
- Side Effects None
- See Also
Cudd_addApply
- Defined in
cuddAddApply.c
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
- Defined in
cuddAddNeg.c
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
- Defined in
cuddAPI.c
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
- Defined in
cuddAPI.c
DdNode *
Cudd_addNonSimCompose(
DdManager * dd,
DdNode * f,
DdNode ** vector
)
- Given a vector of 0-1 ADDs, creates a new ADD by
substituting the 0-1 ADDs for the variables of the ADD f. There
should be an entry in vector for each variable in the manager.
This function implements non-simultaneous 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
- Defined in
cuddCompose.c
DdNode *
Cudd_addNor(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
- NOR of two 0-1 ADDs. Returns NULL
if not a terminal case; f NOR g otherwise.
- Side Effects None
- See Also
Cudd_addApply
- Defined in
cuddAddApply.c
DdNode *
Cudd_addOneZeroMaximum(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
- Returns 1 if f > g and 0 otherwise. Used in
conjunction with Cudd_addApply. Returns NULL if not a terminal
case.
- Side Effects None
- See Also
Cudd_addApply
- Defined in
cuddAddApply.c
DdNode *
Cudd_addOrAbstract(
DdManager * manager,
DdNode * f,
DdNode * cube
)
- Abstracts all the variables in cube from the 0-1 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
- Defined in
cuddAddAbs.c
DdNode *
Cudd_addOr(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
- Disjunction of two 0-1 ADDs. Returns NULL
if not a terminal case; f OR g otherwise.
- Side Effects None
- See Also
Cudd_addApply
- Defined in
cuddAddApply.c
DdNode *
Cudd_addOuterSum(
DdManager * dd,
DdNode * M,
DdNode * r,
DdNode * c
)
- Takes the pointwise minimum of a matrix and the outer
sum of two vectors. This procedure is used in the Floyd-Warshall
all-pair shortest path algorithm. Returns a pointer to the result if
successful; NULL otherwise.
- Side Effects None
- Defined in
cuddMatMult.c
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 i-th entry of permut holds the
index of the variable that is to substitute the i-th
variable. Returns a pointer to the resulting ADD if successful; NULL
otherwise.
- Side Effects None
- See Also
Cudd_bddPermute
Cudd_addSwapVariables
- Defined in
cuddCompose.c
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
- Defined in
cuddAddApply.c
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[nx-1]) encode the row index and
the y variables (y[0] ... y[ny-1]) 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
- Defined in
cuddRead.c
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 n-bit
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
- Defined in
cuddAddWalsh.c
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
- Defined in
cuddGenCof.c
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
- Defined in
cuddAddNeg.c
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
- Defined in
cuddAddInv.c
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
- Defined in
cuddAddApply.c
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
- Defined in
cuddCompose.c
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
- Defined in
cuddAddApply.c
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
- Defined in
cuddMatMult.c
DdNode *
Cudd_addTimes(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
- Integer and floating point multiplication. Returns NULL
if not a terminal case; f * g otherwise. This function can be used also
to take the AND of two 0-1 ADDs.
- Side Effects None
- See Also
Cudd_addApply
- Defined in
cuddAddApply.c
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 variables x (rows) and z (columns). g is
assumed to depend on variables 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
- Defined in
cuddMatMult.c
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
- Defined in
cuddAddAbs.c
DdNode *
Cudd_addVectorCompose(
DdManager * dd,
DdNode * f,
DdNode ** vector
)
- Given a vector of 0-1 ADDs, creates a new ADD by
substituting the 0-1 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
- Defined in
cuddCompose.c
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
- Defined in
cuddAddWalsh.c
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 N-bit numbers, x[0] x[1] ... x[N-1] and
y[0] y[1] ... y[N-1], with 0 the most significant bit.
The ADD is built bottom-up.
It has 3*N-1 internal nodes, if the variables are ordered as follows:
x[0] y[0] x[1] y[1] ... x[N-1] y[N-1].
- Side Effects None
- See Also
Cudd_Xeqy
- Defined in
cuddPriority.c
DdNode *
Cudd_addXnor(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
- XNOR of two 0-1 ADDs. Returns NULL
if not a terminal case; f XNOR g otherwise.
- Side Effects None
- See Also
Cudd_addApply
- Defined in
cuddAddApply.c
DdNode *
Cudd_addXor(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
- XOR of two 0-1 ADDs. Returns NULL
if not a terminal case; f XOR g otherwise.
- Side Effects None
- See Also
Cudd_addApply
- Defined in
cuddAddApply.c
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
- Defined in
cuddCompose.c
DdNode *
Cudd_bddAndAbstractLimit(
DdManager * manager,
DdNode * f,
DdNode * g,
DdNode * cube,
unsigned int limit
)
- 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.
In particular, if the number of new nodes created exceeds
limit
, this function returns NULL.
- Side Effects None
- See Also
Cudd_bddAndAbstract
- Defined in
cuddAndAbs.c
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
- Defined in
cuddAndAbs.c
DdNode *
Cudd_bddAndLimit(
DdManager * dd,
DdNode * f,
DdNode * g,
unsigned int limit
)
- 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 or more new nodes than
limit
are
required.
- Side Effects None
- See Also
Cudd_bddAnd
- Defined in
cuddBddIte.c
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
- Defined in
cuddBddIte.c
int
Cudd_bddApproxConjDecomp(
DdManager * dd, manager
DdNode * f, function to be decomposed
DdNode *** conjuncts address of the first factor
)
- Performs two-way 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
- Defined in
cuddDecomp.c
int
Cudd_bddApproxDisjDecomp(
DdManager * dd, manager
DdNode * f, function to be decomposed
DdNode *** disjuncts address of the array of the disjuncts
)
- Performs two-way 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
- Defined in
cuddDecomp.c
int
Cudd_bddBindVar(
DdManager * dd, manager
int index variable index
)
- This function sets a flag to prevent sifting of a
variable. Returns 1 if successful; 0 otherwise (i.e., invalid
variable index).
- Side Effects Changes the "bindVar" flag in DdSubtable.
- See Also
Cudd_bddUnbindVar
- Defined in
cuddAPI.c
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
- Defined in
cuddBddAbs.c
DdNode **
Cudd_bddCharToVect(
DdManager * dd,
DdNode * f
)
- Computes a vector of BDDs whose image equals a non-zero
function.
The result depends on the variable order. The i-th 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 char-to-vect 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
- Defined in
cuddGenCof.c
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
- Defined in
cuddClip.c
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
- Defined in
cuddClip.c
DdNode *
Cudd_bddClosestCube(
DdManager * dd,
DdNode * f,
DdNode * g,
int * distance
)
- Finds a cube of f at minimum Hamming distance from the
minterms of g. All the minterms of the cube are at the minimum
distance. If the distance is 0, the cube belongs to the
intersection of f and g. Returns the cube if successful; NULL
otherwise.
- Side Effects The distance is returned as a side effect.
- See Also
Cudd_MinHammingDist
- Defined in
cuddPriority.c
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
- Defined in
cuddCompose.c
DdNode *
Cudd_bddComputeCube(
DdManager * dd,
DdNode ** vars,
int * phase,
int n
)
- Computes the cube of an array of BDD variables. If
non-null, 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
Cudd_CubeArrayToBdd
- Defined in
cuddUtil.c
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
- Defined in
cuddGenCof.c
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. Note that if
F=(f1,...,fn) and reordering takes place while computing F @ c, then the
image restriction property (Img(F,c) = Img(F @ c)) is lost.
- Side Effects None
- See Also
Cudd_bddRestrict
Cudd_addConstrain
- Defined in
cuddGenCof.c
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 i-th 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
- Defined in
cuddBddCorr.c
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 ON-set 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
- Defined in
cuddBddCorr.c
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
- Defined in
cuddBddAbs.c
int
Cudd_bddGenConjDecomp(
DdManager * dd, manager
DdNode * f, function to be decomposed
DdNode *** conjuncts address of the array of conjuncts
)
- Performs two-way 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
- Defined in
cuddDecomp.c
int
Cudd_bddGenDisjDecomp(
DdManager * dd, manager
DdNode * f, function to be decomposed
DdNode *** disjuncts address of the array of the disjuncts
)
- Performs two-way 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
- Defined in
cuddDecomp.c
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
- Defined in
cuddBddIte.c
DdNode *
Cudd_bddInterval(
DdManager * dd, DD manager
int N, number of x variables
DdNode ** x, array of x variables
unsigned int lowerB, lower bound
unsigned int upperB upper bound
)
- This function generates a BDD for the function
lowerB ≤ x ≤ upperB, where x is an N-bit number,
x[0] x[1] ... x[N-1], with 0 the most significant bit (important!).
The number of variables N should be sufficient to represent the bounds;
otherwise, the bounds are truncated to their N least significant bits.
Two BDDs are built bottom-up for lowerB ≤ x and x ≤ upperB, and they
are finally conjoined.
- Side Effects None
- See Also
Cudd_Xgty
- Defined in
cuddPriority.c
int
Cudd_bddIsNsVar(
DdManager * dd,
int index
)
- Checks whether a variable is next state. Returns 1 if
the variable's type is present state; 0 if the variable exists but is
not a present state; -1 if the variable does not exist.
- Side Effects none
- See Also
Cudd_bddSetNsVar
Cudd_bddIsPiVar
Cudd_bddIsPsVar
- Defined in
cuddAPI.c
int
Cudd_bddIsPiVar(
DdManager * dd, manager
int index variable index
)
- Checks whether a variable is primary input. Returns 1 if
the variable's type is primary input; 0 if the variable exists but is
not a primary input; -1 if the variable does not exist.
- Side Effects none
- See Also
Cudd_bddSetPiVar
Cudd_bddIsPsVar
Cudd_bddIsNsVar
- Defined in
cuddAPI.c
int
Cudd_bddIsPsVar(
DdManager * dd,
int index
)
- Checks whether a variable is present state. Returns 1 if
the variable's type is present state; 0 if the variable exists but is
not a present state; -1 if the variable does not exist.
- Side Effects none
- See Also
Cudd_bddSetPsVar
Cudd_bddIsPiVar
Cudd_bddIsNsVar
- Defined in
cuddAPI.c
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
- Defined in
cuddEssent.c
int
Cudd_bddIsVarHardGroup(
DdManager * dd,
int index
)
- Checks whether a variable is set to be in a hard group. This
function is used for lazy sifting. Returns 1 if the variable is marked
to be in a hard group; 0 if the variable exists, but it is not marked to be
in a hard group; -1 if the variable does not exist.
- Side Effects none
- See Also
Cudd_bddSetVarHardGroup
- Defined in
cuddAPI.c
int
Cudd_bddIsVarToBeGrouped(
DdManager * dd,
int index
)
- Checks whether a variable is set to be grouped. This
function is used for lazy sifting.
- Side Effects none
- Defined in
cuddAPI.c
int
Cudd_bddIsVarToBeUngrouped(
DdManager * dd,
int index
)
- Checks whether a variable is set to be ungrouped. This
function is used for lazy sifting. Returns 1 if the variable is marked
to be ungrouped; 0 if the variable exists, but it is not marked to be
ungrouped; -1 if the variable does not exist.
- Side Effects none
- See Also
Cudd_bddSetVarToBeUngrouped
- Defined in
cuddAPI.c
DdNode *
Cudd_bddIsop(
DdManager * dd,
DdNode * L,
DdNode * U
)
- Computes a BDD in the interval between L and U with a
simple sum-of-produuct 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
- Defined in
cuddZddIsop.c
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
- Defined in
cuddBddIte.c
int
Cudd_bddIterConjDecomp(
DdManager * dd, manager
DdNode * f, function to be decomposed
DdNode *** conjuncts address of the array of conjuncts
)
- Performs two-way 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
- Defined in
cuddDecomp.c
int
Cudd_bddIterDisjDecomp(
DdManager * dd, manager
DdNode * f, function to be decomposed
DdNode *** disjuncts address of the array of the disjuncts
)
- Performs two-way 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
- Defined in
cuddDecomp.c
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
- Defined in
cuddBddIte.c
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
Cudd_ReadVars
- Defined in
cuddAPI.c
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
- Defined in
cuddGenCof.c
int
Cudd_bddLeqUnless(
DdManager * dd,
DdNode * f,
DdNode * g,
DdNode * D
)
- Tells whether f is less than of equal to G unless D is
1. f, g, and D are BDDs. The function returns 1 if f is less than
of equal to G, and 0 otherwise. No new nodes are created.
- Side Effects None
- See Also
Cudd_EquivDC
Cudd_bddLeq
Cudd_bddIteConstant
- Defined in
cuddSat.c
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
- Defined in
cuddBddIte.c
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
- Defined in
cuddLiteral.c
DdNode *
Cudd_bddMakePrime(
DdManager * dd, manager
DdNode * cube, cube to be expanded
DdNode * f function of which the cube is to be made a prime
)
- Expands cube to a prime implicant of f. Returns the prime
if successful; NULL otherwise. In particular, NULL is returned if cube
is not a real cube or is not an implicant of f.
- Side Effects None
- Defined in
cuddSat.c
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
- Defined in
cuddGenCof.c
DdNode *
Cudd_bddNPAnd(
DdManager * dd,
DdNode * f,
DdNode * g
)
- Computes f non-polluting-and g. The non-polluting AND
of f and g is a hybrid of AND and Restrict. From Restrict, this
operation takes the idea of existentially quantifying the top
variable of the second operand if it does not appear in the first.
Therefore, the variables that appear in the result also appear in f.
For the rest, the function behaves like AND. Since the two operands
play different roles, non-polluting AND is not commutative.
Returns a pointer to the result if successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_bddConstrain
Cudd_bddRestrict
- Defined in
cuddGenCof.c
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
- Defined in
cuddBddIte.c
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
- Defined in
cuddAPI.c
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
- Defined in
cuddAPI.c
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
- Defined in
cuddBddIte.c
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
- Defined in
cuddBddIte.c
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 i-th entry of permut holds the
index of the variable that is to substitute the i-th variable.
Returns a pointer to the resulting BDD if successful; NULL
otherwise.
- Side Effects None
- See Also
Cudd_addPermute
Cudd_bddSwapVariables
- Defined in
cuddCompose.c
DdNode **
Cudd_bddPickArbitraryMinterms(
DdManager * dd, manager
DdNode * f, function from which to pick k minterms
DdNode ** vars, array of variables
int n, size of vars
int k number of minterms to find
)
- Picks k on-set 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 an array of BDDs 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
- Defined in
cuddUtil.c
int
Cudd_bddPickOneCube(
DdManager * ddm,
DdNode * node,
char * string
)
- Picks one on-set 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
- Defined in
cuddUtil.c
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 on-set 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
- Defined in
cuddUtil.c
int
Cudd_bddPrintCover(
DdManager * dd,
DdNode * l,
DdNode * u
)
- Prints a sum of product cover for an incompletely
specified function given by a lower bound and an upper bound. Each
product is a prime implicant obtained by expanding the product
corresponding to a path from node to the constant one. Uses the
package default output file. Returns 1 if successful; 0 otherwise.
- Side Effects None
- See Also
Cudd_PrintMinterm
- Defined in
cuddUtil.c
int
Cudd_bddReadPairIndex(
DdManager * dd,
int index
)
- Reads a corresponding pair index for a given index.
These pair indices are present and next state variable. Returns the
corresponding variable index if the variable exists; -1 otherwise.
- Side Effects modifies the manager
- See Also
Cudd_bddSetPairIndex
- Defined in
cuddAPI.c
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[nx-1]) encode
the row index and the y variables (y[0] ... y[ny-1]) 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
- Defined in
cuddRead.c
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
- Defined in
cuddAPI.c
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)*i-1
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
- Defined in
cuddAPI.c
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
- Defined in
cuddAPI.c
int
Cudd_bddResetVarToBeGrouped(
DdManager * dd,
int index
)
- Resets a variable not to be grouped. This function is
used for lazy sifting. Returns 1 if successful; 0 otherwise.
- Side Effects modifies the manager
- See Also
Cudd_bddSetVarToBeGrouped
Cudd_bddSetVarHardGroup
- Defined in
cuddAPI.c
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
- Defined in
cuddGenCof.c
int
Cudd_bddSetNsVar(
DdManager * dd, manager
int index variable index
)
- Sets a variable type to next state. The variable type is
used by lazy sifting. Returns 1 if successful; 0 otherwise.
- Side Effects modifies the manager
- See Also
Cudd_bddSetPiVar
Cudd_bddSetPsVar
Cudd_bddIsNsVar
- Defined in
cuddAPI.c
int
Cudd_bddSetPairIndex(
DdManager * dd, manager
int index, variable index
int pairIndex corresponding variable index
)
- Sets a corresponding pair index for a given index.
These pair indices are present and next state variable. Returns 1 if
successful; 0 otherwise.
- Side Effects modifies the manager
- See Also
Cudd_bddReadPairIndex
- Defined in
cuddAPI.c
int
Cudd_bddSetPiVar(
DdManager * dd, manager
int index variable index
)
- Sets a variable type to primary input. The variable type is
used by lazy sifting. Returns 1 if successful; 0 otherwise.
- Side Effects modifies the manager
- See Also
Cudd_bddSetPsVar
Cudd_bddSetNsVar
Cudd_bddIsPiVar
- Defined in
cuddAPI.c
int
Cudd_bddSetPsVar(
DdManager * dd, manager
int index variable index
)
- Sets a variable type to present state. The variable type is
used by lazy sifting. Returns 1 if successful; 0 otherwise.
- Side Effects modifies the manager
- See Also
Cudd_bddSetPiVar
Cudd_bddSetNsVar
Cudd_bddIsPsVar
- Defined in
cuddAPI.c
int
Cudd_bddSetVarHardGroup(
DdManager * dd,
int index
)
- Sets a variable to be a hard group. This function is used
for lazy sifting. Returns 1 if successful; 0 otherwise.
- Side Effects modifies the manager
- See Also
Cudd_bddSetVarToBeGrouped
Cudd_bddResetVarToBeGrouped
Cudd_bddIsVarHardGroup
- Defined in
cuddAPI.c
int
Cudd_bddSetVarToBeGrouped(
DdManager * dd,
int index
)
- Sets a variable to be grouped. This function is used for
lazy sifting. Returns 1 if successful; 0 otherwise.
- Side Effects modifies the manager
- See Also
Cudd_bddSetVarHardGroup
Cudd_bddResetVarToBeGrouped
- Defined in
cuddAPI.c
int
Cudd_bddSetVarToBeUngrouped(
DdManager * dd,
int index
)
- Sets a variable to be ungrouped. This function is used
for lazy sifting. Returns 1 if successful; 0 otherwise.
- Side Effects modifies the manager
- See Also
Cudd_bddIsVarToBeUngrouped
- Defined in
cuddAPI.c
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
- Defined in
cuddGenCof.c
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
- Defined in
cuddCompose.c
DdNode *
Cudd_bddTransfer(
DdManager * ddSource,
DdManager * ddDestination,
DdNode * f
)
- Convert a BDD from a manager to another one. The orders of the
variables in the two managers may be different. Returns a
pointer to the BDD in the destination manager if successful; NULL
otherwise.
- Side Effects None
- Defined in
cuddBridge.c
int
Cudd_bddUnbindVar(
DdManager * dd, manager
int index variable index
)
- This function resets the flag that prevents the sifting
of a variable. In successive variable reorderings, the variable will
NOT be skipped, that is, sifted. Initially all variables can be
sifted. It is necessary to call this function only to re-enable
sifting after a call to Cudd_bddBindVar. Returns 1 if successful; 0
otherwise (i.e., invalid variable index).
- Side Effects Changes the "bindVar" flag in DdSubtable.
- See Also
Cudd_bddBindVar
- Defined in
cuddAPI.c
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
- Defined in
cuddBddAbs.c
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
- Defined in
cuddDecomp.c
int
Cudd_bddVarDisjDecomp(
DdManager * dd, manager
DdNode * f, function to be decomposed
DdNode *** disjuncts address of the array of the disjuncts
)
- Performs two-way 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
- Defined in
cuddDecomp.c
int
Cudd_bddVarIsBound(
DdManager * dd, manager
int index variable index
)
- This function returns 1 if a variable is enabled for
sifting. Initially all variables can be sifted. This function returns
0 only if there has been a previous call to Cudd_bddBindVar for that
variable not followed by a call to Cudd_bddUnbindVar. The function returns
0 also in the case in which the index of the variable is out of bounds.
- Side Effects none
- See Also
Cudd_bddBindVar
Cudd_bddUnbindVar
- Defined in
cuddAPI.c
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
- Defined in
cuddBddAbs.c
DdNode *
Cudd_bddVarMap(
DdManager * manager, DD manager
DdNode * f function in which to remap variables
)
- Remaps the variables of a BDD using the default
variable map. A typical use of this function is to swap two sets of
variables. The variable map must be registered with Cudd_SetVarMap.
Returns a pointer to the resulting BDD if successful; NULL
otherwise.
- Side Effects None
- See Also
Cudd_bddPermute
Cudd_bddSwapVariables
Cudd_SetVarMap
- Defined in
cuddCompose.c
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
- Defined in
cuddCompose.c
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
- Defined in
cuddBddIte.c
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
- Defined in
cuddBddAbs.c
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
- Defined in
cuddBddIte.c
void
Cudd_tlcInfoFree(
DdTlcInfo * t
)
- Frees a DdTlcInfo Structure as well as the memory pointed
by it.
- Side Effects None
- Defined in
cuddEssent.c
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
- Defined in
cuddZddSetop.c
DdNode *
Cudd_zddComplement(
DdManager * dd,
DdNode * node
)
- Computes a complement cover for a ZDD node. For lack of a
better method, we first extract the function BDD from the ZDD cover,
then make the complement of the ZDD cover from the complement of the
BDD node by using ISOP. Returns a pointer to the resulting cover if
successful; NULL otherwise. The result depends on current variable
order.
- Side Effects The result depends on current variable order.
- Defined in
cuddZddFuncs.c
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 (double) CUDD_OUT_OF_MEM. This procedure is used in
Cudd_zddCountMinterm.
- Side Effects None
- See Also
Cudd_zddCountMinterm
Cudd_zddCount
- Defined in
cuddZddCount.c
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. If the procedure runs out of memory, it
returns (double) CUDD_OUT_OF_MEM.
- Side Effects None
- See Also
Cudd_zddCountDouble
- Defined in
cuddZddMisc.c
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
- Defined in
cuddZddCount.c
char *
Cudd_zddCoverPathToString(
DdManager * zdd, DD manager
int * path, path of ZDD representing a cover
char * str pointer to string to use if != NULL
)
- Converts a path of a ZDD representing a cover to a
string. The string represents an implicant of the cover. The path
is typically produced by Cudd_zddForeachPath. Returns a pointer to
the string if successful; NULL otherwise. If the str input is NULL,
it allocates a new string. The string passed to this function must
have enough room for all variables and for the terminator.
- Side Effects None
- See Also
Cudd_zddForeachPath
- Defined in
cuddZddUtil.c
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
- Defined in
cuddZddMisc.c
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
- Defined in
cuddZddSetop.c
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
- Defined in
cuddZddSetop.c
DdNode *
Cudd_zddDivideF(
DdManager * dd,
DdNode * f,
DdNode * g
)
- Modified version of Cudd_zddDivide. This function may
disappear in future releases.
- Side Effects None
- Defined in
cuddZddFuncs.c
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
- Defined in
cuddZddFuncs.c
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., out-of-memory,
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 non-null, 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 letter-size
sheet.
- Side Effects None
- See Also
Cudd_DumpDot
Cudd_zddPrintDebug
- Defined in
cuddZddUtil.c
DdGen *
Cudd_zddFirstPath(
DdManager * zdd,
DdNode * f,
int ** path
)
- Defines an iterator on the paths of a ZDD
and finds its first path. Returns a generator that contains the
information necessary to continue the enumeration if successful; NULL
otherwise.
A path is represented as an array of literals, which are integers in
{0, 1, 2}; 0 represents an else arc out of a node, 1 represents a then arc
out of a node, and 2 stands for the absence of a node.
The size of the array equals the number of variables in the manager at
the time Cudd_zddFirstCube is called.
The paths that end in the empty terminal are not enumerated.
- Side Effects The first path is returned as a side effect.
- See Also
Cudd_zddForeachPath
Cudd_zddNextPath
Cudd_GenFree
Cudd_IsGenEmpty
- Defined in
cuddZddUtil.c
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
- Defined in
cuddZddSetop.c
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
- Defined in
cuddZddIsop.c
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
- Defined in
cuddZddSetop.c
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
- Defined in
cuddAPI.c
int
Cudd_zddNextPath(
DdGen * gen,
int ** path
)
- Generates the next path of a ZDD onset,
using generator gen. Returns 0 if the enumeration is completed; 1
otherwise.
- Side Effects The path is returned as a side effect. The
generator is modified.
- See Also
Cudd_zddForeachPath
Cudd_zddFirstPath
Cudd_GenFree
Cudd_IsGenEmpty
- Defined in
cuddZddUtil.c
DdNode *
Cudd_zddPortFromBdd(
DdManager * dd,
DdNode * B
)
- Converts a BDD into a ZDD. This function assumes that
there is a one-to-one 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
- Defined in
cuddZddPort.c
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
- Defined in
cuddZddPort.c
int
Cudd_zddPrintCover(
DdManager * zdd,
DdNode * node
)
- Prints a sum of products from a ZDD representing a cover.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- See Also
Cudd_zddPrintMinterm
- Defined in
cuddZddUtil.c
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 products
- pr = 3 : prints counts + list of nodes
- pr > 3 : prints counts + disjoint sum of products + list of nodes
Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddZddUtil.c
int
Cudd_zddPrintMinterm(
DdManager * zdd,
DdNode * node
)
- Prints a disjoint sum of product form for a ZDD. Returns 1
if successful; 0 otherwise.
- Side Effects None
- See Also
Cudd_zddPrintDebug
Cudd_zddPrintCover
- Defined in
cuddZddUtil.c
void
Cudd_zddPrintSubtable(
DdManager * table
)
- Prints the ZDD table for debugging purposes.
- Side Effects None
- Defined in
cuddZddMisc.c
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
- Defined in
cuddZddFuncs.c
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
- Defined in
cuddAPI.c
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
- Defined in
cuddAPI.c
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)*i-1
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
- Defined in
cuddAPI.c
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
- Defined in
cuddAPI.c
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.
- Defined in
cuddZddReord.c
int
Cudd_zddShuffleHeap(
DdManager * table, DD manager
int * permutation required variable permutation
)
- Reorders ZDD variables according to given permutation.
The i-th entry of the permutation array contains the index of the variable
that should be brought to the i-th 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
- Defined in
cuddZddReord.c
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
- Defined in
cuddZddSetop.c
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
- Defined in
cuddZddSetop.c
void
Cudd_zddSymmProfile(
DdManager * table,
int lower,
int upper
)
- Prints statistics on symmetric ZDD variables.
- Side Effects None
- Defined in
cuddZddSymm.c
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
- Defined in
cuddZddFuncs.c
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
- Defined in
cuddZddSetop.c
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
- Defined in
cuddAPI.c
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
- Defined in
cuddZddFuncs.c
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
- Defined in
cuddZddFuncs.c
static enum st_retval
MarkCacheCleanUp(
char * key,
char * value,
char * arg
)
- Frees memory associated with computed table of
cuddBddLICMarkEdges. Returns ST_CONTINUE.
- Side Effects None
- See Also
Cudd_bddLICompaction
- Defined in
cuddGenCof.c
static int
MarkCacheCompare(
const char * ptr1,
const char * ptr2
)
- Comparison function for the computed table of
cuddBddLICMarkEdges. Returns 0 if the two nodes of the key are equal; 1
otherwise.
- Side Effects None
- See Also
Cudd_bddLICompaction
- Defined in
cuddGenCof.c
static int
MarkCacheHash(
char * ptr,
int modulus
)
- Hash function for the computed table of
cuddBddLICMarkEdges. Returns the bucket number.
- Side Effects None
- See Also
Cudd_bddLICompaction
- Defined in
cuddGenCof.c
static int
PMX(
int maxvar
)
- Performs the crossover between two randomly chosen
parents, and creates two children, x1 and x2. Uses the Partially
Matched Crossover operator.
- Side Effects None
- Defined in
cuddGenetic.c
static int
PairInTables(
DdNode * g,
DdNode * h,
st_table * ghTable
)
- .Check whether the given pair is in the tables. gTable
and hTable are combined.
absence in both is indicated by 0,
presence in gTable is indicated by 1,
presence in hTable by 2 and
presence in both by 3.
The values returned by this function are PAIR_ST,
PAIR_CR, G_ST, G_CR, H_ST, H_CR, BOTH_G, BOTH_H, NONE.
PAIR_ST implies g in gTable and h in hTable
PAIR_CR implies g in hTable and h in gTable
G_ST implies g in gTable and h not in any table
G_CR implies g in hTable and h not in any table
H_ST implies h in hTable and g not in any table
H_CR implies h in gTable and g not in any table
BOTH_G implies both in gTable
BOTH_H implies both in hTable
NONE implies none in table;
- See Also
CheckTablesCacheAndReturn
CheckInTables
- Defined in
cuddDecomp.c
static Conjuncts *
PickOnePair(
DdNode * node,
DdNode * g1,
DdNode * h1,
DdNode * g2,
DdNode * h2,
st_table * ghTable,
st_table * cacheTable
)
- Check the tables for the existence of pair and return
one combination, store in cache. The pair that has more pointers to
it is picked. An approximation of the number of local pointers is
made by taking the reference count of the pairs sent.
- See Also
ZeroCase
BuildConjuncts
- Defined in
cuddDecomp.c
static DdNode *
RAbuildSubset(
DdManager * dd, DD manager
DdNode * node, current node
ApproxInfo * info node info
)
- Builds the subset BDDfor cuddRemapUnderApprox. Based
on the info table, performs remapping or replacement at selected
nodes. Returns a pointer to the result if successful; NULL
otherwise.
- Side Effects None
- See Also
cuddRemapUnderApprox
- Defined in
cuddApprox.c
static int
RAmarkNodes(
DdManager * dd, manager
DdNode * f, function to be analyzed
ApproxInfo * info, info on BDD
int threshold, when to stop approximating
double quality minimum improvement for accepted changes
)
- Marks nodes for remapping. Returns 1 if successful; 0
otherwise.
- Side Effects None
- See Also
cuddRemapUnderApprox
- Defined in
cuddApprox.c
static void
ResizeCountMintermPages(
)
- Resize the number of pages allocated to store the minterm
counts. The procedure moves the counter to the next page when the
end of the page is reached and allocates new pages when necessary.
- Side Effects Changes the size of minterm pages, page, page index, maximum
number of pages freeing stuff in case of memory out.
- Defined in
cuddSubsetHB.c
static void
ResizeCountNodePages(
)
- Resize the number of pages allocated to store the node counts.
The procedure moves the counter to the next page when the end of
the page is reached and allocates new pages when necessary.
- Side Effects Changes the size of pages, page, page index, maximum
number of pages freeing stuff in case of memory out.
- Defined in
cuddSubsetHB.c
static void
ResizeNodeDataPages(
)
- Resize the number of pages allocated to store the node data
The procedure moves the counter to the next page when the end of
the page is reached and allocates new pages when necessary.
- Side Effects Changes the size of pages, page, page index, maximum
number of pages freeing stuff in case of memory out.
- Defined in
cuddSubsetHB.c
static void
ResizeNodeDistPages(
)
- Resize the number of pages allocated to store the distances
related to each node. The procedure moves the counter to the
next page when the end of the page is reached and allocates new
pages when necessary.
- Side Effects Changes the size of pages, page, page index, maximum
number of pages freeing stuff in case of memory out.
- Defined in
cuddSubsetSP.c
static void
ResizeQueuePages(
)
- Resize the number of pages allocated to store nodes in the BFS
traversal of the Bdd. The procedure moves the counter to the
next page when the end of the page is reached and allocates new
pages when necessary.
- Side Effects Changes the size of pages, page, page index, maximum
number of pages freeing stuff in case of memory out.
- Defined in
cuddSubsetSP.c
static void
StoreNodes(
st_table * storeTable,
DdManager * dd,
DdNode * node
)
- rocedure to recursively store nodes that are retained in the subset.
- Side Effects None
- See Also
StoreNodes
- Defined in
cuddSubsetHB.c
static double
SubsetCountMintermAux(
DdNode * node, function to analyze
double max, number of minterms of constant 1
st_table * table visitedTable table
)
- Recursively counts minterms of each node in the DAG.
Similar to the cuddCountMintermAux which recursively counts the
number of minterms for the dag rooted at each node in terms of the
total number of variables (max). This procedure creates the node
data structure and stores the minterm count as part of the node
data structure.
- Side Effects Creates structures of type node quality and fills the st_table
- See Also
SubsetCountMinterm
- Defined in
cuddSubsetHB.c
static st_table *
SubsetCountMinterm(
DdNode * node, function to be analyzed
int nvars number of variables node depends on
)
- Counts minterms of each node in the DAG. Similar to the
Cudd_CountMinterm procedure except this returns the minterm count for
all the nodes in the bdd in an st_table.
- Side Effects none
- See Also
SubsetCountMintermAux
- Defined in
cuddSubsetHB.c
static int
SubsetCountNodesAux(
DdNode * node, current node
st_table * table, table to update node count, also serves as visited table.
double max maximum number of variables
)
- Recursively counts the number of nodes under the dag.
Also counts the number of nodes under the lighter child of
this node. . Note that the same dag may be the lighter child of two
different nodes and have different counts. As with the minterm counts,
the node counts are stored in pages to be space efficient and the
address for these node counts are stored in an st_table associated
to each node.
- Side Effects Updates the node data table with node counts
- See Also
SubsetCountNodes
- Defined in
cuddSubsetHB.c
static int
SubsetCountNodes(
DdNode * node, function to be analyzed
st_table * table, node quality table
int nvars number of variables node depends on
)
- Counts the nodes under the current node and its lighter
child. Calls a recursive procedure to count the number of nodes of
a DAG rooted at a particular node and the number of nodes taken by its
lighter child.
- Side Effects None
- See Also
SubsetCountNodesAux
- Defined in
cuddSubsetHB.c
static DdNode *
UAbuildSubset(
DdManager * dd, DD manager
DdNode * node, current node
ApproxInfo * info node info
)
- Builds the subset BDD. Based on the info table,
replaces selected nodes by zero. Returns a pointer to the result if
successful; NULL otherwise.
- Side Effects None
- See Also
cuddUnderApprox
- Defined in
cuddApprox.c
static int
UAmarkNodes(
DdManager * dd, manager
DdNode * f, function to be analyzed
ApproxInfo * info, info on BDD
int threshold, when to stop approximating
int safe, enforce safe approximation
double quality minimum improvement for accepted changes
)
- Marks nodes for replacement by zero. Returns 1 if successful;
0 otherwise.
- Side Effects None
- See Also
cuddUnderApprox
- Defined in
cuddApprox.c
static Conjuncts *
ZeroCase(
DdManager * dd,
DdNode * node,
Conjuncts * factorsNv,
st_table * ghTable,
st_table * cacheTable,
int switched
)
- If one child is zero, do explicitly what Restrict does or better.
First separate a variable and its child in the base case. In case of a cube
times a function, separate the cube and function. As a last resort, look in
tables.
- Side Effects Frees the BDDs in factorsNv. factorsNv itself is not freed
because it is freed above.
- See Also
BuildConjuncts
- Defined in
cuddDecomp.c
static DdNode *
addBddDoInterval(
DdManager * dd,
DdNode * f,
DdNode * l,
DdNode * u
)
- Performs the recursive step for Cudd_addBddInterval.
Returns a pointer to the BDD if successful; NULL otherwise.
- Side Effects None
- See Also
addBddDoThreshold
addBddDoStrictThreshold
- Defined in
cuddBridge.c
static DdNode *
addBddDoIthBit(
DdManager * dd,
DdNode * f,
DdNode * index
)
- Performs the recursive step for Cudd_addBddIthBit.
Returns a pointer to the BDD if successful; NULL otherwise.
- Side Effects None
- Defined in
cuddBridge.c
static DdNode *
addBddDoStrictThreshold(
DdManager * dd,
DdNode * f,
DdNode * val
)
- Performs the recursive step for Cudd_addBddStrictThreshold.
Returns a pointer to the BDD if successful; NULL otherwise.
- Side Effects None
- See Also
addBddDoThreshold
- Defined in
cuddBridge.c
static DdNode *
addBddDoThreshold(
DdManager * dd,
DdNode * f,
DdNode * val
)
- Performs the recursive step for Cudd_addBddThreshold.
Returns a pointer to the BDD if successful; NULL otherwise.
- Side Effects None
- See Also
addBddDoStrictThreshold
- Defined in
cuddBridge.c
static int
addCheckPositiveCube(
DdManager * manager,
DdNode * cube
)
- Checks whether cube is an ADD representing the product of
positive literals. Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddAddAbs.c
static DdNode *
addDoIthBit(
DdManager * dd,
DdNode * f,
DdNode * index
)
- Performs the recursive step for Cudd_addIthBit.
Returns a pointer to the BDD if successful; NULL otherwise.
- Side Effects None
- Defined in
cuddAddFind.c
static DdNode *
addMMRecur(
DdManager * dd,
DdNode * A,
DdNode * B,
int topP,
int * vars
)
- Performs the recursive step of Cudd_addMatrixMultiply.
Returns a pointer to the result if successful; NULL otherwise.
- Side Effects None
- Defined in
cuddMatMult.c
static int
addMultiplicityGroups(
DdManager * dd, manager
MtrNode * treenode, current tree node
int multiplicity, how many ZDD vars per BDD var
char * vmask, variable pairs for which a group has been already built
char * lmask levels for which a group has already been built
)
- Adds multiplicity groups to a ZDD variable group tree.
Returns 1 if successful; 0 otherwise. This function creates the groups
for set of ZDD variables (whose cardinality is given by parameter
multiplicity) that are created for each BDD variable in
Cudd_zddVarsFromBddVars. The crux of the matter is to determine the index
each new group. (The index of the first variable in the group.)
We first build all the groups for the children of a node, and then deal
with the ZDD variables that are directly attached to the node. The problem
for these is that the tree itself does not provide information on their
position inside the group. While we deal with the children of the node,
therefore, we keep track of all the positions they occupy. The remaining
positions in the tree can be freely used. Also, we keep track of all the
variables placed in the children. All the remaining variables are directly
attached to the group. We can then place any pair of variables not yet
grouped in any pair of available positions in the node.
- Side Effects Changes the variable group tree.
- See Also
Cudd_zddVarsFromBddVars
- Defined in
cuddAPI.c
static DdNode *
addTriangleRecur(
DdManager * dd,
DdNode * f,
DdNode * g,
int * vars,
DdNode * cube
)
- Performs the recursive step of Cudd_addTriangle. Returns
a pointer to the result if successful; NULL otherwise.
- Side Effects None
- Defined in
cuddMatMult.c
static void
addVarToConst(
DdNode * f,
DdNode ** gp,
DdNode ** hp,
DdNode * one,
DdNode * zero
)
- Replaces variables with constants if possible (part of
canonical form).
- Side Effects None
- Defined in
cuddAddIte.c
static DdNode *
addWalshInt(
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
- Defined in
cuddAddWalsh.c
static int
array_compare(
const char * array1,
const char * array2
)
- Comparison function for the computed table. Returns 0 if
the two arrays are equal; 1 otherwise.
- Side Effects None
- Defined in
cuddGenetic.c
static int
array_hash(
char * array,
int modulus
)
- Hash function for the computed table. Returns the bucket
number.
- Side Effects None
- Defined in
cuddGenetic.c
static double
bddAnnotateMintermCount(
DdManager * manager,
DdNode * node,
double max,
st_table * table
)
- Annotates every node in the BDD node with its minterm count.
In this function, every node and the minterm count represented by it are
stored in a hash table.
- Side Effects Fills up 'table' with the pair .
- Defined in
cuddSplit.c
static int
bddCheckPositiveCube(
DdManager * manager,
DdNode * cube
)
- Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddBddAbs.c
static double
bddCorrelationAux(
DdManager * dd,
DdNode * f,
DdNode * g,
st_table * table
)
- Performs the recursive step of Cudd_bddCorrelation.
Returns the fraction of minterms in the ON-set of the EXNOR of f and
g.
- Side Effects None
- See Also
bddCorrelationWeightsAux
- Defined in
cuddBddCorr.c
static double
bddCorrelationWeightsAux(
DdManager * dd,
DdNode * f,
DdNode * g,
double * prob,
st_table * table
)
- Performs the recursive step of Cudd_bddCorrelationWeigths.
- Side Effects None
- See Also
bddCorrelationAux
- Defined in
cuddBddCorr.c
static void
bddFixTree(
DdManager * table,
MtrNode * treenode
)
- Fixes the BDD variable group tree after a
shuffle. Assumes that the order of the variables in a terminal node
has not been changed.
- Side Effects Changes the BDD variable group tree.
- Defined in
cuddReorder.c
static int
bddVarToCanonicalSimple(
DdManager * dd,
DdNode ** fp,
DdNode ** gp,
DdNode ** hp,
unsigned int * topfp,
unsigned int * topgp,
unsigned int * tophp
)
- Makes sure the first two pointers are regular. This
mat require the complementation of the result, which is signaled by
returning 1 instead of 0. This function is simpler than the general
case because it assumes that no two arguments are the same or
complementary, and no argument is constant.
- Side Effects None
- See Also
bddVarToConst
bddVarToCanonical
- Defined in
cuddBddIte.c
static int
bddVarToCanonical(
DdManager * dd,
DdNode ** fp,
DdNode ** gp,
DdNode ** hp,
unsigned int * topfp,
unsigned int * topgp,
unsigned int * tophp
)
- Reduces 2 variable expressions to canonical form.
- Side Effects None
- See Also
bddVarToConst
bddVarToCanonicalSimple
- Defined in
cuddBddIte.c
static void
bddVarToConst(
DdNode * f,
DdNode ** gp,
DdNode ** hp,
DdNode * one
)
- This function performs part of the transformation to
standard form by replacing variables with constants if possible.
- Side Effects None
- See Also
bddVarToCanonical
bddVarToCanonicalSimple
- Defined in
cuddBddIte.c
static int
beforep(
DdHalfWord var1a,
short phase1a,
DdHalfWord var1b,
short phase1b,
DdHalfWord var2a,
short phase2a,
DdHalfWord var2b,
short phase2b
)
- Returns true iff the first argument precedes the second
in the clause order. A clause precedes another if its first lieral
precedes the first literal of the other, or if the first literals
are the same, and its second literal precedes the second literal of
the other clause. A literal precedes another if it has a higher
index, of if it has the same index, but it has lower phase. Phase 0
is the positive phase, and it is lower than Phase 1 (negative
phase).
- Side Effects None
- See Also
equalp
- Defined in
cuddEssent.c
static BitVector *
bitVectorAlloc(
int size
)
- Allocates a bit vector. The parameter size gives the
number of bits. This procedure allocates enough long's to hold the
specified number of bits. Returns a pointer to the allocated vector
if successful; NULL otherwise.
- Side Effects None
- See Also
bitVectorClear
bitVectorFree
- Defined in
cuddEssent.c
static void
bitVectorClear(
BitVector * vector,
int size
)
- Clears a bit vector. The parameter size gives the
number of bits.
- Side Effects None
- See Also
bitVectorAlloc
- Defined in
cuddEssent.c
static void
bitVectorFree(
BitVector * vector
)
- Frees a bit vector.
- Side Effects None
- See Also
bitVectorAlloc
- Defined in
cuddEssent.c
static short
bitVectorRead(
BitVector * vector,
int i
)
- Returns the i-th entry of a bit vector.
- Side Effects None
- See Also
bitVectorSet
- Defined in
cuddEssent.c
static void
bitVectorSet(
BitVector * vector,
int i,
short val
)
- Sets the i-th entry of a bit vector to a value.
- Side Effects None
- See Also
bitVectorRead
- Defined in
cuddEssent.c
static int
build_dd(
DdManager * table,
int num, the index of the individual to be built
int lower,
int upper
)
- Builds a DD from a given order. This procedure also
sifts the final order and inserts into the array the size in nodes
of the result. Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddGenetic.c
static int
checkSymmInfo(
DdManager * table,
DdHalfWord * symmInfo,
int index,
int level
)
- Returns 1 if a variable is the one with the highest index
among those belonging to a symmetry group that are in the top part of
the BDD. The top part is given by level.
- Side Effects None
- See Also
initSymmInfo
- Defined in
cuddExact.c
static DdTlcInfo *
computeClausesWithUniverse(
DdTlcInfo * Cres, list of clauses for child
DdHalfWord label, variable labeling the current node
short phase 0 if E child is zero; 1 if T child is zero
)
- Computes the two-literal clauses for a node with a zero
child, given the clauses for its other child and the label of the
node. Returns a pointer to a TclInfo structure if successful; NULL
otherwise.
- Side Effects None
- See Also
computeClauses
- Defined in
cuddEssent.c
static DdTlcInfo *
computeClauses(
DdTlcInfo * Tres, list of clauses for T child
DdTlcInfo * Eres, list of clauses for E child
DdHalfWord label, variable labeling the current node
int size number of variables in the manager
)
- Computes the two-literal clauses for a node given the
clauses for its children and the label of the node. Returns a
pointer to a TclInfo structure if successful; NULL otherwise.
- Side Effects None
- See Also
computeClausesWithUniverse
- Defined in
cuddEssent.c
static int
computeLB(
DdManager * table, manager
DdHalfWord * order, optimal order for the subset
int roots, roots between lower and upper
int cost, minimum cost for the subset
int lower, lower level to be reordered
int upper, upper level to be reordered
int level offset for the current top bottom var
)
- Computes a lower bound on the size of a BDD from the
following factors:
- size of the lower part of it;
- size of the part of the upper part not subjected to reordering;
- number of roots in the part of the BDD subjected to reordering;
- variable in the support of the roots in the upper part of the
BDD subjected to reordering.
- Side Effects None
- Defined in
cuddExact.c
static int
computeSavings(
DdManager * dd,
DdNode * f,
DdNode * skip,
ApproxInfo * info,
DdLevelQueue * queue
)
- Counts the nodes that would be eliminated if a given
node were replaced by zero. This procedure uses a queue passed by
the caller for efficiency: since the queue is left empty at the
endof the search, it can be reused as is by the next search. Returns
the count (always striclty positive) if successful; 0 otherwise.
- Side Effects None
- See Also
cuddUnderApprox
- Defined in
cuddApprox.c
static void
copyOrder(
DdManager * table,
int * array,
int lower,
int upper
)
- Copies the current variable order to array.
At the same time inverts the permutation.
- Side Effects None
- Defined in
cuddAnneal.c
static DdNode *
createResult(
DdManager * dd,
unsigned int index,
unsigned int phase,
DdNode * cube,
CUDD_VALUE_TYPE distance
)
- Builds a result for cache storage. Returns a pointer
to the resulting ADD if successful; NULL otherwise.
- Side Effects None
- See Also
cuddBddClosestCube
separateCube
- Defined in
cuddPriority.c
DdNode *
cuddAddApplyRecur(
DdManager * dd,
DD_AOP op,
DdNode * f,
DdNode * g
)
- Performs the recursive step of Cudd_addApply. Returns a
pointer to the result if successful; NULL otherwise.
- Side Effects None
- See Also
cuddAddMonadicApplyRecur
- Defined in
cuddAddApply.c
DdNode *
cuddAddBddDoPattern(
DdManager * dd,
DdNode * f
)
- Performs the recursive step for Cudd_addBddPattern. Returns a
pointer to the resulting BDD if successful; NULL otherwise.
- Side Effects None
- Defined in
cuddBridge.c
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
- Defined in
cuddAddIte.c
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
- Defined in
cuddCompose.c
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
- Defined in
cuddGenCof.c
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
- Defined in
cuddAddAbs.c
static DdNode *
cuddAddGeneralVectorComposeRecur(
DdManager * dd, DD manager
DdHashTable * table, computed table
DdNode * f, ADD in which to compose
DdNode ** vectorOn, functions to substitute for x_i
DdNode ** vectorOff, functions to substitute for x_i'
int deepest depth of deepest substitution
)
- Performs the recursive step of Cudd_addGeneralVectorCompose.
- Side Effects None
- Defined in
cuddCompose.c
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
- Defined in
cuddAddIte.c
DdNode *
cuddAddMonadicApplyRecur(
DdManager * dd,
DD_MAOP op,
DdNode * f
)
- Performs the recursive step of Cudd_addMonadicApply. Returns a
pointer to the result if successful; NULL otherwise.
- Side Effects None
- See Also
cuddAddApplyRecur
- Defined in
cuddAddApply.c
DdNode *
cuddAddNegateRecur(
DdManager * dd,
DdNode * f
)
- Implements the recursive step of Cudd_addNegate.
Returns a pointer to the result.
- Side Effects None
- Defined in
cuddAddNeg.c
static DdNode *
cuddAddNonSimComposeRecur(
DdManager * dd,
DdNode * f,
DdNode ** vector,
DdNode * key,
DdNode * cube,
int lastsub
)
- Performs the recursive step of Cudd_addNonSimCompose.
- Side Effects None
- Defined in
cuddCompose.c
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
- Defined in
cuddAddAbs.c
static DdNode *
cuddAddOuterSumRecur(
DdManager * dd,
DdNode * M,
DdNode * r,
DdNode * c
)
- Performs the recursive step of Cudd_addOuterSum.
Returns a pointer to the result if successful; NULL otherwise.
- Side Effects None
- Defined in
cuddMatMult.c
static DdNode *
cuddAddPermuteRecur(
DdManager * manager, DD manager
DdHashTable * table, computed table
DdNode * node, ADD to be reordered
int * permut permutation array
)
- Recursively puts the ADD in the order given in the
array permut. Checks for trivial cases to terminate recursion, then
splits on the children of this node. Once the solutions for the
children are obtained, it puts into the current position the node
from the rest of the ADD that should be here. Then returns this ADD.
The key here is that the node being visited is NOT put in its proper
place by this instance, but rather is switched when its proper
position is reached in the recursion tree.
The DdNode * that is returned is the same ADD as passed in as node,
but in the new order.
- Side Effects None
- See Also
Cudd_addPermute
cuddBddPermuteRecur
- Defined in
cuddCompose.c
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
- Defined in
cuddGenCof.c
DdNode *
cuddAddRoundOffRecur(
DdManager * dd,
DdNode * f,
double trunc
)
- Implements the recursive step of Cudd_addRoundOff.
Returns a pointer to the result.
- Side Effects None
- Defined in
cuddAddNeg.c
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
- Defined in
cuddAddInv.c
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
- Defined in
cuddAddAbs.c
static DdNode *
cuddAddVectorComposeRecur(
DdManager * dd, DD manager
DdHashTable * table, computed table
DdNode * f, ADD in which to compose
DdNode ** vector, functions to substitute
int deepest depth of deepest substitution
)
- Performs the recursive step of Cudd_addVectorCompose.
- Side Effects None
- Defined in
cuddCompose.c
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
- Defined in
cuddTable.c
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
- Defined in
cuddAnneal.c
static DdApaNumber
cuddApaCountMintermAux(
DdNode * node,
int digits,
DdApaNumber max,
DdApaNumber min,
st_table * table
)
- Performs the recursive step of Cudd_ApaCountMinterm.
It is based on the following identity. Let |f| be the
number of minterms of f. Then:
|f| = (|f0|+|f1|)/2
where f0 and f1 are the two cofactors of f.
Uses the identity
|f'| = max - |f|
.
The procedure expects the argument "node" to be a regular pointer, and
guarantees this condition is met in the recursive calls.
For efficiency, the result of a call is cached only if the node has
a reference count greater than 1.
Returns the number of minterms of the function rooted at node.
- Side Effects None
- Defined in
cuddApa.c
static enum st_retval
cuddApaStCountfree(
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
- Defined in
cuddApa.c
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)*i-1
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
- Defined in
cuddReorder.c
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
- Defined in
cuddAndAbs.c
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
- Defined in
cuddBddIte.c
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
- Defined in
cuddBddAbs.c
static DdNode *
cuddBddCharToVect(
DdManager * dd,
DdNode * f,
DdNode * x
)
- Performs the recursive step of Cudd_bddCharToVect.
This function maintains the invariant that f is non-zero.
Returns the i-th component of the vector if successful; otherwise NULL.
- Side Effects None
- See Also
Cudd_bddCharToVect
- Defined in
cuddGenCof.c
static DdNode *
cuddBddClipAndAbsRecur(
DdManager * manager,
DdNode * f,
DdNode * g,
DdNode * cube,
int distance,
int direction
)
- Approximates 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_bddClippingAndAbstract
- Defined in
cuddClip.c
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
- Defined in
cuddClip.c
static DdNode *
cuddBddClippingAndRecur(
DdManager * manager,
DdNode * f,
DdNode * g,
int distance,
int direction
)
- Implements the recursive step of Cudd_bddClippingAnd by taking
the conjunction of two BDDs. Returns a pointer to the result is
successful; NULL otherwise.
- Side Effects None
- See Also
cuddBddClippingAnd
- Defined in
cuddClip.c
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
- Defined in
cuddClip.c
DdNode *
cuddBddClosestCube(
DdManager * dd,
DdNode * f,
DdNode * g,
CUDD_VALUE_TYPE bound
)
- Performs the recursive step of Cudd_bddClosestCube.
Returns the cube if succesful; NULL otherwise. The procedure uses a
four-way recursion to examine all four combinations of cofactors of
f
and g
according to the following formula.
H(f,g) = min(H(ft,gt), H(fe,ge), H(ft,ge)+1, H(fe,gt)+1)
Bounding is based on the following observations.
- If we already found two points at distance 0, there is no point in
continuing. Furthermore,
- If F == not(G) then the best we can hope for is a minimum distance
of 1. If we have already found two points at distance 1, there is
no point in continuing. (Indeed, H(F,G) == 1 in this case. We
have to continue, though, to find the cube.)
The variable bound
is set at the largest value of the distance
that we are still interested in. Therefore, we desist when
(bound == -1) and (F != not(G)) or (bound == 0) and (F == not(G)).
If we were maximally aggressive in using the bound, we would always
set the bound to the minimum distance seen thus far minus one. That
is, we would maintain the invariant
bound < minD,
except at the very beginning, when we have no value for
minD
.
However, we do not use bound < minD
when examining the
two negative cofactors, because we try to find a large cube at
minimum distance. To do so, we try to find a cube in the negative
cofactors at the same or smaller distance from the cube found in the
positive cofactors.
When we compute H(ft,ge)
and H(fe,gt)
we
know that we are going to add 1 to the result of the recursive call
to account for the difference in the splitting variable. Therefore,
we decrease the bound correspondingly.
Another important observation concerns the need of examining all
four pairs of cofators only when both f
and
g
depend on the top variable.
Suppose gt == ge == g
. (That is, g
does
not depend on the top variable.) Then
H(f,g) = min(H(ft,g), H(fe,g), H(ft,g)+1, H(fe,g)+1)
= min(H(ft,g), H(fe,g)) .
Therefore, under these circumstances, we skip the two "cross" cases.
An interesting feature of this function is the scheme used for
caching the results in the global computed table. Since we have a
cube and a distance, we combine them to form an ADD. The
combination replaces the zero child of the top node of the cube with
the negative of the distance. (The use of the negative is to avoid
ambiguity with 1.) The degenerate cases (zero and one) are treated
specially because the distance is known (0 for one, and infinity for
zero).
- Side Effects None
- See Also
Cudd_bddClosestCube
- Defined in
cuddPriority.c
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
- Defined in
cuddCompose.c
static int
cuddBddConstrainDecomp(
DdManager * dd,
DdNode * f,
DdNode ** decomp
)
- Performs the recursive step of Cudd_bddConstrainDecomp.
Returns f super (i) if successful; otherwise NULL.
- Side Effects None
- See Also
Cudd_bddConstrainDecomp
- Defined in
cuddGenCof.c
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
- Defined in
cuddGenCof.c
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
- Defined in
cuddBddAbs.c
DdNode *
cuddBddIntersectRecur(
DdManager * dd,
DdNode * f,
DdNode * g
)
- Implements the recursive step of Cudd_bddIntersect.
- Side Effects None
- See Also
Cudd_bddIntersect
- Defined in
cuddBddIte.c
DdNode *
cuddBddIsop(
DdManager * dd,
DdNode * L,
DdNode * U
)
- Performs the recursive step of Cudd_bddIsop.
- Side Effects None
- See Also
Cudd_bddIsop
- Defined in
cuddZddIsop.c
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
- Defined in
cuddBddIte.c
static DdNode *
cuddBddLICBuildResult(
DdManager * dd,
DdNode * f,
st_table * cache,
st_table * table
)
- Builds the results of Cudd_bddLICompaction.
Returns a pointer to the minimized BDD if successful; otherwise NULL.
- Side Effects None
- See Also
Cudd_bddLICompaction
cuddBddLICMarkEdges
- Defined in
cuddGenCof.c
static int
cuddBddLICMarkEdges(
DdManager * dd,
DdNode * f,
DdNode * c,
st_table * table,
st_table * cache
)
- Performs the edge marking step of Cudd_bddLICompaction.
Returns the LUB of the markings of the two outgoing edges of
f
if successful; otherwise CUDD_OUT_OF_MEM.
- Side Effects None
- See Also
Cudd_bddLICompaction
cuddBddLICBuildResult
- Defined in
cuddGenCof.c
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
- Defined in
cuddGenCof.c
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
- Defined in
cuddLiteral.c
DdNode *
cuddBddMakePrime(
DdManager * dd, manager
DdNode * cube, cube to be expanded
DdNode * f function of which the cube is to be made a prime
)
- Performs the recursive step of Cudd_bddMakePrime.
Returns the prime if successful; NULL otherwise.
- Side Effects None
- Defined in
cuddSat.c
DdNode *
cuddBddNPAndRecur(
DdManager * manager,
DdNode * f,
DdNode * g
)
- Implements the recursive step of Cudd_bddNPAnd.
Returns a pointer to the result is successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_bddNPAnd
- Defined in
cuddGenCof.c
static DdNode *
cuddBddPermuteRecur(
DdManager * manager, DD manager
DdHashTable * table, computed table
DdNode * node, BDD to be reordered
int * permut permutation array
)
- Recursively puts the BDD in the order given in the array permut.
Checks for trivial cases to terminate recursion, then splits on the
children of this node. Once the solutions for the children are
obtained, it puts into the current position the node from the rest of
the BDD that should be here. Then returns this BDD.
The key here is that the node being visited is NOT put in its proper
place by this instance, but rather is switched when its proper position
is reached in the recursion tree.
The DdNode * that is returned is the same BDD as passed in as node,
but in the new order.
- Side Effects None
- See Also
Cudd_bddPermute
cuddAddPermuteRecur
- Defined in
cuddCompose.c
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
- Defined in
cuddGenCof.c
static DdNode *
cuddBddSqueeze(
DdManager * dd,
DdNode * l,
DdNode * u
)
- Performs the recursive step of Cudd_bddSqueeze. This
procedure exploits the fact that if we complement and swap the
bounds of the interval we obtain a valid solution by taking the
complement of the solution to the original problem. Therefore, we
can enforce the condition that the upper bound is always regular.
Returns a pointer to the result if successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_bddSqueeze
- Defined in
cuddGenCof.c
static DdNode *
cuddBddTransferRecur(
DdManager * ddS,
DdManager * ddD,
DdNode * f,
st_table * table
)
- Performs the recursive step of Cudd_bddTransfer.
Returns a pointer to the result if successful; NULL otherwise.
- Side Effects None
- See Also
cuddBddTransfer
- Defined in
cuddBridge.c
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
- Defined in
cuddBridge.c
static DdNode *
cuddBddVarMapRecur(
DdManager * manager, DD manager
DdNode * f BDD to be remapped
)
- Implements the recursive step of Cudd_bddVarMap.
Returns a pointer to the result if successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_bddVarMap
- Defined in
cuddCompose.c
static DdNode *
cuddBddVectorComposeRecur(
DdManager * dd, DD manager
DdHashTable * table, computed table
DdNode * f, BDD in which to compose
DdNode ** vector, functions to be composed
int deepest depth of the deepest substitution
)
- Performs the recursive step of Cudd_bddVectorCompose.
- Side Effects None
- Defined in
cuddCompose.c
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
- Defined in
cuddBddAbs.c
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
- Defined in
cuddBddIte.c
DdNode *
cuddBiasedUnderApprox(
DdManager * dd, DD manager
DdNode * f, current DD
DdNode * b, bias function
int numVars, maximum number of variables
int threshold, threshold under which approximation stops
double quality1, minimum improvement for accepted changes when b=1
double quality0 minimum improvement for accepted changes when b=0
)
- Applies the biased remapping underappoximation algorithm.
Proceeds in three phases:
- collect information on each node in the BDD; this is done via DFS.
- traverse the BDD in top-down 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_BiasedUnderApprox
- Defined in
cuddApprox.c
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
- Defined in
cuddPriority.c
void
cuddCacheFlush(
DdManager * table
)
- Flushes the cache.
- Side Effects None
- Defined in
cuddCache.c
void
cuddCacheInsert1(
DdManager * table,
DD_CTFP1 op,
DdNode * f,
DdNode * data
)
- Inserts a result in the cache for a function with two
operands.
- Side Effects None
- See Also
cuddCacheInsert
cuddCacheInsert2
- Defined in
cuddCache.c
void
cuddCacheInsert2(
DdManager * table,
DD_CTFP op,
DdNode * f,
DdNode * g,
DdNode * data
)
- Inserts a result in the cache for a function with two
operands.
- Side Effects None
- See Also
cuddCacheInsert
cuddCacheInsert1
- Defined in
cuddCache.c
void
cuddCacheInsert(
DdManager * table,
ptruint op,
DdNode * f,
DdNode * g,
DdNode * h,
DdNode * data
)
- Inserts a result in the cache.
- Side Effects None
- See Also
cuddCacheInsert2
cuddCacheInsert1
- Defined in
cuddCache.c
DdNode *
cuddCacheLookup1Zdd(
DdManager * table,
DD_CTFP1 op,
DdNode * f
)
- Returns the result if found; it returns NULL if no
result is found.
- Side Effects None
- See Also
cuddCacheLookupZdd
cuddCacheLookup2Zdd
- Defined in
cuddCache.c
DdNode *
cuddCacheLookup1(
DdManager * table,
DD_CTFP1 op,
DdNode * f
)
- Returns the result if found; it returns NULL if no
result is found.
- Side Effects None
- See Also
cuddCacheLookup
cuddCacheLookup2
- Defined in
cuddCache.c
DdNode *
cuddCacheLookup2Zdd(
DdManager * table,
DD_CTFP op,
DdNode * f,
DdNode * g
)
- Returns the result if found; it returns NULL if no
result is found.
- Side Effects None
- See Also
cuddCacheLookupZdd
cuddCacheLookup1Zdd
- Defined in
cuddCache.c
DdNode *
cuddCacheLookup2(
DdManager * table,
DD_CTFP op,
DdNode * f,
DdNode * g
)
- Returns the result if found; it returns NULL if no
result is found.
- Side Effects None
- See Also
cuddCacheLookup
cuddCacheLookup1
- Defined in
cuddCache.c
DdNode *
cuddCacheLookupZdd(
DdManager * table,
ptruint op,
DdNode * f,
DdNode * g,
DdNode * h
)
- Returns the result if found; it returns NULL if no
result is found.
- Side Effects None
- See Also
cuddCacheLookup2Zdd
cuddCacheLookup1Zdd
- Defined in
cuddCache.c
DdNode *
cuddCacheLookup(
DdManager * table,
ptruint op,
DdNode * f,
DdNode * g,
DdNode * h
)
- Returns the result if found; it returns NULL if no
result is found.
- Side Effects None
- See Also
cuddCacheLookup2
cuddCacheLookup1
- Defined in
cuddCache.c
int
cuddCacheProfile(
DdManager * table,
FILE * fp
)
- Computes and prints a profile of the cache usage.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddCache.c
void
cuddCacheResize(
DdManager * table
)
- Resizes the cache.
- Side Effects None
- Defined in
cuddCache.c
static int
cuddCheckCollisionOrdering(
DdManager * unique,
int i,
int j
)
- Checks whether a collision list is ordered.
- Side Effects None
- Defined in
cuddTable.c
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
- Defined in
cuddCof.c
void
cuddClearDeathRow(
DdManager * table
)
- Clears the death row.
- Side Effects None
- See Also
Cudd_DelayedDerefBdd
Cudd_IterDerefBdd
Cudd_CheckZeroRef
cuddGarbageCollect
- Defined in
cuddRef.c
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
- Defined in
cuddCof.c
int
cuddCollectNodes(
DdNode * f,
st_table * visited
)
- Traverses the DD 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
- Defined in
cuddUtil.c
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
- Defined in
cuddCache.c
static int
cuddConjunctsAux(
DdManager * dd,
DdNode * f,
DdNode ** c1,
DdNode ** c2
)
- Procedure to compute two conjunctive factors of f and
place in *c1 and *c2. Sets up the required data - table of distances
from the constant and local reference count. Also minterm table.
- Defined in
cuddDecomp.c
DdNode *
cuddConstantLookup(
DdManager * table,
ptruint op,
DdNode * f,
DdNode * g,
DdNode * h
)
- 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
- Defined in
cuddCache.c
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 The variable map used for fast variable substitution is
destroyed if it exists. In this case the cache is also cleared.
- See Also
cuddInsertSubtables
Cudd_SetVarMap
- Defined in
cuddTable.c
static void
cuddDoRebalance(
DdNodePtr ** stack,
int stackN
)
- Rebalances a red/black tree.
- Side Effects None
- Defined in
cuddTable.c
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
- Defined in
cuddReorder.c
static int
cuddEstimateCofactorSimple(
DdNode * node,
int i
)
- Performs the recursive step of Cudd_CofactorEstimateSimple.
Returns an estimate of the number of nodes in the DD of the positive
cofactor of node. Uses the least significant bit of the next field as
visited flag. node is supposed to be regular; the invariant is maintained
by this procedure.
- Side Effects None
- Defined in
cuddUtil.c
static int
cuddEstimateCofactor(
DdManager * dd,
st_table * table,
DdNode * node,
int i,
int phase,
DdNode ** ptr
)
- Performs the recursive step of Cudd_CofactorEstimate.
Returns an estimate of the number of nodes in the DD of a
cofactor of node. Uses the least significant bit of the next field as
visited flag. node is supposed to be regular; the invariant is maintained
by this procedure.
- Side Effects None
- Defined in
cuddUtil.c
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
- Defined in
cuddExact.c
static int
cuddFindParent(
DdManager * table,
DdNode * node
)
- Searches the subtables above node for a parent. Returns 1
as soon as one parent is found. Returns 0 is the search is fruitless.
- Side Effects None
- Defined in
cuddTable.c
void
cuddFreeTable(
DdManager * unique
)
- Frees the resources associated to a unique table.
- Side Effects None
- See Also
cuddInitTable
- Defined in
cuddTable.c
int
cuddGarbageCollect(
DdManager * unique,
int clearCache
)
- Performs garbage collection on the BDD and ZDD unique tables.
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
- Defined in
cuddTable.c
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
- Defined in
cuddGenetic.c
void
cuddGetBranches(
DdNode * g,
DdNode ** g1,
DdNode ** g0
)
- Computes the children of g.
- Side Effects None
- Defined in
cuddCof.c
static DdHashItem *
cuddHashTableAlloc(
DdHashTable * hash
)
- Fast storage allocation for items in a hash table. The
first 4 bytes of a chunk contain a pointer to the next block; the
rest contains DD_MEM_CHUNK spaces for hash items. Returns a pointer to
a new item if successful; NULL is memory is full.
- Side Effects None
- See Also
cuddAllocNode
cuddDynamicAllocNode
- Defined in
cuddLCache.c
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
- Defined in
cuddLCache.c
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
- Defined in
cuddLCache.c
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
- Defined in
cuddLCache.c
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
- Defined in
cuddLCache.c
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
- Defined in
cuddLCache.c
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
- Defined in
cuddLCache.c
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
- Defined in
cuddLCache.c
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
- Defined in
cuddLCache.c
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
- Defined in
cuddLCache.c
void
cuddHashTableQuit(
DdHashTable * hash
)
- Shuts down a hash table, dereferencing all the values.
- Side Effects None
- See Also
cuddHashTableInit
- Defined in
cuddLCache.c
static int
cuddHashTableResize(
DdHashTable * hash
)
- Resizes a hash table. Returns 1 if successful; 0
otherwise.
- Side Effects None
- See Also
cuddHashTableInsert
- Defined in
cuddLCache.c
int
cuddHeapProfile(
DdManager * dd
)
- Prints to the manager's 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
- Defined in
cuddCheck.c
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
- Defined in
cuddCache.c
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 depth-first
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
- Defined in
cuddInteract.c
int
cuddInitLinear(
DdManager * table
)
- Initializes the linear transform matrix. Returns 1 if
successful; 0 otherwise.
- Side Effects none
- Defined in
cuddLinear.c
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
unsigned int looseUpTo Limit for fast table growth
)
- Creates and initializes the unique table. Returns a pointer
to the table if successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_Init
cuddFreeTable
- Defined in
cuddTable.c
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