CommandDynamicVarOrdering()
Implements the dynamic_var_ordering command.
CommandPrintBddStats()
Implements the print_bdd_stats command.
CommandSetBddParameters()
Implements the set_bdd_parameters command.
DynOrderTypeConvertToString()
Converts a dynamic ordering method type to a string.
InvalidType()
Function to print a warning that an illegal value was read.
StringConvertToDynOrderType()
Converts a string to a dynamic ordering method type.
add_and_accumulate()
Applies AND to the corresponding discriminants of f and g.
add_and()
Applies AND to the corresponding discriminants of f and g.
add_apply()
Applies binary op to the corresponding discriminants of f and g.
add_build()
Checks the unique table of the DdManager for the existence of an internal node.
add_count_minterm()
Counts the number of ADD minterms of an ADD.
add_cube_diff()
Computes the difference between two ADD cubes.
add_deref()
Dereference an ADD node.
add_dup()
Creates a copy of an ADD node.
add_else()
Returns the else child of an internal node.
add_exist_abstract()
Abstracts away variables from an ADD.
add_false()
Reads the constant FALSE ADD of the manager.
add_free()
Dereference an ADD node. If it dies, recursively decreases the reference count of its children.
add_get_leaf()
Returns the value of a constant node.
add_if_then()
Given a minterm, it returns an ADD indicating the rules to traverse the ADD.
add_iff()
Applies IFF to the corresponding discriminants of f and g.
add_ifthenelse()
Implements ITE(f,g,h).
add_implies()
Applies IMPLY to the corresponding discriminants of f and g.
add_index()
Returns the index of the node.
add_is_false()
Check if the ADD is false.
add_is_one()
Check if the ADD is one.
add_is_true()
Check if the ADD is true.
add_is_zero()
Check if the ADD is zero.
add_isleaf()
Returns 1 if the ADD node is a constant node.
add_leaf()
Creates an returns an ADD for constant leaf_node.
add_monadic_apply()
Applies unary op to the corresponding discriminant of f
add_new_var_at_level()
Returns a new ADD variable at a specified level.
add_new_var_with_index()
Returns the ADD variable with index index.
add_not()
Applies NOT to the corresponding discriminant of f.
add_one()
Reads the constant one ADD of the manager.
add_or_accumulate()
Applies OR to the corresponding discriminants of f and g.
add_or()
Applies OR to the corresponding discriminants of f and g.
add_permute()
Permutes the variables of an ADD.
add_ref()
Reference an ADD node.
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_support()
Finds the variables on which an ADD depends on.
add_then()
Returns the then child of an internal node.
add_to_bdd_strict_threshold()
Converts an ADD to a BDD according to a strict threshold
add_to_bdd()
Converts an ADD to a BDD.
add_true()
Reads the constant TRUE ADD of the manager.
add_value()
Given the result of add_if_then it returns the leaf corresponding.
add_walkleaves()
Applies a generic function to constant nodes.
add_xnor()
Applies XNOR to the corresponding discriminants of f and g.
add_xor()
Applies XOR to the corresponding discriminants of f and g.
add_zero()
Reads the constant zero ADD of the manager.
bdd_DumpBlifBody()
Writes a blif body representing the argument BDDs.
bdd_DumpBlif()
Writes a blif file representing the argument BDDs.
bdd_and_abstract()
Takes the AND of two BDDs and simultaneously abstracts the variables in cube.
bdd_and_accumulate()
Applies AND to the corresponding discriminants of f and g.
bdd_and()
Applies AND to the corresponding discriminants of f and g.
bdd_between()
Return a minimum size BDD between bounds.
bdd_cofactor()
Computes f constrain c.
bdd_compose()
Substitutes g for x_v in the BDD for f.
bdd_compute_essentials()
Finds the essential variables of a DD.
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_count_minterm()
Counts the number of BDD minterms of an BDD.
bdd_cube_diff()
Computes the difference between two BDD cubes.
bdd_cube_intersection()
Computes the intersection between two BDD cubes.
bdd_cube_union()
Computes the union between two BDD cubes.
bdd_deref()
Dereference an BDD node.
bdd_dup()
Creates a copy of an BDD node.
bdd_else()
Returns the else child of a bdd node.
bdd_entailed()
Determines whether f is less than or equal to g.
bdd_false()
Reads the constant FALSE BDD of the manager.
bdd_forall()
Universally abstracts all the variables in cube from f.
bdd_forsome()
Existentially abstracts all the variables in cube from fn.
bdd_free()
Dereference an BDD node. If it dies, recursively decreases the reference count of its children.
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_iff()
Applies IFF to the corresponding discriminants of f and g.
bdd_imply()
Applies IMPLY to the corresponding discriminants of f and g.
bdd_index()
Returns the index of the node.
bdd_intersected()
Determines whether an intersection between f and g is not empty
bdd_is_false()
Check if the BDD is false.
bdd_is_true()
Check if the BDD is TRUE.
bdd_iscomplement()
Returns 1 if the BDD pointer is complemented.
bdd_isleaf()
Returns 1 if the BDD node is a constant node.
bdd_isnot_false()
Check if the BDD is not false.
bdd_isnot_true()
Check if the BDD is not true.
bdd_ite()
Implements ITE(i,t,e).
bdd_largest_cube()
Finds a largest cube in a BDD.
bdd_leq()
Determines whether f is less than or equal to g.
bdd_make_prime()
Expands cube to a prime implicant of f.
bdd_minimize()
Restrict operator as described in Coudert et al. ICCAD90.
bdd_new_var_with_index()
Returns the BDD variable with index index.
bdd_not()
Applies NOT to the corresponding discriminant of f.
bdd_or_accumulate()
Applies OR to the corresponding discriminants of f and g.
bdd_or()
Applies OR to the corresponding discriminants of f and g.
bdd_permute()
Permutes the variables of a BDD.
bdd_pick_all_terms()
Returns the array of All Possible Minterms
bdd_pick_one_minterm_rand()
Picks one on-set minterm randomly from the given DD.
bdd_pick_one_minterm()
Picks one on-set minterm deterministically from the given BDD.
bdd_readperm()
Finds the current position of variable index in the order.
bdd_ref_count()
Returns the reference count of a node.
bdd_ref()
Reference an BDD node.
bdd_simplify_assuming()
BDD restrict according to Coudert and Madre's algorithm (ICCAD90).
bdd_size()
Counts the number of BDD nodes in an BDD.
bdd_support()
Finds the variables on which an BDD depends on.
bdd_swap_variables()
Swaps two sets of variables of the same size (x and y) in the BDD f.
bdd_then()
Returns the then child of a bdd node.
bdd_to_01_add()
Converts a BDD to a 0-1 ADD.
bdd_to_add()
Converts a BDD to a FALSE-TRUE ADD.
bdd_true()
Reads the constant TRUE BDD of the manager.
bdd_xor()
Applies XOR to the corresponding discriminants of f and g.
calculate_bdd_value()
Computes the value of a function with given variable values.
dd_autodyn_disable()
Disables automatic dynamic reordering of BDD and ADD.
dd_autodyn_enable()
Enables automatic dynamic reordering of BDDs and ADDs.
dd_checkzeroref()
Checks the unique table for nodes with non-zero reference counts.
dd_dump_davinci()
Writes a daVnci file representing the argument DDs.
dd_dump_dot()
Writes a dot file representing the argument DDs.
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_ordering_method()
Gets the internal reordering method used.
dd_get_reorderings()
Returns the number of times reordering has occurred.
dd_get_size()
Returns the number of BDD variables in existance.
dd_new_var_block()
Builds a group of variables that should stay adjacent during reordering.
dd_print_stats()
Prints out statistic and setting of the DD manager.
dd_printminterm()
Prints a disjoint sum of products.
dd_reordering_status()
Reports the status of automatic dynamic reordering of BDDs and ADDs.
dd_reorder()
Main dynamic reordering routine.
dd_set_order()
Reorders variables according to given permutation.
dd_set_parameters()
Sets the internal parameters of the package to the given values.
get_dd_nodes_allocated()
Returns the number of nodes in the unique table.
init_dd_package()
Creates a new DD manager.
map_dd()
Applies function f to the list of BDD/ADD l.
quit_dd_package()
Deletes resources associated with a DD manager.
walk_dd()
Applies function f to the list of BDD/ADD l.

Last updated on 2011/04/06 21h:13