source: icGREP/icgrep-devel/cudd-2.5.1/dddmp/doc/dddmpExtDet.html @ 4597

Last change on this file since 4597 was 4597, checked in by nmedfort, 4 years ago

Upload of the CUDD library.

File size: 27.2 KB
Line 
1<HTML>
2<HEAD><TITLE>The dddmp package</TITLE></HEAD>
3<BODY>
4
5<DL>
6<dt><pre>
7<A NAME="Dddmp_Bin2Text"></A>
8int <I></I>
9<B>Dddmp_Bin2Text</B>(
10  char * <b>filein</b>, <i>IN: name of binary file</i>
11  char * <b>fileout</b> <i>IN: name of ASCII file</i>
12)
13</pre>
14<dd> Converts from binary to ASCII format. A BDD array is loaded and
15    and stored to the target file.
16<p>
17
18<dd> <b>Side Effects</b> None
19<p>
20
21<dd> <b>See Also</b> <code><a href="#Dddmp_Text2Bin()">Dddmp_Text2Bin()</a>
22</code>
23
24<dt><pre>
25<A NAME="Dddmp_Text2Bin"></A>
26int <I></I>
27<B>Dddmp_Text2Bin</B>(
28  char * <b>filein</b>, <i>IN: name of ASCII file</i>
29  char * <b>fileout</b> <i>IN: name of binary file</i>
30)
31</pre>
32<dd> Converts from ASCII to binary format. A BDD array is loaded and
33    and stored to the target file.
34<p>
35
36<dd> <b>Side Effects</b> None
37<p>
38
39<dd> <b>See Also</b> <code><a href="#Dddmp_Bin2Text()">Dddmp_Bin2Text()</a>
40</code>
41
42<dt><pre>
43<A NAME="Dddmp_cuddAddArrayLoad"></A>
44int <I></I>
45<B>Dddmp_cuddAddArrayLoad</B>(
46  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
47  Dddmp_RootMatchType  <b>rootMatchMode</b>, <i>IN: storing mode selector</i>
48  char ** <b>rootmatchnames</b>, <i>IN: sorted names for loaded roots</i>
49  Dddmp_VarMatchType  <b>varMatchMode</b>, <i>IN: storing mode selector</i>
50  char ** <b>varmatchnames</b>, <i>IN: array of variable names, by ids</i>
51  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by ids</i>
52  int * <b>varcomposeids</b>, <i>IN: array of new ids, by ids</i>
53  int  <b>mode</b>, <i>IN: requested input file format</i>
54  char * <b>file</b>, <i>IN: file name</i>
55  FILE * <b>fp</b>, <i>IN: file pointer</i>
56  DdNode *** <b>pproots</b> <i>OUT: array of returned BDD roots</i>
57)
58</pre>
59<dd> Reads a dump file representing the argument ADDs. See
60    BDD load functions for detailed explanation.
61<p>
62
63<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
64<p>
65
66<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
67</code>
68
69<dt><pre>
70<A NAME="Dddmp_cuddAddArrayStore"></A>
71int <I></I>
72<B>Dddmp_cuddAddArrayStore</B>(
73  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
74  char * <b>ddname</b>, <i>IN: DD name (or NULL)</i>
75  int  <b>nRoots</b>, <i>IN: number of output BDD roots to be stored</i>
76  DdNode ** <b>f</b>, <i>IN: array of ADD roots to be stored</i>
77  char ** <b>rootnames</b>, <i>IN: array of root names (or NULL)</i>
78  char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
79  int * <b>auxids</b>, <i>IN: array of converted var IDs</i>
80  int  <b>mode</b>, <i>IN: storing mode selector</i>
81  Dddmp_VarInfoType  <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
82  char * <b>fname</b>, <i>IN: File name</i>
83  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
84)
85</pre>
86<dd> Dumps the argument array of ADDs to file. Dumping is
87    either in text or binary form. see the corresponding BDD dump
88    function for further details.
89<p>
90
91<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash
92    table. They are re-linked after the store operation in a
93    modified order.
94<p>
95
96<dd> <b>See Also</b> <code><a href="#Dddmp_cuddAddStore">Dddmp_cuddAddStore</a>
97<a href="#Dddmp_cuddAddLoad">Dddmp_cuddAddLoad</a>
98<a href="#Dddmp_cuddAddArrayLoad">Dddmp_cuddAddArrayLoad</a>
99</code>
100
101<dt><pre>
102<A NAME="Dddmp_cuddAddLoad"></A>
103DdNode * <I></I>
104<B>Dddmp_cuddAddLoad</B>(
105  DdManager * <b>ddMgr</b>, <i>IN: Manager</i>
106  Dddmp_VarMatchType  <b>varMatchMode</b>, <i>IN: storing mode selector</i>
107  char ** <b>varmatchnames</b>, <i>IN: array of variable names by IDs</i>
108  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids by IDs</i>
109  int * <b>varcomposeids</b>, <i>IN: array of new ids by IDs</i>
110  int  <b>mode</b>, <i>IN: requested input file format</i>
111  char * <b>file</b>, <i>IN: file name</i>
112  FILE * <b>fp</b> <i>IN: file pointer</i>
113)
114</pre>
115<dd> Reads a dump file representing the argument ADD.
116    Dddmp_cuddAddArrayLoad is used through a dummy array.
117<p>
118
119<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
120<p>
121
122<dd> <b>See Also</b> <code><a href="#Dddmp_cuddAddStore">Dddmp_cuddAddStore</a>
123<a href="#Dddmp_cuddAddArrayLoad">Dddmp_cuddAddArrayLoad</a>
124</code>
125
126<dt><pre>
127<A NAME="Dddmp_cuddAddStore"></A>
128int <I></I>
129<B>Dddmp_cuddAddStore</B>(
130  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
131  char * <b>ddname</b>, <i>IN: DD name (or NULL)</i>
132  DdNode * <b>f</b>, <i>IN: ADD root to be stored</i>
133  char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
134  int * <b>auxids</b>, <i>IN: array of converted var ids</i>
135  int  <b>mode</b>, <i>IN: storing mode selector</i>
136  Dddmp_VarInfoType  <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
137  char * <b>fname</b>, <i>IN: File name</i>
138  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
139)
140</pre>
141<dd> Dumps the argument ADD to file. Dumping is done through
142    Dddmp_cuddAddArrayStore, And a dummy array of 1 ADD root is
143    used for this purpose.
144<p>
145
146<dd> <b>Side Effects</b> Nodes are temporarily removed from unique hash. They are
147    re-linked after the store operation in a modified order.
148<p>
149
150<dd> <b>See Also</b> <code><a href="#Dddmp_cuddAddLoad">Dddmp_cuddAddLoad</a>
151<a href="#Dddmp_cuddAddArrayLoad">Dddmp_cuddAddArrayLoad</a>
152</code>
153
154<dt><pre>
155<A NAME="Dddmp_cuddBddArrayLoadCnf"></A>
156int <I></I>
157<B>Dddmp_cuddBddArrayLoadCnf</B>(
158  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
159  Dddmp_RootMatchType  <b>rootmatchmode</b>, <i>IN: storing mode selector</i>
160  char ** <b>rootmatchnames</b>, <i>IN: sorted names for loaded roots</i>
161  Dddmp_VarMatchType  <b>varmatchmode</b>, <i>IN: storing mode selector</i>
162  char ** <b>varmatchnames</b>, <i>IN: array of variable names, by IDs</i>
163  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by IDs</i>
164  int * <b>varcomposeids</b>, <i>IN: array of new ids, by IDs</i>
165  int  <b>mode</b>, <i>IN: computation Mode</i>
166  char * <b>file</b>, <i>IN: file name</i>
167  FILE * <b>fp</b>, <i>IN: file pointer</i>
168  DdNode *** <b>rootsPtrPtr</b>, <i>OUT: array of returned BDD roots</i>
169  int * <b>nRoots</b> <i>OUT: number of BDDs returned</i>
170)
171</pre>
172<dd> Reads a dump file representing the argument BDD in a
173    CNF formula.
174<p>
175
176<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
177<p>
178
179<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
180</code>
181
182<dt><pre>
183<A NAME="Dddmp_cuddBddArrayLoad"></A>
184int <I></I>
185<B>Dddmp_cuddBddArrayLoad</B>(
186  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
187  Dddmp_RootMatchType  <b>rootMatchMode</b>, <i>IN: storing mode selector</i>
188  char ** <b>rootmatchnames</b>, <i>IN: sorted names for loaded roots</i>
189  Dddmp_VarMatchType  <b>varMatchMode</b>, <i>IN: storing mode selector</i>
190  char ** <b>varmatchnames</b>, <i>IN: array of variable names, by ids</i>
191  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by ids</i>
192  int * <b>varcomposeids</b>, <i>IN: array of new ids, by ids</i>
193  int  <b>mode</b>, <i>IN: requested input file format</i>
194  char * <b>file</b>, <i>IN: file name</i>
195  FILE * <b>fp</b>, <i>IN: file pointer</i>
196  DdNode *** <b>pproots</b> <i>OUT: array of returned BDD roots</i>
197)
198</pre>
199<dd> Reads a dump file representing the argument BDDs. The header is
200    common to both text and binary mode. The node list is either
201    in text or binary format. A dynamic vector of DD pointers
202    is allocated to support conversion from DD indexes to pointers.
203    Several criteria are supported for variable match between file
204    and dd manager. Several changes/permutations/compositions are allowed
205    for variables while loading DDs. Variable of the dd manager are allowed
206    to match with variables on file on ids, permids, varnames,
207    varauxids; also direct composition between ids and
208    composeids is supported. More in detail:
209    <ol>
210    <li> varMatchMode=DDDMP_VAR_MATCHIDS <p>
211    allows the loading of a DD keeping variable IDs unchanged
212    (regardless of the variable ordering of the reading manager); this
213    is useful, for example, when swapping DDs to file and restoring them
214    later from file, after possible variable reordering activations.
215   
216    <li> varMatchMode=DDDMP_VAR_MATCHPERMIDS <p>
217    is used to allow variable match according to the position in the
218    ordering.
219   
220    <li> varMatchMode=DDDMP_VAR_MATCHNAMES <p>
221    requires a non NULL varmatchnames parameter; this is a vector of
222    strings in one-to-one correspondence with variable IDs of the
223    reading manager. Variables in the DD file read are matched with
224    manager variables according to their name (a non NULL varnames
225    parameter was required while storing the DD file).
226   
227    <li> varMatchMode=DDDMP_VAR_MATCHIDS <p>
228    has a meaning similar to DDDMP_VAR_MATCHNAMES, but integer auxiliary
229    IDs are used instead of strings; the additional non NULL
230    varmatchauxids parameter is needed.
231   
232    <li> varMatchMode=DDDMP_VAR_COMPOSEIDS <p>
233    uses the additional varcomposeids parameter is used as array of
234    variable ids to be composed with ids stored in file.
235    </ol>
236   
237    In the present implementation, the array varnames (3), varauxids (4)
238    and composeids (5) need to have one entry for each variable in the
239    DD manager (NULL pointers are allowed for unused variables
240    in varnames). Hence variables need to be already present in the
241    manager. All arrays are sorted according to IDs.
242
243    All the loaded BDDs are referenced before returning them.
244<p>
245
246<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
247<p>
248
249<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
250</code>
251
252<dt><pre>
253<A NAME="Dddmp_cuddBddArrayStoreBlif"></A>
254int <I></I>
255<B>Dddmp_cuddBddArrayStoreBlif</B>(
256  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
257  int  <b>nroots</b>, <i>IN: number of output BDD roots to be stored</i>
258  DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
259  char ** <b>inputNames</b>, <i>IN: array of variable names (or NULL)</i>
260  char ** <b>outputNames</b>, <i>IN: array of root names (or NULL)</i>
261  char * <b>modelName</b>, <i>IN: Model Name</i>
262  char * <b>fname</b>, <i>IN: File name</i>
263  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
264)
265</pre>
266<dd> Dumps the argument BDD to file.
267    Dumping is done through Dddmp_cuddBddArrayStoreBLif.
268    A dummy array of 1 BDD root is used for this purpose.
269<p>
270
271<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStorePrefix">Dddmp_cuddBddArrayStorePrefix</a>
272</code>
273
274<dt><pre>
275<A NAME="Dddmp_cuddBddArrayStoreCnf"></A>
276int <I></I>
277<B>Dddmp_cuddBddArrayStoreCnf</B>(
278  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
279  DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
280  int  <b>rootN</b>, <i>IN: # output BDD roots to be stored</i>
281  Dddmp_DecompCnfStoreType  <b>mode</b>, <i>IN: format selection</i>
282  int  <b>noHeader</b>, <i>IN: do not store header iff 1</i>
283  char ** <b>varNames</b>, <i>IN: array of variable names (or NULL)</i>
284  int * <b>bddIds</b>, <i>IN: array of converted var IDs</i>
285  int * <b>bddAuxIds</b>, <i>IN: array of BDD node Auxiliary Ids</i>
286  int * <b>cnfIds</b>, <i>IN: array of converted var IDs</i>
287  int  <b>idInitial</b>, <i>IN: starting id for cutting variables</i>
288  int  <b>edgeInTh</b>, <i>IN: Max # Incoming Edges</i>
289  int  <b>pathLengthTh</b>, <i>IN: Max Path Length</i>
290  char * <b>fname</b>, <i>IN: file name</i>
291  FILE * <b>fp</b>, <i>IN: pointer to the store file</i>
292  int * <b>clauseNPtr</b>, <i>OUT: number of clause stored</i>
293  int * <b>varNewNPtr</b> <i>OUT: number of new variable created</i>
294)
295</pre>
296<dd> Dumps the argument array of BDDs to file.
297<p>
298
299<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash
300    table. They are re-linked after the store operation in a
301    modified order.
302    Three methods are allowed:
303    * NodeByNode method: Insert a cut-point for each BDD node (but the
304                         terminal nodes)
305    * MaxtermByMaxterm method: Insert no cut-points, i.e. the off-set of
306                               trhe function is stored
307    * Best method: Tradeoff between the previous two methods.
308      Auxiliary variables, i.e., cut points are inserted following these
309      criterias:
310      * edgeInTh
311        indicates the maximum number of incoming edges up to which
312        no cut point (auxiliary variable) is inserted.
313        If edgeInTh:
314        * is equal to -1 no cut point due to incoming edges are inserted
315          (MaxtermByMaxterm method.)
316        * is equal to 0 a cut point is inserted for each node with a single
317          incoming edge, i.e., each node, (NodeByNode method).
318        * is equal to n a cut point is inserted for each node with (n+1)
319          incoming edges.
320      * pathLengthTh
321        indicates the maximum length path up to which no cut points
322        (auxiliary variable) is inserted.
323        If the path length between two nodes exceeds this value, a cut point
324        is inserted.
325        If pathLengthTh:
326        * is equal to -1 no cut point due path length are inserted
327          (MaxtermByMaxterm method.)
328        * is equal to 0 a cut point is inserted for each node (NodeByNode
329          method).
330        * is equal to n a cut point is inserted on path whose length is
331          equal to (n+1).
332        Notice that the maximum number of literals in a clause is equal
333        to (pathLengthTh + 2), i.e., for each path we have to keep into
334        account a CNF variable for each node plus 2 added variables for
335        the bottom and top-path cut points.
336    The stored file can contain a file header or not depending on the
337    noHeader parameter (IFF 0, usual setting, the header is usually stored.
338    This option can be useful in storing multiple BDDs, as separate BDDs,
339    on the same file leaving the opening of the file to the caller.
340<p>
341
342<dt><pre>
343<A NAME="Dddmp_cuddBddArrayStorePrefix"></A>
344int <I></I>
345<B>Dddmp_cuddBddArrayStorePrefix</B>(
346  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
347  int  <b>nroots</b>, <i>IN: number of output BDD roots to be stored</i>
348  DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
349  char ** <b>inputNames</b>, <i>IN: array of variable names (or NULL)</i>
350  char ** <b>outputNames</b>, <i>IN: array of root names (or NULL)</i>
351  char * <b>modelName</b>, <i>IN: Model Name</i>
352  char * <b>fname</b>, <i>IN: File name</i>
353  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
354)
355</pre>
356<dd> Dumps the argument BDD to file.
357    Dumping is done through Dddmp_cuddBddArrayStorePrefix.
358    A dummy array of 1 BDD root is used for this purpose.
359<p>
360
361<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
362</code>
363
364<dt><pre>
365<A NAME="Dddmp_cuddBddArrayStoreSmv"></A>
366int <I></I>
367<B>Dddmp_cuddBddArrayStoreSmv</B>(
368  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
369  int  <b>nroots</b>, <i>IN: number of output BDD roots to be stored</i>
370  DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
371  char ** <b>inputNames</b>, <i>IN: array of variable names (or NULL)</i>
372  char ** <b>outputNames</b>, <i>IN: array of root names (or NULL)</i>
373  char * <b>modelName</b>, <i>IN: Model Name</i>
374  char * <b>fname</b>, <i>IN: File name</i>
375  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
376)
377</pre>
378<dd> Dumps the argument BDD to file.
379    Dumping is done through Dddmp_cuddBddArrayStorePrefix.
380    A dummy array of 1 BDD root is used for this purpose.
381<p>
382
383<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
384</code>
385
386<dt><pre>
387<A NAME="Dddmp_cuddBddArrayStore"></A>
388int <I></I>
389<B>Dddmp_cuddBddArrayStore</B>(
390  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
391  char * <b>ddname</b>, <i>IN: dd name (or NULL)</i>
392  int  <b>nRoots</b>, <i>IN: number of output BDD roots to be stored</i>
393  DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
394  char ** <b>rootnames</b>, <i>IN: array of root names (or NULL)</i>
395  char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
396  int * <b>auxids</b>, <i>IN: array of converted var IDs</i>
397  int  <b>mode</b>, <i>IN: storing mode selector</i>
398  Dddmp_VarInfoType  <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
399  char * <b>fname</b>, <i>IN: File name</i>
400  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
401)
402</pre>
403<dd> Dumps the argument array of BDDs to file. Dumping is either
404    in text or binary form.  BDDs are stored to the fp (already
405    open) file if not NULL. Otherwise the file whose name is
406    fname is opened in write mode. The header has the same format
407    for both textual and binary dump. Names are allowed for input
408    variables (vnames) and for represented functions (rnames).
409    For sake of generality and because of dynamic variable
410    ordering both variable IDs and permuted IDs are included.
411    New IDs are also supported (auxids). Variables are identified
412    with incremental numbers. according with their positiom in
413    the support set. In text mode, an extra info may be added,
414    chosen among the following options: name, ID, PermID, or an
415    auxiliary id. Since conversion from DD pointers to integers
416    is required, DD nodes are temporarily removed from the unique
417    hash table. This allows the use of the next field to store
418    node IDs.
419<p>
420
421<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash
422    table. They are re-linked after the store operation in a
423    modified order.
424<p>
425
426<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
427<a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
428<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
429</code>
430
431<dt><pre>
432<A NAME="Dddmp_cuddBddDisplayBinary"></A>
433int <I></I>
434<B>Dddmp_cuddBddDisplayBinary</B>(
435  char * <b>fileIn</b>, <i>IN: name of binary file</i>
436  char * <b>fileOut</b> <i>IN: name of text file</i>
437)
438</pre>
439<dd> Display a binary dump file in a text file
440<p>
441
442<dd> <b>Side Effects</b> None
443<p>
444
445<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
446<a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
447</code>
448
449<dt><pre>
450<A NAME="Dddmp_cuddBddLoadCnf"></A>
451int <I></I>
452<B>Dddmp_cuddBddLoadCnf</B>(
453  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
454  Dddmp_VarMatchType  <b>varmatchmode</b>, <i>IN: storing mode selector</i>
455  char ** <b>varmatchnames</b>, <i>IN: array of variable names, by IDs</i>
456  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by IDs</i>
457  int * <b>varcomposeids</b>, <i>IN: array of new ids accessed, by IDs</i>
458  int  <b>mode</b>, <i>IN: computation mode</i>
459  char * <b>file</b>, <i>IN: file name</i>
460  FILE * <b>fp</b>, <i>IN: file pointer</i>
461  DdNode *** <b>rootsPtrPtr</b>, <i>OUT: array of returned BDD roots</i>
462  int * <b>nRoots</b> <i>OUT: number of BDDs returned</i>
463)
464</pre>
465<dd> Reads a dump file representing the argument BDD in a
466    CNF formula.
467    Dddmp_cuddBddArrayLoadCnf is used through a dummy array.
468    The results is returned in different formats depending on the
469    mode selection:
470      IFF mode == 0 Return the Clauses without Conjunction
471      IFF mode == 1 Return the sets of BDDs without Quantification
472      IFF mode == 2 Return the sets of BDDs AFTER Existential Quantification
473<p>
474
475<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
476<p>
477
478<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
479<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
480</code>
481
482<dt><pre>
483<A NAME="Dddmp_cuddBddLoad"></A>
484DdNode * <I></I>
485<B>Dddmp_cuddBddLoad</B>(
486  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
487  Dddmp_VarMatchType  <b>varMatchMode</b>, <i>IN: storing mode selector</i>
488  char ** <b>varmatchnames</b>, <i>IN: array of variable names - by IDs</i>
489  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids - by IDs</i>
490  int * <b>varcomposeids</b>, <i>IN: array of new ids accessed - by IDs</i>
491  int  <b>mode</b>, <i>IN: requested input file format</i>
492  char * <b>file</b>, <i>IN: file name</i>
493  FILE * <b>fp</b> <i>IN: file pointer</i>
494)
495</pre>
496<dd> Reads a dump file representing the argument BDD.
497    Dddmp_cuddBddArrayLoad is used through a dummy array (see this
498    function's description for more details).
499    Mode, the requested input file format, is checked against
500    the file format.
501    The loaded BDDs is referenced before returning it.
502<p>
503
504<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
505<p>
506
507<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
508<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
509</code>
510
511<dt><pre>
512<A NAME="Dddmp_cuddBddStoreBlif"></A>
513int <I></I>
514<B>Dddmp_cuddBddStoreBlif</B>(
515  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
516  int  <b>nRoots</b>, <i>IN: Number of BDD roots</i>
517  DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
518  char ** <b>inputNames</b>, <i>IN: Array of variable names</i>
519  char ** <b>outputNames</b>, <i>IN: Array of root names</i>
520  char * <b>modelName</b>, <i>IN: Model Name</i>
521  char * <b>fileName</b>, <i>IN: File name</i>
522  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
523)
524</pre>
525<dd> Dumps the argument BDD to file.
526    Dumping is done through Dddmp_cuddBddArrayStoreBlif.
527    A dummy array of 1 BDD root is used for this purpose.
528<p>
529
530<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStorePrefix">Dddmp_cuddBddStorePrefix</a>
531</code>
532
533<dt><pre>
534<A NAME="Dddmp_cuddBddStoreCnf"></A>
535int <I></I>
536<B>Dddmp_cuddBddStoreCnf</B>(
537  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
538  DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
539  Dddmp_DecompCnfStoreType  <b>mode</b>, <i>IN: format selection</i>
540  int  <b>noHeader</b>, <i>IN: do not store header iff 1</i>
541  char ** <b>varNames</b>, <i>IN: array of variable names (or NULL)</i>
542  int * <b>bddIds</b>, <i>IN: array of var ids</i>
543  int * <b>bddAuxIds</b>, <i>IN: array of BDD node Auxiliary Ids</i>
544  int * <b>cnfIds</b>, <i>IN: array of CNF var ids</i>
545  int  <b>idInitial</b>, <i>IN: starting id for cutting variables</i>
546  int  <b>edgeInTh</b>, <i>IN: Max # Incoming Edges</i>
547  int  <b>pathLengthTh</b>, <i>IN: Max Path Length</i>
548  char * <b>fname</b>, <i>IN: file name</i>
549  FILE * <b>fp</b>, <i>IN: pointer to the store file</i>
550  int * <b>clauseNPtr</b>, <i>OUT: number of clause stored</i>
551  int * <b>varNewNPtr</b> <i>OUT: number of new variable created</i>
552)
553</pre>
554<dd> Dumps the argument BDD to file.
555    This task is performed by calling the function
556    Dddmp_cuddBddArrayStoreCnf.
557<p>
558
559<dd> <b>Side Effects</b> Nodes are temporarily removed from unique hash. They are
560    re-linked after the store operation in a modified order.
561<p>
562
563<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStoreCnf">Dddmp_cuddBddArrayStoreCnf</a>
564</code>
565
566<dt><pre>
567<A NAME="Dddmp_cuddBddStorePrefix"></A>
568int <I></I>
569<B>Dddmp_cuddBddStorePrefix</B>(
570  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
571  int  <b>nRoots</b>, <i>IN: Number of BDD roots</i>
572  DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
573  char ** <b>inputNames</b>, <i>IN: Array of variable names</i>
574  char ** <b>outputNames</b>, <i>IN: Array of root names</i>
575  char * <b>modelName</b>, <i>IN: Model Name</i>
576  char * <b>fileName</b>, <i>IN: File name</i>
577  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
578)
579</pre>
580<dd> Dumps the argument BDD to file.
581    Dumping is done through Dddmp_cuddBddArrayStorePrefix.
582    A dummy array of 1 BDD root is used for this purpose.
583<p>
584
585<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
586</code>
587
588<dt><pre>
589<A NAME="Dddmp_cuddBddStoreSmv"></A>
590int <I></I>
591<B>Dddmp_cuddBddStoreSmv</B>(
592  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
593  int  <b>nRoots</b>, <i>IN: Number of BDD roots</i>
594  DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
595  char ** <b>inputNames</b>, <i>IN: Array of variable names</i>
596  char ** <b>outputNames</b>, <i>IN: Array of root names</i>
597  char * <b>modelName</b>, <i>IN: Model Name</i>
598  char * <b>fileName</b>, <i>IN: File name</i>
599  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
600)
601</pre>
602<dd> Dumps the argument BDD to file.
603    Dumping is done through Dddmp_cuddBddArrayStorePrefix.
604    A dummy array of 1 BDD root is used for this purpose.
605<p>
606
607<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
608</code>
609
610<dt><pre>
611<A NAME="Dddmp_cuddBddStore"></A>
612int <I></I>
613<B>Dddmp_cuddBddStore</B>(
614  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
615  char * <b>ddname</b>, <i>IN: DD name (or NULL)</i>
616  DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
617  char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
618  int * <b>auxids</b>, <i>IN: array of converted var ids</i>
619  int  <b>mode</b>, <i>IN: storing mode selector</i>
620  Dddmp_VarInfoType  <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
621  char * <b>fname</b>, <i>IN: File name</i>
622  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
623)
624</pre>
625<dd> Dumps the argument BDD to file. Dumping is done through
626    Dddmp_cuddBddArrayStore. A dummy array of 1 BDD root is
627    used for this purpose.
628<p>
629
630<dd> <b>Side Effects</b> Nodes are temporarily removed from unique hash. They are
631    re-linked after the store operation in a modified order.
632<p>
633
634<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
635<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
636</code>
637
638<dt><pre>
639<A NAME="Dddmp_cuddHeaderLoadCnf"></A>
640int <I></I>
641<B>Dddmp_cuddHeaderLoadCnf</B>(
642  int * <b>nVars</b>, <i>OUT: number of DD variables</i>
643  int * <b>nsuppvars</b>, <i>OUT: number of support variables</i>
644  char *** <b>suppVarNames</b>, <i>OUT: array of support variable names</i>
645  char *** <b>orderedVarNames</b>, <i>OUT: array of variable names</i>
646  int ** <b>varIds</b>, <i>OUT: array of variable ids</i>
647  int ** <b>varComposeIds</b>, <i>OUT: array of permids ids</i>
648  int ** <b>varAuxIds</b>, <i>OUT: array of variable aux ids</i>
649  int * <b>nRoots</b>, <i>OUT: number of root in the file</i>
650  char * <b>file</b>, <i>IN: file name</i>
651  FILE * <b>fp</b> <i>IN: file pointer</i>
652)
653</pre>
654<dd> Reads the header of a dump file representing the argument BDDs.
655    Returns main information regarding DD type stored in the file,
656    the variable ordering used, the number of variables, etc.
657    It reads only the header of the file NOT the BDD/ADD section.
658<p>
659
660<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
661</code>
662
663<dt><pre>
664<A NAME="Dddmp_cuddHeaderLoad"></A>
665int <I></I>
666<B>Dddmp_cuddHeaderLoad</B>(
667  Dddmp_DecompType * <b>ddType</b>, <i>OUT: selects the proper decomp type</i>
668  int * <b>nVars</b>, <i>OUT: number of DD variables</i>
669  int * <b>nsuppvars</b>, <i>OUT: number of support variables</i>
670  char *** <b>suppVarNames</b>, <i>OUT: array of support variable names</i>
671  char *** <b>orderedVarNames</b>, <i>OUT: array of variable names</i>
672  int ** <b>varIds</b>, <i>OUT: array of variable ids</i>
673  int ** <b>varComposeIds</b>, <i>OUT: array of permids ids</i>
674  int ** <b>varAuxIds</b>, <i>OUT: array of variable aux ids</i>
675  int * <b>nRoots</b>, <i>OUT: number of root in the file</i>
676  char * <b>file</b>, <i>IN: file name</i>
677  FILE * <b>fp</b> <i>IN: file pointer</i>
678)
679</pre>
680<dd> Reads the header of a dump file representing the argument BDDs.
681    Returns main information regarding DD type stored in the file,
682    the variable ordering used, the number of variables, etc.
683    It reads only the header of the file NOT the BDD/ADD section.
684<p>
685
686<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
687</code>
688
689
690</DL>
691<HR>
692Last updated on 1040218 17h14
693</BODY></HTML>
Note: See TracBrowser for help on using the repository browser.