.\" Automatically generated by Pod::Man v1.34, Pod::Parser v1.13
.\" ========================================================================
.de Sh \" Subsection heading
.de Sp \" Vertical space (when we can't use .PP)
.de Vb \" Begin verbatim text
.de Ve \" End verbatim text
.\" Set up some character translations and predefined strings. \*(-- will
.\" give an unbreakable dash, \*(PI will give pi, \*(L" will give a left
.\" double quote, and \*(R" will give a right double quote. | will give a
.\" real vertical bar. \*(C+ will give a nicer C++. Capital omega is used to
.\" do unbreakable dashes and therefore won't be available. \*(C` and \*(C'
.\" expand to `' in nroff, nothing in troff, for use with C<>.
.ds C+ C\v'-.1v'\h'-1p'\s-2+\h'-1p'+\s0\v'.1v'\h'-1p'
. if (\n(.H=4u)&(1m=24u) .ds -- \(*W\h'-12u'\(*W\h'-12u'-\" diablo 10 pitch
. if (\n(.H=4u)&(1m=20u) .ds -- \(*W\h'-12u'\(*W\h'-8u'-\" diablo 12 pitch
.\" If the F register is turned on, we'll generate index entries on stderr for
.\" titles (.TH), headers (.SH), subsections (.Sh), items (.Ip), and index
.\" entries marked with X<> in POD. Of course, you'll have to process the
.\" output yourself in some meaningful fashion.
. tm Index:\\$1\t\\n%\t"\\$2"
.\" For nroff, turn off justification. Always turn off hyphenation; it makes
.\" way too many mistakes in technical documents.
.\" Accent mark definitions (@(#)ms.acc 1.5 88/02/08 SMI; from UCB 4.2).
.\" Fear. Run. Save yourself. No user-serviceable parts.
. \" fudge factors for nroff and troff
. ds #H ((1u-(\\\\n(.fu%2u))*.13m)
. \" simple accents for nroff and troff
. ds ' \\k:\h'-(\\n(.wu*8/10-\*(#H)'\'\h"|\\n:u"
. ds ` \\k:\h'-(\\n(.wu*8/10-\*(#H)'\`\h'|\\n:u'
. ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'^\h'|\\n:u'
. ds , \\k:\h'-(\\n(.wu*8/10)',\h'|\\n:u'
. ds ~ \\k:\h'-(\\n(.wu-\*(#H-.1m)'~\h'|\\n:u'
. ds / \\k:\h'-(\\n(.wu*8/10-\*(#H)'\z\(sl\h'|\\n:u'
. \" troff and (daisy-wheel) nroff accents
.ds : \\k:\h'-(\\n(.wu*8/10-\*(#H+.1m+\*(#F)'\v'-\*(#V'\z.\h'.2m+\*(#F'.\h'|\\n:u'\v'\*(#V'
.ds 8 \h'\*(#H'\(*b\h'-\*(#H'
.ds o \\k:\h'-(\\n(.wu+\w'\(de'u-\*(#H)/2u'\v'-.3n'\*(#[\z\(de\v'.3n'\h'|\\n:u'\*(#]
.ds d- \h'\*(#H'\(pd\h'-\w'~'u'\v'-.25m'\f2\(hy\fP\v'.25m'\h'-\*(#H'
.ds D- D\\k:\h'-\w'D'u'\v'-.11m'\z\(hy\v'.11m'\h'|\\n:u'
.ds th \*(#[\v'.3m'\s+1I\s-1\v'-.3m'\h'-(\w'I'u*2/3)'\s-1o\s+1\*(#]
.ds Th \*(#[\s+2I\s-2\h'-\w'I'u*3/5'\v'-.3m'o\v'.3m'\*(#]
.ds ae a\h'-(\w'a'u*4/10)'e
.ds Ae A\h'-(\w'A'u*4/10)'E
. \" corrections for vroff
.if v .ds ~ \\k:\h'-(\\n(.wu*9/10-\*(#H)'\s-2\u~\d\s+2\h'|\\n:u'
.if v .ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'\v'-.4m'^\v'.4m'\h'|\\n:u'
. \" for low resolution devices (crt and lpr)
.if \n(.H>23 .if \n(.V>19 \
.\" ========================================================================
.TH Cudd 3 "2004-02-11" "perl v5.8.0" "User Contributed Perl Documentation"
Cudd \- Perl extension for BDDs
\&\f(CW\*(C`use Cudd;\*(C'\fR
\&\f(CW\*(C`my $manager = new Cudd;\*(C'\fR
Cudd extends Perl so that it manipulates Binary Decision Diagrams
(BDDs) by providing an object-oriented encapsulation of the \s-1CUDD\s0
package. The \s-1CUDD\s0 package is written in C and contains a large
collection of efficient \s-1BDD\s0 manipulation functions. Only a small
fraction of those functions are currently made available by the Cudd
module. Those that are available, however, allow one to accomplish
The methods defined by Cudd are divided into two packages. The first
package, Cudd, defines methods that create and manipulate \s-1BDD\s0 managers
and \s-1BDD\s0 variables. These are the methods defined in package Cudd:
Creates a new \s-1BDD\s0 manager.
Creates a new variable in a \s-1BDD\s0 manager.
Returns the constant 1 of a \s-1BDD\s0 manager.
Reorders the BDDs of a manager.
Enables dynamic reordering for a \s-1BDD\s0 manager.
Disables dynamic reordering for a \s-1BDD\s0 manager.
.IX Item "ReportReordering"
Enables reporting of dynamic reordering.
.IP "DoNotReportReordering" 4
.IX Item "DoNotReportReordering"
Disables reporting of dynamic reordering.
Prints statistical information on a \s-1BDD\s0 manager.
Returns the peak number of live nodes in the manager.
Returns the number of live nodes in the manager.
.IP "DynReorderingStatus" 4
.IX Item "DynReorderingStatus"
Returns a list with two elements. The first is 1 if reordering is
currently enabled and 0 otherwise; the second is the reordering method
The second package in module Cudd is Cudd::BDD. It defines methods
that manipulate BDDs. Starting with a set of variables belonging to a
manager, the functions in this package allow one to create BDDs for
arbitrary functions over those variables. These are the methods
Returns the constant 1 \s-1BDD\s0 from the manager of \f(CW$f\fR.
Returns the constant 0 \s-1BDD\s0 from the manager of \f(CW$f\fR.
Computes the conjunction of two BDDs. Overloads '*'.
Computes the disjunction of two BDDs. Overloads '+'.
Computes the exclusive or of two BDDs. Overloads '^'.
Computes the \s-1NAND\s0 of two BDDs.
Computes the \s-1NOR\s0 of two BDDs.
Computes the cofactor of a \s-1BDD\s0 with respect to another. Uses the constrain
algorithm. Overloads '/'.
Computes the cofactor of a \s-1BDD\s0 with respect to another. Uses the restrict
Finds a small \s-1BDD\s0 in an interval.
Existentially quantifies the variables in a cube from a \s-1BDD\s0.
Universally quantifies the variables in a cube from a \s-1BDD\s0.
Existentially quantifies the variables in a cube from the conjunction of
Composes a \s-1BDD\s0 \f(CW$g\fR into a \s-1BDD\s0 \f(CW$f\fR substituting variable \f(CW$var\fR.
Computes the boolean difference of a \s-1BDD\s0 with respect to one variable.
Computes the correlation of two BDDs. The result is a number between 0
and 1. A value of 1 indicates that the functions \f(CW$f\fR and \f(CW$g\fR are
identical. A value of 0 indicates that they are complementary.
Returns 1 if the \s-1BDD\s0 \f(CW$f\fR is monotonic decreasing (negative unate) in
variable \f(CW$var\fR; 0 otherwise.
Returns 1 if the \s-1BDD\s0 \f(CW$f\fR is monotonic increasing (positive unate) in
variable \f(CW$var\fR; 0 otherwise.
Finds the essential variables of a \s-1BDD\s0. Returns an array of all essentials.
Negative essentials correspond to negative literals.
Returns a cube of all the variables in the support of \f(CW$f\fR.
.IP "LiteralSetIntersection" 4
.IX Item "LiteralSetIntersection"
Computes the intersection of two literal sets represented by cube BDDs.
Swaps two sets of variables in a \s-1BDD\s0.
Solves a boolean equation. The first argument \f(CW$f\fR is the left-hand side
of the equation \f(CW$f\fR = 0. The second argument is a reference to the
array of the unknowns. The variables that are not unknowns are
Computes the variable signatures in a \s-1BDD\s0. The signature of a variable
is the fraction of minterms in the on-set of the cofactor w.r.t. to
that variable. The function returns an array of as many signatures as
there are variables plus one. The last element of the array is the
fraction of minterms in the ON-set of the \s-1BDD\s0, and can be used to
normalize the variable signatures.
.IX Item "NormSignatures"
Returns signatures normalized between 0 and 2. See also Signatures.
Computes a subset of a \s-1BDD\s0 with a maximum number of nodes. Uses the
Computes a subset of a \s-1BDD\s0 with a maximum number of nodes. Uses the
Computes a superset of a \s-1BDD\s0 with a maximum number of nodes. Uses the
Computes a superset of a \s-1BDD\s0 with a maximum number of nodes. Uses the
Creates a new variable adjacent to the given variable. Useful in creating the next state variables of FSMs.
Creates a group of variables to be kept adjacent during reordering.
Returns the complement of a \s-1BDD\s0. Overloads '!'.
Returns 1 if the two arguments are equivalent; 0 otherwise. Overloads '=='.
Returns 1 if the two arguments are not equivalent; 0 otherwise. Overloads '!='.
Compares two BDDs \f(CW$f\fR and \f(CW$g\fR and returns 1 if \f(CW$f\fR is less than or equal to \f(CW$g\fR.
Compares two BDDs \f(CW$f\fR and \f(CW$g\fR and returns 1 if \f(CW$f\fR is greater than or equal to \f(CW$g\fR.
Returns 1 if the \s-1BDD\s0 node is complemented, that is, if the \s-1BDD\s0 evaluates to 0 when all variables are assigned 1.
Computes a shortest path in a \s-1BDD\s0.
Returns the number of nodes in the \s-1BDD\s0 or BDDs passed as arguments.
Returns the number of minterms of the \s-1BDD\s0. The function of the \s-1BDD\s0 is
supposed to depend on \f(CW$n\fR variables.
Prints information about a \s-1BDD\s0 \f(CW$f\fR. The \f(CW$pr\fR parameter controls how much
information is printed. The \f(CW$n\fR parameter specifies how many inputs \f(CW$f\fR depends
on. This information is necessary to compute the number of minterms.
Prints a description of a set of BDDs in dot format. The function has
one mandatory parameter, the list of BDDs for which the dot
description is desired, and two optional parameters, the array of
input names and the array of output names. All parameters are array
references. If the input names are omitted but the output names are
not, a reference to an empty array ([]) should be passed for the input
Computes a function included in the intersection of \f(CW$f\fR and \f(CW$g\fR. (That
is, a witness that the intersection is not empty.) Intersect tries to
build as few new nodes as possible.
.IX Item "ConstrainDecomp"
\&\s-1BDD\s0 conjunctive decomposition as in the \s-1CAV96\s0 paper by McMillan. The
decomposition is canonical only for a given variable order. If
canonicity is required, variable ordering must be disabled after the
decomposition has been computed. Returns an array with one entry for
each \s-1BDD\s0 variable.
Computes a vector of functions such that their image equals a non-zero
function. Returns an array with one entry for each \s-1BDD\s0 variable.
.IX Item "PrioritySelect"
Selects pairs from a relation \f(CW\*(C`R(x,y)\*(C'\fR (given as a \s-1BDD\s0)
in such a way that a given x appears in one pair only. Uses a
priority function to determine which y should be paired to a given x.
Returns the priority function that is 1 if the distance of x from y is greater than the distance of x from z.
Returns the priority function that is 1 if the distance of x from y is greater than the distance of y from z.
Returns the priority function that is 1 if x is greater than y.
Applies the C\-Projection to a relation R.
Package Cudd:BDD overloads common operators as follows:
\&\f(CW\*(C`+ \*(C'\fR \-> Or
\&\f(CW\*(C`* \*(C'\fR \-> And
\&\f(CW\*(C`^ \*(C'\fR \-> Xor
\&\f(CW\*(C`! \*(C'\fR \-> Not
\&\f(CW\*(C`/ \*(C'\fR \-> Cofactor
\&\f(CW\*(C`==\*(C'\fR \-> Equal
\&\f(CW\*(C`!=\*(C'\fR \-> Unequal
\&\f(CW\*(C`<=\*(C'\fR \-> Leq
\&\f(CW\*(C`>=\*(C'\fR \-> Geq
The following code fragment creates a manager, two variables \f(CW$x\fR and
\&\f(CW$y\fR in it, and then builds and prints the conjunction of the two
\& my $manager = new Cudd;
\& my $x = $manager->BddVar;
\& my $y = $manager->BddVar;
\& $z->Print(2,1); # (2 variables, verbosity 1)
Fabio Somenzi, Fabio@Colorado.EDU
projects / OpenSPARC-T2-DV / blob