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:
- F @ 0 = 0
- F @ 1 = F
- 0 @ c = 0
- 1 @ c = 1
- F @ F = 1
- F @ F'= 0
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
dd_ptr * f, array of output nodes to be dumped
const char ** inames, array of input names (or NULL)
const 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
dd_ptr * f, array of output nodes to be dumped
const char ** inames, array of input names (or NULL)
const char ** onames, array of output names (or NULL)
FILE * fp pointer to the dump file
)
- Writes a file representing the argument DDs in a format
suitable for the graph drawing program dot.
It returns 1 in case of success; 0 otherwise (e.g., out-of-memory,
file system full).
Cudd_DumpDot does not close the file: This is the caller
responsibility. Cudd_DumpDot 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.
Cudd_DumpDot uses the following convention to draw arcs:
- solid line: THEN arcs;
- dotted line: complement arcs;
- dashed line: regular ELSE arcs.
The dot options are chosen so that the drawing fits on a letter-size
sheet.
- 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,
dd_ptr 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:
- Swapping
- Sifting
- Symmetric Sifting
- Group Sifting
- Window Permutation
- Simulated Annealing
- Genetic Algorithm
- Dynamic Programming (exact)
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:
- dd the DD manager;
- heuristics method used for reordering;
- minsize bound below which no reordering occurs;
- 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