-
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_true()
- Reads the constant TRUE 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_false()
- Reads the constant FALSE ADD of the manager.
-
add_is_true()
- Check if the ADD is true.
-
add_is_false()
- Check if the ADD is false.
-
add_one()
- Reads the constant one ADD of the manager.
-
add_zero()
- Reads the constant zero 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 ADD node is a constant node.
-
bdd_isleaf()
- Returns 1 if the BDD 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 FALSE-TRUE ADD.
-
bdd_to_01_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 and g.
-
add_iff()
- Applies IFF to the corresponding discriminants of f and g.
-
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_true()
- Reads the constant TRUE BDD of the manager.
-
bdd_false()
- Reads the constant FALSE BDD of the manager.
-
bdd_is_true()
- Check if the BDD is TRUE.
-
bdd_isnot_true()
- Check if the BDD is not true.
-
bdd_is_false()
- Check if the BDD is false.
-
bdd_isnot_false()
- Check if the BDD is not false.
-
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_iff()
- Applies IFF 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_intersected()
- Determines whether an intersection between
f and g is not empty
-
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_prime_low()
- Finds a prime implicant for a BDD.
-
bdd_compute_primes_low()
- Finds a set of prime implicants for a BDD.
-
bdd_compute_primes()
- Finds a set of prime implicants for a BDD.
-
bdd_compute_essentials()
- Finds the essential variables of a DD.
-
bdd_leq()
- Determines whether f is less than or equal to g.
-
bdd_swap_variables()
- Swaps two sets of variables of the same size (x and y) in
the BDD f.
-
bdd_DumpBlif()
- Writes a blif file representing the argument BDDs.
-
bdd_DumpBlifBody()
- Writes a blif body representing the argument BDDs.
-
bdd_compose()
- Substitutes g for x_v in the BDD for f.
-
bdd_ref_count()
- Returns the reference count of a node.
-
calculate_bdd_value()
- Computes the value of a function with given variable values.
-
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 2011/04/06 21h:13