<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
<!--Converted with LaTeX2HTML 2K.1beta (1.47)
original version by: Nikos Drakos, CBLU, University of Leeds
* revised and updated by: Marcus Hennecke, Ross Moore, Herb Swan
* with significant contributions from:
Jens Lippmann, Marek Rouchal, Martin Wilck and others -->
<HTML>
<HEAD>
<TITLE>User's Manual</TITLE>
<META NAME="description" CONTENT="User's Manual">
<META NAME="keywords" CONTENT="cuddIntro">
<META NAME="resource-type" CONTENT="document">
<META NAME="distribution" CONTENT="global">
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
<META NAME="Generator" CONTENT="LaTeX2HTML v2K.1beta">
<META HTTP-EQUIV="Content-Style-Type" CONTENT="text/css">
<LINK REL="STYLESHEET" HREF="cuddIntro.css">
<LINK REL="next" HREF="node4.html">
<LINK REL="previous" HREF="node2.html">
<LINK REL="up" HREF="cuddIntro.html">
<LINK REL="next" HREF="node4.html">
</HEAD>
<BODY >
<!--Navigation Panel-->
<A NAME="tex2html272"
HREF="node4.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="icons/next.png"></A>
<A NAME="tex2html268"
HREF="cuddIntro.html">
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="icons/up.png"></A>
<A NAME="tex2html262"
HREF="node2.html">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="icons/prev.png"></A>
<A NAME="tex2html270"
HREF="node8.html">
<IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
SRC="icons/index.png"></A>
<BR>
<B> Next:</B> <A NAME="tex2html273"
HREF="node4.html">Programmer's Manual</A>
<B> Up:</B> <A NAME="tex2html269"
HREF="cuddIntro.html">CUDD: CU Decision Diagram</A>
<B> Previous:</B> <A NAME="tex2html263"
HREF="node2.html">How to Get CUDD</A>
  <B> <A NAME="tex2html271"
HREF="node8.html">Index</A></B>
<BR>
<BR>
<!--End of Navigation Panel-->
<!--Table of Child-Links-->
<A NAME="CHILD_LINKS"><STRONG>Subsections</STRONG></A>
<UL>
<LI><A NAME="tex2html274"
HREF="#SECTION00031000000000000000">Compiling and Linking</A>
<LI><A NAME="tex2html275"
HREF="#SECTION00032000000000000000">Basic Data Structures</A>
<UL>
<LI><A NAME="tex2html276"
HREF="#SECTION00032100000000000000">Nodes</A>
<LI><A NAME="tex2html277"
HREF="#SECTION00032200000000000000">The Manager</A>
<LI><A NAME="tex2html278"
HREF="#SECTION00032300000000000000">Cache</A>
</UL>
<BR>
<LI><A NAME="tex2html279"
HREF="#SECTION00033000000000000000">Initializing and Shutting Down a DdManager</A>
<LI><A NAME="tex2html280"
HREF="#SECTION00034000000000000000">Setting Parameters</A>
<LI><A NAME="tex2html281"
HREF="#SECTION00035000000000000000">Constant Functions</A>
<UL>
<LI><A NAME="tex2html282"
HREF="#SECTION00035100000000000000">One, Logic Zero, and Arithmetic Zero</A>
<LI><A NAME="tex2html283"
HREF="#SECTION00035200000000000000">Predefined Constants</A>
<LI><A NAME="tex2html284"
HREF="#SECTION00035300000000000000">Background</A>
<LI><A NAME="tex2html285"
HREF="#SECTION00035400000000000000">New Constants</A>
</UL>
<BR>
<LI><A NAME="tex2html286"
HREF="#SECTION00036000000000000000">Creating Variables</A>
<UL>
<LI><A NAME="tex2html287"
HREF="#SECTION00036100000000000000">New BDD and ADD Variables</A>
<LI><A NAME="tex2html288"
HREF="#SECTION00036200000000000000">New ZDD Variables</A>
</UL>
<BR>
<LI><A NAME="tex2html289"
HREF="#SECTION00037000000000000000">Basic BDD Manipulation</A>
<LI><A NAME="tex2html290"
HREF="#SECTION00038000000000000000">Basic ADD Manipulation</A>
<LI><A NAME="tex2html291"
HREF="#SECTION00039000000000000000">Basic ZDD Manipulation</A>
<LI><A NAME="tex2html292"
HREF="#SECTION000310000000000000000">Converting ADDs to BDDs and Vice Versa</A>
<LI><A NAME="tex2html293"
HREF="#SECTION000311000000000000000">Converting BDDs to ZDDs and Vice Versa</A>
<LI><A NAME="tex2html294"
HREF="#SECTION000312000000000000000">Variable Reordering for BDDs and ADDs</A>
<LI><A NAME="tex2html295"
HREF="#SECTION000313000000000000000">Grouping Variables</A>
<LI><A NAME="tex2html296"
HREF="#SECTION000314000000000000000">Variable Reordering for ZDDs</A>
<LI><A NAME="tex2html297"
HREF="#SECTION000315000000000000000">Keeping Consistent Variable Orders for BDDs and ZDDs</A>
<LI><A NAME="tex2html298"
HREF="#SECTION000316000000000000000">Hooks</A>
<LI><A NAME="tex2html299"
HREF="#SECTION000317000000000000000">The SIS/VIS Interface</A>
<UL>
<LI><A NAME="tex2html300"
HREF="#SECTION000317100000000000000">Using the CUDD Package in SIS</A>
</UL>
<BR>
<LI><A NAME="tex2html301"
HREF="#SECTION000318000000000000000">Writing Decision Diagrams to a File</A>
<LI><A NAME="tex2html302"
HREF="#SECTION000319000000000000000">Saving and Restoring BDDs</A>
</UL>
<!--End of Table of Child-Links-->
<HR>
<H1><A NAME="SECTION00030000000000000000"></A>
<A NAME="sec:user"></A>
<BR>
User's Manual
</H1>
<P>
This section describes the use of the CUDD package as a black box.
<P>
<H2><A NAME="SECTION00031000000000000000"></A>
<A NAME="sec:compileExt"></A><A NAME="78"></A>
<BR>
Compiling and Linking
</H2>
<P>
To build an application that uses the CUDD package, you should add
<PRE>
#include "util.h"
#include "cudd.h"
</PRE>
<A NAME="81"></A>
to your source files, and should link
<code>libcudd.a</code><A NAME="82"></A>,
<code>libmtr.a</code><A NAME="83"></A>,
<code>libst.a</code><A NAME="84"></A>, and
<code>libutil.a</code><A NAME="85"></A> to your executable. (All these
libraries are part of the distribution.) Some
platforms require specific compiler and linker flags. Refer to the
<TT>Makefile<A NAME="86"></A></TT> in the top level directory of the
distribution.
<P>
Keep in mind that whatever flags affect the size of data
structures--for instance the flags used to use 64-bit pointers where
available--must be specified when compiling both CUDD and the files
that include its header files.
<P>
<H2><A NAME="SECTION00032000000000000000"></A>
<A NAME="sec:struct"></A>
<BR>
Basic Data Structures
</H2>
<P>
<H3><A NAME="SECTION00032100000000000000"></A>
<A NAME="sec:nodes"></A>
<BR>
Nodes
</H3>
<P>
BDDs, ADDs, and ZDDs are made of DdNode's. A DdNode<A NAME="91"></A>
(node<A NAME="92"></A> for short) is a structure with several fields. Those
that are of interest to the application that uses the CUDD package as
a black box are the variable index<A NAME="93"></A>, the
reference<A NAME="94"></A> count, and the value. The
remaining fields are pointers that connect nodes among themselves and
that are used to implement the unique<A NAME="95"></A> table. (See
Section <A HREF="node3.html#sec:manager">3.2.2</A>.)
<P>
The <EM>index</EM> field holds the name of the variable that labels the
node. The index of a variable is a permanent attribute that reflects
the order<A NAME="98"></A> of creation. Index 0 corresponds to
the variable created first. On a machine with 32-bit pointers, the
maximum number of variables is the largest value that can be stored in
an unsigned short integer minus 1. The largest index is reserved for
the constant<A NAME="99"></A> nodes. When 64-bit pointers are
used, the maximum number of variables is the largest value that can be
stored in an unsigned integer minus 1.
<P>
When variables are reordered to reduce the size of the decision
diagrams, the variables may shift in the order, but they retain their
indices. The package keeps track of the variable
permutation<A NAME="100"></A> (and its inverse). The
application is not affected by variable reordering<A NAME="101"></A>,
except in the following cases.
<UL>
<LI>If the application uses
generators<A NAME="103"></A> (<A NAME="tex2html3"
HREF="cuddExtDet.html#Cudd_ForeachCube"><EM>Cudd_ForeachCube</EM></A>
<A NAME="1423"></A> and <A NAME="tex2html4"
HREF="cuddExtDet.html#Cudd_ForeachNode"><EM>Cudd_ForeachNode</EM></A>
<A NAME="1425"></A>) and reordering is enabled, then it
must take care not to call any operation that may create new nodes
(and hence possibly trigger reordering). This is because the cubes
(i.e., paths) and nodes of a diagram change as a result of reordering.
</LI>
<LI>If the application uses <A NAME="tex2html5"
HREF="cuddExtDet.html#Cudd_bddConstrain"><EM> Cudd_bddConstrain</EM></A><A NAME="1427"></A> and reordering
takes place, then the property of <A NAME="tex2html6"
HREF="cuddExtDet.html#Cudd_bddConstrain"><EM>Cudd_bddConstrain</EM></A>
of being an
image restrictor is lost.
</LI>
</UL>
<P>
The CUDD package relies on garbage<A NAME="116"></A>
collection to reclaim the memory used by diagrams that are no longer
in use. The scheme employed for garbage collection is based on keeping
a reference<A NAME="117"></A> count for each node. The
references that are counted are both the internal references
(references from other nodes) and external references (typically
references from the calling environment). When an application creates
a new BDD<A NAME="118"></A>, ADD<A NAME="119"></A>, or ZDD<A NAME="120"></A>,
it must increase its reference count explicitly, through
a call to <A NAME="tex2html7"
HREF="cuddExtDet.html#Cudd_Ref"><EM>Cudd_Ref</EM></A><A NAME="1429"></A>. Similarly, when a
diagram is no longer needed, the application must call <A NAME="tex2html8"
HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A><A NAME="1431"></A> (for BDDs
and ADDs) or <A NAME="tex2html9"
HREF="cuddExtDet.html#Cudd_RecursiveDerefZdd"><EM> Cudd_RecursiveDerefZdd</EM></A><A NAME="1433"></A>
(for ZDDs) to ``recycle<A NAME="130"></A>" the nodes of the
diagram.
<P>
Terminal<A NAME="131"></A> nodes carry a value. This is especially
important for ADDs. By default, the value is a double<A NAME="132"></A>.
To change to something different (e.g., an integer), the
package must be modified and recompiled. Support for this process is
currently very rudimentary.
<P>
<H3><A NAME="SECTION00032200000000000000"></A>
<A NAME="134"></A><A NAME="sec:manager"></A>
<BR>
The Manager
</H3>
<P>
All nodes used in BDDs, ADDs, and ZDDs are kept in special
hash<A NAME="136"></A> tables called the <EM> unique<A NAME="137"></A> tables</EM>. Specifically, BDDs and ADDs
share the same unique table, whereas ZDDs have their own table. As
the name implies, the main purpose of the unique table is to guarantee
that each node is unique; that is, there is no other node labeled by
the same variable and with the same children. This uniqueness property
makes decision diagrams canonical<A NAME="138"></A>. The
unique<A NAME="139"></A> tables and some auxiliary data structures
make up the DdManager<A NAME="140"></A> (manager<A NAME="141"></A> for
short). Though the application that uses only the exported functions
needs not be concerned with most details of the manager, it has to
deal with the manager in the following sense. The application must
initialize the manager by calling an appropriate function. (See
Section <A HREF="node3.html#sec:init">3.3</A>.) Subsequently, it must pass a pointer to the
manager to all the functions that operate on decision diagrams.
<P>
With the exception of a few statistical counters<A NAME="143"></A>, there are no global<A NAME="144"></A> variables in
the CUDD package. Therefore, it is quite possible to have multiple
managers simultaneously active in the same application.<A NAME="tex2html10"
HREF="footnode.html#foot145"><SUP>1</SUP></A> It is the pointers to
the managers that tell the functions on what data they should operate.
<P>
<H3><A NAME="SECTION00032300000000000000"></A>
<A NAME="147"></A><A NAME="sec:memoize"></A>
<BR>
Cache
</H3>
<P>
Efficient recursive manipulation of decision diagrams requires the use
of a table to store computed results. This table<A NAME="149"></A>
is called here the <EM>cache<A NAME="150"></A></EM> because it is
effectively handled like a cache of variable but limited capacity. The
CUDD package starts by default with a small cache, and increases its
size until either no further benefit is achieved, or a limit size is
reached. The user can influence this policy by choosing initial and
limit values for the cache size.
<P>
Too small a cache will cause frequent overwriting of useful results.
Too large a cache will cause overhead, because the whole cache is
scanned every time garbage<A NAME="151"></A> collection takes
place. The optimal parameters depend on the specific application. The
default parameters work reasonably well for a large spectrum of
applications.
<P>
The cache<A NAME="152"></A> of the CUDD package is used by most recursive
functions of the package, and can be used by user-supplied functions
as well. (See Section <A HREF="node4.html#sec:cache">4.4</A>.)
<P>
<H2><A NAME="SECTION00033000000000000000"></A>
<A NAME="155"></A><A NAME="sec:init"></A>
<BR>
Initializing and Shutting Down a DdManager
</H2>
<P>
To use the functions in the CUDD package, one has first to initialize
the package itself by calling <A NAME="tex2html11"
HREF="cuddExtDet.html#Cudd_Init"><EM> Cudd_Init</EM></A><A NAME="1435"></A>. This function takes four
parameters:
<UL>
<LI>numVars<A NAME="161"></A>: It is the initial number of variables
for BDDs and ADDs. If the total number of variables needed by the
application is known, then it is slightly more efficient to create a
manager with that number of variables. If the number is unknown, it
can be set to 0, or to any other lower bound on the number of
variables. Requesting more variables than are actually needed is
not incorrect, but is not efficient.
</LI>
<LI>numVarsZ<A NAME="162"></A>: It is the initial number of variables
for ZDDs. See Sections <A HREF="node3.html#sec:basicZDD">3.9</A> and <A HREF="node3.html#sec:convertZ">3.11</A> for
a discussion of the value of this argument.
</LI>
<LI>numSlots<A NAME="165"></A>: Determines the initial size of each
subtable<A NAME="166"></A> of the unique<A NAME="167"></A> table.
There is a subtable for each variable. The size of each subtable is
dynamically adjusted to reflect the number of nodes. It is normally
O.K. to use the default value for this parameter, which is
CUDD_UNIQUE_SLOTS<A NAME="168"></A>.
</LI>
<LI>cacheSize<A NAME="169"></A>: It is the initial size (number of
entries) of the cache<A NAME="170"></A>. Its default value is
CUDD_CACHE_SLOTS<A NAME="171"></A>.
</LI>
<LI>maxMemory<A NAME="172"></A>: It is the target value for the
maximum memory occupation (in bytes). The package uses this value to
decide two parameters.
<UL>
<LI>the maximum size to which the cache will grow, regardless of
the hit rate or the size of the unique<A NAME="174"></A> table.
</LI>
<LI>the maximum size to which growth of the unique table will be
preferred to garbage collection.
</LI>
</UL>
If maxMemory is set to 0, CUDD tries to guess a good value based on
the available memory.
</LI>
</UL>
A typical call to <A NAME="tex2html12"
HREF="cuddExtDet.html#Cudd_Init"><EM>Cudd_Init</EM></A><A NAME="1437"></A> may look
like this:
<PRE>
manager = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);
</PRE>
To reclaim all the memory associated with a manager, an application
must call <A NAME="tex2html13"
HREF="cuddExtDet.html#Cudd_Quit"><EM>Cudd_Quit</EM></A><A NAME="1439"></A>. This is normally
done before exiting.
<P>
<H2><A NAME="SECTION00034000000000000000"></A>
<A NAME="sec:params"></A>
<BR>
Setting Parameters
</H2>
<P>
The package provides several functions to set the parameters that
control various functions. For instance, the package has an automatic
way of determining whether a larger unique<A NAME="187"></A> table
would make the application run faster. In that case, the package
enters a ``fast growth<A NAME="188"></A>" mode in which resizing of
the unique subtables is favored over garbage<A NAME="189"></A>
collection. When the unique table reaches a given size, however, the
package returns to the normal ``slow growth" mode, even though the
conditions that caused the transition to fast growth still prevail.
The limit size for fast growth<A NAME="190"></A> can be read by <A NAME="tex2html14"
HREF="cuddExtDet.html#Cudd_ReadLooseUpTo"><EM> Cudd_ReadLooseUpTo</EM></A><A NAME="1441"></A> and changed
by <A NAME="tex2html15"
HREF="cuddExtDet.html#Cudd_SetLooseUpTo"><EM>Cudd_SetLooseUpTo</EM></A><A NAME="1443"></A>. Similar
pairs of functions exist for several other parameters. See also
Section <A HREF="node4.html#sec:stats">4.8</A>.
<P>
<H2><A NAME="SECTION00035000000000000000"></A>
<A NAME="199"></A><A NAME="sec:const"></A>
<BR>
Constant Functions
</H2>
<P>
The CUDD Package defines several constant functions. These functions
are created when the manager<A NAME="201"></A> is initialized, and are accessible
through the manager itself.
<P>
<H3><A NAME="SECTION00035100000000000000"></A>
<A NAME="203"></A><A NAME="204"></A><A NAME="sec:zero"></A>
<BR>
One, Logic Zero, and Arithmetic Zero
</H3>
<P>
The constant<A NAME="206"></A> 1 (returned by <A NAME="tex2html16"
HREF="cuddExtDet.html#Cudd_ReadOne"><EM> Cudd_ReadOne</EM></A><A NAME="1445"></A>) is common to BDDs,
ADDs, and ZDDs. However, its meaning is different for ADDs and BDDs,
on the one hand, and ZDDs, on the other hand. The diagram consisting
of the constant 1 node only represents the constant 1 function for
ADDs and BDDs. For ZDDs, its meaning depends on the number of
variables: It is the conjunction of the complements of all variables.
Conversely, the representation of the constant 1 function depends on
the number of variables. The constant 1 function of <IMG
WIDTH="17" HEIGHT="19" ALIGN="BOTTOM" BORDER="0"
SRC="img4.png"
ALT="$n$"> variables is
returned by <A NAME="tex2html17"
HREF="cuddExtDet.html#Cudd_ReadZddOne"><EM>Cudd_ReadZddOne</EM></A><A NAME="1447"></A>.
<P>
The constant 0 is common to ADDs and ZDDs, but not to BDDs. The
BDD<A NAME="213"></A> logic 0 is <B>not</B> associated
with the constant 0 function: It is obtained by complementation (<A NAME="tex2html18"
HREF="cuddExtDet.html#Cudd_Not"><EM> Cudd_Not</EM></A><A NAME="1449"></A>) of the constant 1. (It is also
returned by <A NAME="tex2html19"
HREF="cuddExtDet.html#Cudd_ReadLogicZero"><EM> Cudd_ReadLogicZero</EM></A><A NAME="1451"></A>.) All
other constants are specific to ADDs.
<P>
<H3><A NAME="SECTION00035200000000000000"></A>
<A NAME="sec:predef-const"></A>
<BR>
Predefined Constants
</H3>
<P>
Besides 0 (returned by <A NAME="tex2html20"
HREF="cuddExtDet.html#Cudd_ReadZero"><EM>Cudd_ReadZero</EM></A><A NAME="1453"></A>)
and 1, the following constant<A NAME="226"></A> functions are
created at initialization time.
<OL>
<LI>PlusInfinity<A NAME="228"></A> and
MinusInfinity<A NAME="229"></A>: On computers implementing the
IEEE<A NAME="230"></A> standard 754 for
floating-point<A NAME="231"></A> arithmetic, these two constants
are set to the signed infinities<A NAME="232"></A>. On the DEC
Alphas<A NAME="233"></A>, the option <code>-ieee_with_no_inexact</code> or
<code>-ieee_with_inexact</code> must be passed to the DEC compiler to get
support of the IEEE standard. (The compiler still produces a
warning, but it can be ignored.) Compiling<A NAME="234"></A> with
those options may cause substantial performance degradation on the
Evolution IV CPUs. (Especially if the application does use the
infinities.) The problem is reportedly solved in the Evolution V
CPUs. If <TT>gcc<A NAME="235"></A></TT> is used to compile CUDD on the
Alphas, the symbol <TT>HAVE_IEEE_754<A NAME="236"></A></TT> must
be undefined. (See the Makefile<A NAME="237"></A> for the details.)
The values of these constants are returned by <A NAME="tex2html21"
HREF="cuddExtDet.html#Cudd_ReadPlusInfinity"><EM> Cudd_ReadPlusInfinity</EM></A><A NAME="1455"></A> and <A NAME="tex2html22"
HREF="cuddExtDet.html#Cudd_ReadMinusInfinity"><EM> Cudd_ReadMinusInfinity</EM></A><A NAME="1457"></A>.
</LI>
<LI>Epsilon<A NAME="244"></A>: This constant, initially set to
<IMG
WIDTH="49" HEIGHT="22" ALIGN="BOTTOM" BORDER="0"
SRC="img5.png"
ALT="$10^{-12}$">, is used in comparing floating point values for equality.
Its value is returned by <A NAME="tex2html23"
HREF="cuddExtDet.html#Cudd_ReadEpsilon"><EM> Cudd_ReadEpsilon</EM></A><A NAME="1459"></A>, and it can be
modified by calling <A NAME="tex2html24"
HREF="cuddExtDet.html#Cudd_SetEpsilon"><EM> Cudd_SetEpsilon</EM></A><A NAME="1461"></A>. Unlike the other
constants, it does not correspond to a node.
</LI>
</OL>
<P>
<H3><A NAME="SECTION00035300000000000000"></A>
<A NAME="254"></A><A NAME="sec:background"></A>
<BR>
Background
</H3>
<P>
The background value is a constant<A NAME="256"></A> typically used
to represent non-existing arcs in graphs. Consider a shortest path
problem. Two nodes that are not connected by an arc can be regarded as
being joined by an arc<A NAME="257"></A> of infinite length. In
shortest path problems, it is therefore convenient to set the
background value to PlusInfinity<A NAME="258"></A>. In network flow
problems, on the other hand, two nodes not connected by an arc can be
regarded as joined by an arc<A NAME="259"></A> of 0 capacity.
For these problems, therefore, it is more convenient to set the
background value to 0. In general, when representing
sparse<A NAME="260"></A> matrices, the background value is the value that
is assumed implicitly.
<P>
At initialization, the background value is set to 0. It can be read
with <A NAME="tex2html25"
HREF="cuddExtDet.html#Cudd_ReadBackground"><EM>Cudd_ReadBackground</EM></A><A NAME="1463"></A>,
and modified with <A NAME="tex2html26"
HREF="cuddExtDet.html#Cudd_SetBackground"><EM>Cudd_SetBackground</EM></A>. The background value
affects procedures that read sparse matrices/graphs (<A NAME="tex2html27"
HREF="cuddExtDet.html#Cudd_addRead"><EM> Cudd_addRead</EM></A><A NAME="1465"></A> and <A NAME="tex2html28"
HREF="cuddExtDet.html#Cudd_addHarwell"><EM> Cudd_addHarwell</EM></A><A NAME="1467"></A>), procedures that
print out sum-of-product<A NAME="272"></A> expressions
for ADDs (<A NAME="tex2html29"
HREF="cuddExtDet.html#Cudd_PrintMinterm"><EM> Cudd_PrintMinterm</EM></A><A NAME="1469"></A>), generators
of cubes (<A NAME="tex2html30"
HREF="cuddExtDet.html#Cudd_ForeachCube"><EM>Cudd_ForeachCube</EM></A><A NAME="1471"></A>),
and procedures that count minterms<A NAME="279"></A> (<A NAME="tex2html31"
HREF="cuddExtDet.html#Cudd_CountMinterm"><EM> Cudd_CountMinterm</EM></A><A NAME="1473"></A>).
<P>
<H3><A NAME="SECTION00035400000000000000"></A>
<A NAME="sec:newconst"></A>
<BR>
New Constants
</H3>
<P>
New constant<A NAME="285"></A> can be created by calling <A NAME="tex2html32"
HREF="cuddExtDet.html#Cudd_addConst"><EM> Cudd_addConst</EM></A><A NAME="1475"></A>. This function will
retrieve the ADD<A NAME="289"></A> for the desired
constant, if it already exist, or it will create a new one. Obviously,
new constants should only be used when manipulating ADDs.
<P>
<H2><A NAME="SECTION00036000000000000000"></A>
<A NAME="sec:newvar"></A>
<BR>
Creating Variables
</H2>
<P>
Decision diagrams are typically created by combining simpler decision
diagrams. The simplest decision diagrams, of course, cannot be created
in that way. Constant functions have been discussed in
Section <A HREF="node3.html#sec:const">3.5</A>. In this section we discuss the simple
variable functions, also known as <EM> projection<A NAME="293"></A> functions</EM>.
<P>
<H3><A NAME="SECTION00036100000000000000"></A>
<A NAME="sec:BDDADDvar"></A>
<BR>
New BDD and ADD Variables
</H3>
<P>
The projection<A NAME="296"></A> functions are distinct for
BDDs and ADDs. A projection function for BDDs consists of an internal
node with both outgoing arcs pointing to the constant 1. The <EM> else</EM> arc<A NAME="298"></A> is complemented.
<P>
An ADD projection function, on the other hand, has the <EM>else</EM>
pointer directed to the arithmetic<A NAME="300"></A> zero
function. One should never mix the two types of variables. BDD
variables should be used when manipulating BDDs, and ADD variables
should be used when manipulating ADDs. Three functions are provided
to create BDD variables:
<UL>
<LI><A NAME="tex2html33"
HREF="cuddExtDet.html#Cudd_bddIthVar"><EM>Cudd_bddIthVar</EM></A><A NAME="1477"></A>: Returns
the projection<A NAME="305"></A> function with index <IMG
WIDTH="12" HEIGHT="19" ALIGN="BOTTOM" BORDER="0"
SRC="img6.png"
ALT="$i$">.
If the function does not exist, it is created.
</LI>
<LI><A NAME="tex2html34"
HREF="cuddExtDet.html#Cudd_bddNewVar"><EM>Cudd_bddNewVar</EM></A><A NAME="1479"></A>: Returns a
new projection<A NAME="309"></A> function, whose index is
the largest index in use at the time of the call, plus 1.
</LI>
<LI><A NAME="tex2html35"
HREF="cuddExtDet.html#Cudd_bddNewVarAtLevel"><EM> Cudd_bddNewVarAtLevel</EM></A><A NAME="1481"></A>:
Similar to <A NAME="tex2html36"
HREF="cuddExtDet.html#Cudd_bddNewVar"><EM>Cudd_bddNewVar</EM></A><A NAME="1483"></A>. In
addition it allows to specify the position in the variable
order<A NAME="316"></A> at which the new variable should be
inserted. By contrast, <A NAME="tex2html37"
HREF="cuddExtDet.html#Cudd_bddNewVar"><EM> Cudd_bddNewVar</EM></A><A NAME="1485"></A> adds the new
variable at the end of the order.
</LI>
</UL>
The analogous functions for ADDs are <A NAME="tex2html38"
HREF="cuddExtDet.html#Cudd_addIthVar"><EM> Cudd_addIthVar</EM></A><A NAME="1487"></A>, <A NAME="tex2html39"
HREF="cuddExtDet.html#Cudd_addNewVar"><EM> Cudd_addNewVar</EM></A><A NAME="1489"></A>, and <A NAME="tex2html40"
HREF="cuddExtDet.html#Cudd_addNewVarAtLevel"><EM> Cudd_addNewVarAtLevel</EM></A><A NAME="1491"></A>.
<P>
<H3><A NAME="SECTION00036200000000000000"></A>
<A NAME="331"></A><A NAME="sec:ZDDvars"></A>
<BR>
New ZDD Variables
</H3>
<P>
Unlike the projection functions of BDDs and ADDs, the
projection<A NAME="333"></A> functions of ZDDs have diagrams
with <IMG
WIDTH="47" HEIGHT="34" ALIGN="MIDDLE" BORDER="0"
SRC="img7.png"
ALT="$n+1$"> nodes, where <IMG
WIDTH="17" HEIGHT="19" ALIGN="BOTTOM" BORDER="0"
SRC="img4.png"
ALT="$n$"> is the number of variables. Therefore the
ZDDs of the projection functions change when new variables are added.
This will be discussed in Section <A HREF="node3.html#sec:basicZDD">3.9</A>. Here we assume
that the number of variables is fixed. The ZDD of the <IMG
WIDTH="12" HEIGHT="19" ALIGN="BOTTOM" BORDER="0"
SRC="img6.png"
ALT="$i$">-th
projection function is returned by <A NAME="tex2html41"
HREF="cuddExtDet.html#Cudd_zddIthVar"><EM> Cudd_zddIthVar</EM></A><A NAME="1493"></A>.
<P>
<H2><A NAME="SECTION00037000000000000000"></A>
<A NAME="339"></A><A NAME="sec:basicBDD"></A>
<BR>
Basic BDD Manipulation
</H2>
<P>
Common manipulations of BDDs can be accomplished by calling <A NAME="tex2html42"
HREF="cuddExtDet.html#Cudd_bddIte"><EM> Cudd_bddIte</EM></A>. This function takes three BDDs, <IMG
WIDTH="17" HEIGHT="35" ALIGN="MIDDLE" BORDER="0"
SRC="img8.png"
ALT="$f$">, <IMG
WIDTH="15" HEIGHT="34" ALIGN="MIDDLE" BORDER="0"
SRC="img9.png"
ALT="$g$">, and <IMG
WIDTH="17" HEIGHT="19" ALIGN="BOTTOM" BORDER="0"
SRC="img10.png"
ALT="$h$">,
as arguments and computes <!-- MATH
$f\cdot g + f'\cdot h$
-->
<IMG
WIDTH="97" HEIGHT="37" ALIGN="MIDDLE" BORDER="0"
SRC="img11.png"
ALT="$f\cdot g + f'\cdot h$">. Like all the
functions that create new BDDs or ADDs, <A NAME="tex2html43"
HREF="cuddExtDet.html#Cudd_bddIte"><EM> Cudd_bddIte</EM></A><A NAME="1495"></A> returns a result that must
be explicitly referenced by the caller. <A NAME="tex2html44"
HREF="cuddExtDet.html#Cudd_bddIte"><EM>Cudd_bddIte</EM></A>
can be
used to implement all two-argument boolean functions. However, the
package also provides <A NAME="tex2html45"
HREF="cuddExtDet.html#Cudd_bddAnd"><EM>Cudd_bddAnd</EM></A><A NAME="1497"></A>
as well as the other two-operand boolean functions, which are slightly
more efficient when a two-operand function is called for. The
following fragment of code illustrates how to build the BDD for the
function <!-- MATH
$f = x_0'x_1'x_2'x_3'$
-->
<IMG
WIDTH="110" HEIGHT="37" ALIGN="MIDDLE" BORDER="0"
SRC="img12.png"
ALT="$f = x_0'x_1'x_2'x_3'$">.
<PRE>
DdManager *manager;
DdNode *f, *var, *tmp;
int i;
...
f = Cudd_ReadOne(manager);
Cudd_Ref(f);
for (i = 3; i >= 0; i--) {
var = Cudd_bddIthVar(manager,i);
tmp = Cudd_bddAnd(manager,Cudd_Not(var),f);
Cudd_Ref(tmp);
Cudd_RecursiveDeref(manager,f);
f = tmp;
}
</PRE>
This example illustrates the following points:
<UL>
<LI>Intermediate results must be ``referenced" and ``dereferenced."
However, <TT>var</TT> is a projection<A NAME="355"></A>
function, and its reference<A NAME="356"></A> count is always
greater than 0. Therefore, there is no call to <A NAME="tex2html46"
HREF="cuddExtDet.html#Cudd_Ref"><EM> Cudd_Ref</EM></A><A NAME="1499"></A>.
</LI>
<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"
HREF="cuddExtDet.html#Cudd_bddAnd"><EM> Cudd_bddAnd</EM></A><A NAME="1501"></A> were assigned directly
to <TT>f</TT>, the old <TT>f</TT> would be lost, and there would be no way
to free its nodes.
</LI>
<LI>The statement <TT>f = tmp</TT> has the same effect as:
<PRE>
f = tmp;
Cudd_Ref(f);
Cudd_RecursiveDeref(manager,tmp);
</PRE>
but is more efficient. The reference<A NAME="370"></A> is
``passed" from <TT>tmp</TT> to <TT>f</TT>, and <TT>tmp</TT> is now ready to
be reutilized.
</LI>
<LI>It is normally more efficient to build BDDs ``bottom-up." This
is why the loop goes from 3 to 0. Notice, however, that after
variable reordering, higher index does not necessarily mean ``closer
to the bottom." Of course, in this simple example, efficiency is not
a concern.
</LI>
<LI>Had we wanted to conjoin the variables in a bottom-up fashion
even after reordering, we should have used <A NAME="tex2html48"
HREF="cuddExtDet.html#Cudd_ReadInvPerm"><EM> Cudd_ReadInvPerm</EM></A><A NAME="1503"></A>. One has to be
careful, though, to fix the order of conjunction before entering the
loop. Otherwise, if reordering takes place, it is possible to use
one variable twice and skip another variable.
</LI>
</UL>
<P>
<H2><A NAME="SECTION00038000000000000000"></A>
<A NAME="379"></A><A NAME="sec:basicADD"></A>
<BR>
Basic ADD Manipulation
</H2>
<P>
The most common way to manipulate ADDs is via <A NAME="tex2html49"
HREF="cuddExtDet.html#Cudd_addApply"><EM> Cudd_addApply</EM></A><A NAME="1505"></A>. This function can
apply a wide variety of operators to a pair of ADDs. Among the
available operators are addition, multiplication, division, minimum,
maximum, and boolean operators that work on ADDs whose leaves are
restricted to 0 and 1 (0-1 ADDs).
<P>
The following fragment of code illustrates how to build the ADD for
the function <!-- MATH
$f = 5x_0x_1x_2x_3$
-->
<IMG
WIDTH="119" HEIGHT="35" ALIGN="MIDDLE" BORDER="0"
SRC="img13.png"
ALT="$f = 5x_0x_1x_2x_3$">.
<PRE>
DdManager *manager;
DdNode *f, *var, *tmp;
int i;
...
f = Cudd_addConst(manager,5);
Cudd_Ref(f);
for (i = 3; i >= 0; i--) {
var = Cudd_addIthVar(manager,i);
Cudd_Ref(var);
tmp = Cudd_addApply(manager,Cudd_addTimes,var,f);
Cudd_Ref(tmp);
Cudd_RecursiveDeref(manager,f);
Cudd_RecursiveDeref(manager,var);
f = tmp;
}
</PRE>
This example, contrasted to the example of BDD manipulation,
illustrates the following points:
<UL>
<LI>The ADD projection<A NAME="387"></A> function are not
maintained by the manager. It is therefore necessary to
reference<A NAME="388"></A> and
dereference<A NAME="389"></A> them.
</LI>
<LI>The product of two ADDs is computed by calling <A NAME="tex2html50"
HREF="cuddExtDet.html#Cudd_addApply"><EM> Cudd_addApply</EM></A><A NAME="1507"></A> with <A NAME="tex2html51"
HREF="cuddExtDet.html#Cudd_addTimes"><EM> Cudd_addTimes</EM></A><A NAME="1509"></A> as parameter. There
is no ``apply'' function for BDDs, because <A NAME="tex2html52"
HREF="cuddExtDet.html#Cudd_bddAnd"><EM> Cudd_bddAnd</EM></A><A NAME="1511"></A> and <A NAME="tex2html53"
HREF="cuddExtDet.html#Cudd_bddXor"><EM> Cudd_bddXor</EM></A><A NAME="1513"></A> plus complementation are
sufficient to implement all two-argument boolean functions.
</LI>
</UL>
<P>
<H2><A NAME="SECTION00039000000000000000"></A>
<A NAME="404"></A><A NAME="sec:basicZDD"></A>
<BR>
Basic ZDD Manipulation
</H2>
<P>
ZDDs are often generated by converting<A NAME="406"></A>
existing BDDs. (See Section <A HREF="node3.html#sec:convertZ">3.11</A>.) However, it is also
possible to build ZDDs by applying boolean operators to other ZDDs,
starting from constants and projection<A NAME="408"></A>
functions. The following fragment of code illustrates how to build
the ZDD for the function <!-- MATH
$f = x_0'+x_1'+x_2'+x_3'$
-->
<IMG
WIDTH="174" HEIGHT="37" ALIGN="MIDDLE" BORDER="0"
SRC="img14.png"
ALT="$f = x_0'+x_1'+x_2'+x_3'$">. We assume that the
four variables already exist in the manager when the ZDD for <IMG
WIDTH="17" HEIGHT="35" ALIGN="MIDDLE" BORDER="0"
SRC="img8.png"
ALT="$f$"> is
built. Note the use of De Morgan's law.
<PRE>
DdManager *manager;
DdNode *f, *var, *tmp;
int i;
manager = Cudd_Init(0,4,CUDD_UNIQUE_SLOTS,
CUDD_CACHE_SLOTS,0);
...
tmp = Cudd_ReadZddOne(manager,0);
Cudd_Ref(tmp);
for (i = 3; i >= 0; i--) {
var = Cudd_zddIthVar(manager,i);
Cudd_Ref(var);
f = Cudd_zddIntersect(manager,var,tmp);
Cudd_Ref(f);
Cudd_RecursiveDerefZdd(manager,tmp);
Cudd_RecursiveDerefZdd(manager,var);
tmp = f;
}
f = Cudd_zddDiff(manager,Cudd_ReadZddOne(manager,0),tmp);
Cudd_Ref(f);
Cudd_RecursiveDerefZdd(manager,tmp);
</PRE>
This example illustrates the following points:
<UL>
<LI>The projection<A NAME="412"></A> functions are
referenced, because they are not maintained by the manager.
</LI>
<LI>Complementation is obtained by subtracting from the constant 1
function.
</LI>
<LI>The result of <A NAME="tex2html54"
HREF="cuddExtDet.html#Cudd_ReadZddOne"><EM> Cudd_ReadZddOne</EM></A><A NAME="1515"></A> does not
require referencing.
</LI>
</UL>
CUDD provides functions for the manipulation of
covers<A NAME="417"></A> represented by ZDDs. For instance, <A NAME="tex2html55"
HREF="cuddExtDet.html#Cudd_zddIsop"><EM> Cudd_zddIsop</EM></A><A NAME="1517"></A> builds a ZDD
representing an irredundant<A NAME="421"></A> sum of
products for the incompletely specified function defined by the two
BDDs <IMG
WIDTH="18" HEIGHT="19" ALIGN="BOTTOM" BORDER="0"
SRC="img15.png"
ALT="$L$"> and <IMG
WIDTH="20" HEIGHT="19" ALIGN="BOTTOM" BORDER="0"
SRC="img16.png"
ALT="$U$">. <A NAME="tex2html56"
HREF="cuddExtDet.html#Cudd_zddWeakDiv"><EM> Cudd_zddWeakDiv</EM></A><A NAME="1519"></A> performs the weak
division of two covers given as ZDDs. These functions expect the two
ZDD variables corresponding to the two literals of the function variable
to be adjacent. One has to create variable groups (see
Section <A HREF="node3.html#sec:reordZ">3.14</A>) for reordering<A NAME="426"></A> of
the ZDD variables to work. BDD automatic reordering is safe even
without groups: If realignment of ZDD and ADD/BDD variables is requested
(see Section <A HREF="node3.html#sec:consist">3.15</A>) groups will be kept adjacent.
<P>
<H2><A NAME="SECTION000310000000000000000"></A>
<A NAME="429"></A>
<A NAME="430"></A><A NAME="sec:convert"></A>
<BR>
Converting ADDs to BDDs and Vice Versa
</H2>
<P>
Several procedures are provided to convert ADDs to BDDs, according to
different criteria. (<A NAME="tex2html57"
HREF="cuddExtDet.html#Cudd_addBddPattern"><EM> Cudd_addBddPattern</EM></A><A NAME="1521"></A>, <A NAME="tex2html58"
HREF="cuddExtDet.html#Cudd_addBddInterval"><EM> Cudd_addBddInterval</EM></A><A NAME="1523"></A>, and <A NAME="tex2html59"
HREF="cuddExtDet.html#Cudd_addBddThreshold"><EM> Cudd_addBddThreshold</EM></A><A NAME="1525"></A>.) The
conversion from BDDs to ADDs (<A NAME="tex2html60"
HREF="cuddExtDet.html#Cudd_BddToAdd"><EM> Cudd_BddToAdd</EM></A><A NAME="1527"></A>) is based on the
simple principle of mapping the logical 0<A NAME="444"></A> and 1 on
the arithmetic<A NAME="445"></A> 0 and 1. It is also possible to
convert an ADD with integer values (more precisely, floating point
numbers with 0 fractional part) to an array of BDDs by repeatedly
calling <A NAME="tex2html61"
HREF="cuddExtDet.html#Cudd_addIthBit"><EM>Cudd_addIthBit</EM></A><A NAME="1529"></A>.
<P>
<H2><A NAME="SECTION000311000000000000000"></A>
<A NAME="450"></A>
<A NAME="451"></A><A NAME="sec:convertZ"></A>
<BR>
Converting BDDs to ZDDs and Vice Versa
</H2>
<P>
Many applications first build a set of BDDs and then derive ZDDs from
the BDDs. These applications should create the manager with 0
ZDD<A NAME="453"></A> variables and
create the BDDs. Then they should call <A NAME="tex2html62"
HREF="cuddExtDet.html#Cudd_zddVarsFromBddVars"><EM> Cudd_zddVarsFromBddVars</EM></A><A NAME="1531"></A> to
create the necessary ZDD variables--whose number is likely to be
known once the BDDs are available. This approach eliminates the
difficulties that arise when the number of ZDD variables changes while
ZDDs are being built.
<P>
The simplest conversion from BDDs to ZDDs is a simple change of
representation, which preserves the functions. Simply put, given a BDD
for <IMG
WIDTH="17" HEIGHT="35" ALIGN="MIDDLE" BORDER="0"
SRC="img8.png"
ALT="$f$">, a ZDD for <IMG
WIDTH="17" HEIGHT="35" ALIGN="MIDDLE" BORDER="0"
SRC="img8.png"
ALT="$f$"> is requested. In this case the correspondence
between the BDD variables and ZDD variables is one-to-one. Hence, <A NAME="tex2html63"
HREF="cuddExtDet.html#Cudd_zddVarsFromBddVars"><EM> Cudd_zddVarsFromBddVars</EM></A>
should be called with the <EM> multiplicity</EM> parameter equal to 1. The conversion proper can then
be performed by calling <A NAME="tex2html64"
HREF="cuddExtDet.html#Cudd_zddPortFromBdd"><EM> Cudd_zddPortFromBdd</EM></A><A NAME="1533"></A>. The
inverse transformation is performed by <A NAME="tex2html65"
HREF="cuddExtDet.html#Cudd_zddPortToBdd"><EM> Cudd_zddPortToBdd</EM></A><A NAME="1535"></A>.
<P>
ZDDs are quite often used for the representation of <EM> covers</EM><A NAME="467"></A>. This is normally done by associating
two ZDD variables to each variable of the function. (And hence,
typically, to each BDD variable.) One ZDD variable is associated with
the positive literal of the BDD variable, while the other ZDD variable
is associated with the negative literal. A call to <A NAME="tex2html66"
HREF="cuddExtDet.html#Cudd_zddVarsFromBddVars"><EM> Cudd_zddVarsFromBddVars</EM></A><A NAME="1537"></A>
with <EM>multiplicity</EM> equal to 2 will associate to BDD variable
<IMG
WIDTH="12" HEIGHT="19" ALIGN="BOTTOM" BORDER="0"
SRC="img6.png"
ALT="$i$"> the two ZDD variables <IMG
WIDTH="21" HEIGHT="19" ALIGN="BOTTOM" BORDER="0"
SRC="img17.png"
ALT="$2i$"> and <IMG
WIDTH="51" HEIGHT="34" ALIGN="MIDDLE" BORDER="0"
SRC="img18.png"
ALT="$2i+1$">.
<P>
If a BDD variable group tree exists when <A NAME="tex2html67"
HREF="cuddExtDet.html#Cudd_zddVarsFromBddVars"><EM> Cudd_zddVarsFromBddVars</EM></A>
is called (see Section <A HREF="node3.html#sec:group">3.13</A>)
the function generates a ZDD variable group tree consistent to it. In
any case, all the ZDD variables derived from the same BDD variable are
clustered into a group.
<P>
If the ZDD for <IMG
WIDTH="17" HEIGHT="35" ALIGN="MIDDLE" BORDER="0"
SRC="img8.png"
ALT="$f$"> is created and later a new ZDD variable is added to
the manager, the function represented by the existing ZDD changes.
Suppose, for instance, that two variables are initially created, and
that the ZDD for <IMG
WIDTH="97" HEIGHT="35" ALIGN="MIDDLE" BORDER="0"
SRC="img19.png"
ALT="$f = x_0 + x_1$"> is built. If a third variable is
added, say <IMG
WIDTH="24" HEIGHT="34" ALIGN="MIDDLE" BORDER="0"
SRC="img20.png"
ALT="$x_2$">, then the ZDD represents <!-- MATH
$g = (x_0 + x_1) x_2'$
-->
<IMG
WIDTH="126" HEIGHT="37" ALIGN="MIDDLE" BORDER="0"
SRC="img21.png"
ALT="$g = (x_0 + x_1) x_2'$">
instead. This change in function obviously applies regardless of what
use is made of the ZDD. However, if the ZDD is used to represent a
cover<A NAME="475"></A>, the cover itself is not changed by the
addition of new variable. (What changes is the
characteristic<A NAME="476"></A> function of the cover.)
<P>
<H2><A NAME="SECTION000312000000000000000"></A>
<A NAME="478"></A><A NAME="sec:reorder"></A>
<BR>
Variable Reordering for BDDs and ADDs
</H2>
<P>
The CUDD package provides a rich set of
dynamic<A NAME="480"></A> reordering algorithms. Some of them
are slight variations of existing techniques
[<A
HREF="node7.html#Rudell93">16</A>,<A
HREF="node7.html#Drechs95">6</A>,<A
HREF="node7.html#Bollig95">2</A>,<A
HREF="node7.html#Ishiur91">10</A>,<A
HREF="node7.html#Plessi93">15</A>,<A
HREF="node7.html#Jeong93">11</A>]; some
others have been developed specifically for this package
[<A
HREF="node7.html#Panda94">14</A>,<A
HREF="node7.html#Panda95b">13</A>].
<P>
Reordering affects a unique<A NAME="483"></A> table. This means that
BDDs and ADDs, which share the same unique table are simultaneously
reordered. ZDDs, on the other hand, are reordered separately. In the
following we discuss the reordering of BDDs and ADDs. Reordering for
ZDDs is the subject of Section <A HREF="node3.html#sec:reordZ">3.14</A>.
<P>
Reordering of the variables can be invoked directly by the application
by calling <A NAME="tex2html68"
HREF="cuddExtDet.html#Cudd_ReduceHeap"><EM>Cudd_ReduceHeap</EM></A><A NAME="1539"></A>. Or it
can be automatically triggered by the package when the number of nodes
has reached a given threshold<A NAME="488"></A>. (The
threshold is initialized and automatically adjusted after each
reordering by the package.) To enable automatic dynamic reordering
(also called <EM>asynchronous<A NAME="489"></A></EM>
dynamic reordering in this document) the application must call <A NAME="tex2html69"
HREF="cuddExtDet.html#Cudd_AutodynEnable"><EM> Cudd_AutodynEnable</EM></A><A NAME="1541"></A>. Automatic
dynamic reordering can subsequently be disabled by calling <A NAME="tex2html70"
HREF="cuddExtDet.html#Cudd_AutodynDisable"><EM> Cudd_AutodynDisable</EM></A><A NAME="1543"></A>.
<P>
All reordering methods are available in both the case of direct call
to <A NAME="tex2html71"
HREF="cuddExtDet.html#Cudd_ReduceHeap"><EM>Cudd_ReduceHeap</EM></A><A NAME="1545"></A> and the case of
automatic invocation. For many methods, the reordering procedure is
iterated until no further improvement is obtained. We call these
methods the <EM>converging<A NAME="499"></A></EM> methods.
When constraints are imposed on the relative position of variables
(see Section <A HREF="node3.html#sec:group">3.13</A>) the reordering methods apply inside the
groups. The groups<A NAME="501"></A> themselves are reordered by
sifting<A NAME="502"></A>. Each method is identified by a
constant of the enumerated type <EM> Cudd_ReorderingType<A NAME="503"></A></EM>
defined in <EM>cudd.h<A NAME="504"></A></EM> (the external
header<A NAME="505"></A> file of the CUDD package):
<P>
<DL>
<DT><STRONG>CUDD_REORDER_NONE<A NAME="507"></A>:</STRONG></DT>
<DD>This method
causes no reordering.
</DD>
<DT><STRONG>CUDD_REORDER_SAME<A NAME="508"></A>:</STRONG></DT>
<DD>If passed to
<A NAME="tex2html72"
HREF="cuddExtDet.html#Cudd_AutodynEnable"><EM>Cudd_AutodynEnable</EM></A><A NAME="1547"></A>, this
method leaves the current method for automatic reordering unchanged.
If passed to <A NAME="tex2html73"
HREF="cuddExtDet.html#Cudd_ReduceHeap"><EM>Cudd_ReduceHeap</EM></A><A NAME="1549"></A>,
this method causes the current method for automatic reordering to be
used.
</DD>
<DT><STRONG>CUDD_REORDER_RANDOM<A NAME="515"></A>:</STRONG></DT>
<DD>Pairs of
variables are randomly chosen, and swapped in the order. The swap is
performed by a series of swaps of adjacent variables. The best order
among those obtained by the series of swaps is retained. The number
of pairs chosen for swapping<A NAME="516"></A> equals the
number of variables in the diagram.
</DD>
<DT><STRONG>CUDD_REORDER_RANDOM_PIVOT<A NAME="517"></A>:</STRONG></DT>
<DD>Same as CUDD_REORDER_RANDOM, but the two variables are chosen so
that the first is above the variable with the largest number of
nodes, and the second is below that variable. In case there are
several variables tied for the maximum number of nodes, the one
closest to the root is used.
</DD>
<DT><STRONG>CUDD_REORDER_SIFT<A NAME="518"></A>:</STRONG></DT>
<DD>This method is
an implementation of Rudell's sifting<A NAME="519"></A>
algorithm [<A
HREF="node7.html#Rudell93">16</A>]. A simplified description of sifting is as
follows: Each variable is considered in turn. A variable is moved up
and down in the order so that it takes all possible positions. The
best position is identified and the variable is returned to that
position.
<P>
In reality, things are a bit more complicated. For instance, there
is a limit on the number of variables that will be sifted. This
limit can be read with <A NAME="tex2html74"
HREF="cuddExtDet.html#Cudd_ReadSiftMaxVar"><EM> Cudd_ReadSiftMaxVar</EM></A><A NAME="1551"></A> and set
with <A NAME="tex2html75"
HREF="cuddExtDet.html#Cudd_SetSiftMaxVar"><EM>Cudd_SetSiftMaxVar</EM></A><A NAME="1553"></A>. In
addition, if the diagram grows too much while moving a variable up
or down, that movement is terminated before the variable has reached
one end of the order. The maximum ratio by which the diagram is
allowed to grow while a variable is being sifted can be read with
<A NAME="tex2html76"
HREF="cuddExtDet.html#Cudd_ReadMaxGrowth"><EM>Cudd_ReadMaxGrowth</EM></A><A NAME="1555"></A> and
set with <A NAME="tex2html77"
HREF="cuddExtDet.html#Cudd_SetMaxGrowth"><EM>Cudd_SetMaxGrowth</EM></A><A NAME="1557"></A>.
</DD>
<DT><STRONG>CUDD_REORDER_SIFT_CONVERGE<A NAME="533"></A>:</STRONG></DT>
<DD>This is the converging<A NAME="534"></A> variant of
CUDD_REORDER_SIFT.
</DD>
<DT><STRONG>CUDD_REORDER_SYMM_SIFT<A NAME="535"></A>:</STRONG></DT>
<DD>This method is an implementation of
symmetric<A NAME="536"></A> sifting [<A
HREF="node7.html#Panda94">14</A>]. It is
similar to sifting, with one addition: Variables that become
adjacent during sifting are tested for symmetry<A NAME="538"></A>. If
they are symmetric, they are linked in a group. Sifting then
continues with a group being moved, instead of a single variable.
After symmetric sifting has been run, <A NAME="tex2html78"
HREF="cuddExtDet.html#Cudd_SymmProfile"><EM> Cudd_SymmProfile</EM></A><A NAME="1559"></A> can be called
to report on the symmetry groups found. (Both positive and negative
symmetries are reported.)
</DD>
<DT><STRONG>CUDD_REORDER_SYMM_SIFT_CONV<A NAME="542"></A>:</STRONG></DT>
<DD>This is the converging<A NAME="543"></A> variant of
CUDD_REORDER_SYMM_SIFT.
</DD>
<DT><STRONG>CUDD_REORDER_GROUP_SIFT<A NAME="544"></A>:</STRONG></DT>
<DD>This method is an implementation of group<A NAME="545"></A>
sifting [<A
HREF="node7.html#Panda95b">13</A>]. It is similar to symmetric sifting, but
aggregation<A NAME="547"></A> is not restricted to symmetric
variables.
</DD>
<DT><STRONG>CUDD_REORDER_GROUP_SIFT_CONV<A NAME="548"></A>:</STRONG></DT>
<DD>This method repeats until convergence the combination of
CUDD_REORDER_GROUP_SIFT and CUDD_REORDER_WINDOW4.
</DD>
<DT><STRONG>CUDD_REORDER_WINDOW2<A NAME="549"></A>:</STRONG></DT>
<DD>This
method implements the window<A NAME="550"></A> permutation
approach of Fujita [<A
HREF="node7.html#Fujita91b">8</A>] and Ishiura [<A
HREF="node7.html#Ishiur91">10</A>].
The size of the window is 2.
</DD>
<DT><STRONG>CUDD_REORDER_WINDOW3<A NAME="553"></A>:</STRONG></DT>
<DD>Similar
to CUDD_REORDER_WINDOW2, but with a window of size 3.
</DD>
<DT><STRONG>CUDD_REORDER_WINDOW4<A NAME="554"></A>:</STRONG></DT>
<DD>Similar
to CUDD_REORDER_WINDOW2, but with a window of size 4.
</DD>
<DT><STRONG>CUDD_REORDER_WINDOW2_CONV<A NAME="555"></A>:</STRONG></DT>
<DD>This is the converging<A NAME="556"></A> variant of
CUDD_REORDER_WINDOW2.
</DD>
<DT><STRONG>CUDD_REORDER_WINDOW3_CONV<A NAME="557"></A>:</STRONG></DT>
<DD>This is the converging variant of CUDD_REORDER_WINDOW3.
</DD>
<DT><STRONG>CUDD_REORDER_WINDOW4_CONV<A NAME="558"></A>:</STRONG></DT>
<DD>This is the converging variant of CUDD_REORDER_WINDOW4.
</DD>
<DT><STRONG>CUDD_REORDER_ANNEALING<A NAME="559"></A>:</STRONG></DT>
<DD>This
method is an implementation of simulated
annealing<A NAME="560"></A> for variable
ordering, vaguely resemblant of the algorithm of [<A
HREF="node7.html#Bollig95">2</A>].
This method is potentially very slow.
</DD>
<DT><STRONG>CUDD_REORDER_GENETIC:<A NAME="562"></A></STRONG></DT>
<DD>This
method is an implementation of a genetic<A NAME="563"></A>
algorithm for variable ordering, inspired by the work of Drechsler
[<A
HREF="node7.html#Drechs95">6</A>]. This method is potentially very slow.
</DD>
<DT><STRONG>CUDD_REORDER_EXACT<A NAME="565"></A>:</STRONG></DT>
<DD>This method
implements a dynamic programming approach to
exact<A NAME="566"></A> reordering
[<A
HREF="node7.html#Held62">9</A>,<A
HREF="node7.html#Friedman90">7</A>,<A
HREF="node7.html#Ishiur91">10</A>], with improvements described in
[<A
HREF="node7.html#Jeong93">11</A>]. It only stores one BDD at the time. Therefore, it is
relatively efficient in terms of memory. Compared to other
reordering strategies, it is very slow, and is not recommended for
more than 16 variables.
</DD>
</DL>
So far we have described methods whereby the package selects an order
automatically. A given order of the variables can also be imposed by
calling <A NAME="tex2html79"
HREF="cuddExtDet.html#Cudd_ShuffleHeap"><EM>Cudd_ShuffleHeap</EM></A><A NAME="1561"></A>.
<P>
<H2><A NAME="SECTION000313000000000000000"></A>
<A NAME="574"></A><A NAME="sec:group"></A>
<BR>
Grouping Variables
</H2>
<P>
CUDD allows the application to specify constraints on the positions of
group of variables. It is possible to request that a group of
contiguous variables be kept contiguous by the reordering procedures.
It is also possible to request that the relative order of some groups
of variables be left unchanged. The constraints on the order are
specified by means of a tree<A NAME="576"></A>, which is created in
one of two ways:
<UL>
<LI>By calling <A NAME="tex2html81"
HREF="cuddExtDet.html#Cudd_MakeTreeNode"><EM>Cudd_MakeTreeNode</EM></A><A NAME="1563"></A>.
</LI>
<LI>By calling the functions of the MTR<A NAME="581"></A> library
(part of the distribution), and by registering the result with the
manager using <A NAME="tex2html82"
HREF="cuddExtDet.html#Cudd_SetTree"><EM>Cudd_SetTree</EM></A><A NAME="1565"></A>. The
current tree registered with the manager can be read with <A NAME="tex2html83"
HREF="cuddExtDet.html#Cudd_ReadTree"><EM> Cudd_ReadTree</EM></A><A NAME="1567"></A>.
</LI>
</UL>
<P>
Each node in the tree represents a range of variables. The lower bound
of the range is given by the <EM>low</EM> field of the node, and the
size of the group is given by the <EM>size</EM> field of the
node.<A NAME="tex2html80"
HREF="footnode.html#foot1315"><SUP>2</SUP></A> The variables in
each range are kept contiguous. Furthermore, if a node is marked with
the MTR_FIXED<A NAME="593"></A> flag, then the relative order of the
variable ranges associated to its children is not changed. As an
example, suppose the initial variable order is:
<PRE>
x0, y0, z0, x1, y1, z1, ... , x9, y9, z9.
</PRE>
Suppose we want to keep each group of three variables with the same
index (e.g., <code>x3, y3, z3</code>) contiguous, while allowing the package
to change the order of the groups. We can accomplish this with the
following code:
<PRE>
for (i = 0; i < 10; i++) {
(void) Cudd_MakeTreeNode(manager,i*3,3,MTR_DEFAULT);
}
</PRE>
If we want to keep the order within each group of variables
fixed (i.e., <code>x</code> before <code>y</code> before <code>z</code>) we need to
change MTR_DEFAULT<A NAME="598"></A> into MTR_FIXED.
<P>
The <EM>low</EM> parameter passed to <A NAME="tex2html84"
HREF="cuddExtDet.html#Cudd_MakeTreeNode"><EM> Cudd_MakeTreeNode</EM></A><A NAME="1569"></A> is the index
of a variable (as opposed to its level or position in the order). The
group tree<A NAME="603"></A> can be created at any time. The result
obviously depends on the variable order in effect at creation time.
<P>
It is possible to create a variable group tree also before the
variables themselves are created. The package assumes in this case
that the index of the variables not yet in existence will equal their
position in the order when they are created. Therefore, applications
that rely on <A NAME="tex2html85"
HREF="cuddExtDet.html#Cudd_bddNewVarAtLevel"><EM> Cudd_bddNewVarAtLevel</EM></A><A NAME="1571"></A> or
<A NAME="tex2html86"
HREF="cuddExtDet.html#Cudd_addNewVarAtLevel"><EM>Cudd_addNewVarAtLevel</EM></A><A NAME="1573"></A> to
create new variables have to create the variables before they group
them.
<P>
The reordering procedure will skip all groups whose variables are not
yet in existence. For groups that are only partially in existence, the
reordering procedure will try to reorder the variables already
instantiated, without violating the adjacency constraints.
<P>
<H2><A NAME="SECTION000314000000000000000"></A>
<A NAME="611"></A><A NAME="sec:reordZ"></A>
<BR>
Variable Reordering for ZDDs
</H2>
<P>
Reordering of ZDDs is done in much the same way as the reordering of
BDDs and ADDs. The functions corresponding to <A NAME="tex2html87"
HREF="cuddExtDet.html#Cudd_ReduceHeap"><EM>Cudd_ReduceHeap</EM></A>
and <A NAME="tex2html88"
HREF="cuddExtDet.html#Cudd_ShuffleHeap"><EM>Cudd_ShuffleHeap</EM></A>
are <A NAME="tex2html89"
HREF="cuddExtDet.html#Cudd_zddReduceHeap"><EM> Cudd_zddReduceHeap</EM></A><A NAME="1575"></A> and <A NAME="tex2html90"
HREF="cuddExtDet.html#Cudd_zddShuffleHeap"><EM> Cudd_zddShuffleHeap</EM></A><A NAME="1577"></A>. To enable
dynamic<A NAME="623"></A> reordering, the application must
call <A NAME="tex2html91"
HREF="cuddExtDet.html#Cudd_AutodynEnableZdd"><EM>Cudd_AutodynEnableZdd</EM></A><A NAME="1579"></A>,
and to disable dynamic reordering, it must call <A NAME="tex2html92"
HREF="cuddExtDet.html#Cudd_AutodynDisableZdd"><EM> Cudd_AutodynDisableZdd</EM></A><A NAME="1581"></A>. In
the current implementation, however, the choice of reordering methods
for ZDDs is more limited. Specifically, these methods are available:
<P>
<DL>
<DT><STRONG>CUDD_REORDER_NONE<A NAME="631"></A>;</STRONG></DT>
<DD>
</DD>
<DT><STRONG>CUDD_REORDER_SAME<A NAME="632"></A>;</STRONG></DT>
<DD>
</DD>
<DT><STRONG>CUDD_REORDER_RANDOM<A NAME="633"></A>;</STRONG></DT>
<DD>
</DD>
<DT><STRONG>CUDD_REORDER_RANDOM_PIVOT<A NAME="634"></A>;</STRONG></DT>
<DD>
</DD>
<DT><STRONG>CUDD_REORDER_SIFT<A NAME="635"></A>;</STRONG></DT>
<DD>
</DD>
<DT><STRONG>CUDD_REORDER_SIFT_CONVERGE<A NAME="636"></A>;</STRONG></DT>
<DD>
</DD>
<DT><STRONG>CUDD_REORDER_SYMM_SIFT<A NAME="637"></A>;</STRONG></DT>
<DD>
</DD>
<DT><STRONG>CUDD_REORDER_SYMM_SIFT_CONV<A NAME="638"></A>.</STRONG></DT>
<DD>
</DD>
</DL>
<P>
To create ZDD variable groups, the application calls <A NAME="tex2html93"
HREF="cuddExtDet.html#Cudd_MakeZddTreeNode"><EM> Cudd_MakeZddTreeNode</EM></A><A NAME="1583"></A>.
<P>
<H2><A NAME="SECTION000315000000000000000"></A>
<A NAME="sec:consist"></A>
<BR>
Keeping Consistent Variable Orders for BDDs and ZDDs
</H2>
<P>
Several applications that manipulate both BDDs and ZDDs benefit from
keeping a fixed correspondence between the order of the BDD variables
and the order of the ZDD variables. If each BDD variable corresponds
to a group of ZDD variables, then it is often desirable that the
groups of ZDD variables be in the same order as the corresponding BDD
variables. CUDD allows the ZDD order to
track the BDD order and vice versa. To have the ZDD order track
the BDD order, the application calls <A NAME="tex2html94"
HREF="cuddExtDet.html#Cudd_zddRealignEnable"><EM> Cudd_zddRealignEnable</EM></A><A NAME="1585"></A>. The
effect of this call can be reversed by calling <A NAME="tex2html95"
HREF="cuddExtDet.html#Cudd_zddRealignDisable"><EM> Cudd_zddRealignDisable</EM></A><A NAME="1587"></A>. When
ZDD realignment is in effect, automatic reordering of ZDDs should be
disabled.
<P>
<H2><A NAME="SECTION000316000000000000000"></A>
<A NAME="652"></A><A NAME="sec:hooks"></A>
<BR>
Hooks
</H2>
<P>
Hooks in CUDD are lists of application-specified functions to be run on
certain occasions. Each hook is identified by a constant of the
enumerated type <A NAME="tex2html96"
HREF="cuddExtDet.html#Cudd_HookType"><EM>Cudd_HookType</EM></A><A NAME="1589"></A>. In Version
2.4.1 hooks are defined for these occasions:
<UL>
<LI>before garbage collection (CUDD_PRE_GC_HOOK);
</LI>
<LI>after garbage collection (CUDD_POST_GC_HOOK);
</LI>
<LI>before variable reordering (CUDD_PRE_REORDERING_HOOK);
</LI>
<LI>after variable reordering (CUDD_POST_REORDERING_HOOK).
</LI>
</UL>
The current implementation of hooks is experimental. A function added
to a hook receives a pointer to the manager, a pointer to a constant
string, and a pointer to void as arguments; it must return 1 if
successful; 0 otherwise. The second argument is one of ``DD,''
``BDD,'' and ``ZDD.'' This allows the hook functions to tell the type
of diagram for which reordering or garbage collection takes place. The
third argument varies depending on the hook. The hook functions called
before or after garbage collection<A NAME="659"></A> do
not use it. The hook functions called before
reordering<A NAME="660"></A> are passed, in addition to the
pointer to the manager, also the method used for reordering. The hook
functions called after reordering are passed the start time. To add a
function to a hook, one uses <A NAME="tex2html97"
HREF="cuddExtDet.html#Cudd_AddHook"><EM> Cudd_AddHook</EM></A><A NAME="1591"></A>. The function of a given hook
are called in the order in which they were added to the hook. For
sample hook functions, one may look at
<I>Cudd_StdPreReordHook</I><A NAME="1593"></A> and
<I>Cudd_StdPostReordHook</I><A NAME="1595"></A>.
<P>
<H2><A NAME="SECTION000317000000000000000"></A>
<A NAME="669"></A><A NAME="670"></A><A NAME="sec:sis-vis"></A>
<BR>
The SIS/VIS Interface
</H2>
<P>
The CUDD package contains interface functions that emulate the
behavior of the original BDD package used in SIS [<A
HREF="node7.html#Sentov92">17</A>] and
in the newer
<A NAME="tex2html98"
HREF="http://vlsi.Colorado.EDU/~vis/">VIS</A>
[<A
HREF="node7.html#VIS">4</A>]. How to build VIS with CUDD is described
in the installation documents of VIS. (Version 1.1 and later.)
<P>
<H3><A NAME="SECTION000317100000000000000"></A>
<A NAME="677"></A><A NAME="sec:sis"></A>
<BR>
Using the CUDD Package in SIS
</H3>
<P>
This section describes how to build SIS with the CUDD package. Let
<TT>SISDIR<A NAME="679"></A></TT> designate the root of the directory
hierarchy where the sources for SIS reside. Let <TT> CUDDDIR<A NAME="680"></A></TT> be the root of the directory hierarchy where
the distribution of the CUDD package resides. To build SIS with the
CUDD package, follow these steps.
<OL>
<LI>Create directories <TT>SISDIR/sis/cudd</TT> and <TT> SISDIR/sis/mtr</TT>.
</LI>
<LI>Copy all files from <TT>CUDDDIR/cudd</TT> and <TT>CUDDDIR/sis</TT> to
<TT>SISDIR/sis/cudd</TT> and all files from <TT>CUDDDIR/mtr</TT> to <TT> SISDIR/sis/mtr</TT>.
</LI>
<LI>Copy <TT>CUDDDIR/cudd/doc/cudd.doc</TT> to <TT>SISDIR/sis/cudd</TT>;
also copy <TT>CUDDDIR/mtr/doc/mtr.doc</TT> to <TT>SISDIR/sis/mtr</TT>.
</LI>
<LI>In <TT>SISDIR/sis/cudd</TT> make <TT>bdd.h</TT> a symbolic link to
<TT>cuddBdd.h</TT>. (That is: <TT>ln -s cuddBdd.h bdd.h</TT>.)
</LI>
<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>.
</LI>
<LI>Copy <TT>CUDDDIR/sis/st.[ch]</TT> and <TT>CUDDDIR/st/doc/st.doc</TT>
to <TT>SISDIR/sis/st</TT>. (This will overwrite the original files: You
may want to save them beforehand.)
</LI>
<LI>From <TT>CUDDDIR/util</TT> copy <TT>datalimit.c</TT>
to <TT>SISDIR/sis/util</TT>. Update <TT>util.h</TT> and <TT>Makefile</TT>
in <TT>SISDIR/sis/util</TT>. Specifically, add the declaration
<TT>EXTERN long getSoftDataLimit();</TT> to <TT>util.h</TT> and add
<TT>datalimit.c</TT> to the list of source files (PSRC) in <TT>Makefile</TT>.
</LI>
<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
bdd</TT>.)
</LI>
<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
mtr to the list of directories to be made (DIRS).
</LI>
<LI>In <TT>SISDIR/sis/include</TT> make <TT>mtr.h</TT> a symbolic link to
<TT>../mtr/mtr.h</TT>.
</LI>
<LI>In <TT>SISDIR/sis/doc</TT> make <TT>cudd.doc</TT> a symbolic link to
<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
../mtr/mtr.doc .</TT>.)
</LI>
<LI>From <TT>SISDIR</TT> do <TT>make clean</TT> followed by <TT>make -i</TT>.
This should create a working copy of SIS that uses the CUDD package.
</LI>
</OL>
<P>
The replacement for the <TT>st</TT> library is because the version
shipped with the CUDD package tests for out-of-memory conditions.
Notice that the version of the <TT>st</TT> library to be used for
replacement is not the one used for the normal build, because the
latter has been modified for C++ compatibility. The above installation
procedure has been tested on SIS 1.3. SIS can be obtained via
anonymous FTP<A NAME="742"></A> from <A NAME="tex2html99"
HREF="ftp://ic.eecs.berkeley.edu"><TT> ic.eecs.berkeley.edu</TT></A>. To build SIS
1.3, you need <TT>sis-1.2.tar.Z</TT> and <TT>sis-1.2.patch1.Z</TT>. When
compiling on a DEC Alpha<A NAME="747"></A>, you should add the <TT> -ieee_with_no_inexact</TT> flag. (See
Section <A HREF="node3.html#sec:predef-const">3.5.2</A>.) Refer to the <TT>Makefile</TT> in the
top level directory of the distribution for how to compile with 32-bit
pointers.
<P>
<H2><A NAME="SECTION000318000000000000000"></A>
<A NAME="sec:dump"></A>
<BR>
Writing Decision Diagrams to a File
</H2>
<P>
The CUDD package provides several functions to write decision diagrams
to a file. <A NAME="tex2html101"
HREF="cuddExtDet.html#Cudd_DumpBlif"><EM>Cudd_DumpBlif</EM></A><A NAME="1597"></A> writes a
file in <EM>blif</EM> format. It is restricted to BDDs. The diagrams
are written as a network of multiplexers, one multiplexer for each
internal node of the BDD.
<P>
<A NAME="tex2html102"
HREF="cuddExtDet.html#Cudd_DumpDot"><EM>Cudd_DumpDot</EM></A><A NAME="1599"></A> produces input suitable to
the graph-drawing<A NAME="760"></A> program
<A NAME="tex2html103"
HREF="http://www.research.att.com/sw/tools/graphviz"><EM>dot</EM></A>
written by
Eleftherios Koutsofios and Stephen C. North. An example of drawing
produced by dot from the output of <A NAME="tex2html104"
HREF="cuddExtDet.html#Cudd_DumpDot"><EM>Cudd_DumpDot</EM></A>
is shown in
Figure <A HREF="node3.html#fi:phase">1</A>. It is restricted to BDDs and ADDs.
<P></P>
<DIV ALIGN="CENTER"><A NAME="fi:phase"></A><A NAME="1339"></A>
<TABLE>
<CAPTION ALIGN="BOTTOM"><STRONG>Figure 1:</STRONG>
A BDD representing a phase constraint for the optimization of
fixed-polarity Reed-Muller forms. The label of each node is the
unique part of the node address. All nodes on the same level
correspond to the same variable, whose name is shown at the left of
the diagram. Dotted lines indicate complement<A NAME="768"></A>
arcs. Dashed lines indicate regular<A NAME="769"></A> ``else"
arcs.</CAPTION>
<TR><TD><IMG
WIDTH="429" HEIGHT="701" BORDER="0"
SRC="img22.png"
ALT="\begin{figure}\centerline{\epsfig{file=phase.ps,height=15.5cm}}\end{figure}"></TD></TR>
</TABLE>
</DIV><P></P>
<A NAME="tex2html105"
HREF="cuddExtDet.html#Cudd_zddDumpDot"><EM>Cudd_zddDumpDot</EM></A><A NAME="1601"></A> is the analog of <A NAME="tex2html106"
HREF="cuddExtDet.html#Cudd_DumpDot"><EM> Cudd_DumpDot</EM></A>
for ZDDs.
<P>
<A NAME="tex2html107"
HREF="cuddExtDet.html#Cudd_DumpDaVinci"><EM>Cudd_DumpDaVinci</EM></A><A NAME="1603"></A> produces input suitable to
the graph-drawing<A NAME="780"></A> program
<A NAME="tex2html108"
HREF="ftp://ftp.uni-bremen.de/pub/graphics/daVinci"><EM> daVinci</EM></A>
developed
at the University of Bremen. It is restricted to BDDs and ADDs.
<P>
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.
<P>
<H2><A NAME="SECTION000319000000000000000"></A>
<A NAME="sec:save-restore"></A>
<BR>
Saving and Restoring BDDs
</H2>
<P>
The <A NAME="tex2html109"
HREF="ftp://ftp.polito.it/pub/research/dddmp/"><EM>dddmp</EM></A>
library<A NAME="789"></A> by Gianpiero Cabodi and
Stefano Quer allows a CUDD application to save BDDs to disk in compact
form for later retrieval. See the library's own documentation for the
details.
<P>
<HR>
<!--Navigation Panel-->
<A NAME="tex2html272"
HREF="node4.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="icons/next.png"></A>
<A NAME="tex2html268"
HREF="cuddIntro.html">
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="icons/up.png"></A>
<A NAME="tex2html262"
HREF="node2.html">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="icons/prev.png"></A>
<A NAME="tex2html270"
HREF="node8.html">
<IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
SRC="icons/index.png"></A>
<BR>
<B> Next:</B> <A NAME="tex2html273"
HREF="node4.html">Programmer's Manual</A>
<B> Up:</B> <A NAME="tex2html269"
HREF="cuddIntro.html">CUDD: CU Decision Diagram</A>
<B> Previous:</B> <A NAME="tex2html263"
HREF="node2.html">How to Get CUDD</A>
  <B> <A NAME="tex2html271"
HREF="node8.html">Index</A></B>
<!--End of Navigation Panel-->
<ADDRESS>
Fabio Somenzi
2005-05-17
</ADDRESS>
</BODY>
</HTML>
distrib
>
Mandriva
>
2010.0
>
i586
>
media
>
contrib-release
>
by-pkgid
>
a24e1a39141f9b4ca49bd1e2e23a54ba
>
files
>
1091
