emergency commit
[cl-cudd.git] / distr / cudd / doc / node3.html
blobbb0e9ae238f3ad8b294cd8d2f44979ab4d5e9ba0
1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
3 <!--Converted with jLaTeX2HTML 2002-2-1 (1.70) JA patch-2.0
4 patched version by: Kenshi Muto, Debian Project.
5 * modified by: Shige TAKENO
6 LaTeX2HTML 2002-2-1 (1.70),
7 original version by: Nikos Drakos, CBLU, University of Leeds
8 * revised and updated by: Marcus Hennecke, Ross Moore, Herb Swan
9 * with significant contributions from:
10 Jens Lippmann, Marek Rouchal, Martin Wilck and others -->
11 <HTML>
12 <HEAD>
13 <TITLE>User's Manual</TITLE>
14 <META NAME="description" CONTENT="User's Manual">
15 <META NAME="keywords" CONTENT="cuddIntro">
16 <META NAME="resource-type" CONTENT="document">
17 <META NAME="distribution" CONTENT="global">
19 <META NAME="Generator" CONTENT="jLaTeX2HTML v2002-2-1 JA patch-2.0">
20 <META HTTP-EQUIV="Content-Style-Type" CONTENT="text/css">
22 <LINK REL="STYLESHEET" HREF="cuddIntro.css">
24 <LINK REL="next" HREF="node4.html">
25 <LINK REL="previous" HREF="node2.html">
26 <LINK REL="up" HREF="cuddIntro.html">
27 <LINK REL="next" HREF="node4.html">
28 </HEAD>
30 <BODY >
31 <!--Navigation Panel-->
32 <A NAME="tex2html111"
33 HREF="node4.html">
34 <IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
35 SRC="icons/next.png"></A>
36 <A NAME="tex2html107"
37 HREF="cuddIntro.html">
38 <IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
39 SRC="icons/up.png"></A>
40 <A NAME="tex2html101"
41 HREF="node2.html">
42 <IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
43 SRC="icons/prev.png"></A>
44 <A NAME="tex2html109"
45 HREF="node8.html">
46 <IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
47 SRC="icons/index.png"></A>
48 <BR>
49 <B> Next:</B> <A NAME="tex2html112"
50 HREF="node4.html">Programmer's Manual</A>
51 <B> Up:</B> <A NAME="tex2html108"
52 HREF="cuddIntro.html">CUDD: CU Decision Diagram</A>
53 <B> Previous:</B> <A NAME="tex2html102"
54 HREF="node2.html">How to Get CUDD</A>
55 &nbsp; <B> <A NAME="tex2html110"
56 HREF="node8.html">Index</A></B>
57 <BR>
58 <BR>
59 <!--End of Navigation Panel-->
60 <!--Table of Child-Links-->
61 <A NAME="CHILD_LINKS"><STRONG>Subsections</STRONG></A>
63 <UL>
64 <LI><A NAME="tex2html113"
65 HREF="node3.html#SECTION00031000000000000000">Compiling and Linking</A>
66 <LI><A NAME="tex2html114"
67 HREF="node3.html#SECTION00032000000000000000">Basic Data Structures</A>
68 <UL>
69 <LI><A NAME="tex2html115"
70 HREF="node3.html#SECTION00032100000000000000">Nodes</A>
71 <LI><A NAME="tex2html116"
72 HREF="node3.html#SECTION00032200000000000000">The Manager</A>
73 <LI><A NAME="tex2html117"
74 HREF="node3.html#SECTION00032300000000000000">Cache</A>
75 </UL>
76 <BR>
77 <LI><A NAME="tex2html118"
78 HREF="node3.html#SECTION00033000000000000000">Initializing and Shutting Down a DdManager</A>
79 <LI><A NAME="tex2html119"
80 HREF="node3.html#SECTION00034000000000000000">Setting Parameters</A>
81 <LI><A NAME="tex2html120"
82 HREF="node3.html#SECTION00035000000000000000">Constant Functions</A>
83 <UL>
84 <LI><A NAME="tex2html121"
85 HREF="node3.html#SECTION00035100000000000000">One, Logic Zero, and Arithmetic Zero</A>
86 <LI><A NAME="tex2html122"
87 HREF="node3.html#SECTION00035200000000000000">Predefined Constants</A>
88 <LI><A NAME="tex2html123"
89 HREF="node3.html#SECTION00035300000000000000">Background</A>
90 <LI><A NAME="tex2html124"
91 HREF="node3.html#SECTION00035400000000000000">New Constants</A>
92 </UL>
93 <BR>
94 <LI><A NAME="tex2html125"
95 HREF="node3.html#SECTION00036000000000000000">Creating Variables</A>
96 <UL>
97 <LI><A NAME="tex2html126"
98 HREF="node3.html#SECTION00036100000000000000">New BDD and ADD Variables</A>
99 <LI><A NAME="tex2html127"
100 HREF="node3.html#SECTION00036200000000000000">New ZDD Variables</A>
101 </UL>
102 <BR>
103 <LI><A NAME="tex2html128"
104 HREF="node3.html#SECTION00037000000000000000">Basic BDD Manipulation</A>
105 <LI><A NAME="tex2html129"
106 HREF="node3.html#SECTION00038000000000000000">Basic ADD Manipulation</A>
107 <LI><A NAME="tex2html130"
108 HREF="node3.html#SECTION00039000000000000000">Basic ZDD Manipulation</A>
109 <LI><A NAME="tex2html131"
110 HREF="node3.html#SECTION000310000000000000000">Converting ADDs to BDDs and Vice Versa</A>
111 <LI><A NAME="tex2html132"
112 HREF="node3.html#SECTION000311000000000000000">Converting BDDs to ZDDs and Vice Versa</A>
113 <LI><A NAME="tex2html133"
114 HREF="node3.html#SECTION000312000000000000000">Variable Reordering for BDDs and ADDs</A>
115 <LI><A NAME="tex2html134"
116 HREF="node3.html#SECTION000313000000000000000">Grouping Variables</A>
117 <LI><A NAME="tex2html135"
118 HREF="node3.html#SECTION000314000000000000000">Variable Reordering for ZDDs</A>
119 <LI><A NAME="tex2html136"
120 HREF="node3.html#SECTION000315000000000000000">Keeping Consistent Variable Orders for BDDs and ZDDs</A>
121 <LI><A NAME="tex2html137"
122 HREF="node3.html#SECTION000316000000000000000">Hooks</A>
123 <LI><A NAME="tex2html138"
124 HREF="node3.html#SECTION000317000000000000000">The SIS/VIS Interface</A>
125 <UL>
126 <LI><A NAME="tex2html139"
127 HREF="node3.html#SECTION000317100000000000000">Using the CUDD Package in SIS</A>
128 </UL>
129 <BR>
130 <LI><A NAME="tex2html140"
131 HREF="node3.html#SECTION000318000000000000000">Writing Decision Diagrams to a File</A>
132 <LI><A NAME="tex2html141"
133 HREF="node3.html#SECTION000319000000000000000">Saving and Restoring BDDs</A>
134 </UL>
135 <!--End of Table of Child-Links-->
136 <HR>
138 <H1><A NAME="SECTION00030000000000000000"></A>
139 <A NAME="sec:user"></A>
140 <BR>
141 User's Manual
142 </H1>
145 This section describes the use of the CUDD package as a black box.
149 <H2><A NAME="SECTION00031000000000000000"></A>
150 <A NAME="sec:compileExt"></A><A NAME="79"></A>
151 <BR>
152 Compiling and Linking
153 </H2>
156 To build an application that uses the CUDD package, you should add
157 <PRE>
158 #include "util.h"
159 #include "cudd.h"
160 </PRE>
161 <A NAME="82"></A>
162 to your source files, and should link
163 <code>libcudd.a</code><A NAME="83"></A>,
164 <code>libmtr.a</code><A NAME="84"></A>,
165 <code>libst.a</code><A NAME="85"></A>, and
166 <code>libutil.a</code><A NAME="86"></A> to your executable. (All these
167 libraries are part of the distribution.) Some
168 platforms require specific compiler and linker flags. Refer to the
169 <TT>Makefile<A NAME="87"></A></TT> in the top level directory of the
170 distribution.
173 Keep in mind that whatever flags affect the size of data
174 structures--for instance the flags used to use 64-bit pointers where
175 available--must be specified when compiling both CUDD and the files
176 that include its header files.
180 <H2><A NAME="SECTION00032000000000000000"></A>
181 <A NAME="sec:struct"></A>
182 <BR>
183 Basic Data Structures
184 </H2>
188 <H3><A NAME="SECTION00032100000000000000"></A>
189 <A NAME="sec:nodes"></A>
190 <BR>
191 Nodes
192 </H3>
195 BDDs, ADDs, and ZDDs are made of DdNode's. A DdNode<A NAME="92"></A>
196 (node<A NAME="93"></A> for short) is a structure with several fields. Those
197 that are of interest to the application that uses the CUDD package as
198 a black box are the variable index<A NAME="94"></A>, the
199 reference<A NAME="95"></A> count, and the value. The
200 remaining fields are pointers that connect nodes among themselves and
201 that are used to implement the unique<A NAME="96"></A> table. (See
202 Section&nbsp;<A HREF="#sec:manager">3.2.2</A>.)
205 The <I>index</I> field holds the name of the variable that labels the
206 node. The index of a variable is a permanent attribute that reflects
207 the order<A NAME="99"></A> of creation. Index 0 corresponds to
208 the variable created first. On a machine with 32-bit pointers, the
209 maximum number of variables is the largest value that can be stored in
210 an unsigned short integer minus 1. The largest index is reserved for
211 the constant<A NAME="100"></A> nodes. When 64-bit pointers are
212 used, the maximum number of variables is the largest value that can be
213 stored in an unsigned integer minus 1.
216 When variables are reordered to reduce the size of the decision
217 diagrams, the variables may shift in the order, but they retain their
218 indices. The package keeps track of the variable
219 permutation<A NAME="101"></A> (and its inverse). The
220 application is not affected by variable reordering<A NAME="102"></A>,
221 except in the following cases.
223 <UL>
224 <LI>If the application uses generators<A NAME="104"></A>
225 (<I>Cudd_ForeachCube</I> <A NAME="1101"></A> and
226 <I>Cudd_ForeachNode</I><A NAME="1103"></A>) and reordering is
227 enabled, then it must take care not to call any operation that may
228 create new nodes (and hence possibly trigger reordering). This is
229 because the cubes (i.e., paths) and nodes of a diagram change as a
230 result of reordering.
231 </LI>
232 <LI>If the application uses
233 <I>Cudd_bddConstrain</I><A NAME="1105"></A> and reordering
234 takes place, then the property of <I>Cudd_bddConstrain</I> of
235 being an image restrictor is lost.
236 </LI>
237 </UL>
240 The CUDD package relies on garbage<A NAME="113"></A>
241 collection to reclaim the memory used by diagrams that are no longer
242 in use. The scheme employed for garbage collection is based on keeping
243 a reference<A NAME="114"></A> count for each node. The
244 references that are counted are both the internal references
245 (references from other nodes) and external references (typically
246 references from the calling environment). When an application creates
247 a new BDD<A NAME="115"></A>, ADD<A NAME="116"></A>, or ZDD<A NAME="117"></A>, it must
248 increase its reference count explicitly, through a call to
249 <I>Cudd_Ref</I><A NAME="1107"></A>. Similarly, when a diagram is no
250 longer needed, the application must call
251 <I>Cudd_RecursiveDeref</I><A NAME="1109"></A> (for BDDs and
252 ADDs) or <I>Cudd_RecursiveDerefZdd</I><A NAME="1111"></A>
253 (for ZDDs) to ``recycle<A NAME="124"></A>'' the nodes of the
254 diagram.
257 Terminal<A NAME="125"></A> nodes carry a value. This is especially
258 important for ADDs. By default, the value is a double<A NAME="126"></A>.
259 To change to something different (e.g., an integer), the
260 package must be modified and recompiled. Support for this process is
261 currently very rudimentary.
265 <H3><A NAME="SECTION00032200000000000000"></A>
266 <A NAME="128"></A><A NAME="sec:manager"></A>
267 <BR>
268 The Manager
269 </H3>
272 All nodes used in BDDs, ADDs, and ZDDs are kept in special
273 hash<A NAME="130"></A> tables called the
274 <I>unique<A NAME="131"></A> tables</I>. Specifically, BDDs and ADDs
275 share the same unique table, whereas ZDDs have their own table. As
276 the name implies, the main purpose of the unique table is to guarantee
277 that each node is unique; that is, there is no other node labeled by
278 the same variable and with the same children. This uniqueness
279 property makes decision diagrams canonical<A NAME="132"></A>. The
280 unique<A NAME="133"></A> tables and some auxiliary data structures
281 make up the DdManager<A NAME="134"></A> (manager<A NAME="135"></A> for
282 short). Though the application that uses only the exported functions
283 needs not be concerned with most details of the manager, it has to
284 deal with the manager in the following sense. The application must
285 initialize the manager by calling an appropriate function. (See
286 Section&nbsp;<A HREF="#sec:init">3.3</A>.) Subsequently, it must pass a pointer to the
287 manager to all the functions that operate on decision diagrams.
290 With the exception of a few statistical counters<A NAME="137"></A>, there are no global<A NAME="138"></A> variables in
291 the CUDD package. Therefore, it is quite possible to have multiple
292 managers simultaneously active in the same application.<A NAME="tex2html3"
293 HREF="footnode.html#foot139"><SUP>1</SUP></A> It is the pointers to
294 the managers that tell the functions on what data they should operate.
298 <H3><A NAME="SECTION00032300000000000000"></A>
299 <A NAME="141"></A><A NAME="sec:memoize"></A>
300 <BR>
301 Cache
302 </H3>
305 Efficient recursive manipulation of decision diagrams requires the use
306 of a table to store computed results. This table<A NAME="143"></A>
307 is called here the <I>cache<A NAME="144"></A></I> because it is
308 effectively handled like a cache of variable but limited capacity. The
309 CUDD package starts by default with a small cache, and increases its
310 size until either no further benefit is achieved, or a limit size is
311 reached. The user can influence this policy by choosing initial and
312 limit values for the cache size.
315 Too small a cache will cause frequent overwriting of useful results.
316 Too large a cache will cause overhead, because the whole cache is
317 scanned every time garbage<A NAME="145"></A> collection takes
318 place. The optimal parameters depend on the specific application. The
319 default parameters work reasonably well for a large spectrum of
320 applications.
323 The cache<A NAME="146"></A> of the CUDD package is used by most recursive
324 functions of the package, and can be used by user-supplied functions
325 as well. (See Section&nbsp;<A HREF="node4.html#sec:cache">4.4</A>.)
329 <H2><A NAME="SECTION00033000000000000000"></A>
330 <A NAME="149"></A><A NAME="sec:init"></A>
331 <BR>
332 Initializing and Shutting Down a DdManager
333 </H2>
336 To use the functions in the CUDD package, one has first to initialize
337 the package itself by calling <I>Cudd_Init</I><A NAME="1113"></A>.
338 This function takes four parameters:
340 <UL>
341 <LI>numVars<A NAME="154"></A>: It is the initial number of variables
342 for BDDs and ADDs. If the total number of variables needed by the
343 application is known, then it is slightly more efficient to create a
344 manager with that number of variables. If the number is unknown, it
345 can be set to 0, or to any other lower bound on the number of
346 variables. Requesting more variables than are actually needed is
347 not incorrect, but is not efficient.
348 </LI>
349 <LI>numVarsZ<A NAME="155"></A>: It is the initial number of variables
350 for ZDDs. See Sections&nbsp;<A HREF="#sec:basicZDD">3.9</A> and&nbsp;<A HREF="#sec:convertZ">3.11</A> for
351 a discussion of the value of this argument.
352 </LI>
353 <LI>numSlots<A NAME="158"></A>: Determines the initial size of each
354 subtable<A NAME="159"></A> of the unique<A NAME="160"></A> table.
355 There is a subtable for each variable. The size of each subtable is
356 dynamically adjusted to reflect the number of nodes. It is normally
357 O.K. to use the default value for this parameter, which is
358 CUDD_UNIQUE_SLOTS<A NAME="161"></A>.
359 </LI>
360 <LI>cacheSize<A NAME="162"></A>: It is the initial size (number of
361 entries) of the cache<A NAME="163"></A>. Its default value is
362 CUDD_CACHE_SLOTS<A NAME="164"></A>.
363 </LI>
364 <LI>maxMemory<A NAME="165"></A>: It is the target value for the
365 maximum memory occupation (in bytes). The package uses this value to
366 decide two parameters.
368 <UL>
369 <LI>the maximum size to which the cache will grow, regardless of
370 the hit rate or the size of the unique<A NAME="167"></A> table.
371 </LI>
372 <LI>the maximum size to which growth of the unique table will be
373 preferred to garbage collection.
375 </LI>
376 </UL>
377 If maxMemory is set to 0, CUDD tries to guess a good value based on
378 the available memory.
379 </LI>
380 </UL>
381 A typical call to <I>Cudd_Init</I><A NAME="1115"></A> may look
382 like this:
383 <PRE>
384 manager = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);
385 </PRE>
386 To reclaim all the memory associated with a manager, an application
387 must call <I>Cudd_Quit</I><A NAME="1117"></A>. This is normally
388 done before exiting.
392 <H2><A NAME="SECTION00034000000000000000"></A>
393 <A NAME="sec:params"></A>
394 <BR>
395 Setting Parameters
396 </H2>
399 The package provides several functions to set the parameters that
400 control various functions. For instance, the package has an automatic
401 way of determining whether a larger unique<A NAME="178"></A> table
402 would make the application run faster. In that case, the package
403 enters a ``fast growth<A NAME="179"></A>'' mode in which resizing of
404 the unique subtables is favored over garbage<A NAME="180"></A>
405 collection. When the unique table reaches a given size, however, the
406 package returns to the normal ``slow growth'' mode, even though the
407 conditions that caused the transition to fast growth still prevail.
408 The limit size for fast growth<A NAME="181"></A> can be read by
409 <I>Cudd_ReadLooseUpTo</I><A NAME="1119"></A> and changed by
410 <I>Cudd_SetLooseUpTo</I><A NAME="1121"></A>. Similar pairs of
411 functions exist for several other parameters. See also
412 Section&nbsp;<A HREF="node4.html#sec:stats">4.8</A>.
416 <H2><A NAME="SECTION00035000000000000000"></A>
417 <A NAME="188"></A><A NAME="sec:const"></A>
418 <BR>
419 Constant Functions
420 </H2>
423 The CUDD Package defines several constant functions. These functions
424 are created when the manager<A NAME="190"></A> is initialized, and are accessible
425 through the manager itself.
429 <H3><A NAME="SECTION00035100000000000000"></A>
430 <A NAME="192"></A><A NAME="193"></A><A NAME="sec:zero"></A>
431 <BR>
432 One, Logic Zero, and Arithmetic Zero
433 </H3>
436 The constant<A NAME="195"></A> 1 (returned by
437 <I>Cudd_ReadOne</I><A NAME="1123"></A>) is common to BDDs, ADDs, and
438 ZDDs. However, its meaning is different for ADDs and BDDs, on the one
439 hand, and ZDDs, on the other hand. The diagram consisting of the
440 constant 1 node only represents the constant 1 function for ADDs and
441 BDDs. For ZDDs, its meaning depends on the number of variables: It is
442 the conjunction of the complements of all variables. Conversely, the
443 representation of the constant 1 function depends on the number of
444 variables. The constant 1 function of <IMG
445 WIDTH="15" HEIGHT="15" ALIGN="BOTTOM" BORDER="0"
446 SRC="img4.png"
447 ALT="$n$"> variables is returned by
448 <I>Cudd_ReadZddOne</I><A NAME="1125"></A>.
451 The constant 0 is common to ADDs and ZDDs, but not to BDDs. The
452 BDD<A NAME="200"></A> logic 0 is <B>not</B> associated with the constant 0
453 function: It is obtained by complementation
454 (<I>Cudd_Not</I><A NAME="1127"></A>) of the constant 1. (It is also
455 returned by <I>Cudd_ReadLogicZero</I><A NAME="1129"></A>.)
456 All other constants are specific to ADDs.
460 <H3><A NAME="SECTION00035200000000000000"></A>
461 <A NAME="sec:predef-const"></A>
462 <BR>
463 Predefined Constants
464 </H3>
467 Besides 0 (returned by <I>Cudd_ReadZero</I><A NAME="1131"></A>)
468 and 1, the following constant<A NAME="210"></A> functions are
469 created at initialization time.
471 <OL>
472 <LI>PlusInfinity<A NAME="212"></A> and
473 MinusInfinity<A NAME="213"></A>: On computers implementing the
474 IEEE<A NAME="214"></A> standard 754 for
475 floating-point<A NAME="215"></A> arithmetic, these two constants
476 are set to the signed infinities<A NAME="216"></A>. On the DEC
477 Alphas<A NAME="217"></A>, the option <code>-ieee_with_no_inexact</code> or
478 <code>-ieee_with_inexact</code> must be passed to the DEC compiler to get
479 support of the IEEE standard. (The compiler still produces a
480 warning, but it can be ignored.) Compiling<A NAME="218"></A> with
481 those options may cause substantial performance degradation on the
482 Evolution IV CPUs. (Especially if the application does use the
483 infinities.) The problem is reportedly solved in the Evolution V
484 CPUs. If <TT>gcc<A NAME="219"></A></TT> is used to compile CUDD on the
485 Alphas, the symbol <TT>HAVE_IEEE_754<A NAME="220"></A></TT>
486 must be undefined. (See the Makefile<A NAME="221"></A> for the
487 details.) The values of these constants are returned by
488 <I>Cudd_ReadPlusInfinity</I><A NAME="1133"></A> and
489 <I>Cudd_ReadMinusInfinity</I><A NAME="1135"></A>.
490 </LI>
491 <LI>Epsilon<A NAME="226"></A>: This constant, initially set to
492 <IMG
493 WIDTH="47" HEIGHT="18" ALIGN="BOTTOM" BORDER="0"
494 SRC="img5.png"
495 ALT="$10^{-12}$">, is used in comparing floating point values for equality.
496 Its value is returned by
497 <I>Cudd_ReadEpsilon</I><A NAME="1137"></A>, and it can be
498 modified by calling <I>Cudd_SetEpsilon</I><A NAME="1139"></A>.
499 Unlike the other constants, it does not correspond to a node.
500 </LI>
501 </OL>
505 <H3><A NAME="SECTION00035300000000000000"></A>
506 <A NAME="234"></A><A NAME="sec:background"></A>
507 <BR>
508 Background
509 </H3>
512 The background value is a constant<A NAME="236"></A> typically used
513 to represent non-existing arcs in graphs. Consider a shortest path
514 problem. Two nodes that are not connected by an arc can be regarded as
515 being joined by an arc<A NAME="237"></A> of infinite length. In
516 shortest path problems, it is therefore convenient to set the
517 background value to PlusInfinity<A NAME="238"></A>. In network flow
518 problems, on the other hand, two nodes not connected by an arc can be
519 regarded as joined by an arc<A NAME="239"></A> of 0 capacity.
520 For these problems, therefore, it is more convenient to set the
521 background value to 0. In general, when representing
522 sparse<A NAME="240"></A> matrices, the background value is the value that
523 is assumed implicitly.
526 At initialization, the background value is set to 0. It can be read
527 with <I>Cudd_ReadBackground</I><A NAME="1141"></A>, and
528 modified with <I>Cudd_SetBackground</I>. The background value
529 affects procedures that read sparse matrices/graphs
530 (<I>Cudd_addRead</I><A NAME="1143"></A> and
531 <I>Cudd_addHarwell</I><A NAME="1145"></A>), procedures that print
532 out sum-of-product<A NAME="248"></A> expressions for
533 ADDs (<I>Cudd_PrintMinterm</I><A NAME="1147"></A>), generators
534 of cubes (<I>Cudd_ForeachCube</I><A NAME="1149"></A>), and
535 procedures that count minterms<A NAME="253"></A>
536 (<I>Cudd_CountMinterm</I><A NAME="1151"></A>).
540 <H3><A NAME="SECTION00035400000000000000"></A>
541 <A NAME="sec:newconst"></A>
542 <BR>
543 New Constants
544 </H3>
547 New constant<A NAME="258"></A> can be created by calling
548 <I>Cudd_addConst</I><A NAME="1153"></A>. This function will
549 retrieve the ADD<A NAME="261"></A> for the desired constant, if it already
550 exist, or it will create a new one. Obviously, new constants should
551 only be used when manipulating ADDs.
555 <H2><A NAME="SECTION00036000000000000000"></A>
556 <A NAME="sec:newvar"></A>
557 <BR>
558 Creating Variables
559 </H2>
562 Decision diagrams are typically created by combining simpler decision
563 diagrams. The simplest decision diagrams, of course, cannot be
564 created in that way. Constant functions have been discussed in
565 Section&nbsp;<A HREF="#sec:const">3.5</A>. In this section we discuss the simple
566 variable functions, also known as <I>projection<A NAME="265"></A> functions</I>.
570 <H3><A NAME="SECTION00036100000000000000"></A>
571 <A NAME="sec:BDDADDvar"></A>
572 <BR>
573 New BDD and ADD Variables
574 </H3>
577 The projection<A NAME="268"></A> functions are distinct for
578 BDDs and ADDs. A projection function for BDDs consists of an internal
579 node with both outgoing arcs pointing to the constant 1. The
580 <I>else</I> arc<A NAME="270"></A> is complemented.
583 An ADD projection function, on the other hand, has the <I>else</I>
584 pointer directed to the arithmetic<A NAME="272"></A> zero
585 function. One should never mix the two types of variables. BDD
586 variables should be used when manipulating BDDs, and ADD variables
587 should be used when manipulating ADDs. Three functions are provided
588 to create BDD variables:
590 <UL>
591 <LI><I>Cudd_bddIthVar</I><A NAME="1155"></A>: Returns
592 the projection<A NAME="276"></A> function with index <IMG
593 WIDTH="10" HEIGHT="15" ALIGN="BOTTOM" BORDER="0"
594 SRC="img6.png"
595 ALT="$i$">.
596 If the function does not exist, it is created.
597 </LI>
598 <LI><I>Cudd_bddNewVar</I><A NAME="1157"></A>: Returns a
599 new projection<A NAME="279"></A> function, whose index is
600 the largest index in use at the time of the call, plus 1.
601 </LI>
602 <LI><I>Cudd_bddNewVarAtLevel</I><A NAME="1159"></A>:
603 Similar to <I>Cudd_bddNewVar</I><A NAME="1161"></A>. In
604 addition it allows to specify the position in the variable
605 order<A NAME="284"></A> at which the new variable should be
606 inserted. In contrast, <I>Cudd_bddNewVar</I><A NAME="1163"></A>
607 adds the new variable at the end of the order.
608 </LI>
609 </UL>
610 The analogous functions for ADDs are
611 <I>Cudd_addIthVar</I><A NAME="1165"></A>,
612 <I>Cudd_addNewVar</I><A NAME="1167"></A>, and
613 <I>Cudd_addNewVarAtLevel</I><A NAME="1169"></A>.
617 <H3><A NAME="SECTION00036200000000000000"></A>
618 <A NAME="295"></A><A NAME="sec:ZDDvars"></A>
619 <BR>
620 New ZDD Variables
621 </H3>
624 Unlike the projection functions of BDDs and ADDs, the
625 projection<A NAME="297"></A> functions of ZDDs have diagrams
626 with <IMG
627 WIDTH="45" HEIGHT="32" ALIGN="MIDDLE" BORDER="0"
628 SRC="img7.png"
629 ALT="$n+1$"> nodes, where <IMG
630 WIDTH="15" HEIGHT="15" ALIGN="BOTTOM" BORDER="0"
631 SRC="img4.png"
632 ALT="$n$"> is the number of variables. Therefore the
633 ZDDs of the projection functions change when new variables are added.
634 This will be discussed in Section&nbsp;<A HREF="#sec:basicZDD">3.9</A>. Here we assume
635 that the number of variables is fixed. The ZDD of the <IMG
636 WIDTH="10" HEIGHT="15" ALIGN="BOTTOM" BORDER="0"
637 SRC="img6.png"
638 ALT="$i$">-th
639 projection function is returned by
640 <I>Cudd_zddIthVar</I><A NAME="1171"></A>.
644 <H2><A NAME="SECTION00037000000000000000"></A>
645 <A NAME="302"></A><A NAME="sec:basicBDD"></A>
646 <BR>
647 Basic BDD Manipulation
648 </H2>
651 Common manipulations of BDDs can be accomplished by calling
652 <I>Cudd_bddIte</I>. This function takes three BDDs, <IMG
653 WIDTH="15" HEIGHT="33" ALIGN="MIDDLE" BORDER="0"
654 SRC="img8.png"
655 ALT="$f$">, <IMG
656 WIDTH="13" HEIGHT="32" ALIGN="MIDDLE" BORDER="0"
657 SRC="img9.png"
658 ALT="$g$">, and
659 <IMG
660 WIDTH="14" HEIGHT="15" ALIGN="BOTTOM" BORDER="0"
661 SRC="img10.png"
662 ALT="$h$">, as arguments and computes <!-- MATH
663 $f\cdot g + f'\cdot h$
665 <IMG
666 WIDTH="95" HEIGHT="35" ALIGN="MIDDLE" BORDER="0"
667 SRC="img11.png"
668 ALT="$f\cdot g + f'\cdot h$">. Like all the
669 functions that create new BDDs or ADDs, <I>Cudd_bddIte</I><A NAME="1173"></A> returns a result that must be
670 explicitly referenced by the caller. <I>Cudd_bddIte</I> can be used
671 to implement all two-argument boolean functions. However, the package
672 also provides <I>Cudd_bddAnd</I><A NAME="1175"></A> as well as the
673 other two-operand boolean functions, which are slightly more efficient
674 when a two-operand function is called for. The following fragment of
675 code illustrates how to build the BDD for the function <!-- MATH
676 $f =
677 x_0'x_1'x_2'x_3'$
679 <IMG
680 WIDTH="108" HEIGHT="35" ALIGN="MIDDLE" BORDER="0"
681 SRC="img12.png"
682 ALT="$f =
683 x_0'x_1'x_2'x_3'$">.
684 <PRE>
685 DdManager *manager;
686 DdNode *f, *var, *tmp;
687 int i;
691 f = Cudd_ReadOne(manager);
692 Cudd_Ref(f);
693 for (i = 3; i &gt;= 0; i--) {
694 var = Cudd_bddIthVar(manager,i);
695 tmp = Cudd_bddAnd(manager,Cudd_Not(var),f);
696 Cudd_Ref(tmp);
697 Cudd_RecursiveDeref(manager,f);
698 f = tmp;
700 </PRE>
701 This example illustrates the following points:
703 <UL>
704 <LI>Intermediate results must be ``referenced'' and
705 ``dereferenced.'' However, <TT>var</TT> is a
706 projection<A NAME="314"></A> function, and its
707 reference<A NAME="315"></A> count is always greater than
708 0. Therefore, there is no call to <I>Cudd_Ref</I><A NAME="1177"></A>.
709 </LI>
710 <LI>The new <TT>f</TT> must be assigned to a temporary variable
711 (<TT>tmp</TT> in this example). If the result of
712 <I>Cudd_bddAnd</I><A NAME="1179"></A> were assigned directly to
713 <TT>f</TT>, the old <TT>f</TT> would be lost, and there would be no
714 way to free its nodes.
715 </LI>
716 <LI>The statement <TT>f = tmp</TT> has the same effect as:
717 <PRE>
718 f = tmp;
719 Cudd_Ref(f);
720 Cudd_RecursiveDeref(manager,tmp);
721 </PRE>
722 but is more efficient. The reference<A NAME="327"></A> is
723 ``passed'' from <TT>tmp</TT> to <TT>f</TT>, and <TT>tmp</TT> is now
724 ready to be reutilized.
725 </LI>
726 <LI>It is normally more efficient to build BDDs ``bottom-up.'' This
727 is why the loop goes from 3 to 0. Notice, however, that after
728 variable reordering, higher index does not necessarily mean ``closer
729 to the bottom.'' Of course, in this simple example, efficiency is
730 not a concern.
731 </LI>
732 <LI>Had we wanted to conjoin the variables in a bottom-up fashion
733 even after reordering, we should have used
734 <I>Cudd_ReadInvPerm</I><A NAME="1181"></A>. One has to be
735 careful, though, to fix the order of conjunction before entering the
736 loop. Otherwise, if reordering takes place, it is possible to use
737 one variable twice and skip another variable.
738 </LI>
739 </UL>
743 <H2><A NAME="SECTION00038000000000000000"></A>
744 <A NAME="335"></A><A NAME="sec:basicADD"></A>
745 <BR>
746 Basic ADD Manipulation
747 </H2>
750 The most common way to manipulate ADDs is via
751 <I>Cudd_addApply</I><A NAME="1183"></A>. This function can apply a
752 wide variety of operators to a pair of ADDs. Among the available
753 operators are addition, multiplication, division, minimum, maximum,
754 and boolean operators that work on ADDs whose leaves are restricted to
755 0 and 1 (0-1 ADDs).
758 The following fragment of code illustrates how to build the ADD for
759 the function <!-- MATH
760 $f = 5x_0x_1x_2x_3$
762 <IMG
763 WIDTH="117" HEIGHT="33" ALIGN="MIDDLE" BORDER="0"
764 SRC="img13.png"
765 ALT="$f = 5x_0x_1x_2x_3$">.
766 <PRE>
767 DdManager *manager;
768 DdNode *f, *var, *tmp;
769 int i;
773 f = Cudd_addConst(manager,5);
774 Cudd_Ref(f);
775 for (i = 3; i &gt;= 0; i--) {
776 var = Cudd_addIthVar(manager,i);
777 Cudd_Ref(var);
778 tmp = Cudd_addApply(manager,Cudd_addTimes,var,f);
779 Cudd_Ref(tmp);
780 Cudd_RecursiveDeref(manager,f);
781 Cudd_RecursiveDeref(manager,var);
782 f = tmp;
784 </PRE>
785 This example, contrasted to the example of BDD manipulation,
786 illustrates the following points:
788 <UL>
789 <LI>The ADD projection<A NAME="342"></A> function are not
790 maintained by the manager. It is therefore necessary to
791 reference<A NAME="343"></A> and
792 dereference<A NAME="344"></A> them.
793 </LI>
794 <LI>The product of two ADDs is computed by calling
795 <I>Cudd_addApply</I><A NAME="1185"></A> with
796 <I>Cudd_addTimes</I><A NAME="1187"></A> as parameter. There is
797 no ``apply'' function for BDDs, because
798 <I>Cudd_bddAnd</I><A NAME="1189"></A> and
799 <I>Cudd_bddXor</I><A NAME="1191"></A> plus complementation are
800 sufficient to implement all two-argument boolean functions.
801 </LI>
802 </UL>
806 <H2><A NAME="SECTION00039000000000000000"></A>
807 <A NAME="355"></A><A NAME="sec:basicZDD"></A>
808 <BR>
809 Basic ZDD Manipulation
810 </H2>
813 ZDDs are often generated by converting<A NAME="357"></A>
814 existing BDDs. (See Section&nbsp;<A HREF="#sec:convertZ">3.11</A>.) However, it is also
815 possible to build ZDDs by applying boolean operators to other ZDDs,
816 starting from constants and projection<A NAME="359"></A>
817 functions. The following fragment of code illustrates how to build
818 the ZDD for the function <!-- MATH
819 $f = x_0'+x_1'+x_2'+x_3'$
821 <IMG
822 WIDTH="172" HEIGHT="35" ALIGN="MIDDLE" BORDER="0"
823 SRC="img14.png"
824 ALT="$f = x_0'+x_1'+x_2'+x_3'$">. We assume that the
825 four variables already exist in the manager when the ZDD for <IMG
826 WIDTH="15" HEIGHT="33" ALIGN="MIDDLE" BORDER="0"
827 SRC="img8.png"
828 ALT="$f$"> is
829 built. Note the use of De Morgan's law.
830 <PRE>
831 DdManager *manager;
832 DdNode *f, *var, *tmp;
833 int i;
835 manager = Cudd_Init(0,4,CUDD_UNIQUE_SLOTS,
836 CUDD_CACHE_SLOTS,0);
839 tmp = Cudd_ReadZddOne(manager,0);
840 Cudd_Ref(tmp);
841 for (i = 3; i &gt;= 0; i--) {
842 var = Cudd_zddIthVar(manager,i);
843 Cudd_Ref(var);
844 f = Cudd_zddIntersect(manager,var,tmp);
845 Cudd_Ref(f);
846 Cudd_RecursiveDerefZdd(manager,tmp);
847 Cudd_RecursiveDerefZdd(manager,var);
848 tmp = f;
850 f = Cudd_zddDiff(manager,Cudd_ReadZddOne(manager,0),tmp);
851 Cudd_Ref(f);
852 Cudd_RecursiveDerefZdd(manager,tmp);
853 </PRE>
854 This example illustrates the following points:
856 <UL>
857 <LI>The projection<A NAME="363"></A> functions are
858 referenced, because they are not maintained by the manager.
859 </LI>
860 <LI>Complementation is obtained by subtracting from the constant 1
861 function.
862 </LI>
863 <LI>The result of <I>Cudd_ReadZddOne</I><A NAME="1193"></A>
864 does not require referencing.
865 </LI>
866 </UL>
867 CUDD provides functions for the manipulation of
868 covers<A NAME="367"></A> represented by ZDDs. For instance,
869 <I>Cudd_zddIsop</I><A NAME="1195"></A> builds a ZDD representing an
870 irredundant<A NAME="370"></A> sum of products for the
871 incompletely specified function defined by the two BDDs <IMG
872 WIDTH="16" HEIGHT="15" ALIGN="BOTTOM" BORDER="0"
873 SRC="img15.png"
874 ALT="$L$"> and <IMG
875 WIDTH="18" HEIGHT="15" ALIGN="BOTTOM" BORDER="0"
876 SRC="img16.png"
877 ALT="$U$">.
878 <I>Cudd_zddWeakDiv</I><A NAME="1197"></A> performs the weak
879 division of two covers given as ZDDs. These functions expect the two
880 ZDD variables corresponding to the two literals of the function
881 variable to be adjacent. One has to create variable groups (see
882 Section&nbsp;<A HREF="#sec:reordZ">3.14</A>) for reordering<A NAME="374"></A> of
883 the ZDD variables to work. BDD automatic reordering is safe even
884 without groups: If realignment of ZDD and ADD/BDD variables is
885 requested (see Section&nbsp;<A HREF="#sec:consist">3.15</A>) groups will be kept
886 adjacent.
890 <H2><A NAME="SECTION000310000000000000000"></A>
891 <A NAME="377"></A>
892 <A NAME="378"></A><A NAME="sec:convert"></A>
893 <BR>
894 Converting ADDs to BDDs and Vice Versa
895 </H2>
898 Several procedures are provided to convert ADDs to BDDs, according to
899 different criteria.
900 (<I>Cudd_addBddPattern</I><A NAME="1199"></A>,
901 <I>Cudd_addBddInterval</I><A NAME="1201"></A>, and
902 <I>Cudd_addBddThreshold</I><A NAME="1203"></A>.) The
903 conversion from BDDs to ADDs
904 (<I>Cudd_BddToAdd</I><A NAME="1205"></A>) is based on the simple
905 principle of mapping the logical 0<A NAME="388"></A> and 1 on the
906 arithmetic<A NAME="389"></A> 0 and 1. It is also possible to
907 convert an ADD with integer values (more precisely, floating point
908 numbers with 0 fractional part) to an array of BDDs by repeatedly
909 calling <I>Cudd_addIthBit</I><A NAME="1207"></A>.
913 <H2><A NAME="SECTION000311000000000000000"></A>
914 <A NAME="393"></A>
915 <A NAME="394"></A><A NAME="sec:convertZ"></A>
916 <BR>
917 Converting BDDs to ZDDs and Vice Versa
918 </H2>
921 Many applications first build a set of BDDs and then derive ZDDs from
922 the BDDs. These applications should create the manager with 0
923 ZDD<A NAME="396"></A> variables and create the BDDs. Then they should call
924 <I>Cudd_zddVarsFromBddVars</I><A NAME="1209"></A> to
925 create the necessary ZDD variables--whose number is likely to be
926 known once the BDDs are available. This approach eliminates the
927 difficulties that arise when the number of ZDD variables changes while
928 ZDDs are being built.
931 The simplest conversion from BDDs to ZDDs is a simple change of
932 representation, which preserves the functions. Simply put, given a BDD
933 for <IMG
934 WIDTH="15" HEIGHT="33" ALIGN="MIDDLE" BORDER="0"
935 SRC="img8.png"
936 ALT="$f$">, a ZDD for <IMG
937 WIDTH="15" HEIGHT="33" ALIGN="MIDDLE" BORDER="0"
938 SRC="img8.png"
939 ALT="$f$"> is requested. In this case the correspondence
940 between the BDD variables and ZDD variables is one-to-one. Hence,
941 <I>Cudd_zddVarsFromBddVars</I> should be called with the
942 <I>multiplicity</I> parameter equal to 1. The conversion proper can
943 then be performed by calling
944 <I>Cudd_zddPortFromBdd</I><A NAME="1211"></A>. The inverse
945 transformation is performed by
946 <I>Cudd_zddPortToBdd</I><A NAME="1213"></A>.
949 ZDDs are quite often used for the representation of
950 <I>covers</I><A NAME="406"></A>. This is normally done by
951 associating two ZDD variables to each variable of the function. (And
952 hence, typically, to each BDD variable.) One ZDD variable is
953 associated with the positive literal of the BDD variable, while the
954 other ZDD variable is associated with the negative literal. A call to
955 <I>Cudd_zddVarsFromBddVars</I><A NAME="1215"></A> with
956 <I>multiplicity</I> equal to 2 will associate to BDD variable <IMG
957 WIDTH="10" HEIGHT="15" ALIGN="BOTTOM" BORDER="0"
958 SRC="img6.png"
959 ALT="$i$"> the
960 two ZDD variables <IMG
961 WIDTH="19" HEIGHT="15" ALIGN="BOTTOM" BORDER="0"
962 SRC="img17.png"
963 ALT="$2i$"> and <IMG
964 WIDTH="49" HEIGHT="32" ALIGN="MIDDLE" BORDER="0"
965 SRC="img18.png"
966 ALT="$2i+1$">.
969 If a BDD variable group tree exists when
970 <I>Cudd_zddVarsFromBddVars</I> is called (see
971 Section&nbsp;<A HREF="#sec:group">3.13</A>) the function generates a ZDD variable group
972 tree consistent to it. In any case, all the ZDD variables derived
973 from the same BDD variable are clustered into a group.
976 If the ZDD for <IMG
977 WIDTH="15" HEIGHT="33" ALIGN="MIDDLE" BORDER="0"
978 SRC="img8.png"
979 ALT="$f$"> is created and later a new ZDD variable is added to
980 the manager, the function represented by the existing ZDD changes.
981 Suppose, for instance, that two variables are initially created, and
982 that the ZDD for <IMG
983 WIDTH="94" HEIGHT="33" ALIGN="MIDDLE" BORDER="0"
984 SRC="img19.png"
985 ALT="$f = x_0 + x_1$"> is built. If a third variable is
986 added, say <IMG
987 WIDTH="22" HEIGHT="32" ALIGN="MIDDLE" BORDER="0"
988 SRC="img20.png"
989 ALT="$x_2$">, then the ZDD represents <!-- MATH
990 $g = (x_0 + x_1) x_2'$
992 <IMG
993 WIDTH="124" HEIGHT="35" ALIGN="MIDDLE" BORDER="0"
994 SRC="img21.png"
995 ALT="$g = (x_0 + x_1) x_2'$">
996 instead. This change in function obviously applies regardless of what
997 use is made of the ZDD. However, if the ZDD is used to represent a
998 cover<A NAME="412"></A>, the cover itself is not changed by the
999 addition of new variable. (What changes is the
1000 characteristic<A NAME="413"></A> function of the cover.)
1004 <H2><A NAME="SECTION000312000000000000000"></A>
1005 <A NAME="415"></A><A NAME="sec:reorder"></A>
1006 <BR>
1007 Variable Reordering for BDDs and ADDs
1008 </H2>
1011 The CUDD package provides a rich set of
1012 dynamic<A NAME="417"></A> reordering algorithms. Some of them
1013 are slight variations of existing techniques
1015 HREF="node7.html#Rudell93">16</A>,<A
1016 HREF="node7.html#Drechs95">6</A>,<A
1017 HREF="node7.html#Bollig95">2</A>,<A
1018 HREF="node7.html#Ishiur91">10</A>,<A
1019 HREF="node7.html#Plessi93">15</A>,<A
1020 HREF="node7.html#Jeong93">11</A>]; some
1021 others have been developed specifically for this package
1023 HREF="node7.html#Panda94">14</A>,<A
1024 HREF="node7.html#Panda95b">13</A>].
1027 Reordering affects a unique<A NAME="420"></A> table. This means that
1028 BDDs and ADDs, which share the same unique table are simultaneously
1029 reordered. ZDDs, on the other hand, are reordered separately. In the
1030 following we discuss the reordering of BDDs and ADDs. Reordering for
1031 ZDDs is the subject of Section&nbsp;<A HREF="#sec:reordZ">3.14</A>.
1034 Reordering of the variables can be invoked directly by the application
1035 by calling <I>Cudd_ReduceHeap</I><A NAME="1217"></A>. Or it can
1036 be automatically triggered by the package when the number of nodes has
1037 reached a given threshold<A NAME="424"></A>. (The threshold
1038 is initialized and automatically adjusted after each reordering by the
1039 package.) To enable automatic dynamic reordering (also called
1040 <I>asynchronous<A NAME="425"></A></I> dynamic reordering
1041 in this document) the application must call
1042 <I>Cudd_AutodynEnable</I><A NAME="1219"></A>. Automatic
1043 dynamic reordering can subsequently be disabled by calling
1044 <I>Cudd_AutodynDisable</I><A NAME="1221"></A>.
1047 All reordering methods are available in both the case of direct call
1048 to <I>Cudd_ReduceHeap</I><A NAME="1223"></A> and the case of
1049 automatic invocation. For many methods, the reordering procedure is
1050 iterated until no further improvement is obtained. We call these
1051 methods the <I>converging<A NAME="432"></A></I> methods.
1052 When constraints are imposed on the relative position of variables
1053 (see Section&nbsp;<A HREF="#sec:group">3.13</A>) the reordering methods apply inside the
1054 groups. The groups<A NAME="434"></A> themselves are reordered
1055 by sifting<A NAME="435"></A>. Each method is identified by a
1056 constant of the enumerated type
1057 <I>Cudd_ReorderingType<A NAME="436"></A></I>
1058 defined in <I>cudd.h<A NAME="437"></A></I> (the external
1059 header<A NAME="438"></A> file of the CUDD package):
1062 <DL>
1063 <DT><STRONG>CUDD_REORDER_NONE<A NAME="440"></A>:</STRONG></DT>
1064 <DD>This method
1065 causes no reordering.
1066 </DD>
1067 <DT><STRONG>CUDD_REORDER_SAME<A NAME="441"></A>:</STRONG></DT>
1068 <DD>If passed to
1069 <I>Cudd_AutodynEnable</I><A NAME="1225"></A>, this
1070 method leaves the current method for automatic reordering unchanged.
1071 If passed to <I>Cudd_ReduceHeap</I><A NAME="1227"></A>,
1072 this method causes the current method for automatic reordering to be
1073 used.
1074 </DD>
1075 <DT><STRONG>CUDD_REORDER_RANDOM<A NAME="446"></A>:</STRONG></DT>
1076 <DD>Pairs of
1077 variables are randomly chosen, and swapped in the order. The swap is
1078 performed by a series of swaps of adjacent variables. The best order
1079 among those obtained by the series of swaps is retained. The number
1080 of pairs chosen for swapping<A NAME="447"></A> equals the
1081 number of variables in the diagram.
1082 </DD>
1083 <DT><STRONG>CUDD_REORDER_RANDOM_PIVOT<A NAME="448"></A>:</STRONG></DT>
1084 <DD>Same as CUDD_REORDER_RANDOM, but the two variables are chosen so
1085 that the first is above the variable with the largest number of
1086 nodes, and the second is below that variable. In case there are
1087 several variables tied for the maximum number of nodes, the one
1088 closest to the root is used.
1089 </DD>
1090 <DT><STRONG>CUDD_REORDER_SIFT<A NAME="449"></A>:</STRONG></DT>
1091 <DD>This method is
1092 an implementation of Rudell's sifting<A NAME="450"></A>
1093 algorithm [<A
1094 HREF="node7.html#Rudell93">16</A>]. A simplified description of sifting is as
1095 follows: Each variable is considered in turn. A variable is moved up
1096 and down in the order so that it takes all possible positions. The
1097 best position is identified and the variable is returned to that
1098 position.
1101 In reality, things are a bit more complicated. For instance, there
1102 is a limit on the number of variables that will be sifted. This
1103 limit can be read with
1104 <I>Cudd_ReadSiftMaxVar</I><A NAME="1229"></A> and set with
1105 <I>Cudd_SetSiftMaxVar</I><A NAME="1231"></A>. In addition,
1106 if the diagram grows too much while moving a variable up or down,
1107 that movement is terminated before the variable has reached one end
1108 of the order. The maximum ratio by which the diagram is allowed to
1109 grow while a variable is being sifted can be read with
1110 <I>Cudd_ReadMaxGrowth</I><A NAME="1233"></A> and set with
1111 <I>Cudd_SetMaxGrowth</I><A NAME="1235"></A>.
1112 </DD>
1113 <DT><STRONG>CUDD_REORDER_SIFT_CONVERGE<A NAME="460"></A>:</STRONG></DT>
1114 <DD>This is the converging<A NAME="461"></A> variant of
1115 CUDD_REORDER_SIFT.
1116 </DD>
1117 <DT><STRONG>CUDD_REORDER_SYMM_SIFT<A NAME="462"></A>:</STRONG></DT>
1118 <DD>This method is an implementation of
1119 symmetric<A NAME="463"></A> sifting [<A
1120 HREF="node7.html#Panda94">14</A>]. It is
1121 similar to sifting, with one addition: Variables that become
1122 adjacent during sifting are tested for symmetry<A NAME="465"></A>. If
1123 they are symmetric, they are linked in a group. Sifting then
1124 continues with a group being moved, instead of a single variable.
1125 After symmetric sifting has been run,
1126 <I>Cudd_SymmProfile</I><A NAME="1237"></A> can be called to
1127 report on the symmetry groups found. (Both positive and negative
1128 symmetries are reported.)
1129 </DD>
1130 <DT><STRONG>CUDD_REORDER_SYMM_SIFT_CONV<A NAME="468"></A>:</STRONG></DT>
1131 <DD>This is the converging<A NAME="469"></A> variant of
1132 CUDD_REORDER_SYMM_SIFT.
1133 </DD>
1134 <DT><STRONG>CUDD_REORDER_GROUP_SIFT<A NAME="470"></A>:</STRONG></DT>
1135 <DD>This method is an implementation of group<A NAME="471"></A>
1136 sifting [<A
1137 HREF="node7.html#Panda95b">13</A>]. It is similar to symmetric sifting, but
1138 aggregation<A NAME="473"></A> is not restricted to symmetric
1139 variables.
1140 </DD>
1141 <DT><STRONG>CUDD_REORDER_GROUP_SIFT_CONV<A NAME="474"></A>:</STRONG></DT>
1142 <DD>This method repeats until convergence the combination of
1143 CUDD_REORDER_GROUP_SIFT and CUDD_REORDER_WINDOW4.
1144 </DD>
1145 <DT><STRONG>CUDD_REORDER_WINDOW2<A NAME="475"></A>:</STRONG></DT>
1146 <DD>This
1147 method implements the window<A NAME="476"></A> permutation
1148 approach of Fujita [<A
1149 HREF="node7.html#Fujita91b">8</A>] and Ishiura [<A
1150 HREF="node7.html#Ishiur91">10</A>].
1151 The size of the window is 2.
1152 </DD>
1153 <DT><STRONG>CUDD_REORDER_WINDOW3<A NAME="479"></A>:</STRONG></DT>
1154 <DD>Similar
1155 to CUDD_REORDER_WINDOW2, but with a window of size 3.
1156 </DD>
1157 <DT><STRONG>CUDD_REORDER_WINDOW4<A NAME="480"></A>:</STRONG></DT>
1158 <DD>Similar
1159 to CUDD_REORDER_WINDOW2, but with a window of size 4.
1160 </DD>
1161 <DT><STRONG>CUDD_REORDER_WINDOW2_CONV<A NAME="481"></A>:</STRONG></DT>
1162 <DD>This is the converging<A NAME="482"></A> variant of
1163 CUDD_REORDER_WINDOW2.
1164 </DD>
1165 <DT><STRONG>CUDD_REORDER_WINDOW3_CONV<A NAME="483"></A>:</STRONG></DT>
1166 <DD>This is the converging variant of CUDD_REORDER_WINDOW3.
1167 </DD>
1168 <DT><STRONG>CUDD_REORDER_WINDOW4_CONV<A NAME="484"></A>:</STRONG></DT>
1169 <DD>This is the converging variant of CUDD_REORDER_WINDOW4.
1170 </DD>
1171 <DT><STRONG>CUDD_REORDER_ANNEALING<A NAME="485"></A>:</STRONG></DT>
1172 <DD>This
1173 method is an implementation of simulated
1174 annealing<A NAME="486"></A> for variable
1175 ordering, vaguely resemblant of the algorithm of [<A
1176 HREF="node7.html#Bollig95">2</A>].
1177 This method is potentially very slow.
1178 </DD>
1179 <DT><STRONG>CUDD_REORDER_GENETIC:<A NAME="488"></A></STRONG></DT>
1180 <DD>This
1181 method is an implementation of a genetic<A NAME="489"></A>
1182 algorithm for variable ordering, inspired by the work of Drechsler
1184 HREF="node7.html#Drechs95">6</A>]. This method is potentially very slow.
1185 </DD>
1186 <DT><STRONG>CUDD_REORDER_EXACT<A NAME="491"></A>:</STRONG></DT>
1187 <DD>This method
1188 implements a dynamic programming approach to
1189 exact<A NAME="492"></A> reordering
1191 HREF="node7.html#Held62">9</A>,<A
1192 HREF="node7.html#Friedman90">7</A>,<A
1193 HREF="node7.html#Ishiur91">10</A>], with improvements described in
1195 HREF="node7.html#Jeong93">11</A>]. It only stores one BDD at the time. Therefore, it is
1196 relatively efficient in terms of memory. Compared to other
1197 reordering strategies, it is very slow, and is not recommended for
1198 more than 16 variables.
1199 </DD>
1200 </DL>
1201 So far we have described methods whereby the package selects an order
1202 automatically. A given order of the variables can also be imposed by
1203 calling <I>Cudd_ShuffleHeap</I><A NAME="1239"></A>.
1207 <H2><A NAME="SECTION000313000000000000000"></A>
1208 <A NAME="499"></A><A NAME="sec:group"></A>
1209 <BR>
1210 Grouping Variables
1211 </H2>
1214 CUDD allows the application to specify constraints on the positions of
1215 group of variables. It is possible to request that a group of
1216 contiguous variables be kept contiguous by the reordering procedures.
1217 It is also possible to request that the relative order of some groups
1218 of variables be left unchanged. The constraints on the order are
1219 specified by means of a tree<A NAME="501"></A>, which is created in
1220 one of two ways:
1222 <UL>
1223 <LI>By calling <I>Cudd_MakeTreeNode</I><A NAME="1241"></A>.
1224 </LI>
1225 <LI>By calling the functions of the MTR<A NAME="505"></A> library
1226 (part of the distribution), and by registering the result with the
1227 manager using <I>Cudd_SetTree</I><A NAME="1243"></A>. The current
1228 tree registered with the manager can be read with
1229 <I>Cudd_ReadTree</I><A NAME="1245"></A>.
1230 </LI>
1231 </UL>
1234 Each node in the tree represents a range of variables. The lower bound
1235 of the range is given by the <I>low</I> field of the node, and the
1236 size of the group is given by the <I>size</I> field of the
1237 node.<A NAME="tex2html4"
1238 HREF="footnode.html#foot1076"><SUP>2</SUP></A> The variables
1239 in each range are kept contiguous. Furthermore, if a node is marked
1240 with the MTR_FIXED<A NAME="515"></A> flag, then the relative order of
1241 the variable ranges associated to its children is not changed. As an
1242 example, suppose the initial variable order is:
1243 <PRE>
1244 x0, y0, z0, x1, y1, z1, ... , x9, y9, z9.
1245 </PRE>
1246 Suppose we want to keep each group of three variables with the same
1247 index (e.g., <code>x3, y3, z3</code>) contiguous, while allowing the package
1248 to change the order of the groups. We can accomplish this with the
1249 following code:
1250 <PRE>
1251 for (i = 0; i &lt; 10; i++) {
1252 (void) Cudd_MakeTreeNode(manager,i*3,3,MTR_DEFAULT);
1254 </PRE>
1255 If we want to keep the order within each group of variables
1256 fixed (i.e., <code>x</code> before <code>y</code> before <code>z</code>) we need to
1257 change MTR_DEFAULT<A NAME="520"></A> into MTR_FIXED.
1260 The <I>low</I> parameter passed to
1261 <I>Cudd_MakeTreeNode</I><A NAME="1247"></A> is the index of a
1262 variable (as opposed to its level or position in the order). The
1263 group tree<A NAME="524"></A> can be created at any time. The
1264 result obviously depends on the variable order in effect at creation
1265 time.
1268 It is possible to create a variable group tree also before the
1269 variables themselves are created. The package assumes in this case
1270 that the index of the variables not yet in existence will equal their
1271 position in the order when they are created. Therefore, applications
1272 that rely on
1273 <I>Cudd_bddNewVarAtLevel</I><A NAME="1249"></A> or
1274 <I>Cudd_addNewVarAtLevel</I><A NAME="1251"></A> to create
1275 new variables have to create the variables before they group them.
1278 The reordering procedure will skip all groups whose variables are not
1279 yet in existence. For groups that are only partially in existence, the
1280 reordering procedure will try to reorder the variables already
1281 instantiated, without violating the adjacency constraints.
1285 <H2><A NAME="SECTION000314000000000000000"></A>
1286 <A NAME="530"></A><A NAME="sec:reordZ"></A>
1287 <BR>
1288 Variable Reordering for ZDDs
1289 </H2>
1292 Reordering of ZDDs is done in much the same way as the reordering of
1293 BDDs and ADDs. The functions corresponding to <I>Cudd_ReduceHeap</I>
1294 and <I>Cudd_ShuffleHeap</I> are
1295 <I>Cudd_zddReduceHeap</I><A NAME="1253"></A> and
1296 <I>Cudd_zddShuffleHeap</I><A NAME="1255"></A>. To enable
1297 dynamic<A NAME="538"></A> reordering, the application must
1298 call <I>Cudd_AutodynEnableZdd</I><A NAME="1257"></A>, and
1299 to disable dynamic reordering, it must call
1300 <I>Cudd_AutodynDisableZdd</I><A NAME="1259"></A>. In the
1301 current implementation, however, the choice of reordering methods for
1302 ZDDs is more limited. Specifically, these methods are available:
1305 <DL>
1306 <DT><STRONG>CUDD_REORDER_NONE<A NAME="544"></A>;</STRONG></DT>
1307 <DD>
1308 </DD>
1309 <DT><STRONG>CUDD_REORDER_SAME<A NAME="545"></A>;</STRONG></DT>
1310 <DD>
1311 </DD>
1312 <DT><STRONG>CUDD_REORDER_RANDOM<A NAME="546"></A>;</STRONG></DT>
1313 <DD>
1314 </DD>
1315 <DT><STRONG>CUDD_REORDER_RANDOM_PIVOT<A NAME="547"></A>;</STRONG></DT>
1316 <DD>
1317 </DD>
1318 <DT><STRONG>CUDD_REORDER_SIFT<A NAME="548"></A>;</STRONG></DT>
1319 <DD>
1320 </DD>
1321 <DT><STRONG>CUDD_REORDER_SIFT_CONVERGE<A NAME="549"></A>;</STRONG></DT>
1322 <DD>
1323 </DD>
1324 <DT><STRONG>CUDD_REORDER_SYMM_SIFT<A NAME="550"></A>;</STRONG></DT>
1325 <DD>
1326 </DD>
1327 <DT><STRONG>CUDD_REORDER_SYMM_SIFT_CONV<A NAME="551"></A>.</STRONG></DT>
1328 <DD>
1329 </DD>
1330 </DL>
1333 To create ZDD variable groups, the application calls
1334 <I>Cudd_MakeZddTreeNode</I><A NAME="1261"></A>.
1338 <H2><A NAME="SECTION000315000000000000000"></A>
1339 <A NAME="sec:consist"></A>
1340 <BR>
1341 Keeping Consistent Variable Orders for BDDs and ZDDs
1342 </H2>
1345 Several applications that manipulate both BDDs and ZDDs benefit from
1346 keeping a fixed correspondence between the order of the BDD variables
1347 and the order of the ZDD variables. If each BDD variable corresponds
1348 to a group of ZDD variables, then it is often desirable that the
1349 groups of ZDD variables be in the same order as the corresponding BDD
1350 variables. CUDD allows the ZDD order to track the BDD order and vice
1351 versa. To have the ZDD order track the BDD order, the application
1352 calls <I>Cudd_zddRealignEnable</I><A NAME="1263"></A>. The
1353 effect of this call can be reversed by calling
1354 <I>Cudd_zddRealignDisable</I><A NAME="1265"></A>. When
1355 ZDD realignment is in effect, automatic reordering of ZDDs should be
1356 disabled.
1360 <H2><A NAME="SECTION000316000000000000000"></A>
1361 <A NAME="562"></A><A NAME="sec:hooks"></A>
1362 <BR>
1363 Hooks
1364 </H2>
1367 Hooks in CUDD are lists of application-specified functions to be run on
1368 certain occasions. Each hook is identified by a constant of the
1369 enumerated type <I>Cudd_HookType</I><A NAME="1267"></A>. In Version
1370 2.4.2 hooks are defined for these occasions:
1372 <UL>
1373 <LI>before garbage collection (CUDD_PRE_GC_HOOK);
1374 </LI>
1375 <LI>after garbage collection (CUDD_POST_GC_HOOK);
1376 </LI>
1377 <LI>before variable reordering (CUDD_PRE_REORDERING_HOOK);
1378 </LI>
1379 <LI>after variable reordering (CUDD_POST_REORDERING_HOOK).
1380 </LI>
1381 </UL>
1382 The current implementation of hooks is experimental. A function added
1383 to a hook receives a pointer to the manager, a pointer to a constant
1384 string, and a pointer to void as arguments; it must return 1 if
1385 successful; 0 otherwise. The second argument is one of ``DD,''
1386 ``BDD,'' and ``ZDD.'' This allows the hook functions to tell the type
1387 of diagram for which reordering or garbage collection takes place. The
1388 third argument varies depending on the hook. The hook functions called
1389 before or after garbage collection<A NAME="568"></A> do
1390 not use it. The hook functions called before
1391 reordering<A NAME="569"></A> are passed, in addition to the
1392 pointer to the manager, also the method used for reordering. The hook
1393 functions called after reordering are passed the start time. To add a
1394 function to a hook, one uses <I>Cudd_AddHook</I><A NAME="1269"></A>.
1395 The function of a given hook
1396 are called in the order in which they were added to the hook. For
1397 sample hook functions, one may look at
1398 <I>Cudd_StdPreReordHook</I><A NAME="1271"></A> and
1399 <I>Cudd_StdPostReordHook</I><A NAME="1273"></A>.
1403 <H2><A NAME="SECTION000317000000000000000"></A>
1404 <A NAME="577"></A><A NAME="578"></A><A NAME="sec:sis-vis"></A>
1405 <BR>
1406 The SIS/VIS Interface
1407 </H2>
1410 The CUDD package contains interface functions that emulate the
1411 behavior of the original BDD package used in SIS [<A
1412 HREF="node7.html#Sentov92">17</A>] and
1413 in the newer
1414 <A NAME="tex2html5"
1415 HREF="http://vlsi.Colorado.EDU/~vis/">VIS</A>
1417 HREF="node7.html#VIS">4</A>]. How to build VIS with CUDD is described
1418 in the installation documents of VIS. (Version 1.1 and later.)
1422 <H3><A NAME="SECTION000317100000000000000"></A>
1423 <A NAME="585"></A><A NAME="sec:sis"></A>
1424 <BR>
1425 Using the CUDD Package in SIS
1426 </H3>
1429 This section describes how to build SIS with the CUDD package. Let
1430 <TT>SISDIR<A NAME="587"></A></TT> designate the root of the directory
1431 hierarchy where the sources for SIS reside. Let
1432 <TT>CUDDDIR<A NAME="588"></A></TT> be the root of the directory hierarchy
1433 where the distribution of the CUDD package resides. To build SIS with
1434 the CUDD package, follow these steps.
1436 <OL>
1437 <LI>Create directories <TT>SISDIR/sis/cudd</TT> and
1438 <TT>SISDIR/sis/mtr</TT>.
1439 </LI>
1440 <LI>Copy all files from <TT>CUDDDIR/cudd</TT> and
1441 <TT>CUDDDIR/sis</TT> to <TT>SISDIR/sis/cudd</TT> and all files from
1442 <TT>CUDDDIR/mtr</TT> to <TT>SISDIR/sis/mtr</TT>.
1443 </LI>
1444 <LI>Copy <TT>CUDDDIR/cudd/doc/cudd.doc</TT> to
1445 <TT>SISDIR/sis/cudd</TT>; also copy <TT>CUDDDIR/mtr/doc/mtr.doc</TT>
1446 to <TT>SISDIR/sis/mtr</TT>.
1447 </LI>
1448 <LI>In <TT>SISDIR/sis/cudd</TT> make <TT>bdd.h</TT> a symbolic link
1449 to <TT>cuddBdd.h</TT>. (That is: <TT>ln -s cuddBdd.h bdd.h</TT>.)
1450 </LI>
1451 <LI>In <TT>SISDIR/sis/cudd</TT> delete <TT>Makefile</TT> and rename
1452 <TT>Makefile.sis</TT> as <TT>Makefile</TT>. Do the same in
1453 <TT>SISDIR/sis/mtr</TT>.
1454 </LI>
1455 <LI>Copy <TT>CUDDDIR/sis/st.[ch]</TT> and <TT>CUDDDIR/st/doc/st.doc</TT>
1456 to <TT>SISDIR/sis/st</TT>. (This will overwrite the original files: You
1457 may want to save them beforehand.)
1458 </LI>
1459 <LI>From <TT>CUDDDIR/util</TT> copy <TT>datalimit.c</TT> to
1460 <TT>SISDIR/sis/util</TT>. Update <TT>util.h</TT> and
1461 <TT>Makefile</TT> in <TT>SISDIR/sis/util</TT>. Specifically, add the
1462 declaration <TT>EXTERN long getSoftDataLimit();</TT> to
1463 <TT>util.h</TT> and add <TT>datalimit.c</TT> to the list of source
1464 files (PSRC) in <TT>Makefile</TT>.
1465 </LI>
1466 <LI>In <TT>SISDIR/sis</TT> remove the link from <TT>bdd</TT> to
1467 <TT>bdd_cmu</TT> or <TT>bdd_ucb</TT> (that is, <TT>rm bdd</TT>)
1468 and make <TT>bdd</TT> a symbolic link to <TT>cudd</TT>. (That is:
1469 <TT>ln -s cudd bdd</TT>.)
1470 </LI>
1471 <LI>Still in <TT>SISDIR/sis</TT>, edit <TT>Makefile</TT>, <TT>Makefile.oct</TT>, and <TT>Makefile.nooct</TT>. In all three files add
1472 mtr to the list of directories to be made (DIRS).
1473 </LI>
1474 <LI>In <TT>SISDIR/sis/include</TT> make <TT>mtr.h</TT> a symbolic
1475 link to <TT>../mtr/mtr.h</TT>.
1476 </LI>
1477 <LI>In <TT>SISDIR/sis/doc</TT> make <TT>cudd.doc</TT> a symbolic
1478 link to <TT>../cudd/cudd.doc</TT> and <TT>mtr.doc</TT> a symbolic
1479 link to <TT>../mtr/mtr.doc</TT>. (That is: <TT>ln -s
1480 ../cudd/cudd.doc .; ln -s ../mtr/mtr.doc .</TT>.)
1481 </LI>
1482 <LI>From <TT>SISDIR</TT> do <TT>make clean</TT> followed by
1483 <TT>make -i</TT>. This should create a working copy of SIS that
1484 uses the CUDD package.
1485 </LI>
1486 </OL>
1489 The replacement for the <TT>st</TT> library is because the version
1490 shipped with the CUDD package tests for out-of-memory conditions.
1491 Notice that the version of the <TT>st</TT> library to be used for
1492 replacement is not the one used for the normal build, because the
1493 latter has been modified for C++ compatibility. The above installation
1494 procedure has been tested on SIS 1.3. SIS can be obtained via
1495 anonymous FTP<A NAME="650"></A> from
1496 <A NAME="tex2html6"
1497 HREF="ftp://ic.eecs.berkeley.edu"><TT>ic.eecs.berkeley.edu</TT></A>.
1498 To build SIS 1.3, you need <TT>sis-1.2.tar.Z</TT> and
1499 <TT>sis-1.2.patch1.Z</TT>. When compiling on a DEC Alpha<A NAME="655"></A>, you should add the <TT>-ieee_with_no_inexact</TT> flag.
1500 (See Section&nbsp;<A HREF="#sec:predef-const">3.5.2</A>.) Refer to the <TT>Makefile</TT>
1501 in the top level directory of the distribution for how to compile with
1502 32-bit pointers.
1506 <H2><A NAME="SECTION000318000000000000000"></A>
1507 <A NAME="sec:dump"></A>
1508 <BR>
1509 Writing Decision Diagrams to a File
1510 </H2>
1513 The CUDD package provides several functions to write decision diagrams
1514 to a file. <I>Cudd_DumpBlif</I><A NAME="1275"></A> writes a
1515 file in <I>blif</I> format. It is restricted to BDDs. The diagrams
1516 are written as a network of multiplexers, one multiplexer for each
1517 internal node of the BDD.
1520 <I>Cudd_DumpDot</I><A NAME="1277"></A> produces input suitable to
1521 the graph-drawing<A NAME="666"></A> program
1522 <A NAME="tex2html8"
1523 HREF="http://www.research.att.com/sw/tools/graphviz"><I>dot</I></A>
1524 written by Eleftherios Koutsofios and Stephen C. North. An example of
1525 drawing produced by dot from the output of <I>Cudd_DumpDot</I> is
1526 shown in Figure&nbsp;<A HREF="#fi:phase">1</A>. It is restricted to BDDs and ADDs.
1528 <DIV ALIGN="CENTER"><A NAME="fi:phase"></A><A NAME="1082"></A>
1529 <TABLE>
1530 <CAPTION ALIGN="BOTTOM"><STRONG>Figure 1:</STRONG>
1531 A BDD representing a phase constraint for the optimization of
1532 fixed-polarity Reed-Muller forms. The label of each node is the
1533 unique part of the node address. All nodes on the same level
1534 correspond to the same variable, whose name is shown at the left of
1535 the diagram. Dotted lines indicate complement<A NAME="673"></A>
1536 arcs. Dashed lines indicate regular<A NAME="674"></A> ``else''
1537 arcs.</CAPTION>
1538 <TR><TD>
1539 <DIV ALIGN="CENTER">
1540 <IMG
1541 WIDTH="429" HEIGHT="701" ALIGN="BOTTOM" BORDER="0"
1542 SRC="img22.png"
1543 ALT="\includegraphics[height=15.5cm]{phase.ps}"></DIV></TD></TR>
1544 </TABLE>
1545 </DIV>
1547 <I>Cudd_zddDumpDot</I><A NAME="1279"></A> is the analog of
1548 <I>Cudd_DumpDot</I> for ZDDs.
1551 <I>Cudd_DumpDaVinci</I><A NAME="1281"></A> produces input
1552 suitable to the graph-drawing<A NAME="682"></A> program
1553 <A NAME="tex2html9"
1554 HREF="ftp://ftp.uni-bremen.de/pub/graphics/daVinci"><I>daVinci</I></A>
1555 developed at the University of Bremen. It is restricted to BDDs and
1556 ADDs.
1559 Functions are also available to produce the input format of
1560 <I>DDcal</I> (see Section&nbsp;<A HREF="node2.html#sec:getFriends">2.2</A>) and factored forms.
1564 <H2><A NAME="SECTION000319000000000000000"></A>
1565 <A NAME="sec:save-restore"></A>
1566 <BR>
1567 Saving and Restoring BDDs
1568 </H2>
1572 <A NAME="tex2html10"
1573 HREF="ftp://ftp.polito.it/pub/research/dddmp/"><I>dddmp</I></A>
1574 library<A NAME="691"></A> by Gianpiero Cabodi and Stefano Quer
1575 allows a CUDD application to save BDDs to disk in compact form for
1576 later retrieval. See the library's own documentation for the details.
1579 <HR>
1580 <!--Navigation Panel-->
1581 <A NAME="tex2html111"
1582 HREF="node4.html">
1583 <IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
1584 SRC="icons/next.png"></A>
1585 <A NAME="tex2html107"
1586 HREF="cuddIntro.html">
1587 <IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
1588 SRC="icons/up.png"></A>
1589 <A NAME="tex2html101"
1590 HREF="node2.html">
1591 <IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
1592 SRC="icons/prev.png"></A>
1593 <A NAME="tex2html109"
1594 HREF="node8.html">
1595 <IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
1596 SRC="icons/index.png"></A>
1597 <BR>
1598 <B> Next:</B> <A NAME="tex2html112"
1599 HREF="node4.html">Programmer's Manual</A>
1600 <B> Up:</B> <A NAME="tex2html108"
1601 HREF="cuddIntro.html">CUDD: CU Decision Diagram</A>
1602 <B> Previous:</B> <A NAME="tex2html102"
1603 HREF="node2.html">How to Get CUDD</A>
1604 &nbsp; <B> <A NAME="tex2html110"
1605 HREF="node8.html">Index</A></B>
1606 <!--End of Navigation Panel-->
1607 <ADDRESS>
1608 Fabio Somenzi
1609 2009-02-20
1610 </ADDRESS>
1611 </BODY>
1612 </HTML>