int 
CommandDynamicVarOrdering(
  int  argc, 
  char ** argv 
)
Implements the dynamic_var_ordering command.

Defined in ddCmd.c

int 
CommandPrintBddStats(
  int  argc, 
  char ** argv 
)
Implements the print_bdd_stats command.

Defined in ddCmd.c

int 
CommandSetBddParameters(
  int  argc, 
  char ** argv 
)
Implements the set_bdd_parameters command.

Defined in ddCmd.c

char * 
DynOrderTypeConvertToString(
  int  method 
)
Converts a dynamic ordering method type to a string. This string must NOT be freed by the caller.

Defined in dd.c

static void 
InvalidType(
  FILE * file, 
  char * field, 
  char * expected 
)
Function to print a warning that an illegal value was read.

See Also bdd_set_parameters
Defined in dd.c

int 
StringConvertToDynOrderType(
  char * string 
)
Converts a string to a dynamic ordering method type. If string is not "sift" or "window", then returns REORDER_.

Defined in dd.c

void 
add_and_accumulate(
  DdManager * dd, 
  add_ptr * a, 
  add_ptr  b 
)
Applies logical AND to the corresponding discriminants of f and g and stores the result in f. f and g must have only FALSE or TRUE as terminal nodes.

Side Effects The result is stored in the first operand.

See Also add_and
Defined in dd.c

add_ptr 
add_and(
  DdManager * dd, 
  add_ptr  a, 
  add_ptr  b 
)
Applies logical AND to the corresponding discriminants of f and g. f and g must have only FALSE or TRUE as terminal nodes. Returns a pointer to the result if successful; a failure is generated otherwise.

See Also add_or add_xor add_not
Defined in dd.c

add_ptr 
add_apply(
  DdManager * dd, 
  NPFNN  op, 
  add_ptr  f, 
  add_ptr  g 
)
Returns a pointer to the result if successful; a failure is generated otherwise.

Defined in dd.c

add_ptr 
add_build(
  DdManager * dd, 
  int  level, 
  add_ptr  t, 
  add_ptr  e 
)
Checks the unique table for the existence of an internal node. If it does not exist, it creates a new one. The reference count of whatever is returned is increased by one unit. For a newly created node, increments the reference counts of what T and E point to. Returns a pointer to the new node if successful; a failure occurs if memory is exhausted or if reordering took place.

Defined in dd.c

double 
add_count_minterm(
  DdManager * dd, 
  add_ptr  fn, 
  int  nvars 
)
Counts the number of minterms of an ADD. The function is assumed to depend on nvars variables. The minterm count is represented as a double, to allow for a larger number of variables. Returns the number of minterms of the function rooted at node. The result is parameterized by the number of "nvars" passed as argument.

See Also bdd_size bdd_count_minterm
Defined in dd.c

add_ptr 
add_cube_diff(
  DdManager * dd, 
  add_ptr  a, 
  add_ptr  b 
)
Computes the difference between two ADD cubes, i.e. the cube of ADD variables belonging to cube a and not belonging to cube b. Returns a pointer to the resulting cube; a failure is generated otherwise.

See Also bdd_cube_diff
Defined in dd.c

void 
add_deref(
  add_ptr  fn 
)
Dereference an ADD node.

Side Effects The reference count of the node is decremented by one.

See Also add_ref add_free
Defined in dd.c

add_ptr 
add_dup(
  add_ptr  dd_node 
)
Creates a copy of an ADD node.

Side Effects The reference count is increased by one unit.

See Also add_ref add_free add_deref
Defined in dd.c

add_ptr 
add_else(
  DdManager * dd, 
  add_ptr  f 
)
Returns the else child of an internal node. If f is a constant node, the result is unpredictable. Notice that the reference count of the returned node is not incremented.

Side Effects none

See Also add_else
Defined in dd.c

add_ptr 
add_exist_abstract(
  DdManager* dd, 
  add_ptr  a, 
  bdd_ptr  b 
)
Abstracts away variables from an ADD, summing up the values of the merged branches.

Defined in dd.c

add_ptr 
add_false(
  DdManager * dd 
)
Reads the constant FALSE ADD of the manager.

See Also add_true
Defined in dd.c

void 
add_free(
  DdManager * dd, 
  add_ptr  dd_node 
)
Decreases the reference count of node. If the node dies, recursively decreases the reference counts of its children. It is used to dispose off an ADD that is no longer needed.

Side Effects The reference count of the node is decremented by one, and if the node dies a recursive dereferencing is applied to its children.

Defined in dd.c

node_ptr 
add_get_leaf(
  DdManager * dd, 
  add_ptr  Leaf 
)
Returns the value of a constant node. If Leaf is an internal node, a failure occurs.

Defined in dd.c

add_ptr 
add_if_then(
  DdManager * dd, 
  add_ptr  I, 
  add_ptr  T 
)
Given a minterm, it returns an ADD indicating the rules to traverse the ADD.

See Also add_value
Defined in dd.c

add_ptr 
add_iff(
  DdManager * dd, 
  add_ptr  a, 
  add_ptr  b 
)
Applies logical IFF to the corresponding discriminants of f and g. f and g must have only FALSE or TRUE as terminal nodes. Returns a pointer to the result if successful; a failure is generated otherwise.

See Also add_and add_xor add_or add_not
Defined in dd.c

add_ptr 
add_ifthenelse(
  DdManager * dd, 
  add_ptr  If, 
  add_ptr  Then, 
  add_ptr  Else 
)
Implements ITE(f,g,h). This procedure assumes that f is a FALSE-TRUE ADD. Returns a pointer to the resulting ADD if successful; a failure is generated otherwise.

Defined in dd.c

add_ptr 
add_implies(
  DdManager * dd, 
  add_ptr  a, 
  add_ptr  b 
)
Applies logical IMPLY to the corresponding discriminants of f and g. f and g must have only FALSE or TRUE as terminal nodes. Returns a pointer to the result if successful; a failure is generated otherwise.

See Also add_and add_xor add_or add_not
Defined in dd.c

int 
add_index(
  DdManager * dd, 
  add_ptr  f 
)
Returns the index of the node.

Side Effects None

Defined in dd.c

int 
add_is_false(
  DdManager * dd, 
  add_ptr  f 
)
Check if the ADD is false.

See Also add_false
Defined in dd.c

int 
add_is_one(
  DdManager * dd, 
  add_ptr  f 
)
Check if the ADD is one.

See Also add_true
Defined in dd.c

int 
add_is_true(
  DdManager * dd, 
  add_ptr  f 
)
Check if the ADD is true.

See Also add_true
Defined in dd.c

int 
add_is_zero(
  DdManager * dd, 
  add_ptr  f 
)
Check if the ADD is zero.

See Also add_false
Defined in dd.c

int 
add_isleaf(
  add_ptr  dd_node 
)
Returns 1 if the ADD node is a constant node (rather than an internal node). All constant nodes have the same index (MAX_VAR_INDEX).

Defined in dd.c

add_ptr 
add_leaf(
  DdManager * dd, 
  node_ptr  leaf_node 
)
Retrieves the ADD for constant leaf_node if it already exists, or creates a new ADD. Returns a pointer to the ADD if successful; fails otherwise.

Side Effects The reference count of the node is incremented by one unit.

Defined in dd.c

add_ptr 
add_monadic_apply(
  DdManager * dd, 
   , 
  add_ptr  f 
)
Returns a pointer to the result if successful; a failure is generated otherwise. NOTE: At the moment CUDD does not have unary 'apply', so you have to provide a binary op, which is actually unary and applies to the first operand only.

Defined in dd.c

add_ptr 
add_new_var_at_level(
  DdManager * dd, 
  int  level 
)
Creates a new ADD variable. The new variable has an index equal to the largest previous index plus 1 and is positioned at the specified level in the order. Returns a pointer to the new variable if successful; a failure is generated otherwise. The returned value is referenced.

See Also add_new_var_with_index
Defined in dd.c

add_ptr 
add_new_var_with_index(
  DdManager * dd, 
  int  index 
)
Retrieves the ADD variable with index index if it already exists, or creates a new ADD variable. Returns a pointer to the variable if successful; a failure is generated otherwise. An ADD variable differs from a BDD variable because it points to the arithmetic zero, instead of having a complement pointer to 1. The returned value is referenced.

See Also add_new_var_at_level
Defined in dd.c

add_ptr 
add_not(
  DdManager * dd, 
  add_ptr  a 
)
Applies logical NOT to the corresponding discriminant of f. f must have only FALSE or TRUE as terminal nodes. Returns a pointer to the result if successful; a failure is generated otherwise.

See Also add_and add_xor add_or add_imply
Defined in dd.c

add_ptr 
add_one(
  DdManager * dd 
)
Reads the constant one ADD of the manager.

See Also add_false
Defined in dd.c

void 
add_or_accumulate(
  DdManager * dd, 
  add_ptr * a, 
  add_ptr  b 
)
Applies logical OR to the corresponding discriminants of f and g and stores the result in f. f and g must have only FALSE or TRUE as terminal nodes.

Side Effects The result is stored in the first operand.

See Also add_and
Defined in dd.c

add_ptr 
add_or(
  DdManager * dd, 
  add_ptr  a, 
  add_ptr  b 
)
Applies logical OR to the corresponding discriminants of f and g. f and g must have only FALSE or TRUE as terminal nodes. Returns a pointer to the result if successful; a failure is generated otherwise.

See Also add_and add_xor add_not add_imply
Defined in dd.c

add_ptr 
add_permute(
  DdManager * dd, 
  add_ptr  fn, 
  int * permut 
)
Given a permutation in array permut, creates a new ADD with permuted variables. There should be an entry in array permut for each variable in the manager. The i-th entry of permut holds the index of the variable that is to substitute the i-th variable. Returns a pointer to the resulting ADD if successful; a failure is generated otherwise. The reuslt is referenced.

See Also bdd_permute
Defined in dd.c

void 
add_ref(
  add_ptr  fn 
)
Reference an ADD node.

Side Effects The reference count of the node is incremented by one.

See Also add_deref add_free
Defined in dd.c

add_ptr 
add_simplify_assuming(
  DdManager * dd, 
  add_ptr  a, 
  add_ptr  b 
)
ADD restrict according to Coudert and Madre's algorithm (ICCAD90). Returns the restricted ADD if successful; a failure is generated otherwise. If application of restrict results in an ADD larger than the input ADD, the input ADD is returned.

Defined in dd.c

int 
add_size(
  DdManager * dd, 
  add_ptr  fn 
)
Counts the number of ADD nodes in an ADD. Returns the number of nodes in the graph rooted at node.

See Also add_count_minterm
Defined in dd.c

add_ptr 
add_support(
  DdManager * dd, 
  add_ptr  fn 
)
Finds the variables on which an ADD depends on. Returns an ADD consisting of the product of the variables if successful; a failure is generated otherwise.

See Also bdd_support
Defined in dd.c

add_ptr 
add_then(
  DdManager * dd, 
  add_ptr  f 
)
Returns the then child of an internal node. If f is a constant node, the result is unpredictable. Notice that the reference count of the returned node is not incremented.

Side Effects none

See Also add_else
Defined in dd.c

bdd_ptr 
add_to_bdd_strict_threshold(
  DdManager * dd, 
  add_ptr  fn, 
  int  k 
)
Converts an ADD to a BDD by replacing all discriminants greater than value k with TRUE, and all other discriminants with FALSE. Returns a pointer to the resulting BDD if successful; a failure is generated otherwise.

See Also add_to_bdd_threshold add_to_bdd bdd_to_01_add
Defined in dd.c

bdd_ptr 
add_to_bdd(
  DdManager * dd, 
  add_ptr  fn 
)
Converts an ADD to a BDD. Only TRUE and FALSE leaves are admitted. Returns a pointer to the resulting BDD if successful; NULL otherwise.

See Also bdd_to_add bdd_to_01_add
Defined in dd.c

add_ptr 
add_true(
  DdManager * dd 
)
Reads the constant TRUE ADD of the manager.

See Also add_false
Defined in dd.c

node_ptr 
add_value(
  DdManager * dd, 
  add_ptr  fn 
)
Given the result of add_if_then it returns the leaf corresponding. The ADD is traversed according to the rules given as a result of add_if_then. If it is costant, then the corresponding value is returned. The Else branch is recursively traversed, if the result of this travesring is an ELSE_CNST, then the result of the traversing of the Then branch is returned.

See Also add_if_then
Defined in dd.c

void 
add_walkleaves(
  VPFCVT  op, 
  add_ptr  f 
)
Applies a generic function VPFCVT op to the constants nodes of f.

Defined in dd.c

add_ptr 
add_xnor(
  DdManager * dd, 
  add_ptr  a, 
  add_ptr  b 
)
Applies logical XNOR to the corresponding discriminants of f and g. f and g must have only FALSE or TRUE as terminal nodes. Returns a pointer to the result if successful; a failure is generated otherwise.

See Also add_xor add_or add_and add_not add_imply
Defined in dd.c

add_ptr 
add_xor(
  DdManager * dd, 
  add_ptr  a, 
  add_ptr  b 
)
Applies logical XOR to the corresponding discriminants of f and g. f and g must have only FALSE or TRUE as terminal nodes. Returns a pointer to the result if successful; a failure is generated otherwise.

See Also add_or add_and add_not add_imply
Defined in dd.c

add_ptr 
add_zero(
  DdManager * dd 
)
Reads the constant zero ADD of the manager.

See Also add_true
Defined in dd.c

int 
bdd_DumpBlifBody(
  DdManager* dd, manager
  int  n, number of output nodes to be dumped
  bdd_ptr* f, array of output nodes to be dumped
  char** inames, array of input names (or NULL)
  char** onames, array of output names (or NULL)
  FILE* fp pointer to the dump file
)
Writes a blif body representing the argument BDDs as a network of multiplexers. No header (.model, .inputs, and .outputs) and footer (.end) are produced by this function. One multiplexer is written for each BDD node. It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file system full, or an ADD with constants different from 0 and 1). bdd_DumpBlifBody does not close the file: This is the caller responsibility. bdd_DumpBlifBody uses a minimal unique subset of the hexadecimal address of a node as name for it. If the argument inames is non-null, it is assumed to hold the pointers to the names of the inputs. Similarly for onames. This function prints out only .names part.

Side Effects None

See Also bdd_DumpBlif dd_dump_dot
Defined in dd.c

int 
bdd_DumpBlif(
  DdManager* dd, manager
  int  n, number of output nodes to be dumped
  bdd_ptr* f, array of output nodes to be dumped
  char** inames, array of input names (or NULL)
  char** onames, array of output names (or NULL)
  char* mname, model name (or NULL)
  FILE* fp pointer to the dump file
)
Writes a blif file representing the argument BDDs as a network of multiplexers. One multiplexer is written for each BDD node. It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file system full, or an ADD with constants different from 0 and 1). bdd_DumpBlif does not close the file: This is the caller responsibility. bdd_DumpBlif uses a minimal unique subset of the hexadecimal address of a node as name for it. If the argument inames is non-null, it is assumed to hold the pointers to the names of the inputs. Similarly for onames.

Side Effects None

See Also bdd_DumpBlifBody dd_dump_dot
Defined in dd.c

bdd_ptr 
bdd_and_abstract(
  DdManager * dd, 
  bdd_ptr  T, 
  bdd_ptr  S, 
  bdd_ptr  V 
)
Takes the AND of two BDDs and simultaneously abstracts the variables in cube. The variables are existentially abstracted. Returns a pointer to the result if successful; a failure is generated otherwise.

See Also bdd_and bdd_forsome
Defined in dd.c

void 
bdd_and_accumulate(
  DdManager * dd, 
  bdd_ptr * a, 
  bdd_ptr  b 
)
Applies logical AND to the corresponding discriminants of f and g and stores the result in f. f and g must be two BDDs. The result is referenced.

Side Effects The result is stored in the first operand and referenced.

See Also bdd_and
Defined in dd.c

bdd_ptr 
bdd_and(
  DdManager * dd, 
  bdd_ptr  a, 
  bdd_ptr  b 
)
Applies logical AND to the corresponding discriminants of f and g. f and g must be BDDs. Returns a pointer to the result if successful; a failure is generated otherwise.

See Also bdd_or bdd_xor bdd_not
Defined in dd.c

bdd_ptr 
bdd_between(
  DdManager * dd, 
  bdd_ptr  f_min, 
  bdd_ptr  f_max 
)
Return a minimum size BDD between bounds.

See Also bdd_minimize bdd_simplify_assuming bdd_cofactor
Defined in dd.c

bdd_ptr 
bdd_cofactor(
  DdManager * dd, 
  bdd_ptr  f, 
  bdd_ptr  g 
)
Computes f constrain c (f @ c). Uses a canonical form: (f' @ c) = ( f @ c)'. (Note: this is not true for c.) List of special cases: Returns a pointer to the result if successful; a failure is generated otherwise.

See Also bdd_minimize bdd_simplify_assuming
Defined in dd.c

bdd_ptr 
bdd_compose(
  DdManager * dd, 
  bdd_ptr  f, 
  bdd_ptr  g, 
  int  v 
)
Substitutes g for x_v in the BDD for f. v is the index of the variable to be substituted. bdd_compose passes the corresponding projection function to the recursive procedure, so that the cache may be used. Returns the composed BDD if successful; an error (which either results in a jump to the last CATCH-FAIL block, or in a call to exit()) is triggered otherwise.

Side Effects None

Defined in dd.c

bdd_ptr 
bdd_compute_essentials(
  DdManager * dd, 
  bdd_ptr  b 
)
Returns the cube of the essential variables. A positive literal means that the variable must be set to 1 for the function to be 1. A negative literal means that the variable must be set to 0 for the function to be 1. Returns a pointer to the cube BDD if successful; NULL otherwise.

Side Effects None

Defined in dd.c

bdd_ptr 
bdd_compute_prime_low(
  DdManager * dd, 
  bdd_ptr  b, 
  bdd_ptr  low 
)
Finds the prime implicant of a BDD b based on the largest cube in low where low implies b.

Side Effects None

Defined in dd.c

array_t * 
bdd_compute_primes_low(
  DdManager * dd, 
  bdd_ptr  b, 
  bdd_ptr  low 
)
Finds the set of prime implicants of a BDD b that are implied by low where low implies b.

Side Effects None

Defined in dd.c

array_t * 
bdd_compute_primes(
  DdManager * dd, 
  bdd_ptr  b 
)
Finds the set of prime implicants of a BDD b.

Side Effects None

Defined in dd.c

double 
bdd_count_minterm(
  DdManager * dd, 
  bdd_ptr  fn, 
  int  nvars 
)
Counts the number of minterms of an BDD. The function is assumed to depend on nvars variables. The minterm count is represented as a double, to allow for a larger number of variables. Returns the number of minterms of the function rooted at node. The result is parameterized by the number of "nvars" passed as argument.

See Also bdd_size bdd_count_minterm
Defined in dd.c

bdd_ptr 
bdd_cube_diff(
  DdManager * dd, 
  bdd_ptr  a, 
  bdd_ptr  b 
)
Computes the difference between two BDD cubes, i.e. the cube of BDD variables belonging to cube a and not belonging to cube b. Returns a pointer to the resulting cube; a failure is generated otherwise.

See Also add_cube_diff
Defined in dd.c

bdd_ptr 
bdd_cube_intersection(
  DdManager * dd, 
  bdd_ptr  a, 
  bdd_ptr  b 
)
Computes the difference between two BDD cubes, i.e. the cube of BDD variables belonging to cube a AND belonging to cube b. Returns a pointer to the resulting cube; a failure is generated otherwise.

See Also bdd_cube_union bdd_cube_diff
Defined in dd.c

bdd_ptr 
bdd_cube_union(
  DdManager * dd, 
  bdd_ptr  a, 
  bdd_ptr  b 
)
Computes the union between two BDD cubes, i.e. the cube of BDD variables belonging to cube a OR to cube b. Returns a pointer to the resulting cube; a failure is generated otherwise.

See Also bdd_cube_intersection bdd_and
Defined in dd.c

void 
bdd_deref(
  bdd_ptr  dd_node 
)
Dereference an BDD node.

Side Effects The reference count of the node is decremented by one.

See Also bdd_ref bdd_free
Defined in dd.c

bdd_ptr 
bdd_dup(
  bdd_ptr  dd_node 
)
Creates a copy of an BDD node.

Side Effects The reference count is increased by one unit.

See Also bdd_ref bdd_free bdd_deref
Defined in dd.c

bdd_ptr 
bdd_else(
  DdManager * dd, 
  bdd_ptr  f 
)
Returns the else child of a bdd node. The node must not be a leaf node. Notice that this funxction does not save the bdd. Is the responsibility of the user to save it if it is the case.

Side Effects None

Defined in dd.c

int 
bdd_entailed(
  DdManager * dd, 
  bdd_ptr  f, 
  bdd_ptr  g 
)
Returns 1 if f is less than or equal to g; 0 otherwise. No new nodes are created.

Side Effects None

Defined in dd.c

bdd_ptr 
bdd_false(
  DdManager * dd 
)
Reads the constant FALSE BDD of the manager.

See Also bdd_true
Defined in dd.c

bdd_ptr 
bdd_forall(
  DdManager * dd, 
  bdd_ptr  fn, 
  bdd_ptr  cube 
)
Universally abstracts all the variables in cube from f. Returns the abstracted BDD if successful; a failure is generated otherwise.

See Also bdd_forsome
Defined in dd.c

bdd_ptr 
bdd_forsome(
  DdManager * dd, 
  bdd_ptr  fn, 
  bdd_ptr  cube 
)
Existentially abstracts all the variables in cube from fn. Returns the abstracted BDD if successful; a failure is generated otherwise.

See Also bdd_forall
Defined in dd.c

void 
bdd_free(
  DdManager * dd, 
  bdd_ptr  dd_node 
)
Decreases the reference count of node. If the node dies, recursively decreases the reference counts of its children. It is used to dispose off a BDD that is no longer needed.

Side Effects The reference count of the node is decremented by one, and if the node dies a recursive dereferencing is applied to its children.

Defined in dd.c

int 
bdd_get_lowest_index(
  DdManager * dd, 
  bdd_ptr  a 
)
Returns the index of the lowest variable in the BDD, i.e. the variable in BDD a with the highest position in the ordering.

Defined in dd.c

bdd_ptr 
bdd_get_one_sparse_sat(
  DdManager * dd, 
  bdd_ptr  d 
)
Finds a satisfying path in the BDD d. This path should not include all variabales. It only need ot include the levels needed to satify the BDD.

Defined in dd.c

bdd_ptr 
bdd_iff(
  DdManager * dd, 
  bdd_ptr  a, 
  bdd_ptr  b 
)
Applies logical IFF to the corresponding discriminants of f and g. f and g must be BDDs. Returns a pointer to the result if successful; a failure is generated otherwise.

See Also bdd_or bdd_xor bdd_not
Defined in dd.c

bdd_ptr 
bdd_imply(
  DdManager * dd, 
  bdd_ptr  a, 
  bdd_ptr  b 
)
Applies logical IMPLY to the corresponding discriminants of f and g. f and g must be BDDs. Returns a pointer to the result if successful; a failure is generated otherwise.

See Also bdd_or bdd_xor bdd_not
Defined in dd.c

int 
bdd_index(
  DdManager * dd, 
  bdd_ptr  f 
)
Returns the index of the node.

Side Effects None

Defined in dd.c

int 
bdd_intersected(
  DdManager * dd, 
  bdd_ptr  f, 
  bdd_ptr  g 
)
Returns 1 if an intersection between f and g is not empty; 0 otherwise. No new nodes are created.

Side Effects None

Defined in dd.c

int 
bdd_is_false(
  DdManager * dd, 
  bdd_ptr  f 
)
Check if the BDD is false.

See Also bdd_false
Defined in dd.c

int 
bdd_is_true(
  DdManager * dd, 
  bdd_ptr  f 
)
Check if the BDD is TRUE.

See Also bdd_true
Defined in dd.c

int 
bdd_iscomplement(
  DdManager * dd, 
  bdd_ptr  f 
)
Returns 1 if the BDD pointer is complemented.

Side Effects None

Defined in dd.c

int 
bdd_isleaf(
  bdd_ptr  dd_node 
)
Returns 1 if the BDD node is a constant node (rather than an internal node). All constant nodes have the same index (MAX_VAR_INDEX).

Defined in dd.c

int 
bdd_isnot_false(
  DdManager * dd, 
  bdd_ptr  f 
)
Check if the BDD is not false.

See Also bdd_false
Defined in dd.c

int 
bdd_isnot_true(
  DdManager * dd, 
  bdd_ptr  f 
)
Check if the BDD is not true.

See Also bdd_true
Defined in dd.c

bdd_ptr 
bdd_ite(
  DdManager * dd, 
  bdd_ptr  i, 
  bdd_ptr  t, 
  bdd_ptr  e 
)
Implements ITE(i,t,e). Returns a pointer to the resulting BDD if successful; a failure is generated otherwise.

Side Effects None

Defined in dd.c

bdd_ptr 
bdd_largest_cube(
  DdManager * dd, 
  bdd_ptr  b, 
  int * length 
)
Finds a largest cube in a BDD b, i.e. an implicant of BDD b. Notice that, it is not guaranteed to be the largest implicant of b.

Side Effects The number of literals of the cube is returned in length.

Defined in dd.c

int 
bdd_leq(
  DdManager * dd, 
  bdd_ptr  f, 
  bdd_ptr  g 
)
Returns 1 if f is less than or equal to g; 0 otherwise. No new nodes are created.

Side Effects None

Defined in dd.c

bdd_ptr 
bdd_make_prime(
  DdManager * dd, 
  bdd_ptr  cube, 
  bdd_ptr  b 
)
Expands cube to a prime implicant of f. Returns the prime if successful; NULL otherwise. In particular, NULL is returned if cube is not a real cube or is not an implicant of f.

Side Effects None

Defined in dd.c

bdd_ptr 
bdd_minimize(
  DdManager * dd, 
  bdd_ptr  fn, 
  bdd_ptr  c 
)
Restrict operator as described in Coudert et al. ICCAD90. Always returns a BDD not larger than the input f if successful; a failure is generated otherwise. The result is referenced.

See Also bdd_simplify_assuming
Defined in dd.c

bdd_ptr 
bdd_new_var_with_index(
  DdManager * dd, 
  int  index 
)
Retrieves the BDD variable with index index if it already exists, or creates a new BDD variable. Returns a pointer to the variable if successful; a failure is generated otherwise. The returned value is referenced.

See Also bdd_new_var_at_level add_new_var_at_level
Defined in dd.c

bdd_ptr 
bdd_not(
  DdManager * dd, 
  bdd_ptr  fn 
)
Applies logical NOT to the corresponding discriminant of f. f must be a BDD. Returns a pointer to the result if successful; a failure is generated otherwise.

See Also bdd_and bdd_xor bdd_or bdd_imply
Defined in dd.c

void 
bdd_or_accumulate(
  DdManager * dd, 
  bdd_ptr * a, 
  bdd_ptr  b 
)
Applies logical OR to the corresponding discriminants of f and g and stores the result in f. f and g must be two BDDs. The result is referenced.

Side Effects The result is stored in the first operand and referenced.

See Also bdd_and
Defined in dd.c

bdd_ptr 
bdd_or(
  DdManager * dd, 
  bdd_ptr  a, 
  bdd_ptr  b 
)
Applies logical OR to the corresponding discriminants of f and g. f and g must be BDDs. Returns a pointer to the result if successful; a failure is generated otherwise.

See Also bdd_and bdd_xor bdd_not
Defined in dd.c

bdd_ptr 
bdd_permute(
  DdManager * dd, 
  bdd_ptr  fn, 
  int * permut 
)
Given a permutation in array permut, creates a new BDD with permuted variables. There should be an entry in array permut for each variable in the manager. The i-th entry of permut holds the index of the variable that is to substitute the i-th variable. Returns a pointer to the resulting BDD if successful; a failure is generated otherwise. The result is referenced.

See Also bdd_permute
Defined in dd.c

int 
bdd_pick_all_terms(
  DdManager * dd, dd manager
  bdd_ptr  pick_from_set, minterm from which to pick all term
  bdd_ptr * vars, The array of vars to be put in the returned array
  int  vars_dim, The size of the above array
  bdd_ptr * result, The array used as return value
  int  result_dim The size of the above array
)
Takes a minterm and returns an array of all its terms, according to variables specified in the array vars[

See Also bdd_pick_one_minterm_rand bdd_pick_one_minterm
Defined in dd.c

bdd_ptr 
bdd_pick_one_minterm_rand(
  DdManager * dd, 
  bdd_ptr  fn, 
  bdd_ptr * vars, 
  int  n 
)
Picks one on-set minterm randomly from the given DD. The minterm is in terms of vars. Builds a BDD for the minterm and returns a pointer to it if successful; a failure is generated otherwise. There are two reasons why the procedure may fail: It may run out of memory; or the function f may be the constant 0.

Defined in dd.c

bdd_ptr 
bdd_pick_one_minterm(
  DdManager * dd, 
  bdd_ptr  fn, 
  bdd_ptr * vars, 
  int  n 
)
Picks one on-set minterm deterministically from the given DD. The minterm is in terms of vars. Builds a BDD for the minterm and returns a pointer to it if successful; a failure is generated otherwise. There are two reasons why the procedure may fail: It may run out of memory; or the function fn may be the constant 0. The result is referenced.

Defined in dd.c

int 
bdd_readperm(
  DdManager * dd, 
  bdd_ptr  f 
)
Finds the current position of variable index in the order.

Side Effects None

Defined in dd.c

int 
bdd_ref_count(
  bdd_ptr  n 
)
Returns the reference count of a node. The node pointer can be either regular or complemented.

Side Effects None

Defined in dd.c

void 
bdd_ref(
  bdd_ptr  dd_node 
)
Reference an BDD node.

Side Effects The reference count of the node is incremented by one.

See Also bdd_deref bdd_free
Defined in dd.c

bdd_ptr 
bdd_simplify_assuming(
  DdManager * dd, 
  bdd_ptr  fn, 
  bdd_ptr  c 
)
BDD restrict according to Coudert and Madre's algorithm (ICCAD90). Returns the restricted BDD if successful; a failure is generated otherwise. If application of restrict results in an BDD larger than the input BDD, the input BDD is returned.

Defined in dd.c

int 
bdd_size(
  DdManager * dd, 
  bdd_ptr  fn 
)
Counts the number of BDD nodes in an BDD. Returns the number of nodes in the graph rooted at node.

See Also bdd_count_minterm
Defined in dd.c

bdd_ptr 
bdd_support(
  DdManager * dd, 
  bdd_ptr  fn 
)
Finds the variables on which an BDD depends on. Returns an BDD consisting of the product of the variables if successful; a failure is generated otherwise.

See Also add_support
Defined in dd.c

bdd_ptr 
bdd_swap_variables(
  DdManager * dd, 
  bdd_ptr  f, 
  bdd_ptr * x_varlist, 
  bdd_ptr * y_varlist, 
  int  n 
)
Swaps two sets of variables of the same size (x and y) in the BDD f. The size is given by n. The two sets of variables are assumed to be disjoint. Returns a pointer to the resulting BDD if successful; an error (which either results in a jump to the last CATCH-FAIL block, or in a call to exit()) is triggered otherwise.

Side Effects None

Defined in dd.c

bdd_ptr 
bdd_then(
  DdManager * dd, 
  bdd_ptr  f 
)
Returns the then child of a bdd node. The node must not be a leaf node. Notice that this funxction does not save the bdd. Is the responsibility of the user to save it if it is the case.

Side Effects None

Defined in dd.c

add_ptr 
bdd_to_01_add(
  DdManager * dd, 
  bdd_ptr  fn 
)
Converts a BDD to a 0-1 ADD. Returns a pointer to the resulting ADD if successful; a failure is generated otherwise.

See Also bdd_to_add
Defined in dd.c

add_ptr 
bdd_to_add(
  DdManager * dd, 
  bdd_ptr  fn 
)
Converts a BDD to a FALSE-TRUE ADD. Returns a pointer to the resulting ADD if successful; a failure is generated otherwise.

See Also add_to_bdd bdd_to_01_add
Defined in dd.c

bdd_ptr 
bdd_true(
  DdManager * dd 
)
Reads the constant TRUE BDD of the manager.

See Also bdd_false
Defined in dd.c

bdd_ptr 
bdd_xor(
  DdManager * dd, 
  bdd_ptr  a, 
  bdd_ptr  b 
)
Applies logical XOR to the corresponding discriminants of f and g. f and g must be BDDs. Returns a pointer to the result if successful; a failure is generated otherwise.

See Also bdd_or bdd_imply bdd_not
Defined in dd.c

int 
calculate_bdd_value(
  DdManager* mgr, 
  bdd_ptr  f, 
  int* values 
)
Computes the value (0 or 1) of the given function with the given values for variables. The parameter "values" must be an array, at least as long as the number of indices in the BDD.

Side Effects None

Defined in dd.c

void 
dd_autodyn_disable(
  DdManager * dd 
)
Disables automatic dynamic reordering of BDD and ADD.

See Also dd_autodyn_enable dd_reordering_status
Defined in dd.c

void 
dd_autodyn_enable(
  DdManager * dd, 
  dd_reorderingtype  method 
)
Enables automatic dynamic reordering of BDDs and ADDs. Parameter method is used to determine the method used for reordering. If REORDER_SAME is passed, the method is unchanged.

See Also dd_autodyn_disable dd_reordering_status
Defined in dd.c

int 
dd_checkzeroref(
  DdManager * dd 
)
Checks the unique table for nodes with non-zero reference counts. It is normally called before dd_quit to make sure that there are no memory leaks due to missing add/bdd_free's. Takes into account that reference counts may saturate and that the basic constants and the projection functions are referenced by the manager. Returns the number of nodes with non-zero reference count. (Except for the cases mentioned above.)

Defined in dd.c

int 
dd_dump_davinci(
  DdManager * dd, manager
  int  n, number of output nodes to be dumped
  bdd_ptr * f, array of output nodes to be dumped
  char ** inames, array of input names (or NULL)
  char ** onames, array of output names (or NULL)
  FILE * fp pointer to the dump file
)
Writes a daVnci file representing the argument DDs. For a better description see the "Cudd_DumpDaVinci" documentation in the CUDD package.

See Also dd_dump_davinci
Defined in dd.c

int 
dd_dump_dot(
  DdManager * dd, manager
  int  n, number of output nodes to be dumped
  bdd_ptr * f, array of output nodes to be dumped
  char ** inames, array of input names (or NULL)
  char ** onames, array of output names (or NULL)
  FILE * fp pointer to the dump file
)
Writes a dot file representing the argument DDs. For a better description see the "Cudd_DumpDot" documentation in the CUDD package.

See Also dd_dump_davinci
Defined in dd.c

int 
dd_free_var_block(
  DdManager* dd, 
  dd_block* group 
)
Dissolves a group previously created by dd_new_var_block. Returns 0 if the group was actually removed, 1 otherwise (that may be not due to an error)

Side Effects Modifies the variable tree.

Defined in dd.c

int 
dd_get_index_at_level(
  DdManager * dd, 
  int  level 
)
Returns the index of the variable currently in the i-th position of the order. If the index is MAX_VAR_INDEX, returns MAX_VAR_INDEX; otherwise, if the index is out of bounds fails.

Defined in dd.c

int 
dd_get_level_at_index(
  DdManager * dd, 
  int  index 
)
Returns the current position of the i-th variable in the order. If the index is CUDD_MAXINDEX, returns CUDD_MAXINDEX; otherwise, if the index is out of bounds returns -1.

Side Effects None

See Also Cudd_ReadInvPerm Cudd_ReadPermZdd
Defined in dd.c

dd_reorderingtype 
dd_get_ordering_method(
  DdManager * dd 
)
Returns the internal reordering method used.

Defined in dd.c

int 
dd_get_reorderings(
  DdManager* dd 
)
Returns the number of times reordering has occurred in the manager. The number includes both the calls to Cudd_ReduceHeap from the application program and those automatically performed by the package. However, calls that do not even initiate reordering are not counted. A call may not initiate reordering if there are fewer than minsize live nodes in the manager, or if CUDD_REORDER_NONE is specified as reordering method. The calls to Cudd_ShuffleHeap are not counted.

Defined in dd.c

int 
dd_get_size(
  DdManager * dd 
)
Returns the number of BDD variables in existance.

Defined in dd.c

dd_block * 
dd_new_var_block(
  DdManager * dd, 
  int  start_index, 
  int  offset 
)
Builds a group of variables that should stay adjacent during reordering. The group is made up of n variables. The first variable in the group is f. The other variables are the n-1 variables following f in the order at the time of invocation of this function. Returns a handle to the variable group if successful else fail.

Side Effects Modifies the variable tree.

Defined in dd.c

void 
dd_print_stats(
  DdManager * mgr, 
  FILE * file 
)
Prints out statistics and settings for a CUDD manager.

Defined in dd.c

int 
dd_printminterm(
  DdManager * manager, 
  DdNode * node 
)
Prints a disjoint sum of product cover for the function rooted at node. Each product corresponds to a path from node a leaf node different from the logical zero, and different from the background value. Uses the standard output. Returns 1 if successful; 0 otherwise.

Defined in dd.c

int 
dd_reordering_status(
  DdManager * dd, 
  dd_reorderingtype * method 
)
Reports the status of automatic dynamic reordering of BDDs and ADDs. Parameter method is set to the reordering method currently selected. Returns 1 if automatic reordering is enabled; 0 otherwise.

Side Effects Parameter method is set to the reordering method currently selected.

See Also dd_autodyn_disable dd_autodyn_enable
Defined in dd.c

int 
dd_reorder(
  DdManager * dd, 
  int  method, 
  int  minsize 
)
Main dynamic reordering routine. Calls one of the possible reordering procedures: For sifting, symmetric sifting, group sifting, and window permutation it is possible to request reordering to convergence.

Returns 1 in case of success; 0 otherwise. In the case of symmetric sifting (with and without convergence) returns 1 plus the number of symmetric variables, in case of success.

This functions takes as arguments:

Side Effects Changes the variable order for all diagrams and clears the cache.

See Also Cudd_ReduceHeap
Defined in dd.c

int 
dd_set_order(
  DdManager* dd, 
  int* permutation 
)
Reorders variables according to given permutation. The i-th entry of the permutation array contains the index of the variable that should be brought to the i-th level. The size of the array should be equal or greater to the number of variables currently in use. Returns 1 in case of success; 0 otherwise.

Side Effects Changes the variable order for all diagrams and clears the cache.

Defined in dd.c

int 
dd_set_parameters(
  DdManager * mgr, 
  OptsHandler_ptr  opt, 
  FILE * file 
)
The CUDD package has a set of parameters that can be assigned different values. This function receives a table which maps strings to values and sets the parameters represented by the strings to the pertinent values. Some basic type checking is done. It returns 1 if everything is correct and 0 otherwise.

Defined in dd.c

int 
get_dd_nodes_allocated(
  DdManager * dd 
)
Returns the total number of nodes currently in the unique table, including the dead nodes.

Defined in dd.c

DdManager* 
init_dd_package(
    
)
Creates a new DD manager, initializes the table, the basic constants and the projection functions.
"maxMemory" (the last parameter of the function "Cudd_Init") is set to 0. In such a way "Cudd_Init" decides suitables values for the maximum size of the cache and for the limit for fast unique table growth based on the available memory. Returns a pointer to the manager if successful; else abort depending the mode (interactive or batch) the system is used.

See Also quit_dd_package
Defined in dd.c

node_ptr 
map_dd(
  DdManager * dd, 
  NPFDD  f, 
  node_ptr  l 
)
This function acts like the Lisp mapcar. It returns the list of the result of the application of function code>f to each element of list l.

See Also map walk walk_dd
Defined in dd.c

void 
quit_dd_package(
  DdManager * dd 
)
Deletes resources associated with a DD manager and resets the global statistical counters. (Otherwise, another manager subsequently created would inherit the stats of this one.)

See Also init_dd_package
Defined in dd.c

void 
walk_dd(
  DdManager * dd, 
  VPFDD  f, 
  node_ptr  l 
)
This function acts like the map_dd
. This functions applies the function f to each element of list l. Nothing is returned, performs side-effects on the elements.

See Also map walk map_dd
Defined in dd.c

Last updated on 2010/11/04 13h:34