void
dd_autodyn_disable(
DdManager * dd
)
- Disables automatic dynamic reordering of BDD and ADD.
- See Also
dd_autodyn_enable
dd_reordering_status
void
dd_autodyn_enable(
DdManager * dd,
dd_reorderingtype method
)
- Enables automatic dynamic reordering of BDDs and
ADDs. Parameter method is used to determine the method used for
reordering. If REORDER_SAME is passed, the method is
unchanged.
- See Also
dd_autodyn_disable
dd_reordering_status
int
dd_checkzeroref(
DdManager * dd
)
- Checks the unique table for nodes with non-zero
reference counts. It is normally called before dd_quit to make sure
that there are no memory leaks due to missing add/bdd_free's.
Takes into account that reference counts may saturate and that the
basic constants and the projection functions are referenced by the
manager. Returns the number of nodes with non-zero reference count.
(Except for the cases mentioned above.)
int
dd_dump_davinci(
DdManager * dd, manager
int n, number of output nodes to be dumped
bdd_ptr * f, array of output nodes to be dumped
char ** inames, array of input names (or NULL)
char ** onames, array of output names (or NULL)
FILE * fp pointer to the dump file
)
- Writes a daVnci file representing the argument
DDs. For a better description see the "Cudd_DumpDaVinci" documentation
in the CUDD package.
- See Also
dd_dump_davinci
int
dd_dump_dot(
DdManager * dd, manager
int n, number of output nodes to be dumped
bdd_ptr * f, array of output nodes to be dumped
char ** inames, array of input names (or NULL)
char ** onames, array of output names (or NULL)
FILE * fp pointer to the dump file
)
- Writes a dot file representing the argument
DDs. For a better description see the "Cudd_DumpDot" documentation
in the CUDD package.
- See Also
dd_dump_davinci
int
dd_free_var_block(
DdManager* dd,
dd_block* group
)
- Dissolves a group previously created by
dd_new_var_block. Returns 0 if the group was actually removed, 1
otherwise (that may be not due to an error)
- Side Effects Modifies the variable tree.
int
dd_get_index_at_level(
DdManager * dd,
int level
)
- Returns the index of the variable currently in the i-th
position of the order. If the index is MAX_VAR_INDEX, returns
MAX_VAR_INDEX; otherwise, if the index is out of bounds fails.
int
dd_get_level_at_index(
DdManager * dd,
int index
)
- Returns the current position of the i-th variable in the
order. If the index is CUDD_MAXINDEX, returns CUDD_MAXINDEX; otherwise,
if the index is out of bounds returns -1.
- Side Effects None
- See Also
Cudd_ReadInvPerm
Cudd_ReadPermZdd
dd_reorderingtype
dd_get_ordering_method(
DdManager * dd
)
- Returns the internal reordering method used.
int
dd_get_reorderings(
DdManager* dd
)
- Returns the number of times reordering has occurred in
the manager. The number includes both the calls to Cudd_ReduceHeap
from the application program and those automatically performed by
the package. However, calls that do not even initiate reordering are
not counted. A call may not initiate reordering if there are fewer
than minsize live nodes in the manager, or if CUDD_REORDER_NONE is
specified as reordering method. The calls to Cudd_ShuffleHeap are
not counted.
int
dd_get_size(
DdManager * dd
)
- Returns the number of BDD variables in existance.
dd_block *
dd_new_var_block(
DdManager * dd,
int start_index,
int offset
)
- Builds a group of variables that should stay adjacent
during reordering. The group is made up of n variables. The first
variable in the group is f. The other variables are the n-1
variables following f in the order at the time of invocation of this
function. Returns a handle to the variable group if successful else fail.
- Side Effects Modifies the variable tree.
void
dd_print_stats(
DdManager * mgr,
FILE * file
)
- Prints out statistics and settings for a CUDD manager.
int
dd_printminterm(
DdManager * manager,
DdNode * node
)
- Prints a disjoint sum of product cover for the function
rooted at node. Each product corresponds to a path from node a leaf
node different from the logical zero, and different from the
background value. Uses the standard output. Returns 1 if successful;
0 otherwise.
int
dd_reordering_status(
DdManager * dd,
dd_reorderingtype * method
)
- Reports the status of automatic dynamic reordering of
BDDs and ADDs. Parameter method is set to the reordering method
currently selected. Returns 1 if automatic reordering is enabled; 0
otherwise.
- Side Effects Parameter method is set to the reordering method currently
selected.
- See Also
dd_autodyn_disable
dd_autodyn_enable
int
dd_reorder(
DdManager * dd,
int method,
int minsize
)
- Main dynamic reordering routine.
Calls one of the possible reordering procedures:
- Swapping
- Sifting
- Symmetric Sifting
- Group Sifting
- Window Permutation
- Simulated Annealing
- Genetic Algorithm
- Dynamic Programming (exact)
For sifting, symmetric sifting, group sifting, and window
permutation it is possible to request reordering to convergence.
Returns 1 in case of success; 0 otherwise. In the case of symmetric
sifting (with and without convergence) returns 1 plus the number of
symmetric variables, in case of success.
This functions takes as arguments:
- dd the DD manager;
- heuristics method used for reordering;
- minsize bound below which no reordering occurs;
- Side Effects Changes the variable order for all diagrams and clears
the cache.
- See Also
Cudd_ReduceHeap
int
dd_set_order(
DdManager* dd,
int* permutation
)
- Reorders variables according to given permutation.
The i-th entry of the permutation array contains the index of the variable
that should be brought to the i-th level. The size of the array should be
equal or greater to the number of variables currently in use.
Returns 1 in case of success; 0 otherwise.
- Side Effects Changes the variable order for all diagrams and clears
the cache.
int
dd_set_parameters(
DdManager * mgr,
OptsHandler_ptr opt,
FILE * file
)
- The CUDD package has a set of parameters that can be assigned
different values. This function receives a table which maps strings to
values and sets the parameters represented by the strings to the pertinent
values. Some basic type checking is done. It returns 1 if everything is
correct and 0 otherwise.