Context Navigation

node3.html

Last change on this file 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)
4	original 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>
139	User's Manual
140	</H1>
141
142	<P>
143	This 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>
150	Compiling and Linking
151	</H2>
152
153	<P>
154	To 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>
160	to 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
165	libraries are part of the distribution.) Some
166	platforms require specific compiler and linker flags. Refer to the
167	<TT>Makefile<A NAME="86"></A></TT> in the top level directory of the
168	distribution.
169
170	<P>
171	Keep in mind that whatever flags affect the size of data
172	structures--for instance the flags used to use 64-bit pointers where
173	available--must be specified when compiling both CUDD and the files
174	that include its header files.
175
176	<P>
177
178	<H2><A NAME="SECTION00032000000000000000"></A>
179	<A NAME="sec:struct"></A>
180	<BR>
181	Basic Data Structures
182	</H2>
183
184	<P>
185
186	<H3><A NAME="SECTION00032100000000000000"></A>
187	<A NAME="sec:nodes"></A>
188	<BR>
189	Nodes
190	</H3>
191
192	<P>
193	BDDs, 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
195	that are of interest to the application that uses the CUDD package as
196	a black box are the variable index<A NAME="93"></A>, the
197	reference<A NAME="94"></A> count, and the value. The
198	remaining fields are pointers that connect nodes among themselves and
199	that are used to implement the unique<A NAME="95"></A> table. (See
200	Section <A HREF="node3.html#sec:manager">3.2.2</A>.)
201
202	<P>
203	The <EM>index</EM> field holds the name of the variable that labels the
204	node. The index of a variable is a permanent attribute that reflects
205	the order<A NAME="98"></A> of creation. Index 0 corresponds to
206	the variable created first. On a machine with 32-bit pointers, the
207	maximum number of variables is the largest value that can be stored in
208	an unsigned short integer minus 1. The largest index is reserved for
209	the constant<A NAME="99"></A> nodes. When 64-bit pointers are
210	used, the maximum number of variables is the largest value that can be
211	stored in an unsigned integer minus 1.
212
213	<P>
214	When variables are reordered to reduce the size of the decision
215	diagrams, the variables may shift in the order, but they retain their
216	indices. The package keeps track of the variable
217	permutation<A NAME="100"></A> (and its inverse). The
218	application is not affected by variable reordering<A NAME="101"></A>,
219	except 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
235	takes place, then the property of <A NAME="tex2html6"
236	HREF="cuddExtDet.html#Cudd_bddConstrain"><EM>Cudd_bddConstrain</EM></A>
237	of being an
238	image restrictor is lost.
239	</LI>
240	</UL>
241
242	<P>
243	The CUDD package relies on garbage<A NAME="116"></A>
244	collection to reclaim the memory used by diagrams that are no longer
245	in use. The scheme employed for garbage collection is based on keeping
246	a reference<A NAME="117"></A> count for each node. The
247	references that are counted are both the internal references
248	(references from other nodes) and external references (typically
249	references from the calling environment). When an application creates
250	a new BDD<A NAME="118"></A>, ADD<A NAME="119"></A>, or ZDD<A NAME="120"></A>,
251	it must increase its reference count explicitly, through
252	a call to <A NAME="tex2html7"
253	HREF="cuddExtDet.html#Cudd_Ref"><EM>Cudd_Ref</EM></A><A NAME="1429"></A>. Similarly, when a
254	diagram 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
256	and 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
259	diagram.
260
261	<P>
262	Terminal<A NAME="131"></A> nodes carry a value. This is especially
263	important for ADDs. By default, the value is a double<A NAME="132"></A>.
264	To change to something different (e.g., an integer), the
265	package must be modified and recompiled. Support for this process is
266	currently very rudimentary.
267
268	<P>
269
270	<H3><A NAME="SECTION00032200000000000000"></A>
271	<A NAME="134"></A><A NAME="sec:manager"></A>
272	<BR>
273	The Manager
274	</H3>
275
276	<P>
277	All nodes used in BDDs, ADDs, and ZDDs are kept in special
278	hash<A NAME="136"></A> tables called the <EM> unique<A NAME="137"></A> tables</EM>. Specifically, BDDs and ADDs
279	share the same unique table, whereas ZDDs have their own table. As
280	the name implies, the main purpose of the unique table is to guarantee
281	that each node is unique; that is, there is no other node labeled by
282	the same variable and with the same children. This uniqueness property
283	makes decision diagrams canonical<A NAME="138"></A>. The
284	unique<A NAME="139"></A> tables and some auxiliary data structures
285	make up the DdManager<A NAME="140"></A> (manager<A NAME="141"></A> for
286	short). Though the application that uses only the exported functions
287	needs not be concerned with most details of the manager, it has to
288	deal with the manager in the following sense. The application must
289	initialize the manager by calling an appropriate function. (See
290	Section <A HREF="node3.html#sec:init">3.3</A>.) Subsequently, it must pass a pointer to the
291	manager to all the functions that operate on decision diagrams.
292
293	<P>
294	With the exception of a few statistical counters<A NAME="143"></A>, there are no global<A NAME="144"></A> variables in
295	the CUDD package. Therefore, it is quite possible to have multiple
296	managers simultaneously active in the same application.<A NAME="tex2html10"
297	HREF="footnode.html#foot145"><SUP>1</SUP></A> It is the pointers to
298	the 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>
305	Cache
306	</H3>
307
308	<P>
309	Efficient recursive manipulation of decision diagrams requires the use
310	of a table to store computed results. This table<A NAME="149"></A>
311	is called here the <EM>cache<A NAME="150"></A></EM> because it is
312	effectively handled like a cache of variable but limited capacity. The
313	CUDD package starts by default with a small cache, and increases its
314	size until either no further benefit is achieved, or a limit size is
315	reached. The user can influence this policy by choosing initial and
316	limit values for the cache size.
317
318	<P>
319	Too small a cache will cause frequent overwriting of useful results.
320	Too large a cache will cause overhead, because the whole cache is
321	scanned every time garbage<A NAME="151"></A> collection takes
322	place. The optimal parameters depend on the specific application. The
323	default parameters work reasonably well for a large spectrum of
324	applications.
325
326	<P>
327	The cache<A NAME="152"></A> of the CUDD package is used by most recursive
328	functions of the package, and can be used by user-supplied functions
329	as well. (See Section <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>
336	Initializing and Shutting Down a DdManager
337	</H2>
338
339	<P>
340	To use the functions in the CUDD package, one has first to initialize
341	the 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
343	parameters:
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 <A HREF="node3.html#sec:basicZDD">3.9</A> and <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>
386	A typical call to <A NAME="tex2html12"
387	HREF="cuddExtDet.html#Cudd_Init"><EM>Cudd_Init</EM></A><A NAME="1437"></A> may look
388	like this:
389	<PRE>
390	manager = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);
391	</PRE>
392	To reclaim all the memory associated with a manager, an application
393	must call <A NAME="tex2html13"
394	HREF="cuddExtDet.html#Cudd_Quit"><EM>Cudd_Quit</EM></A><A NAME="1439"></A>. This is normally
395	done before exiting.
396
397	<P>
398
399	<H2><A NAME="SECTION00034000000000000000"></A>
400	<A NAME="sec:params"></A>
401	<BR>
402	Setting Parameters
403	</H2>
404
405	<P>
406	The package provides several functions to set the parameters that
407	control various functions. For instance, the package has an automatic
408	way of determining whether a larger unique<A NAME="187"></A> table
409	would make the application run faster. In that case, the package
410	enters a ``fast growth<A NAME="188"></A>" mode in which resizing of
411	the unique subtables is favored over garbage<A NAME="189"></A>
412	collection. When the unique table reaches a given size, however, the
413	package returns to the normal ``slow growth" mode, even though the
414	conditions that caused the transition to fast growth still prevail.
415	The 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
417	by <A NAME="tex2html15"
418	HREF="cuddExtDet.html#Cudd_SetLooseUpTo"><EM>Cudd_SetLooseUpTo</EM></A><A NAME="1443"></A>. Similar
419	pairs of functions exist for several other parameters. See also
420	Section <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>
427	Constant Functions
428	</H2>
429
430	<P>
431	The CUDD Package defines several constant functions. These functions
432	are created when the manager<A NAME="201"></A> is initialized, and are accessible
433	through 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>
440	One, Logic Zero, and Arithmetic Zero
441	</H3>
442
443	<P>
444	The 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,
446	ADDs, and ZDDs. However, its meaning is different for ADDs and BDDs,
447	on the one hand, and ZDDs, on the other hand. The diagram consisting
448	of the constant 1 node only represents the constant 1 function for
449	ADDs and BDDs. For ZDDs, its meaning depends on the number of
450	variables: It is the conjunction of the complements of all variables.
451	Conversely, the representation of the constant 1 function depends on
452	the 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
456	returned by <A NAME="tex2html17"
457	HREF="cuddExtDet.html#Cudd_ReadZddOne"><EM>Cudd_ReadZddOne</EM></A><A NAME="1447"></A>.
458
459	<P>
460	The constant 0 is common to ADDs and ZDDs, but not to BDDs. The
461	BDD<A NAME="213"></A> logic 0 is <B>not</B> associated
462	with 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
464	returned by <A NAME="tex2html19"
465	HREF="cuddExtDet.html#Cudd_ReadLogicZero"><EM> Cudd_ReadLogicZero</EM></A><A NAME="1451"></A>.) All
466	other constants are specific to ADDs.
467
468	<P>
469
470	<H3><A NAME="SECTION00035200000000000000"></A>
471	<A NAME="sec:predef-const"></A>
472	<BR>
473	Predefined Constants
474	</H3>
475
476	<P>
477	Besides 0 (returned by <A NAME="tex2html20"
478	HREF="cuddExtDet.html#Cudd_ReadZero"><EM>Cudd_ReadZero</EM></A><A NAME="1453"></A>)
479	and 1, the following constant<A NAME="226"></A> functions are
480	created 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
511	modified by calling <A NAME="tex2html24"
512	HREF="cuddExtDet.html#Cudd_SetEpsilon"><EM> Cudd_SetEpsilon</EM></A><A NAME="1461"></A>. Unlike the other
513
514	constants, 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>
523	Background
524	</H3>
525
526	<P>
527	The background value is a constant<A NAME="256"></A> typically used
528	to represent non-existing arcs in graphs. Consider a shortest path
529	problem. Two nodes that are not connected by an arc can be regarded as
530	being joined by an arc<A NAME="257"></A> of infinite length. In
531	shortest path problems, it is therefore convenient to set the
532	background value to PlusInfinity<A NAME="258"></A>. In network flow
533	problems, on the other hand, two nodes not connected by an arc can be
534	regarded as joined by an arc<A NAME="259"></A> of 0 capacity.
535	For these problems, therefore, it is more convenient to set the
536	background value to 0. In general, when representing
537	sparse<A NAME="260"></A> matrices, the background value is the value that
538	is assumed implicitly.
539
540	<P>
541	At initialization, the background value is set to 0. It can be read
542	with <A NAME="tex2html25"
543	HREF="cuddExtDet.html#Cudd_ReadBackground"><EM>Cudd_ReadBackground</EM></A><A NAME="1463"></A>,
544	and modified with <A NAME="tex2html26"
545	HREF="cuddExtDet.html#Cudd_SetBackground"><EM>Cudd_SetBackground</EM></A>. The background value
546	affects 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
549	print out sum-of-product<A NAME="272"></A> expressions
550	for ADDs (<A NAME="tex2html29"
551	HREF="cuddExtDet.html#Cudd_PrintMinterm"><EM> Cudd_PrintMinterm</EM></A><A NAME="1469"></A>), generators
552	of cubes (<A NAME="tex2html30"
553	HREF="cuddExtDet.html#Cudd_ForeachCube"><EM>Cudd_ForeachCube</EM></A><A NAME="1471"></A>),
554	and 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>
562	New Constants
563	</H3>
564
565	<P>
566	New 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
568	retrieve the ADD<A NAME="289"></A> for the desired
569	constant, if it already exist, or it will create a new one. Obviously,
570	new 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>
577	Creating Variables
578	</H2>
579
580	<P>
581	Decision diagrams are typically created by combining simpler decision
582	diagrams. The simplest decision diagrams, of course, cannot be created
583	in that way. Constant functions have been discussed in
584	Section <A HREF="node3.html#sec:const">3.5</A>. In this section we discuss the simple
585	variable 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>
592	New BDD and ADD Variables
593	</H3>
594
595	<P>
596	The projection<A NAME="296"></A> functions are distinct for
597	BDDs and ADDs. A projection function for BDDs consists of an internal
598	node with both outgoing arcs pointing to the constant 1. The <EM> else</EM> arc<A NAME="298"></A> is complemented.
599
600	<P>
601	An ADD projection function, on the other hand, has the <EM>else</EM>
602	pointer directed to the arithmetic<A NAME="300"></A> zero
603	function. One should never mix the two types of variables. BDD
604	variables should be used when manipulating BDDs, and ADD variables
605	should be used when manipulating ADDs. Three functions are provided
606	to 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
612	the 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
621	new 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
627	Similar to <A NAME="tex2html36"
628	HREF="cuddExtDet.html#Cudd_bddNewVar"><EM>Cudd_bddNewVar</EM></A><A NAME="1483"></A>. In
629
630	addition 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
635	variable at the end of the order.
636	</LI>
637	</UL>
638	The 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>
648	New ZDD Variables
649	</H3>
650
651	<P>
652	Unlike the projection functions of BDDs and ADDs, the
653	projection<A NAME="333"></A> functions of ZDDs have diagrams
654	with <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
661	ZDDs of the projection functions change when new variables are added.
662	This will be discussed in Section <A HREF="node3.html#sec:basicZDD">3.9</A>. Here we assume
663	that 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
667	projection 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>
675	Basic BDD Manipulation
676	</H2>
677
678	<P>
679	Common 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$">,
690	as 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
697	functions 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
699	be explicitly referenced by the caller. <A NAME="tex2html44"
700	HREF="cuddExtDet.html#Cudd_bddIte"><EM>Cudd_bddIte</EM></A>
701	can be
702	used to implement all two-argument boolean functions. However, the
703	package also provides <A NAME="tex2html45"
704	HREF="cuddExtDet.html#Cudd_bddAnd"><EM>Cudd_bddAnd</EM></A><A NAME="1497"></A>
705	as well as the other two-operand boolean functions, which are slightly
706	more efficient when a two-operand function is called for. The
707	following fragment of code illustrates how to build the BDD for the
708	function <!-- 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 >= 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>
732	This 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
744	to <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
767	careful, 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>
778	Basic ADD Manipulation
779	</H2>
780
781	<P>
782	The 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
784	apply a wide variety of operators to a pair of ADDs. Among the
785	available operators are addition, multiplication, division, minimum,
786	maximum, and boolean operators that work on ADDs whose leaves are
787	restricted to 0 and 1 (0-1 ADDs).
788
789	<P>
790	The following fragment of code illustrates how to build the ADD for
791	the 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 >= 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>
817	This example, contrasted to the example of BDD manipulation,
818	illustrates 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
830	is 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
834	sufficient 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>
843	Basic ZDD Manipulation
844	</H2>
845
846	<P>
847	ZDDs are often generated by converting<A NAME="406"></A>
848	existing BDDs. (See Section <A HREF="node3.html#sec:convertZ">3.11</A>.) However, it is also
849	possible to build ZDDs by applying boolean operators to other ZDDs,
850	starting from constants and projection<A NAME="408"></A>
851	functions. The following fragment of code illustrates how to build
852	the 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
859	four 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
863	built. 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 >= 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>
888	This 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
900	require referencing.
901	</LI>
902	</UL>
903	CUDD provides functions for the manipulation of
904	covers<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
906	representing an irredundant<A NAME="421"></A> sum of
907	products for the incompletely specified function defined by the two
908	BDDs <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
916	division of two covers given as ZDDs. These functions expect the two
917	ZDD variables corresponding to the two literals of the function variable
918	to be adjacent. One has to create variable groups (see
919	Section <A HREF="node3.html#sec:reordZ">3.14</A>) for reordering<A NAME="426"></A> of
920	the ZDD variables to work. BDD automatic reordering is safe even
921	without groups: If realignment of ZDD and ADD/BDD variables is requested
922	(see Section <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>
930	Converting ADDs to BDDs and Vice Versa
931	</H2>
932
933	<P>
934	Several procedures are provided to convert ADDs to BDDs, according to
935	different 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
939	conversion 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
941	simple principle of mapping the logical 0<A NAME="444"></A> and 1 on
942	the arithmetic<A NAME="445"></A> 0 and 1. It is also possible to
943	convert an ADD with integer values (more precisely, floating point
944	numbers with 0 fractional part) to an array of BDDs by repeatedly
945	calling <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>
954	Converting BDDs to ZDDs and Vice Versa
955	</H2>
956
957	<P>
958	Many applications first build a set of BDDs and then derive ZDDs from
959	the BDDs. These applications should create the manager with 0
960	ZDD<A NAME="453"></A> variables and
961	create 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
963	create the necessary ZDD variables--whose number is likely to be
964	known once the BDDs are available. This approach eliminates the
965	difficulties that arise when the number of ZDD variables changes while
966	ZDDs are being built.
967
968	<P>
969	The simplest conversion from BDDs to ZDDs is a simple change of
970	representation, which preserves the functions. Simply put, given a BDD
971	for <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
978	between 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>
980	should be called with the <EM> multiplicity</EM> parameter equal to 1. The conversion proper can then
981	be performed by calling <A NAME="tex2html64"
982	HREF="cuddExtDet.html#Cudd_zddPortFromBdd"><EM> Cudd_zddPortFromBdd</EM></A><A NAME="1533"></A>. The
983	inverse 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>
987	ZDDs are quite often used for the representation of <EM> covers</EM><A NAME="467"></A>. This is normally done by associating
988	two ZDD variables to each variable of the function. (And hence,
989	typically, to each BDD variable.) One ZDD variable is associated with
990	the positive literal of the BDD variable, while the other ZDD variable
991	is 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>
993	with <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>
1006	If a BDD variable group tree exists when <A NAME="tex2html67"
1007	HREF="cuddExtDet.html#Cudd_zddVarsFromBddVars"><EM> Cudd_zddVarsFromBddVars</EM></A>
1008	is called (see Section <A HREF="node3.html#sec:group">3.13</A>)
1009	the function generates a ZDD variable group tree consistent to it. In
1010	any case, all the ZDD variables derived from the same BDD variable are
1011	clustered into a group.
1012
1013	<P>
1014	If 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
1018	the manager, the function represented by the existing ZDD changes.
1019	Suppose, for instance, that two variables are initially created, and
1020	that 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
1024	added, 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'$">
1034	instead. This change in function obviously applies regardless of what
1035	use is made of the ZDD. However, if the ZDD is used to represent a
1036	cover<A NAME="475"></A>, the cover itself is not changed by the
1037	addition of new variable. (What changes is the
1038	characteristic<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>
1045	Variable Reordering for BDDs and ADDs
1046	</H2>
1047
1048	<P>
1049	The CUDD package provides a rich set of
1050	dynamic<A NAME="480"></A> reordering algorithms. Some of them
1051	are 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
1059	others 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>
1065	Reordering affects a unique<A NAME="483"></A> table. This means that
1066	BDDs and ADDs, which share the same unique table are simultaneously
1067	reordered. ZDDs, on the other hand, are reordered separately. In the
1068	following we discuss the reordering of BDDs and ADDs. Reordering for
1069	ZDDs is the subject of Section <A HREF="node3.html#sec:reordZ">3.14</A>.
1070
1071	<P>
1072	Reordering of the variables can be invoked directly by the application
1073	by calling <A NAME="tex2html68"
1074	HREF="cuddExtDet.html#Cudd_ReduceHeap"><EM>Cudd_ReduceHeap</EM></A><A NAME="1539"></A>. Or it
1075	can be automatically triggered by the package when the number of nodes
1076	has reached a given threshold<A NAME="488"></A>. (The
1077	threshold is initialized and automatically adjusted after each
1078	reordering by the package.) To enable automatic dynamic reordering
1079	(also called <EM>asynchronous<A NAME="489"></A></EM>
1080	dynamic 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
1082	dynamic 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>
1086	All reordering methods are available in both the case of direct call
1087	to <A NAME="tex2html71"
1088	HREF="cuddExtDet.html#Cudd_ReduceHeap"><EM>Cudd_ReduceHeap</EM></A><A NAME="1545"></A> and the case of
1089	automatic invocation. For many methods, the reordering procedure is
1090	iterated until no further improvement is obtained. We call these
1091	methods the <EM>converging<A NAME="499"></A></EM> methods.
1092	When constraints are imposed on the relative position of variables
1093	(see Section <A HREF="node3.html#sec:group">3.13</A>) the reordering methods apply inside the
1094	groups. The groups<A NAME="501"></A> themselves are reordered by
1095	sifting<A NAME="502"></A>. Each method is identified by a
1096	constant of the enumerated type <EM> Cudd_ReorderingType<A NAME="503"></A></EM>
1097	defined in <EM>cudd.h<A NAME="504"></A></EM> (the external
1098	header<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
1111	method 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
1115	this 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>
1144	In 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
1149	with <A NAME="tex2html75"
1150	HREF="cuddExtDet.html#Cudd_SetSiftMaxVar"><EM>Cudd_SetSiftMaxVar</EM></A><A NAME="1553"></A>. In
1151
1152	addition, 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
1159	set 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
1165	CUDD_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
1178	to 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>
1252	So far we have described methods whereby the package selects an order
1253	automatically. A given order of the variables can also be imposed by
1254	calling <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>
1262	Grouping Variables
1263	</H2>
1264
1265	<P>
1266	CUDD allows the application to specify constraints on the positions of
1267	group of variables. It is possible to request that a group of
1268	contiguous variables be kept contiguous by the reordering procedures.
1269	It is also possible to request that the relative order of some groups
1270	of variables be left unchanged. The constraints on the order are
1271	specified by means of a tree<A NAME="576"></A>, which is created in
1272	one 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
1284	current 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>
1290	Each node in the tree represents a range of variables. The lower bound
1291	of the range is given by the <EM>low</EM> field of the node, and the
1292	size of the group is given by the <EM>size</EM> field of the
1293	node.<A NAME="tex2html80"
1294	HREF="footnode.html#foot1315"><SUP>2</SUP></A> The variables in
1295	each range are kept contiguous. Furthermore, if a node is marked with
1296	the MTR_FIXED<A NAME="593"></A> flag, then the relative order of the
1297	variable ranges associated to its children is not changed. As an
1298	example, suppose the initial variable order is:
1299	<PRE>
1300	x0, y0, z0, x1, y1, z1, ... , x9, y9, z9.
1301	</PRE>
1302	Suppose we want to keep each group of three variables with the same
1303	index (e.g., <code>x3, y3, z3</code>) contiguous, while allowing the package
1304	to change the order of the groups. We can accomplish this with the
1305	following code:
1306	<PRE>
1307	for (i = 0; i < 10; i++) {
1308	(void) Cudd_MakeTreeNode(manager,i*3,3,MTR_DEFAULT);
1309	}
1310	</PRE>
1311	If we want to keep the order within each group of variables
1312	fixed (i.e., <code>x</code> before <code>y</code> before <code>z</code>) we need to
1313	change MTR_DEFAULT<A NAME="598"></A> into MTR_FIXED.
1314
1315	<P>
1316	The <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
1318	of a variable (as opposed to its level or position in the order). The
1319	group tree<A NAME="603"></A> can be created at any time. The result
1320	obviously depends on the variable order in effect at creation time.
1321
1322	<P>
1323	It is possible to create a variable group tree also before the
1324	variables themselves are created. The package assumes in this case
1325	that the index of the variables not yet in existence will equal their
1326	position in the order when they are created. Therefore, applications
1327	that 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
1331	create new variables have to create the variables before they group
1332	them.
1333
1334	<P>
1335	The reordering procedure will skip all groups whose variables are not
1336	yet in existence. For groups that are only partially in existence, the
1337	reordering procedure will try to reorder the variables already
1338	instantiated, 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>
1345	Variable Reordering for ZDDs
1346	</H2>
1347
1348	<P>
1349	Reordering of ZDDs is done in much the same way as the reordering of
1350	BDDs and ADDs. The functions corresponding to <A NAME="tex2html87"
1351	HREF="cuddExtDet.html#Cudd_ReduceHeap"><EM>Cudd_ReduceHeap</EM></A>
1352	and <A NAME="tex2html88"
1353	HREF="cuddExtDet.html#Cudd_ShuffleHeap"><EM>Cudd_ShuffleHeap</EM></A>
1354	are <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
1357	dynamic<A NAME="623"></A> reordering, the application must
1358	call <A NAME="tex2html91"
1359	HREF="cuddExtDet.html#Cudd_AutodynEnableZdd"><EM>Cudd_AutodynEnableZdd</EM></A><A NAME="1579"></A>,
1360	and 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
1362	the current implementation, however, the choice of reordering methods
1363	for 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>
1394	To 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>
1402	Keeping Consistent Variable Orders for BDDs and ZDDs
1403	</H2>
1404
1405	<P>
1406	Several applications that manipulate both BDDs and ZDDs benefit from
1407	keeping a fixed correspondence between the order of the BDD variables
1408	and the order of the ZDD variables. If each BDD variable corresponds
1409	to a group of ZDD variables, then it is often desirable that the
1410	groups of ZDD variables be in the same order as the corresponding BDD
1411	variables. CUDD allows the ZDD order to
1412	track the BDD order and vice versa. To have the ZDD order track
1413	the BDD order, the application calls <A NAME="tex2html94"
1414	HREF="cuddExtDet.html#Cudd_zddRealignEnable"><EM> Cudd_zddRealignEnable</EM></A><A NAME="1585"></A>. The
1415	effect 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
1417	ZDD realignment is in effect, automatic reordering of ZDDs should be
1418	disabled.
1419
1420	<P>
1421
1422	<H2><A NAME="SECTION000316000000000000000"></A>
1423	<A NAME="652"></A><A NAME="sec:hooks"></A>
1424	<BR>
1425	Hooks
1426	</H2>
1427
1428	<P>
1429	Hooks in CUDD are lists of application-specified functions to be run on
1430	certain occasions. Each hook is identified by a constant of the
1431	enumerated type <A NAME="tex2html96"
1432	HREF="cuddExtDet.html#Cudd_HookType"><EM>Cudd_HookType</EM></A><A NAME="1589"></A>. In Version
1433	2.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>
1445	The current implementation of hooks is experimental. A function added
1446	to a hook receives a pointer to the manager, a pointer to a constant
1447	string, and a pointer to void as arguments; it must return 1 if
1448	successful; 0 otherwise. The second argument is one of ``DD,''
1449	``BDD,'' and ``ZDD.'' This allows the hook functions to tell the type
1450	of diagram for which reordering or garbage collection takes place. The
1451	third argument varies depending on the hook. The hook functions called
1452	before or after garbage collection<A NAME="659"></A> do
1453	not use it. The hook functions called before
1454	reordering<A NAME="660"></A> are passed, in addition to the
1455	pointer to the manager, also the method used for reordering. The hook
1456	functions called after reordering are passed the start time. To add a
1457	function 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
1459	are called in the order in which they were added to the hook. For
1460	sample 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>
1469	The SIS/VIS Interface
1470	</H2>
1471
1472	<P>
1473	The CUDD package contains interface functions that emulate the
1474	behavior of the original BDD package used in SIS [<A
1475	HREF="node7.html#Sentov92">17</A>] and
1476	in 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
1481	in 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>
1488	Using the CUDD Package in SIS
1489	</H3>
1490
1491	<P>
1492	This 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
1494	hierarchy where the sources for SIS reside. Let <TT> CUDDDIR<A NAME="680"></A></TT> be the root of the directory hierarchy where
1495	the distribution of the CUDD package resides. To build SIS with the
1496	CUDD 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>
1541	The replacement for the <TT>st</TT> library is because the version
1542	shipped with the CUDD package tests for out-of-memory conditions.
1543	Notice that the version of the <TT>st</TT> library to be used for
1544	replacement is not the one used for the normal build, because the
1545	latter has been modified for C++ compatibility. The above installation
1546	procedure has been tested on SIS 1.3. SIS can be obtained via
1547	anonymous 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
1549	1.3, you need <TT>sis-1.2.tar.Z</TT> and <TT>sis-1.2.patch1.Z</TT>. When
1550	compiling on a DEC Alpha<A NAME="747"></A>, you should add the <TT> -ieee_with_no_inexact</TT> flag. (See
1551	Section <A HREF="node3.html#sec:predef-const">3.5.2</A>.) Refer to the <TT>Makefile</TT> in the
1552	top level directory of the distribution for how to compile with 32-bit
1553	pointers.
1554
1555	<P>
1556
1557	<H2><A NAME="SECTION000318000000000000000"></A>
1558	<A NAME="sec:dump"></A>
1559	<BR>
1560	Writing Decision Diagrams to a File
1561	</H2>
1562
1563	<P>
1564	The CUDD package provides several functions to write decision diagrams
1565	to a file. <A NAME="tex2html101"
1566	HREF="cuddExtDet.html#Cudd_DumpBlif"><EM>Cudd_DumpBlif</EM></A><A NAME="1597"></A> writes a
1567	file in <EM>blif</EM> format. It is restricted to BDDs. The diagrams
1568	are written as a network of multiplexers, one multiplexer for each
1569	internal 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
1574	the 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>
1577	written by
1578	Eleftherios Koutsofios and Stephen C. North. An example of drawing
1579	produced by dot from the output of <A NAME="tex2html104"
1580	HREF="cuddExtDet.html#Cudd_DumpDot"><EM>Cudd_DumpDot</EM></A>
1581	is shown in
1582	Figure <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>
1588	A 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>
1605	for 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
1610	the 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>
1613	developed
1614	at the University of Bremen. It is restricted to BDDs and ADDs.
1615
1616	<P>
1617	Functions are also available to produce the input format of <EM> DDcal</EM> (see Section <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>
1624	Saving and Restoring BDDs
1625	</H2>
1626
1627	<P>
1628	The <A NAME="tex2html109"
1629	HREF="ftp://ftp.polito.it/pub/research/dddmp/"><EM>dddmp</EM></A>
1630	library<A NAME="789"></A> by Gianpiero Cabodi and
1631	Stefano Quer allows a CUDD application to save BDDs to disk in compact
1632	form for later retrieval. See the library's own documentation for the
1633	details.
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>
1665	Fabio Somenzi
1666	2005-05-17
1667	</ADDRESS>
1668	</BODY>
1669	</HTML>

Note: See TracBrowser for help on using the repository browser.

Context Navigation

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

Download in other formats: