-
dd.h
- External header file
-
ddInt.h
- Internal header file
-
dd.c
- NuSMV interface to the Decision Diagram Package of the
University of Colorado.
-
ddCmd.c
- The shell interface of the DD package
dd.h
External header file
By: Marco Roveri
ddInt.h
Internal header file
By: Marco Roveri
dd.c
NuSMV interface to the Decision Diagram Package of the
University of Colorado.
By: Marco Roveri
This file implements the interface between the NuSMV
system and the California University Decision Diagram (henceforth
referred as CUDD). The CUDD package is a generic implementation of a
decision diagram data structure. For the time being, only Boole
expansion is implemented and the leaves in the in the nodes can be
the constants zero, one or any arbitrary value. A coding standard
has been defined. I.e all the functions acting on BDD and ADD have
"bdd" and "add" respectively as prefix.
The BDD or ADD returned as a result of an operation are always
referenced (see the CUDD User Manual for more details about this),
and need to be dereferenced when the result is no more necessary to
computation, in order to release the memory associated to it when
garbage collection occurs.
All the functions takes as first argument the decision diagram
manager (henceforth referred as DdManager).
-
init_dd_package()
- Creates a new DD manager.
-
quit_dd_package()
- Deletes resources associated with a DD manager.
-
dd_checkzeroref()
- Checks the unique table for nodes with non-zero reference
counts.
-
get_dd_nodes_allocated()
- Returns the number of nodes in the unique table.
-
map_dd()
- Applies function
f
to the list of BDD/ADD l
.
-
walk_dd()
- Applies function
f
to the list of BDD/ADD l
.
-
dd_print_stats()
- Prints out statistic and setting of the DD manager.
-
dd_new_var_block()
- Builds a group of variables that should stay adjacent
during reordering.
-
dd_free_var_block()
- Dissolves a group previously created by dd_new_var_block
-
dd_get_index_at_level()
- Returns the index of the variable currently in the i-th
position of the order.
-
dd_get_level_at_index()
- Returns the current position of the i-th variable in the
order.
-
dd_get_size()
- Returns the number of BDD variables in existance.
-
dd_set_order()
- Reorders variables according to given permutation.
-
dd_autodyn_enable()
- Enables automatic dynamic reordering of BDDs and ADDs.
-
dd_autodyn_disable()
- Disables automatic dynamic reordering of BDD and ADD.
-
dd_reordering_status()
- Reports the status of automatic dynamic reordering of BDDs
and ADDs.
-
dd_reorder()
- Main dynamic reordering routine.
-
dd_get_reorderings()
- Returns the number of times reordering has occurred.
-
dd_get_ordering_method()
- Gets the internal reordering method used.
-
StringConvertToDynOrderType()
- Converts a string to a dynamic ordering method type.
-
DynOrderTypeConvertToString()
- Converts a dynamic ordering method type to a string.
-
dd_set_parameters()
- Sets the internal parameters of the package to the given values.
-
dd_printminterm()
- Prints a disjoint sum of products.
-
dd_dump_dot()
- Writes a dot file representing the argument DDs.
-
dd_dump_davinci()
- Writes a daVnci file representing the argument DDs.
-
add_one()
- Reads the constant 1 ADD of the manager.
-
add_then()
- Returns the then child of an internal node.
-
add_index()
- Returns the index of the node.
-
add_else()
- Returns the else child of an internal node.
-
add_zero()
- Reads the constant 0 ADD of the manager.
-
add_is_one()
- Check if the ADD is one.
-
add_is_zero()
- Check if the ADD is zero.
-
add_ref()
- Reference an ADD node.
-
add_deref()
- Dereference an ADD node.
-
add_free()
- Dereference an ADD node. If it dies, recursively decreases
the reference count of its children.
-
add_dup()
- Creates a copy of an ADD node.
-
add_leaf()
- Creates an returns an ADD for constant leaf_node.
-
add_isleaf()
- Returns 1 if the node is a constant node.
-
add_get_leaf()
- Returns the value of a constant node.
-
add_build()
- Checks the unique table of the DdManager for the
existence of an internal node.
-
add_new_var_with_index()
- Returns the ADD variable with index
index
.
-
add_new_var_at_level()
- Returns a new ADD variable at a specified level.
-
add_to_bdd()
- Converts an ADD to a BDD.
-
add_to_bdd_strict_threshold()
- Converts an ADD to a BDD according to a strict threshold
-
bdd_to_add()
- Converts a BDD to a 0-1 ADD.
-
add_and()
- Applies AND to the corresponding discriminants of f and g.
-
add_or()
- Applies OR to the corresponding discriminants of f and g.
-
add_xor()
- Applies XOR to the corresponding discriminants of f and g.
-
add_xnor()
- Applies XNOR to the corresponding discriminants of f and g.
-
add_not()
- Applies NOT to the corresponding discriminant of f.
-
add_implies()
- Applies IMPLY to the corresponding discriminants of f.
-
add_iff()
- Applies IMPLY to the corresponding discriminants of f.
-
add_and_accumulate()
- Applies AND to the corresponding discriminants of f and g.
-
add_or_accumulate()
- Applies OR to the corresponding discriminants of f and g.
-
add_apply()
- Applies binary op to the corresponding discriminants of f and g.
-
add_monadic_apply()
- Applies unary op to the corresponding discriminant of f
-
add_exist_abstract()
- Abstracts away variables from an ADD.
-
add_ifthenelse()
- Implements ITE(f,g,h).
-
add_cube_diff()
- Computes the difference between two ADD cubes.
-
add_permute()
- Permutes the variables of an ADD.
-
add_support()
- Finds the variables on which an ADD depends on.
-
add_simplify_assuming()
- ADD restrict according to Coudert and Madre's algorithm (ICCAD90).
-
add_size()
- Counts the number of ADD nodes in an ADD.
-
add_count_minterm()
- Counts the number of ADD minterms of an ADD.
-
add_value()
- Given the result of add_if_then it returns the leaf corresponding.
-
add_if_then()
- Given a minterm, it returns an ADD indicating the rules
to traverse the ADD.
-
add_walkleaves()
- Applies a generic function to constant nodes.
-
bdd_one()
- Reads the constant 1 BDD of the manager.
-
bdd_zero()
- Reads the constant 0 BDD of the manager.
-
bdd_is_one()
- Check il the BDD is one.
-
bdd_isnot_one()
- Check il the BDD is not one.
-
bdd_is_zero()
- Check if the BDD is zero.
-
bdd_isnot_zero()
- Check if the BDD is not zero.
-
bdd_ref()
- Reference an BDD node.
-
bdd_deref()
- Dereference an BDD node.
-
bdd_free()
- Dereference an BDD node. If it dies, recursively decreases
the reference count of its children.
-
bdd_dup()
- Creates a copy of an BDD node.
-
bdd_not()
- Applies NOT to the corresponding discriminant of f.
-
bdd_and()
- Applies AND to the corresponding discriminants of f and g.
-
bdd_or()
- Applies OR to the corresponding discriminants of f and g.
-
bdd_xor()
- Applies XOR to the corresponding discriminants of f and g.
-
bdd_imply()
- Applies IMPLY to the corresponding discriminants of f and g.
-
bdd_and_accumulate()
- Applies AND to the corresponding discriminants of f and g.
-
bdd_or_accumulate()
- Applies OR to the corresponding discriminants of f and g.
-
bdd_forsome()
- Existentially abstracts all the variables in cube from fn.
-
bdd_forall()
- Universally abstracts all the variables in cube from f.
-
bdd_permute()
- Permutes the variables of a BDD.
-
bdd_and_abstract()
- Takes the AND of two BDDs and simultaneously abstracts the
variables in cube.
-
bdd_simplify_assuming()
- BDD restrict according to Coudert and Madre's algorithm
(ICCAD90).
-
bdd_minimize()
- Restrict operator as described in Coudert et al. ICCAD90.
-
bdd_cofactor()
- Computes f constrain c.
-
bdd_between()
- Return a minimum size BDD between bounds.
-
bdd_entailed()
- Determines whether f is less than or equal to g.
-
bdd_then()
- Returns the then child of a bdd node.
-
bdd_else()
- Returns the else child of a bdd node.
-
bdd_iscomplement()
- Returns 1 if the BDD pointer is complemented.
-
bdd_readperm()
- Finds the current position of variable index in the
order.
-
bdd_index()
- Returns the index of the node.
-
bdd_ite()
- Implements ITE(i,t,e).
-
bdd_size()
- Counts the number of BDD nodes in an BDD.
-
bdd_count_minterm()
- Counts the number of BDD minterms of an BDD.
-
bdd_support()
- Finds the variables on which an BDD depends on.
-
bdd_pick_one_minterm()
- Picks one on-set minterm deterministically from the given BDD.
-
bdd_pick_one_minterm_rand()
- Picks one on-set minterm randomly from the given DD.
-
bdd_pick_all_terms()
- Returns the array of All Possible Minterms
-
bdd_new_var_with_index()
- Returns the BDD variable with index
index
.
-
bdd_cube_diff()
- Computes the difference between two BDD cubes.
-
bdd_cube_union()
- Computes the union between two BDD cubes.
-
bdd_cube_intersection()
- Computes the intersection between two BDD cubes.
-
bdd_get_lowest_index()
- Returns the index of the lowest variable in the BDD a.
-
bdd_get_one_sparse_sat()
- Finds a satisfying path in the BDD d.
-
bdd_make_prime()
- Expands cube to a prime implicant of f.
-
bdd_largest_cube()
- Finds a largest cube in a BDD.
-
bdd_compute_primes()
- Finds a set of prime implicants for a BDD.
-
InvalidType()
- Function to print a warning that an illegal value was read.
ddCmd.c
The shell interface of the DD package
By: Marco Roveri
Shell interface of the DD package. here are provided
the shell commands to modyfy all the modifiable DD options.
-
CommandDynamicVarOrdering()
- Implements the dynamic_var_ordering command.
-
CommandSetBddParameters()
- Implements the set_bdd_parameters command.
-
CommandPrintBddStats()
- Implements the print_bdd_stats command.
Last updated on 2009/03/04 12h:51