- See Also
cuddDestroySubtables
- Defined in
cuddTable.c
int
cuddIsInDeathRow(
DdManager * dd,
DdNode * f
)
- Checks whether a node is in the death row. Returns the
position of the first occurrence if the node is present; -1
otherwise.
- Side Effects None
- See Also
Cudd_DelayedDerefBdd
cuddClearDeathRow
- Defined in
cuddRef.c
void
cuddLevelQueueDequeue(
DdLevelQueue * queue,
int level
)
- Remove an item from the front of a level queue.
- Side Effects None
- See Also
cuddLevelQueueEnqueue
- Defined in
cuddLevelQ.c
void *
cuddLevelQueueEnqueue(
DdLevelQueue * queue, level queue
void * key, key to be enqueued
int level level at which to insert
)
- Inserts a new key in a level queue. A new entry is
created in the queue only if the node is not already
enqueued. Returns a pointer to the queue item if successful; NULL
otherwise.
- Side Effects None
- See Also
cuddLevelQueueInit
cuddLevelQueueDequeue
- Defined in
cuddLevelQ.c
DdLevelQueue *
cuddLevelQueueInit(
int levels, number of levels
int itemSize, size of the item
int numBuckets initial number of hash buckets
)
- Initializes a level queue. A level queue is a queue
where inserts are based on the levels of the nodes. Within each
level the policy is FIFO. Level queues are useful in traversing a
BDD top-down. Queue items are kept in a free list when dequeued for
efficiency. Returns a pointer to the new queue if successful; NULL
otherwise.
- Side Effects None
- See Also
cuddLevelQueueQuit
cuddLevelQueueEnqueue
cuddLevelQueueDequeue
- Defined in
cuddLevelQ.c
void
cuddLevelQueueQuit(
DdLevelQueue * queue
)
- Shuts down a level queue and releases all the
associated memory.
- Side Effects None
- See Also
cuddLevelQueueInit
- Defined in
cuddLevelQ.c
int
cuddLinearAndSifting(
DdManager * table,
int lower,
int upper
)
- BDD reduction based on combination of sifting and linear
transformations. Assumes that no dead nodes are present.
- Order all the variables according to the number of entries
in each unique table.
- Sift the variable up and down, remembering each time the
total size of the DD heap. At each position, linear transformation
of the two adjacent variables is tried and is accepted if it reduces
the size of the DD.
- Select the best permutation.
- Repeat 3 and 4 for all variables.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddLinear.c
int
cuddLinearInPlace(
DdManager * table,
int x,
int y
)
- Linearly combines two adjacent variables. Specifically,
replaces the top variable with the exclusive nor of the two variables.
It assumes that no dead nodes are present on entry to this
procedure. The procedure then guarantees that no dead nodes will be
present when it terminates. cuddLinearInPlace assumes that x <
y. Returns the number of keys in the table if successful; 0
otherwise.
- Side Effects The two subtables corrresponding to variables x and y are
modified. The global counters of the unique table are also affected.
- See Also
cuddSwapInPlace
- Defined in
cuddLinear.c
static void
cuddLocalCacheAddToList(
DdLocalCache * cache
)
- Inserts a local cache in the manager list.
- Side Effects None
- Defined in
cuddLCache.c
void
cuddLocalCacheClearAll(
DdManager * manager
)
- Clears the local caches of a manager.
Used before reordering.
- Side Effects None
- Defined in
cuddLCache.c
void
cuddLocalCacheClearDead(
DdManager * manager
)
- Clears the dead entries of the local caches of a manager.
Used during garbage collection.
- Side Effects None
- Defined in
cuddLCache.c
DdLocalCache *
cuddLocalCacheInit(
DdManager * manager, manager
unsigned int keySize, size of the key (number of operands)
unsigned int cacheSize, Initial size of the cache
unsigned int maxCacheSize Size of the cache beyond which no resizing occurs
)
- Initializes a computed table. Returns a pointer the
the new local cache in case of success; NULL otherwise.
- Side Effects None
- See Also
cuddInitCache
- Defined in
cuddLCache.c
void
cuddLocalCacheInsert(
DdLocalCache * cache,
DdNodePtr * key,
DdNode * value
)
- Inserts a result in a local cache.
- Side Effects None
- Defined in
cuddLCache.c
DdNode *
cuddLocalCacheLookup(
DdLocalCache * cache,
DdNodePtr * key
)
- Looks up in a local cache. Returns the result if found;
it returns NULL if no result is found.
- Side Effects None
- Defined in
cuddLCache.c
int
cuddLocalCacheProfile(
DdLocalCache * cache
)
- Computes and prints a profile of a local cache usage.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddLCache.c
void
cuddLocalCacheQuit(
DdLocalCache * cache cache to be shut down
)
- Initializes the computed table. It is called by
Cudd_Init. Returns a pointer the the new local cache in case of
success; NULL otherwise.
- Side Effects None
- See Also
cuddLocalCacheInit
- Defined in
cuddLCache.c
static void
cuddLocalCacheRemoveFromList(
DdLocalCache * cache
)
- Removes a local cache from the manager list.
- Side Effects None
- Defined in
cuddLCache.c
static void
cuddLocalCacheResize(
DdLocalCache * cache
)
- Resizes a local cache.
- Side Effects None
- Defined in
cuddLCache.c
DdNode *
cuddMakeBddFromZddCover(
DdManager * dd,
DdNode * node
)
- Converts a ZDD cover to a BDD graph. If successful, it
returns a BDD node, otherwise it returns NULL. It is a recursive
algorithm as the following. First computes 3 cofactors of a ZDD cover;
f1, f0 and fd. Second, compute BDDs(b1, b0 and bd) of f1, f0 and fd.
Third, compute T=b1+bd and E=b0+bd. Fourth, compute ITE(v,T,E) where v
is the variable which has the index of the top node of the ZDD cover.
In this case, since the index of v can be larger than either one of T or
one of E, cuddUniqueInterIVO is called, here IVO stands for
independent variable ordering.
- See Also
Cudd_MakeBddFromZddCover
- Defined in
cuddZddIsop.c
static int
cuddMinHammingDistRecur(
DdNode * f,
int * minterm,
DdHashTable * table,
int upperBound
)
- Performs the recursive step of Cudd_MinHammingDist.
It is based on the following identity. Let H(f) be the
minimum Hamming distance of the minterms of f from the reference
minterm. Then:
H(f) = min(H(f0)+h0,H(f1)+h1)
where f0 and f1 are the two cofactors of f with respect to its top
variable; h0 is 1 if the minterm assigns 1 to the top variable of f;
h1 is 1 if the minterm assigns 0 to the top variable of f.
The upper bound on the distance is used to bound the depth of the
recursion.
Returns the minimum distance unless it exceeds the upper bound or
computation fails.
- Side Effects None
- See Also
Cudd_MinHammingDist
- Defined in
cuddPriority.c
int
cuddNextHigh(
DdManager * table,
int x
)
- Finds the next subtable with a larger index. Returns the
index.
- Side Effects None
- See Also
cuddNextLow
- Defined in
cuddReorder.c
int
cuddNextLow(
DdManager * table,
int x
)
- Finds the next subtable with a smaller index. Returns the
index.
- Side Effects None
- See Also
cuddNextHigh
- Defined in
cuddReorder.c
static int
cuddNodeArrayRecur(
DdNode * f,
DdNodePtr * table,
int index
)
- Performs the recursive step of cuddNodeArray. Returns
an the number of nodes in the DD. Clear the least significant bit
of the next field that was used as visited flag by
cuddNodeArrayRecur when counting the nodes. node is supposed to be
regular; the invariant is maintained by this procedure.
- Side Effects None
- Defined in
cuddUtil.c
DdNodePtr *
cuddNodeArray(
DdNode * f,
int * n
)
- Traverses the DD f and collects all its nodes in an array.
The caller should free the array returned by cuddNodeArray.
Returns a pointer to the array of nodes in case of success; NULL
otherwise. The nodes are collected in reverse topological order, so
that a node is always preceded in the array by all its descendants.
- Side Effects The number of nodes is returned as a side effect.
- See Also
Cudd_FirstNode
- Defined in
cuddUtil.c
static void
cuddOrderedInsert(
DdNodePtr * root,
DdNodePtr node
)
- Inserts a DdNode in a red/black search tree. Nodes from
the same "page" (defined by DD_PAGE_MASK) are linked in a LIFO list.
- Side Effects None
- See Also
cuddOrderedThread
- Defined in
cuddTable.c
static DdNode *
cuddOrderedThread(
DdNode * root,
DdNode * list
)
- Threads all the nodes of a search tree into a linear
list. For each node of the search tree, the "left" child, if non-null, has
a lower address than its parent, and the "right" child, if non-null, has a
higher address than its parent.
The list is sorted in order of increasing addresses. The search
tree is destroyed as a result of this operation. The last element of
the linear list is made to point to the address passed in list. Each
node if the search tree is a linearly-linked list of nodes from the
same memory page (as defined in DD_PAGE_MASK). When a node is added to
the linear list, all the elements of the linked list are added.
- Side Effects The search tree is destroyed as a result of this operation.
- See Also
cuddOrderedInsert
- Defined in
cuddTable.c
void
cuddPrintNode(
DdNode * f,
FILE * fp
)
- Prints out information on a node.
- Side Effects None
- Defined in
cuddCheck.c
void
cuddPrintVarGroups(
DdManager * dd, manager
MtrNode * root, root of the group tree
int zdd, 0: BDD; 1: ZDD
int silent flag to check tree syntax only
)
- Prints the variable groups as a parenthesized list.
For each group the level range that it represents is printed. After
each group, the group's flags are printed, preceded by a `|'. For
each flag (except MTR_TERMINAL) a character is printed.
- F: MTR_FIXED
- N: MTR_NEWNODE
- S: MTR_SOFT
The second argument, silent, if different from 0, causes
Cudd_PrintVarGroups to only check the syntax of the group tree.
- Side Effects None
- Defined in
cuddCheck.c
int
cuddP(
DdManager * dd,
DdNode * f
)
- Prints a DD to the standard output. One line per node is
printed. Returns 1 if successful; 0 otherwise.
- Side Effects None
- See Also
Cudd_PrintDebug
- Defined in
cuddUtil.c
void
cuddReclaimZdd(
DdManager * table,
DdNode * n
)
- Brings children of a dead ZDD node back.
- Side Effects None
- See Also
cuddReclaim
- Defined in
cuddRef.c
void
cuddReclaim(
DdManager * table,
DdNode * n
)
- Brings children of a dead node back.
- Side Effects None
- See Also
cuddReclaimZdd
- Defined in
cuddRef.c
void
cuddRehash(
DdManager * unique,
int i
)
- Doubles the size of a unique subtable and rehashes its
contents.
- Side Effects None
- Defined in
cuddTable.c
DdNode *
cuddRemapUnderApprox(
DdManager * dd, DD manager
DdNode * f, current DD
int numVars, maximum number of variables
int threshold, threshold under which approximation stops
double quality minimum improvement for accepted changes
)
- Applies the remapping underappoximation algorithm.
Proceeds in three phases:
- collect information on each node in the BDD; this is done via DFS.
- traverse the BDD in top-down fashion and compute for each node
whether remapping increases density.
- traverse the BDD via DFS and actually perform the elimination.
Returns the approximated BDD if successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_RemapUnderApprox
- Defined in
cuddApprox.c
int
cuddResizeLinear(
DdManager * table
)
- Resizes the linear transform matrix. Returns 1 if
successful; 0 otherwise.
- Side Effects none
- Defined in
cuddLinear.c
int
cuddResizeTableZdd(
DdManager * unique,
int index
)
- Increases the number of ZDD subtables in a unique table so
that it meets or exceeds index. When new ZDD variables are created, it
is possible to preserve the functions unchanged, or it is possible to
preserve the covers unchanged, but not both. cuddResizeTableZdd preserves
the covers. Returns 1 if successful; 0 otherwise.
- Side Effects None
- See Also
ddResizeTable
- Defined in
cuddTable.c
static void
cuddRotateLeft(
DdNodePtr * nodeP
)
- Performs the left rotation for red/black trees.
- Side Effects None
- See Also
cuddRotateRight
- Defined in
cuddTable.c
static void
cuddRotateRight(
DdNodePtr * nodeP
)
- Performs the right rotation for red/black trees.
- Side Effects None
- See Also
cuddRotateLeft
- Defined in
cuddTable.c
void
cuddSetInteract(
DdManager * table,
int x,
int y
)
- Given a pair of variables 0 <= x < y < table->size,
sets the corresponding bit of the interaction matrix to 1.
- Side Effects None
- Defined in
cuddInteract.c
void
cuddShrinkDeathRow(
DdManager * table
)
- Shrinks the death row by a factor of four.
- Side Effects None
- See Also
cuddClearDeathRow
- Defined in
cuddRef.c
void
cuddShrinkSubtable(
DdManager * unique,
int i
)
- Shrinks a subtable.
- Side Effects None
- See Also
cuddRehash
- Defined in
cuddTable.c
int
cuddSifting(
DdManager * table,
int lower,
int upper
)
- Implementation of Rudell's sifting algorithm.
Assumes that no dead nodes are present.
- Order all the variables according to the number of entries
in each unique table.
- Sift the variable up and down, remembering each time the
total size of the DD heap.
- Select the best permutation.
- Repeat 3 and 4 for all variables.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddReorder.c
void
cuddSlowTableGrowth(
DdManager * unique
)
- Adjusts parameters of a table to slow down its growth.
- Side Effects None
- Defined in
cuddTable.c
DdNode *
cuddSolveEqnRecur(
DdManager * bdd,
DdNode * F, the left-hand side of the equation
DdNode * Y, the cube of remaining y variables
DdNode ** G, the array of solutions
int n, number of unknowns
int * yIndex, array holding the y variable indices
int i level of recursion
)
- Implements the recursive step of Cudd_SolveEqn.
Returns NULL if the intermediate solution blows up
or reordering occurs. The parametric solutions are
stored in the array G.
- Side Effects none
- See Also
Cudd_SolveEqn
Cudd_VerifySol
- Defined in
cuddSolve.c
DdNode*
cuddSplitSetRecur(
DdManager * manager,
st_table * mtable,
int * varSeen,
DdNode * p,
double n,
double max,
int index
)
- Implements the recursive step of Cudd_SplitSet. The
procedure recursively traverses the BDD and checks to see if any
node satisfies the minterm requirements as specified by 'n'. At any
node X, n is compared to the number of minterms in the onset of X's
children. If either of the child nodes have exactly n minterms, then
that node is returned; else, if n is greater than the onset of one
of the child nodes, that node is retained and the difference in the
number of minterms is extracted from the other child. In case n
minterms can be extracted from constant 1, the algorithm returns the
result with at most log(n) nodes.
- Side Effects The array 'varSeen' is updated at every recursive call
to set the variables traversed by the procedure.
- Defined in
cuddSplit.c
enum st_retval
cuddStCountfree(
char * key,
char * value,
char * arg
)
- Frees the memory used to store the minterm counts
recorded in the visited table. Returns ST_CONTINUE.
- Side Effects None
- Defined in
cuddUtil.c
DdNode *
cuddSubsetHeavyBranch(
DdManager * dd, DD manager
DdNode * f, current DD
int numVars, maximum number of variables
int threshold threshold size for the subset
)
- Here a subset BDD is built by throwing away one of the
children. Starting at root, annotate each node with the number of
minterms (in terms of the total number of variables specified -
numVars), number of nodes taken by the DAG rooted at this node and
number of additional nodes taken by the child that has the lesser
minterms. The child with the lower number of minterms is thrown away
and a dyanmic count of the nodes of the subset is kept. Once the
threshold is reached the subset is returned to the calling
procedure.
- Side Effects None
- See Also
Cudd_SubsetHeavyBranch
- Defined in
cuddSubsetHB.c
DdNode *
cuddSubsetShortPaths(
DdManager * dd, DD manager
DdNode * f, function to be subset
int numVars, total number of variables in consideration
int threshold, maximum number of nodes allowed in the subset
int hardlimit flag determining whether thershold should be respected strictly
)
- The outermost procedure to return a subset of the given
BDD with the largest cubes. The path lengths are calculated, the maximum
allowable path length is determined and the number of nodes of this
path length that can be used to build a subset. If the threshold is
larger than the size of the original BDD, the original BDD is
returned.
- Side Effects None
- See Also
Cudd_SubsetShortPaths
- Defined in
cuddSubsetSP.c
int
cuddSwapInPlace(
DdManager * table,
int x,
int y
)
- Swaps two adjacent variables. It assumes that no dead
nodes are present on entry to this procedure. The procedure then
guarantees that no dead nodes will be present when it terminates.
cuddSwapInPlace assumes that x < y. Returns the number of keys in
the table if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddReorder.c
int
cuddSwapping(
DdManager * table,
int lower,
int upper,
Cudd_ReorderingType heuristic
)
- Implementation of Plessier's algorithm that reorders
variables by a sequence of (non-adjacent) swaps.
- Select two variables (RANDOM or HEURISTIC).
- Permute these variables.
- If the nodes have decreased accept the permutation.
- Otherwise reconstruct the original heap.
- Loop.
Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddReorder.c
int
cuddSymmCheck(
DdManager * table,
int x,
int y
)
- Checks for symmetry of x and y. Ignores projection
functions, unless they are isolated. Returns 1 in case of symmetry; 0
otherwise.
- Side Effects None
- Defined in
cuddSymmetry.c
int
cuddSymmSiftingConv(
DdManager * table,
int lower,
int upper
)
- Symmetric sifting to convergence algorithm.
Assumes that no dead nodes are present.
- Order all the variables according to the number of entries in
each unique subtable.
- Sift the variable up and down, remembering each time the total
size of the DD heap and grouping variables that are symmetric.
- Select the best permutation.
- Repeat 3 and 4 for all variables.
- Repeat 1-4 until no further improvement.
Returns 1 plus the number of symmetric variables if successful; 0
otherwise.
- Side Effects None
- See Also
cuddSymmSifting
- Defined in
cuddSymmetry.c
int
cuddSymmSifting(
DdManager * table,
int lower,
int upper
)
- Symmetric sifting algorithm.
Assumes that no dead nodes are present.
- Order all the variables according to the number of entries in
each unique subtable.
- Sift the variable up and down, remembering each time the total
size of the DD heap and grouping variables that are symmetric.
- Select the best permutation.
- Repeat 3 and 4 for all variables.
Returns 1 plus the number of symmetric variables if successful; 0
otherwise.
- Side Effects None
- See Also
cuddSymmSiftingConv
- Defined in
cuddSymmetry.c
int
cuddTestInteract(
DdManager * table,
int x,
int y
)
- Given a pair of variables 0 <= x < y < table->size,
tests whether the corresponding bit of the interaction matrix is 1.
Returns the value of the bit.
- Side Effects None
- Defined in
cuddInteract.c
int
cuddTimesInDeathRow(
DdManager * dd,
DdNode * f
)
- Counts how many times a node is in the death row.
- Side Effects None
- See Also
Cudd_DelayedDerefBdd
cuddClearDeathRow
cuddIsInDeathRow
- Defined in
cuddRef.c
int
cuddTreeSifting(
DdManager * table, DD table
Cudd_ReorderingType method reordering method for the groups of leaves
)
- Tree sifting algorithm. Assumes that a tree representing
a group hierarchy is passed as a parameter. It then reorders each
group in postorder fashion by calling ddTreeSiftingAux. Assumes that
no dead nodes are present. Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddGroup.c
DdNode *
cuddUnderApprox(
DdManager * dd, DD manager
DdNode * f, current DD
int numVars, maximum number of variables
int threshold, threshold under which approximation stops
int safe, enforce safe approximation
double quality minimum improvement for accepted changes
)
- Applies Tom Shiple's underappoximation algorithm. Proceeds
in three phases:
- collect information on each node in the BDD; this is done via DFS.
- traverse the BDD in top-down fashion and compute for each node
whether its elimination increases density.
- traverse the BDD via DFS and actually perform the elimination.
Returns the approximated BDD if successful; NULL otherwise.
- Side Effects None
- See Also
Cudd_UnderApprox
- Defined in
cuddApprox.c
DdNode *
cuddUniqueConst(
DdManager * unique,
CUDD_VALUE_TYPE value
)
- Checks the unique table for the existence of a constant node.
If it does not exist, it creates a new one. Does not
modify the reference count of whatever is returned. A newly created
internal node comes back with a reference count 0. Returns a
pointer to the new node.
- Side Effects None
- Defined in
cuddTable.c
DdNode *
cuddUniqueInterIVO(
DdManager * unique,
int index,
DdNode * T,
DdNode * E
)
- Wrapper for cuddUniqueInter that is independent of
variable ordering (IVO). This function does not require parameter
index to precede the indices of the top nodes of T and E in the
variable order. Returns a pointer to the result node under normal
conditions; NULL if reordering occurred or memory was exhausted.
- Side Effects None
- See Also
cuddUniqueInter
Cudd_MakeBddFromZddCover
- Defined in
cuddTable.c
DdNode *
cuddUniqueInterZdd(
DdManager * unique,
int index,
DdNode * T,
DdNode * E
)
- Checks the unique table for the existence of an internal
ZDD node. If it does not exist, it creates a new one. Does not
modify the reference count of whatever is returned. A newly created
internal node comes back with a reference count 0. For a newly
created node, increments the reference counts of what T and E point
to. Returns a pointer to the new node if successful; NULL if memory
is exhausted or if reordering took place.
- Side Effects None
- See Also
cuddUniqueInter
- Defined in
cuddTable.c
DdNode *
cuddUniqueInter(
DdManager * unique,
int index,
DdNode * T,
DdNode * E
)
- Checks the unique table for the existence of an internal
node. If it does not exist, it creates a new one. Does not
modify the reference count of whatever is returned. A newly created
internal node comes back with a reference count 0. For a newly
created node, increments the reference counts of what T and E point
to. Returns a pointer to the new node if successful; NULL if memory
is exhausted or if reordering took place.
- Side Effects None
- See Also
cuddUniqueInterZdd
- Defined in
cuddTable.c
static DdNode *
cuddUniqueLookup(
DdManager * unique,
int index,
DdNode * T,
DdNode * E
)
- Checks the unique table for the existence of an internal
node. Returns a pointer to the node if it is in the table; NULL otherwise.
- Side Effects None
- See Also
cuddUniqueInter
- Defined in
cuddUtil.c
void
cuddUpdateInteractionMatrix(
DdManager * table,
int xindex,
int yindex
)
- Updates the interaction matrix.
- Side Effects none
- Defined in
cuddLinear.c
DdNode *
cuddVerifySol(
DdManager * bdd,
DdNode * F, the left-hand side of the equation
DdNode ** G, the array of solutions
int * yIndex, array holding the y variable indices
int n number of unknowns
)
- Implements the recursive step of Cudd_VerifySol.
- Side Effects none
- See Also
Cudd_VerifySol
- Defined in
cuddSolve.c
int
cuddWindowReorder(
DdManager * table, DD table
int low, lowest index to reorder
int high, highest index to reorder
Cudd_ReorderingType submethod window reordering option
)
- Reorders by applying the method of the sliding window.
Tries all possible permutations to the variables in a window that
slides from low to high. The size of the window is determined by
submethod. Assumes that no dead nodes are present. Returns 1 in
case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddWindow.c
static void
cuddXorLinear(
DdManager * table,
int x,
int y
)
- XORs two rows of the linear transform matrix and replaces
the first row with the result.
- Side Effects none
- Defined in
cuddLinear.c
int
cuddZddAlignToBdd(
DdManager * table DD manager
)
- Reorders ZDD variables according to the order of the
BDD variables. This function can be called at the end of BDD
reordering to insure that the order of the ZDD variables is
consistent with the order of the BDD variables. The number of ZDD
variables must be a multiple of the number of BDD variables. Let
M
be the ratio of the two numbers. cuddZddAlignToBdd
then considers the ZDD variables from M*i
to
(M+1)*i-1
as corresponding to BDD variable
i
. This function should be normally called from
Cudd_ReduceHeap, which clears the cache. Returns 1 in case of
success; 0 otherwise.
- Side Effects Changes the ZDD variable order for all diagrams and performs
garbage collection of the ZDD unique table.
- See Also
Cudd_zddShuffleHeap
Cudd_ReduceHeap
- Defined in
cuddZddReord.c
DdNode *
cuddZddChangeAux(
DdManager * zdd,
DdNode * P,
DdNode * zvar
)
- Performs the recursive step of Cudd_zddChange.
- Side Effects None
- Defined in
cuddZddSetop.c
DdNode *
cuddZddChange(
DdManager * dd,
DdNode * P,
int var
)
- Substitutes a variable with its complement in a ZDD.
returns a pointer to the result if successful; NULL
otherwise. cuddZddChange performs the same function as
Cudd_zddChange, but does not restart if reordering has taken
place. Therefore it can be called from within a recursive
procedure.
- Side Effects None
- See Also
Cudd_zddChange
- Defined in
cuddZddSetop.c
DdNode *
cuddZddComplement(
DdManager * dd,
DdNode * node
)
- Computes the complement of a ZDD node. So far, since we
couldn't find a direct way to get the complement of a ZDD cover, we first
convert a ZDD cover to a BDD, then make the complement of the ZDD cover
from the complement of the BDD node by using ISOP.
- Side Effects The result depends on current variable order.
- Defined in
cuddZddFuncs.c
static double
cuddZddCountDoubleStep(
DdNode * P,
st_table * table,
DdNode * base,
DdNode * empty
)
- Performs the recursive step of Cudd_zddCountDouble.
- Side Effects None
- Defined in
cuddZddCount.c
static int
cuddZddCountStep(
DdNode * P,
st_table * table,
DdNode * base,
DdNode * empty
)
- Performs the recursive step of Cudd_zddCount.
- Side Effects None
- Defined in
cuddZddCount.c
static int
cuddZddDagInt(
DdNode * n,
st_table * tab
)
- Performs the recursive step of Cudd_zddDagSize. Does
not check for out-of-memory conditions.
- Side Effects None
- Defined in
cuddZddMisc.c
DdNode *
cuddZddDiff(
DdManager * zdd,
DdNode * P,
DdNode * Q
)
- Performs the recursive step of Cudd_zddDiff.
- Side Effects None
- Defined in
cuddZddSetop.c
DdNode *
cuddZddDivideF(
DdManager * dd,
DdNode * f,
DdNode * g
)
- Performs the recursive step of Cudd_zddDivideF.
- Side Effects None
- See Also
Cudd_zddDivideF
- Defined in
cuddZddFuncs.c
DdNode *
cuddZddDivide(
DdManager * dd,
DdNode * f,
DdNode * g
)
- Performs the recursive step of Cudd_zddDivide.
- Side Effects None
- See Also
Cudd_zddDivide
- Defined in
cuddZddFuncs.c
void
cuddZddFreeUniv(
DdManager * zdd
)
- Frees the ZDD universe.
- Side Effects None
- See Also
cuddZddInitUniv
- Defined in
cuddInit.c
int
cuddZddGetCofactors2(
DdManager * dd,
DdNode * f,
int v,
DdNode ** f1,
DdNode ** f0
)
- Computes the two-way decomposition of f w.r.t. v.
- Side Effects The results are returned in f1 and f0.
- See Also
cuddZddGetCofactors3
- Defined in
cuddZddFuncs.c
int
cuddZddGetCofactors3(
DdManager * dd,
DdNode * f,
int v,
DdNode ** f1,
DdNode ** f0,
DdNode ** fd
)
- Computes the three-way decomposition of function f (represented
by a ZDD) wit respect to variable v. Returns 0 if successful; 1 otherwise.
- Side Effects The results are returned in f1, f0, and fd.
- See Also
cuddZddGetCofactors2
- Defined in
cuddZddFuncs.c
int
cuddZddGetNegVarIndex(
DdManager * dd,
int index
)
- Returns the index of negative ZDD variable.
- Defined in
cuddZddFuncs.c
int
cuddZddGetNegVarLevel(
DdManager * dd,
int index
)
- Returns the level of negative ZDD variable.
- Defined in
cuddZddFuncs.c
DdNode *
cuddZddGetNodeIVO(
DdManager * dd,
int index,
DdNode * g,
DdNode * h
)
- Wrapper for cuddUniqueInterZdd that is independent of
variable ordering (IVO). This function does not require parameter
index to precede the indices of the top nodes of g and h in the
variable order. Returns a pointer to the result node under normal
conditions; NULL if reordering occurred or memory was exhausted.
- Side Effects None
- See Also
cuddZddGetNode
cuddZddIsop
- Defined in
cuddTable.c
DdNode *
cuddZddGetNode(
DdManager * zdd,
int id,
DdNode * T,
DdNode * E
)
- Wrapper for cuddUniqueInterZdd, which applies the ZDD
reduction rule. Returns a pointer to the result node under normal
conditions; NULL if reordering occurred or memory was exhausted.
- Side Effects None
- See Also
cuddUniqueInterZdd
- Defined in
cuddTable.c
int
cuddZddGetPosVarIndex(
DdManager * dd,
int index
)
- Returns the index of positive ZDD variable.
- Defined in
cuddZddFuncs.c
int
cuddZddGetPosVarLevel(
DdManager * dd,
int index
)
- Returns the level of positive ZDD variable.
- Defined in
cuddZddFuncs.c
int
cuddZddInitUniv(
DdManager * zdd
)
- Initializes the ZDD universe. Returns 1 if successful; 0
otherwise.
- Side Effects None
- See Also
cuddZddFreeUniv
- Defined in
cuddInit.c
DdNode *
cuddZddIntersect(
DdManager * zdd,
DdNode * P,
DdNode * Q
)
- Performs the recursive step of Cudd_zddIntersect.
- Side Effects None
- Defined in
cuddZddSetop.c
DdNode *
cuddZddIsop(
DdManager * dd,
DdNode * L,
DdNode * U,
DdNode ** zdd_I
)
- Performs the recursive step of Cudd_zddIsop.
- Side Effects None
- See Also
Cudd_zddIsop
- Defined in
cuddZddIsop.c
DdNode *
cuddZddIte(
DdManager * dd,
DdNode * f,
DdNode * g,
DdNode * h
)
- Performs the recursive step of Cudd_zddIte.
- Side Effects None
- Defined in
cuddZddSetop.c
static int
cuddZddLinearAux(
DdManager * table,
int x,
int xLow,
int xHigh
)
- Given xLow <= x <= xHigh moves x up and down between the
boundaries. Finds the best position and does the required changes.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddZddLin.c
static int
cuddZddLinearBackward(
DdManager * table,
int size,
Move * moves
)
- Given a set of moves, returns the ZDD heap to the
position giving the minimum size. In case of ties, returns to the
closest position giving the minimum size. Returns 1 in case of
success; 0 otherwise.
- Side Effects None
- Defined in
cuddZddLin.c
static Move *
cuddZddLinearDown(
DdManager * table,
int x,
int xHigh,
Move * prevMoves
)
- Sifts a variable down. Moves x down until either it
reaches the bound (xHigh) or the size of the ZDD heap increases too
much. Returns the set of moves in case of success; NULL if memory is
full.
- Side Effects None
- Defined in
cuddZddLin.c
static int
cuddZddLinearInPlace(
DdManager * table,
int x,
int y
)
- Linearly combines two adjacent variables. It assumes
that no dead nodes are present on entry to this procedure. The
procedure then guarantees that no dead nodes will be present when it
terminates. cuddZddLinearInPlace assumes that x < y. Returns the
number of keys in the table if successful; 0 otherwise.
- Side Effects None
- See Also
cuddZddSwapInPlace
cuddLinearInPlace
- Defined in
cuddZddLin.c
int
cuddZddLinearSifting(
DdManager * table,
int lower,
int upper
)
- Implementation of the linear sifting algorithm for ZDDs.
Assumes that no dead nodes are present.
- Order all the variables according to the number of entries
in each unique table.
- Sift the variable up and down and applies the XOR transformation,
remembering each time the total size of the DD heap.
- Select the best permutation.
- Repeat 3 and 4 for all variables.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddZddLin.c
static Move *
cuddZddLinearUp(
DdManager * table,
int y,
int xLow,
Move * prevMoves
)
- Sifts a variable up applying the XOR
transformation. Moves y up until either it reaches the bound (xLow)
or the size of the ZDD heap increases too much. Returns the set of
moves in case of success; NULL if memory is full.
- Side Effects None
- Defined in
cuddZddLin.c
int
cuddZddNextHigh(
DdManager * table,
int x
)
- Finds the next subtable with a larger index. Returns the
index.
- Side Effects None
- Defined in
cuddZddReord.c
int
cuddZddNextLow(
DdManager * table,
int x
)
- Finds the next subtable with a smaller index. Returns the
index.
- Side Effects None
- Defined in
cuddZddReord.c
DdNode *
cuddZddProduct(
DdManager * dd,
DdNode * f,
DdNode * g
)
- Performs the recursive step of Cudd_zddProduct.
- Side Effects None
- See Also
Cudd_zddProduct
- Defined in
cuddZddFuncs.c
int
cuddZddP(
DdManager * zdd,
DdNode * f
)
- Prints a ZDD to the standard output. One line per node is
printed. Returns 1 if successful; 0 otherwise.
- Side Effects None
- See Also
Cudd_zddPrintDebug
- Defined in
cuddZddUtil.c
static int
cuddZddSiftingAux(
DdManager * table,
int x,
int x_low,
int x_high
)
- Given xLow <= x <= xHigh moves x up and down between the
boundaries. Finds the best position and does the required changes.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddZddReord.c
static int
cuddZddSiftingBackward(
DdManager * table,
Move * moves,
int size
)
- Given a set of moves, returns the ZDD heap to the
position giving the minimum size. In case of ties, returns to the
closest position giving the minimum size. Returns 1 in case of
success; 0 otherwise.
- Side Effects None
- Defined in
cuddZddReord.c
static Move *
cuddZddSiftingDown(
DdManager * table,
int x,
int x_high,
int initial_size
)
- Sifts a variable down. Moves x down until either it
reaches the bound (x_high) or the size of the ZDD heap increases too
much. Returns the set of moves in case of success; NULL if memory is
full.
- Side Effects None
- Defined in
cuddZddReord.c
static Move *
cuddZddSiftingUp(
DdManager * table,
int x,
int x_low,
int initial_size
)
- Sifts a variable up. Moves y up until either it reaches
the bound (x_low) or the size of the ZDD heap increases too much.
Returns the set of moves in case of success; NULL if memory is full.
- Side Effects None
- Defined in
cuddZddReord.c
int
cuddZddSifting(
DdManager * table,
int lower,
int upper
)
- Implementation of Rudell's sifting algorithm.
Assumes that no dead nodes are present.
- Order all the variables according to the number of entries
in each unique table.
- Sift the variable up and down, remembering each time the
total size of the DD heap.
- Select the best permutation.
- Repeat 3 and 4 for all variables.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddZddReord.c
DdNode *
cuddZddSubset0(
DdManager * dd,
DdNode * P,
int var
)
- Computes the negative cofactor of a ZDD w.r.t. a
variable. In terms of combinations, the result is the set of all
combinations in which the variable is negated. Returns a pointer to
the result if successful; NULL otherwise. cuddZddSubset0 performs
the same function as Cudd_zddSubset0, but does not restart if
reordering has taken place. Therefore it can be called from within a
recursive procedure.
- Side Effects None
- See Also
cuddZddSubset1
Cudd_zddSubset0
- Defined in
cuddZddSetop.c
DdNode *
cuddZddSubset1(
DdManager * dd,
DdNode * P,
int var
)
- Computes the positive cofactor of a ZDD w.r.t. a
variable. In terms of combinations, the result is the set of all
combinations in which the variable is asserted. Returns a pointer to
the result if successful; NULL otherwise. cuddZddSubset1 performs
the same function as Cudd_zddSubset1, but does not restart if
reordering has taken place. Therefore it can be called from within a
recursive procedure.
- Side Effects None
- See Also
cuddZddSubset0
Cudd_zddSubset1
- Defined in
cuddZddSetop.c
int
cuddZddSwapInPlace(
DdManager * table,
int x,
int y
)
- Swaps two adjacent variables. It assumes that no dead
nodes are present on entry to this procedure. The procedure then
guarantees that no dead nodes will be present when it terminates.
cuddZddSwapInPlace assumes that x < y. Returns the number of keys in
the table if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddZddReord.c
int
cuddZddSwapping(
DdManager * table,
int lower,
int upper,
Cudd_ReorderingType heuristic
)
- Implementation of Plessier's algorithm that reorders
variables by a sequence of (non-adjacent) swaps.
- Select two variables (RANDOM or HEURISTIC).
- Permute these variables.
- If the nodes have decreased accept the permutation.
- Otherwise reconstruct the original heap.
- Loop.
Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddZddReord.c
int
cuddZddSymmCheck(
DdManager * table,
int x,
int y
)
- Checks for symmetry of x and y. Ignores projection
functions, unless they are isolated. Returns 1 in case of
symmetry; 0 otherwise.
- Side Effects None
- Defined in
cuddZddSymm.c
static int
cuddZddSymmSiftingAux(
DdManager * table,
int x,
int x_low,
int x_high
)
- Given x_low <= x <= x_high moves x up and down between the
boundaries. Finds the best position and does the required changes.
Assumes that x is not part of a symmetry group. Returns 1 if
successful; 0 otherwise.
- Side Effects None
- Defined in
cuddZddSymm.c
static int
cuddZddSymmSiftingBackward(
DdManager * table,
Move * moves,
int size
)
- Given a set of moves, returns the ZDD heap to the
position giving the minimum size. In case of ties, returns to the
closest position giving the minimum size. Returns 1 in case of
success; 0 otherwise.
- Side Effects None
- Defined in
cuddZddSymm.c
static int
cuddZddSymmSiftingConvAux(
DdManager * table,
int x,
int x_low,
int x_high
)
- Given x_low <= x <= x_high moves x up and down between the
boundaries. Finds the best position and does the required changes.
Assumes that x is either an isolated variable, or it is the bottom of
a symmetry group. All symmetries may not have been found, because of
exceeded growth limit. Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddZddSymm.c
int
cuddZddSymmSiftingConv(
DdManager * table,
int lower,
int upper
)
- Symmetric sifting to convergence algorithm for ZDDs.
Assumes that no dead nodes are present.
- Order all the variables according to the number of entries in
each unique subtable.
- Sift the variable up and down, remembering each time the total
size of the ZDD heap and grouping variables that are symmetric.
- Select the best permutation.
- Repeat 3 and 4 for all variables.
- Repeat 1-4 until no further improvement.
Returns 1 plus the number of symmetric variables if successful; 0
otherwise.
- Side Effects None
- See Also
cuddZddSymmSifting
- Defined in
cuddZddSymm.c
static Move *
cuddZddSymmSifting_down(
DdManager * table,
int x,
int x_high,
int initial_size
)
- Moves x down until either it reaches the bound (x_high)
or the size of the ZDD heap increases too much. Assumes that x is the
bottom of a symmetry group. Checks x for symmetry to the adjacent
variables. If symmetry is found, the symmetry group of x is merged
with the symmetry group of the other variable. Returns the set of
moves in case of success; ZDD_MV_OOM if memory is full.
- Side Effects None
- Defined in
cuddZddSymm.c
static Move *
cuddZddSymmSifting_up(
DdManager * table,
int x,
int x_low,
int initial_size
)
- Moves x up until either it reaches the bound (x_low) or
the size of the ZDD heap increases too much. Assumes that x is the top
of a symmetry group. Checks x for symmetry to the adjacent
variables. If symmetry is found, the symmetry group of x is merged
with the symmetry group of the other variable. Returns the set of
moves in case of success; ZDD_MV_OOM if memory is full.
- Side Effects None
- Defined in
cuddZddSymm.c
int
cuddZddSymmSifting(
DdManager * table,
int lower,
int upper
)
- Symmetric sifting algorithm.
Assumes that no dead nodes are present.
- Order all the variables according to the number of entries in
each unique subtable.
- Sift the variable up and down, remembering each time the total
size of the ZDD heap and grouping variables that are symmetric.
- Select the best permutation.
- Repeat 3 and 4 for all variables.
Returns 1 plus the number of symmetric variables if successful; 0
otherwise.
- Side Effects None
- See Also
cuddZddSymmSiftingConv
- Defined in
cuddZddSymm.c
static void
cuddZddSymmSummary(
DdManager * table,
int lower,
int upper,
int * symvars,
int * symgroups
)
- Counts numbers of symmetric variables and symmetry
groups.
- Side Effects None
- Defined in
cuddZddSymm.c
int
cuddZddTreeSifting(
DdManager * table, DD table
Cudd_ReorderingType method reordering method for the groups of leaves
)
- Tree sifting algorithm for ZDDs. Assumes that a tree
representing a group hierarchy is passed as a parameter. It then
reorders each group in postorder fashion by calling
zddTreeSiftingAux. Assumes that no dead nodes are present. Returns
1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddZddGroup.c
DdNode *
cuddZddUnateProduct(
DdManager * dd,
DdNode * f,
DdNode * g
)
- Performs the recursive step of Cudd_zddUnateProduct.
- Side Effects None
- See Also
Cudd_zddUnateProduct
- Defined in
cuddZddFuncs.c
static Move*
cuddZddUndoMoves(
DdManager * table,
Move * moves
)
- Given a set of moves, returns the ZDD heap to the
order in effect before the moves. Returns 1 in case of success;
0 otherwise.
- Side Effects None
- Defined in
cuddZddLin.c
DdNode *
cuddZddUnion(
DdManager * zdd,
DdNode * P,
DdNode * Q
)
- Performs the recursive step of Cudd_zddUnion.
- Side Effects None
- Defined in
cuddZddSetop.c
int
cuddZddUniqueCompare(
int * ptr_x,
int * ptr_y
)
- Comparison function used by qsort to order the
variables according to the number of keys in the subtables.
Returns the difference in number of keys between the two
variables being compared.
- Side Effects None
- Defined in
cuddZddReord.c
DdNode *
cuddZddWeakDivF(
DdManager * dd,
DdNode * f,
DdNode * g
)
- Performs the recursive step of Cudd_zddWeakDivF.
- Side Effects None
- See Also
Cudd_zddWeakDivF
- Defined in
cuddZddFuncs.c
DdNode *
cuddZddWeakDiv(
DdManager * dd,
DdNode * f,
DdNode * g
)
- Performs the recursive step of Cudd_zddWeakDiv.
- Side Effects None
- See Also
Cudd_zddWeakDiv
- Defined in
cuddZddFuncs.c
static DdNode *
ddBddToAddRecur(
DdManager * dd,
DdNode * B
)
- Performs the recursive step for Cudd_BddToAdd. Returns a
pointer to the resulting ADD if successful; NULL otherwise.
- Side Effects None
- Defined in
cuddBridge.c
static int
ddCheckPermuation(
DdManager * table,
MtrNode * treenode,
int * perm,
int * invperm
)
- Checks the BDD variable group tree before a shuffle.
Returns 1 if successful; 0 otherwise.
- Side Effects Changes the BDD variable group tree.
- Defined in
cuddReorder.c
static void
ddClearFlag(
DdNode * f
)
- Performs a DFS from f, clearing the LSB of the next
pointers.
- Side Effects None
- See Also
ddSupportStep
ddDagInt
- Defined in
cuddUtil.c
static void
ddClearGlobal(
DdManager * table,
int lower,
int maxlevel
)
- Scans the DD and clears the LSB of the next pointers.
The LSB of the next pointers are used as markers to tell whether a
node was reached. Once the roots are counted, these flags are
reset.
- Side Effects None
- See Also
ddCountRoots
- Defined in
cuddExact.c
static void
ddClearGlobal(
DdManager * table
)
- The LSB of the next pointers are used as markers to tell
whether a node was reached by at least one DFS. Once the interaction
matrix is built, these flags are reset.
- Side Effects None
- Defined in
cuddInteract.c
static void
ddClearLocal(
DdNode * f
)
- Performs a DFS from f, clearing the LSB of the then pointers.
- Side Effects None
- Defined in
cuddInteract.c
static double *
ddCofMintermAux(
DdManager * dd,
DdNode * node,
st_table * table
)
- Traverses the DD node and computes the fraction of
minterms in the on-set of all positive cofactors simultaneously.
It allocates an array with two more entries than there are
variables below the one labeling the node. One extra entry (the
first in the array) is for the variable labeling the node. The other
entry (the last one in the array) holds the fraction of minterms of
the function rooted at node. Each other entry holds the value for
one cofactor. The array is put in a symbol table, to avoid repeated
computation, and its address is returned by the procedure, for use
by the caller. Returns a pointer to the array of cofactor measures.
- Side Effects None
- Defined in
cuddSign.c
static int
ddCountInternalMtrNodes(
DdManager * table,
MtrNode * treenode
)
- Counts the number of internal nodes of the group tree.
Returns the count.
- Side Effects None
- Defined in
cuddGroup.c
static double
ddCountMintermAux(
DdNode * node,
double max,
DdHashTable * table
)
- Performs the recursive step of Cudd_CountMinterm.
It is based on the following identity. Let |f| be the
number of minterms of f. Then:
|f| = (|f0|+|f1|)/2
where f0 and f1 are the two cofactors of f. Does not use the
identity |f'| = max - |f|, to minimize loss of accuracy due to
roundoff. Returns the number of minterms of the function rooted at
node.
- Side Effects None
- Defined in
cuddUtil.c
static double
ddCountPathAux(
DdNode * node,
st_table * table
)
- Performs the recursive step of Cudd_CountPath.
It is based on the following identity. Let |f| be the
number of paths of f. Then:
|f| = |f0|+|f1|
where f0 and f1 are the two cofactors of f. Uses the
identity |f'| = |f|, to improve the utilization of the (local) cache.
Returns the number of paths of the function rooted at node.
- Side Effects None
- Defined in
cuddUtil.c
static double
ddCountPathsToNonZero(
DdNode * N,
st_table * table
)
- Performs the recursive step of Cudd_CountPathsToNonZero.
It is based on the following identity. Let |f| be the
number of paths of f. Then:
|f| = |f0|+|f1|
where f0 and f1 are the two cofactors of f. Returns the number of
paths of the function rooted at node.
- Side Effects None
- Defined in
cuddUtil.c
static int
ddCountRoots(
DdManager * table,
int lower,
int upper
)
- Counts the number of roots at the levels between lower and
upper. The computation is based on breadth-first search.
A node is a root if it is not reachable from any previously visited node.
(All the nodes at level lower are therefore considered roots.)
The visited flag uses the LSB of the next pointer. Returns the root
count. The roots that are constant nodes are always ignored.
- Side Effects None
- See Also
ddClearGlobal
- Defined in
cuddExact.c
static void
ddCreateGroup(
DdManager * table,
int x,
int y
)
- Creates a group encompassing variables from x to y in the
DD table. In the current implementation it must be y == x+1.
Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddGroup.c
static int
ddDagInt(
DdNode * n
)
- Performs the recursive step of Cudd_DagSize. Returns the
number of nodes in the graph rooted at n.
- Side Effects None
- Defined in
cuddUtil.c
static void
ddDissolveGroup(
DdManager * table,
int x,
int y
)
- x and y are variables in a group to be cut in two. The cut
is to pass between x and y.
- Side Effects None
- Defined in
cuddGroup.c
static int
ddDoDumpBlif(
DdManager * dd,
DdNode * f,
FILE * fp,
st_table * visited,
char ** names,
int mv
)
- Performs the recursive step of Cudd_DumpBlif. Traverses
the BDD f and writes a multiplexer-network description to the file
pointed by fp in blif format. f is assumed to be a regular pointer
and ddDoDumpBlif guarantees this assumption in the recursive calls.
- Side Effects None
- Defined in
cuddExport.c
static int
ddDoDumpDDcal(
DdManager * dd,
DdNode * f,
FILE * fp,
st_table * visited,
char ** names,
unsigned long mask
)
- Performs the recursive step of Cudd_DumpDDcal. Traverses
the BDD f and writes a line for each node to the file
pointed by fp in DDcal format. f is assumed to be a regular pointer
and ddDoDumpDDcal guarantees this assumption in the recursive calls.
- Side Effects None
- Defined in
cuddExport.c
static int
ddDoDumpDaVinci(
DdManager * dd,
DdNode * f,
FILE * fp,
st_table * visited,
char ** names,
unsigned long mask
)
- Performs the recursive step of Cudd_DumpDaVinci.
- Side Effects None
- Defined in
cuddExport.c
static int
ddDoDumpFactoredForm(
DdManager * dd,
DdNode * f,
FILE * fp,
char ** names
)
- Performs the recursive step of
Cudd_DumpFactoredForm. Traverses the BDD f and writes a factored
form for each node to the file pointed by fp in terms of the
factored forms of the children. Constants are propagated, and
absorption is applied. f is assumed to be a regular pointer and
ddDoDumpFActoredForm guarantees this assumption in the recursive
calls.
- Side Effects None
- See Also
Cudd_DumpFactoredForm
- Defined in
cuddExport.c
static int
ddEpdCountMintermAux(
DdNode * node,
EpDouble * max,
EpDouble * epd,
st_table * table
)
- Performs the recursive step of Cudd_EpdCountMinterm.
It is based on the following identity. Let |f| be the
number of minterms of f. Then:
|f| = (|f0|+|f1|)/2
where f0 and f1 are the two cofactors of f. Does not use the
identity |f'| = max - |f|, to minimize loss of accuracy due to
roundoff. Returns the number of minterms of the function rooted at
node.
- Side Effects None
- Defined in
cuddUtil.c
static enum st_retval
ddEpdFree(
char * key,
char * value,
char * arg
)
- Frees the memory used to store the minterm counts
recorded in the visited table. Returns ST_CONTINUE.
- Side Effects None
- Defined in
cuddUtil.c
static int
ddExchange(
DdManager * table,
int x,
int y,
double temp
)
- This is the same funcion as ddSwapping except for
comparison expression. Use probability function, exp(-size_change/temp).
- Side Effects None
- Defined in
cuddAnneal.c
static int
ddExtSymmCheck(
DdManager * table,
int x,
int y
)
- Checks for extended symmetry of x and y. Returns 1 in
case of extended symmetry; 0 otherwise.
- Side Effects None
- Defined in
cuddGroup.c
static DdNode *
ddFindEssentialRecur(
DdManager * dd,
DdNode * f
)
- Implements the recursive step of Cudd_FindEssential.
Returns a pointer to the cube BDD if successful; NULL otherwise.
- Side Effects None
- Defined in
cuddEssent.c
static void
ddFindNodeHiLo(
DdManager * table,
MtrNode * treenode,
int * lower,
int * upper
)
- Finds the lower and upper bounds of the group
represented by treenode. From the index and size fields we need to
derive the current positions, and find maximum and minimum.
- Side Effects The bounds are returned as side effects.
- Defined in
cuddGroup.c
static DdTlcInfo *
ddFindTwoLiteralClausesRecur(
DdManager * dd,
DdNode * f,
st_table * table
)
- Implements the recursive step of
Cudd_FindTwoLiteralClauses. The DD node is assumed to be not
constant. Returns a pointer to a set of clauses if successful; NULL
otherwise.
- Side Effects None
- See Also
Cudd_FindTwoLiteralClauses
- Defined in
cuddEssent.c
static void
ddFixLimits(
DdManager * unique
)
- Adjusts the values of table fields controlling the.
sizes of subtables and computed table. If the computed table is too small
according to the new values, it is resized.
- Side Effects Modifies manager fields. May resize computed table.
- Defined in
cuddTable.c
static int
ddGroupMoveBackward(
DdManager * table,
int x,
int y
)
- Undoes the swap two groups. Returns 1 in case of
success; 0 otherwise.
- Side Effects None
- Defined in
cuddGroup.c
static int
ddGroupMove(
DdManager * table,
int x,
int y,
Move ** moves
)
- Swaps two groups and records the move. Returns the
number of keys in the DD table in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddGroup.c
static int
ddGroupSiftingAux(
DdManager * table,
int x,
int xLow,
int xHigh,
DD_CHKFP checkFunction,
int lazyFlag
)
- Sifts one variable up and down until it has taken all
positions. Checks for aggregation. There may be at most two sweeps,
even if the group grows. Assumes that x is either an isolated
variable, or it is the bottom of a group. All groups may not have
been found. The variable being moved is returned to the best position
seen during sifting. Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddGroup.c
static int
ddGroupSiftingBackward(
DdManager * table,
Move * moves,
int size,
int upFlag,
int lazyFlag
)
- Determines the best position for a variables and returns
it there. Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddGroup.c
static int
ddGroupSiftingDown(
DdManager * table,
int x,
int xHigh,
DD_CHKFP checkFunction,
Move ** moves
)
- Sifts down a variable until it reaches position xHigh.
Assumes that x is the bottom of a group (or a singleton). Records
all the moves. Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddGroup.c
static int
ddGroupSiftingUp(
DdManager * table,
int y,
int xLow,
DD_CHKFP checkFunction,
Move ** moves
)
- Sifts up a variable until either it reaches position
xLow or the size of the DD heap increases too much. Assumes that y is
the top of a group (or a singleton). Checks y for aggregation to the
adjacent variables. Records all the moves that are appended to the
list of moves received as input and returned as a side effect.
Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddGroup.c
static int
ddGroupSifting(
DdManager * table,
int lower,
int upper,
DD_CHKFP checkFunction,
int lazyFlag
)
- Sifts from treenode->low to treenode->high. If
croupcheck == CUDD_GROUP_CHECK7, it checks for group creation at the
end of the initial sifting. If a group is created, it is then sifted
again. After sifting one variable, the group that contains it is
dissolved. Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddGroup.c
static int
ddIsIthAddVarPair(
DdManager * dd,
DdNode * f,
DdNode * g,
unsigned int i
)
- Comparison of a pair of functions to the i-th ADD
variable. Returns 1 if the functions are the i-th ADD variable and its
complement; 0 otherwise.
- Side Effects None
- Defined in
cuddCompose.c
static int
ddIsIthAddVar(
DdManager * dd,
DdNode * f,
unsigned int i
)
- Comparison of a function to the i-th ADD variable. Returns 1 if
the function is the i-th ADD variable; 0 otherwise.
- Side Effects None
- Defined in
cuddCompose.c
static int
ddIsVarHandled(
DdManager * dd,
int index
)
- Checks whether a variables is already handled. This
function is used for lazy sifting.
- Side Effects none
- Defined in
cuddGroup.c
static int
ddJumpingAux(
DdManager * table,
int x,
int x_low,
int x_high,
double temp
)
- If x==x_low, it executes jumping_down. If x==x_high, it
executes jumping_up. This funcion is similar to ddSiftingAux. Returns
1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddAnneal.c
static Move *
ddJumpingDown(
DdManager * table,
int x,
int x_high,
int initial_size
)
- This is a simplified version of ddSiftingDown. It does not
use lower bounding. Returns the set of moves in case of success; NULL
if memory is full.
- Side Effects None
- Defined in
cuddAnneal.c
static Move *
ddJumpingUp(
DdManager * table,
int x,
int x_low,
int initial_size
)
- This is a simplified version of ddSiftingUp. It does not
use lower bounding. Returns the set of moves in case of success; NULL
if memory is full.
- Side Effects None
- Defined in
cuddAnneal.c
static unsigned int
ddLCHash(
DdNodePtr * key,
unsigned int keysize,
int shift
)
- Computes the hash value for a local cache. Returns the
bucket index.
- Side Effects None
- Defined in
cuddLCache.c
static int
ddLeavesInt(
DdNode * n
)
- Performs the recursive step of Cudd_CountLeaves. Returns
the number of leaves in the DD rooted at n.
- Side Effects None
- See Also
Cudd_CountLeaves
- Defined in
cuddUtil.c
static int
ddLinearAndSiftingAux(
DdManager * table,
int x,
int xLow,
int xHigh
)
- Given xLow <= x <= xHigh moves x up and down between the
boundaries. At each step a linear transformation is tried, and, if it
decreases the size of the DD, it is accepted. Finds the best position
and does the required changes. Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddLinear.c
static int
ddLinearAndSiftingBackward(
DdManager * table,
int size,
Move * moves
)
- Given a set of moves, returns the DD heap to the
position giving the minimum size. In case of ties, returns to the
closest position giving the minimum size. Returns 1 in case of
success; 0 otherwise.
- Side Effects None
- Defined in
cuddLinear.c
static Move *
ddLinearAndSiftingDown(
DdManager * table,
int x,
int xHigh,
Move * prevMoves
)
- Sifts a variable down and applies linear
transformations. Moves x down until either it reaches the bound
(xHigh) or the size of the DD heap increases too much. Returns the
set of moves in case of success; NULL if memory is full.
- Side Effects None
- Defined in
cuddLinear.c
static Move *
ddLinearAndSiftingUp(
DdManager * table,
int y,
int xLow,
Move * prevMoves
)
- Sifts a variable up and applies linear transformations.
Moves y up until either it reaches the bound (xLow) or the size of
the DD heap increases too much. Returns the set of moves in case of
success; NULL if memory is full.
- Side Effects None
- Defined in
cuddLinear.c
static int
ddLinearUniqueCompare(
int * ptrX,
int * ptrY
)
- Comparison function used by qsort to order the
variables according to the number of keys in the subtables.
Returns the difference in number of keys between the two
variables being compared.
- Side Effects None
- Defined in
cuddLinear.c
static void
ddMergeGroups(
DdManager * table,
MtrNode * treenode,
int low,
int high
)
- Creates a single group from low to high and adjusts the
index field of the tree node.
- Side Effects None
- Defined in
cuddGroup.c
static int
ddNoCheck(
DdManager * table,
int x,
int y
)
- Pretends to check two variables for aggregation. Always
returns 0.
- Side Effects None
- Defined in
cuddGroup.c
static void
ddPatchTree(
DdManager * dd,
MtrNode * treenode
)
- Fixes a variable tree after the insertion of new subtables.
After such an insertion, the low fields of the tree below the insertion
point are inconsistent.
- Side Effects None
- Defined in
cuddTable.c
static int
ddPermuteWindow3(
DdManager * table,
int x
)
- Tries all the permutations of the three variables between
x and x+2 and retains the best. Assumes that no dead nodes are
present. Returns the index of the best permutation (1-6) in case of
success; 0 otherwise.Assumes that no dead nodes are present. Returns
the index of the best permutation (1-6) in case of success; 0
otherwise.
- Side Effects None
- Defined in
cuddWindow.c
static int
ddPermuteWindow4(
DdManager * table,
int w
)
- Tries all the permutations of the four variables between
w and w+3 and retains the best. Assumes that no dead nodes are
present. Returns the index of the best permutation (1-24) in case of
success; 0 otherwise.
- Side Effects None
- Defined in
cuddWindow.c
static int
ddPickArbitraryMinterms(
DdManager * dd,
DdNode * node,
int nvars,
int nminterms,
char ** string
)
- Performs the recursive step of Cudd_bddPickArbitraryMinterms.
Returns 1 if successful; 0 otherwise.
- Side Effects none
- See Also
Cudd_bddPickArbitraryMinterms
- Defined in
cuddUtil.c
static int
ddPickRepresentativeCube(
DdManager * dd,
DdNode * node,
double * weight,
char * string
)
- Finds a representative cube of a BDD with the weight of
each variable. From the top variable, if the weight is greater than or
equal to 0.0, choose THEN branch unless the child is the constant 0.
Otherwise, choose ELSE branch unless the child is the constant 0.
- Side Effects Cudd_SubsetWithMaskVars Cudd_bddPickOneCube
- Defined in
cuddUtil.c
static void
ddPrintMintermAux(
DdManager * dd, manager
DdNode * node, current node
int * list current recursion path
)
- Performs the recursive step of Cudd_PrintMinterm.
- Side Effects None
- Defined in
cuddUtil.c
static void
ddRehashZdd(
DdManager * unique,
int i
)
- Rehashes a ZDD unique subtable.
- Side Effects None
- See Also
cuddRehash
- Defined in
cuddTable.c
static int
ddReorderChildren(
DdManager * table,
MtrNode * treenode,
Cudd_ReorderingType method
)
- Reorders the children of a group tree node according to
the options. After reordering puts all the variables in the group
and/or its descendents in a single group. This allows hierarchical
reordering. If the variables in the group do not exist yet, simply
does nothing. Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddGroup.c
static int
ddReorderPostprocess(
DdManager * table
)
- Cleans up at the end of reordering.
- Side Effects None
- Defined in
cuddReorder.c
static int
ddReorderPreprocess(
DdManager * table
)
- Prepares the DD heap for dynamic reordering. Does
garbage collection, to guarantee that there are no dead nodes;
clears the cache, which is invalidated by dynamic reordering; initializes
the number of isolated projection functions; and initializes the
interaction matrix. Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddReorder.c
static void
ddReportRefMess(
DdManager * unique, manager
int i, table in which the problem occurred
const char * caller procedure that detected the problem
)
- Reports problem in garbage collection.
- Side Effects None
- See Also
cuddGarbageCollect
cuddGarbageCollectZdd
- Defined in
cuddTable.c
static int
ddResetVarHandled(
DdManager * dd,
int index
)
- Resets a variable to be processed. This function is used
for lazy sifting.
- Side Effects none
- Defined in
cuddGroup.c
static int
ddResizeTable(
DdManager * unique,
int index
)
- Increases the number of subtables in a unique table so
that it meets or exceeds index. Returns 1 if successful; 0 otherwise.
- Side Effects None
- See Also
cuddResizeTableZdd
- Defined in
cuddTable.c
static int
ddSecDiffCheck(
DdManager * table,
int x,
int y
)
- Checks two variables for aggregation. The check is based
on the second difference of the number of nodes as a function of the
layer. If the second difference is lower than a given threshold
(typically negative) then the two variables should be aggregated.
Returns 1 if the two variables pass the test; 0 otherwise.
- Side Effects None
- Defined in
cuddGroup.c
static int
ddSetVarHandled(
DdManager * dd,
int index
)
- Sets a variable to already handled. This function is used
for lazy sifting.
- Side Effects none
- Defined in
cuddGroup.c
static int
ddShuffle(
DdManager * table,
DdHalfWord * permutation,
int lower,
int upper
)
- Reorders variables according to a given permutation.
The i-th permutation array contains the index of the variable that
should be brought to the i-th level. ddShuffle assumes that no
dead nodes are present and that the interaction matrix is properly
initialized. The reordering is achieved by a series of upward sifts.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddExact.c
static int
ddShuffle(
DdManager * table,
int * permutation
)
- Reorders variables according to a given permutation.
The i-th permutation array contains the index of the variable that
should be brought to the i-th level. ddShuffle assumes that no
dead nodes are present and that the interaction matrix is properly
initialized. The reordering is achieved by a series of upward sifts.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddReorder.c
static int
ddSiftUp(
DdManager * table,
int x,
int xLow
)
- Takes a variable from position x and sifts it up to
position xLow; xLow should be less than or equal to x.
Returns 1 if successful; 0 otherwise
- Side Effects None
- Defined in
cuddExact.c
static int
ddSiftUp(
DdManager * table,
int x,
int xLow
)
- Takes a variable from position x and sifts it up to
position xLow; xLow should be less than or equal to x.
Returns 1 if successful; 0 otherwise
- Side Effects None
- Defined in
cuddReorder.c
static int
ddSiftingAux(
DdManager * table,
int x,
int xLow,
int xHigh
)
- Given xLow <= x <= xHigh moves x up and down between the
boundaries. Finds the best position and does the required changes.
Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddReorder.c
static int
ddSiftingBackward(
DdManager * table,
int size,
Move * moves
)
- Given a set of moves, returns the DD heap to the
position giving the minimum size. In case of ties, returns to the
closest position giving the minimum size. Returns 1 in case of
success; 0 otherwise.
- Side Effects None
- Defined in
cuddReorder.c
static Move *
ddSiftingDown(
DdManager * table,
int x,
int xHigh
)
- Sifts a variable down. Moves x down until either it
reaches the bound (xHigh) or the size of the DD heap increases too
much. Returns the set of moves in case of success; NULL if memory is
full.
- Side Effects None
- Defined in
cuddReorder.c
static Move *
ddSiftingUp(
DdManager * table,
int y,
int xLow
)
- Sifts a variable up. Moves y up until either it reaches
the bound (xLow) or the size of the DD heap increases too much.
Returns the set of moves in case of success; NULL if memory is full.
- Side Effects None
- Defined in
cuddReorder.c
static void
ddSuppInteract(
DdNode * f,
int * support
)
- Performs a DFS from f. Uses the LSB of the then pointer
as visited flag.
- Side Effects Accumulates in support the variables on which f depends.
- Defined in
cuddInteract.c
static void
ddSupportStep(
DdNode * f,
int * support
)
- Performs the recursive step of Cudd_Support. Performs a
DFS from f. The support is accumulated in supp as a side effect. Uses
the LSB of the then pointer as visited flag.
- Side Effects None
- See Also
ddClearFlag
- Defined in
cuddUtil.c
static Move *
ddSwapAny(
DdManager * table,
int x,
int y
)
- Swaps any two variables. Returns the set of moves.
- Side Effects None
- Defined in
cuddReorder.c
static int
ddSymmGroupMoveBackward(
DdManager * table,
int x,
int y
)
- Undoes the swap of two groups. x is assumed to be the
bottom variable of the first group. y is assumed to be the top
variable of the second group. Returns the number of keys in the table
if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddSymmetry.c
static int
ddSymmGroupMove(
DdManager * table,
int x,
int y,
Move ** moves
)
- Swaps two groups. x is assumed to be the bottom variable
of the first group. y is assumed to be the top variable of the second
group. Updates the list of moves. Returns the number of keys in the
table if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddSymmetry.c
static int
ddSymmSiftingAux(
DdManager * table,
int x,
int xLow,
int xHigh
)
- Given xLow <= x <= xHigh moves x up and down between the
boundaries. Finds the best position and does the required changes.
Assumes that x is not part of a symmetry group. Returns 1 if
successful; 0 otherwise.
- Side Effects None
- Defined in
cuddSymmetry.c
static int
ddSymmSiftingBackward(
DdManager * table,
Move * moves,
int size
)
- Given a set of moves, returns the DD heap to the
position giving the minimum size. In case of ties, returns to the
closest position giving the minimum size. Returns 1 in case of
success; 0 otherwise.
- Side Effects None
- Defined in
cuddSymmetry.c
static int
ddSymmSiftingConvAux(
DdManager * table,
int x,
int xLow,
int xHigh
)
- Given xLow <= x <= xHigh moves x up and down between the
boundaries. Finds the best position and does the required changes.
Assumes that x is either an isolated variable, or it is the bottom of
a symmetry group. All symmetries may not have been found, because of
exceeded growth limit. Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddSymmetry.c
static Move *
ddSymmSiftingDown(
DdManager * table,
int x,
int xHigh
)
- Moves x down until either it reaches the bound (xHigh)
or the size of the DD heap increases too much. Assumes that x is the
bottom of a symmetry group. Checks x for symmetry to the adjacent
variables. If symmetry is found, the symmetry group of x is merged
with the symmetry group of the other variable. Returns the set of
moves in case of success; MV_OOM if memory is full.
- Side Effects None
- Defined in
cuddSymmetry.c
static Move *
ddSymmSiftingUp(
DdManager * table,
int y,
int xLow
)
- Moves x up until either it reaches the bound (xLow) or
the size of the DD heap increases too much. Assumes that x is the top
of a symmetry group. Checks x for symmetry to the adjacent
variables. If symmetry is found, the symmetry group of x is merged
with the symmetry group of the other variable. Returns the set of
moves in case of success; MV_OOM if memory is full.
- Side Effects None
- Defined in
cuddSymmetry.c
static void
ddSymmSummary(
DdManager * table,
int lower,
int upper,
int * symvars,
int * symgroups
)
- Counts numbers of symmetric variables and symmetry
groups.
- Side Effects None
- Defined in
cuddSymmetry.c
static int
ddSymmUniqueCompare(
int * ptrX,
int * ptrY
)
- Comparison function used by qsort to order the variables
according to the number of keys in the subtables.
Returns the difference in number of keys between the two
variables being compared.
- Side Effects None
- Defined in
cuddSymmetry.c
static int
ddTreeSiftingAux(
DdManager * table,
MtrNode * treenode,
Cudd_ReorderingType method
)
- Recursively visits the group tree and reorders each
group in postorder fashion. Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddGroup.c
static Move*
ddUndoMoves(
DdManager * table,
Move * moves
)
- Given a set of moves, returns the DD heap to the
order in effect before the moves. Returns 1 in case of success;
0 otherwise.
- Side Effects None
- Defined in
cuddLinear.c
static int
ddUniqueCompareGroup(
int * ptrX,
int * ptrY
)
- Comparison function used by qsort to order the variables
according to the number of keys in the subtables. Returns the
difference in number of keys between the two variables being
compared.
- Side Effects None
- Defined in
cuddGroup.c
static int
ddUniqueCompare(
int * ptrX,
int * ptrY
)
- Comparison function used by qsort to order the
variables according to the number of keys in the subtables.
Returns the difference in number of keys between the two
variables being compared.
- Side Effects None
- Defined in
cuddReorder.c
static void
ddUpdateInteract(
DdManager * table,
int * support
)
- If support[i
- Side Effects None
- Defined in
cuddInteract.c
static int
ddUpdateMtrTree(
DdManager * table,
MtrNode * treenode,
int * perm,
int * invperm
)
- Updates the BDD variable group tree before a shuffle.
Returns 1 if successful; 0 otherwise.
- Side Effects Changes the BDD variable group tree.
- Defined in
cuddReorder.c
static int
ddVarGroupCheck(
DdManager * table,
int x,
int y
)
- Checks for grouping of x and y. Returns 1 in
case of grouping; 0 otherwise. This function is used for lazy sifting.
- Side Effects None
- Defined in
cuddGroup.c
static int
ddWindow2(
DdManager * table,
int low,
int high
)
- Reorders by applying a sliding window of width 2.
Tries both permutations of the variables in a window
that slides from low to high. Assumes that no dead nodes are
present. Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddWindow.c
static int
ddWindow3(
DdManager * table,
int low,
int high
)
- Reorders by applying a sliding window of width 3.
Tries all possible permutations to the variables in a
window that slides from low to high. Assumes that no dead nodes are
present. Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddWindow.c
static int
ddWindow4(
DdManager * table,
int low,
int high
)
- Reorders by applying a sliding window of width 4.
Tries all possible permutations to the variables in a
window that slides from low to high. Assumes that no dead nodes are
present. Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddWindow.c
static int
ddWindowConv2(
DdManager * table,
int low,
int high
)
- Reorders by repeatedly applying a sliding window of width
2. Tries both permutations of the variables in a window
that slides from low to high. Assumes that no dead nodes are
present. Uses an event-driven approach to determine convergence.
Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddWindow.c
static int
ddWindowConv3(
DdManager * table,
int low,
int high
)
- Reorders by repeatedly applying a sliding window of width
3. Tries all possible permutations to the variables in a
window that slides from low to high. Assumes that no dead nodes are
present. Uses an event-driven approach to determine convergence.
Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddWindow.c
static int
ddWindowConv4(
DdManager * table,
int low,
int high
)
- Reorders by repeatedly applying a sliding window of width
4. Tries all possible permutations to the variables in a
window that slides from low to high. Assumes that no dead nodes are
present. Uses an event-driven approach to determine convergence.
Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddWindow.c
static void
debugCheckParent(
DdManager * table,
DdNode * node
)
- Searches all the subtables above node. Very expensive.
The same check is now implemented more efficiently in ddDebugCheck.
- Side Effects None
- See Also
debugFindParent
- Defined in
cuddCheck.c
static void
debugFindParent(
DdManager * table,
DdNode * node
)
- Searches the subtables above node for its parents.
- Side Effects None
- Defined in
cuddCheck.c
static int
dp2(
DdManager * dd,
DdNode * f,
st_table * t
)
- Performs the recursive step of cuddP. Returns 1 in case
of success; 0 otherwise.
- Side Effects None
- Defined in
cuddUtil.c
static DdTlcInfo *
emptyClauseSet(
)
- Returns a pointer to an empty set of clauses if
successful; NULL otherwise. No bit vector for the phases is
allocated.
- Side Effects None
- Defined in
cuddEssent.c
static int
equalp(
DdHalfWord var1a,
short phase1a,
DdHalfWord var1b,
short phase1b,
DdHalfWord var2a,
short phase2a,
DdHalfWord var2b,
short phase2b
)
- Returns true iff the two arguments are identical
clauses. Since literals are sorted, we only need to compare
literals in the same position.
- Side Effects None
- See Also
beforep
- Defined in
cuddEssent.c
static double
find_average_fitness(
)
- Returns the average fitness of the population.
- Side Effects None
- Defined in
cuddGenetic.c
static int
find_best(
)
- Returns the index of the fittest individual.
- Side Effects None
- Defined in
cuddGenetic.c
static void
fixVarTree(
MtrNode * treenode,
int * perm,
int size
)
- Fixes a variable group tree.
- Side Effects Changes the variable group tree.
- Defined in
cuddAPI.c
static void
freeMatrix(
DdHalfWord ** matrix
)
- Frees a two-dimensional matrix allocated by getMatrix.
- Side Effects None
- See Also
getMatrix
- Defined in
cuddExact.c
static enum st_retval
freePathPair(
char * key,
char * value,
char * arg
)
- Frees the entries of the visited symbol table. Returns
ST_CONTINUE.
- Side Effects None
- Defined in
cuddSat.c
static NodeData *
gatherInfoAux(
DdNode * node, function to analyze
ApproxInfo * info, info on BDD
int parity gather parity information
)
- Recursively counts minterms and computes reference
counts of each node in the BDD. Similar to the cuddCountMintermAux
which recursively counts the number of minterms for the dag rooted
at each node in terms of the total number of variables (max). It assumes
that the node pointer passed to it is regular and it maintains the
invariant.
- Side Effects None
- See Also
gatherInfo
- Defined in
cuddApprox.c
static ApproxInfo *
gatherInfo(
DdManager * dd, manager
DdNode * node, function to be analyzed
int numVars, number of variables node depends on
int parity gather parity information
)
- Counts minterms and computes reference counts of each
node in the BDD . The minterm count is separately computed for the
node and its complement. This is to avoid cancellation
errors. Returns a pointer to the data structure holding the
information gathered if successful; NULL otherwise.
- Side Effects None
- See Also
cuddUnderApprox
gatherInfoAux
- Defined in
cuddApprox.c
static int
gcd(
int x,
int y
)
- Returns the gcd of two integers. Uses the binary GCD
algorithm described in Cormen, Leiserson, and Rivest.
- Side Effects None
- Defined in
cuddExact.c
static DdNode *
getCube(
DdManager * manager,
st_table * visited,
DdNode * f,
int cost
)
- Build a BDD for a largest cube of f.
Given the minimum length from the root, and the minimum
lengths for each node (in visited), apply triangulation at each node.
Of the two children of each node on a shortest path, at least one is
on a shortest path. In case of ties the procedure chooses the THEN
children.
Returns a pointer to the cube BDD representing the path if
successful; NULL otherwise.
- Side Effects None
- Defined in
cuddSat.c
static cuddPathPair
getLargest(
DdNode * root,
st_table * visited
)
- Finds the size of the largest cube(s) in a DD.
This problem is translated into finding the shortest paths from a node
when both THEN and ELSE arcs have unit lengths.
Uses a local symbol table to store the lengths for each
node. Only the lengths for the regular nodes are entered in the table,
because those for the complement nodes are simply obtained by swapping
the two lenghts.
Returns a pair of lengths: the length of the shortest path to 1;
and the length of the shortest path to 0. This is done so as to take
complement arcs into account.
- Side Effects none
- Defined in
cuddSat.c
static int
getLevelKeys(
DdManager * table,
int l
)
- Returns the number of nodes at one level of a unique table.
The projection function, if isolated, is not counted.
- Side Effects None
- Defined in
cuddExact.c
static DdHalfWord **
getMatrix(
int rows, number of rows
int cols number of columns
)
- Allocates a two-dimensional matrix of ints.
Returns the pointer to the matrix if successful; NULL otherwise.
- Side Effects None
- See Also
freeMatrix
- Defined in
cuddExact.c
static int
getMaxBinomial(
int n
)
- Computes the maximum value of (n choose k) for a given
n. The maximum value occurs for k = n/2 when n is even, or k =
(n-1)/2 when n is odd. The algorithm used in this procedure avoids
intermediate overflow problems. It is based on the identity
binomial(n,k) = n/k * binomial(n-1,k-1).
Returns the computed value if successful; -1 if out of range.
- Side Effects None
- Defined in
cuddExact.c
static DdNode *
getPath(
DdManager * manager,
st_table * visited,
DdNode * f,
int * weight,
int cost
)
- Build a BDD for a shortest path of f.
Given the minimum length from the root, and the minimum
lengths for each node (in visited), apply triangulation at each node.
Of the two children of each node on a shortest path, at least one is
on a shortest path. In case of ties the procedure chooses the THEN
children.
Returns a pointer to the cube BDD representing the path if
successful; NULL otherwise.
- Side Effects None
- Defined in
cuddSat.c
static cuddPathPair
getShortest(
DdNode * root,
int * cost,
int * support,
st_table * visited
)
- Finds the length of the shortest path(s) in a DD.
Uses a local symbol table to store the lengths for each
node. Only the lengths for the regular nodes are entered in the table,
because those for the complement nodes are simply obtained by swapping
the two lenghts.
Returns a pair of lengths: the length of the shortest path to 1;
and the length of the shortest path to 0. This is done so as to take
complement arcs into account.
- Side Effects Accumulates the support of the DD in support.
- Defined in
cuddSat.c
static void
hashDelete(
DdLevelQueue * queue,
DdQueueItem * item
)
- Removes an item from the hash table of a level queue.
Nothing is done if the item is not in the table.
- Side Effects None
- See Also
cuddLevelQueueDequeue
hashInsert
- Defined in
cuddLevelQ.c
static int
hashInsert(
DdLevelQueue * queue,
DdQueueItem * item
)
- Inserts an item in the hash table of a level queue. Returns
1 if successful; 0 otherwise. No check is performed to see if an item with
the same key is already in the hash table.
- Side Effects None
- See Also
cuddLevelQueueEnqueue
- Defined in
cuddLevelQ.c
static DdQueueItem *
hashLookup(
DdLevelQueue * queue,
void * key
)
- Looks up a key in the hash table of a level queue. Returns
a pointer to the item with the given key if the key is found; NULL
otherwise.
- Side Effects None
- See Also
cuddLevelQueueEnqueue
hashInsert
- Defined in
cuddLevelQ.c
static int
hashResize(
DdLevelQueue * queue
)
- Resizes the hash table of a level queue. Returns 1 if
successful; 0 otherwise.
- Side Effects None
- See Also
hashInsert
- Defined in
cuddLevelQ.c
static int
impliedp(
DdHalfWord var1,
short phase1,
DdHalfWord var2,
short phase2,
BitVector * olv,
BitVector * olp
)
- Returns true iff either literal of a clause is in a set
of literals. The first four arguments specify the clause. The
remaining two arguments specify the literal set.
- Side Effects None
- Defined in
cuddEssent.c
static DdHalfWord *
initSymmInfo(
DdManager * table,
int lower,
int upper
)
- Translates the symmetry information stored in the next
field of each subtable from level to indices. This procedure is called
immediately after symmetric sifting, so that the next fields are correct.
By translating this informaton in terms of indices, we make it independent
of subsequent reorderings. The format used is that of the next fields:
a circular list where each variable points to the next variable in the
same symmetry group. Only the entries between lower and upper are
considered. The procedure returns a pointer to an array
holding the symmetry information if successful; NULL otherwise.
- Side Effects None
- See Also
checkSymmInfo
- Defined in
cuddExact.c
static int
largest(
)
- Finds the largest DD in the population. If an order is
repeated, it avoids choosing the copy that is in the computed table
(it has repeat[i
- Side Effects None
- Defined in
cuddGenetic.c
static int
make_random(
DdManager * table,
int lower
)
- Generates the random sequences for the initial population.
The sequences are permutations of the indices between lower and
upper in the current order.
- Side Effects None
- Defined in
cuddGenetic.c
static DdNode *
mintermsFromUniverse(
DdManager * manager,
DdNode ** vars,
int numVars,
double n,
int index
)
- Recursive procedure to extract n mintems from constant 1.
- Side Effects None
- Defined in
cuddSplit.c
static int
oneliteralp(
DdHalfWord var
)
- Returns true iff the argument is a one-literal clause.
A one-litaral clause has the constant FALSE as second literal.
Since the constant TRUE is never used, it is sufficient to test for
a constant.
- Side Effects None
- Defined in
cuddEssent.c
static void
pushDown(
DdHalfWord * order,
int j,
int level
)
- Pushes a variable in the order down to position "level."
- Side Effects None
- Defined in
cuddExact.c
static int
rand_int(
int a
)
- Generates a random number between 0 and the integer a.
- Side Effects None
- Defined in
cuddGenetic.c
static double
random_generator(
)
- Returns a double precision value between 0.0 and 1.0.
- Side Effects None
- Defined in
cuddAnneal.c
static int
restoreOrder(
DdManager * table,
int * array,
int lower,
int upper
)
- Restores the variable order in array by a series of sifts up.
Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddAnneal.c
static int
roulette(
int * p1,
int * p2
)
- Selects two distinct parents with the roulette wheel method.
- Side Effects The indices of the selected parents are returned as side
effects.
- Defined in
cuddGenetic.c
static DdNode *
selectMintermsFromUniverse(
DdManager * manager,
int * varSeen,
double n
)
- This function prepares an array of variables which have not been
encountered so far when traversing the procedure cuddSplitSetRecur. This
array is then used to extract the required number of minterms from a constant
1. The algorithm guarantees that the size of BDD will be utmost log(n).
- Side Effects None
- Defined in
cuddSplit.c
static int
sentinelp(
DdHalfWord var1,
DdHalfWord var2
)
- Returns true iff the argument is the sentinel clause.
A sentinel clause has both variables equal to 0.
- Side Effects None
- Defined in
cuddEssent.c
static DdNode *
separateCube(
DdManager * dd,
DdNode * f,
CUDD_VALUE_TYPE * distance
)
- Separates cube from distance. Returns the cube if
successful; NULL otherwise.
- Side Effects The distance is returned as a side effect.
- See Also
cuddBddClosestCube
createResult
- Defined in
cuddPriority.c
static int
siftBackwardProb(
DdManager * table,
Move * moves,
int size,
double temp
)
- Otherwise, "tosses a coin" to decide whether to keep
the current configuration or return the DD to the original
one. Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddAnneal.c
static int
sift_up(
DdManager * table,
int x,
int x_low
)
- Takes a variable from position x and sifts it up to
position x_low; x_low should be less than x. Returns 1 if successful;
0 otherwise
- Side Effects None
- Defined in
cuddGenetic.c
static enum st_retval
stPathTableDdFree(
char * key,
char * value,
char * arg
)
- None
- Side Effects None
- Defined in
cuddSubsetSP.c
static enum st_retval
st_zdd_count_dbl_free(
char * key,
char * value,
char * arg
)
- Frees the memory associated with the computed table of
Cudd_zddCountDouble.
- Side Effects None
- Defined in
cuddZddCount.c
static enum st_retval
st_zdd_countfree(
char * key,
char * value,
char * arg
)
- Frees the memory associated with the computed table of
Cudd_zddCount.
- Side Effects None
- Defined in
cuddZddCount.c
static int
stopping_criterion(
int c1,
int c2,
int c3,
int c4,
double temp
)
- If temperature is STOP_TEMP or there is no improvement
then terminates. Returns 1 if the termination criterion is met; 0
otherwise.
- Side Effects None
- Defined in
cuddAnneal.c
static DdTlcInfo *
tlcInfoAlloc(
)
- Returns a pointer to a DdTlcInfo Structure if successful;
NULL otherwise.
- Side Effects None
- See Also
Cudd_tlcInfoFree
- Defined in
cuddEssent.c
static int
updateEntry(
DdManager * table,
DdHalfWord * order,
int level,
int cost,
DdHalfWord ** orders,
int * costs,
int subsets,
char * mask,
int lower,
int upper
)
- Updates entry for a subset. Finds the subset, if it exists.
If the new order for the subset has lower cost, or if the subset did not
exist, it stores the new order and cost. Returns the number of subsets
currently in the table.
- Side Effects None
- Defined in
cuddExact.c
static void
updateParity(
DdNode * node, function to analyze
ApproxInfo * info, info on BDD
int newparity new parity for node
)
- Recursively update the parity of the paths reaching a node.
Assumes that node is regular and propagates the invariant.
- Side Effects None
- See Also
gatherInfoAux
- Defined in
cuddApprox.c
static int
updateRefs(
DdManager * dd,
DdNode * f,
DdNode * skip,
ApproxInfo * info,
DdLevelQueue * queue
)
- Update function reference counts to account for replacement.
Returns the number of nodes saved if successful; 0 otherwise.
- Side Effects None
- See Also
UAmarkNodes
RAmarkNodes
- Defined in
cuddApprox.c
static int
updateUB(
DdManager * table,
int oldBound,
DdHalfWord * bestOrder,
int lower,
int upper
)
- Updates the upper bound and saves the best order seen so far.
Returns the current value of the upper bound.
- Side Effects None
- Defined in
cuddExact.c
static int
zddCountInternalMtrNodes(
DdManager * table,
MtrNode * treenode
)
- Counts the number of internal nodes of the group tree.
Returns the count.
- Side Effects None
- Defined in
cuddZddGroup.c
static void
zddFindNodeHiLo(
DdManager * table,
MtrNode * treenode,
int * lower,
int * upper
)
- Finds the lower and upper bounds of the group represented
by treenode. The high and low fields of treenode are indices. From
those we need to derive the current positions, and find maximum and
minimum.
- Side Effects The bounds are returned as side effects.
- Defined in
cuddZddGroup.c
static void
zddFixTree(
DdManager * table,
MtrNode * treenode
)
- Fixes the ZDD variable group tree after a
shuffle. Assumes that the order of the variables in a terminal node
has not been changed.
- Side Effects Changes the ZDD variable group tree.
- Defined in
cuddZddReord.c
static int
zddGroupMoveBackward(
DdManager * table,
int x,
int y
)
- Undoes the swap two groups. Returns 1 in case of
success; 0 otherwise.
- Side Effects None
- Defined in
cuddZddGroup.c
static int
zddGroupMove(
DdManager * table,
int x,
int y,
Move ** moves
)
- Swaps two groups and records the move. Returns the
number of keys in the DD table in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddZddGroup.c
static int
zddGroupSiftingAux(
DdManager * table,
int x,
int xLow,
int xHigh
)
- Sifts one variable up and down until it has taken all
positions. Checks for aggregation. There may be at most two sweeps,
even if the group grows. Assumes that x is either an isolated
variable, or it is the bottom of a group. All groups may not have
been found. The variable being moved is returned to the best position
seen during sifting. Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddZddGroup.c
static int
zddGroupSiftingBackward(
DdManager * table,
Move * moves,
int size
)
- Determines the best position for a variables and returns
it there. Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddZddGroup.c
static int
zddGroupSiftingDown(
DdManager * table,
int x,
int xHigh,
Move ** moves
)
- Sifts down a variable until it reaches position xHigh.
Assumes that x is the bottom of a group (or a singleton). Records
all the moves. Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddZddGroup.c
static int
zddGroupSiftingUp(
DdManager * table,
int y,
int xLow,
Move ** moves
)
- Sifts up a variable until either it reaches position
xLow or the size of the DD heap increases too much. Assumes that y is
the top of a group (or a singleton). Checks y for aggregation to the
adjacent variables. Records all the moves that are appended to the
list of moves received as input and returned as a side effect.
Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddZddGroup.c
static int
zddGroupSifting(
DdManager * table,
int lower,
int upper
)
- Sifts from treenode->low to treenode->high. If
croupcheck == CUDD_GROUP_CHECK7, it checks for group creation at the
end of the initial sifting. If a group is created, it is then sifted
again. After sifting one variable, the group that contains it is
dissolved. Returns 1 in case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddZddGroup.c
static void
zddMergeGroups(
DdManager * table,
MtrNode * treenode,
int low,
int high
)
- Creates a single group from low to high and adjusts the
idex field of the tree node.
- Side Effects None
- Defined in
cuddZddGroup.c
static DdNode *
zddPortFromBddStep(
DdManager * dd,
DdNode * B,
int expected
)
- Performs the recursive step of Cudd_zddPortFromBdd.
- Side Effects None
- Defined in
cuddZddPort.c
static DdNode *
zddPortToBddStep(
DdManager * dd, manager
DdNode * f, ZDD to be converted
int depth recursion depth
)
- Performs the recursive step of Cudd_zddPortToBdd.
- Side Effects None
- Defined in
cuddZddPort.c
static void
zddPrintCoverAux(
DdManager * zdd, manager
DdNode * node, current node
int level, depth in the recursion
int * list current recursion path
)
- Performs the recursive step of Cudd_zddPrintCover.
- Side Effects None
- Defined in
cuddZddUtil.c
static int
zddReorderChildren(
DdManager * table,
MtrNode * treenode,
Cudd_ReorderingType method
)
- Reorders the children of a group tree node according to
the options. After reordering puts all the variables in the group
and/or its descendents in a single group. This allows hierarchical
reordering. If the variables in the group do not exist yet, simply
does nothing. Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddZddGroup.c
static int
zddReorderPostprocess(
DdManager * table
)
- Shrinks almost empty subtables at the end of reordering to
guarantee that they have a reasonable load factor. However, if there many
nodes are being reclaimed, then no resizing occurs. Returns 1 in case of
success; 0 otherwise.
- Side Effects None
- Defined in
cuddZddReord.c
static void
zddReorderPreprocess(
DdManager * table
)
- Prepares the ZDD heap for dynamic reordering. Does
garbage collection, to guarantee that there are no dead nodes;
and clears the cache, which is invalidated by dynamic reordering.
- Side Effects None
- Defined in
cuddZddReord.c
static int
zddShuffle(
DdManager * table,
int * permutation
)
- Reorders ZDD variables according to a given permutation.
The i-th permutation array contains the index of the variable that
should be brought to the i-th level. zddShuffle assumes that no
dead nodes are present. The reordering is achieved by a series of
upward sifts. Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddZddReord.c
static int
zddSiftUp(
DdManager * table,
int x,
int xLow
)
- Takes a ZDD variable from position x and sifts it up to
position xLow; xLow should be less than or equal to x.
Returns 1 if successful; 0 otherwise
- Side Effects None
- Defined in
cuddZddReord.c
static Move *
zddSwapAny(
DdManager * table,
int x,
int y
)
- Swaps any two variables. Returns the set of moves.
- Side Effects None
- Defined in
cuddZddReord.c
static int
zddTreeSiftingAux(
DdManager * table,
MtrNode * treenode,
Cudd_ReorderingType method
)
- Recursively visits the group tree and reorders each
group in postorder fashion. Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddZddGroup.c
static int
zddUniqueCompareGroup(
int * ptrX,
int * ptrY
)
- Comparison function used by qsort to order the variables
according to the number of keys in the subtables. Returns the
difference in number of keys between the two variables being
compared.
- Side Effects None
- Defined in
cuddZddGroup.c
static void
zddVarToConst(
DdNode * f,
DdNode ** gp,
DdNode ** hp,
DdNode * base,
DdNode * empty
)
- Replaces variables with constants if possible (part of
canonical form).
- Side Effects None
- Defined in
cuddZddSetop.c
static int
zdd_group_move_backward(
DdManager * table,
int x,
int y
)
- Undoes the swap of two groups. x is assumed to be the
bottom variable of the first group. y is assumed to be the top
variable of the second group. Returns 1 if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddZddSymm.c
static int
zdd_group_move(
DdManager * table,
int x,
int y,
Move ** moves
)
- Swaps two groups. x is assumed to be the bottom variable
of the first group. y is assumed to be the top variable of the second
group. Updates the list of moves. Returns the number of keys in the
table if successful; 0 otherwise.
- Side Effects None
- Defined in
cuddZddSymm.c
static void
zdd_print_minterm_aux(
DdManager * zdd, manager
DdNode * node, current node
int level, depth in the recursion
int * list current recursion path
)
- Performs the recursive step of Cudd_zddPrintMinterm.
- Side Effects None
- Defined in
cuddZddUtil.c
static DdNode *
zdd_subset0_aux(
DdManager * zdd,
DdNode * P,
DdNode * zvar
)
- Performs the recursive step of Cudd_zddSubset0.
- Side Effects None
- Defined in
cuddZddSetop.c
static DdNode *
zdd_subset1_aux(
DdManager * zdd,
DdNode * P,
DdNode * zvar
)
- Performs the recursive step of Cudd_zddSubset1.
- Side Effects None
- Defined in
cuddZddSetop.c
static int
zp2(
DdManager * zdd,
DdNode * f,
st_table * t
)
- Performs the recursive step of cuddZddP. Returns 1 in
case of success; 0 otherwise.
- Side Effects None
- Defined in
cuddZddUtil.c
(
)
- Adds node to the head of the free list. Does not
deallocate memory chunks that become free. This function is also
used by the dynamic reordering functions.
- Side Effects None
- See Also
cuddAllocNode
cuddDynamicAllocNode
cuddDeallocMove
- Defined in
cuddInt.h
(
)
- Adds node to the head of the free list. Does not
deallocate memory chunks that become free. This function is also
used by the dynamic reordering functions.
- Side Effects None
- See Also
cuddDeallocNode
cuddDynamicAllocNode
- Defined in
cuddInt.h
(
)
- Clears the 4 least significant bits of a pointer.
- Side Effects none
- Defined in
cuddInt.h
(
)
- Complements a DD if condition c is true; c should be
either 0 or 1, because it is used directly (for efficiency). If in
doubt on the values c may take, use "(c) ? Cudd_Not(node) : node".
- Side Effects none
- See Also
Cudd_Not
- Defined in
cudd.h
(
)
- Complements a DD by flipping the complement attribute of
the pointer (the least significant bit).
- Side Effects none
- See Also
Cudd_NotCond
- Defined in
cudd.h
(
)
- Computes hash function for keys of three operands.
- Side Effects None
- See Also
ddLCHash2
ddLCHash
- Defined in
cuddLCache.c
(
)
- Computes hash function for keys of two operands.
- Side Effects None
- See Also
ddLCHash3
ddLCHash
- Defined in
cuddLCache.c
(
)
- Computes the absolute value of a number.
- Side Effects none
- Defined in
cuddInt.h
(
)
- Computes the maximum of two numbers.
- Side Effects none
- See Also
ddMin
- Defined in
cuddInt.h
(
)
- Computes the minimum of two numbers.
- Side Effects none
- See Also
ddMax
- Defined in
cuddInt.h
(
)
- Decreases the reference count of node. It is primarily
used in recursive procedures to decrease the ref count of a result
node before returning it. This accomplishes the goal of removing the
protection applied by a previous cuddRef. This being a macro, it is
faster than Cudd_Deref, but it cannot be used in constructs like
cuddDeref(a = b()).
- Side Effects none
- See Also
Cudd_Deref
- Defined in
cuddInt.h
(
)
- Enforces DD_MINUS_INF_VAL <= x <= DD_PLUS_INF_VAL.
Furthermore, if x <= DD_MINUS_INF_VAL/2, x is set to
DD_MINUS_INF_VAL. Similarly, if DD_PLUS_INF_VAL/2 <= x, x is set to
DD_PLUS_INF_VAL. Normally this macro is a NOOP. However, if
HAVE_IEEE_754 is not defined, it makes sure that a value does not
get larger than infinity in absolute value, and once it gets to
infinity, stays there. If the value overflows before this macro is
applied, no recovery is possible.
- Side Effects none
- Defined in
cuddInt.h
(
)
- Extract the least significant digit of a double digit. Used
in the manipulation of arbitrary precision integers.
- Side Effects None
- See Also
DD_MSDIGIT
- Defined in
cuddInt.h
(
)
- Extract the most significant digit of a double digit. Used
in the manipulation of arbitrary precision integers.
- Side Effects None
- See Also
DD_LSDIGIT
- Defined in
cuddInt.h
(
)
- Finds the current position of ZDD variable index in the
order. This macro duplicates the functionality of Cudd_ReadPermZdd,
but it does not check for out-of-bounds indices and it is more
efficient.
- Side Effects none
- See Also
Cudd_ReadPermZdd
- Defined in
cuddInt.h
(
)
- Finds the current position of variable index in the
order. This macro duplicates the functionality of Cudd_ReadPerm,
but it does not check for out-of-bounds indices and it is more
efficient.
- Side Effects none
- See Also
Cudd_ReadPerm
- Defined in
cuddInt.h
(
)
- Hash function for the cache for functions with two
operands.
- Side Effects none
- See Also
ddHash
ddCHash
- Defined in
cuddInt.h
(
)
- Hash function for the cache.
- Side Effects none
- See Also
ddHash
ddCHash2
- Defined in
cuddInt.h
(
)
- Hash function for the table of a level queue.
- Side Effects None
- See Also
hashInsert
hashLookup
hashDelete
- Defined in
cuddLevelQ.c
(
)
- Hash function for the unique table.
- Side Effects none
- See Also
ddCHash
ddCHash2
- Defined in
cuddInt.h
(
)
- Increases the reference count of a node, if it is not
saturated. This being a macro, it is faster than Cudd_Ref, but it
cannot be used in constructs like cuddRef(a = b()).
- Side Effects none
- See Also
Cudd_Ref
- Defined in
cuddInt.h
(
)
- Iterates over the cubes of a decision diagram f.
- DdManager *manager;
- DdNode *f;
- DdGen *gen;
- int *cube;
- CUDD_VALUE_TYPE value;
Cudd_ForeachCube allocates and frees the generator. Therefore the
application should not try to do that. Also, the cube is freed at the
end of Cudd_ForeachCube and hence is not available outside of the loop.
CAUTION: It is assumed that dynamic reordering will not occur while
there are open generators. It is the user's responsibility to make sure
that dynamic reordering does not occur. As long as new nodes are not created
during generation, and dynamic reordering is not called explicitly,
dynamic reordering will not occur. Alternatively, it is sufficient to
disable dynamic reordering. It is a mistake to dispose of a diagram
on which generation is ongoing.
- Side Effects none
- See Also
Cudd_ForeachNode
Cudd_FirstCube
Cudd_NextCube
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_AutodynDisable
- Defined in
cudd.h
(
)
- Iterates over the nodes of a decision diagram f.
- DdManager *manager;
- DdNode *f;
- DdGen *gen;
- DdNode *node;
The nodes are returned in a seemingly random order.
Cudd_ForeachNode allocates and frees the generator. Therefore the
application should not try to do that.
CAUTION: It is assumed that dynamic reordering will not occur while
there are open generators. It is the user's responsibility to make sure
that dynamic reordering does not occur. As long as new nodes are not created
during generation, and dynamic reordering is not called explicitly,
dynamic reordering will not occur. Alternatively, it is sufficient to
disable dynamic reordering. It is a mistake to dispose of a diagram
on which generation is ongoing.
- Side Effects none
- See Also
Cudd_ForeachCube
Cudd_FirstNode
Cudd_NextNode
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_AutodynDisable
- Defined in
cudd.h
(
)
- Iterates over the paths of a ZDD f.
- DdManager *manager;
- DdNode *f;
- DdGen *gen;
- int *path;
Cudd_zddForeachPath allocates and frees the generator. Therefore the
application should not try to do that. Also, the path is freed at the
end of Cudd_zddForeachPath and hence is not available outside of the loop.
CAUTION: It is assumed that dynamic reordering will not occur while
there are open generators. It is the user's responsibility to make sure
that dynamic reordering does not occur. As long as new nodes are not created
during generation, and dynamic reordering is not called explicitly,
dynamic reordering will not occur. Alternatively, it is sufficient to
disable dynamic reordering. It is a mistake to dispose of a diagram
on which generation is ongoing.
- Side Effects none
- See Also
Cudd_zddFirstPath
Cudd_zddNextPath
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_AutodynDisable
- Defined in
cudd.h
(
)
- Iterates over the primes of a Boolean function producing
a prime and irredundant cover.
- DdManager *manager;
- DdNode *l;
- DdNode *u;
- DdGen *gen;
- int *cube;
The Boolean function is described by an upper bound and a lower bound. If
the function is completely specified, the two bounds coincide.
Cudd_ForeachPrime allocates and frees the generator. Therefore the
application should not try to do that. Also, the cube is freed at the
end of Cudd_ForeachPrime and hence is not available outside of the loop.
CAUTION: It is a mistake to change a diagram on which generation is ongoing.
- Side Effects none
- See Also
Cudd_ForeachCube
Cudd_FirstPrime
Cudd_NextPrime
Cudd_GenFree
Cudd_IsGenEmpty
- Defined in
cudd.h
(
)
- Outputs a line of stats if DD_COUNT and DD_STATS are
defined. Increments the number of recursive calls if DD_COUNT is
defined.
- Side Effects None
- Defined in
cuddInt.h
(
)
- Returns 1 if a pointer is complemented.
- Side Effects none
- See Also
Cudd_Regular
Cudd_Complement
- Defined in
cudd.h
(
)
- Returns 1 if the absolute value of the difference of the two
arguments x and y is less than e.
- Side Effects none
- Defined in
cuddInt.h
(
)
- Returns 1 if the node is a constant node (rather than an
internal node). All constant nodes have the same index
(CUDD_CONST_INDEX). The pointer passed to Cudd_IsConstant may be either
regular or complemented.
- Side Effects none
- Defined in
cudd.h
(
)
- Returns 1 if the node is a constant node (rather than an
internal node). All constant nodes have the same index
(CUDD_CONST_INDEX). The pointer passed to cuddIsConstant must be regular.
- Side Effects none
- See Also
Cudd_IsConstant
- Defined in
cuddInt.h
(
)
- Returns the arithmetic 0 constant node. This is different
from the logical zero. The latter is obtained by
Cudd_Not(DD_ONE(dd)).
- Side Effects none
- See Also
DD_ONE
Cudd_Not
DD_PLUS_INFINITY
DD_MINUS_INFINITY
- Defined in
cuddInt.h
(
)
- Returns the complemented version of a pointer.
- Side Effects none
- See Also
Cudd_Regular
Cudd_IsComplement
- Defined in
cudd.h
(
)
- Returns the constant 1 node.
- Side Effects none
- See Also
DD_ZERO
DD_PLUS_INFINITY
DD_MINUS_INFINITY
- Defined in
cuddInt.h
(
)
- Returns the current position in the order of variable
index. This macro is obsolete and is kept for compatibility. New
applications should use Cudd_ReadPerm instead.
- Side Effects none
- See Also
Cudd_ReadPerm
- Defined in
cudd.h
(
)
- Returns the else child of an internal node. If
node
is a constant node, the result is unpredictable.
The pointer passed to cuddE must be regular.
- Side Effects none
- See Also
Cudd_E
- Defined in
cuddInt.h
(
)
- Returns the else child of an internal node. If
node
is a constant node, the result is unpredictable.
- Side Effects none
- See Also
Cudd_T
Cudd_V
- Defined in
cudd.h
(
)
- Returns the minus infinity constant node.
- Side Effects none
- See Also
DD_ONE
DD_ZERO
DD_PLUS_INFINITY
- Defined in
cuddInt.h
(
)
- Returns the plus infinity constant node.
- Side Effects none
- See Also
DD_ONE
DD_ZERO
DD_MINUS_INFINITY
- Defined in
cuddInt.h
(
)
- Returns the regular version of a pointer.
- Side Effects none
- See Also
Cudd_Complement
Cudd_IsComplement
- Defined in
cudd.h
(
)
- Returns the then child of an internal node. If
node
is a constant node, the result is unpredictable.
The pointer passed to cuddT must be regular.
- Side Effects none
- See Also
Cudd_T
- Defined in
cuddInt.h
(
)
- Returns the then child of an internal node. If
node
is a constant node, the result is unpredictable.
- Side Effects none
- See Also
Cudd_E
Cudd_V
- Defined in
cudd.h
(
)
- Returns the value of a constant node. If
node
is an internal node, the result is unpredictable.
The pointer passed to cuddV must be regular.
- Side Effects none
- See Also
Cudd_V
- Defined in
cuddInt.h
(
)
- Returns the value of a constant node. If
node
is an internal node, the result is unpredictable.
- Side Effects none
- See Also
Cudd_T
Cudd_E
- Defined in
cudd.h
(
)
- Saturating decrement operator.
- Side Effects none
- See Also
cuddSatInc
- Defined in
cuddInt.h
(
)
- Saturating increment operator.
- Side Effects none
- See Also
cuddSatDec
- Defined in
cuddInt.h