source: vis_dev/glu-2.3/src/cuBdd/doc/node3.html @ 13

Last change on this file since 13 was 13, checked in by cecile, 13 years ago

library glu 2.3

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