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