You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
693 lines
27 KiB
693 lines
27 KiB
<HTML>
|
|
<HEAD><TITLE>The dddmp package</TITLE></HEAD>
|
|
<BODY>
|
|
|
|
<DL>
|
|
<dt><pre>
|
|
<A NAME="Dddmp_Bin2Text"></A>
|
|
int <I></I>
|
|
<B>Dddmp_Bin2Text</B>(
|
|
char * <b>filein</b>, <i>IN: name of binary file</i>
|
|
char * <b>fileout</b> <i>IN: name of ASCII file</i>
|
|
)
|
|
</pre>
|
|
<dd> Converts from binary to ASCII format. A BDD array is loaded and
|
|
and stored to the target file.
|
|
<p>
|
|
|
|
<dd> <b>Side Effects</b> None
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_Text2Bin()">Dddmp_Text2Bin()</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_Text2Bin"></A>
|
|
int <I></I>
|
|
<B>Dddmp_Text2Bin</B>(
|
|
char * <b>filein</b>, <i>IN: name of ASCII file</i>
|
|
char * <b>fileout</b> <i>IN: name of binary file</i>
|
|
)
|
|
</pre>
|
|
<dd> Converts from ASCII to binary format. A BDD array is loaded and
|
|
and stored to the target file.
|
|
<p>
|
|
|
|
<dd> <b>Side Effects</b> None
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_Bin2Text()">Dddmp_Bin2Text()</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddAddArrayLoad"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddAddArrayLoad</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
|
|
Dddmp_RootMatchType <b>rootMatchMode</b>, <i>IN: storing mode selector</i>
|
|
char ** <b>rootmatchnames</b>, <i>IN: sorted names for loaded roots</i>
|
|
Dddmp_VarMatchType <b>varMatchMode</b>, <i>IN: storing mode selector</i>
|
|
char ** <b>varmatchnames</b>, <i>IN: array of variable names, by ids</i>
|
|
int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by ids</i>
|
|
int * <b>varcomposeids</b>, <i>IN: array of new ids, by ids</i>
|
|
int <b>mode</b>, <i>IN: requested input file format</i>
|
|
char * <b>file</b>, <i>IN: file name</i>
|
|
FILE * <b>fp</b>, <i>IN: file pointer</i>
|
|
DdNode *** <b>pproots</b> <i>OUT: array of returned BDD roots</i>
|
|
)
|
|
</pre>
|
|
<dd> Reads a dump file representing the argument ADDs. See
|
|
BDD load functions for detailed explanation.
|
|
<p>
|
|
|
|
<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddAddArrayStore"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddAddArrayStore</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
|
|
char * <b>ddname</b>, <i>IN: DD name (or NULL)</i>
|
|
int <b>nRoots</b>, <i>IN: number of output BDD roots to be stored</i>
|
|
DdNode ** <b>f</b>, <i>IN: array of ADD roots to be stored</i>
|
|
char ** <b>rootnames</b>, <i>IN: array of root names (or NULL)</i>
|
|
char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
|
|
int * <b>auxids</b>, <i>IN: array of converted var IDs</i>
|
|
int <b>mode</b>, <i>IN: storing mode selector</i>
|
|
Dddmp_VarInfoType <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
|
|
char * <b>fname</b>, <i>IN: File name</i>
|
|
FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
|
|
)
|
|
</pre>
|
|
<dd> Dumps the argument array of ADDs to file. Dumping is
|
|
either in text or binary form. see the corresponding BDD dump
|
|
function for further details.
|
|
<p>
|
|
|
|
<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash
|
|
table. They are re-linked after the store operation in a
|
|
modified order.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddAddStore">Dddmp_cuddAddStore</a>
|
|
<a href="#Dddmp_cuddAddLoad">Dddmp_cuddAddLoad</a>
|
|
<a href="#Dddmp_cuddAddArrayLoad">Dddmp_cuddAddArrayLoad</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddAddLoad"></A>
|
|
DdNode * <I></I>
|
|
<B>Dddmp_cuddAddLoad</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: Manager</i>
|
|
Dddmp_VarMatchType <b>varMatchMode</b>, <i>IN: storing mode selector</i>
|
|
char ** <b>varmatchnames</b>, <i>IN: array of variable names by IDs</i>
|
|
int * <b>varmatchauxids</b>, <i>IN: array of variable auxids by IDs</i>
|
|
int * <b>varcomposeids</b>, <i>IN: array of new ids by IDs</i>
|
|
int <b>mode</b>, <i>IN: requested input file format</i>
|
|
char * <b>file</b>, <i>IN: file name</i>
|
|
FILE * <b>fp</b> <i>IN: file pointer</i>
|
|
)
|
|
</pre>
|
|
<dd> Reads a dump file representing the argument ADD.
|
|
Dddmp_cuddAddArrayLoad is used through a dummy array.
|
|
<p>
|
|
|
|
<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddAddStore">Dddmp_cuddAddStore</a>
|
|
<a href="#Dddmp_cuddAddArrayLoad">Dddmp_cuddAddArrayLoad</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddAddStore"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddAddStore</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
|
|
char * <b>ddname</b>, <i>IN: DD name (or NULL)</i>
|
|
DdNode * <b>f</b>, <i>IN: ADD root to be stored</i>
|
|
char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
|
|
int * <b>auxids</b>, <i>IN: array of converted var ids</i>
|
|
int <b>mode</b>, <i>IN: storing mode selector</i>
|
|
Dddmp_VarInfoType <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
|
|
char * <b>fname</b>, <i>IN: File name</i>
|
|
FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
|
|
)
|
|
</pre>
|
|
<dd> Dumps the argument ADD to file. Dumping is done through
|
|
Dddmp_cuddAddArrayStore, And a dummy array of 1 ADD root is
|
|
used for this purpose.
|
|
<p>
|
|
|
|
<dd> <b>Side Effects</b> Nodes are temporarily removed from unique hash. They are
|
|
re-linked after the store operation in a modified order.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddAddLoad">Dddmp_cuddAddLoad</a>
|
|
<a href="#Dddmp_cuddAddArrayLoad">Dddmp_cuddAddArrayLoad</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddBddArrayLoadCnf"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddBddArrayLoadCnf</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
|
|
Dddmp_RootMatchType <b>rootmatchmode</b>, <i>IN: storing mode selector</i>
|
|
char ** <b>rootmatchnames</b>, <i>IN: sorted names for loaded roots</i>
|
|
Dddmp_VarMatchType <b>varmatchmode</b>, <i>IN: storing mode selector</i>
|
|
char ** <b>varmatchnames</b>, <i>IN: array of variable names, by IDs</i>
|
|
int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by IDs</i>
|
|
int * <b>varcomposeids</b>, <i>IN: array of new ids, by IDs</i>
|
|
int <b>mode</b>, <i>IN: computation Mode</i>
|
|
char * <b>file</b>, <i>IN: file name</i>
|
|
FILE * <b>fp</b>, <i>IN: file pointer</i>
|
|
DdNode *** <b>rootsPtrPtr</b>, <i>OUT: array of returned BDD roots</i>
|
|
int * <b>nRoots</b> <i>OUT: number of BDDs returned</i>
|
|
)
|
|
</pre>
|
|
<dd> Reads a dump file representing the argument BDD in a
|
|
CNF formula.
|
|
<p>
|
|
|
|
<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddBddArrayLoad"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddBddArrayLoad</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
|
|
Dddmp_RootMatchType <b>rootMatchMode</b>, <i>IN: storing mode selector</i>
|
|
char ** <b>rootmatchnames</b>, <i>IN: sorted names for loaded roots</i>
|
|
Dddmp_VarMatchType <b>varMatchMode</b>, <i>IN: storing mode selector</i>
|
|
char ** <b>varmatchnames</b>, <i>IN: array of variable names, by ids</i>
|
|
int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by ids</i>
|
|
int * <b>varcomposeids</b>, <i>IN: array of new ids, by ids</i>
|
|
int <b>mode</b>, <i>IN: requested input file format</i>
|
|
char * <b>file</b>, <i>IN: file name</i>
|
|
FILE * <b>fp</b>, <i>IN: file pointer</i>
|
|
DdNode *** <b>pproots</b> <i>OUT: array of returned BDD roots</i>
|
|
)
|
|
</pre>
|
|
<dd> Reads a dump file representing the argument BDDs. The header is
|
|
common to both text and binary mode. The node list is either
|
|
in text or binary format. A dynamic vector of DD pointers
|
|
is allocated to support conversion from DD indexes to pointers.
|
|
Several criteria are supported for variable match between file
|
|
and dd manager. Several changes/permutations/compositions are allowed
|
|
for variables while loading DDs. Variable of the dd manager are allowed
|
|
to match with variables on file on ids, permids, varnames,
|
|
varauxids; also direct composition between ids and
|
|
composeids is supported. More in detail:
|
|
<ol>
|
|
<li> varMatchMode=DDDMP_VAR_MATCHIDS <p>
|
|
allows the loading of a DD keeping variable IDs unchanged
|
|
(regardless of the variable ordering of the reading manager); this
|
|
is useful, for example, when swapping DDs to file and restoring them
|
|
later from file, after possible variable reordering activations.
|
|
|
|
<li> varMatchMode=DDDMP_VAR_MATCHPERMIDS <p>
|
|
is used to allow variable match according to the position in the
|
|
ordering.
|
|
|
|
<li> varMatchMode=DDDMP_VAR_MATCHNAMES <p>
|
|
requires a non NULL varmatchnames parameter; this is a vector of
|
|
strings in one-to-one correspondence with variable IDs of the
|
|
reading manager. Variables in the DD file read are matched with
|
|
manager variables according to their name (a non NULL varnames
|
|
parameter was required while storing the DD file).
|
|
|
|
<li> varMatchMode=DDDMP_VAR_MATCHIDS <p>
|
|
has a meaning similar to DDDMP_VAR_MATCHNAMES, but integer auxiliary
|
|
IDs are used instead of strings; the additional non NULL
|
|
varmatchauxids parameter is needed.
|
|
|
|
<li> varMatchMode=DDDMP_VAR_COMPOSEIDS <p>
|
|
uses the additional varcomposeids parameter is used as array of
|
|
variable ids to be composed with ids stored in file.
|
|
</ol>
|
|
|
|
In the present implementation, the array varnames (3), varauxids (4)
|
|
and composeids (5) need to have one entry for each variable in the
|
|
DD manager (NULL pointers are allowed for unused variables
|
|
in varnames). Hence variables need to be already present in the
|
|
manager. All arrays are sorted according to IDs.
|
|
|
|
All the loaded BDDs are referenced before returning them.
|
|
<p>
|
|
|
|
<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddBddArrayStoreBlif"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddBddArrayStoreBlif</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
|
|
int <b>nroots</b>, <i>IN: number of output BDD roots to be stored</i>
|
|
DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
|
|
char ** <b>inputNames</b>, <i>IN: array of variable names (or NULL)</i>
|
|
char ** <b>outputNames</b>, <i>IN: array of root names (or NULL)</i>
|
|
char * <b>modelName</b>, <i>IN: Model Name</i>
|
|
char * <b>fname</b>, <i>IN: File name</i>
|
|
FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
|
|
)
|
|
</pre>
|
|
<dd> Dumps the argument BDD to file.
|
|
Dumping is done through Dddmp_cuddBddArrayStoreBLif.
|
|
A dummy array of 1 BDD root is used for this purpose.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStorePrefix">Dddmp_cuddBddArrayStorePrefix</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddBddArrayStoreCnf"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddBddArrayStoreCnf</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
|
|
DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
|
|
int <b>rootN</b>, <i>IN: # output BDD roots to be stored</i>
|
|
Dddmp_DecompCnfStoreType <b>mode</b>, <i>IN: format selection</i>
|
|
int <b>noHeader</b>, <i>IN: do not store header iff 1</i>
|
|
char ** <b>varNames</b>, <i>IN: array of variable names (or NULL)</i>
|
|
int * <b>bddIds</b>, <i>IN: array of converted var IDs</i>
|
|
int * <b>bddAuxIds</b>, <i>IN: array of BDD node Auxiliary Ids</i>
|
|
int * <b>cnfIds</b>, <i>IN: array of converted var IDs</i>
|
|
int <b>idInitial</b>, <i>IN: starting id for cutting variables</i>
|
|
int <b>edgeInTh</b>, <i>IN: Max # Incoming Edges</i>
|
|
int <b>pathLengthTh</b>, <i>IN: Max Path Length</i>
|
|
char * <b>fname</b>, <i>IN: file name</i>
|
|
FILE * <b>fp</b>, <i>IN: pointer to the store file</i>
|
|
int * <b>clauseNPtr</b>, <i>OUT: number of clause stored</i>
|
|
int * <b>varNewNPtr</b> <i>OUT: number of new variable created</i>
|
|
)
|
|
</pre>
|
|
<dd> Dumps the argument array of BDDs to file.
|
|
<p>
|
|
|
|
<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash
|
|
table. They are re-linked after the store operation in a
|
|
modified order.
|
|
Three methods are allowed:
|
|
* NodeByNode method: Insert a cut-point for each BDD node (but the
|
|
terminal nodes)
|
|
* MaxtermByMaxterm method: Insert no cut-points, i.e. the off-set of
|
|
trhe function is stored
|
|
* Best method: Tradeoff between the previous two methods.
|
|
Auxiliary variables, i.e., cut points are inserted following these
|
|
criterias:
|
|
* edgeInTh
|
|
indicates the maximum number of incoming edges up to which
|
|
no cut point (auxiliary variable) is inserted.
|
|
If edgeInTh:
|
|
* is equal to -1 no cut point due to incoming edges are inserted
|
|
(MaxtermByMaxterm method.)
|
|
* is equal to 0 a cut point is inserted for each node with a single
|
|
incoming edge, i.e., each node, (NodeByNode method).
|
|
* is equal to n a cut point is inserted for each node with (n+1)
|
|
incoming edges.
|
|
* pathLengthTh
|
|
indicates the maximum length path up to which no cut points
|
|
(auxiliary variable) is inserted.
|
|
If the path length between two nodes exceeds this value, a cut point
|
|
is inserted.
|
|
If pathLengthTh:
|
|
* is equal to -1 no cut point due path length are inserted
|
|
(MaxtermByMaxterm method.)
|
|
* is equal to 0 a cut point is inserted for each node (NodeByNode
|
|
method).
|
|
* is equal to n a cut point is inserted on path whose length is
|
|
equal to (n+1).
|
|
Notice that the maximum number of literals in a clause is equal
|
|
to (pathLengthTh + 2), i.e., for each path we have to keep into
|
|
account a CNF variable for each node plus 2 added variables for
|
|
the bottom and top-path cut points.
|
|
The stored file can contain a file header or not depending on the
|
|
noHeader parameter (IFF 0, usual setting, the header is usually stored.
|
|
This option can be useful in storing multiple BDDs, as separate BDDs,
|
|
on the same file leaving the opening of the file to the caller.
|
|
<p>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddBddArrayStorePrefix"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddBddArrayStorePrefix</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
|
|
int <b>nroots</b>, <i>IN: number of output BDD roots to be stored</i>
|
|
DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
|
|
char ** <b>inputNames</b>, <i>IN: array of variable names (or NULL)</i>
|
|
char ** <b>outputNames</b>, <i>IN: array of root names (or NULL)</i>
|
|
char * <b>modelName</b>, <i>IN: Model Name</i>
|
|
char * <b>fname</b>, <i>IN: File name</i>
|
|
FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
|
|
)
|
|
</pre>
|
|
<dd> Dumps the argument BDD to file.
|
|
Dumping is done through Dddmp_cuddBddArrayStorePrefix.
|
|
A dummy array of 1 BDD root is used for this purpose.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddBddArrayStoreSmv"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddBddArrayStoreSmv</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
|
|
int <b>nroots</b>, <i>IN: number of output BDD roots to be stored</i>
|
|
DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
|
|
char ** <b>inputNames</b>, <i>IN: array of variable names (or NULL)</i>
|
|
char ** <b>outputNames</b>, <i>IN: array of root names (or NULL)</i>
|
|
char * <b>modelName</b>, <i>IN: Model Name</i>
|
|
char * <b>fname</b>, <i>IN: File name</i>
|
|
FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
|
|
)
|
|
</pre>
|
|
<dd> Dumps the argument BDD to file.
|
|
Dumping is done through Dddmp_cuddBddArrayStorePrefix.
|
|
A dummy array of 1 BDD root is used for this purpose.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddBddArrayStore"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddBddArrayStore</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
|
|
char * <b>ddname</b>, <i>IN: dd name (or NULL)</i>
|
|
int <b>nRoots</b>, <i>IN: number of output BDD roots to be stored</i>
|
|
DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
|
|
char ** <b>rootnames</b>, <i>IN: array of root names (or NULL)</i>
|
|
char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
|
|
int * <b>auxids</b>, <i>IN: array of converted var IDs</i>
|
|
int <b>mode</b>, <i>IN: storing mode selector</i>
|
|
Dddmp_VarInfoType <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
|
|
char * <b>fname</b>, <i>IN: File name</i>
|
|
FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
|
|
)
|
|
</pre>
|
|
<dd> Dumps the argument array of BDDs to file. Dumping is either
|
|
in text or binary form. BDDs are stored to the fp (already
|
|
open) file if not NULL. Otherwise the file whose name is
|
|
fname is opened in write mode. The header has the same format
|
|
for both textual and binary dump. Names are allowed for input
|
|
variables (vnames) and for represented functions (rnames).
|
|
For sake of generality and because of dynamic variable
|
|
ordering both variable IDs and permuted IDs are included.
|
|
New IDs are also supported (auxids). Variables are identified
|
|
with incremental numbers. according with their positiom in
|
|
the support set. In text mode, an extra info may be added,
|
|
chosen among the following options: name, ID, PermID, or an
|
|
auxiliary id. Since conversion from DD pointers to integers
|
|
is required, DD nodes are temporarily removed from the unique
|
|
hash table. This allows the use of the next field to store
|
|
node IDs.
|
|
<p>
|
|
|
|
<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash
|
|
table. They are re-linked after the store operation in a
|
|
modified order.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
|
|
<a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
|
|
<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddBddDisplayBinary"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddBddDisplayBinary</B>(
|
|
char * <b>fileIn</b>, <i>IN: name of binary file</i>
|
|
char * <b>fileOut</b> <i>IN: name of text file</i>
|
|
)
|
|
</pre>
|
|
<dd> Display a binary dump file in a text file
|
|
<p>
|
|
|
|
<dd> <b>Side Effects</b> None
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
|
|
<a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddBddLoadCnf"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddBddLoadCnf</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
|
|
Dddmp_VarMatchType <b>varmatchmode</b>, <i>IN: storing mode selector</i>
|
|
char ** <b>varmatchnames</b>, <i>IN: array of variable names, by IDs</i>
|
|
int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by IDs</i>
|
|
int * <b>varcomposeids</b>, <i>IN: array of new ids accessed, by IDs</i>
|
|
int <b>mode</b>, <i>IN: computation mode</i>
|
|
char * <b>file</b>, <i>IN: file name</i>
|
|
FILE * <b>fp</b>, <i>IN: file pointer</i>
|
|
DdNode *** <b>rootsPtrPtr</b>, <i>OUT: array of returned BDD roots</i>
|
|
int * <b>nRoots</b> <i>OUT: number of BDDs returned</i>
|
|
)
|
|
</pre>
|
|
<dd> Reads a dump file representing the argument BDD in a
|
|
CNF formula.
|
|
Dddmp_cuddBddArrayLoadCnf is used through a dummy array.
|
|
The results is returned in different formats depending on the
|
|
mode selection:
|
|
IFF mode == 0 Return the Clauses without Conjunction
|
|
IFF mode == 1 Return the sets of BDDs without Quantification
|
|
IFF mode == 2 Return the sets of BDDs AFTER Existential Quantification
|
|
<p>
|
|
|
|
<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
|
|
<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddBddLoad"></A>
|
|
DdNode * <I></I>
|
|
<B>Dddmp_cuddBddLoad</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
|
|
Dddmp_VarMatchType <b>varMatchMode</b>, <i>IN: storing mode selector</i>
|
|
char ** <b>varmatchnames</b>, <i>IN: array of variable names - by IDs</i>
|
|
int * <b>varmatchauxids</b>, <i>IN: array of variable auxids - by IDs</i>
|
|
int * <b>varcomposeids</b>, <i>IN: array of new ids accessed - by IDs</i>
|
|
int <b>mode</b>, <i>IN: requested input file format</i>
|
|
char * <b>file</b>, <i>IN: file name</i>
|
|
FILE * <b>fp</b> <i>IN: file pointer</i>
|
|
)
|
|
</pre>
|
|
<dd> Reads a dump file representing the argument BDD.
|
|
Dddmp_cuddBddArrayLoad is used through a dummy array (see this
|
|
function's description for more details).
|
|
Mode, the requested input file format, is checked against
|
|
the file format.
|
|
The loaded BDDs is referenced before returning it.
|
|
<p>
|
|
|
|
<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
|
|
<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddBddStoreBlif"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddBddStoreBlif</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
|
|
int <b>nRoots</b>, <i>IN: Number of BDD roots</i>
|
|
DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
|
|
char ** <b>inputNames</b>, <i>IN: Array of variable names</i>
|
|
char ** <b>outputNames</b>, <i>IN: Array of root names</i>
|
|
char * <b>modelName</b>, <i>IN: Model Name</i>
|
|
char * <b>fileName</b>, <i>IN: File name</i>
|
|
FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
|
|
)
|
|
</pre>
|
|
<dd> Dumps the argument BDD to file.
|
|
Dumping is done through Dddmp_cuddBddArrayStoreBlif.
|
|
A dummy array of 1 BDD root is used for this purpose.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStorePrefix">Dddmp_cuddBddStorePrefix</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddBddStoreCnf"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddBddStoreCnf</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
|
|
DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
|
|
Dddmp_DecompCnfStoreType <b>mode</b>, <i>IN: format selection</i>
|
|
int <b>noHeader</b>, <i>IN: do not store header iff 1</i>
|
|
char ** <b>varNames</b>, <i>IN: array of variable names (or NULL)</i>
|
|
int * <b>bddIds</b>, <i>IN: array of var ids</i>
|
|
int * <b>bddAuxIds</b>, <i>IN: array of BDD node Auxiliary Ids</i>
|
|
int * <b>cnfIds</b>, <i>IN: array of CNF var ids</i>
|
|
int <b>idInitial</b>, <i>IN: starting id for cutting variables</i>
|
|
int <b>edgeInTh</b>, <i>IN: Max # Incoming Edges</i>
|
|
int <b>pathLengthTh</b>, <i>IN: Max Path Length</i>
|
|
char * <b>fname</b>, <i>IN: file name</i>
|
|
FILE * <b>fp</b>, <i>IN: pointer to the store file</i>
|
|
int * <b>clauseNPtr</b>, <i>OUT: number of clause stored</i>
|
|
int * <b>varNewNPtr</b> <i>OUT: number of new variable created</i>
|
|
)
|
|
</pre>
|
|
<dd> Dumps the argument BDD to file.
|
|
This task is performed by calling the function
|
|
Dddmp_cuddBddArrayStoreCnf.
|
|
<p>
|
|
|
|
<dd> <b>Side Effects</b> Nodes are temporarily removed from unique hash. They are
|
|
re-linked after the store operation in a modified order.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStoreCnf">Dddmp_cuddBddArrayStoreCnf</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddBddStorePrefix"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddBddStorePrefix</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
|
|
int <b>nRoots</b>, <i>IN: Number of BDD roots</i>
|
|
DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
|
|
char ** <b>inputNames</b>, <i>IN: Array of variable names</i>
|
|
char ** <b>outputNames</b>, <i>IN: Array of root names</i>
|
|
char * <b>modelName</b>, <i>IN: Model Name</i>
|
|
char * <b>fileName</b>, <i>IN: File name</i>
|
|
FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
|
|
)
|
|
</pre>
|
|
<dd> Dumps the argument BDD to file.
|
|
Dumping is done through Dddmp_cuddBddArrayStorePrefix.
|
|
A dummy array of 1 BDD root is used for this purpose.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddBddStoreSmv"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddBddStoreSmv</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
|
|
int <b>nRoots</b>, <i>IN: Number of BDD roots</i>
|
|
DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
|
|
char ** <b>inputNames</b>, <i>IN: Array of variable names</i>
|
|
char ** <b>outputNames</b>, <i>IN: Array of root names</i>
|
|
char * <b>modelName</b>, <i>IN: Model Name</i>
|
|
char * <b>fileName</b>, <i>IN: File name</i>
|
|
FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
|
|
)
|
|
</pre>
|
|
<dd> Dumps the argument BDD to file.
|
|
Dumping is done through Dddmp_cuddBddArrayStorePrefix.
|
|
A dummy array of 1 BDD root is used for this purpose.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddBddStore"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddBddStore</B>(
|
|
DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
|
|
char * <b>ddname</b>, <i>IN: DD name (or NULL)</i>
|
|
DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
|
|
char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
|
|
int * <b>auxids</b>, <i>IN: array of converted var ids</i>
|
|
int <b>mode</b>, <i>IN: storing mode selector</i>
|
|
Dddmp_VarInfoType <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
|
|
char * <b>fname</b>, <i>IN: File name</i>
|
|
FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
|
|
)
|
|
</pre>
|
|
<dd> Dumps the argument BDD to file. Dumping is done through
|
|
Dddmp_cuddBddArrayStore. A dummy array of 1 BDD root is
|
|
used for this purpose.
|
|
<p>
|
|
|
|
<dd> <b>Side Effects</b> Nodes are temporarily removed from unique hash. They are
|
|
re-linked after the store operation in a modified order.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
|
|
<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddHeaderLoadCnf"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddHeaderLoadCnf</B>(
|
|
int * <b>nVars</b>, <i>OUT: number of DD variables</i>
|
|
int * <b>nsuppvars</b>, <i>OUT: number of support variables</i>
|
|
char *** <b>suppVarNames</b>, <i>OUT: array of support variable names</i>
|
|
char *** <b>orderedVarNames</b>, <i>OUT: array of variable names</i>
|
|
int ** <b>varIds</b>, <i>OUT: array of variable ids</i>
|
|
int ** <b>varComposeIds</b>, <i>OUT: array of permids ids</i>
|
|
int ** <b>varAuxIds</b>, <i>OUT: array of variable aux ids</i>
|
|
int * <b>nRoots</b>, <i>OUT: number of root in the file</i>
|
|
char * <b>file</b>, <i>IN: file name</i>
|
|
FILE * <b>fp</b> <i>IN: file pointer</i>
|
|
)
|
|
</pre>
|
|
<dd> Reads the header of a dump file representing the argument BDDs.
|
|
Returns main information regarding DD type stored in the file,
|
|
the variable ordering used, the number of variables, etc.
|
|
It reads only the header of the file NOT the BDD/ADD section.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
|
|
</code>
|
|
|
|
<dt><pre>
|
|
<A NAME="Dddmp_cuddHeaderLoad"></A>
|
|
int <I></I>
|
|
<B>Dddmp_cuddHeaderLoad</B>(
|
|
Dddmp_DecompType * <b>ddType</b>, <i>OUT: selects the proper decomp type</i>
|
|
int * <b>nVars</b>, <i>OUT: number of DD variables</i>
|
|
int * <b>nsuppvars</b>, <i>OUT: number of support variables</i>
|
|
char *** <b>suppVarNames</b>, <i>OUT: array of support variable names</i>
|
|
char *** <b>orderedVarNames</b>, <i>OUT: array of variable names</i>
|
|
int ** <b>varIds</b>, <i>OUT: array of variable ids</i>
|
|
int ** <b>varComposeIds</b>, <i>OUT: array of permids ids</i>
|
|
int ** <b>varAuxIds</b>, <i>OUT: array of variable aux ids</i>
|
|
int * <b>nRoots</b>, <i>OUT: number of root in the file</i>
|
|
char * <b>file</b>, <i>IN: file name</i>
|
|
FILE * <b>fp</b> <i>IN: file pointer</i>
|
|
)
|
|
</pre>
|
|
<dd> Reads the header of a dump file representing the argument BDDs.
|
|
Returns main information regarding DD type stored in the file,
|
|
the variable ordering used, the number of variables, etc.
|
|
It reads only the header of the file NOT the BDD/ADD section.
|
|
<p>
|
|
|
|
<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
|
|
</code>
|
|
|
|
|
|
</DL>
|
|
<HR>
|
|
Last updated on 1040218 17h14
|
|
</BODY></HTML>
|