Commit | Line | Data |
---|---|---|
86530b38 AT |
1 | .\" Automatically generated by Pod::Man v1.34, Pod::Parser v1.13 |
2 | .\" | |
3 | .\" Standard preamble: | |
4 | .\" ======================================================================== | |
5 | .de Sh \" Subsection heading | |
6 | .br | |
7 | .if t .Sp | |
8 | .ne 5 | |
9 | .PP | |
10 | \fB\\$1\fR | |
11 | .PP | |
12 | .. | |
13 | .de Sp \" Vertical space (when we can't use .PP) | |
14 | .if t .sp .5v | |
15 | .if n .sp | |
16 | .. | |
17 | .de Vb \" Begin verbatim text | |
18 | .ft CW | |
19 | .nf | |
20 | .ne \\$1 | |
21 | .. | |
22 | .de Ve \" End verbatim text | |
23 | .ft R | |
24 | .fi | |
25 | .. | |
26 | .\" Set up some character translations and predefined strings. \*(-- will | |
27 | .\" give an unbreakable dash, \*(PI will give pi, \*(L" will give a left | |
28 | .\" double quote, and \*(R" will give a right double quote. | will give a | |
29 | .\" real vertical bar. \*(C+ will give a nicer C++. Capital omega is used to | |
30 | .\" do unbreakable dashes and therefore won't be available. \*(C` and \*(C' | |
31 | .\" expand to `' in nroff, nothing in troff, for use with C<>. | |
32 | .tr \(*W-|\(bv\*(Tr | |
33 | .ds C+ C\v'-.1v'\h'-1p'\s-2+\h'-1p'+\s0\v'.1v'\h'-1p' | |
34 | .ie n \{\ | |
35 | . ds -- \(*W- | |
36 | . ds PI pi | |
37 | . if (\n(.H=4u)&(1m=24u) .ds -- \(*W\h'-12u'\(*W\h'-12u'-\" diablo 10 pitch | |
38 | . if (\n(.H=4u)&(1m=20u) .ds -- \(*W\h'-12u'\(*W\h'-8u'-\" diablo 12 pitch | |
39 | . ds L" "" | |
40 | . ds R" "" | |
41 | . ds C` "" | |
42 | . ds C' "" | |
43 | 'br\} | |
44 | .el\{\ | |
45 | . ds -- \|\(em\| | |
46 | . ds PI \(*p | |
47 | . ds L" `` | |
48 | . ds R" '' | |
49 | 'br\} | |
50 | .\" | |
51 | .\" If the F register is turned on, we'll generate index entries on stderr for | |
52 | .\" titles (.TH), headers (.SH), subsections (.Sh), items (.Ip), and index | |
53 | .\" entries marked with X<> in POD. Of course, you'll have to process the | |
54 | .\" output yourself in some meaningful fashion. | |
55 | .if \nF \{\ | |
56 | . de IX | |
57 | . tm Index:\\$1\t\\n%\t"\\$2" | |
58 | .. | |
59 | . nr % 0 | |
60 | . rr F | |
61 | .\} | |
62 | .\" | |
63 | .\" For nroff, turn off justification. Always turn off hyphenation; it makes | |
64 | .\" way too many mistakes in technical documents. | |
65 | .hy 0 | |
66 | .if n .na | |
67 | .\" | |
68 | .\" Accent mark definitions (@(#)ms.acc 1.5 88/02/08 SMI; from UCB 4.2). | |
69 | .\" Fear. Run. Save yourself. No user-serviceable parts. | |
70 | . \" fudge factors for nroff and troff | |
71 | .if n \{\ | |
72 | . ds #H 0 | |
73 | . ds #V .8m | |
74 | . ds #F .3m | |
75 | . ds #[ \f1 | |
76 | . ds #] \fP | |
77 | .\} | |
78 | .if t \{\ | |
79 | . ds #H ((1u-(\\\\n(.fu%2u))*.13m) | |
80 | . ds #V .6m | |
81 | . ds #F 0 | |
82 | . ds #[ \& | |
83 | . ds #] \& | |
84 | .\} | |
85 | . \" simple accents for nroff and troff | |
86 | .if n \{\ | |
87 | . ds ' \& | |
88 | . ds ` \& | |
89 | . ds ^ \& | |
90 | . ds , \& | |
91 | . ds ~ ~ | |
92 | . ds / | |
93 | .\} | |
94 | .if t \{\ | |
95 | . ds ' \\k:\h'-(\\n(.wu*8/10-\*(#H)'\'\h"|\\n:u" | |
96 | . ds ` \\k:\h'-(\\n(.wu*8/10-\*(#H)'\`\h'|\\n:u' | |
97 | . ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'^\h'|\\n:u' | |
98 | . ds , \\k:\h'-(\\n(.wu*8/10)',\h'|\\n:u' | |
99 | . ds ~ \\k:\h'-(\\n(.wu-\*(#H-.1m)'~\h'|\\n:u' | |
100 | . ds / \\k:\h'-(\\n(.wu*8/10-\*(#H)'\z\(sl\h'|\\n:u' | |
101 | .\} | |
102 | . \" troff and (daisy-wheel) nroff accents | |
103 | .ds : \\k:\h'-(\\n(.wu*8/10-\*(#H+.1m+\*(#F)'\v'-\*(#V'\z.\h'.2m+\*(#F'.\h'|\\n:u'\v'\*(#V' | |
104 | .ds 8 \h'\*(#H'\(*b\h'-\*(#H' | |
105 | .ds o \\k:\h'-(\\n(.wu+\w'\(de'u-\*(#H)/2u'\v'-.3n'\*(#[\z\(de\v'.3n'\h'|\\n:u'\*(#] | |
106 | .ds d- \h'\*(#H'\(pd\h'-\w'~'u'\v'-.25m'\f2\(hy\fP\v'.25m'\h'-\*(#H' | |
107 | .ds D- D\\k:\h'-\w'D'u'\v'-.11m'\z\(hy\v'.11m'\h'|\\n:u' | |
108 | .ds th \*(#[\v'.3m'\s+1I\s-1\v'-.3m'\h'-(\w'I'u*2/3)'\s-1o\s+1\*(#] | |
109 | .ds Th \*(#[\s+2I\s-2\h'-\w'I'u*3/5'\v'-.3m'o\v'.3m'\*(#] | |
110 | .ds ae a\h'-(\w'a'u*4/10)'e | |
111 | .ds Ae A\h'-(\w'A'u*4/10)'E | |
112 | . \" corrections for vroff | |
113 | .if v .ds ~ \\k:\h'-(\\n(.wu*9/10-\*(#H)'\s-2\u~\d\s+2\h'|\\n:u' | |
114 | .if v .ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'\v'-.4m'^\v'.4m'\h'|\\n:u' | |
115 | . \" for low resolution devices (crt and lpr) | |
116 | .if \n(.H>23 .if \n(.V>19 \ | |
117 | \{\ | |
118 | . ds : e | |
119 | . ds 8 ss | |
120 | . ds o a | |
121 | . ds d- d\h'-1'\(ga | |
122 | . ds D- D\h'-1'\(hy | |
123 | . ds th \o'bp' | |
124 | . ds Th \o'LP' | |
125 | . ds ae ae | |
126 | . ds Ae AE | |
127 | .\} | |
128 | .rm #[ #] #H #V #F C | |
129 | .\" ======================================================================== | |
130 | .\" | |
131 | .IX Title "Cudd 3" | |
132 | .TH Cudd 3 "2004-02-11" "perl v5.8.0" "User Contributed Perl Documentation" | |
133 | .SH "NAME" | |
134 | Cudd \- Perl extension for BDDs | |
135 | .SH "SYNOPSIS" | |
136 | .IX Header "SYNOPSIS" | |
137 | \&\f(CW\*(C`use Cudd;\*(C'\fR | |
138 | .PP | |
139 | \&\f(CW\*(C`my $manager = new Cudd;\*(C'\fR | |
140 | .PP | |
141 | and so on | |
142 | .SH "DESCRIPTION" | |
143 | .IX Header "DESCRIPTION" | |
144 | Cudd extends Perl so that it manipulates Binary Decision Diagrams | |
145 | (BDDs) by providing an object-oriented encapsulation of the \s-1CUDD\s0 | |
146 | package. The \s-1CUDD\s0 package is written in C and contains a large | |
147 | collection of efficient \s-1BDD\s0 manipulation functions. Only a small | |
148 | fraction of those functions are currently made available by the Cudd | |
149 | module. Those that are available, however, allow one to accomplish | |
150 | most tasks. | |
151 | .Sh "" | |
152 | .IX Subsection "" | |
153 | The methods defined by Cudd are divided into two packages. The first | |
154 | package, Cudd, defines methods that create and manipulate \s-1BDD\s0 managers | |
155 | and \s-1BDD\s0 variables. These are the methods defined in package Cudd: | |
156 | .IP "new" 4 | |
157 | .IX Item "new" | |
158 | Creates a new \s-1BDD\s0 manager. | |
159 | .IP "BddVar" 4 | |
160 | .IX Item "BddVar" | |
161 | Creates a new variable in a \s-1BDD\s0 manager. | |
162 | .IP "BddOne" 4 | |
163 | .IX Item "BddOne" | |
164 | Returns the constant 1 of a \s-1BDD\s0 manager. | |
165 | .IP "Reorder" 4 | |
166 | .IX Item "Reorder" | |
167 | Reorders the BDDs of a manager. | |
168 | .IP "EnableDyn" 4 | |
169 | .IX Item "EnableDyn" | |
170 | Enables dynamic reordering for a \s-1BDD\s0 manager. | |
171 | .IP "DisableDyn" 4 | |
172 | .IX Item "DisableDyn" | |
173 | Disables dynamic reordering for a \s-1BDD\s0 manager. | |
174 | .IP "ReportReordering" 4 | |
175 | .IX Item "ReportReordering" | |
176 | Enables reporting of dynamic reordering. | |
177 | .IP "DoNotReportReordering" 4 | |
178 | .IX Item "DoNotReportReordering" | |
179 | Disables reporting of dynamic reordering. | |
180 | .IP "Info" 4 | |
181 | .IX Item "Info" | |
182 | Prints statistical information on a \s-1BDD\s0 manager. | |
183 | .IP "PeakLiveNodes" 4 | |
184 | .IX Item "PeakLiveNodes" | |
185 | Returns the peak number of live nodes in the manager. | |
186 | .IP "LiveNodes" 4 | |
187 | .IX Item "LiveNodes" | |
188 | Returns the number of live nodes in the manager. | |
189 | .IP "DynReorderingStatus" 4 | |
190 | .IX Item "DynReorderingStatus" | |
191 | Returns a list with two elements. The first is 1 if reordering is | |
192 | currently enabled and 0 otherwise; the second is the reordering method | |
193 | currently selected. | |
194 | .Sh "" | |
195 | .IX Subsection "" | |
196 | The second package in module Cudd is Cudd::BDD. It defines methods | |
197 | that manipulate BDDs. Starting with a set of variables belonging to a | |
198 | manager, the functions in this package allow one to create BDDs for | |
199 | arbitrary functions over those variables. These are the methods | |
200 | defined by Cudd::BDD: | |
201 | .IP "One" 4 | |
202 | .IX Item "One" | |
203 | Returns the constant 1 \s-1BDD\s0 from the manager of \f(CW$f\fR. | |
204 | .IP "Zero" 4 | |
205 | .IX Item "Zero" | |
206 | Returns the constant 0 \s-1BDD\s0 from the manager of \f(CW$f\fR. | |
207 | .IP "And" 4 | |
208 | .IX Item "And" | |
209 | Computes the conjunction of two BDDs. Overloads '*'. | |
210 | .IP "Or" 4 | |
211 | .IX Item "Or" | |
212 | Computes the disjunction of two BDDs. Overloads '+'. | |
213 | .IP "Xor" 4 | |
214 | .IX Item "Xor" | |
215 | Computes the exclusive or of two BDDs. Overloads '^'. | |
216 | .IP "Nand" 4 | |
217 | .IX Item "Nand" | |
218 | Computes the \s-1NAND\s0 of two BDDs. | |
219 | .IP "Nor" 4 | |
220 | .IX Item "Nor" | |
221 | Computes the \s-1NOR\s0 of two BDDs. | |
222 | .IP "Cofactor" 4 | |
223 | .IX Item "Cofactor" | |
224 | Computes the cofactor of a \s-1BDD\s0 with respect to another. Uses the constrain | |
225 | algorithm. Overloads '/'. | |
226 | .IP "Restrict" 4 | |
227 | .IX Item "Restrict" | |
228 | Computes the cofactor of a \s-1BDD\s0 with respect to another. Uses the restrict | |
229 | algorithm. | |
230 | .IP "Squeeze" 4 | |
231 | .IX Item "Squeeze" | |
232 | Finds a small \s-1BDD\s0 in an interval. | |
233 | .IP "Exists" 4 | |
234 | .IX Item "Exists" | |
235 | Existentially quantifies the variables in a cube from a \s-1BDD\s0. | |
236 | .IP "Forall" 4 | |
237 | .IX Item "Forall" | |
238 | Universally quantifies the variables in a cube from a \s-1BDD\s0. | |
239 | .IP "AndExists" 4 | |
240 | .IX Item "AndExists" | |
241 | Existentially quantifies the variables in a cube from the conjunction of | |
242 | two BDDs. | |
243 | .IP "Compose" 4 | |
244 | .IX Item "Compose" | |
245 | Composes a \s-1BDD\s0 \f(CW$g\fR into a \s-1BDD\s0 \f(CW$f\fR substituting variable \f(CW$var\fR. | |
246 | .IP "BooleanDiff" 4 | |
247 | .IX Item "BooleanDiff" | |
248 | Computes the boolean difference of a \s-1BDD\s0 with respect to one variable. | |
249 | .IP "Correlation" 4 | |
250 | .IX Item "Correlation" | |
251 | Computes the correlation of two BDDs. The result is a number between 0 | |
252 | and 1. A value of 1 indicates that the functions \f(CW$f\fR and \f(CW$g\fR are | |
253 | identical. A value of 0 indicates that they are complementary. | |
254 | .IP "Decreasing" 4 | |
255 | .IX Item "Decreasing" | |
256 | Returns 1 if the \s-1BDD\s0 \f(CW$f\fR is monotonic decreasing (negative unate) in | |
257 | variable \f(CW$var\fR; 0 otherwise. | |
258 | .IP "Increasing" 4 | |
259 | .IX Item "Increasing" | |
260 | Returns 1 if the \s-1BDD\s0 \f(CW$f\fR is monotonic increasing (positive unate) in | |
261 | variable \f(CW$var\fR; 0 otherwise. | |
262 | .IP "Essentials" 4 | |
263 | .IX Item "Essentials" | |
264 | Finds the essential variables of a \s-1BDD\s0. Returns an array of all essentials. | |
265 | Negative essentials correspond to negative literals. | |
266 | .IP "Support" 4 | |
267 | .IX Item "Support" | |
268 | Returns a cube of all the variables in the support of \f(CW$f\fR. | |
269 | .IP "LiteralSetIntersection" 4 | |
270 | .IX Item "LiteralSetIntersection" | |
271 | Computes the intersection of two literal sets represented by cube BDDs. | |
272 | .IP "SwapVariables" 4 | |
273 | .IX Item "SwapVariables" | |
274 | Swaps two sets of variables in a \s-1BDD\s0. | |
275 | .IP "SolveEqn" 4 | |
276 | .IX Item "SolveEqn" | |
277 | Solves a boolean equation. The first argument \f(CW$f\fR is the left-hand side | |
278 | of the equation \f(CW$f\fR = 0. The second argument is a reference to the | |
279 | array of the unknowns. The variables that are not unknowns are | |
280 | parameters. | |
281 | .IP "Signatures" 4 | |
282 | .IX Item "Signatures" | |
283 | Computes the variable signatures in a \s-1BDD\s0. The signature of a variable | |
284 | is the fraction of minterms in the on-set of the cofactor w.r.t. to | |
285 | that variable. The function returns an array of as many signatures as | |
286 | there are variables plus one. The last element of the array is the | |
287 | fraction of minterms in the ON-set of the \s-1BDD\s0, and can be used to | |
288 | normalize the variable signatures. | |
289 | .IP "NormSignatures" 4 | |
290 | .IX Item "NormSignatures" | |
291 | Returns signatures normalized between 0 and 2. See also Signatures. | |
292 | .IP "SubsetHB" 4 | |
293 | .IX Item "SubsetHB" | |
294 | Computes a subset of a \s-1BDD\s0 with a maximum number of nodes. Uses the | |
295 | heavy branch approach. | |
296 | .IP "SubsetSP" 4 | |
297 | .IX Item "SubsetSP" | |
298 | Computes a subset of a \s-1BDD\s0 with a maximum number of nodes. Uses the | |
299 | short paths approach. | |
300 | .IP "SupersetHB" 4 | |
301 | .IX Item "SupersetHB" | |
302 | Computes a superset of a \s-1BDD\s0 with a maximum number of nodes. Uses the | |
303 | heavy branch approach. | |
304 | .IP "SupersetSP" 4 | |
305 | .IX Item "SupersetSP" | |
306 | Computes a superset of a \s-1BDD\s0 with a maximum number of nodes. Uses the | |
307 | short paths approach. | |
308 | .IP "NewAdjVar" 4 | |
309 | .IX Item "NewAdjVar" | |
310 | Creates a new variable adjacent to the given variable. Useful in creating the next state variables of FSMs. | |
311 | .IP "GroupVars" 4 | |
312 | .IX Item "GroupVars" | |
313 | Creates a group of variables to be kept adjacent during reordering. | |
314 | .IP "Not" 4 | |
315 | .IX Item "Not" | |
316 | Returns the complement of a \s-1BDD\s0. Overloads '!'. | |
317 | .IP "Equal" 4 | |
318 | .IX Item "Equal" | |
319 | Returns 1 if the two arguments are equivalent; 0 otherwise. Overloads '=='. | |
320 | .IP "Unequal" 4 | |
321 | .IX Item "Unequal" | |
322 | Returns 1 if the two arguments are not equivalent; 0 otherwise. Overloads '!='. | |
323 | .IP "Leq" 4 | |
324 | .IX Item "Leq" | |
325 | 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. | |
326 | Overloads '<='. | |
327 | .IP "Geq" 4 | |
328 | .IX Item "Geq" | |
329 | 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. | |
330 | Overloads '>='. | |
331 | .IP "IsComplement" 4 | |
332 | .IX Item "IsComplement" | |
333 | 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. | |
334 | .IP "ShortestPath" 4 | |
335 | .IX Item "ShortestPath" | |
336 | Computes a shortest path in a \s-1BDD\s0. | |
337 | .IP "Size" 4 | |
338 | .IX Item "Size" | |
339 | Returns the number of nodes in the \s-1BDD\s0 or BDDs passed as arguments. | |
340 | .IP "Minterms" 4 | |
341 | .IX Item "Minterms" | |
342 | Returns the number of minterms of the \s-1BDD\s0. The function of the \s-1BDD\s0 is | |
343 | supposed to depend on \f(CW$n\fR variables. | |
344 | .IP "Print" 4 | |
345 | .IX Item "Print" | |
346 | Prints information about a \s-1BDD\s0 \f(CW$f\fR. The \f(CW$pr\fR parameter controls how much | |
347 | information is printed. The \f(CW$n\fR parameter specifies how many inputs \f(CW$f\fR depends | |
348 | on. This information is necessary to compute the number of minterms. | |
349 | .IP "Dot" 4 | |
350 | .IX Item "Dot" | |
351 | Prints a description of a set of BDDs in dot format. The function has | |
352 | one mandatory parameter, the list of BDDs for which the dot | |
353 | description is desired, and two optional parameters, the array of | |
354 | input names and the array of output names. All parameters are array | |
355 | references. If the input names are omitted but the output names are | |
356 | not, a reference to an empty array ([]) should be passed for the input | |
357 | names. | |
358 | .IP "Intersect" 4 | |
359 | .IX Item "Intersect" | |
360 | Computes a function included in the intersection of \f(CW$f\fR and \f(CW$g\fR. (That | |
361 | is, a witness that the intersection is not empty.) Intersect tries to | |
362 | build as few new nodes as possible. | |
363 | .IP "ConstrainDecomp" 4 | |
364 | .IX Item "ConstrainDecomp" | |
365 | \&\s-1BDD\s0 conjunctive decomposition as in the \s-1CAV96\s0 paper by McMillan. The | |
366 | decomposition is canonical only for a given variable order. If | |
367 | canonicity is required, variable ordering must be disabled after the | |
368 | decomposition has been computed. Returns an array with one entry for | |
369 | each \s-1BDD\s0 variable. | |
370 | .IP "CharToVect" 4 | |
371 | .IX Item "CharToVect" | |
372 | Computes a vector of functions such that their image equals a non-zero | |
373 | function. Returns an array with one entry for each \s-1BDD\s0 variable. | |
374 | .IP "PrioritySelect" 4 | |
375 | .IX Item "PrioritySelect" | |
376 | Selects pairs from a relation \f(CW\*(C`R(x,y)\*(C'\fR (given as a \s-1BDD\s0) | |
377 | in such a way that a given x appears in one pair only. Uses a | |
378 | priority function to determine which y should be paired to a given x. | |
379 | .IP "PiDxygtdxz" 4 | |
380 | .IX Item "PiDxygtdxz" | |
381 | Returns the priority function that is 1 if the distance of x from y is greater than the distance of x from z. | |
382 | .IP "PiDxygtdyz" 4 | |
383 | .IX Item "PiDxygtdyz" | |
384 | Returns the priority function that is 1 if the distance of x from y is greater than the distance of y from z. | |
385 | .IP "PiXgty" 4 | |
386 | .IX Item "PiXgty" | |
387 | Returns the priority function that is 1 if x is greater than y. | |
388 | .IP "CProjection" 4 | |
389 | .IX Item "CProjection" | |
390 | Applies the C\-Projection to a relation R. | |
391 | .IP "Shuffle" 4 | |
392 | .IX Item "Shuffle" | |
393 | Imposes a given order. | |
394 | .PP | |
395 | Package Cudd:BDD overloads common operators as follows: | |
396 | .PP | |
397 | \&\f(CW\*(C`+ \*(C'\fR \-> Or | |
398 | .PP | |
399 | \&\f(CW\*(C`* \*(C'\fR \-> And | |
400 | .PP | |
401 | \&\f(CW\*(C`^ \*(C'\fR \-> Xor | |
402 | .PP | |
403 | \&\f(CW\*(C`! \*(C'\fR \-> Not | |
404 | .PP | |
405 | \&\f(CW\*(C`/ \*(C'\fR \-> Cofactor | |
406 | .PP | |
407 | \&\f(CW\*(C`==\*(C'\fR \-> Equal | |
408 | .PP | |
409 | \&\f(CW\*(C`!=\*(C'\fR \-> Unequal | |
410 | .PP | |
411 | \&\f(CW\*(C`<=\*(C'\fR \-> Leq | |
412 | .PP | |
413 | \&\f(CW\*(C`>=\*(C'\fR \-> Geq | |
414 | .SH "EXAMPLE" | |
415 | .IX Header "EXAMPLE" | |
416 | The following code fragment creates a manager, two variables \f(CW$x\fR and | |
417 | \&\f(CW$y\fR in it, and then builds and prints the conjunction of the two | |
418 | variables. | |
419 | .PP | |
420 | .Vb 5 | |
421 | \& my $manager = new Cudd; | |
422 | \& my $x = $manager->BddVar; | |
423 | \& my $y = $manager->BddVar; | |
424 | \& my $z = $x * $y; | |
425 | \& $z->Print(2,1); # (2 variables, verbosity 1) | |
426 | .Ve | |
427 | .SH "AUTHOR" | |
428 | .IX Header "AUTHOR" | |
429 | Fabio Somenzi, Fabio@Colorado.EDU | |
430 | .SH "SEE ALSO" | |
431 | .IX Header "SEE ALSO" | |
432 | \&\fIperl\fR\|(1). |