static unsigned int
AssessPathLength(
unsigned int * pathLengthArray, array determining number of nodes belonging to the different path lengths
int threshold, threshold to determine maximum allowable nodes in the subset
int numVars, maximum number of variables
unsigned int * excess, number of nodes labeled maxpath required in the subset
FILE * fp where to write messages
)
- Chooses the maximum allowable path length under each node.
The corner cases are when the threshold is larger than the number
of nodes in the BDD iself, in which case 'numVars + 1' is returned.
If all nodes of a particular path length are needed, then the
maxpath returned is the next one with excess nodes = 0;
- Side Effects None
- Defined in
cuddSubsetSP.c
static int
BAapplyBias(
DdManager * dd,
DdNode * f,
DdNode * b,
ApproxInfo * info,
DdHashTable * cache
)
- Finds don't care nodes by traversing f and b in parallel.
Returns the care status of the visited f node if successful; CARE_ERROR
otherwise.
- Side Effects None
- See Also
cuddBiasedUnderApprox
- Defined in
cuddApprox.c
static int
BAmarkNodes(
DdManager * dd, manager
DdNode * f, function to be analyzed
ApproxInfo * info, info on BDD
int threshold, when to stop approximating
double quality1, minimum improvement for accepted changes when b=1
double quality0 minimum improvement for accepted changes when b=0
)
- Marks nodes for remapping. Returns 1 if successful; 0
otherwise.
- Side Effects None
- See Also
cuddRemapUnderApprox
- Defined in
cuddApprox.c
static Conjuncts *
BuildConjuncts(
DdManager * dd,
DdNode * node,
st_table * distanceTable,
st_table * cacheTable,
int approxDistance,
int maxLocalRef,
st_table * ghTable,
st_table * mintermTable
)
- Builds the conjuncts recursively, bottom up. Constants
are returned as (f, f). The cache is checked for previously computed
result. The decomposition points are determined by the local
reference count of this node and the longest distance from the
constant. At the decomposition point, the factors returned are (f,
1). Recur on the two children. The order is determined by the
heavier branch. Combine the factors of the two children and pick the
one that already occurs in the gh table. Occurence in g is indicated
by value 1, occurence in h by 2, occurence in both 3.
- See Also
cuddConjunctsAux
- Defined in
cuddDecomp.c
static DdNode *
BuildSubsetBdd(
DdManager * dd, DD manager
st_table * pathTable, path table with path lengths and computed results
DdNode * node, current node
struct AssortedInfo * info, assorted information structure
st_table * subsetNodeTable table storing computed results
)
- Builds the BDD with nodes labeled with path length
under maxpath and as many nodes labeled maxpath as determined by the
threshold. The procedure uses the path table to determine which nodes
in the original bdd need to be retained. This procedure picks a
shortest path (tie break decided by taking the child with the shortest
distance to the constant) and recurs down the path till it reaches the
constant. the procedure then starts building the subset upward from
the constant. All nodes labeled by path lengths less than the given
maxpath are used to build the subset. However, in the case of nodes
that have label equal to maxpath, as many are chosen as required by
the threshold. This number is stored in the info structure in the
field thresholdReached. This field is decremented whenever a node
labeled maxpath is encountered and the nodes labeled maxpath are
aggregated in a maxpath table. As soon as the thresholdReached count
goes to 0, the shortest path from this node to the constant is found.
The extraction of nodes with the above labeling is based on the fact
that each node, labeled with a path length, P, has at least one child
labeled P or less. So extracting all nodes labeled a given path length
P ensures complete paths between the root and the constant. Extraction
of a partial number of nodes with a given path length may result in
incomplete paths and hence the additional number of nodes are grabbed
to complete the path. Since the Bdd is built bottom-up, other nodes
labeled maxpath do lie on complete paths. The procedure may cause the
subset to have a larger or smaller number of nodes than the specified
threshold. The increase in the number of nodes is caused by the
building of a subset and the reduction by recombination. However in
most cases, the recombination overshadows the increase and the
procedure returns a result with lower number of nodes than specified.
The subsetNodeTable is NIL when there is no hard limit on the number
of nodes. Further efforts towards keeping the subset closer to the
threshold number were abandoned in favour of keeping the procedure
simple and fast.
- Side Effects SubsetNodeTable is changed if it is not NIL.
- Defined in
cuddSubsetSP.c
static DdNode *
BuildSubsetBdd(
DdManager * dd, DD manager
DdNode * node, current node
int * size, current size of the subset
st_table * visitedTable, visited table storing all node data
int threshold,
st_table * storeTable,
st_table * approxTable
)
- The procedure carries out the building of the subset BDD
starting at the root. Using the three different counts labelling each node,
the procedure chooses the heavier branch starting from the root and keeps
track of the number of nodes it discards at each step, thus keeping count
of the size of the subset BDD dynamically. Once the threshold is satisfied,
the procedure then calls ITE to build the BDD.
- Side Effects None
- Defined in
cuddSubsetHB.c
static Conjuncts *
CheckInTables(
DdNode * node,
DdNode * g1,
DdNode * h1,
DdNode * g2,
DdNode * h2,
st_table * ghTable,
st_table * cacheTable,
int * outOfMem
)
- Check if the two pairs exist in the table. If any of
the conjuncts do exist, store in the cache and return the
corresponding pair.
- See Also
ZeroCase
BuildConjuncts
- Defined in
cuddDecomp.c
static Conjuncts *
CheckTablesCacheAndReturn(
DdNode * node,
DdNode * g,
DdNode * h,
st_table * ghTable,
st_table * cacheTable
)
- Check the tables for the existence of pair and return
one combination, cache the result. The assumption is that one of the
conjuncts is already in the tables.
- Side Effects g and h referenced for the cache
- See Also
ZeroCase
- Defined in
cuddDecomp.c
static void
ConjunctsFree(
DdManager * dd,
Conjuncts * factors
)
- Free factors structure
- Side Effects None
- Defined in
cuddDecomp.c
static enum st_retval
CorrelCleanUp(
char * key,
char * value,
char * arg
)
- Frees memory associated with hash table. Returns
ST_CONTINUE.
- Side Effects None
- Defined in
cuddBddCorr.c
static int
CorrelCompare(
const char * key1,
const char * key2
)
- Compares two hash table entries. Returns 0 if they are
identical; 1 otherwise.
- Side Effects None
- Defined in
cuddBddCorr.c
static int
CorrelHash(
char * key,
int modulus
)
- Hashes a hash table entry. It is patterned after
st_strhash. Returns a value between 0 and modulus.
- Side Effects None
- Defined in
cuddBddCorr.c
static double
CountMinterms(
DdNode * node,
double max,
st_table * mintermTable,
FILE * fp
)
- Count the number of minterms of each node ina a BDD and
store it in a hash table.
- Side Effects None
- Defined in
cuddDecomp.c
static NodeStat *
CreateBotDist(
DdNode * node,
st_table * distanceTable
)
- Get longest distance of node from constant. Returns the
distance of the root from the constant if successful; CUDD_OUT_OF_MEM
otherwise.
- Side Effects None
- Defined in
cuddDecomp.c
static int
CreateBotDist(
DdNode * node, current node
st_table * pathTable, path table with path lengths
unsigned int * pathLengthArray, array that stores number of nodes belonging to a particular path length.
FILE * fp where to write messages
)
- Labels each node with the shortest distance from the constant.
This is done in a DFS search of the BDD. Each node has an odd
and even parity distance from the sink (since there exists paths to both
zero and one) which is less than MAXSHORTINT. At each node these distances
are updated using the minimum distance of its children from the constant.
SInce now both the length from the root and child is known, the minimum path
length(length of the shortest path between the root and the constant that
this node lies on) of this node can be calculated and used to update the
pathLengthArray
- Side Effects Updates Path Table and path length array
- See Also
CreatePathTable
CreateTopDist
AssessPathLength
- Defined in
cuddSubsetSP.c
static st_table *
CreatePathTable(
DdNode * node, root of function
unsigned int * pathLengthArray, array of path lengths to store nodes labeled with the various path lengths
FILE * fp where to write messages
)
- The outer procedure to label each node with its shortest
distance from the root and constant. Calls CreateTopDist and CreateBotDist.
The basis for computing the distance between root and constant is that
the distance may be the sum of even distances from the node to the root
and constant or the sum of odd distances from the node to the root and
constant. Both CreateTopDist and CreateBotDist create the odd and
even parity distances from the root and constant respectively.
- Side Effects None
- See Also
CreateTopDist
CreateBotDist
- Defined in
cuddSubsetSP.c
static void
CreateTopDist(
st_table * pathTable, hast table to store path lengths
int parentPage, the pointer to the page on which the first parent in the queue is to be found.
int parentQueueIndex, pointer to the first parent on the page
int topLen, current distance from the root
DdNode ** childPage, pointer to the page on which the first child is to be added.
int childQueueIndex, pointer to the first child
int numParents, number of parents to process in this recursive call
FILE * fp where to write messages
)
- Labels each node with its shortest distance from the root.
This is done in a BFS search of the BDD. The nodes are processed
in a queue implemented as pages(array) to reduce memory fragmentation.
An entry is created for each node visited. The distance from the root
to the node with the corresponding parity is updated. The procedure
is called recursively each recusion level handling nodes at a given
level from the root.
- Side Effects Creates entries in the pathTable
- See Also
CreatePathTable
CreateBotDist
- Defined in
cuddSubsetSP.c
int
Cudd_AddHook(
DdManager * dd,
DD_HFP f,
Cudd_HookType where
)
- Adds a function to a hook. A hook is a list of
application-provided functions called on certain occasions by the
package. Returns 1 if the function is successfully added; 2 if the
function was already in the list; 0 otherwise.
- Side Effects None
- See Also
Cudd_RemoveHook
- Defined in
cuddAPI.c
DdApaDigit
Cudd_ApaAdd(
int digits,
DdApaNumber a,
DdApaNumber b,
DdApaNumber sum
)
- Adds two arbitrary precision integers. Returns the
carry out of the most significant digit.
- Side Effects The result of the sum is stored in parameter
sum
.
- Defined in
cuddApa.c
int
Cudd_ApaCompareRatios(
int digitsFirst,
DdApaNumber firstNum,
unsigned int firstDen,
int digitsSecond,
DdApaNumber secondNum,
unsigned int secondDen
)
- Compares the ratios of two arbitrary precision integers
to two unsigned ints. Returns 1 if the first number is larger; 0 if
they are equal; -1 if the second number is larger.
- Side Effects None
- Defined in
cuddApa.c
int
Cudd_ApaCompare(
int digitsFirst,
DdApaNumber first,
int digitsSecond,
DdApaNumber second
)
- Compares two arbitrary precision integers. Returns 1 if
the first number is larger; 0 if they are equal; -1 if the second
number is larger.
- Side Effects None
- Defined in
cuddApa.c
void
Cudd_ApaCopy(
int digits,
DdApaNumber source,
DdApaNumber dest
)
- Makes a copy of an arbitrary precision integer.
- Side Effects Changes parameter
dest
.
- Defined in
cuddApa.c
DdApaNumber
Cudd_ApaCountMinterm(
DdManager * manager,
DdNode * node,
int nvars,
int * digits
)
- Counts the number of minterms of a DD. The function is
assumed to depend on nvars variables. The minterm count is
represented as an arbitrary precision unsigned integer, to allow for
any number of variables CUDD supports. Returns a pointer to the
array representing the number of minterms of the function rooted at
node if successful; NULL otherwise.
- Side Effects The number of digits of the result is returned in
parameter
digits
.
- See Also
Cudd_CountMinterm
- Defined in
cuddApa.c
unsigned int
Cudd_ApaIntDivision(
int digits,
DdApaNumber dividend,
unsigned int divisor,
DdApaNumber quotient
)
- Divides an arbitrary precision integer by a 32-bit
unsigned integer. Returns the remainder of the division. This
procedure relies on the assumption that the number of bits of a
DdApaDigit plus the number of bits of an unsigned int is less the
number of bits of the mantissa of a double. This guarantees that the
product of a DdApaDigit and an unsigned int can be represented
without loss of precision by a double. On machines where this
assumption is not satisfied, this procedure will malfunction.
- Side Effects The quotient is returned in parameter
quotient
.
- See Also
Cudd_ApaShortDivision
- Defined in
cuddApa.c
int
Cudd_ApaNumberOfDigits(
int binaryDigits
)
- Finds the number of digits for an arbitrary precision
integer given the maximum number of binary digits. The number of
binary digits should be positive. Returns the number of digits if
successful; 0 otherwise.
- Side Effects None
- Defined in
cuddApa.c
void
Cudd_ApaPowerOfTwo(
int digits,
DdApaNumber number,
int power
)
- Sets an arbitrary precision integer to a power of
two. If the power of two is too large to be represented, the number
is set to 0.
- Side Effects The result is returned in parameter
number
.
- Defined in
cuddApa.c
int
Cudd_ApaPrintDecimal(
FILE * fp,
int digits,
DdApaNumber number
)
- Prints an arbitrary precision integer in decimal format.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- See Also
Cudd_ApaPrintHex
Cudd_ApaPrintExponential
- Defined in
cuddApa.c
int
Cudd_ApaPrintDensity(
FILE * fp,
DdManager * dd,
DdNode * node,
int nvars
)
- Prints the density of a BDD or ADD using
arbitrary precision arithmetic. Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddApa.c
int
Cudd_ApaPrintExponential(
FILE * fp,
int digits,
DdApaNumber number,
int precision
)
- Prints an arbitrary precision integer in exponential format.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- See Also
Cudd_ApaPrintHex
Cudd_ApaPrintDecimal
- Defined in
cuddApa.c
int
Cudd_ApaPrintHex(
FILE * fp,
int digits,
DdApaNumber number
)
- Prints an arbitrary precision integer in hexadecimal format.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- See Also
Cudd_ApaPrintDecimal
Cudd_ApaPrintExponential
- Defined in
cuddApa.c
int
Cudd_ApaPrintMintermExp(
FILE * fp,
DdManager * dd,
DdNode * node,
int nvars,
int precision
)
- Prints the number of minterms of a BDD or ADD in
exponential format using arbitrary precision arithmetic. Parameter
precision controls the number of signficant digits printed. Returns
1 if successful; 0 otherwise.
- Side Effects None
- See Also
Cudd_ApaPrintMinterm
- Defined in
cuddApa.c
int
Cudd_ApaPrintMinterm(
FILE * fp,
DdManager * dd,
DdNode * node,
int nvars
)
- Prints the number of minterms of a BDD or ADD using
arbitrary precision arithmetic. Returns 1 if successful; 0 otherwise.
- Side Effects None
- See Also
Cudd_ApaPrintMintermExp
- Defined in
cuddApa.c
void
Cudd_ApaSetToLiteral(
int digits,
DdApaNumber number,
DdApaDigit literal
)
- Sets an arbitrary precision integer to a one-digit literal.
- Side Effects The result is returned in parameter
number
.
- Defined in
cuddApa.c
void
Cudd_ApaShiftRight(
int digits,
DdApaDigit in,
DdApaNumber a,
DdApaNumber b
)
- Shifts right an arbitrary precision integer by one
binary place. The most significant binary digit of the result is
taken from parameter
in
.
- Side Effects The result is returned in parameter
b
.
- Defined in
cuddApa.c
DdApaDigit
Cudd_ApaShortDivision(
int digits,
DdApaNumber dividend,
DdApaDigit divisor,
DdApaNumber quotient
)
- Divides an arbitrary precision integer by a digit.
- Side Effects The quotient is returned in parameter
quotient
.
- Defined in
cuddApa.c
DdApaDigit
Cudd_ApaSubtract(
int digits,
DdApaNumber a,
DdApaNumber b,
DdApaNumber diff
)
- Subtracts two arbitrary precision integers. Returns the
borrow out of the most significant digit.
- Side Effects The result of the subtraction is stored in parameter
diff
.
- Defined in
cuddApa.c
void
Cudd_AutodynDisableZdd(
DdManager * unique
)
- Disables automatic dynamic reordering of ZDDs.
- Side Effects None
- See Also
Cudd_AutodynEnableZdd
Cudd_ReorderingStatusZdd
Cudd_AutodynDisable
- Defined in
cuddAPI.c
void
Cudd_AutodynDisable(
DdManager * unique
)
- Disables automatic dynamic reordering.
- Side Effects None
- See Also
Cudd_AutodynEnable
Cudd_ReorderingStatus
Cudd_AutodynDisableZdd
- Defined in
cuddAPI.c
void
Cudd_AutodynEnableZdd(
DdManager * unique,
Cudd_ReorderingType method
)
- Enables automatic dynamic reordering of ZDDs. Parameter
method is used to determine the method used for reordering ZDDs. If
CUDD_REORDER_SAME is passed, the method is unchanged.
- Side Effects None
- See Also
Cudd_AutodynDisableZdd
Cudd_ReorderingStatusZdd
Cudd_AutodynEnable
- Defined in
cuddAPI.c
void
Cudd_AutodynEnable(
DdManager * unique,
Cudd_ReorderingType method
)
- Enables automatic dynamic reordering of BDDs and
ADDs. Parameter method is used to determine the method used for
reordering. If CUDD_REORDER_SAME is passed, the method is
unchanged.
- Side Effects None
- See Also
Cudd_AutodynDisable
Cudd_ReorderingStatus
Cudd_AutodynEnableZdd
- Defined in
cuddAPI.c
double
Cudd_AverageDistance(
DdManager * dd
)
- Computes the average distance between adjacent nodes in
the manager. Adjacent nodes are node pairs such that the second node
is the then child, else child, or next node in the collision list.
- Side Effects None
- Defined in
cuddUtil.c
DdNode *
Cudd_BddToAdd(
DdManager * dd,
DdNode * B
)
- Converts a BDD to a 0-1 ADD. Returns a pointer to the
resulting ADD if successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_addBddPattern
Cudd_addBddThreshold
Cudd_addBddInterval
Cudd_addBddStrictThreshold
- Defined in
cuddBridge.c
int
Cudd_BddToCubeArray(
DdManager * dd,
DdNode * cube,
int * array
)
- Builds a positional array from the BDD of a cube.
Array must have one entry for each BDD variable. The positional
array has 1 in i-th position if the variable of index i appears in
true form in the cube; it has 0 in i-th position if the variable of
index i appears in complemented form in the cube; finally, it has 2
in i-th position if the variable of index i does not appear in the
cube. Returns 1 if successful (the BDD is indeed a cube); 0
otherwise.
- Side Effects The result is in the array passed by reference.
- See Also
Cudd_CubeArrayToBdd
- Defined in
cuddUtil.c
DdNode *
Cudd_BiasedOverApprox(
DdManager * dd, manager
DdNode * f, function to be superset
DdNode * b, bias function
int numVars, number of variables in the support of f
int threshold, when to stop approximation
double quality1, minimum improvement for accepted changes when b=1
double quality0 minimum improvement for accepted changes when b=0
)
- Extracts a dense superset from a BDD. The procedure is
identical to the underapproximation procedure except for the fact that it
works on the complement of the given function. Extracting the subset
of the complement function is equivalent to extracting the superset
of the function.
Returns a pointer to the BDD of the superset if successful. NULL if
intermediate result causes the procedure to run out of memory. The
parameter numVars is the maximum number of variables to be used in
minterm calculation. The optimal number
should be as close as possible to the size of the support of f.
However, it is safe to pass the value returned by Cudd_ReadSize for
numVars when the number of variables is under 1023. If numVars is
larger than 1023, it will overflow. If a 0 parameter is passed then
the procedure will compute a value which will avoid overflow but
will cause underflow with 2046 variables or more.
- Side Effects None
- See Also
Cudd_SupersetHeavyBranch
Cudd_SupersetShortPaths
Cudd_RemapOverApprox
Cudd_BiasedUnderApprox
Cudd_ReadSize
- Defined in
cuddApprox.c
DdNode *
Cudd_BiasedUnderApprox(
DdManager * dd, manager
DdNode * f, function to be subset
DdNode * b, bias function
int numVars, number of variables in the support of f
int threshold, when to stop approximation
double quality1, minimum improvement for accepted changes when b=1
double quality0 minimum improvement for accepted changes when b=0
)
- Extracts a dense subset from a BDD. This procedure uses
a biased remapping technique and density as the cost function. The bias
is a function. This procedure tries to approximate where the bias is 0
and preserve the given function where the bias is 1.
Returns a pointer to the BDD of the subset if
successful. NULL if the procedure runs out of memory. The parameter
numVars is the maximum number of variables to be used in minterm
calculation. The optimal number should be as close as possible to
the size of the support of f. However, it is safe to pass the value
returned by Cudd_ReadSize for numVars when the number of variables
is under 1023. If numVars is larger than 1023, it will cause
overflow. If a 0 parameter is passed then the procedure will compute
a value which will avoid overflow but will cause underflow with 2046
variables or more.
- Side Effects None
- See Also
Cudd_SubsetShortPaths
Cudd_SubsetHeavyBranch
Cudd_UnderApprox
Cudd_RemapUnderApprox
Cudd_ReadSize
- Defined in
cuddApprox.c
DdNode *
Cudd_CProjection(
DdManager * dd,
DdNode * R,
DdNode * Y
)
- Computes the compatible projection of relation R with
respect to cube Y. Returns a pointer to the c-projection if
successful; NULL otherwise. For a comparison between Cudd_CProjection
and Cudd_PrioritySelect, see the documentation of the latter.
- Side Effects None
- See Also
Cudd_PrioritySelect
- Defined in
cuddPriority.c
int
Cudd_CheckKeys(
DdManager * table
)
- Checks for the following conditions:
- Wrong sizes of subtables.
- Wrong number of keys found in unique subtable.
- Wrong number of dead found in unique subtable.
- Wrong number of keys found in the constant table
- Wrong number of dead found in the constant table
- Wrong number of total slots found
- Wrong number of maximum keys found
- Wrong number of total dead found
Reports the average length of non-empty lists. Returns the number of
subtables for which the number of keys is wrong.
- Side Effects None
- See Also
Cudd_DebugCheck
- Defined in
cuddCheck.c
int
Cudd_CheckZeroRef(
DdManager * manager
)
- Checks the unique table for nodes with non-zero
reference counts. It is normally called before Cudd_Quit to make sure
that there are no memory leaks due to missing Cudd_RecursiveDeref's.
Takes into account that reference counts may saturate and that the
basic constants and the projection functions are referenced by the
manager. Returns the number of nodes with non-zero reference count.
(Except for the cases mentioned above.)
- Side Effects None
- Defined in
cuddRef.c
int
Cudd_ClassifySupport(
DdManager * dd, manager
DdNode * f, first DD
DdNode * g, second DD
DdNode ** common, cube of shared variables
DdNode ** onlyF, cube of variables only in f
DdNode ** onlyG cube of variables only in g
)
- Classifies the variables in the support of two DDs
f
and g
, depending on whther they appear
in both DDs, only in f
, or only in g
.
Returns 1 if successful; 0 otherwise.
- Side Effects The cubes of the three classes of variables are
returned as side effects.
- See Also
Cudd_Support
Cudd_VectorSupport
- Defined in
cuddUtil.c
void
Cudd_ClearErrorCode(
DdManager * dd
)
- Clear the error code of a manager.
- Side Effects None
- See Also
Cudd_ReadErrorCode
- Defined in
cuddAPI.c
double *
Cudd_CofMinterm(
DdManager * dd,
DdNode * node
)
- Computes the fraction of minterms in the on-set of all
the positive cofactors of DD. Returns the pointer to an array of
doubles if successful; NULL otherwise. The array has as many
positions as there are BDD variables in the manager plus one. The
last position of the array contains the fraction of the minterms in
the ON-set of the function represented by the BDD or ADD. The other
positions of the array hold the variable signatures.
- Side Effects None
- Defined in
cuddSign.c
DdNode *
Cudd_Cofactor(
DdManager * dd,
DdNode * f,
DdNode * g
)
- Computes the cofactor of f with respect to g; g must be
the BDD or the ADD of a cube. Returns a pointer to the cofactor if
successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_bddConstrain
Cudd_bddRestrict
- Defined in
cuddCof.c
int
Cudd_CountLeaves(
DdNode * node
)
- Counts the number of leaves in a DD. Returns the number
of leaves in the DD rooted at node if successful; CUDD_OUT_OF_MEM
otherwise.
- Side Effects None
- See Also
Cudd_PrintDebug
- Defined in
cuddUtil.c
double
Cudd_CountMinterm(
DdManager * manager,
DdNode * node,
int nvars
)
- Counts the number of minterms of a DD. The function is
assumed to depend on nvars variables. The minterm count is
represented as a double, to allow for a larger number of variables.
Returns the number of minterms of the function rooted at node if
successful; (double) CUDD_OUT_OF_MEM otherwise.
- Side Effects None
- See Also
Cudd_PrintDebug
Cudd_CountPath
- Defined in
cuddUtil.c
double
Cudd_CountPathsToNonZero(
DdNode * node
)
- Counts the number of paths to a non-zero terminal of a
DD. The path count is
represented as a double, to allow for a larger number of variables.
Returns the number of paths of the function rooted at node.
- Side Effects None
- See Also
Cudd_CountMinterm
Cudd_CountPath
- Defined in
cuddUtil.c
double
Cudd_CountPath(
DdNode * node
)
- Counts the number of paths of a DD. Paths to all
terminal nodes are counted. The path count is represented as a
double, to allow for a larger number of variables. Returns the
number of paths of the function rooted at node if successful;
(double) CUDD_OUT_OF_MEM otherwise.
- Side Effects None
- See Also
Cudd_CountMinterm
- Defined in
cuddUtil.c
DdNode *
Cudd_CubeArrayToBdd(
DdManager * dd,
int * array
)
- Builds a cube from a positional array. The array must
have one integer entry for each BDD variable. If the i-th entry is
1, the variable of index i appears in true form in the cube; If the
i-th entry is 0, the variable of index i appears complemented in the
cube; otherwise the variable does not appear in the cube. Returns a
pointer to the BDD for the cube if successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_bddComputeCube
Cudd_IndicesToCube
Cudd_BddToCubeArray
- Defined in
cuddUtil.c
int
Cudd_DagSize(
DdNode * node
)
- Counts the number of nodes in a DD. Returns the number
of nodes in the graph rooted at node.
- Side Effects None
- See Also
Cudd_SharingSize
Cudd_PrintDebug
- Defined in
cuddUtil.c
int
Cudd_DeadAreCounted(
DdManager * dd
)
- Tells whether dead nodes are counted towards triggering
reordering. Returns 1 if dead nodes are counted; 0 otherwise.
- Side Effects None
- See Also
Cudd_TurnOnCountDead
Cudd_TurnOffCountDead
- Defined in
cuddAPI.c
int
Cudd_DebugCheck(
DdManager * table
)
- Checks for inconsistencies in the DD heap:
- node has illegal index
- live node has dead children
- node has illegal Then or Else pointers
- BDD/ADD node has identical children
- ZDD node has zero then child
- wrong number of total nodes
- wrong number of dead nodes
- ref count error at node
Returns 0 if no inconsistencies are found; DD_OUT_OF_MEM if there is
not enough memory; 1 otherwise.
- Side Effects None
- See Also
Cudd_CheckKeys
- Defined in
cuddCheck.c
DdNode *
Cudd_Decreasing(
DdManager * dd,
DdNode * f,
int i
)
- Determines whether the function represented by BDD f is
negative unate (monotonic decreasing) in variable i. Returns the
constant one is f is unate and the (logical) constant zero if it is not.
This function does not generate any new nodes.
- Side Effects None
- See Also
Cudd_Increasing
- Defined in
cuddSat.c
void
Cudd_DelayedDerefBdd(
DdManager * table,
DdNode * n
)
- Enqueues node n for later dereferencing. If the queue
is full decreases the reference count of the oldest node N to make
room for n. If N dies, recursively decreases the reference counts of
its children. It is used to dispose of a BDD that is currently not
needed, but may be useful again in the near future. The dereferencing
proper is done as in Cudd_IterDerefBdd.
- Side Effects None
- See Also
Cudd_RecursiveDeref
Cudd_IterDerefBdd
- Defined in
cuddRef.c
double
Cudd_Density(
DdManager * dd, manager
DdNode * f, function whose density is sought
int nvars size of the support of f
)
- Computes the density of a BDD or ADD. The density is
the ratio of the number of minterms to the number of nodes. If 0 is
passed as number of variables, the number of variables existing in
the manager is used. Returns the density if successful; (double)
CUDD_OUT_OF_MEM otherwise.
- Side Effects None
- See Also
Cudd_CountMinterm
Cudd_DagSize
- Defined in
cuddUtil.c
void
Cudd_Deref(
DdNode * node
)
- Decreases the reference count of node. It is primarily
used in recursive procedures to decrease the ref count of a result
node before returning it. This accomplishes the goal of removing the
protection applied by a previous Cudd_Ref.
- Side Effects None
- See Also
Cudd_RecursiveDeref
Cudd_RecursiveDerefZdd
Cudd_Ref
- Defined in
cuddRef.c
void
Cudd_DisableGarbageCollection(
DdManager * dd
)
- Disables garbage collection. Garbage collection is
initially enabled. This function may be called to disable it.
However, garbage collection will still occur when a new node must be
created and no memory is left, or when garbage collection is required
for correctness. (E.g., before reordering.)
- Side Effects None
- See Also
Cudd_EnableGarbageCollection
Cudd_GarbageCollectionEnabled
- Defined in
cuddAPI.c
int
Cudd_DisableReorderingReporting(
DdManager * dd
)
- Disables reporting of reordering stats.
Returns 1 if successful; 0 otherwise.
- Side Effects Removes functions from the pre-reordering and post-reordering
hooks.
- See Also
Cudd_EnableReorderingReporting
Cudd_ReorderingReporting
- Defined in
cuddAPI.c
DdNode *
Cudd_Disequality(
DdManager * dd, DD manager
int N, number of x and y variables
int c, right-hand side constant
DdNode ** x, array of x variables
DdNode ** y array of y variables
)
- This function generates a BDD for the function x -y != c.
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 BDD is built bottom-up.
It has a linear number of 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_Xgty
- Defined in
cuddPriority.c
int
Cudd_DumpBlifBody(
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
int mv 0: blif, 1: blif-MV
)
- Writes a blif body representing the argument BDDs as a
network of multiplexers. No header (.model, .inputs, and .outputs) and
footer (.end) are produced by this function. One multiplexer is written
for each BDD node. It returns 1 in case of success; 0 otherwise (e.g.,
out-of-memory, file system full, or an ADD with constants different
from 0 and 1). Cudd_DumpBlifBody does not close the file: This is the
caller responsibility. Cudd_DumpBlifBody 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. This function prints out only
.names part.
- Side Effects None
- See Also
Cudd_DumpBlif
Cudd_DumpDot
Cudd_PrintDebug
Cudd_DumpDDcal
Cudd_DumpDaVinci
Cudd_DumpFactoredForm
- Defined in
cuddExport.c
int
Cudd_DumpBlif(
DdManager * dd, manager
int n, number of output nodes to be dumped
DdNode ** f, array of output nodes to be dumped
char ** inames, array of input names (or NULL)
char ** onames, array of output names (or NULL)
char * mname, model name (or NULL)
FILE * fp, pointer to the dump file
int mv 0: blif, 1: blif-MV
)
- Writes a blif file representing the argument BDDs as a
network of multiplexers. One multiplexer is written for each BDD
node. It returns 1 in case of success; 0 otherwise (e.g.,
out-of-memory, file system full, or an ADD with constants different
from 0 and 1). Cudd_DumpBlif does not close the file: This is the
caller responsibility. Cudd_DumpBlif uses a minimal unique subset of
the hexadecimal address of a node as name for it. If the argument
inames is non-null, it is assumed to hold the pointers to the names
of the inputs. Similarly for onames.
- Side Effects None
- See Also
Cudd_DumpBlifBody
Cudd_DumpDot
Cudd_PrintDebug
Cudd_DumpDDcal
Cudd_DumpDaVinci
Cudd_DumpFactoredForm
- Defined in
cuddExport.c
int
Cudd_DumpDDcal(
DdManager * dd, manager
int n, number of output nodes to be dumped
DdNode ** f, array of output nodes to be dumped
char ** inames, array of input names (or NULL)
char ** onames, array of output names (or NULL)
FILE * fp pointer to the dump file
)
- Writes a DDcal file representing the argument BDDs.
It returns 1 in case of success; 0 otherwise (e.g., out-of-memory or
file system full). Cudd_DumpDDcal does not close the file: This
is the caller responsibility. Cudd_DumpDDcal uses a minimal unique
subset of the hexadecimal address of a node as name for it. If the
argument inames is non-null, it is assumed to hold the pointers to
the names of the inputs. Similarly for onames.
- Side Effects None
- See Also
Cudd_DumpDot
Cudd_PrintDebug
Cudd_DumpBlif
Cudd_DumpDaVinci
Cudd_DumpFactoredForm
- Defined in
cuddExport.c
int
Cudd_DumpDaVinci(
DdManager * dd, manager
int n, number of output nodes to be dumped
DdNode ** f, array of output nodes to be dumped
char ** inames, array of input names (or NULL)
char ** onames, array of output names (or NULL)
FILE * fp pointer to the dump file
)
- Writes a daVinci file representing the argument BDDs.
It returns 1 in case of success; 0 otherwise (e.g., out-of-memory or
file system full). Cudd_DumpDaVinci does not close the file: This
is the caller responsibility. Cudd_DumpDaVinci uses a minimal unique
subset of the hexadecimal address of a node as name for it. If the
argument inames is non-null, it is assumed to hold the pointers to
the names of the inputs. Similarly for onames.
- Side Effects None
- See Also
Cudd_DumpDot
Cudd_PrintDebug
Cudd_DumpBlif
Cudd_DumpDDcal
Cudd_DumpFactoredForm
- Defined in
cuddExport.c
int
Cudd_DumpDot(
DdManager * dd, manager
int n, number of output nodes to be dumped
DdNode ** f, array of output nodes to be dumped
char ** inames, array of input names (or NULL)
char ** onames, array of output names (or NULL)
FILE * fp pointer to the dump file
)
- Writes a file representing the argument DDs in a format
suitable for the graph drawing program dot.
It returns 1 in case of success; 0 otherwise (e.g., out-of-memory,
file system full).
Cudd_DumpDot does not close the file: This is the caller
responsibility. Cudd_DumpDot uses a minimal unique subset of the
hexadecimal address of a node as name for it.
If the argument inames is non-null, it is assumed to hold the pointers
to the names of the inputs. Similarly for onames.
Cudd_DumpDot uses the following convention to draw arcs:
- solid line: THEN arcs;
- dotted line: complement arcs;
- dashed line: regular ELSE arcs.
The dot options are chosen so that the drawing fits on a letter-size
sheet.
- Side Effects None
- See Also
Cudd_DumpBlif
Cudd_PrintDebug
Cudd_DumpDDcal
Cudd_DumpDaVinci
Cudd_DumpFactoredForm
- Defined in
cuddExport.c
int
Cudd_DumpFactoredForm(
DdManager * dd, manager
int n, number of output nodes to be dumped
DdNode ** f, array of output nodes to be dumped
char ** inames, array of input names (or NULL)
char ** onames, array of output names (or NULL)
FILE * fp pointer to the dump file
)
- Writes factored forms representing the argument BDDs.
The format of the factored form is the one used in the genlib files
for technology mapping in sis. It returns 1 in case of success; 0
otherwise (e.g., file system full). Cudd_DumpFactoredForm does not
close the file: This is the caller responsibility. Caution must be
exercised because a factored form may be exponentially larger than
the argument BDD. If the argument inames is non-null, it is assumed
to hold the pointers to the names of the inputs. Similarly for
onames.
- Side Effects None
- See Also
Cudd_DumpDot
Cudd_PrintDebug
Cudd_DumpBlif
Cudd_DumpDaVinci
Cudd_DumpDDcal
- Defined in
cuddExport.c
DdNode *
Cudd_Dxygtdxz(
DdManager * dd, DD manager
int N, number of x, y, and z variables
DdNode ** x, array of x variables
DdNode ** y, array of y variables
DdNode ** z array of z variables
)
- This function generates a BDD for the function d(x,y)
> d(x,z);
x, y, and z are N-bit numbers, x[0] x[1] ... x[N-1],
y[0] y[1] ... y[N-1], and z[0] z[1] ... z[N-1],
with 0 the most significant bit.
The distance d(x,y) is defined as:
sum_{i=0}^{N-1}(|x_i - y_i| cdot 2^{N-i-1}).
The BDD is built bottom-up.
It has 7*N-3 internal nodes, if the variables are ordered as follows:
x[0] y[0] z[0] x[1] y[1] z[1] ... x[N-1] y[N-1] z[N-1].
- Side Effects None
- See Also
Cudd_PrioritySelect
Cudd_Dxygtdyz
Cudd_Xgty
Cudd_bddAdjPermuteX
- Defined in
cuddPriority.c
DdNode *
Cudd_Dxygtdyz(
DdManager * dd, DD manager
int N, number of x, y, and z variables
DdNode ** x, array of x variables
DdNode ** y, array of y variables
DdNode ** z array of z variables
)
- This function generates a BDD for the function d(x,y)
> d(y,z);
x, y, and z are N-bit numbers, x[0] x[1] ... x[N-1],
y[0] y[1] ... y[N-1], and z[0] z[1] ... z[N-1],
with 0 the most significant bit.
The distance d(x,y) is defined as:
sum_{i=0}^{N-1}(|x_i - y_i| cdot 2^{N-i-1}).
The BDD is built bottom-up.
It has 7*N-3 internal nodes, if the variables are ordered as follows:
x[0] y[0] z[0] x[1] y[1] z[1] ... x[N-1] y[N-1] z[N-1].
- Side Effects None
- See Also
Cudd_PrioritySelect
Cudd_Dxygtdxz
Cudd_Xgty
Cudd_bddAdjPermuteX
- Defined in
cuddPriority.c
void
Cudd_EnableGarbageCollection(
DdManager * dd
)
- Enables garbage collection. Garbage collection is
initially enabled. Therefore it is necessary to call this function
only if garbage collection has been explicitly disabled.
- Side Effects None
- See Also
Cudd_DisableGarbageCollection
Cudd_GarbageCollectionEnabled
- Defined in
cuddAPI.c
int
Cudd_EnableReorderingReporting(
DdManager * dd
)
- Enables reporting of reordering stats.
Returns 1 if successful; 0 otherwise.
- Side Effects Installs functions in the pre-reordering and post-reordering
hooks.
- See Also
Cudd_DisableReorderingReporting
Cudd_ReorderingReporting
- Defined in
cuddAPI.c
int
Cudd_EpdCountMinterm(
DdManager * manager,
DdNode * node,
int nvars,
EpDouble * epd
)
- Counts the number of minterms of a DD with extended precision.
The function is assumed to depend on nvars variables. The minterm count is
represented as an EpDouble, to allow any number of variables.
Returns 0 if successful; CUDD_OUT_OF_MEM otherwise.
- Side Effects None
- See Also
Cudd_PrintDebug
Cudd_CountPath
- Defined in
cuddUtil.c
int
Cudd_EqualSupNorm(
DdManager * dd, manager
DdNode * f, first ADD
DdNode * g, second ADD
CUDD_VALUE_TYPE tolerance, maximum allowed difference
int pr verbosity level
)
- Compares two ADDs for equality within tolerance. Two
ADDs are reported to be equal if the maximum difference between them
(the sup norm of their difference) is less than or equal to the
tolerance parameter. Returns 1 if the two ADDs are equal (within
tolerance); 0 otherwise. If parameter
pr
is positive
the first failure is reported to the standard output.
- Side Effects None
- Defined in
cuddSat.c
int
Cudd_EquivDC(
DdManager * dd,
DdNode * F,
DdNode * G,
DdNode * D
)
- Tells whether F and G are identical wherever D is 0. F
and G are either two ADDs or two BDDs. D is either a 0-1 ADD or a
BDD. The function returns 1 if F and G are equivalent, and 0
otherwise. No new nodes are created.
- Side Effects None
- See Also
Cudd_bddLeqUnless
- Defined in
cuddSat.c
int
Cudd_EstimateCofactorSimple(
DdNode * node,
int i
)
- Estimates the number of nodes in a cofactor of a DD.
Returns an estimate of the number of nodes in the positive cofactor of
the graph rooted at node with respect to the variable whose index is i.
This procedure implements with minor changes the algorithm of Cabodi et al.
(ICCAD96). It does not allocate any memory, it does not change the
state of the manager, and it is fast. However, it has been observed to
overestimate the size of the cofactor by as much as a factor of 2.
- Side Effects None
- See Also
Cudd_DagSize
- Defined in
cuddUtil.c
int
Cudd_EstimateCofactor(
DdManager * dd, manager
DdNode * f, function
int i, index of variable
int phase 1: positive; 0: negative
)
- Estimates the number of nodes in a cofactor of a DD.
Returns an estimate of the number of nodes in a cofactor of
the graph rooted at node with respect to the variable whose index is i.
In case of failure, returns CUDD_OUT_OF_MEM.
This function uses a refinement of the algorithm of Cabodi et al.
(ICCAD96). The refinement allows the procedure to account for part
of the recombination that may occur in the part of the cofactor above
the cofactoring variable. This procedure does no create any new node.
It does keep a small table of results; therefore it may run out of memory.
If this is a concern, one should use Cudd_EstimateCofactorSimple, which
is faster, does not allocate any memory, but is less accurate.
- Side Effects None
- See Also
Cudd_DagSize
Cudd_EstimateCofactorSimple
- Defined in
cuddUtil.c
DdNode *
Cudd_Eval(
DdManager * dd,
DdNode * f,
int * inputs
)
- Finds the value of a DD for a given variable
assignment. The variable assignment is passed in an array of int's,
that should specify a zero or a one for each variable in the support
of the function. Returns a pointer to a constant node. No new nodes
are produced.
- Side Effects None
- See Also
Cudd_bddLeq
Cudd_addEvalConst
- Defined in
cuddSat.c
double
Cudd_ExpectedUsedSlots(
DdManager * dd
)
- Computes the fraction of slots in the unique table that
should be in use. This expected value is based on the assumption
that the hash function distributes the keys randomly; it can be
compared with the result of Cudd_ReadUsedSlots to monitor the
performance of the unique table hash function.
- Side Effects None
- See Also
Cudd_ReadSlots
Cudd_ReadUsedSlots
- Defined in
cuddAPI.c
DdNode *
Cudd_FindEssential(
DdManager * dd,
DdNode * f
)
- Returns the cube of the essential variables. A positive
literal means that the variable must be set to 1 for the function to be
1. A negative literal means that the variable must be set to 0 for the
function to be 1. Returns a pointer to the cube BDD if successful;
NULL otherwise.
- Side Effects None
- See Also
Cudd_bddIsVarEssential
- Defined in
cuddEssent.c
DdTlcInfo *
Cudd_FindTwoLiteralClauses(
DdManager * dd,
DdNode * f
)
- Returns the one- and two-literal clauses of a DD.
Returns a pointer to the structure holding the clauses if
successful; NULL otherwise. For a constant DD, the empty set of clauses
is returned. This is obviously correct for a non-zero constant. For the
constant zero, it is based on the assumption that only those clauses
containing variables in the support of the function are considered. Since
the support of a constant function is empty, no clauses are returned.
- Side Effects None
- See Also
Cudd_FindEssential
- Defined in
cuddEssent.c
DdGen *
Cudd_FirstCube(
DdManager * dd,
DdNode * f,
int ** cube,
CUDD_VALUE_TYPE * value
)
- Defines an iterator on the onset of a decision diagram
and finds its first cube. Returns a generator that contains the
information necessary to continue the enumeration if successful; NULL
otherwise.
A cube is represented as an array of literals, which are integers in
{0, 1, 2}; 0 represents a complemented literal, 1 represents an
uncomplemented literal, and 2 stands for don't care. The enumeration
produces a disjoint cover of the function associated with the diagram.
The size of the array equals the number of variables in the manager at
the time Cudd_FirstCube is called.
For each cube, a value is also returned. This value is always 1 for a
BDD, while it may be different from 1 for an ADD.
For BDDs, the offset is the set of cubes whose value is the logical zero.
For ADDs, the offset is the set of cubes whose value is the
background value. The cubes of the offset are not enumerated.
- Side Effects The first cube and its value are returned as side effects.
- See Also
Cudd_ForeachCube
Cudd_NextCube
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_FirstNode
- Defined in
cuddUtil.c
DdGen *
Cudd_FirstNode(
DdManager * dd,
DdNode * f,
DdNode ** node
)
- Defines an iterator on the nodes of a decision diagram
and finds its first node. Returns a generator that contains the
information necessary to continue the enumeration if successful;
NULL otherwise. The nodes are enumerated in a reverse topological
order, so that a node is always preceded in the enumeration by its
descendants.
- Side Effects The first node is returned as a side effect.
- See Also
Cudd_ForeachNode
Cudd_NextNode
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_FirstCube
- Defined in
cuddUtil.c
DdGen *
Cudd_FirstPrime(
DdManager * dd,
DdNode * l,
DdNode * u,
int ** cube
)
- Defines an iterator on a pair of BDDs describing a
(possibly incompletely specified) Boolean functions and finds the
first cube of a cover of the function. Returns a generator
that contains the information necessary to continue the enumeration
if successful; NULL otherwise.
The two argument BDDs are the lower and upper bounds of an interval.
It is a mistake to call this function with a lower bound that is not
less than or equal to the upper bound.
A cube is represented as an array of literals, which are integers in
{0, 1, 2}; 0 represents a complemented literal, 1 represents an
uncomplemented literal, and 2 stands for don't care. The enumeration
produces a prime and irredundant cover of the function associated
with the two BDDs. The size of the array equals the number of
variables in the manager at the time Cudd_FirstCube is called.
This iterator can only be used on BDDs.
- Side Effects The first cube is returned as side effect.
- See Also
Cudd_ForeachPrime
Cudd_NextPrime
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_FirstCube
Cudd_FirstNode
- Defined in
cuddUtil.c
void
Cudd_FreeTree(
DdManager * dd
)
- Frees the variable group tree of the manager.
- Side Effects None
- See Also
Cudd_SetTree
Cudd_ReadTree
Cudd_FreeZddTree
- Defined in
cuddAPI.c
void
Cudd_FreeZddTree(
DdManager * dd
)
- Frees the variable group tree of the manager.
- Side Effects None
- See Also
Cudd_SetZddTree
Cudd_ReadZddTree
Cudd_FreeTree
- Defined in
cuddAPI.c
int
Cudd_GarbageCollectionEnabled(
DdManager * dd
)
- Returns 1 if garbage collection is enabled; 0 otherwise.
- Side Effects None
- See Also
Cudd_EnableGarbageCollection
Cudd_DisableGarbageCollection
- Defined in
cuddAPI.c
int
Cudd_GenFree(
DdGen * gen
)
- Frees a CUDD generator. Always returns 0, so that it can
be used in mis-like foreach constructs.
- Side Effects None
- See Also
Cudd_ForeachCube
Cudd_ForeachNode
Cudd_FirstCube
Cudd_NextCube
Cudd_FirstNode
Cudd_NextNode
Cudd_IsGenEmpty
- Defined in
cuddUtil.c
DdNode *
Cudd_Increasing(
DdManager * dd,
DdNode * f,
int i
)
- Determines whether the function represented by BDD f is
positive unate (monotonic increasing) in variable i. It is based on
Cudd_Decreasing and the fact that f is monotonic increasing in i if
and only if its complement is monotonic decreasing in i.
- Side Effects None
- See Also
Cudd_Decreasing
- Defined in
cuddSat.c
DdNode *
Cudd_IndicesToCube(
DdManager * dd,
int * array,
int n
)
- Builds a cube of BDD variables from an array of indices.
Returns a pointer to the result if successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_bddComputeCube
Cudd_CubeArrayToBdd
- Defined in
cuddUtil.c
DdNode *
Cudd_Inequality(
DdManager * dd, DD manager
int N, number of x and y variables
int c, right-hand side constant
DdNode ** x, array of x variables
DdNode ** y array of y variables
)
- This function generates a BDD for the function x -y ≥ c.
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 BDD is built bottom-up.
It has a linear number of 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_Xgty
- Defined in
cuddPriority.c
DdManager *
Cudd_Init(
unsigned int numVars, initial number of BDD variables (i.e., subtables)
unsigned int numVarsZ, initial number of ZDD variables (i.e., subtables)
unsigned int numSlots, initial size of the unique tables
unsigned int cacheSize, initial size of the cache
unsigned long maxMemory target maximum memory occupation
)
- Creates a new DD manager, initializes the table, the
basic constants and the projection functions. If maxMemory is 0,
Cudd_Init decides suitable values for the maximum size of the cache
and for the limit for fast unique table growth based on the available
memory. Returns a pointer to the manager if successful; NULL
otherwise.
- Side Effects None
- See Also
Cudd_Quit
- Defined in
cuddInit.c
int
Cudd_IsGenEmpty(
DdGen * gen
)
- Queries the status of a generator. Returns 1 if the
generator is empty or NULL; 0 otherswise.
- Side Effects None
- See Also
Cudd_ForeachCube
Cudd_ForeachNode
Cudd_FirstCube
Cudd_NextCube
Cudd_FirstNode
Cudd_NextNode
Cudd_GenFree
- Defined in
cuddUtil.c
int
Cudd_IsInHook(
DdManager * dd,
DD_HFP f,
Cudd_HookType where
)
- Checks whether a function is in a hook. A hook is a list of
application-provided functions called on certain occasions by the
package. Returns 1 if the function is found; 0 otherwise.
- Side Effects None
- See Also
Cudd_AddHook
Cudd_RemoveHook
- Defined in
cuddAPI.c
int
Cudd_IsNonConstant(
DdNode * f
)
- Returns 1 if a DD node is not constant. This function is
useful to test the results of Cudd_bddIteConstant, Cudd_addIteConstant,
Cudd_addEvalConst. These results may be a special value signifying
non-constant. In the other cases the macro Cudd_IsConstant can be used.
- Side Effects None
- See Also
Cudd_IsConstant
Cudd_bddIteConstant
Cudd_addIteConstant
Cudd_addEvalConst
- Defined in
cuddAPI.c
void
Cudd_IterDerefBdd(
DdManager * table,
DdNode * n
)
- Decreases the reference count of node n. If n dies,
recursively decreases the reference counts of its children. It is
used to dispose of a BDD that is no longer needed. It is more
efficient than Cudd_RecursiveDeref, but it cannot be used on
ADDs. The greater efficiency comes from being able to assume that no
constant node will ever die as a result of a call to this
procedure.
- Side Effects None
- See Also
Cudd_RecursiveDeref
Cudd_DelayedDerefBdd
- Defined in
cuddRef.c
DdNode *
Cudd_LargestCube(
DdManager * manager,
DdNode * f,
int * length
)
- Finds a largest cube in a DD. f is the DD we want to
get the largest cube for. The problem is translated into the one of
finding a shortest path in f, when both THEN and ELSE arcs are assumed to
have unit length. This yields a largest cube in the disjoint cover
corresponding to the DD. Therefore, it is not necessarily the largest
implicant of f. Returns the largest cube as a BDD.
- Side Effects The number of literals of the cube is returned in length.
- See Also
Cudd_ShortestPath
- Defined in
cuddSat.c
DdNode *
Cudd_MakeBddFromZddCover(
DdManager * dd,
DdNode * node
)
- Converts a ZDD cover to a BDD graph. If successful, it
returns a BDD node, otherwise it returns NULL.
- See Also
cuddMakeBddFromZddCover
- Defined in
cuddZddIsop.c
MtrNode *
Cudd_MakeTreeNode(
DdManager * dd, manager
unsigned int low, index of the first group variable
unsigned int size, number of variables in the group
unsigned int type MTR_DEFAULT or MTR_FIXED
)
- Creates a new variable group. The group starts at
variable and contains size variables. The parameter low is the index
of the first variable. If the variable already exists, its current
position in the order is known to the manager. If the variable does
not exist yet, the position is assumed to be the same as the index.
The group tree is created if it does not exist yet.
Returns a pointer to the group if successful; NULL otherwise.
- Side Effects The variable tree is changed.
- See Also
Cudd_MakeZddTreeNode
- Defined in
cuddGroup.c
MtrNode *
Cudd_MakeZddTreeNode(
DdManager * dd, manager
unsigned int low, index of the first group variable
unsigned int size, number of variables in the group
unsigned int type MTR_DEFAULT or MTR_FIXED
)
- Creates a new ZDD variable group. The group starts at
variable and contains size variables. The parameter low is the index
of the first variable. If the variable already exists, its current
position in the order is known to the manager. If the variable does
not exist yet, the position is assumed to be the same as the index.
The group tree is created if it does not exist yet.
Returns a pointer to the group if successful; NULL otherwise.
- Side Effects The ZDD variable tree is changed.
- See Also
Cudd_MakeTreeNode
- Defined in
cuddZddGroup.c
int
Cudd_MinHammingDist(
DdManager * dd, DD manager
DdNode * f, function to examine
int * minterm, reference minterm
int upperBound distance above which an approximate answer is OK
)
- Returns the minimum Hamming distance between the
minterms of a function f and a reference minterm. The function is
given as a BDD; the minterm is given as an array of integers, one
for each variable in the manager. Returns the minimum distance if
it is less than the upper bound; the upper bound if the minimum
distance is at least as large; CUDD_OUT_OF_MEM in case of failure.
- Side Effects None
- See Also
Cudd_addHamming
Cudd_bddClosestCube
- Defined in
cuddPriority.c
DdApaNumber
Cudd_NewApaNumber(
int digits
)
- Allocates memory for an arbitrary precision
integer. Returns a pointer to the allocated memory if successful;
NULL otherwise.
- Side Effects None
- Defined in
cuddApa.c
int
Cudd_NextCube(
DdGen * gen,
int ** cube,
CUDD_VALUE_TYPE * value
)
- Generates the next cube of a decision diagram onset,
using generator gen. Returns 0 if the enumeration is completed; 1
otherwise.
- Side Effects The cube and its value are returned as side effects. The
generator is modified.
- See Also
Cudd_ForeachCube
Cudd_FirstCube
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_NextNode
- Defined in
cuddUtil.c
int
Cudd_NextNode(
DdGen * gen,
DdNode ** node
)
- Finds the node of a decision diagram, using generator
gen. Returns 0 if the enumeration is completed; 1 otherwise.
- Side Effects The next node is returned as a side effect.
- See Also
Cudd_ForeachNode
Cudd_FirstNode
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_NextCube
- Defined in
cuddUtil.c
int
Cudd_NextPrime(
DdGen * gen,
int ** cube
)
- Generates the next cube of a Boolean function,
using generator gen. Returns 0 if the enumeration is completed; 1
otherwise.
- Side Effects The cube and is returned as side effects. The
generator is modified.
- See Also
Cudd_ForeachPrime
Cudd_FirstPrime
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_NextCube
Cudd_NextNode
- Defined in
cuddUtil.c
unsigned int
Cudd_NodeReadIndex(
DdNode * node
)
- Returns the index of the node. The node pointer can be
either regular or complemented.
- Side Effects None
- See Also
Cudd_ReadIndex
- Defined in
cuddAPI.c
void
Cudd_OutOfMem(
long size size of the allocation that failed
)
- Warns that a memory allocation failed.
This function can be used as replacement of MMout_of_memory to prevent
the safe_mem functions of the util package from exiting when malloc
returns NULL. One possible use is in case of discretionary allocations;
for instance, the allocation of memory to enlarge the computed table.
- Side Effects None
- Defined in
cuddUtil.c
DdNode *
Cudd_OverApprox(
DdManager * dd, manager
DdNode * f, function to be superset
int numVars, number of variables in the support of f
int threshold, when to stop approximation
int safe, enforce safe approximation
double quality minimum improvement for accepted changes
)
- Extracts a dense superset from a BDD. The procedure is
identical to the underapproximation procedure except for the fact that it
works on the complement of the given function. Extracting the subset
of the complement function is equivalent to extracting the superset
of the function.
Returns a pointer to the BDD of the superset if successful. NULL if
intermediate result causes the procedure to run out of memory. The
parameter numVars is the maximum number of variables to be used in
minterm calculation. The optimal number
should be as close as possible to the size of the support of f.
However, it is safe to pass the value returned by Cudd_ReadSize for
numVars when the number of variables is under 1023. If numVars is
larger than 1023, it will overflow. If a 0 parameter is passed then
the procedure will compute a value which will avoid overflow but
will cause underflow with 2046 variables or more.
- Side Effects None
- See Also
Cudd_SupersetHeavyBranch
Cudd_SupersetShortPaths
Cudd_ReadSize
- Defined in
cuddApprox.c
unsigned int
Cudd_Prime(
unsigned int p
)
- Returns the next prime >= p.
- Side Effects None
- Defined in
cuddTable.c
int
Cudd_PrintDebug(
DdManager * dd,
DdNode * f,
int n,
int pr
)
- Prints to the standard output a DD and its statistics.
The statistics include the number of nodes, the number of leaves, and
the number of minterms. (The number of minterms is the number of
assignments to the variables that cause the function to be different
from the logical zero (for BDDs) and from the background value (for
ADDs.) The statistics are printed if pr > 0. Specifically:
- pr = 0 : prints nothing
- pr = 1 : prints counts of nodes and minterms
- pr = 2 : prints counts + disjoint sum of product
- pr = 3 : prints counts + list of nodes
- pr > 3 : prints counts + disjoint sum of product + list of nodes
For the purpose of counting the number of minterms, the function is
supposed to depend on n variables. Returns 1 if successful; 0 otherwise.
- Side Effects None
- See Also
Cudd_DagSize
Cudd_CountLeaves
Cudd_CountMinterm
Cudd_PrintMinterm
- Defined in
cuddUtil.c
int
Cudd_PrintInfo(
DdManager * dd,
FILE * fp
)
- Prints out statistics and settings for a CUDD manager.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddAPI.c
int
Cudd_PrintLinear(
DdManager * table
)
- Prints the linear transform matrix. Returns 1 in case of
success; 0 otherwise.
- Side Effects none
- Defined in
cuddLinear.c
int
Cudd_PrintMinterm(
DdManager * manager,
DdNode * node
)
- Prints a disjoint sum of product cover for the function
rooted at node. Each product corresponds to a path from node to a
leaf node different from the logical zero, and different from the
background value. Uses the package default output file. Returns 1
if successful; 0 otherwise.
- Side Effects None
- See Also
Cudd_PrintDebug
Cudd_bddPrintCover
- Defined in
cuddUtil.c
int
Cudd_PrintTwoLiteralClauses(
DdManager * dd,
DdNode * f,
char ** names,
FILE * fp
)
- Prints the one- and two-literal clauses. Returns 1 if
successful; 0 otherwise. The argument "names" can be NULL, in which case
the variable indices are printed.
- Side Effects None
- See Also
Cudd_FindTwoLiteralClauses
- Defined in
cuddEssent.c
void
Cudd_PrintVersion(
FILE * fp
)
- Prints the package version number.
- Side Effects None
- Defined in
cuddUtil.c
DdNode *
Cudd_PrioritySelect(
DdManager * dd, manager
DdNode * R, BDD of the relation
DdNode ** x, array of x variables
DdNode ** y, array of y variables
DdNode ** z, array of z variables (optional: may be NULL)
DdNode * Pi, BDD of the priority function (optional: may be NULL)
int n, size of x, y, and z
DD_PRFP Pifunc function used to build Pi if it is NULL
)
- Selects pairs from a relation R(x,y) (given as a BDD)
in such a way that a given x appears in one pair only. Uses a
priority function to determine which y should be paired to a given x.
Cudd_PrioritySelect returns a pointer to
the selected function if successful; NULL otherwise.
Three of the arguments--x, y, and z--are vectors of BDD variables.
The first two are the variables on which R depends. The third vectore
is a vector of auxiliary variables, used during the computation. This
vector is optional. If a NULL value is passed instead,
Cudd_PrioritySelect will create the working variables on the fly.
The sizes of x and y (and z if it is not NULL) should equal n.
The priority function Pi can be passed as a BDD, or can be built by
Cudd_PrioritySelect. If NULL is passed instead of a DdNode *,
parameter Pifunc is used by Cudd_PrioritySelect to build a BDD for the
priority function. (Pifunc is a pointer to a C function.) If Pi is not
NULL, then Pifunc is ignored. Pifunc should have the same interface as
the standard priority functions (e.g., Cudd_Dxygtdxz).
Cudd_PrioritySelect and Cudd_CProjection can sometimes be used
interchangeably. Specifically, calling Cudd_PrioritySelect with
Cudd_Xgty as Pifunc produces the same result as calling
Cudd_CProjection with the all-zero minterm as reference minterm.
However, depending on the application, one or the other may be
preferable:
- When extracting representatives from an equivalence relation,
Cudd_CProjection has the advantage of nor requiring the auxiliary
variables.
- When computing matchings in general bipartite graphs,
Cudd_PrioritySelect normally obtains better results because it can use
more powerful matching schemes (e.g., Cudd_Dxygtdxz).
- Side Effects If called with z == NULL, will create new variables in
the manager.
- See Also
Cudd_Dxygtdxz
Cudd_Dxygtdyz
Cudd_Xgty
Cudd_bddAdjPermuteX
Cudd_CProjection
- Defined in
cuddPriority.c
void
Cudd_Quit(
DdManager * unique
)
- Deletes resources associated with a DD manager and
resets the global statistical counters. (Otherwise, another manaqger
subsequently created would inherit the stats of this one.)
- Side Effects None
- See Also
Cudd_Init
- Defined in
cuddInit.c
long
Cudd_Random(
)
- Portable number generator based on ran2 from "Numerical
Recipes in C." It is a long period (> 2 * 10^18) random number generator
of L'Ecuyer with Bays-Durham shuffle. Returns a long integer uniformly
distributed between 0 and<PHONE_NUMBER> (inclusive of the endpoint values).
The random generator can be explicitly initialized by calling
Cudd_Srandom. If no explicit initialization is performed, then the
seed 1 is assumed.
- Side Effects None
- See Also
Cudd_Srandom
- Defined in
cuddUtil.c
int
Cudd_ReadArcviolation(
DdManager * dd
)
- Returns the current value of the arcviolation
parameter. This parameter is used in group sifting to decide how
many arcs into
y
not coming from x
are
tolerable when checking for aggregation due to extended
symmetry. The value should be between 0 and 100. A small value
causes fewer variables to be aggregated. The default value is 0.
- Side Effects None
- See Also
Cudd_SetArcviolation
- Defined in
cuddAPI.c
DdNode *
Cudd_ReadBackground(
DdManager * dd
)
- Reads the background constant of the manager.
- Side Effects None
- Defined in
cuddAPI.c
double
Cudd_ReadCacheHits(
DdManager * dd
)
- Returns the number of cache hits.
- Side Effects None
- See Also
Cudd_ReadCacheLookUps
- Defined in
cuddAPI.c
double
Cudd_ReadCacheLookUps(
DdManager * dd
)
- Returns the number of cache look-ups.
- Side Effects None
- See Also
Cudd_ReadCacheHits
- Defined in
cuddAPI.c
unsigned int
Cudd_ReadCacheSlots(
DdManager * dd
)
- Reads the number of slots in the cache.
- Side Effects None
- See Also
Cudd_ReadCacheUsedSlots
- Defined in
cuddAPI.c
double
Cudd_ReadCacheUsedSlots(
DdManager * dd
)
- Reads the fraction of used slots in the cache. The unused
slots are those in which no valid data is stored. Garbage collection,
variable reordering, and cache resizing may cause used slots to become
unused.
- Side Effects None
- See Also
Cudd_ReadCacheSlots
- Defined in
cuddAPI.c
unsigned int
Cudd_ReadDead(
DdManager * dd
)
- Returns the number of dead nodes in the unique table.
- Side Effects None
- See Also
Cudd_ReadKeys
- Defined in
cuddAPI.c
CUDD_VALUE_TYPE
Cudd_ReadEpsilon(
DdManager * dd
)
- Reads the epsilon parameter of the manager. The epsilon
parameter control the comparison between floating point numbers.
- Side Effects None
- See Also
Cudd_SetEpsilon
- Defined in
cuddAPI.c
Cudd_ErrorType
Cudd_ReadErrorCode(
DdManager * dd
)
- Returns the code of the last error. The error codes are
defined in cudd.h.
- Side Effects None
- See Also
Cudd_ClearErrorCode
- Defined in
cuddAPI.c
long
Cudd_ReadGarbageCollectionTime(
DdManager * dd
)
- Returns the number of milliseconds spent doing garbage
collection since the manager was initialized.
- Side Effects None
- See Also
Cudd_ReadGarbageCollections
- Defined in
cuddAPI.c
int
Cudd_ReadGarbageCollections(
DdManager * dd
)
- Returns the number of times garbage collection has
occurred in the manager. The number includes both the calls from
reordering procedures and those caused by requests to create new
nodes.
- Side Effects None
- See Also
Cudd_ReadGarbageCollectionTime
- Defined in
cuddAPI.c
Cudd_AggregationType
Cudd_ReadGroupcheck(
DdManager * dd
)
- Reads the groupcheck parameter of the manager. The
groupcheck parameter determines the aggregation criterion in group
sifting.
- Side Effects None
- See Also
Cudd_SetGroupcheck
- Defined in
cuddAPI.c
int
Cudd_ReadInvPermZdd(
DdManager * dd,
int i
)
- Returns the index of the ZDD variable currently in the
i-th position of the order. If the index is CUDD_CONST_INDEX, returns
CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.
- Side Effects None
- See Also
Cudd_ReadPerm
Cudd_ReadInvPermZdd
- Defined in
cuddAPI.c
int
Cudd_ReadInvPerm(
DdManager * dd,
int i
)
- Returns the index of the variable currently in the i-th
position of the order. If the index is CUDD_CONST_INDEX, returns
CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.
- Side Effects None
- See Also
Cudd_ReadPerm
Cudd_ReadInvPermZdd
- Defined in
cuddAPI.c
int
Cudd_ReadIthClause(
DdTlcInfo * tlc,
int i,
DdHalfWord * var1,
DdHalfWord * var2,
int * phase1,
int * phase2
)
- Accesses the i-th clause of a DD given the clause set which
must be already computed. Returns 1 if successful; 0 if i is out of range,
or in case of error.
- Side Effects the four components of a clause are returned as side effects.
- See Also
Cudd_FindTwoLiteralClauses
- Defined in
cuddEssent.c
unsigned int
Cudd_ReadKeys(
DdManager * dd
)
- Returns the total number of nodes currently in the unique
table, including the dead nodes.
- Side Effects None
- See Also
Cudd_ReadDead
- Defined in
cuddAPI.c
int
Cudd_ReadLinear(
DdManager * table, CUDD manager
int x, row index
int y column index
)
- Reads an entry of the linear transform matrix.
- Side Effects none
- Defined in
cuddLinear.c
DdNode *
Cudd_ReadLogicZero(
DdManager * dd
)
- Returns the zero constant of the manager. The logic zero
constant is the complement of the one constant, and is distinct from
the arithmetic zero.
- Side Effects None
- See Also
Cudd_ReadOne
Cudd_ReadZero
- Defined in
cuddAPI.c
unsigned int
Cudd_ReadLooseUpTo(
DdManager * dd
)
- Reads the looseUpTo parameter of the manager.
- Side Effects None
- See Also
Cudd_SetLooseUpTo
Cudd_ReadMinHit
Cudd_ReadMinDead
- Defined in
cuddAPI.c
unsigned int
Cudd_ReadMaxCacheHard(
DdManager * dd
)
- Reads the maxCacheHard parameter of the manager.
- Side Effects None
- See Also
Cudd_SetMaxCacheHard
Cudd_ReadMaxCache
- Defined in
cuddAPI.c
unsigned int
Cudd_ReadMaxCache(
DdManager * dd
)
- Returns the soft limit for the cache size. The soft limit
- Side Effects None
- See Also
Cudd_ReadMaxCache
- Defined in
cuddAPI.c
double
Cudd_ReadMaxGrowthAlternate(
DdManager * dd
)
- Reads the maxGrowthAlt parameter of the manager. This
parameter is analogous to the maxGrowth paramter, and is used every
given number of reorderings instead of maxGrowth. The number of
reorderings is set with Cudd_SetReorderingCycle. If the number of
reorderings is 0 (default) maxGrowthAlt is never used.
- Side Effects None
- See Also
Cudd_ReadMaxGrowth
Cudd_SetMaxGrowthAlternate
Cudd_SetReorderingCycle
Cudd_ReadReorderingCycle
- Defined in
cuddAPI.c
double
Cudd_ReadMaxGrowth(
DdManager * dd
)
- Reads the maxGrowth parameter of the manager. This
parameter determines how much the number of nodes can grow during
sifting of a variable. Overall, sifting never increases the size of
the decision diagrams. This parameter only refers to intermediate
results. A lower value will speed up sifting, possibly at the
expense of quality.
- Side Effects None
- See Also
Cudd_SetMaxGrowth
Cudd_ReadMaxGrowthAlternate
- Defined in
cuddAPI.c
unsigned int
Cudd_ReadMaxLive(
DdManager * dd
)
- Reads the maximum allowed number of live nodes. When this
number is exceeded, the package returns NULL.
- Side Effects none
- See Also
Cudd_SetMaxLive
- Defined in
cuddAPI.c
unsigned long
Cudd_ReadMaxMemory(
DdManager * dd
)
- Reads the maximum allowed memory. When this
number is exceeded, the package returns NULL.
- Side Effects none
- See Also
Cudd_SetMaxMemory
- Defined in
cuddAPI.c
unsigned long
Cudd_ReadMemoryInUse(
DdManager * dd
)
- Returns the memory in use by the manager measured in bytes.
- Side Effects None
- Defined in
cuddAPI.c
unsigned int
Cudd_ReadMinDead(
DdManager * dd
)
- Reads the minDead parameter of the manager. The minDead
parameter is used by the package to decide whether to collect garbage
or resize a subtable of the unique table when the subtable becomes
too full. The application can indirectly control the value of minDead
by setting the looseUpTo parameter.
- Side Effects None
- See Also
Cudd_ReadDead
Cudd_ReadLooseUpTo
Cudd_SetLooseUpTo
- Defined in
cuddAPI.c
unsigned int
Cudd_ReadMinHit(
DdManager * dd
)
- Reads the hit rate that causes resizinig of the computed
table.
- Side Effects None
- See Also
Cudd_SetMinHit
- Defined in
cuddAPI.c
DdNode *
Cudd_ReadMinusInfinity(
DdManager * dd
)
- Reads the minus-infinity constant from the manager.
- Side Effects None
- Defined in
cuddAPI.c
unsigned int
Cudd_ReadNextReordering(
DdManager * dd
)
- Returns the threshold for the next dynamic reordering.
The threshold is in terms of number of nodes and is in effect only
if reordering is enabled. The count does not include the dead nodes,
unless the countDead parameter of the manager has been changed from
its default setting.
- Side Effects None
- See Also
Cudd_SetNextReordering
- Defined in
cuddAPI.c
long
Cudd_ReadNodeCount(
DdManager * dd
)
- Reports the number of live nodes in BDDs and ADDs. This
number does not include the isolated projection functions and the
unused constants. These nodes that are not counted are not part of
the DDs manipulated by the application.
- Side Effects None
- See Also
Cudd_ReadPeakNodeCount
Cudd_zddReadNodeCount
- Defined in
cuddAPI.c
double
Cudd_ReadNodesDropped(
DdManager * dd
)
- Returns the number of nodes killed by dereferencing if the
keeping of this statistic is enabled; -1 otherwise. This statistic is
enabled only if the package is compiled with DD_STATS defined.
- Side Effects None
- See Also
Cudd_ReadNodesFreed
- Defined in
cuddAPI.c
double
Cudd_ReadNodesFreed(
DdManager * dd
)
- Returns the number of nodes returned to the free list if the
keeping of this statistic is enabled; -1 otherwise. This statistic is
enabled only if the package is compiled with DD_STATS defined.
- Side Effects None
- See Also
Cudd_ReadNodesDropped
- Defined in
cuddAPI.c
int
Cudd_ReadNumberXovers(
DdManager * dd
)
- Reads the current number of crossovers used by the
genetic algorithm for variable reordering. A larger number of crossovers will
cause the genetic algorithm to take more time, but will generally
produce better results. The default value is 0, in which case the
package uses three times the number of variables as number of crossovers,
with a maximum of 60.
- Side Effects None
- See Also
Cudd_SetNumberXovers
- Defined in
cuddAPI.c
DdNode *
Cudd_ReadOne(
DdManager * dd
)
- Returns the one constant of the manager. The one
constant is common to ADDs and BDDs.
- Side Effects None
- See Also
Cudd_ReadZero
Cudd_ReadLogicZero
Cudd_ReadZddOne
- Defined in
cuddAPI.c
int
Cudd_ReadPeakLiveNodeCount(
DdManager * dd
)
- Reports the peak number of live nodes. This count is kept
only if CUDD is compiled with DD_STATS defined. If DD_STATS is not
defined, this function returns -1.
- Side Effects None
- See Also
Cudd_ReadNodeCount
Cudd_PrintInfo
Cudd_ReadPeakNodeCount
- Defined in
cuddAPI.c
long
Cudd_ReadPeakNodeCount(
DdManager * dd
)
- Reports the peak number of nodes. This number includes
node on the free list. At the peak, the number of nodes on the free
list is guaranteed to be less than DD_MEM_CHUNK.
- Side Effects None
- See Also
Cudd_ReadNodeCount
Cudd_PrintInfo
- Defined in
cuddAPI.c
int
Cudd_ReadPermZdd(
DdManager * dd,
int i
)
- Returns the current position of the i-th ZDD variable
in the order. If the index is CUDD_CONST_INDEX, returns
CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns
-1.
- Side Effects None
- See Also
Cudd_ReadInvPermZdd
Cudd_ReadPerm
- Defined in
cuddAPI.c
int
Cudd_ReadPerm(
DdManager * dd,
int i
)
- Returns the current position of the i-th variable in
the order. If the index is CUDD_CONST_INDEX, returns
CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns
-1.
- Side Effects None
- See Also
Cudd_ReadInvPerm
Cudd_ReadPermZdd
- Defined in
cuddAPI.c
DdNode *
Cudd_ReadPlusInfinity(
DdManager * dd
)
- Reads the plus-infinity constant from the manager.
- Side Effects None
- Defined in
cuddAPI.c
int
Cudd_ReadPopulationSize(
DdManager * dd
)
- Reads the current size of the population used by the
genetic algorithm for variable reordering. A larger population size will
cause the genetic algorithm to take more time, but will generally
produce better results. The default value is 0, in which case the
package uses three times the number of variables as population size,
with a maximum of 120.
- Side Effects None
- See Also
Cudd_SetPopulationSize
- Defined in
cuddAPI.c
int
Cudd_ReadRecomb(
DdManager * dd
)
- Returns the current value of the recombination
parameter used in group sifting. A larger (positive) value makes the
aggregation of variables due to the second difference criterion more
likely. A smaller (negative) value makes aggregation less likely.
- Side Effects None
- See Also
Cudd_SetRecomb
- Defined in
cuddAPI.c
double
Cudd_ReadRecursiveCalls(
DdManager * dd
)
- Returns the number of recursive calls if the package is
compiled with DD_COUNT defined.
- Side Effects None
- Defined in
cuddAPI.c
int
Cudd_ReadReorderingCycle(
DdManager * dd
)
- Reads the reordCycle parameter of the manager. This
parameter determines how often the alternate threshold on maximum
growth is used in reordering.
- Side Effects None
- See Also
Cudd_ReadMaxGrowthAlternate
Cudd_SetMaxGrowthAlternate
Cudd_SetReorderingCycle
- Defined in
cuddAPI.c
long
Cudd_ReadReorderingTime(
DdManager * dd
)
- Returns the number of milliseconds spent reordering
variables since the manager was initialized. The time spent in collecting
garbage before reordering is included.
- Side Effects None
- See Also
Cudd_ReadReorderings
- Defined in
cuddAPI.c
int
Cudd_ReadReorderings(
DdManager * dd
)
- Returns the number of times reordering has occurred in the
manager. The number includes both the calls to Cudd_ReduceHeap from
the application program and those automatically performed by the
package. However, calls that do not even initiate reordering are not
counted. A call may not initiate reordering if there are fewer than
minsize live nodes in the manager, or if CUDD_REORDER_NONE is specified
as reordering method. The calls to Cudd_ShuffleHeap are not counted.
- Side Effects None
- See Also
Cudd_ReduceHeap
Cudd_ReadReorderingTime
- Defined in
cuddAPI.c
int
Cudd_ReadSiftMaxSwap(
DdManager * dd
)
- Reads the siftMaxSwap parameter of the manager. This
parameter gives the maximum number of swaps that will be attempted
for each invocation of sifting. The real number of swaps may exceed
the set limit because the package will always complete the sifting
of the variable that causes the limit to be reached.
- Side Effects None
- See Also
Cudd_ReadSiftMaxVar
Cudd_SetSiftMaxSwap
- Defined in
cuddAPI.c
int
Cudd_ReadSiftMaxVar(
DdManager * dd
)
- Reads the siftMaxVar parameter of the manager. This
parameter gives the maximum number of variables that will be sifted
for each invocation of sifting.
- Side Effects None
- See Also
Cudd_ReadSiftMaxSwap
Cudd_SetSiftMaxVar
- Defined in
cuddAPI.c
int
Cudd_ReadSize(
DdManager * dd
)
- Returns the number of BDD variables in existance.
- Side Effects None
- See Also
Cudd_ReadZddSize
- Defined in
cuddAPI.c
unsigned int
Cudd_ReadSlots(
DdManager * dd
)
- Returns the total number of slots of the unique table.
This number ismainly for diagnostic purposes.
- Side Effects None
- Defined in
cuddAPI.c
FILE *
Cudd_ReadStderr(
DdManager * dd
)
- Reads the stderr of a manager. This is the file pointer to
which messages normally going to stderr are written. It is initialized
to stderr. Cudd_SetStderr allows the application to redirect it.
- Side Effects None
- See Also
Cudd_SetStderr
Cudd_ReadStdout
- Defined in
cuddAPI.c
FILE *
Cudd_ReadStdout(
DdManager * dd
)
- Reads the stdout of a manager. This is the file pointer to
which messages normally going to stdout are written. It is initialized
to stdout. Cudd_SetStdout allows the application to redirect it.
- Side Effects None
- See Also
Cudd_SetStdout
Cudd_ReadStderr
- Defined in
cuddAPI.c
double
Cudd_ReadSwapSteps(
DdManager * dd
)
- Reads the number of elementary reordering steps.
- Side Effects none
- Defined in
cuddAPI.c
int
Cudd_ReadSymmviolation(
DdManager * dd
)
- Returns the current value of the symmviolation
parameter. This parameter is used in group sifting to decide how
many violations to the symmetry conditions
f10 = f01
or
f11 = f00
are tolerable when checking for aggregation
due to extended symmetry. The value should be between 0 and 100. A
small value causes fewer variables to be aggregated. The default
value is 0.
- Side Effects None
- See Also
Cudd_SetSymmviolation
- Defined in
cuddAPI.c
MtrNode *
Cudd_ReadTree(
DdManager * dd
)
- Returns the variable group tree of the manager.
- Side Effects None
- See Also
Cudd_SetTree
Cudd_FreeTree
Cudd_ReadZddTree
- Defined in
cuddAPI.c
double
Cudd_ReadUniqueLinks(
DdManager * dd
)
- Returns the number of links followed during look-ups in the
unique table if the keeping of this statistic is enabled; -1 otherwise.
If an item is found in the first position of its collision list, the
number of links followed is taken to be 0. If it is in second position,
the number of links is 1, and so on. This statistic is enabled only if
the package is compiled with DD_UNIQUE_PROFILE defined.
- Side Effects None
- See Also
Cudd_ReadUniqueLookUps
- Defined in
cuddAPI.c
double
Cudd_ReadUniqueLookUps(
DdManager * dd
)
- Returns the number of look-ups in the unique table if the
keeping of this statistic is enabled; -1 otherwise. This statistic is
enabled only if the package is compiled with DD_UNIQUE_PROFILE defined.
- Side Effects None
- See Also
Cudd_ReadUniqueLinks
- Defined in
cuddAPI.c
double
Cudd_ReadUsedSlots(
DdManager * dd
)
- Reads the fraction of used slots in the unique
table. The unused slots are those in which no valid data is
stored. Garbage collection, variable reordering, and subtable
resizing may cause used slots to become unused.
- Side Effects None
- See Also
Cudd_ReadSlots
- Defined in
cuddAPI.c
DdNode *
Cudd_ReadVars(
DdManager * dd,
int i
)
- Returns the i-th element of the vars array if it falls
within the array bounds; NULL otherwise. If i is the index of an
existing variable, this function produces the same result as
Cudd_bddIthVar. However, if the i-th var does not exist yet,
Cudd_bddIthVar will create it, whereas Cudd_ReadVars will not.
- Side Effects None
- See Also
Cudd_bddIthVar
- Defined in
cuddAPI.c
DdNode *
Cudd_ReadZddOne(
DdManager * dd,
int i
)
- Returns the ZDD for the constant 1 function.
The representation of the constant 1 function as a ZDD depends on
how many variables it (nominally) depends on. The index of the
topmost variable in the support is given as argument
i
.
- Side Effects None
- See Also
Cudd_ReadOne
- Defined in
cuddAPI.c
int
Cudd_ReadZddSize(
DdManager * dd
)
- Returns the number of ZDD variables in existance.
- Side Effects None
- See Also
Cudd_ReadSize
- Defined in
cuddAPI.c
MtrNode *
Cudd_ReadZddTree(
DdManager * dd
)
- Returns the variable group tree of the manager.
- Side Effects None
- See Also
Cudd_SetZddTree
Cudd_FreeZddTree
Cudd_ReadTree
- Defined in
cuddAPI.c
DdNode *
Cudd_ReadZero(
DdManager * dd
)
- Returns the zero constant of the manager. The zero
constant is the arithmetic zero, rather than the logic zero. The
latter is the complement of the one constant.
- Side Effects None
- See Also
Cudd_ReadOne
Cudd_ReadLogicZero
- Defined in
cuddAPI.c
void
Cudd_RecursiveDerefZdd(
DdManager * table,
DdNode * n
)
- Decreases the reference count of ZDD node n. If n dies,
recursively decreases the reference counts of its children. It is
used to dispose of a ZDD that is no longer needed.
- Side Effects None
- See Also
Cudd_Deref
Cudd_Ref
Cudd_RecursiveDeref
- Defined in
cuddRef.c
void
Cudd_RecursiveDeref(
DdManager * table,
DdNode * n
)
- Decreases the reference count of node n. If n dies,
recursively decreases the reference counts of its children. It is
used to dispose of a DD that is no longer needed.
- Side Effects None
- See Also
Cudd_Deref
Cudd_Ref
Cudd_RecursiveDerefZdd
- Defined in
cuddRef.c
int
Cudd_ReduceHeap(
DdManager * table, DD manager
Cudd_ReorderingType heuristic, method used for reordering
int minsize bound below which no reordering occurs
)
- Main dynamic reordering routine.
Calls one of the possible reordering procedures:
- Swapping
- Sifting
- Symmetric Sifting
- Group Sifting
- Window Permutation
- Simulated Annealing
- Genetic Algorithm
- Dynamic Programming (exact)
For sifting, symmetric sifting, group sifting, and window
permutation it is possible to request reordering to convergence.
The core of all methods is the reordering procedure
cuddSwapInPlace() which swaps two adjacent variables and is based
on Rudell's paper.
Returns 1 in case of success; 0 otherwise. In the case of symmetric
sifting (with and without convergence) returns 1 plus the number of
symmetric variables, in case of success.
- Side Effects Changes the variable order for all diagrams and clears
the cache.
- Defined in
cuddReorder.c
void
Cudd_Ref(
DdNode * n
)
- Increases the reference count of a node, if it is not
saturated.
- Side Effects None
- See Also
Cudd_RecursiveDeref
Cudd_Deref
- Defined in
cuddRef.c
DdNode *
Cudd_RemapOverApprox(
DdManager * dd, manager
DdNode * f, function to be superset
int numVars, number of variables in the support of f
int threshold, when to stop approximation
double quality minimum improvement for accepted changes
)
- Extracts a dense superset from a BDD. The procedure is
identical to the underapproximation procedure except for the fact that it
works on the complement of the given function. Extracting the subset
of the complement function is equivalent to extracting the superset
of the function.
Returns a pointer to the BDD of the superset if successful. NULL if
intermediate result causes the procedure to run out of memory. The
parameter numVars is the maximum number of variables to be used in
minterm calculation. The optimal number
should be as close as possible to the size of the support of f.
However, it is safe to pass the value returned by Cudd_ReadSize for
numVars when the number of variables is under 1023. If numVars is
larger than 1023, it will overflow. If a 0 parameter is passed then
the procedure will compute a value which will avoid overflow but
will cause underflow with 2046 variables or more.
- Side Effects None
- See Also
Cudd_SupersetHeavyBranch
Cudd_SupersetShortPaths
Cudd_ReadSize
- Defined in
cuddApprox.c
DdNode *
Cudd_RemapUnderApprox(
DdManager * dd, manager
DdNode * f, function to be subset
int numVars, number of variables in the support of f
int threshold, when to stop approximation
double quality minimum improvement for accepted changes
)
- Extracts a dense subset from a BDD. This procedure uses
a remapping technique and density as the cost function.
Returns a pointer to the BDD of the subset if
successful. NULL if the procedure runs out of memory. The parameter
numVars is the maximum number of variables to be used in minterm
calculation. The optimal number should be as close as possible to
the size of the support of f. However, it is safe to pass the value
returned by Cudd_ReadSize for numVars when the number of variables
is under 1023. If numVars is larger than 1023, it will cause
overflow. If a 0 parameter is passed then the procedure will compute
a value which will avoid overflow but will cause underflow with 2046
variables or more.
- Side Effects None
- See Also
Cudd_SubsetShortPaths
Cudd_SubsetHeavyBranch
Cudd_UnderApprox
Cudd_ReadSize
- Defined in
cuddApprox.c
int
Cudd_RemoveHook(
DdManager * dd,
DD_HFP f,
Cudd_HookType where
)
- Removes a function from a hook. A hook is a list of
application-provided functions called on certain occasions by the
package. Returns 1 if successful; 0 the function was not in the list.
- Side Effects None
- See Also
Cudd_AddHook
- Defined in
cuddAPI.c
int
Cudd_ReorderingReporting(
DdManager * dd
)
- Returns 1 if reporting of reordering stats is enabled;
0 otherwise.
- Side Effects none
- See Also
Cudd_EnableReorderingReporting
Cudd_DisableReorderingReporting
- Defined in
cuddAPI.c
int
Cudd_ReorderingStatusZdd(
DdManager * unique,
Cudd_ReorderingType * method
)
- Reports the status of automatic dynamic reordering of
ZDDs. Parameter method is set to the ZDD reordering method currently
selected. Returns 1 if automatic reordering is enabled; 0
otherwise.
- Side Effects Parameter method is set to the ZDD reordering method currently
selected.
- See Also
Cudd_AutodynEnableZdd
Cudd_AutodynDisableZdd
Cudd_ReorderingStatus
- Defined in
cuddAPI.c
int
Cudd_ReorderingStatus(
DdManager * unique,
Cudd_ReorderingType * method
)
- Reports the status of automatic dynamic reordering of
BDDs and ADDs. Parameter method is set to the reordering method
currently selected. Returns 1 if automatic reordering is enabled; 0
otherwise.
- Side Effects Parameter method is set to the reordering method currently
selected.
- See Also
Cudd_AutodynEnable
Cudd_AutodynDisable
Cudd_ReorderingStatusZdd
- Defined in
cuddAPI.c
void
Cudd_SetArcviolation(
DdManager * dd,
int arcviolation
)
- Sets the value of the arcviolation
parameter. This parameter is used in group sifting to decide how
many arcs into
y
not coming from x
are
tolerable when checking for aggregation due to extended
symmetry. The value should be between 0 and 100. A small value
causes fewer variables to be aggregated. The default value is 0.
- Side Effects None
- See Also
Cudd_ReadArcviolation
- Defined in
cuddAPI.c
void
Cudd_SetBackground(
DdManager * dd,
DdNode * bck
)
- Sets the background constant of the manager. It assumes
that the DdNode pointer bck is already referenced.
- Side Effects None
- Defined in
cuddAPI.c
void
Cudd_SetEpsilon(
DdManager * dd,
CUDD_VALUE_TYPE ep
)
- Sets the epsilon parameter of the manager to ep. The epsilon
parameter control the comparison between floating point numbers.
- Side Effects None
- See Also
Cudd_ReadEpsilon
- Defined in
cuddAPI.c
void
Cudd_SetGroupcheck(
DdManager * dd,
Cudd_AggregationType gc
)
- Sets the parameter groupcheck of the manager to gc. The
groupcheck parameter determines the aggregation criterion in group
sifting.
- Side Effects None
- See Also
Cudd_ReadGroupCheck
- Defined in
cuddAPI.c
void
Cudd_SetLooseUpTo(
DdManager * dd,
unsigned int lut
)
- Sets the looseUpTo parameter of the manager. This
parameter of the manager controls the threshold beyond which no fast
growth of the unique table is allowed. The threshold is given as a
number of slots. If the value passed to this function is 0, the
function determines a suitable value based on the available memory.
- Side Effects None
- See Also
Cudd_ReadLooseUpTo
Cudd_SetMinHit
- Defined in
cuddAPI.c
void
Cudd_SetMaxCacheHard(
DdManager * dd,
unsigned int mc
)
- Sets the maxCacheHard parameter of the manager. The
cache cannot grow larger than maxCacheHard entries. This parameter
allows an application to control the trade-off of memory versus
speed. If the value passed to this function is 0, the function
determines a suitable maximum cache size based on the available memory.
- Side Effects None
- See Also
Cudd_ReadMaxCacheHard
Cudd_SetMaxCache
- Defined in
cuddAPI.c
void
Cudd_SetMaxGrowthAlternate(
DdManager * dd,
double mg
)
- Sets the maxGrowthAlt parameter of the manager. This
parameter is analogous to the maxGrowth paramter, and is used every
given number of reorderings instead of maxGrowth. The number of
reorderings is set with Cudd_SetReorderingCycle. If the number of
reorderings is 0 (default) maxGrowthAlt is never used.
- Side Effects None
- See Also
Cudd_ReadMaxGrowthAlternate
Cudd_SetMaxGrowth
Cudd_SetReorderingCycle
Cudd_ReadReorderingCycle
- Defined in
cuddAPI.c
void
Cudd_SetMaxGrowth(
DdManager * dd,
double mg
)
- Sets the maxGrowth parameter of the manager. This
parameter determines how much the number of nodes can grow during
sifting of a variable. Overall, sifting never increases the size of
the decision diagrams. This parameter only refers to intermediate
results. A lower value will speed up sifting, possibly at the
expense of quality.
- Side Effects None
- See Also
Cudd_ReadMaxGrowth
Cudd_SetMaxGrowthAlternate
- Defined in
cuddAPI.c
void
Cudd_SetMaxLive(
DdManager * dd,
unsigned int maxLive
)
- Sets the maximum allowed number of live nodes. When this
number is exceeded, the package returns NULL.
- Side Effects none
- See Also
Cudd_ReadMaxLive
- Defined in
cuddAPI.c
void
Cudd_SetMaxMemory(
DdManager * dd,
unsigned long maxMemory
)
- Sets the maximum allowed memory. When this
number is exceeded, the package returns NULL.
- Side Effects none
- See Also
Cudd_ReadMaxMemory
- Defined in
cuddAPI.c
void
Cudd_SetMinHit(
DdManager * dd,
unsigned int hr
)
- Sets the minHit parameter of the manager. This
parameter controls the resizing of the computed table. If the hit
rate is larger than the specified value, and the cache is not
already too large, then its size is doubled.
- Side Effects None
- See Also
Cudd_ReadMinHit
- Defined in
cuddAPI.c
void
Cudd_SetNextReordering(
DdManager * dd,
unsigned int next
)
- Sets the threshold for the next dynamic reordering.
The threshold is in terms of number of nodes and is in effect only
if reordering is enabled. The count does not include the dead nodes,
unless the countDead parameter of the manager has been changed from
its default setting.
- Side Effects None
- See Also
Cudd_ReadNextReordering
- Defined in
cuddAPI.c
void
Cudd_SetNumberXovers(
DdManager * dd,
int numberXovers
)
- Sets the number of crossovers used by the genetic
algorithm for variable reordering. A larger number of crossovers
will cause the genetic algorithm to take more time, but will
generally produce better results. The default value is 0, in which
case the package uses three times the number of variables as number
of crossovers, with a maximum of 60.
- Side Effects None
- See Also
Cudd_ReadNumberXovers
- Defined in
cuddAPI.c
void
Cudd_SetPopulationSize(
DdManager * dd,
int populationSize
)
- Sets the size of the population used by the
genetic algorithm for variable reordering. A larger population size will
cause the genetic algorithm to take more time, but will generally
produce better results. The default value is 0, in which case the
package uses three times the number of variables as population size,
with a maximum of 120.
- Side Effects Changes the manager.
- See Also
Cudd_ReadPopulationSize
- Defined in
cuddAPI.c
void
Cudd_SetRecomb(
DdManager * dd,
int recomb
)
- Sets the value of the recombination parameter used in
group sifting. A larger (positive) value makes the aggregation of
variables due to the second difference criterion more likely. A
smaller (negative) value makes aggregation less likely. The default
value is 0.
- Side Effects Changes the manager.
- See Also
Cudd_ReadRecomb
- Defined in
cuddAPI.c
void
Cudd_SetReorderingCycle(
DdManager * dd,
int cycle
)
- Sets the reordCycle parameter of the manager. This
parameter determines how often the alternate threshold on maximum
growth is used in reordering.
- Side Effects None
- See Also
Cudd_ReadMaxGrowthAlternate
Cudd_SetMaxGrowthAlternate
Cudd_ReadReorderingCycle
- Defined in
cuddAPI.c
void
Cudd_SetSiftMaxSwap(
DdManager * dd,
int sms
)
- Sets the siftMaxSwap parameter of the manager. This
parameter gives the maximum number of swaps that will be attempted
for each invocation of sifting. The real number of swaps may exceed
the set limit because the package will always complete the sifting
of the variable that causes the limit to be reached.
- Side Effects None
- See Also
Cudd_SetSiftMaxVar
Cudd_ReadSiftMaxSwap
- Defined in
cuddAPI.c
void
Cudd_SetSiftMaxVar(
DdManager * dd,
int smv
)
- Sets the siftMaxVar parameter of the manager. This
parameter gives the maximum number of variables that will be sifted
for each invocation of sifting.
- Side Effects None
- See Also
Cudd_SetSiftMaxSwap
Cudd_ReadSiftMaxVar
- Defined in
cuddAPI.c
void
Cudd_SetStderr(
DdManager * dd,
FILE * fp
)
- Sets the stderr of a manager.
- Side Effects None
- See Also
Cudd_ReadStderr
Cudd_SetStdout
- Defined in
cuddAPI.c
void
Cudd_SetStdout(
DdManager * dd,
FILE * fp
)
- Sets the stdout of a manager.
- Side Effects None
- See Also
Cudd_ReadStdout
Cudd_SetStderr
- Defined in
cuddAPI.c
void
Cudd_SetSymmviolation(
DdManager * dd,
int symmviolation
)
- Sets the value of the symmviolation
parameter. This parameter is used in group sifting to decide how
many violations to the symmetry conditions
f10 = f01
or
f11 = f00
are tolerable when checking for aggregation
due to extended symmetry. The value should be between 0 and 100. A
small value causes fewer variables to be aggregated. The default
value is 0.
- Side Effects Changes the manager.
- See Also
Cudd_ReadSymmviolation
- Defined in
cuddAPI.c
void
Cudd_SetTree(
DdManager * dd,
MtrNode * tree
)
- Sets the variable group tree of the manager.
- Side Effects None
- See Also
Cudd_FreeTree
Cudd_ReadTree
Cudd_SetZddTree
- Defined in
cuddAPI.c
int
Cudd_SetVarMap(
DdManager * manager, DD manager
DdNode ** x, first array of variables
DdNode ** y, second array of variables
int n length of both arrays
)
- Registers with the manager a variable mapping described
by two sets of variables. This variable mapping is then used by
functions like Cudd_bddVarMap. This function is convenient for
those applications that perform the same mapping several times.
However, if several different permutations are used, it may be more
efficient not to rely on the registered mapping, because changing
mapping causes the cache to be cleared. (The initial setting,
however, does not clear the cache.) The two sets of variables (x and
y) must have the same size (x and y). The size is given by n. The
two sets of variables are normally disjoint, but this restriction is
not imposeded by the function. When new variables are created, the
map is automatically extended (each new variable maps to
itself). The typical use, however, is to wait until all variables
are created, and then create the map. Returns 1 if the mapping is
successfully registered with the manager; 0 otherwise.
- Side Effects Modifies the manager. May clear the cache.
- See Also
Cudd_bddVarMap
Cudd_bddPermute
Cudd_bddSwapVariables
- Defined in
cuddCompose.c
void
Cudd_SetZddTree(
DdManager * dd,
MtrNode * tree
)
- Sets the ZDD variable group tree of the manager.
- Side Effects None
- See Also
Cudd_FreeZddTree
Cudd_ReadZddTree
Cudd_SetTree
- Defined in
cuddAPI.c
int
Cudd_SharingSize(
DdNode ** nodeArray,
int n
)
- Counts the number of nodes in an array of DDs. Shared
nodes are counted only once. Returns the total number of nodes.
- Side Effects None
- See Also
Cudd_DagSize
- Defined in
cuddUtil.c
int
Cudd_ShortestLength(
DdManager * manager,
DdNode * f,
int * weight
)
- Find the length of the shortest path(s) in a DD. f is
the DD we want to get the shortest path for; weight[i] is the
weight of the THEN edge coming from the node whose index is i. All
ELSE edges have 0 weight. Returns the length of the shortest
path(s) if such a path is found; a large number if the function is
identically 0, and CUDD_OUT_OF_MEM in case of failure.
- Side Effects None
- See Also
Cudd_ShortestPath
- Defined in
cuddSat.c
DdNode *
Cudd_ShortestPath(
DdManager * manager,
DdNode * f,
int * weight,
int * support,
int * length
)
- Finds a shortest path in a DD. f is the DD we want to
get the shortest path for; weight[i] is the weight of the THEN arc
coming from the node whose index is i. If weight is NULL, then unit
weights are assumed for all THEN arcs. All ELSE arcs have 0 weight.
If non-NULL, both weight and support should point to arrays with at
least as many entries as there are variables in the manager.
Returns the shortest path as the BDD of a cube.
- Side Effects support contains on return the true support of f.
If support is NULL on entry, then Cudd_ShortestPath does not compute
the true support info. length contains the length of the path.
- See Also
Cudd_ShortestLength
Cudd_LargestCube
- Defined in
cuddSat.c
int
Cudd_ShuffleHeap(
DdManager * table, DD manager
int * permutation required variable permutation
)
- Reorders 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 variable order for all diagrams and clears
the cache.
- See Also
Cudd_ReduceHeap
- Defined in
cuddReorder.c
DdNode *
Cudd_SolveEqn(
DdManager * bdd,
DdNode * F, the left-hand side of the equation
DdNode * Y, the cube of the y variables
DdNode ** G, the array of solutions (return parameter)
int ** yIndex, index of y variables
int n numbers of unknowns
)
- Implements the solution for F(x,y) = 0. The return
value is the consistency condition. The y variables are the unknowns
and the remaining variables are the parameters. Returns the
consistency condition if successful; NULL otherwise. Cudd_SolveEqn
allocates an array and fills it with the indices of the
unknowns. This array is used by Cudd_VerifySol.
- Side Effects The solution is returned in G; the indices of the y
variables are returned in yIndex.
- See Also
Cudd_VerifySol
- Defined in
cuddSolve.c
DdNode *
Cudd_SplitSet(
DdManager * manager,
DdNode * S,
DdNode ** xVars,
int n,
double m
)
- Returns
m
minterms from a BDD whose
support has n
variables at most. The procedure tries
to create as few extra nodes as possible. The function represented
by S
depends on at most n
of the variables
in xVars
. Returns a BDD with m
minterms
of the on-set of S if successful; NULL otherwise.
- Side Effects None
- Defined in
cuddSplit.c
void
Cudd_Srandom(
long seed
)
- Initializer for the portable number generator based on
ran2 in "Numerical Recipes in C." The input is the seed for the
generator. If it is negative, its absolute value is taken as seed.
If it is 0, then 1 is taken as seed. The initialized sets up the two
recurrences used to generate a long-period stream, and sets up the
shuffle table.
- Side Effects None
- See Also
Cudd_Random
- Defined in
cuddUtil.c
int
Cudd_StdPostReordHook(
DdManager * dd,
const char * str,
void * data
)
- Sample hook function to call after reordering.
Prints on the manager's stdout final size and reordering time.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- See Also
Cudd_StdPreReordHook
- Defined in
cuddAPI.c
int
Cudd_StdPreReordHook(
DdManager * dd,
const char * str,
void * data
)
- Sample hook function to call before reordering.
Prints on the manager's stdout reordering method and initial size.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- See Also
Cudd_StdPostReordHook
- Defined in
cuddAPI.c
DdNode *
Cudd_SubsetCompress(
DdManager * dd, manager
DdNode * f, BDD whose subset is sought
int nvars, number of variables in the support of f
int threshold maximum number of nodes in the subset
)
- Finds a dense subset of BDD
f
. Density is
the ratio of number of minterms to number of nodes. Uses several
techniques in series. It is more expensive than other subsetting
procedures, but often produces better results. See
Cudd_SubsetShortPaths for a description of the threshold and nvars
parameters. Returns a pointer to the result if successful; NULL
otherwise.
- Side Effects None
- See Also
Cudd_SubsetRemap
Cudd_SubsetShortPaths
Cudd_SubsetHeavyBranch
Cudd_bddSqueeze
- Defined in
cuddGenCof.c
DdNode *
Cudd_SubsetHeavyBranch(
DdManager * dd, manager
DdNode * f, function to be subset
int numVars, number of variables in the support of f
int threshold maximum number of nodes in the subset
)
- Extracts a dense subset from a BDD. This procedure
builds a subset by throwing away one of the children of each node,
starting from the root, until the result is small enough. The child
that is eliminated from the result is the one that contributes the
fewer minterms. Returns a pointer to the BDD of the subset if
successful. NULL if the procedure runs out of memory. The parameter
numVars is the maximum number of variables to be used in minterm
calculation and node count calculation. The optimal number should
be as close as possible to the size of the support of f. However,
it is safe to pass the value returned by Cudd_ReadSize for numVars
when the number of variables is under 1023. If numVars is larger
than 1023, it will overflow. If a 0 parameter is passed then the
procedure will compute a value which will avoid overflow but will
cause underflow with 2046 variables or more.
- Side Effects None
- See Also
Cudd_SubsetShortPaths
Cudd_SupersetHeavyBranch
Cudd_ReadSize
- Defined in
cuddSubsetHB.c
DdNode *
Cudd_SubsetShortPaths(
DdManager * dd, manager
DdNode * f, function to be subset
int numVars, number of variables in the support of f
int threshold, maximum number of nodes in the subset
int hardlimit flag: 1 if threshold is a hard limit
)
- Extracts a dense subset from a BDD. This procedure
tries to preserve the shortest paths of the input BDD, because they
give many minterms and contribute few nodes. This procedure may
increase the number of nodes in trying to create the subset or
reduce the number of nodes due to recombination as compared to the
original BDD. Hence the threshold may not be strictly adhered to. In
practice, recombination overshadows the increase in the number of
nodes and results in small BDDs as compared to the threshold. The
hardlimit specifies whether threshold needs to be strictly adhered
to. If it is set to 1, the procedure ensures that result is never
larger than the specified limit but may be considerably less than
the threshold. Returns a pointer to the BDD for the subset if
successful; NULL otherwise. The value for numVars should be as
close as possible to the size of the support of f for better
efficiency. However, it is safe to pass the value returned by
Cudd_ReadSize for numVars. If 0 is passed, then the value returned
by Cudd_ReadSize is used.
- Side Effects None
- See Also
Cudd_SupersetShortPaths
Cudd_SubsetHeavyBranch
Cudd_ReadSize
- Defined in
cuddSubsetSP.c
DdNode *
Cudd_SubsetWithMaskVars(
DdManager * dd, manager
DdNode * f, function from which to pick a cube
DdNode ** vars, array of variables
int nvars, size of vars
DdNode ** maskVars, array of variables
int mvars size of maskVars
)
- Extracts a subset from a BDD in the following procedure.
1. Compute the weight for each mask variable by counting the number of
minterms for both positive and negative cofactors of the BDD with
respect to each mask variable. (weight = #positive - #negative)
2. Find a representative cube of the BDD by using the weight. From the
top variable of the BDD, for each variable, if the weight is greater
than 0.0, choose THEN branch, othereise ELSE branch, until meeting
the constant 1.
3. Quantify out the variables not in maskVars from the representative
cube and if a variable in maskVars is don't care, replace the
variable with a constant(1 or 0) depending on the weight.
4. Make a subset of the BDD by multiplying with the modified cube.
- Side Effects None
- Defined in
cuddUtil.c
DdNode *
Cudd_SupersetCompress(
DdManager * dd, manager
DdNode * f, BDD whose superset is sought
int nvars, number of variables in the support of f
int threshold maximum number of nodes in the superset
)
- Finds a dense superset of BDD
f
. Density is
the ratio of number of minterms to number of nodes. Uses several
techniques in series. It is more expensive than other supersetting
procedures, but often produces better results. See
Cudd_SupersetShortPaths for a description of the threshold and nvars
parameters. Returns a pointer to the result if successful; NULL
otherwise.
- Side Effects None
- See Also
Cudd_SubsetCompress
Cudd_SupersetRemap
Cudd_SupersetShortPaths
Cudd_SupersetHeavyBranch
Cudd_bddSqueeze
- Defined in
cuddGenCof.c
DdNode *
Cudd_SupersetHeavyBranch(
DdManager * dd, manager
DdNode * f, function to be superset
int numVars, number of variables in the support of f
int threshold maximum number of nodes in the superset
)
- Extracts a dense superset from a BDD. The procedure is
identical to the subset procedure except for the fact that it
receives the complement of the given function. Extracting the subset
of the complement function is equivalent to extracting the superset
of the function. This procedure builds a superset by throwing away
one of the children of each node starting from the root of the
complement function, until the result is small enough. The child
that is eliminated from the result is the one that contributes the
fewer minterms.
Returns a pointer to the BDD of the superset if successful. NULL if
intermediate result causes the procedure to run out of memory. The
parameter numVars is the maximum number of variables to be used in
minterm calculation and node count calculation. The optimal number
should be as close as possible to the size of the support of f.
However, it is safe to pass the value returned by Cudd_ReadSize for
numVars when the number of variables is under 1023. If numVars is
larger than 1023, it will overflow. If a 0 parameter is passed then
the procedure will compute a value which will avoid overflow but
will cause underflow with 2046 variables or more.
- Side Effects None
- See Also
Cudd_SubsetHeavyBranch
Cudd_SupersetShortPaths
Cudd_ReadSize
- Defined in
cuddSubsetHB.c
DdNode *
Cudd_SupersetShortPaths(
DdManager * dd, manager
DdNode * f, function to be superset
int numVars, number of variables in the support of f
int threshold, maximum number of nodes in the subset
int hardlimit flag: 1 if threshold is a hard limit
)
- Extracts a dense superset from a BDD. The procedure is
identical to the subset procedure except for the fact that it
receives the complement of the given function. Extracting the subset
of the complement function is equivalent to extracting the superset
of the function. This procedure tries to preserve the shortest
paths of the complement BDD, because they give many minterms and
contribute few nodes. This procedure may increase the number of
nodes in trying to create the superset or reduce the number of nodes
due to recombination as compared to the original BDD. Hence the
threshold may not be strictly adhered to. In practice, recombination
overshadows the increase in the number of nodes and results in small
BDDs as compared to the threshold. The hardlimit specifies whether
threshold needs to be strictly adhered to. If it is set to 1, the
procedure ensures that result is never larger than the specified
limit but may be considerably less than the threshold. Returns a
pointer to the BDD for the superset if successful; NULL
otherwise. The value for numVars should be as close as possible to
the size of the support of f for better efficiency. However, it is
safe to pass the value returned by Cudd_ReadSize for numVar. If 0
is passed, then the value returned by Cudd_ReadSize is used.
- Side Effects None
- See Also
Cudd_SubsetShortPaths
Cudd_SupersetHeavyBranch
Cudd_ReadSize
- Defined in
cuddSubsetSP.c
int *
Cudd_SupportIndex(
DdManager * dd, manager
DdNode * f DD whose support is sought
)
- Finds the variables on which a DD depends. Returns an
index array of the variables if successful; NULL otherwise. The
size of the array equals the number of variables in the manager.
Each entry of the array is 1 if the corresponding variable is in the
support of the DD and 0 otherwise.
- Side Effects None
- See Also
Cudd_Support
Cudd_VectorSupport
Cudd_ClassifySupport
- Defined in
cuddUtil.c
int
Cudd_SupportSize(
DdManager * dd, manager
DdNode * f DD whose support size is sought
)
- Counts the variables on which a DD depends.
Returns the number of the variables if successful; CUDD_OUT_OF_MEM
otherwise.
- Side Effects None
- See Also
Cudd_Support
- Defined in
cuddUtil.c
DdNode *
Cudd_Support(
DdManager * dd, manager
DdNode * f DD whose support is sought
)
- Finds the variables on which a DD depends.
Returns a BDD consisting of the product of the variables if
successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_VectorSupport
Cudd_ClassifySupport
- Defined in
cuddUtil.c
void
Cudd_SymmProfile(
DdManager * table,
int lower,
int upper
)
- Prints statistics on symmetric variables.
- Side Effects None
- Defined in
cuddSymmetry.c
void
Cudd_TurnOffCountDead(
DdManager * dd
)
- Causes the dead nodes not to be counted towards
triggering reordering. This causes less frequent reorderings. By
default dead nodes are not counted. Therefore there is no need to
call this function unless Cudd_TurnOnCountDead has been previously
called.
- Side Effects Changes the manager.
- See Also
Cudd_TurnOnCountDead
Cudd_DeadAreCounted
- Defined in
cuddAPI.c
void
Cudd_TurnOnCountDead(
DdManager * dd
)
- Causes the dead nodes to be counted towards triggering
reordering. This causes more frequent reorderings. By default dead
nodes are not counted.
- Side Effects Changes the manager.
- See Also
Cudd_TurnOffCountDead
Cudd_DeadAreCounted
- Defined in
cuddAPI.c
DdNode *
Cudd_UnderApprox(
DdManager * dd, manager
DdNode * f, function to be subset
int numVars, number of variables in the support of f
int threshold, when to stop approximation
int safe, enforce safe approximation
double quality minimum improvement for accepted changes
)
- Extracts a dense subset from a BDD. This procedure uses
a variant of Tom Shiple's underapproximation method. The main
difference from the original method is that density is used as cost
function. Returns a pointer to the BDD of the subset if
successful. NULL if the procedure runs out of memory. The parameter
numVars is the maximum number of variables to be used in minterm
calculation. The optimal number should be as close as possible to
the size of the support of f. However, it is safe to pass the value
returned by Cudd_ReadSize for numVars when the number of variables
is under 1023. If numVars is larger than 1023, it will cause
overflow. If a 0 parameter is passed then the procedure will compute
a value which will avoid overflow but will cause underflow with 2046
variables or more.
- Side Effects None
- See Also
Cudd_SubsetShortPaths
Cudd_SubsetHeavyBranch
Cudd_ReadSize
- Defined in
cuddApprox.c
int *
Cudd_VectorSupportIndex(
DdManager * dd, manager
DdNode ** F, array of DDs whose support is sought
int n size of the array
)
- Finds the variables on which a set of DDs depends.
The set must contain either BDDs and ADDs, or ZDDs.
Returns an index array of the variables if successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_SupportIndex
Cudd_VectorSupport
Cudd_ClassifySupport
- Defined in
cuddUtil.c
int
Cudd_VectorSupportSize(
DdManager * dd, manager
DdNode ** F, array of DDs whose support is sought
int n size of the array
)
- Counts the variables on which a set of DDs depends.
The set must contain either BDDs and ADDs, or ZDDs.
Returns the number of the variables if successful; CUDD_OUT_OF_MEM
otherwise.
- Side Effects None
- See Also
Cudd_VectorSupport
Cudd_SupportSize
- Defined in
cuddUtil.c
DdNode *
Cudd_VectorSupport(
DdManager * dd, manager
DdNode ** F, array of DDs whose support is sought
int n size of the array
)
- Finds the variables on which a set of DDs depends.
The set must contain either BDDs and ADDs, or ZDDs.
Returns a BDD consisting of the product of the variables if
successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_Support
Cudd_ClassifySupport
- Defined in
cuddUtil.c
DdNode *
Cudd_VerifySol(
DdManager * bdd,
DdNode * F, the left-hand side of the equation
DdNode ** G, the array of solutions
int * yIndex, index of y variables
int n numbers of unknowns
)
- Checks the solution of F(x,y) = 0. This procedure
substitutes the solution components for the unknowns of F and returns
the resulting BDD for F.
- Side Effects Frees the memory pointed by yIndex.
- See Also
Cudd_SolveEqn
- Defined in
cuddSolve.c
DdNode *
Cudd_Xeqy(
DdManager * dd, DD manager
int N, number of x and y variables
DdNode ** x, array of x variables
DdNode ** y array of y variables
)
- This function generates a BDD for the function x==y.
Both x and y are 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 BDD 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_addXeqy
- Defined in
cuddPriority.c
DdNode *
Cudd_Xgty(
DdManager * dd, DD manager
int N, number of x and y variables
DdNode ** z, array of z variables: unused
DdNode ** x, array of x variables
DdNode ** y array of y variables
)
- This function generates a BDD for the function x > y.
Both x and y are 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 BDD 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].
Argument z is not used by Cudd_Xgty: it is included to make it
call-compatible to Cudd_Dxygtdxz and Cudd_Dxygtdyz.
- Side Effects None
- See Also
Cudd_PrioritySelect
Cudd_Dxygtdxz
Cudd_Dxygtdyz
- Defined in
cuddPriority.c
DdNode *
Cudd_addAgreement(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
- Returns NULL if not a terminal case; f op g otherwise,
where f op g is f if f==g; background if f!=g.
- Side Effects None
- See Also
Cudd_addApply
- Defined in
cuddAddApply.c
DdNode *
Cudd_addApply(
DdManager * dd,
DD_AOP op,
DdNode * f,
DdNode * g
)
- Applies op to the corresponding discriminants of f and g.
Returns a pointer to the result if succssful; NULL otherwise.
- Side Effects None
- See Also
Cudd_addMonadicApply
Cudd_addPlus
Cudd_addTimes
Cudd_addThreshold
Cudd_addSetNZ
Cudd_addDivide
Cudd_addMinus
Cudd_addMinimum
Cudd_addMaximum
Cudd_addOneZeroMaximum
Cudd_addDiff
Cudd_addAgreement
Cudd_addOr
Cudd_addNand
Cudd_addNor
Cudd_addXor
Cudd_addXnor
- Defined in
cuddAddApply.c
DdNode *
Cudd_addBddInterval(
DdManager * dd,
DdNode * f,
CUDD_VALUE_TYPE lower,
CUDD_VALUE_TYPE upper
)
- Converts an ADD to a BDD by replacing all
discriminants greater than or equal to lower and less than or equal to
upper with 1, and all other discriminants with 0. Returns a pointer to
the resulting BDD if successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_addBddThreshold
Cudd_addBddStrictThreshold
Cudd_addBddPattern
Cudd_BddToAdd
- Defined in
cuddBridge.c
DdNode *
Cudd_addBddIthBit(
DdManager * dd,
DdNode * f,
int bit
)
- Converts an ADD to a BDD by replacing all
discriminants whose i-th bit is equal to 1 with 1, and all other
discriminants with 0. The i-th bit refers to the integer
representation of the leaf value. If the value is has a fractional
part, it is ignored. Repeated calls to this procedure allow one to
transform an integer-valued ADD into an array of BDDs, one for each
bit of the leaf values. Returns a pointer to the resulting BDD if
successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_addBddInterval
Cudd_addBddPattern
Cudd_BddToAdd
- Defined in
cuddBridge.c
DdNode *
Cudd_addBddPattern(
DdManager * dd,
DdNode * f
)
- Converts an ADD to a BDD by replacing all
discriminants different from 0 with 1. Returns a pointer to the
resulting BDD if successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_BddToAdd
Cudd_addBddThreshold
Cudd_addBddInterval
Cudd_addBddStrictThreshold
- Defined in
cuddBridge.c
DdNode *
Cudd_addBddStrictThreshold(
DdManager * dd,
DdNode * f,
CUDD_VALUE_TYPE value
)
- Converts an ADD to a BDD by replacing all
discriminants STRICTLY greater than value with 1, and all other
discriminants with 0. Returns a pointer to the resulting BDD if
successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_addBddInterval
Cudd_addBddPattern
Cudd_BddToAdd
Cudd_addBddThreshold
- Defined in
cuddBridge.c
DdNode *
Cudd_addBddThreshold(
DdManager * dd,
DdNode * f,
CUDD_VALUE_TYPE value
)
- Converts an ADD to a BDD by replacing all
discriminants greater than or equal to value with 1, and all other
discriminants with 0. Returns a pointer to the resulting BDD if
successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_addBddInterval
Cudd_addBddPattern
Cudd_BddToAdd
Cudd_addBddStrictThreshold
- Defined in
cuddBridge.c
DdNode *
Cudd_addCmpl(
DdManager * dd,
DdNode * f
)
- Computes the complement of an ADD a la C language: The
complement of 0 is 1 and the complement of everything else is 0.
Returns a pointer to the resulting ADD if successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_addNegate
- Defined in
cuddAddIte.c
DdNode *
Cudd_addCompose(
DdManager * dd,
DdNode * f,
DdNode * g,
int v
)
- Substitutes g for x_v in the ADD for f. v is the index of the
variable to be substituted. g must be a 0-1 ADD. Cudd_bddCompose passes
the corresponding projection function to the recursive procedure, so
that the cache may be used. Returns the composed ADD if successful;
NULL otherwise.
- Side Effects None
- See Also
Cudd_bddCompose
- Defined in
cuddCompose.c
DdNode *
Cudd_addComputeCube(
DdManager * dd,
DdNode ** vars,
int * phase,
int n
)
- Computes the cube of an array of ADD 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_bddComputeCube
- Defined in
cuddUtil.c
DdNode *
Cudd_addConstrain(
DdManager * dd,
DdNode * f,
DdNode * c
)
- Computes f constrain c (f @ c), for f an ADD and c a 0-1
ADD. List of special cases:
- F @ 0 = 0
- F @ 1 = F
- 0 @ c = 0
- 1 @ c = 1
- F @ F = 1
Returns a pointer to the result if successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_bddConstrain
- Defined in
cuddGenCof.c
DdNode *
Cudd_addConst(
DdManager * dd,
CUDD_VALUE_TYPE c
)
- Retrieves the ADD for constant c if it already
exists, or creates a new ADD. Returns a pointer to the
ADD if successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_addNewVar
Cudd_addIthVar
- Defined in
cuddAPI.c
DdNode *
Cudd_addDiff(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
- Returns NULL if not a terminal case; f op g otherwise,
where f op g is plusinfinity if f=g; min(f,g) if f!=g.
- Side Effects None
- See Also
Cudd_addApply
- Defined in
cuddAddApply.c
DdNode *
Cudd_addDivide(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
- Integer and floating point division. Returns NULL if not
a terminal case; f / g otherwise.
- Side Effects None
- See Also
Cudd_addApply
- Defined in
cuddAddApply.c
DdNode *
Cudd_addEvalConst(
DdManager * dd,
DdNode * f,
DdNode * g
)
- Checks whether ADD g is constant whenever ADD f is 1. f
must be a 0-1 ADD. Returns a pointer to the resulting ADD (which may
or may not be constant) or DD_NON_CONSTANT. If f is identically 0,
the check is assumed to be successful, and the background value is
returned. No new nodes are created.
- Side Effects None
- See Also
Cudd_addIteConstant
Cudd_addLeq
- Defined in
cuddAddIte.c
DdNode *
Cudd_addExistAbstract(
DdManager * manager,
DdNode * f,
DdNode * cube
)
- Abstracts all the variables in cube from f by summing
over all possible values taken by the variables. Returns the
abstracted ADD.
- Side Effects None
- See Also
Cudd_addUnivAbstract
Cudd_bddExistAbstract
Cudd_addOrAbstract
- Defined in
cuddAddAbs.c
DdNode *
Cudd_addFindMax(
DdManager * dd,
DdNode * f
)
- Returns a pointer to a constant ADD.
- Side Effects None
- Defined in
cuddAddFind.c
DdNode *
Cudd_addFindMin(
DdManager * dd,
DdNode * f
)
- Returns a pointer to a constant ADD.
- Side Effects None
- Defined in
cuddAddFind.c
DdNode *
Cudd_addGeneralVectorCompose(
DdManager * dd,
DdNode * f,
DdNode ** vectorOn,
DdNode ** vectorOff
)
- Given a vector of ADDs, creates a new ADD by substituting the
ADDs for the variables of the ADD f. vectorOn contains ADDs to be substituted
for the x_v and vectorOff the ADDs to be substituted for x_v'. 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_addVectorCompose
Cudd_addNonSimCompose
Cudd_addPermute
Cudd_addCompose
Cudd_bddVectorCompose
- Defined in
cuddCompose.c
DdNode *
Cudd_addHamming(
DdManager * dd,
DdNode ** xVars,
DdNode ** yVars,
int nVars
)
- Computes the Hamming distance ADD. Returns an ADD that
gives the Hamming distance between its two arguments if successful;
NULL otherwise. The two vectors xVars and yVars identify the variables
that form the two arguments.
- Side Effects None
- Defined in
cuddPriority.c
int
Cudd_addHarwell(
FILE * fp, pointer to the input file
DdManager * dd, DD manager
DdNode ** E, characteristic function of the graph
DdNode *** x, array of row variables
DdNode *** y, array of column variables
DdNode *** xn, array of complemented row variables
DdNode *** yn_, array of complemented column variables
int * nx, number or row variables
int * ny, number or column variables
int * m, number of rows
int * n, number of columns
int bx, first index of row variables
int sx, step of row variables
int by, first index of column variables
int sy, step of column variables
int pr verbosity level
)
- Reads in a matrix in the format of the Harwell-Boeing
benchmark suite. The variables are ordered as follows:
x[0] y[0] x[1] y[1] ...
0 is the most significant bit. On input, nx and ny hold the numbers
of row and column variables already in existence. On output, they
hold the numbers of row and column variables actually used by the
matrix. m and n are set to the numbers of rows and columns of the
matrix. Their values on input are immaterial. Returns 1 on
success; 0 otherwise. The ADD for the sparse matrix is returned in
E, and its reference count is > 0.
- Side Effects None
- See Also
Cudd_addRead
Cudd_bddRead
- Defined in
cuddHarwell.c
DdNode *
Cudd_addIteConstant(
DdManager * dd,
DdNode * f,
DdNode * g,
DdNode * h
)
- Implements ITEconstant for ADDs. f must be a 0-1 ADD.
Returns a pointer to the resulting ADD (which may or may not be
constant) or DD_NON_CONSTANT. No new nodes are created. This function
can be used, for instance, to check that g has a constant value
(specified by h) whenever f is 1. If the constant value is unknown,
then one should use Cudd_addEvalConst.
- Side Effects None
- See Also
Cudd_addIte
Cudd_addEvalConst
Cudd_bddIteConstant
- Defined in
cuddAddIte.c
DdNode *
Cudd_addIte(
DdManager * dd,
DdNode * f,
DdNode * g,
DdNode * h
)
- Implements ITE(f,g,h). This procedure assumes that f is
a 0-1 ADD. Returns a pointer to the resulting ADD if successful; NULL
otherwise.
- Side Effects None
- See Also
Cudd_bddIte
Cudd_addIteConstant
Cudd_addApply
- Defined in
cuddAddIte.c
DdNode *
Cudd_addIthBit(
DdManager * dd,
DdNode * f,
int bit
)
- Produces an ADD from another ADD by replacing all
discriminants whose i-th bit is equal to 1 with 1, and all other
discriminants with 0. The i-th bit refers to the integer
representation of the leaf value. If the value is has a fractional
part, it is ignored. Repeated calls to this procedure allow one to
transform an integer-valued ADD into an array of ADDs, one for each
bit of the leaf values. Returns a pointer to the resulting ADD if
successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_addBddIthBit
- Defined in
cuddAddFind.c
DdNode *
Cudd_addIthVar(
DdManager * dd,
int i
)
- Retrieves the ADD variable with index i if it already
exists, or creates a new ADD variable. Returns a pointer to the
variable if successful; NULL otherwise. An ADD variable differs from
a BDD variable because it points to the arithmetic zero, instead of
having a complement pointer to 1.
- Side Effects None
- See Also
Cudd_addNewVar
Cudd_bddIthVar
Cudd_addConst
Cudd_addNewVarAtLevel
- Defined in
cuddAPI.c
int
Cudd_addLeq(
DdManager * dd,
DdNode * f,
DdNode * g
)
- Returns 1 if f is less than or equal to g; 0 otherwise.
No new nodes are created. This procedure works for arbitrary ADDs.
For 0-1 ADDs Cudd_addEvalConst is more efficient.
- Side Effects None
- See Also
Cudd_addIteConstant
Cudd_addEvalConst
Cudd_bddLeq
- Defined in
cuddAddIte.c
DdNode *
Cudd_addLog(
DdManager * dd,
DdNode * f
)
- Natural logarithm of an ADDs. Returns NULL
if not a terminal case; log(f) otherwise. The discriminants of f must
be positive double's.
- Side Effects None
- See Also
Cudd_addMonadicApply
- Defined in
cuddAddApply.c
DdNode *
Cudd_addMatrixMultiply(
DdManager * dd,
DdNode * A,
DdNode * B,
DdNode ** z,
int nz
)
- Calculates the product of two matrices, A and B,
represented as ADDs. This procedure implements the quasiring multiplication
algorithm. A is assumed to depend on variables x (rows) and z
(columns). B is assumed to depend on variables z (rows) and y
(columns). The product of A and B then depends on x (rows) and y
(columns). Only the z variables have to be explicitly identified;
they are the "summation" variables. Returns a pointer to the
result if successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_addTimesPlus
Cudd_addTriangle
Cudd_bddAndAbstract
- Defined in
cuddMatMult.c
DdNode *
Cudd_addMaximum(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
- Integer and floating point max for Cudd_addApply.
Returns NULL if not a terminal case; max(f,g) otherwise.
- Side Effects None
- See Also
Cudd_addApply
- Defined in
cuddAddApply.c
DdNode *
Cudd_addMinimum(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
- Integer and floating point min for Cudd_addApply.
Returns NULL if not a terminal case; min(f,g) otherwise.
- Side Effects None
- See Also
Cudd_addApply
- Defined in
cuddAddApply.c
DdNode *
Cudd_addMinus(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
- Integer and floating point subtraction. Returns NULL if
not a terminal case; f - g otherwise.
- Side Effects None
- See Also
Cudd_addApply
- Defined in
cuddAddApply.c
DdNode *
Cudd_addMonadicApply(
DdManager * dd,
DD_MAOP op,
DdNode * f
)
- Applies op to the discriminants of f.
Returns a pointer to the result if succssful; NULL otherwise.
- Side Effects None
- See Also
Cudd_addApply
Cudd_addLog
- Defined in
cuddAddApply.c
DdNode *
Cudd_addNand(
DdManager * dd,
DdNode ** f,
DdNode ** g
)
- NAND of two 0-1 ADDs. Returns NULL