-
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_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 IMPLY to the corresponding discriminants of f.
-
add_ifthenelse()
- Implements ITE(f,g,h).
-
add_implies()
- Applies IMPLY to the corresponding discriminants of f.
-
add_index()
- Returns the index of the node.
-
add_is_one()
- Check if the ADD is one.
-
add_is_zero()
- Check if the ADD is zero.
-
add_isleaf()
- Returns 1 if the 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 1 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_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 0 ADD of the manager.
-
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_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_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_imply()
- Applies IMPLY to the corresponding discriminants of f and g.
-
bdd_index()
- Returns the index of the node.
-
bdd_is_one()
- Check il the BDD is one.
-
bdd_is_zero()
- Check if the BDD is zero.
-
bdd_iscomplement()
- Returns 1 if the BDD pointer is complemented.
-
bdd_isnot_one()
- Check il the BDD is not one.
-
bdd_isnot_zero()
- Check if the BDD is not zero.
-
bdd_ite()
- Implements ITE(i,t,e).
-
bdd_largest_cube()
- Finds a largest cube in a BDD.
-
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_one()
- Reads the constant 1 BDD of the manager.
-
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()
- 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_then()
- Returns the then child of a bdd node.
-
bdd_to_add()
- Converts a BDD to a 0-1 ADD.
-
bdd_xor()
- Applies XOR to the corresponding discriminants of f and g.
-
bdd_zero()
- Reads the constant 0 BDD of the manager.
-
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 2009/03/04 12h:51