source: icGREP/icgrep-devel/cudd-2.5.1/dddmp/doc/dddmpAllDet.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: 124.9 KB
Line 
1<html>
2<head><title>The dddmp package: all functions </title></head>
3<body>
4
5A set of internal low-level routines of the dddmp package
6    doing:
7    <ul>
8      <li> read and write of node codes in binary mode,
9      <li> read and write of integers in binary mode,
10      <li> marking/unmarking nodes as visited,
11      <li> numbering nodes.
12    </ul>
13<HR>
14<DL>
15<dt><pre>
16<A NAME="DddmpBddReadHeaderCnf"></A>
17static Dddmp_Hdr_t * <I></I>
18<B>DddmpBddReadHeaderCnf</B>(
19  char * <b>file</b>, <i>IN: file name</i>
20  FILE * <b>fp</b> <i>IN: file pointer</i>
21)
22</pre>
23<dd> Reads the header of a dump file. Builds a Dddmp_Hdr_t struct
24    containing all infos in the header, for next manipulations.
25<p>
26
27<dd> <b>Side Effects</b> none
28<p>
29
30<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoadCnf.c"TARGET="ABSTRACT"><CODE>dddmpLoadCnf.c</CODE></A>
31
32<dt><pre>
33<A NAME="DddmpBddReadHeader"></A>
34static Dddmp_Hdr_t * <I></I>
35<B>DddmpBddReadHeader</B>(
36  char * <b>file</b>, <i>IN: file name</i>
37  FILE * <b>fp</b> <i>IN: file pointer</i>
38)
39</pre>
40<dd> Reads the header of a dump file. Builds a Dddmp_Hdr_t struct
41    containing all infos in the header, for next manipulations.
42<p>
43
44<dd> <b>Side Effects</b> none
45<p>
46
47<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoad.c"TARGET="ABSTRACT"><CODE>dddmpLoad.c</CODE></A>
48
49<dt><pre>
50<A NAME="DddmpClearVisitedAdd"></A>
51void <I></I>
52<B>DddmpClearVisitedAdd</B>(
53  DdNode * <b>f</b> <i>IN: BDD node to be marked (as not visited)</i>
54)
55</pre>
56<dd> Marks a node as not visited
57<p>
58
59<dd> <b>Side Effects</b> None
60<p>
61
62<dd> <b>See Also</b> <code><a href="#DddmpVisitedAdd">DddmpVisitedAdd</a>
63()
64<a href="#DddmpSetVisitedAdd">DddmpSetVisitedAdd</a>
65()
66</code>
67
68<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>
69
70<dt><pre>
71<A NAME="DddmpClearVisitedBdd"></A>
72void <I></I>
73<B>DddmpClearVisitedBdd</B>(
74  DdNode * <b>f</b> <i>IN: BDD node to be marked (as not visited)</i>
75)
76</pre>
77<dd> Marks a node as not visited
78<p>
79
80<dd> <b>Side Effects</b> None
81<p>
82
83<dd> <b>See Also</b> <code><a href="#DddmpVisited">DddmpVisited</a>
84()
85<a href="#DddmpSetVisited">DddmpSetVisited</a>
86()
87</code>
88
89<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>
90
91<dt><pre>
92<A NAME="DddmpClearVisitedCnfRecur"></A>
93static int <I></I>
94<B>DddmpClearVisitedCnfRecur</B>(
95  DdNode * <b>f</b> <i>IN: root of the BDD to be marked</i>
96)
97</pre>
98<dd> Mark ALL nodes as not visited (it recurs on the node children)
99<p>
100
101<dd> <b>Side Effects</b> None
102<p>
103
104<dd> <b>See Also</b> <code><a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
105()
106<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
107()
108</code>
109
110<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
111
112<dt><pre>
113<A NAME="DddmpClearVisitedCnfRecur"></A>
114static int <I></I>
115<B>DddmpClearVisitedCnfRecur</B>(
116  DdNode * <b>f</b> <i>IN: root of the BDD to be marked</i>
117)
118</pre>
119<dd> Mark ALL nodes as not visited (it recurs on the node children)
120<p>
121
122<dd> <b>Side Effects</b> None
123<p>
124
125<dd> <b>See Also</b> <code><a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
126()
127<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
128()
129</code>
130
131<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
132
133<dt><pre>
134<A NAME="DddmpClearVisitedCnf"></A>
135static void <I></I>
136<B>DddmpClearVisitedCnf</B>(
137  DdNode * <b>f</b> <i>IN: BDD node to be marked (as not visited)</i>
138)
139</pre>
140<dd> Marks a node as not visited
141<p>
142
143<dd> <b>Side Effects</b> None
144<p>
145
146<dd> <b>See Also</b> <code><a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
147()
148<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
149()
150</code>
151
152<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
153
154<dt><pre>
155<A NAME="DddmpClearVisitedCnf"></A>
156static void <I></I>
157<B>DddmpClearVisitedCnf</B>(
158  DdNode * <b>f</b> <i>IN: BDD node to be marked (as not visited)</i>
159)
160</pre>
161<dd> Marks a node as not visited
162<p>
163
164<dd> <b>Side Effects</b> None
165<p>
166
167<dd> <b>See Also</b> <code><a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
168()
169<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
170()
171</code>
172
173<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
174
175<dt><pre>
176<A NAME="DddmpClearVisited"></A>
177void <I></I>
178<B>DddmpClearVisited</B>(
179  DdNode * <b>f</b> <i>IN: BDD node to be marked (as not visited)</i>
180)
181</pre>
182<dd> Marks a node as not visited
183<p>
184
185<dd> <b>Side Effects</b> None
186<p>
187
188<dd> <b>See Also</b> <code><a href="#DddmpVisited">DddmpVisited</a>
189()
190<a href="#DddmpSetVisited">DddmpSetVisited</a>
191()
192</code>
193
194<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>
195
196<dt><pre>
197<A NAME="DddmpCnfClauses2Bdd"></A>
198static int <I></I>
199<B>DddmpCnfClauses2Bdd</B>(
200  Dddmp_Hdr_t * <b>Hdr</b>, <i>IN: file header</i>
201  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
202  int ** <b>cnfTable</b>, <i>IN: CNF table for clauses</i>
203  int  <b>mode</b>, <i>IN: computation mode</i>
204  DdNode *** <b>rootsPtrPtr</b> <i>OUT: array of returned BDD roots (by reference)</i>
205)
206</pre>
207<dd> Transforms CNF clauses into BDDs. Clauses are stored in an
208   internal structure previously read. The results can be given in
209   different format according to the mode selection:
210     IFF mode == 0 Return the Clauses without Conjunction
211     IFF mode == 1 Return the sets of BDDs without Quantification
212     IFF mode == 2 Return the sets of BDDs AFTER Existential Quantification
213<p>
214
215<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoadCnf.c"TARGET="ABSTRACT"><CODE>dddmpLoadCnf.c</CODE></A>
216
217<dt><pre>
218<A NAME="DddmpCuddBddArrayStoreCnf"></A>
219static int <I></I>
220<B>DddmpCuddBddArrayStoreCnf</B>(
221  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
222  DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
223  int  <b>rootN</b>, <i>IN: # of output BDD roots to be stored</i>
224  Dddmp_DecompCnfStoreType  <b>mode</b>, <i>IN: format selection</i>
225  int  <b>noHeader</b>, <i>IN: do not store header iff 1</i>
226  char ** <b>varNames</b>, <i>IN: array of variable names (or NULL)</i>
227  int * <b>bddIds</b>, <i>IN: array of BDD node Ids (or NULL)</i>
228  int * <b>bddAuxIds</b>, <i>IN: array of BDD Aux Ids (or NULL)</i>
229  int * <b>cnfIds</b>, <i>IN: array of CNF ids (or NULL)</i>
230  int  <b>idInitial</b>, <i>IN: starting id for cutting variables</i>
231  int  <b>edgeInTh</b>, <i>IN: Max # Incoming Edges</i>
232  int  <b>pathLengthTh</b>, <i>IN: Max Path Length</i>
233  char * <b>fname</b>, <i>IN: file name</i>
234  FILE * <b>fp</b>, <i>IN: pointer to the store file</i>
235  int * <b>clauseNPtr</b>, <i>OUT: number of clause stored</i>
236  int * <b>varNewNPtr</b> <i>OUT: number of new variable created</i>
237)
238</pre>
239<dd> Dumps the argument array of BDDs/ADDs to file in CNF format.
240    The following arrays: varNames, bddIds, bddAuxIds, and cnfIds
241    fix the correspondence among variable names, BDD ids, BDD
242    auxiliary ids and the ids used to store the CNF problem.
243    All these arrays are automatically created iff NULL.
244    Auxiliary variable, iff necessary, are created starting from value
245    idInitial.
246    Iff idInitial is <= 0 its value is selected as the number of internal
247    CUDD variable + 2.
248    Auxiliary variables, i.e., cut points are inserted following these
249    criterias:
250    * edgeInTh
251      indicates the maximum number of incoming edges up to which
252      no cut point (auxiliary variable) is inserted.
253      If edgeInTh:
254      * is equal to -1 no cut point due to incoming edges are inserted
255        (MaxtermByMaxterm method.)
256        * is equal to 0 a cut point is inserted for each node with a single
257        incoming edge, i.e., each node, (NodeByNode method).
258        * is equal to n a cut point is inserted for each node with (n+1)
259        incoming edges.
260    * pathLengthTh
261      indicates the maximum length path up to which no cut points
262      (auxiliary variable) is inserted.
263      If the path length between two nodes exceeds this value, a cut point
264      is inserted.
265      If pathLengthTh:
266      * is equal to -1 no cut point due path length are inserted
267        (MaxtermByMaxterm method.)
268        * is equal to 0 a cut point is inserted for each node (NodeByNode
269        method).
270        * is equal to n a cut point is inserted on path whose length is
271        equal to (n+1).
272      Notice that the maximum number of literals in a clause is equal
273      to (pathLengthTh + 2), i.e., for each path we have to keep into
274      account a CNF variable for each node plus 2 added variables for
275      the bottom and top-path cut points.
276<p>
277
278<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash table.
279    They are re-linked after the store operation in a modified
280    order.
281<p>
282
283<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
284</code>
285
286<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>
287
288<dt><pre>
289<A NAME="DddmpCuddBddArrayStore"></A>
290int <I></I>
291<B>DddmpCuddBddArrayStore</B>(
292  Dddmp_DecompType  <b>ddType</b>, <i>IN: Selects the decomp type BDD</i>
293  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
294  char * <b>ddname</b>, <i>IN: DD name (or NULL)</i>
295  int  <b>nRoots</b>, <i>IN: number of output BDD roots to be stored</i>
296  DdNode ** <b>f</b>, <i>IN: array of DD roots to be stored</i>
297  char ** <b>rootnames</b>, <i>IN: array of root names (or NULL)</i>
298  char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
299  int * <b>auxids</b>, <i>IN: array of converted var IDs</i>
300  int  <b>mode</b>, <i>IN: storing mode selector</i>
301  Dddmp_VarInfoType  <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
302  char * <b>fname</b>, <i>IN: File name</i>
303  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
304)
305</pre>
306<dd> Dumps the argument array of BDDs to file.
307    Internal function doing inner steps of store for BDDs.
308<p>
309
310<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash
311    table. They are re-linked after the store operation in a
312    modified order.
313<p>
314
315<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
316<a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
317<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
318</code>
319
320<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreBdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreBdd.c</CODE></A>
321
322<dt><pre>
323<A NAME="DddmpCuddDdArrayLoadCnf"></A>
324static int <I></I>
325<B>DddmpCuddDdArrayLoadCnf</B>(
326  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
327  Dddmp_RootMatchType  <b>rootmatchmode</b>, <i>IN: storing mode selector</i>
328  char ** <b>rootmatchnames</b>, <i>IN: sorted names for loaded roots</i>
329  Dddmp_VarMatchType  <b>varmatchmode</b>, <i>IN: storing mode selector</i>
330  char ** <b>varmatchnames</b>, <i>IN: array of variable names, by ids</i>
331  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by ids</i>
332  int * <b>varcomposeids</b>, <i>IN: array of new ids, by ids</i>
333  int  <b>mode</b>, <i>IN: computation mode</i>
334  char * <b>file</b>, <i>IN: file name</i>
335  FILE * <b>fp</b>, <i>IN: file pointer</i>
336  DdNode *** <b>rootsPtrPtr</b>, <i>OUT: array of BDD roots</i>
337  int * <b>nRoots</b> <i>OUT: number of BDDs returned</i>
338)
339</pre>
340<dd> Reads a dump file representing the argument BDDs in CNF
341    format.
342      IFF mode == 0 Return the Clauses without Conjunction
343      IFF mode == 1 Return the sets of BDDs without Quantification
344      IFF mode == 2 Return the sets of BDDs AFTER Existential Quantification
345<p>
346
347<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
348<p>
349
350<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
351</code>
352
353<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoadCnf.c"TARGET="ABSTRACT"><CODE>dddmpLoadCnf.c</CODE></A>
354
355<dt><pre>
356<A NAME="DddmpCuddDdArrayLoad"></A>
357static int <I></I>
358<B>DddmpCuddDdArrayLoad</B>(
359  Dddmp_DecompType  <b>ddType</b>, <i>IN: Selects decomp type</i>
360  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
361  Dddmp_RootMatchType  <b>rootMatchMode</b>, <i>IN: storing mode selector</i>
362  char ** <b>rootmatchnames</b>, <i>IN: sorted names for loaded roots</i>
363  Dddmp_VarMatchType  <b>varMatchMode</b>, <i>IN: storing mode selector</i>
364  char ** <b>varmatchnames</b>, <i>IN: array of variable names, by ids</i>
365  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by ids</i>
366  int * <b>varcomposeids</b>, <i>IN: array of new ids, by ids</i>
367  int  <b>mode</b>, <i>IN: requested input file format</i>
368  char * <b>file</b>, <i>IN: file name</i>
369  FILE * <b>fp</b>, <i>IN: file pointer</i>
370  DdNode *** <b>pproots</b> <i>OUT: array BDD roots (by reference)</i>
371)
372</pre>
373<dd> Reads a dump file representing the argument BDDs. The header is
374    common to both text and binary mode. The node list is either
375    in text or binary format. A dynamic vector of DD pointers
376    is allocated to support conversion from DD indexes to pointers.
377    Several criteria are supported for variable match between file
378    and dd manager. Several changes/permutations/compositions are allowed
379    for variables while loading DDs. Variable of the dd manager are allowed
380    to match with variables on file on ids, permids, varnames,
381    varauxids; also direct composition between ids and
382    composeids is supported. More in detail:
383    <ol>
384    <li> varMatchMode=DDDMP_VAR_MATCHIDS <p>
385    allows the loading of a DD keeping variable IDs unchanged
386    (regardless of the variable ordering of the reading manager); this
387    is useful, for example, when swapping DDs to file and restoring them
388    later from file, after possible variable reordering activations.
389   
390    <li> varMatchMode=DDDMP_VAR_MATCHPERMIDS <p>
391    is used to allow variable match according to the position in the ordering.
392   
393    <li> varMatchMode=DDDMP_VAR_MATCHNAMES <p>
394    requires a non NULL varmatchnames parameter; this is a vector of
395    strings in one-to-one correspondence with variable IDs of the
396    reading manager. Variables in the DD file read are matched with
397    manager variables according to their name (a non NULL varnames
398    parameter was required while storing the DD file).
399   
400    <li> varMatchMode=DDDMP_VAR_MATCHIDS <p>
401    has a meaning similar to DDDMP_VAR_MATCHNAMES, but integer auxiliary
402    IDs are used instead of strings; the additional non NULL
403    varmatchauxids parameter is needed.
404   
405    <li> varMatchMode=DDDMP_VAR_COMPOSEIDS <p>
406    uses the additional varcomposeids parameter is used as array of
407    variable ids to be composed with ids stored in file.
408    </ol>
409   
410    In the present implementation, the array varnames (3), varauxids (4)
411    and composeids (5) need to have one entry for each variable in the
412    DD manager (NULL pointers are allowed for unused variables
413    in varnames). Hence variables need to be already present in the
414    manager. All arrays are sorted according to IDs.
415<p>
416
417<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
418<p>
419
420<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
421</code>
422
423<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoad.c"TARGET="ABSTRACT"><CODE>dddmpLoad.c</CODE></A>
424
425<dt><pre>
426<A NAME="DddmpCuddDdArrayStoreBdd"></A>
427int <I></I>
428<B>DddmpCuddDdArrayStoreBdd</B>(
429  Dddmp_DecompType  <b>ddType</b>, <i>IN: Selects the decomp type: BDD or ADD</i>
430  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
431  char * <b>ddname</b>, <i>IN: DD name (or NULL)</i>
432  int  <b>nRoots</b>, <i>IN: number of output BDD roots to be stored</i>
433  DdNode ** <b>f</b>, <i>IN: array of DD roots to be stored</i>
434  char ** <b>rootnames</b>, <i>IN: array of root names (or NULL)</i>
435  char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
436  int * <b>auxids</b>, <i>IN: array of converted var IDs</i>
437  int  <b>mode</b>, <i>IN: storing mode selector</i>
438  Dddmp_VarInfoType  <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
439  char * <b>fname</b>, <i>IN: File name</i>
440  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
441)
442</pre>
443<dd> Dumps the argument array of BDDs/ADDs to file. Internal
444    function doing inner steps of store for BDDs and ADDs.
445    ADD store is presently supported only with the text format.
446<p>
447
448<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash
449    table. They are re-linked after the store operation in a
450    modified order.
451<p>
452
453<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
454<a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
455<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
456</code>
457
458<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreAdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreAdd.c</CODE></A>
459
460<dt><pre>
461<A NAME="DddmpCuddDdArrayStoreBlifBody"></A>
462static int <I></I>
463<B>DddmpCuddDdArrayStoreBlifBody</B>(
464  DdManager * <b>ddMgr</b>, <i>IN: Manager</i>
465  int  <b>n</b>, <i>IN: Number of output nodes to be dumped</i>
466  DdNode ** <b>f</b>, <i>IN: Array of output nodes to be dumped</i>
467  char ** <b>inputNames</b>, <i>IN: Array of input names (or NULL)</i>
468  char ** <b>outputNames</b>, <i>IN: Array of output names (or NULL)</i>
469  FILE * <b>fp</b> <i>IN: Pointer to the dump file</i>
470)
471</pre>
472<dd> Writes a blif body representing the argument BDDs as a
473    network of multiplexers. One multiplexer is written for each BDD
474    node. It returns 1 in case of success; 0 otherwise (e.g.,
475    out-of-memory, file system full, or an ADD with constants different
476    from 0 and 1).
477    DddmpCuddDdArrayStoreBlif does not close the file: This is the
478    caller responsibility.
479    DddmpCuddDdArrayStoreBlif uses a minimal unique subset of
480    the hexadecimal address of a node as name for it.  If the argument
481    inputNames is non-null, it is assumed to hold the pointers to the names
482    of the inputs. Similarly for outputNames. This function prints out only
483    .names part.
484<p>
485
486<dd> <b>Side Effects</b> None
487<p>
488
489<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>
490
491<dt><pre>
492<A NAME="DddmpCuddDdArrayStoreBlifStep"></A>
493static int <I></I>
494<B>DddmpCuddDdArrayStoreBlifStep</B>(
495  DdManager * <b>ddMgr</b>, <i></i>
496  DdNode * <b>f</b>, <i></i>
497  FILE * <b>fp</b>, <i></i>
498  st_table * <b>visited</b>, <i></i>
499  char ** <b>names</b> <i></i>
500)
501</pre>
502<dd> Performs the recursive step of DddmpCuddDdArrayStoreBlif.
503    Traverses the BDD f and writes a multiplexer-network description to
504    the file pointed by fp in blif format.
505    f is assumed to be a regular pointer and DddmpCuddDdArrayStoreBlifStep
506    guarantees this assumption in the recursive calls.
507<p>
508
509<dd> <b>Side Effects</b> None
510<p>
511
512<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>
513
514<dt><pre>
515<A NAME="DddmpCuddDdArrayStoreBlif"></A>
516static int <I></I>
517<B>DddmpCuddDdArrayStoreBlif</B>(
518  DdManager * <b>ddMgr</b>, <i>IN: Manager</i>
519  int  <b>n</b>, <i>IN: Number of output nodes to be dumped</i>
520  DdNode ** <b>f</b>, <i>IN: Array of output nodes to be dumped</i>
521  char ** <b>inputNames</b>, <i>IN: Array of input names (or NULL)</i>
522  char ** <b>outputNames</b>, <i>IN: Array of output names (or NULL)</i>
523  char * <b>modelName</b>, <i>IN: Model name (or NULL)</i>
524  FILE * <b>fp</b> <i>IN: Pointer to the dump file</i>
525)
526</pre>
527<dd> Writes a blif file representing the argument BDDs as a
528    network of multiplexers. One multiplexer is written for each BDD
529    node. It returns 1 in case of success; 0 otherwise (e.g.,
530    out-of-memory, file system full, or an ADD with constants different
531    from 0 and 1).
532    DddmpCuddDdArrayStoreBlif does not close the file: This is the
533    caller responsibility.
534    DddmpCuddDdArrayStoreBlif uses a minimal unique subset of
535    the hexadecimal address of a node as name for it.  If the argument
536    inames is non-null, it is assumed to hold the pointers to the names
537    of the inputs. Similarly for outputNames.
538    It prefixes the string "NODE" to each nome to have "regular" names
539    for each elements.
540<p>
541
542<dd> <b>Side Effects</b> None
543<p>
544
545<dd> <b>See Also</b> <code><a href="#DddmpCuddDdArrayStoreBlifBody">DddmpCuddDdArrayStoreBlifBody</a>
546<a href="#Cudd_DumpBlif">Cudd_DumpBlif</a>
547</code>
548
549<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>
550
551<dt><pre>
552<A NAME="DddmpCuddDdArrayStorePrefixBody"></A>
553static int <I></I>
554<B>DddmpCuddDdArrayStorePrefixBody</B>(
555  DdManager * <b>ddMgr</b>, <i>IN: Manager</i>
556  int  <b>n</b>, <i>IN: Number of output nodes to be dumped</i>
557  DdNode ** <b>f</b>, <i>IN: Array of output nodes to be dumped</i>
558  char ** <b>inputNames</b>, <i>IN: Array of input names (or NULL)</i>
559  char ** <b>outputNames</b>, <i>IN: Array of output names (or NULL)</i>
560  FILE * <b>fp</b> <i>IN: Pointer to the dump file</i>
561)
562</pre>
563<dd> One multiplexer is written for each BDD node.
564    It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file
565    system full, or an ADD with constants different from 0 and 1).
566    It does not close the file: This is the caller responsibility.
567    It uses a minimal unique subset of the hexadecimal address of a node as
568    name for it.
569    If the argument inputNames is non-null, it is assumed to hold the
570    pointers to the names of the inputs. Similarly for outputNames.
571    For each BDD node of function f, variable v, then child T, and else
572    child E it stores:
573    f = v * T + v' * E
574    that is
575    (OR f (AND v T) (AND (NOT v) E))
576    If E is a complemented child this results in the following
577    (OR f (AND v T) (AND (NOT v) (NOT E)))
578<p>
579
580<dd> <b>Side Effects</b> None
581<p>
582
583<dd> <b>See Also</b> <code><a href="#DddmpCuddDdArrayStoreBlif">DddmpCuddDdArrayStoreBlif</a>
584</code>
585
586<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>
587
588<dt><pre>
589<A NAME="DddmpCuddDdArrayStorePrefixStep"></A>
590static int <I></I>
591<B>DddmpCuddDdArrayStorePrefixStep</B>(
592  DdManager * <b>ddMgr</b>, <i></i>
593  DdNode * <b>f</b>, <i></i>
594  FILE * <b>fp</b>, <i></i>
595  st_table * <b>visited</b>, <i></i>
596  char ** <b>names</b> <i></i>
597)
598</pre>
599<dd> Performs the recursive step of
600    DddmpCuddDdArrayStorePrefixBody.
601    Traverses the BDD f and writes a multiplexer-network description to the
602    file pointed by fp.
603    For each BDD node of function f, variable v, then child T, and else
604    child E it stores:
605    f = v * T + v' * E
606    that is
607    (OR f (AND v T) (AND (NOT v) E))
608    If E is a complemented child this results in the following
609    (OR f (AND v T) (AND (NOT v) (NOT E)))
610    f is assumed to be a regular pointer and the function guarantees this
611    assumption in the recursive calls.
612<p>
613
614<dd> <b>Side Effects</b> None
615<p>
616
617<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>
618
619<dt><pre>
620<A NAME="DddmpCuddDdArrayStorePrefix"></A>
621static int <I></I>
622<B>DddmpCuddDdArrayStorePrefix</B>(
623  DdManager * <b>ddMgr</b>, <i>IN: Manager</i>
624  int  <b>n</b>, <i>IN: Number of output nodes to be dumped</i>
625  DdNode ** <b>f</b>, <i>IN: Array of output nodes to be dumped</i>
626  char ** <b>inputNames</b>, <i>IN: Array of input names (or NULL)</i>
627  char ** <b>outputNames</b>, <i>IN: Array of output names (or NULL)</i>
628  char * <b>modelName</b>, <i>IN: Model name (or NULL)</i>
629  FILE * <b>fp</b> <i>IN: Pointer to the dump file</i>
630)
631</pre>
632<dd> One multiplexer is written for each BDD node.
633    It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file
634    system full, or an ADD with constants different from 0 and 1).
635    It does not close the file: This is the caller responsibility.
636    It uses a minimal unique subset of the hexadecimal address of a node as
637    name for it.
638    If the argument inputNames is non-null, it is assumed to hold the
639    pointers to the names of the inputs. Similarly for outputNames.
640    For each BDD node of function f, variable v, then child T, and else
641    child E it stores:
642    f = v * T + v' * E
643    that is
644    (OR f (AND v T) (AND (NOT v) E))
645    If E is a complemented child this results in the following
646    (OR f (AND v T) (AND (NOT v) (NOT E)))
647    Comments (COMMENT) are added at the beginning of the description to
648    describe inputs and outputs of the design.
649    A buffer (BUF) is add on the output to cope with complemented functions.
650<p>
651
652<dd> <b>Side Effects</b> None
653<p>
654
655<dd> <b>See Also</b> <code><a href="#DddmpCuddDdArrayStoreBlif">DddmpCuddDdArrayStoreBlif</a>
656</code>
657
658<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>
659
660<dt><pre>
661<A NAME="DddmpCuddDdArrayStoreSmvBody"></A>
662static int <I></I>
663<B>DddmpCuddDdArrayStoreSmvBody</B>(
664  DdManager * <b>ddMgr</b>, <i>IN: Manager</i>
665  int  <b>n</b>, <i>IN: Number of output nodes to be dumped</i>
666  DdNode ** <b>f</b>, <i>IN: Array of output nodes to be dumped</i>
667  char ** <b>inputNames</b>, <i>IN: Array of input names (or NULL)</i>
668  char ** <b>outputNames</b>, <i>IN: Array of output names (or NULL)</i>
669  FILE * <b>fp</b> <i>IN: Pointer to the dump file</i>
670)
671</pre>
672<dd> One multiplexer is written for each BDD node.
673    It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file
674    system full, or an ADD with constants different from 0 and 1).
675    It does not close the file: This is the caller responsibility.
676    It uses a minimal unique subset of the hexadecimal address of a node as
677    name for it.
678    If the argument inputNames is non-null, it is assumed to hold the
679    pointers to the names of the inputs. Similarly for outputNames.
680    For each BDD node of function f, variable v, then child T, and else
681    child E it stores:
682    f = v * T + v' * E
683    that is
684    (OR f (AND v T) (AND (NOT v) E))
685    If E is a complemented child this results in the following
686    (OR f (AND v T) (AND (NOT v) (NOT E)))
687<p>
688
689<dd> <b>Side Effects</b> None
690<p>
691
692<dd> <b>See Also</b> <code><a href="#DddmpCuddDdArrayStoreBlif">DddmpCuddDdArrayStoreBlif</a>
693</code>
694
695<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>
696
697<dt><pre>
698<A NAME="DddmpCuddDdArrayStoreSmvStep"></A>
699static int <I></I>
700<B>DddmpCuddDdArrayStoreSmvStep</B>(
701  DdManager * <b>ddMgr</b>, <i></i>
702  DdNode * <b>f</b>, <i></i>
703  FILE * <b>fp</b>, <i></i>
704  st_table * <b>visited</b>, <i></i>
705  char ** <b>names</b> <i></i>
706)
707</pre>
708<dd> Performs the recursive step of
709    DddmpCuddDdArrayStoreSmvBody.
710    Traverses the BDD f and writes a multiplexer-network description to the
711    file pointed by fp.
712    For each BDD node of function f, variable v, then child T, and else
713    child E it stores:
714    f = v * T + v' * E
715    that is
716    (OR f (AND v T) (AND (NOT v) E))
717    If E is a complemented child this results in the following
718    (OR f (AND v T) (AND (NOT v) (NOT E)))
719    f is assumed to be a regular pointer and the function guarantees this
720    assumption in the recursive calls.
721<p>
722
723<dd> <b>Side Effects</b> None
724<p>
725
726<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>
727
728<dt><pre>
729<A NAME="DddmpCuddDdArrayStoreSmv"></A>
730static int <I></I>
731<B>DddmpCuddDdArrayStoreSmv</B>(
732  DdManager * <b>ddMgr</b>, <i>IN: Manager</i>
733  int  <b>n</b>, <i>IN: Number of output nodes to be dumped</i>
734  DdNode ** <b>f</b>, <i>IN: Array of output nodes to be dumped</i>
735  char ** <b>inputNames</b>, <i>IN: Array of input names (or NULL)</i>
736  char ** <b>outputNames</b>, <i>IN: Array of output names (or NULL)</i>
737  char * <b>modelName</b>, <i>IN: Model name (or NULL)</i>
738  FILE * <b>fp</b> <i>IN: Pointer to the dump file</i>
739)
740</pre>
741<dd> One multiplexer is written for each BDD node.
742    It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file
743    system full, or an ADD with constants different from 0 and 1).
744    It does not close the file: This is the caller responsibility.
745    It uses a minimal unique subset of the hexadecimal address of a node as
746    name for it.
747    If the argument inputNames is non-null, it is assumed to hold the
748    pointers to the names of the inputs. Similarly for outputNames.
749    For each BDD node of function f, variable v, then child T, and else
750    child E it stores:
751    f = v * T + v' * E
752    that is
753    (OR f (AND v T) (AND (NOT v) E))
754    If E is a complemented child this results in the following
755    (OR f (AND v T) (AND (NOT v) (NOT E)))
756    Comments (COMMENT) are added at the beginning of the description to
757    describe inputs and outputs of the design.
758    A buffer (BUF) is add on the output to cope with complemented functions.
759<p>
760
761<dd> <b>Side Effects</b> None
762<p>
763
764<dd> <b>See Also</b> <code><a href="#DddmpCuddDdArrayStoreBlif">DddmpCuddDdArrayStoreBlif</a>
765</code>
766
767<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>
768
769<dt><pre>
770<A NAME="DddmpDdNodesCheckIncomingAndScanPath"></A>
771static void <I></I>
772<B>DddmpDdNodesCheckIncomingAndScanPath</B>(
773  DdNode * <b>f</b>, <i>IN: BDD node to be numbered</i>
774  int  <b>pathLengthCurrent</b>, <i>IN: Current Path Length</i>
775  int  <b>edgeInTh</b>, <i>IN: Max # In-Edges, after a Insert Cut Point</i>
776  int  <b>pathLengthTh</b> <i>IN: Max Path Length (after, Insert a Cut Point)</i>
777)
778</pre>
779<dd> Number nodes recursively in post-order.
780    The "visited" flag is used with the right polarity.
781    The node is assigned to a new CNF variable only if it is a "shared"
782    node (i.e. the number of its incoming edges is greater than 1).
783<p>
784
785<dd> <b>Side Effects</b> "visited" flags are set.
786<p>
787
788<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
789
790<dt><pre>
791<A NAME="DddmpDdNodesCheckIncomingAndScanPath"></A>
792static void <I></I>
793<B>DddmpDdNodesCheckIncomingAndScanPath</B>(
794  DdNode * <b>f</b>, <i>IN: BDD node to be numbered</i>
795  int  <b>pathLengthCurrent</b>, <i>IN: Current Path Length</i>
796  int  <b>edgeInTh</b>, <i>IN: Max # In-Edges, after a Insert Cut Point</i>
797  int  <b>pathLengthTh</b> <i>IN: Max Path Length (after, Insert a Cut Point)</i>
798)
799</pre>
800<dd> Number nodes recursively in post-order.
801    The "visited" flag is used with the right polarity.
802    The node is assigned to a new CNF variable only if it is a "shared"
803    node (i.e. the number of its incoming edges is greater than 1).
804<p>
805
806<dd> <b>Side Effects</b> "visited" flags are set.
807<p>
808
809<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
810
811<dt><pre>
812<A NAME="DddmpDdNodesCountEdgesAndNumber"></A>
813int <I></I>
814<B>DddmpDdNodesCountEdgesAndNumber</B>(
815  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
816  DdNode ** <b>f</b>, <i>IN: Array of BDDs</i>
817  int  <b>rootN</b>, <i>IN: Number of BDD roots in the array of BDDs</i>
818  int  <b>edgeInTh</b>, <i>IN: Max # In-Edges, after a Insert Cut Point</i>
819  int  <b>pathLengthTh</b>, <i>IN: Max Path Length (after, Insert a Cut Point)</i>
820  int * <b>cnfIds</b>, <i>OUT: CNF identifiers for variables</i>
821  int  <b>id</b> <i>OUT: Number of Temporary Variables Introduced</i>
822)
823</pre>
824<dd> Removes nodes from unique table and numbers each node according
825    to the number of its incoming BDD edges.
826<p>
827
828<dd> <b>Side Effects</b> Nodes are temporarily removed from unique table
829<p>
830
831<dd> <b>See Also</b> <code><a href="#RemoveFromUniqueRecurCnf()">RemoveFromUniqueRecurCnf()</a>
832</code>
833
834<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
835
836<dt><pre>
837<A NAME="DddmpDdNodesCountEdgesAndNumber"></A>
838int <I></I>
839<B>DddmpDdNodesCountEdgesAndNumber</B>(
840  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
841  DdNode ** <b>f</b>, <i>IN: Array of BDDs</i>
842  int  <b>rootN</b>, <i>IN: Number of BDD roots in the array of BDDs</i>
843  int  <b>edgeInTh</b>, <i>IN: Max # In-Edges, after a Insert Cut Point</i>
844  int  <b>pathLengthTh</b>, <i>IN: Max Path Length (after, Insert a Cut Point)</i>
845  int * <b>cnfIds</b>, <i>OUT: CNF identifiers for variables</i>
846  int  <b>id</b> <i>OUT: Number of Temporary Variables Introduced</i>
847)
848</pre>
849<dd> Removes nodes from unique table and numbers each node according
850    to the number of its incoming BDD edges.
851<p>
852
853<dd> <b>Side Effects</b> Nodes are temporarily removed from unique table
854<p>
855
856<dd> <b>See Also</b> <code><a href="#RemoveFromUniqueRecurCnf()">RemoveFromUniqueRecurCnf()</a>
857</code>
858
859<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
860
861<dt><pre>
862<A NAME="DddmpDdNodesCountEdgesRecur"></A>
863static int <I></I>
864<B>DddmpDdNodesCountEdgesRecur</B>(
865  DdNode * <b>f</b> <i>IN: root of the BDD</i>
866)
867</pre>
868<dd> Counts (recursively) the number of incoming edges for each
869    node of a BDD. This number is stored in the index field.
870<p>
871
872<dd> <b>Side Effects</b> "visited" flags remain untouched.
873<p>
874
875<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
876
877<dt><pre>
878<A NAME="DddmpDdNodesCountEdgesRecur"></A>
879static int <I></I>
880<B>DddmpDdNodesCountEdgesRecur</B>(
881  DdNode * <b>f</b> <i>IN: root of the BDD</i>
882)
883</pre>
884<dd> Counts (recursively) the number of incoming edges for each
885    node of a BDD. This number is stored in the index field.
886<p>
887
888<dd> <b>Side Effects</b> "visited" flags remain untouched.
889<p>
890
891<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
892
893<dt><pre>
894<A NAME="DddmpDdNodesNumberEdgesRecur"></A>
895static int <I></I>
896<B>DddmpDdNodesNumberEdgesRecur</B>(
897  DdNode * <b>f</b>, <i>IN: BDD node to be numbered</i>
898  int * <b>cnfIds</b>, <i>IN: possible source for numbering</i>
899  int  <b>id</b> <i>IN/OUT: possible source for numbering</i>
900)
901</pre>
902<dd> Number nodes recursively in post-order.
903    The "visited" flag is used with the inverse polarity.
904    Numbering follows the subsequent strategy:
905    * if the index = 0 it remains so
906    * if the index >= 1 it gets enumerated.
907      This implies that the node is assigned to a new CNF variable only if
908      it is not a terminal node otherwise it is assigned the index of
909      the BDD variable.
910<p>
911
912<dd> <b>Side Effects</b> "visited" flags are reset.
913<p>
914
915<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
916
917<dt><pre>
918<A NAME="DddmpDdNodesNumberEdgesRecur"></A>
919static int <I></I>
920<B>DddmpDdNodesNumberEdgesRecur</B>(
921  DdNode * <b>f</b>, <i>IN: BDD node to be numbered</i>
922  int * <b>cnfIds</b>, <i>IN: possible source for numbering</i>
923  int  <b>id</b> <i>IN/OUT: possible source for numbering</i>
924)
925</pre>
926<dd> Number nodes recursively in post-order.
927    The "visited" flag is used with the inverse polarity.
928    Numbering follows the subsequent strategy:
929    * if the index = 0 it remains so
930    * if the index >= 1 it gets enumerated.
931      This implies that the node is assigned to a new CNF variable only if
932      it is not a terminal node otherwise it is assigned the index of
933      the BDD variable.
934<p>
935
936<dd> <b>Side Effects</b> "visited" flags are reset.
937<p>
938
939<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
940
941<dt><pre>
942<A NAME="DddmpDdNodesResetCountRecur"></A>
943static int <I></I>
944<B>DddmpDdNodesResetCountRecur</B>(
945  DdNode * <b>f</b> <i>IN: root of the BDD whose counters are reset</i>
946)
947</pre>
948<dd> Resets counter and visited flag for ALL nodes of a BDD (it
949    recurs on the node children). The index field of the node is
950    used as counter.
951<p>
952
953<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
954
955<dt><pre>
956<A NAME="DddmpDdNodesResetCountRecur"></A>
957static int <I></I>
958<B>DddmpDdNodesResetCountRecur</B>(
959  DdNode * <b>f</b> <i>IN: root of the BDD whose counters are reset</i>
960)
961</pre>
962<dd> Resets counter and visited flag for ALL nodes of a BDD (it
963    recurs on the node children). The index field of the node is
964    used as counter.
965<p>
966
967<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
968
969<dt><pre>
970<A NAME="DddmpFreeHeaderCnf"></A>
971static void <I></I>
972<B>DddmpFreeHeaderCnf</B>(
973  Dddmp_Hdr_t * <b>Hdr</b> <i>IN: pointer to header</i>
974)
975</pre>
976<dd> Frees the internal header structure by freeing all internal
977    fields first.
978<p>
979
980<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoadCnf.c"TARGET="ABSTRACT"><CODE>dddmpLoadCnf.c</CODE></A>
981
982<dt><pre>
983<A NAME="DddmpFreeHeader"></A>
984static void <I></I>
985<B>DddmpFreeHeader</B>(
986  Dddmp_Hdr_t * <b>Hdr</b> <i>IN: pointer to header</i>
987)
988</pre>
989<dd> Frees the internal header structureby freeing all internal
990    fields first.
991<p>
992
993<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoad.c"TARGET="ABSTRACT"><CODE>dddmpLoad.c</CODE></A>
994
995<dt><pre>
996<A NAME="DddmpIntArrayDup"></A>
997int * <I></I>
998<B>DddmpIntArrayDup</B>(
999  int * <b>array</b>, <i>IN: array of ints to be duplicated</i>
1000  int  <b>n</b> <i>IN: size of the array</i>
1001)
1002</pre>
1003<dd> Allocates memory and copies source array
1004<p>
1005
1006<dd> <b>Side Effects</b> None
1007<p>
1008
1009<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>
1010
1011<dt><pre>
1012<A NAME="DddmpIntArrayRead"></A>
1013int * <I></I>
1014<B>DddmpIntArrayRead</B>(
1015  FILE * <b>fp</b>, <i>IN: input file</i>
1016  int  <b>n</b> <i>IN: size of the array</i>
1017)
1018</pre>
1019<dd> Allocates memory and inputs source array
1020<p>
1021
1022<dd> <b>Side Effects</b> None
1023<p>
1024
1025<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>
1026
1027<dt><pre>
1028<A NAME="DddmpIntArrayWrite"></A>
1029int <I></I>
1030<B>DddmpIntArrayWrite</B>(
1031  FILE * <b>fp</b>, <i>IN: output file</i>
1032  int * <b>array</b>, <i>IN: array of ints</i>
1033  int  <b>n</b> <i>IN: size of the array</i>
1034)
1035</pre>
1036<dd> Outputs an array of ints to a specified file
1037<p>
1038
1039<dd> <b>Side Effects</b> None
1040<p>
1041
1042<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>
1043
1044<dt><pre>
1045<A NAME="DddmpNumberAddNodes"></A>
1046int <I></I>
1047<B>DddmpNumberAddNodes</B>(
1048  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
1049  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
1050  int  <b>n</b> <i>IN: number of BDD roots in the array of BDDs</i>
1051)
1052</pre>
1053<dd> Node numbering is required to convert pointers to integers.
1054    Since nodes are removed from unique table, no new nodes should
1055    be generated before re-inserting nodes in the unique table
1056    (DddmpUnnumberDdNodes()).
1057<p>
1058
1059<dd> <b>Side Effects</b> Nodes are temporarily removed from unique table
1060<p>
1061
1062<dd> <b>See Also</b> <code><a href="#RemoveFromUniqueRecurAdd">RemoveFromUniqueRecurAdd</a>
1063()
1064<a href="#NumberNodeRecurAdd">NumberNodeRecurAdd</a>
1065()
1066<a href="#DddmpUnnumberDdNodesAdd">DddmpUnnumberDdNodesAdd</a>
1067()
1068</code>
1069
1070<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>
1071
1072<dt><pre>
1073<A NAME="DddmpNumberBddNodes"></A>
1074int <I></I>
1075<B>DddmpNumberBddNodes</B>(
1076  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
1077  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
1078  int  <b>n</b> <i>IN: number of BDD roots in the array of BDDs</i>
1079)
1080</pre>
1081<dd> Node numbering is required to convert pointers to integers.
1082    Since nodes are removed from unique table, no new nodes should
1083    be generated before re-inserting nodes in the unique table
1084    (DddmpUnnumberBddNodes ()).
1085<p>
1086
1087<dd> <b>Side Effects</b> Nodes are temporarily removed from unique table
1088<p>
1089
1090<dd> <b>See Also</b> <code><a href="#RemoveFromUniqueRecur()">RemoveFromUniqueRecur()</a>
1091<a href="#NumberNodeRecur()">NumberNodeRecur()</a>
1092<a href="#DddmpUnnumberBddNodes">DddmpUnnumberBddNodes</a>
1093()
1094</code>
1095
1096<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>
1097
1098<dt><pre>
1099<A NAME="DddmpNumberDdNodesCnf"></A>
1100int <I></I>
1101<B>DddmpNumberDdNodesCnf</B>(
1102  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
1103  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
1104  int  <b>rootN</b>, <i>IN: number of BDD roots in the array of BDDs</i>
1105  int * <b>cnfIds</b>, <i>OUT: CNF identifiers for variables</i>
1106  int  <b>id</b> <i>OUT: number of Temporary Variables Introduced</i>
1107)
1108</pre>
1109<dd> Node numbering is required to convert pointers to integers.
1110    Since nodes are removed from unique table, no new nodes should
1111    be generated before re-inserting nodes in the unique table
1112    (DddmpUnnumberDdNodesCnf()).
1113<p>
1114
1115<dd> <b>Side Effects</b> Nodes are temporarily removed from unique table
1116<p>
1117
1118<dd> <b>See Also</b> <code><a href="#RemoveFromUniqueRecurCnf()">RemoveFromUniqueRecurCnf()</a>
1119<a href="#NumberNodeRecurCnf()">NumberNodeRecurCnf()</a>
1120<a href="#DddmpUnnumberDdNodesCnf()">DddmpUnnumberDdNodesCnf()</a>
1121</code>
1122
1123<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
1124
1125<dt><pre>
1126<A NAME="DddmpNumberDdNodesCnf"></A>
1127int <I></I>
1128<B>DddmpNumberDdNodesCnf</B>(
1129  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
1130  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
1131  int  <b>rootN</b>, <i>IN: number of BDD roots in the array of BDDs</i>
1132  int * <b>cnfIds</b>, <i>OUT: CNF identifiers for variables</i>
1133  int  <b>id</b> <i>OUT: number of Temporary Variables Introduced</i>
1134)
1135</pre>
1136<dd> Node numbering is required to convert pointers to integers.
1137    Since nodes are removed from unique table, no new nodes should
1138    be generated before re-inserting nodes in the unique table
1139    (DddmpUnnumberDdNodesCnf()).
1140<p>
1141
1142<dd> <b>Side Effects</b> Nodes are temporarily removed from unique table
1143<p>
1144
1145<dd> <b>See Also</b> <code><a href="#RemoveFromUniqueRecurCnf()">RemoveFromUniqueRecurCnf()</a>
1146<a href="#NumberNodeRecurCnf()">NumberNodeRecurCnf()</a>
1147<a href="#DddmpUnnumberDdNodesCnf()">DddmpUnnumberDdNodesCnf()</a>
1148</code>
1149
1150<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
1151
1152<dt><pre>
1153<A NAME="DddmpNumberDdNodes"></A>
1154int <I></I>
1155<B>DddmpNumberDdNodes</B>(
1156  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
1157  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
1158  int  <b>n</b> <i>IN: number of BDD roots in the array of BDDs</i>
1159)
1160</pre>
1161<dd> Node numbering is required to convert pointers to integers.
1162    Since nodes are removed from unique table, no new nodes should
1163    be generated before re-inserting nodes in the unique table
1164    (DddmpUnnumberDdNodes()).
1165<p>
1166
1167<dd> <b>Side Effects</b> Nodes are temporarily removed from unique table
1168<p>
1169
1170<dd> <b>See Also</b> <code><a href="#RemoveFromUniqueRecur()">RemoveFromUniqueRecur()</a>
1171<a href="#NumberNodeRecur()">NumberNodeRecur()</a>
1172<a href="#DddmpUnnumberDdNodes()">DddmpUnnumberDdNodes()</a>
1173</code>
1174
1175<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>
1176
1177<dt><pre>
1178<A NAME="DddmpPrintBddAndNextRecur"></A>
1179static int <I></I>
1180<B>DddmpPrintBddAndNextRecur</B>(
1181  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
1182  DdNode * <b>f</b> <i>IN: root of the BDD to be displayed</i>
1183)
1184</pre>
1185<dd> Prints debug info for a BDD on the screen. It recurs on
1186    node's children.
1187<p>
1188
1189<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
1190
1191<dt><pre>
1192<A NAME="DddmpPrintBddAndNextRecur"></A>
1193static int <I></I>
1194<B>DddmpPrintBddAndNextRecur</B>(
1195  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
1196  DdNode * <b>f</b> <i>IN: root of the BDD to be displayed</i>
1197)
1198</pre>
1199<dd> Prints debug info for a BDD on the screen. It recurs on
1200    node's children.
1201<p>
1202
1203<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
1204
1205<dt><pre>
1206<A NAME="DddmpPrintBddAndNext"></A>
1207int <I></I>
1208<B>DddmpPrintBddAndNext</B>(
1209  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
1210  DdNode ** <b>f</b>, <i>IN: Array of BDDs to be displayed</i>
1211  int  <b>rootN</b> <i>IN: Number of BDD roots in the array of BDDs</i>
1212)
1213</pre>
1214<dd> Prints debug information for an array of BDDs on the screen
1215<p>
1216
1217<dd> <b>Side Effects</b> None
1218<p>
1219
1220<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
1221
1222<dt><pre>
1223<A NAME="DddmpPrintBddAndNext"></A>
1224int <I></I>
1225<B>DddmpPrintBddAndNext</B>(
1226  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
1227  DdNode ** <b>f</b>, <i>IN: Array of BDDs to be displayed</i>
1228  int  <b>rootN</b> <i>IN: Number of BDD roots in the array of BDDs</i>
1229)
1230</pre>
1231<dd> Prints debug information for an array of BDDs on the screen
1232<p>
1233
1234<dd> <b>Side Effects</b> None
1235<p>
1236
1237<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
1238
1239<dt><pre>
1240<A NAME="DddmpReadCnfClauses"></A>
1241static int <I></I>
1242<B>DddmpReadCnfClauses</B>(
1243  Dddmp_Hdr_t * <b>Hdr</b>, <i>IN: file header</i>
1244  int *** <b>cnfTable</b>, <i>OUT: CNF table for clauses</i>
1245  FILE * <b>fp</b> <i>IN: source file</i>
1246)
1247</pre>
1248<dd> Read the CNF clauses from the file in the standard DIMACS
1249    format. Store all the clauses in an internal structure for
1250    future transformation into BDDs.
1251<p>
1252
1253<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoadCnf.c"TARGET="ABSTRACT"><CODE>dddmpLoadCnf.c</CODE></A>
1254
1255<dt><pre>
1256<A NAME="DddmpReadCode"></A>
1257int <I></I>
1258<B>DddmpReadCode</B>(
1259  FILE * <b>fp</b>, <i>IN: file where to read the code</i>
1260  struct binary_dd_code * <b>pcode</b> <i>OUT: the read code</i>
1261)
1262</pre>
1263<dd> Reads a 1 byte node code. See DddmpWriteCode()
1264    for code description.
1265<p>
1266
1267<dd> <b>Side Effects</b> None
1268<p>
1269
1270<dd> <b>See Also</b> <code><a href="#DddmpWriteCode()">DddmpWriteCode()</a>
1271</code>
1272
1273<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpBinary.c"TARGET="ABSTRACT"><CODE>dddmpBinary.c</CODE></A>
1274
1275<dt><pre>
1276<A NAME="DddmpReadInt"></A>
1277int <I></I>
1278<B>DddmpReadInt</B>(
1279  FILE * <b>fp</b>, <i>IN: file where to read the integer</i>
1280  int * <b>pid</b> <i>OUT: the read integer</i>
1281)
1282</pre>
1283<dd> Reads an integer coded on a sequence of bytes. See
1284    DddmpWriteInt() for format.
1285<p>
1286
1287<dd> <b>Side Effects</b> None
1288<p>
1289
1290<dd> <b>See Also</b> <code><a href="#DddmpWriteInt()">DddmpWriteInt()</a>
1291</code>
1292
1293<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpBinary.c"TARGET="ABSTRACT"><CODE>dddmpBinary.c</CODE></A>
1294
1295<dt><pre>
1296<A NAME="DddmpReadNodeIndexAdd"></A>
1297int <I></I>
1298<B>DddmpReadNodeIndexAdd</B>(
1299  DdNode * <b>f</b> <i>IN: BDD node</i>
1300)
1301</pre>
1302<dd> Reads the index of a node. LSB is skipped (used as visited
1303    flag).
1304<p>
1305
1306<dd> <b>Side Effects</b> None
1307<p>
1308
1309<dd> <b>See Also</b> <code><a href="#DddmpWriteNodeIndexAdd">DddmpWriteNodeIndexAdd</a>
1310()
1311<a href="#DddmpSetVisitedAdd">DddmpSetVisitedAdd</a>
1312()
1313<a href="#DddmpVisitedAdd">DddmpVisitedAdd</a>
1314()
1315</code>
1316
1317<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>
1318
1319<dt><pre>
1320<A NAME="DddmpReadNodeIndexBdd"></A>
1321int <I></I>
1322<B>DddmpReadNodeIndexBdd</B>(
1323  DdNode * <b>f</b> <i>IN: BDD node</i>
1324)
1325</pre>
1326<dd> Reads the index of a node. LSB is skipped (used as visited
1327    flag).
1328<p>
1329
1330<dd> <b>Side Effects</b> None
1331<p>
1332
1333<dd> <b>See Also</b> <code><a href="#DddmpWriteNodeIndexBdd">DddmpWriteNodeIndexBdd</a>
1334()
1335<a href="#DddmpSetVisitedBdd">DddmpSetVisitedBdd</a>
1336()
1337<a href="#DddmpVisitedBdd">DddmpVisitedBdd</a>
1338()
1339</code>
1340
1341<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>
1342
1343<dt><pre>
1344<A NAME="DddmpReadNodeIndexCnf"></A>
1345int <I></I>
1346<B>DddmpReadNodeIndexCnf</B>(
1347  DdNode * <b>f</b> <i>IN: BDD node</i>
1348)
1349</pre>
1350<dd> Reads the index of a node. LSB is skipped (used as visited
1351    flag).
1352<p>
1353
1354<dd> <b>Side Effects</b> None
1355<p>
1356
1357<dd> <b>See Also</b> <code><a href="#DddmpWriteNodeIndexCnf()">DddmpWriteNodeIndexCnf()</a>
1358<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
1359()
1360<a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
1361()
1362</code>
1363
1364<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
1365
1366<dt><pre>
1367<A NAME="DddmpReadNodeIndexCnf"></A>
1368static int <I></I>
1369<B>DddmpReadNodeIndexCnf</B>(
1370  DdNode * <b>f</b> <i>IN: BDD node</i>
1371)
1372</pre>
1373<dd> Reads the index of a node. LSB is skipped (used as visited
1374                flag).
1375<p>
1376
1377<dd> <b>Side Effects</b> None
1378<p>
1379
1380<dd> <b>See Also</b> <code><a href="#DddmpWriteNodeIndexCnf()">DddmpWriteNodeIndexCnf()</a>
1381<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
1382()
1383<a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
1384()
1385</code>
1386
1387<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
1388
1389<dt><pre>
1390<A NAME="DddmpReadNodeIndex"></A>
1391int <I></I>
1392<B>DddmpReadNodeIndex</B>(
1393  DdNode * <b>f</b> <i>IN: BDD node</i>
1394)
1395</pre>
1396<dd> Reads the index of a node. LSB is skipped (used as visited
1397    flag).
1398<p>
1399
1400<dd> <b>Side Effects</b> None
1401<p>
1402
1403<dd> <b>See Also</b> <code><a href="#DddmpWriteNodeIndex()">DddmpWriteNodeIndex()</a>
1404<a href="#DddmpSetVisited">DddmpSetVisited</a>
1405()
1406<a href="#DddmpVisited">DddmpVisited</a>
1407()
1408</code>
1409
1410<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>
1411
1412<dt><pre>
1413<A NAME="DddmpSetVisitedAdd"></A>
1414void <I></I>
1415<B>DddmpSetVisitedAdd</B>(
1416  DdNode * <b>f</b> <i>IN: BDD node to be marked (as visited)</i>
1417)
1418</pre>
1419<dd> Marks a node as visited
1420<p>
1421
1422<dd> <b>Side Effects</b> None
1423<p>
1424
1425<dd> <b>See Also</b> <code><a href="#DddmpVisitedAdd">DddmpVisitedAdd</a>
1426()
1427<a href="#DddmpClearVisitedAdd">DddmpClearVisitedAdd</a>
1428()
1429</code>
1430
1431<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>
1432
1433<dt><pre>
1434<A NAME="DddmpSetVisitedBdd"></A>
1435void <I></I>
1436<B>DddmpSetVisitedBdd</B>(
1437  DdNode * <b>f</b> <i>IN: BDD node to be marked (as visited)</i>
1438)
1439</pre>
1440<dd> Marks a node as visited
1441<p>
1442
1443<dd> <b>Side Effects</b> None
1444<p>
1445
1446<dd> <b>See Also</b> <code><a href="#DddmpVisitedBdd">DddmpVisitedBdd</a>
1447()
1448<a href="#DddmpClearVisitedBdd">DddmpClearVisitedBdd</a>
1449()
1450</code>
1451
1452<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>
1453
1454<dt><pre>
1455<A NAME="DddmpSetVisitedCnf"></A>
1456static void <I></I>
1457<B>DddmpSetVisitedCnf</B>(
1458  DdNode * <b>f</b> <i>IN: BDD node to be marked (as visited)</i>
1459)
1460</pre>
1461<dd> Marks a node as visited
1462<p>
1463
1464<dd> <b>Side Effects</b> None
1465<p>
1466
1467<dd> <b>See Also</b> <code><a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
1468()
1469<a href="#DddmpClearVisitedCnf">DddmpClearVisitedCnf</a>
1470()
1471</code>
1472
1473<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
1474
1475<dt><pre>
1476<A NAME="DddmpSetVisitedCnf"></A>
1477void <I></I>
1478<B>DddmpSetVisitedCnf</B>(
1479  DdNode * <b>f</b> <i>IN: BDD node to be marked (as visited)</i>
1480)
1481</pre>
1482<dd> Marks a node as visited
1483<p>
1484
1485<dd> <b>Side Effects</b> None
1486<p>
1487
1488<dd> <b>See Also</b> <code><a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
1489()
1490<a href="#DddmpClearVisitedCnf">DddmpClearVisitedCnf</a>
1491()
1492</code>
1493
1494<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
1495
1496<dt><pre>
1497<A NAME="DddmpSetVisited"></A>
1498void <I></I>
1499<B>DddmpSetVisited</B>(
1500  DdNode * <b>f</b> <i>IN: BDD node to be marked (as visited)</i>
1501)
1502</pre>
1503<dd> Marks a node as visited
1504<p>
1505
1506<dd> <b>Side Effects</b> None
1507<p>
1508
1509<dd> <b>See Also</b> <code><a href="#DddmpVisited">DddmpVisited</a>
1510()
1511<a href="#DddmpClearVisited">DddmpClearVisited</a>
1512()
1513</code>
1514
1515<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>
1516
1517<dt><pre>
1518<A NAME="DddmpStrArrayDup"></A>
1519char ** <I></I>
1520<B>DddmpStrArrayDup</B>(
1521  char ** <b>array</b>, <i>IN: array of strings to be duplicated</i>
1522  int  <b>n</b> <i>IN: size of the array</i>
1523)
1524</pre>
1525<dd> Allocates memory and copies source array
1526<p>
1527
1528<dd> <b>Side Effects</b> None
1529<p>
1530
1531<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>
1532
1533<dt><pre>
1534<A NAME="DddmpStrArrayFree"></A>
1535void <I></I>
1536<B>DddmpStrArrayFree</B>(
1537  char ** <b>array</b>, <i>IN: array of strings</i>
1538  int  <b>n</b> <i>IN: size of the array</i>
1539)
1540</pre>
1541<dd> Frees memory for strings and the array of pointers
1542<p>
1543
1544<dd> <b>Side Effects</b> None
1545<p>
1546
1547<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>
1548
1549<dt><pre>
1550<A NAME="DddmpStrArrayRead"></A>
1551char ** <I></I>
1552<B>DddmpStrArrayRead</B>(
1553  FILE * <b>fp</b>, <i>IN: input file</i>
1554  int  <b>n</b> <i>IN: size of the array</i>
1555)
1556</pre>
1557<dd> Allocates memory and inputs source array
1558<p>
1559
1560<dd> <b>Side Effects</b> None
1561<p>
1562
1563<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>
1564
1565<dt><pre>
1566<A NAME="DddmpStrArrayWrite"></A>
1567int <I></I>
1568<B>DddmpStrArrayWrite</B>(
1569  FILE * <b>fp</b>, <i>IN: output file</i>
1570  char ** <b>array</b>, <i>IN: array of strings</i>
1571  int  <b>n</b> <i>IN: size of the array</i>
1572)
1573</pre>
1574<dd> Outputs an array of strings to a specified file
1575<p>
1576
1577<dd> <b>Side Effects</b> None
1578<p>
1579
1580<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>
1581
1582<dt><pre>
1583<A NAME="DddmpStrDup"></A>
1584char * <I></I>
1585<B>DddmpStrDup</B>(
1586  char * <b>str</b> <i>IN: string to be duplicated</i>
1587)
1588</pre>
1589<dd> Allocates memory and copies source string
1590<p>
1591
1592<dd> <b>Side Effects</b> None
1593<p>
1594
1595<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>
1596
1597<dt><pre>
1598<A NAME="DddmpUnnumberAddNodes"></A>
1599void <I></I>
1600<B>DddmpUnnumberAddNodes</B>(
1601  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
1602  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
1603  int  <b>n</b> <i>IN: number of BDD roots in the array of BDDs</i>
1604)
1605</pre>
1606<dd> Node indexes are no more needed. Nodes are re-linked in the
1607    unique table.
1608<p>
1609
1610<dd> <b>Side Effects</b> None
1611<p>
1612
1613<dd> <b>See Also</b> <code><a href="#DddmpNumberDdNodeAdd">DddmpNumberDdNodeAdd</a>
1614()
1615</code>
1616
1617<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>
1618
1619<dt><pre>
1620<A NAME="DddmpUnnumberBddNodes"></A>
1621void <I></I>
1622<B>DddmpUnnumberBddNodes</B>(
1623  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
1624  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
1625  int  <b>n</b> <i>IN: number of BDD roots in the array of BDDs</i>
1626)
1627</pre>
1628<dd> Node indexes are no more needed. Nodes are re-linked in the
1629    unique table.
1630<p>
1631
1632<dd> <b>Side Effects</b> None
1633<p>
1634
1635<dd> <b>See Also</b> <code><a href="#DddmpNumberBddNode">DddmpNumberBddNode</a>
1636()
1637</code>
1638
1639<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>
1640
1641<dt><pre>
1642<A NAME="DddmpUnnumberDdNodesCnf"></A>
1643void <I></I>
1644<B>DddmpUnnumberDdNodesCnf</B>(
1645  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
1646  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
1647  int  <b>rootN</b> <i>IN: number of BDD roots in the array of BDDs</i>
1648)
1649</pre>
1650<dd> Node indexes are no more needed. Nodes are re-linked in the
1651    unique table.
1652<p>
1653
1654<dd> <b>Side Effects</b> None
1655<p>
1656
1657<dd> <b>See Also</b> <code><a href="#DddmpNumberDdNode()">DddmpNumberDdNode()</a>
1658</code>
1659
1660<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
1661
1662<dt><pre>
1663<A NAME="DddmpUnnumberDdNodesCnf"></A>
1664void <I></I>
1665<B>DddmpUnnumberDdNodesCnf</B>(
1666  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
1667  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
1668  int  <b>rootN</b> <i>IN: number of BDD roots in the array of BDDs</i>
1669)
1670</pre>
1671<dd> Node indexes are no more needed. Nodes are re-linked in the
1672    unique table.
1673<p>
1674
1675<dd> <b>Side Effects</b> None
1676<p>
1677
1678<dd> <b>See Also</b> <code><a href="#DddmpNumberDdNode()">DddmpNumberDdNode()</a>
1679</code>
1680
1681<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
1682
1683<dt><pre>
1684<A NAME="DddmpUnnumberDdNodes"></A>
1685void <I></I>
1686<B>DddmpUnnumberDdNodes</B>(
1687  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
1688  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
1689  int  <b>n</b> <i>IN: number of BDD roots in the array of BDDs</i>
1690)
1691</pre>
1692<dd> Node indexes are no more needed. Nodes are re-linked in the
1693    unique table.
1694<p>
1695
1696<dd> <b>Side Effects</b> None
1697<p>
1698
1699<dd> <b>See Also</b> <code><a href="#DddmpNumberDdNode()">DddmpNumberDdNode()</a>
1700</code>
1701
1702<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>
1703
1704<dt><pre>
1705<A NAME="DddmpVisitedAdd"></A>
1706int <I></I>
1707<B>DddmpVisitedAdd</B>(
1708  DdNode * <b>f</b> <i>IN: BDD node to be tested</i>
1709)
1710</pre>
1711<dd> Returns true if node is visited
1712<p>
1713
1714<dd> <b>Side Effects</b> None
1715<p>
1716
1717<dd> <b>See Also</b> <code><a href="#DddmpSetVisitedAdd">DddmpSetVisitedAdd</a>
1718()
1719<a href="#DddmpClearVisitedAdd">DddmpClearVisitedAdd</a>
1720()
1721</code>
1722
1723<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>
1724
1725<dt><pre>
1726<A NAME="DddmpVisitedBdd"></A>
1727int <I></I>
1728<B>DddmpVisitedBdd</B>(
1729  DdNode * <b>f</b> <i>IN: BDD node to be tested</i>
1730)
1731</pre>
1732<dd> Returns true if node is visited
1733<p>
1734
1735<dd> <b>Side Effects</b> None
1736<p>
1737
1738<dd> <b>See Also</b> <code><a href="#DddmpSetVisitedBdd">DddmpSetVisitedBdd</a>
1739()
1740<a href="#DddmpClearVisitedBdd">DddmpClearVisitedBdd</a>
1741()
1742</code>
1743
1744<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>
1745
1746<dt><pre>
1747<A NAME="DddmpVisitedCnf"></A>
1748int <I></I>
1749<B>DddmpVisitedCnf</B>(
1750  DdNode * <b>f</b> <i>IN: BDD node to be tested</i>
1751)
1752</pre>
1753<dd> Returns true if node is visited
1754<p>
1755
1756<dd> <b>Side Effects</b> None
1757<p>
1758
1759<dd> <b>See Also</b> <code><a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
1760()
1761<a href="#DddmpClearVisitedCnf">DddmpClearVisitedCnf</a>
1762()
1763</code>
1764
1765<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
1766
1767<dt><pre>
1768<A NAME="DddmpVisitedCnf"></A>
1769static int <I></I>
1770<B>DddmpVisitedCnf</B>(
1771  DdNode * <b>f</b> <i>IN: BDD node to be tested</i>
1772)
1773</pre>
1774<dd> Returns true if node is visited
1775<p>
1776
1777<dd> <b>Side Effects</b> None
1778<p>
1779
1780<dd> <b>See Also</b> <code><a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
1781()
1782<a href="#DddmpClearVisitedCnf">DddmpClearVisitedCnf</a>
1783()
1784</code>
1785
1786<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
1787
1788<dt><pre>
1789<A NAME="DddmpVisited"></A>
1790int <I></I>
1791<B>DddmpVisited</B>(
1792  DdNode * <b>f</b> <i>IN: BDD node to be tested</i>
1793)
1794</pre>
1795<dd> Returns true if node is visited
1796<p>
1797
1798<dd> <b>Side Effects</b> None
1799<p>
1800
1801<dd> <b>See Also</b> <code><a href="#DddmpSetVisited">DddmpSetVisited</a>
1802()
1803<a href="#DddmpClearVisited">DddmpClearVisited</a>
1804()
1805</code>
1806
1807<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>
1808
1809<dt><pre>
1810<A NAME="DddmpWriteCode"></A>
1811int <I></I>
1812<B>DddmpWriteCode</B>(
1813  FILE * <b>fp</b>, <i>IN: file where to write the code</i>
1814  struct binary_dd_code  <b>code</b> <i>IN: the code to be written</i>
1815)
1816</pre>
1817<dd> outputs a 1 byte node code using the following format:
1818     <pre>
1819     Unused      : 1 bit;
1820     V           : 2 bits;     (variable code)
1821     T           : 2 bits;     (Then code)
1822     Ecompl      : 1 bit;      (Else complemented)
1823     E           : 2 bits;     (Else code)
1824    </pre>
1825    Ecompl is set with complemented edges.
1826<p>
1827
1828<dd> <b>Side Effects</b> None
1829<p>
1830
1831<dd> <b>See Also</b> <code><a href="#DddmpReadCode()">DddmpReadCode()</a>
1832</code>
1833
1834<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpBinary.c"TARGET="ABSTRACT"><CODE>dddmpBinary.c</CODE></A>
1835
1836<dt><pre>
1837<A NAME="DddmpWriteInt"></A>
1838int <I></I>
1839<B>DddmpWriteInt</B>(
1840  FILE * <b>fp</b>, <i>IN: file where to write the integer</i>
1841  int  <b>id</b> <i>IN: integer to be written</i>
1842)
1843</pre>
1844<dd> Writes an integer as a sequence of bytes (MSByte first).
1845    For each byte 7 bits are used for data and one (LSBit) as link
1846    with a further byte (LSB = 1 means one more byte).
1847<p>
1848
1849<dd> <b>Side Effects</b> None
1850<p>
1851
1852<dd> <b>See Also</b> <code><a href="#DddmpReadInt()">DddmpReadInt()</a>
1853</code>
1854
1855<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpBinary.c"TARGET="ABSTRACT"><CODE>dddmpBinary.c</CODE></A>
1856
1857<dt><pre>
1858<A NAME="DddmpWriteNodeIndexAdd"></A>
1859void <I></I>
1860<B>DddmpWriteNodeIndexAdd</B>(
1861  DdNode * <b>f</b>, <i>IN: BDD node</i>
1862  int  <b>id</b> <i>IN: index to be written</i>
1863)
1864</pre>
1865<dd> The index of the node is written in the "next" field of
1866    a DdNode struct. LSB is not used (set to 0). It is used as
1867    "visited" flag in DD traversals.
1868<p>
1869
1870<dd> <b>Side Effects</b> None
1871<p>
1872
1873<dd> <b>See Also</b> <code><a href="#DddmpReadNodeIndexAdd">DddmpReadNodeIndexAdd</a>
1874()
1875<a href="#DddmpSetVisitedAdd">DddmpSetVisitedAdd</a>
1876()
1877<a href="#DddmpVisitedAdd">DddmpVisitedAdd</a>
1878()
1879</code>
1880
1881<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>
1882
1883<dt><pre>
1884<A NAME="DddmpWriteNodeIndexBdd"></A>
1885void <I></I>
1886<B>DddmpWriteNodeIndexBdd</B>(
1887  DdNode * <b>f</b>, <i>IN: BDD node</i>
1888  int  <b>id</b> <i>IN: index to be written</i>
1889)
1890</pre>
1891<dd> The index of the node is written in the "next" field of
1892    a DdNode struct. LSB is not used (set to 0). It is used as
1893    "visited" flag in DD traversals.
1894<p>
1895
1896<dd> <b>Side Effects</b> None
1897<p>
1898
1899<dd> <b>See Also</b> <code><a href="#DddmpReadNodeIndexBdd()">DddmpReadNodeIndexBdd()</a>
1900<a href="#DddmpSetVisitedBdd">DddmpSetVisitedBdd</a>
1901()
1902<a href="#DddmpVisitedBdd">DddmpVisitedBdd</a>
1903()
1904</code>
1905
1906<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>
1907
1908<dt><pre>
1909<A NAME="DddmpWriteNodeIndexCnfBis"></A>
1910int <I></I>
1911<B>DddmpWriteNodeIndexCnfBis</B>(
1912  DdNode * <b>f</b>, <i>IN: BDD node</i>
1913  int  <b>id</b> <i>IN: index to be written</i>
1914)
1915</pre>
1916<dd> The index of the node is written in the "next" field of
1917    a DdNode struct. LSB is not used (set to 0). It is used as
1918    "visited" flag in DD traversals.
1919<p>
1920
1921<dd> <b>Side Effects</b> None
1922<p>
1923
1924<dd> <b>See Also</b> <code><a href="#DddmpReadNodeIndexCnf()">DddmpReadNodeIndexCnf()</a>
1925<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
1926()
1927<a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
1928()
1929</code>
1930
1931<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
1932
1933<dt><pre>
1934<A NAME="DddmpWriteNodeIndexCnfWithTerminalCheck"></A>
1935static int <I></I>
1936<B>DddmpWriteNodeIndexCnfWithTerminalCheck</B>(
1937  DdNode * <b>f</b>, <i>IN: BDD node</i>
1938  int * <b>cnfIds</b>, <i>IN: possible source for the index to be written</i>
1939  int  <b>id</b> <i>IN: possible source for the index to be written</i>
1940)
1941</pre>
1942<dd> The index of the node is written in the "next" field of
1943    a DdNode struct. LSB is not used (set to 0). It is used as
1944    "visited" flag in DD traversals. The index corresponds to
1945    the BDD node variable if both the node's children are a
1946    constant node, otherwise a new CNF variable is used.
1947<p>
1948
1949<dd> <b>Side Effects</b> None
1950<p>
1951
1952<dd> <b>See Also</b> <code><a href="#DddmpReadNodeIndexCnf()">DddmpReadNodeIndexCnf()</a>
1953<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
1954()
1955<a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
1956()
1957</code>
1958
1959<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
1960
1961<dt><pre>
1962<A NAME="DddmpWriteNodeIndexCnf"></A>
1963int <I></I>
1964<B>DddmpWriteNodeIndexCnf</B>(
1965  DdNode * <b>f</b>, <i>IN: BDD node</i>
1966  int  <b>id</b> <i>IN: index to be written</i>
1967)
1968</pre>
1969<dd> The index of the node is written in the "next" field of
1970    a DdNode struct. LSB is not used (set to 0). It is used as
1971    "visited" flag in DD traversals.
1972<p>
1973
1974<dd> <b>Side Effects</b> None
1975<p>
1976
1977<dd> <b>See Also</b> <code><a href="#DddmpReadNodeIndexCnf()">DddmpReadNodeIndexCnf()</a>
1978<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
1979()
1980<a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
1981()
1982</code>
1983
1984<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
1985
1986<dt><pre>
1987<A NAME="DddmpWriteNodeIndexCnf"></A>
1988static int <I></I>
1989<B>DddmpWriteNodeIndexCnf</B>(
1990  DdNode * <b>f</b>, <i>IN: BDD node</i>
1991  int * <b>cnfIds</b>, <i>IN: possible source for the index to be written</i>
1992  int  <b>id</b> <i>IN: possible source for the index to be written</i>
1993)
1994</pre>
1995<dd> The index of the node is written in the "next" field of
1996    a DdNode struct. LSB is not used (set to 0). It is used as
1997    "visited" flag in DD traversals. The index corresponds to
1998    the BDD node variable if both the node's children are a
1999    constant node, otherwise a new CNF variable is used.
2000<p>
2001
2002<dd> <b>Side Effects</b> None
2003<p>
2004
2005<dd> <b>See Also</b> <code><a href="#DddmpReadNodeIndexCnf()">DddmpReadNodeIndexCnf()</a>
2006<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
2007()
2008<a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
2009()
2010</code>
2011
2012<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
2013
2014<dt><pre>
2015<A NAME="DddmpWriteNodeIndex"></A>
2016void <I></I>
2017<B>DddmpWriteNodeIndex</B>(
2018  DdNode * <b>f</b>, <i>IN: BDD node</i>
2019  int  <b>id</b> <i>IN: index to be written</i>
2020)
2021</pre>
2022<dd> The index of the node is written in the "next" field of
2023    a DdNode struct. LSB is not used (set to 0). It is used as
2024    "visited" flag in DD traversals.
2025<p>
2026
2027<dd> <b>Side Effects</b> None
2028<p>
2029
2030<dd> <b>See Also</b> <code><a href="#DddmpReadNodeIndex()">DddmpReadNodeIndex()</a>
2031<a href="#DddmpSetVisited">DddmpSetVisited</a>
2032()
2033<a href="#DddmpVisited">DddmpVisited</a>
2034()
2035</code>
2036
2037<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>
2038
2039<dt><pre>
2040<A NAME="Dddmp_Bin2Text"></A>
2041int <I></I>
2042<B>Dddmp_Bin2Text</B>(
2043  char * <b>filein</b>, <i>IN: name of binary file</i>
2044  char * <b>fileout</b> <i>IN: name of ASCII file</i>
2045)
2046</pre>
2047<dd> Converts from binary to ASCII format. A BDD array is loaded and
2048    and stored to the target file.
2049<p>
2050
2051<dd> <b>Side Effects</b> None
2052<p>
2053
2054<dd> <b>See Also</b> <code><a href="#Dddmp_Text2Bin()">Dddmp_Text2Bin()</a>
2055</code>
2056
2057<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpConvert.c"TARGET="ABSTRACT"><CODE>dddmpConvert.c</CODE></A>
2058
2059<dt><pre>
2060<A NAME="Dddmp_Text2Bin"></A>
2061int <I></I>
2062<B>Dddmp_Text2Bin</B>(
2063  char * <b>filein</b>, <i>IN: name of ASCII file</i>
2064  char * <b>fileout</b> <i>IN: name of binary file</i>
2065)
2066</pre>
2067<dd> Converts from ASCII to binary format. A BDD array is loaded and
2068    and stored to the target file.
2069<p>
2070
2071<dd> <b>Side Effects</b> None
2072<p>
2073
2074<dd> <b>See Also</b> <code><a href="#Dddmp_Bin2Text()">Dddmp_Bin2Text()</a>
2075</code>
2076
2077<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpConvert.c"TARGET="ABSTRACT"><CODE>dddmpConvert.c</CODE></A>
2078
2079<dt><pre>
2080<A NAME="Dddmp_cuddAddArrayLoad"></A>
2081int <I></I>
2082<B>Dddmp_cuddAddArrayLoad</B>(
2083  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2084  Dddmp_RootMatchType  <b>rootMatchMode</b>, <i>IN: storing mode selector</i>
2085  char ** <b>rootmatchnames</b>, <i>IN: sorted names for loaded roots</i>
2086  Dddmp_VarMatchType  <b>varMatchMode</b>, <i>IN: storing mode selector</i>
2087  char ** <b>varmatchnames</b>, <i>IN: array of variable names, by ids</i>
2088  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by ids</i>
2089  int * <b>varcomposeids</b>, <i>IN: array of new ids, by ids</i>
2090  int  <b>mode</b>, <i>IN: requested input file format</i>
2091  char * <b>file</b>, <i>IN: file name</i>
2092  FILE * <b>fp</b>, <i>IN: file pointer</i>
2093  DdNode *** <b>pproots</b> <i>OUT: array of returned BDD roots</i>
2094)
2095</pre>
2096<dd> Reads a dump file representing the argument ADDs. See
2097    BDD load functions for detailed explanation.
2098<p>
2099
2100<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
2101<p>
2102
2103<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
2104</code>
2105
2106<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoad.c"TARGET="ABSTRACT"><CODE>dddmpLoad.c</CODE></A>
2107
2108<dt><pre>
2109<A NAME="Dddmp_cuddAddArrayStore"></A>
2110int <I></I>
2111<B>Dddmp_cuddAddArrayStore</B>(
2112  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2113  char * <b>ddname</b>, <i>IN: DD name (or NULL)</i>
2114  int  <b>nRoots</b>, <i>IN: number of output BDD roots to be stored</i>
2115  DdNode ** <b>f</b>, <i>IN: array of ADD roots to be stored</i>
2116  char ** <b>rootnames</b>, <i>IN: array of root names (or NULL)</i>
2117  char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
2118  int * <b>auxids</b>, <i>IN: array of converted var IDs</i>
2119  int  <b>mode</b>, <i>IN: storing mode selector</i>
2120  Dddmp_VarInfoType  <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
2121  char * <b>fname</b>, <i>IN: File name</i>
2122  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
2123)
2124</pre>
2125<dd> Dumps the argument array of ADDs to file. Dumping is
2126    either in text or binary form. see the corresponding BDD dump
2127    function for further details.
2128<p>
2129
2130<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash
2131    table. They are re-linked after the store operation in a
2132    modified order.
2133<p>
2134
2135<dd> <b>See Also</b> <code><a href="#Dddmp_cuddAddStore">Dddmp_cuddAddStore</a>
2136<a href="#Dddmp_cuddAddLoad">Dddmp_cuddAddLoad</a>
2137<a href="#Dddmp_cuddAddArrayLoad">Dddmp_cuddAddArrayLoad</a>
2138</code>
2139
2140<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreAdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreAdd.c</CODE></A>
2141
2142<dt><pre>
2143<A NAME="Dddmp_cuddAddLoad"></A>
2144DdNode * <I></I>
2145<B>Dddmp_cuddAddLoad</B>(
2146  DdManager * <b>ddMgr</b>, <i>IN: Manager</i>
2147  Dddmp_VarMatchType  <b>varMatchMode</b>, <i>IN: storing mode selector</i>
2148  char ** <b>varmatchnames</b>, <i>IN: array of variable names by IDs</i>
2149  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids by IDs</i>
2150  int * <b>varcomposeids</b>, <i>IN: array of new ids by IDs</i>
2151  int  <b>mode</b>, <i>IN: requested input file format</i>
2152  char * <b>file</b>, <i>IN: file name</i>
2153  FILE * <b>fp</b> <i>IN: file pointer</i>
2154)
2155</pre>
2156<dd> Reads a dump file representing the argument ADD.
2157    Dddmp_cuddAddArrayLoad is used through a dummy array.
2158<p>
2159
2160<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
2161<p>
2162
2163<dd> <b>See Also</b> <code><a href="#Dddmp_cuddAddStore">Dddmp_cuddAddStore</a>
2164<a href="#Dddmp_cuddAddArrayLoad">Dddmp_cuddAddArrayLoad</a>
2165</code>
2166
2167<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoad.c"TARGET="ABSTRACT"><CODE>dddmpLoad.c</CODE></A>
2168
2169<dt><pre>
2170<A NAME="Dddmp_cuddAddStore"></A>
2171int <I></I>
2172<B>Dddmp_cuddAddStore</B>(
2173  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2174  char * <b>ddname</b>, <i>IN: DD name (or NULL)</i>
2175  DdNode * <b>f</b>, <i>IN: ADD root to be stored</i>
2176  char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
2177  int * <b>auxids</b>, <i>IN: array of converted var ids</i>
2178  int  <b>mode</b>, <i>IN: storing mode selector</i>
2179  Dddmp_VarInfoType  <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
2180  char * <b>fname</b>, <i>IN: File name</i>
2181  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
2182)
2183</pre>
2184<dd> Dumps the argument ADD to file. Dumping is done through
2185    Dddmp_cuddAddArrayStore, And a dummy array of 1 ADD root is
2186    used for this purpose.
2187<p>
2188
2189<dd> <b>Side Effects</b> Nodes are temporarily removed from unique hash. They are
2190    re-linked after the store operation in a modified order.
2191<p>
2192
2193<dd> <b>See Also</b> <code><a href="#Dddmp_cuddAddLoad">Dddmp_cuddAddLoad</a>
2194<a href="#Dddmp_cuddAddArrayLoad">Dddmp_cuddAddArrayLoad</a>
2195</code>
2196
2197<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreAdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreAdd.c</CODE></A>
2198
2199<dt><pre>
2200<A NAME="Dddmp_cuddBddArrayLoadCnf"></A>
2201int <I></I>
2202<B>Dddmp_cuddBddArrayLoadCnf</B>(
2203  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2204  Dddmp_RootMatchType  <b>rootmatchmode</b>, <i>IN: storing mode selector</i>
2205  char ** <b>rootmatchnames</b>, <i>IN: sorted names for loaded roots</i>
2206  Dddmp_VarMatchType  <b>varmatchmode</b>, <i>IN: storing mode selector</i>
2207  char ** <b>varmatchnames</b>, <i>IN: array of variable names, by IDs</i>
2208  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by IDs</i>
2209  int * <b>varcomposeids</b>, <i>IN: array of new ids, by IDs</i>
2210  int  <b>mode</b>, <i>IN: computation Mode</i>
2211  char * <b>file</b>, <i>IN: file name</i>
2212  FILE * <b>fp</b>, <i>IN: file pointer</i>
2213  DdNode *** <b>rootsPtrPtr</b>, <i>OUT: array of returned BDD roots</i>
2214  int * <b>nRoots</b> <i>OUT: number of BDDs returned</i>
2215)
2216</pre>
2217<dd> Reads a dump file representing the argument BDD in a
2218    CNF formula.
2219<p>
2220
2221<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
2222<p>
2223
2224<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
2225</code>
2226
2227<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoadCnf.c"TARGET="ABSTRACT"><CODE>dddmpLoadCnf.c</CODE></A>
2228
2229<dt><pre>
2230<A NAME="Dddmp_cuddBddArrayLoad"></A>
2231int <I></I>
2232<B>Dddmp_cuddBddArrayLoad</B>(
2233  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2234  Dddmp_RootMatchType  <b>rootMatchMode</b>, <i>IN: storing mode selector</i>
2235  char ** <b>rootmatchnames</b>, <i>IN: sorted names for loaded roots</i>
2236  Dddmp_VarMatchType  <b>varMatchMode</b>, <i>IN: storing mode selector</i>
2237  char ** <b>varmatchnames</b>, <i>IN: array of variable names, by ids</i>
2238  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by ids</i>
2239  int * <b>varcomposeids</b>, <i>IN: array of new ids, by ids</i>
2240  int  <b>mode</b>, <i>IN: requested input file format</i>
2241  char * <b>file</b>, <i>IN: file name</i>
2242  FILE * <b>fp</b>, <i>IN: file pointer</i>
2243  DdNode *** <b>pproots</b> <i>OUT: array of returned BDD roots</i>
2244)
2245</pre>
2246<dd> Reads a dump file representing the argument BDDs. The header is
2247    common to both text and binary mode. The node list is either
2248    in text or binary format. A dynamic vector of DD pointers
2249    is allocated to support conversion from DD indexes to pointers.
2250    Several criteria are supported for variable match between file
2251    and dd manager. Several changes/permutations/compositions are allowed
2252    for variables while loading DDs. Variable of the dd manager are allowed
2253    to match with variables on file on ids, permids, varnames,
2254    varauxids; also direct composition between ids and
2255    composeids is supported. More in detail:
2256    <ol>
2257    <li> varMatchMode=DDDMP_VAR_MATCHIDS <p>
2258    allows the loading of a DD keeping variable IDs unchanged
2259    (regardless of the variable ordering of the reading manager); this
2260    is useful, for example, when swapping DDs to file and restoring them
2261    later from file, after possible variable reordering activations.
2262   
2263    <li> varMatchMode=DDDMP_VAR_MATCHPERMIDS <p>
2264    is used to allow variable match according to the position in the
2265    ordering.
2266   
2267    <li> varMatchMode=DDDMP_VAR_MATCHNAMES <p>
2268    requires a non NULL varmatchnames parameter; this is a vector of
2269    strings in one-to-one correspondence with variable IDs of the
2270    reading manager. Variables in the DD file read are matched with
2271    manager variables according to their name (a non NULL varnames
2272    parameter was required while storing the DD file).
2273   
2274    <li> varMatchMode=DDDMP_VAR_MATCHIDS <p>
2275    has a meaning similar to DDDMP_VAR_MATCHNAMES, but integer auxiliary
2276    IDs are used instead of strings; the additional non NULL
2277    varmatchauxids parameter is needed.
2278   
2279    <li> varMatchMode=DDDMP_VAR_COMPOSEIDS <p>
2280    uses the additional varcomposeids parameter is used as array of
2281    variable ids to be composed with ids stored in file.
2282    </ol>
2283   
2284    In the present implementation, the array varnames (3), varauxids (4)
2285    and composeids (5) need to have one entry for each variable in the
2286    DD manager (NULL pointers are allowed for unused variables
2287    in varnames). Hence variables need to be already present in the
2288    manager. All arrays are sorted according to IDs.
2289
2290    All the loaded BDDs are referenced before returning them.
2291<p>
2292
2293<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
2294<p>
2295
2296<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
2297</code>
2298
2299<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoad.c"TARGET="ABSTRACT"><CODE>dddmpLoad.c</CODE></A>
2300
2301<dt><pre>
2302<A NAME="Dddmp_cuddBddArrayStoreBlif"></A>
2303int <I></I>
2304<B>Dddmp_cuddBddArrayStoreBlif</B>(
2305  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2306  int  <b>nroots</b>, <i>IN: number of output BDD roots to be stored</i>
2307  DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
2308  char ** <b>inputNames</b>, <i>IN: array of variable names (or NULL)</i>
2309  char ** <b>outputNames</b>, <i>IN: array of root names (or NULL)</i>
2310  char * <b>modelName</b>, <i>IN: Model Name</i>
2311  char * <b>fname</b>, <i>IN: File name</i>
2312  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
2313)
2314</pre>
2315<dd> Dumps the argument BDD to file.
2316    Dumping is done through Dddmp_cuddBddArrayStoreBLif.
2317    A dummy array of 1 BDD root is used for this purpose.
2318<p>
2319
2320<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStorePrefix">Dddmp_cuddBddArrayStorePrefix</a>
2321</code>
2322
2323<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>
2324
2325<dt><pre>
2326<A NAME="Dddmp_cuddBddArrayStoreCnf"></A>
2327int <I></I>
2328<B>Dddmp_cuddBddArrayStoreCnf</B>(
2329  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2330  DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
2331  int  <b>rootN</b>, <i>IN: # output BDD roots to be stored</i>
2332  Dddmp_DecompCnfStoreType  <b>mode</b>, <i>IN: format selection</i>
2333  int  <b>noHeader</b>, <i>IN: do not store header iff 1</i>
2334  char ** <b>varNames</b>, <i>IN: array of variable names (or NULL)</i>
2335  int * <b>bddIds</b>, <i>IN: array of converted var IDs</i>
2336  int * <b>bddAuxIds</b>, <i>IN: array of BDD node Auxiliary Ids</i>
2337  int * <b>cnfIds</b>, <i>IN: array of converted var IDs</i>
2338  int  <b>idInitial</b>, <i>IN: starting id for cutting variables</i>
2339  int  <b>edgeInTh</b>, <i>IN: Max # Incoming Edges</i>
2340  int  <b>pathLengthTh</b>, <i>IN: Max Path Length</i>
2341  char * <b>fname</b>, <i>IN: file name</i>
2342  FILE * <b>fp</b>, <i>IN: pointer to the store file</i>
2343  int * <b>clauseNPtr</b>, <i>OUT: number of clause stored</i>
2344  int * <b>varNewNPtr</b> <i>OUT: number of new variable created</i>
2345)
2346</pre>
2347<dd> Dumps the argument array of BDDs to file.
2348<p>
2349
2350<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash
2351    table. They are re-linked after the store operation in a
2352    modified order.
2353    Three methods are allowed:
2354    * NodeByNode method: Insert a cut-point for each BDD node (but the
2355                         terminal nodes)
2356    * MaxtermByMaxterm method: Insert no cut-points, i.e. the off-set of
2357                               trhe function is stored
2358    * Best method: Tradeoff between the previous two methods.
2359      Auxiliary variables, i.e., cut points are inserted following these
2360      criterias:
2361      * edgeInTh
2362        indicates the maximum number of incoming edges up to which
2363        no cut point (auxiliary variable) is inserted.
2364        If edgeInTh:
2365        * is equal to -1 no cut point due to incoming edges are inserted
2366          (MaxtermByMaxterm method.)
2367        * is equal to 0 a cut point is inserted for each node with a single
2368          incoming edge, i.e., each node, (NodeByNode method).
2369        * is equal to n a cut point is inserted for each node with (n+1)
2370          incoming edges.
2371      * pathLengthTh
2372        indicates the maximum length path up to which no cut points
2373        (auxiliary variable) is inserted.
2374        If the path length between two nodes exceeds this value, a cut point
2375        is inserted.
2376        If pathLengthTh:
2377        * is equal to -1 no cut point due path length are inserted
2378          (MaxtermByMaxterm method.)
2379        * is equal to 0 a cut point is inserted for each node (NodeByNode
2380          method).
2381        * is equal to n a cut point is inserted on path whose length is
2382          equal to (n+1).
2383        Notice that the maximum number of literals in a clause is equal
2384        to (pathLengthTh + 2), i.e., for each path we have to keep into
2385        account a CNF variable for each node plus 2 added variables for
2386        the bottom and top-path cut points.
2387    The stored file can contain a file header or not depending on the
2388    noHeader parameter (IFF 0, usual setting, the header is usually stored.
2389    This option can be useful in storing multiple BDDs, as separate BDDs,
2390    on the same file leaving the opening of the file to the caller.
2391<p>
2392
2393<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>
2394
2395<dt><pre>
2396<A NAME="Dddmp_cuddBddArrayStorePrefix"></A>
2397int <I></I>
2398<B>Dddmp_cuddBddArrayStorePrefix</B>(
2399  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2400  int  <b>nroots</b>, <i>IN: number of output BDD roots to be stored</i>
2401  DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
2402  char ** <b>inputNames</b>, <i>IN: array of variable names (or NULL)</i>
2403  char ** <b>outputNames</b>, <i>IN: array of root names (or NULL)</i>
2404  char * <b>modelName</b>, <i>IN: Model Name</i>
2405  char * <b>fname</b>, <i>IN: File name</i>
2406  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
2407)
2408</pre>
2409<dd> Dumps the argument BDD to file.
2410    Dumping is done through Dddmp_cuddBddArrayStorePrefix.
2411    A dummy array of 1 BDD root is used for this purpose.
2412<p>
2413
2414<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
2415</code>
2416
2417<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>
2418
2419<dt><pre>
2420<A NAME="Dddmp_cuddBddArrayStoreSmv"></A>
2421int <I></I>
2422<B>Dddmp_cuddBddArrayStoreSmv</B>(
2423  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2424  int  <b>nroots</b>, <i>IN: number of output BDD roots to be stored</i>
2425  DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
2426  char ** <b>inputNames</b>, <i>IN: array of variable names (or NULL)</i>
2427  char ** <b>outputNames</b>, <i>IN: array of root names (or NULL)</i>
2428  char * <b>modelName</b>, <i>IN: Model Name</i>
2429  char * <b>fname</b>, <i>IN: File name</i>
2430  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
2431)
2432</pre>
2433<dd> Dumps the argument BDD to file.
2434    Dumping is done through Dddmp_cuddBddArrayStorePrefix.
2435    A dummy array of 1 BDD root is used for this purpose.
2436<p>
2437
2438<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
2439</code>
2440
2441<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>
2442
2443<dt><pre>
2444<A NAME="Dddmp_cuddBddArrayStore"></A>
2445int <I></I>
2446<B>Dddmp_cuddBddArrayStore</B>(
2447  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2448  char * <b>ddname</b>, <i>IN: dd name (or NULL)</i>
2449  int  <b>nRoots</b>, <i>IN: number of output BDD roots to be stored</i>
2450  DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
2451  char ** <b>rootnames</b>, <i>IN: array of root names (or NULL)</i>
2452  char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
2453  int * <b>auxids</b>, <i>IN: array of converted var IDs</i>
2454  int  <b>mode</b>, <i>IN: storing mode selector</i>
2455  Dddmp_VarInfoType  <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
2456  char * <b>fname</b>, <i>IN: File name</i>
2457  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
2458)
2459</pre>
2460<dd> Dumps the argument array of BDDs to file. Dumping is either
2461    in text or binary form.  BDDs are stored to the fp (already
2462    open) file if not NULL. Otherwise the file whose name is
2463    fname is opened in write mode. The header has the same format
2464    for both textual and binary dump. Names are allowed for input
2465    variables (vnames) and for represented functions (rnames).
2466    For sake of generality and because of dynamic variable
2467    ordering both variable IDs and permuted IDs are included.
2468    New IDs are also supported (auxids). Variables are identified
2469    with incremental numbers. according with their positiom in
2470    the support set. In text mode, an extra info may be added,
2471    chosen among the following options: name, ID, PermID, or an
2472    auxiliary id. Since conversion from DD pointers to integers
2473    is required, DD nodes are temporarily removed from the unique
2474    hash table. This allows the use of the next field to store
2475    node IDs.
2476<p>
2477
2478<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash
2479    table. They are re-linked after the store operation in a
2480    modified order.
2481<p>
2482
2483<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
2484<a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
2485<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
2486</code>
2487
2488<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreBdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreBdd.c</CODE></A>
2489
2490<dt><pre>
2491<A NAME="Dddmp_cuddBddDisplayBinary"></A>
2492int <I></I>
2493<B>Dddmp_cuddBddDisplayBinary</B>(
2494  char * <b>fileIn</b>, <i>IN: name of binary file</i>
2495  char * <b>fileOut</b> <i>IN: name of text file</i>
2496)
2497</pre>
2498<dd> Display a binary dump file in a text file
2499<p>
2500
2501<dd> <b>Side Effects</b> None
2502<p>
2503
2504<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
2505<a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
2506</code>
2507
2508<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDbg.c"TARGET="ABSTRACT"><CODE>dddmpDbg.c</CODE></A>
2509
2510<dt><pre>
2511<A NAME="Dddmp_cuddBddLoadCnf"></A>
2512int <I></I>
2513<B>Dddmp_cuddBddLoadCnf</B>(
2514  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2515  Dddmp_VarMatchType  <b>varmatchmode</b>, <i>IN: storing mode selector</i>
2516  char ** <b>varmatchnames</b>, <i>IN: array of variable names, by IDs</i>
2517  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by IDs</i>
2518  int * <b>varcomposeids</b>, <i>IN: array of new ids accessed, by IDs</i>
2519  int  <b>mode</b>, <i>IN: computation mode</i>
2520  char * <b>file</b>, <i>IN: file name</i>
2521  FILE * <b>fp</b>, <i>IN: file pointer</i>
2522  DdNode *** <b>rootsPtrPtr</b>, <i>OUT: array of returned BDD roots</i>
2523  int * <b>nRoots</b> <i>OUT: number of BDDs returned</i>
2524)
2525</pre>
2526<dd> Reads a dump file representing the argument BDD in a
2527    CNF formula.
2528    Dddmp_cuddBddArrayLoadCnf is used through a dummy array.
2529    The results is returned in different formats depending on the
2530    mode selection:
2531      IFF mode == 0 Return the Clauses without Conjunction
2532      IFF mode == 1 Return the sets of BDDs without Quantification
2533      IFF mode == 2 Return the sets of BDDs AFTER Existential Quantification
2534<p>
2535
2536<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
2537<p>
2538
2539<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
2540<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
2541</code>
2542
2543<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoadCnf.c"TARGET="ABSTRACT"><CODE>dddmpLoadCnf.c</CODE></A>
2544
2545<dt><pre>
2546<A NAME="Dddmp_cuddBddLoad"></A>
2547DdNode * <I></I>
2548<B>Dddmp_cuddBddLoad</B>(
2549  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2550  Dddmp_VarMatchType  <b>varMatchMode</b>, <i>IN: storing mode selector</i>
2551  char ** <b>varmatchnames</b>, <i>IN: array of variable names - by IDs</i>
2552  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids - by IDs</i>
2553  int * <b>varcomposeids</b>, <i>IN: array of new ids accessed - by IDs</i>
2554  int  <b>mode</b>, <i>IN: requested input file format</i>
2555  char * <b>file</b>, <i>IN: file name</i>
2556  FILE * <b>fp</b> <i>IN: file pointer</i>
2557)
2558</pre>
2559<dd> Reads a dump file representing the argument BDD.
2560    Dddmp_cuddBddArrayLoad is used through a dummy array (see this
2561    function's description for more details).
2562    Mode, the requested input file format, is checked against
2563    the file format.
2564    The loaded BDDs is referenced before returning it.
2565<p>
2566
2567<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
2568<p>
2569
2570<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
2571<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
2572</code>
2573
2574<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoad.c"TARGET="ABSTRACT"><CODE>dddmpLoad.c</CODE></A>
2575
2576<dt><pre>
2577<A NAME="Dddmp_cuddBddStoreBlif"></A>
2578int <I></I>
2579<B>Dddmp_cuddBddStoreBlif</B>(
2580  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2581  int  <b>nRoots</b>, <i>IN: Number of BDD roots</i>
2582  DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
2583  char ** <b>inputNames</b>, <i>IN: Array of variable names</i>
2584  char ** <b>outputNames</b>, <i>IN: Array of root names</i>
2585  char * <b>modelName</b>, <i>IN: Model Name</i>
2586  char * <b>fileName</b>, <i>IN: File name</i>
2587  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
2588)
2589</pre>
2590<dd> Dumps the argument BDD to file.
2591    Dumping is done through Dddmp_cuddBddArrayStoreBlif.
2592    A dummy array of 1 BDD root is used for this purpose.
2593<p>
2594
2595<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStorePrefix">Dddmp_cuddBddStorePrefix</a>
2596</code>
2597
2598<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>
2599
2600<dt><pre>
2601<A NAME="Dddmp_cuddBddStoreCnf"></A>
2602int <I></I>
2603<B>Dddmp_cuddBddStoreCnf</B>(
2604  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2605  DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
2606  Dddmp_DecompCnfStoreType  <b>mode</b>, <i>IN: format selection</i>
2607  int  <b>noHeader</b>, <i>IN: do not store header iff 1</i>
2608  char ** <b>varNames</b>, <i>IN: array of variable names (or NULL)</i>
2609  int * <b>bddIds</b>, <i>IN: array of var ids</i>
2610  int * <b>bddAuxIds</b>, <i>IN: array of BDD node Auxiliary Ids</i>
2611  int * <b>cnfIds</b>, <i>IN: array of CNF var ids</i>
2612  int  <b>idInitial</b>, <i>IN: starting id for cutting variables</i>
2613  int  <b>edgeInTh</b>, <i>IN: Max # Incoming Edges</i>
2614  int  <b>pathLengthTh</b>, <i>IN: Max Path Length</i>
2615  char * <b>fname</b>, <i>IN: file name</i>
2616  FILE * <b>fp</b>, <i>IN: pointer to the store file</i>
2617  int * <b>clauseNPtr</b>, <i>OUT: number of clause stored</i>
2618  int * <b>varNewNPtr</b> <i>OUT: number of new variable created</i>
2619)
2620</pre>
2621<dd> Dumps the argument BDD to file.
2622    This task is performed by calling the function
2623    Dddmp_cuddBddArrayStoreCnf.
2624<p>
2625
2626<dd> <b>Side Effects</b> Nodes are temporarily removed from unique hash. They are
2627    re-linked after the store operation in a modified order.
2628<p>
2629
2630<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStoreCnf">Dddmp_cuddBddArrayStoreCnf</a>
2631</code>
2632
2633<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>
2634
2635<dt><pre>
2636<A NAME="Dddmp_cuddBddStorePrefix"></A>
2637int <I></I>
2638<B>Dddmp_cuddBddStorePrefix</B>(
2639  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2640  int  <b>nRoots</b>, <i>IN: Number of BDD roots</i>
2641  DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
2642  char ** <b>inputNames</b>, <i>IN: Array of variable names</i>
2643  char ** <b>outputNames</b>, <i>IN: Array of root names</i>
2644  char * <b>modelName</b>, <i>IN: Model Name</i>
2645  char * <b>fileName</b>, <i>IN: File name</i>
2646  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
2647)
2648</pre>
2649<dd> Dumps the argument BDD to file.
2650    Dumping is done through Dddmp_cuddBddArrayStorePrefix.
2651    A dummy array of 1 BDD root is used for this purpose.
2652<p>
2653
2654<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
2655</code>
2656
2657<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>
2658
2659<dt><pre>
2660<A NAME="Dddmp_cuddBddStoreSmv"></A>
2661int <I></I>
2662<B>Dddmp_cuddBddStoreSmv</B>(
2663  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2664  int  <b>nRoots</b>, <i>IN: Number of BDD roots</i>
2665  DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
2666  char ** <b>inputNames</b>, <i>IN: Array of variable names</i>
2667  char ** <b>outputNames</b>, <i>IN: Array of root names</i>
2668  char * <b>modelName</b>, <i>IN: Model Name</i>
2669  char * <b>fileName</b>, <i>IN: File name</i>
2670  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
2671)
2672</pre>
2673<dd> Dumps the argument BDD to file.
2674    Dumping is done through Dddmp_cuddBddArrayStorePrefix.
2675    A dummy array of 1 BDD root is used for this purpose.
2676<p>
2677
2678<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
2679</code>
2680
2681<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>
2682
2683<dt><pre>
2684<A NAME="Dddmp_cuddBddStore"></A>
2685int <I></I>
2686<B>Dddmp_cuddBddStore</B>(
2687  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2688  char * <b>ddname</b>, <i>IN: DD name (or NULL)</i>
2689  DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
2690  char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
2691  int * <b>auxids</b>, <i>IN: array of converted var ids</i>
2692  int  <b>mode</b>, <i>IN: storing mode selector</i>
2693  Dddmp_VarInfoType  <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
2694  char * <b>fname</b>, <i>IN: File name</i>
2695  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
2696)
2697</pre>
2698<dd> Dumps the argument BDD to file. Dumping is done through
2699    Dddmp_cuddBddArrayStore. A dummy array of 1 BDD root is
2700    used for this purpose.
2701<p>
2702
2703<dd> <b>Side Effects</b> Nodes are temporarily removed from unique hash. They are
2704    re-linked after the store operation in a modified order.
2705<p>
2706
2707<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
2708<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
2709</code>
2710
2711<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreBdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreBdd.c</CODE></A>
2712
2713<dt><pre>
2714<A NAME="Dddmp_cuddHeaderLoadCnf"></A>
2715int <I></I>
2716<B>Dddmp_cuddHeaderLoadCnf</B>(
2717  int * <b>nVars</b>, <i>OUT: number of DD variables</i>
2718  int * <b>nsuppvars</b>, <i>OUT: number of support variables</i>
2719  char *** <b>suppVarNames</b>, <i>OUT: array of support variable names</i>
2720  char *** <b>orderedVarNames</b>, <i>OUT: array of variable names</i>
2721  int ** <b>varIds</b>, <i>OUT: array of variable ids</i>
2722  int ** <b>varComposeIds</b>, <i>OUT: array of permids ids</i>
2723  int ** <b>varAuxIds</b>, <i>OUT: array of variable aux ids</i>
2724  int * <b>nRoots</b>, <i>OUT: number of root in the file</i>
2725  char * <b>file</b>, <i>IN: file name</i>
2726  FILE * <b>fp</b> <i>IN: file pointer</i>
2727)
2728</pre>
2729<dd> Reads the header of a dump file representing the argument BDDs.
2730    Returns main information regarding DD type stored in the file,
2731    the variable ordering used, the number of variables, etc.
2732    It reads only the header of the file NOT the BDD/ADD section.
2733<p>
2734
2735<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
2736</code>
2737
2738<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoadCnf.c"TARGET="ABSTRACT"><CODE>dddmpLoadCnf.c</CODE></A>
2739
2740<dt><pre>
2741<A NAME="Dddmp_cuddHeaderLoad"></A>
2742int <I></I>
2743<B>Dddmp_cuddHeaderLoad</B>(
2744  Dddmp_DecompType * <b>ddType</b>, <i>OUT: selects the proper decomp type</i>
2745  int * <b>nVars</b>, <i>OUT: number of DD variables</i>
2746  int * <b>nsuppvars</b>, <i>OUT: number of support variables</i>
2747  char *** <b>suppVarNames</b>, <i>OUT: array of support variable names</i>
2748  char *** <b>orderedVarNames</b>, <i>OUT: array of variable names</i>
2749  int ** <b>varIds</b>, <i>OUT: array of variable ids</i>
2750  int ** <b>varComposeIds</b>, <i>OUT: array of permids ids</i>
2751  int ** <b>varAuxIds</b>, <i>OUT: array of variable aux ids</i>
2752  int * <b>nRoots</b>, <i>OUT: number of root in the file</i>
2753  char * <b>file</b>, <i>IN: file name</i>
2754  FILE * <b>fp</b> <i>IN: file pointer</i>
2755)
2756</pre>
2757<dd> Reads the header of a dump file representing the argument BDDs.
2758    Returns main information regarding DD type stored in the file,
2759    the variable ordering used, the number of variables, etc.
2760    It reads only the header of the file NOT the BDD/ADD section.
2761<p>
2762
2763<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
2764</code>
2765
2766<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoad.c"TARGET="ABSTRACT"><CODE>dddmpLoad.c</CODE></A>
2767
2768<dt><pre>
2769<A NAME="FindVarname"></A>
2770int <I></I>
2771<B>FindVarname</B>(
2772  char * <b>name</b>, <i>IN: name to look for</i>
2773  char ** <b>array</b>, <i>IN: search array</i>
2774  int  <b>n</b> <i>IN: size of the array</i>
2775)
2776</pre>
2777<dd> Binary search of a name within a sorted array of strings.
2778    Used when matching names of variables.
2779<p>
2780
2781<dd> <b>Side Effects</b> None
2782<p>
2783
2784<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>
2785
2786<dt><pre>
2787<A NAME="NodeBinaryStoreBdd"></A>
2788static int <I></I>
2789<B>NodeBinaryStoreBdd</B>(
2790  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2791  DdNode * <b>f</b>, <i>IN: DD node to be stored</i>
2792  int  <b>mode</b>, <i>IN: store mode</i>
2793  int * <b>supportids</b>, <i>IN: internal ids for variables</i>
2794  char ** <b>varnames</b>, <i>IN: names of variables: to be stored with nodes</i>
2795  int * <b>outids</b>, <i>IN: output ids for variables</i>
2796  FILE * <b>fp</b>, <i>IN: store file</i>
2797  int  <b>idf</b>, <i>IN: index of the node</i>
2798  int  <b>vf</b>, <i>IN: variable of the node</i>
2799  int  <b>idT</b>, <i>IN: index of the Then node</i>
2800  int  <b>idE</b>, <i>IN: index of the Else node</i>
2801  int  <b>vT</b>, <i>IN: variable of the Then node</i>
2802  int  <b>vE</b>, <i>IN: variable of the Else node</i>
2803  DdNode * <b>T</b>, <i>IN: Then node</i>
2804  DdNode * <b>E</b> <i>IN: Else node</i>
2805)
2806</pre>
2807<dd> Store 1 0 0 for the terminal node.
2808    Store id, left child pointer, right pointer for all the other nodes.
2809    Store every information as coded binary values.
2810<p>
2811
2812<dd> <b>Side Effects</b> None
2813<p>
2814
2815<dd> <b>See Also</b> <code><a href="#NodeTextStoreBdd">NodeTextStoreBdd</a>
2816</code>
2817
2818<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreBdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreBdd.c</CODE></A>
2819
2820<dt><pre>
2821<A NAME="NodeStoreRecurAdd"></A>
2822static int <I></I>
2823<B>NodeStoreRecurAdd</B>(
2824  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2825  DdNode * <b>f</b>, <i>IN: DD node to be stored</i>
2826  int  <b>mode</b>, <i>IN: store mode</i>
2827  int * <b>supportids</b>, <i>IN: internal ids for variables</i>
2828  char ** <b>varnames</b>, <i>IN: names of variables: to be stored with nodes</i>
2829  int * <b>outids</b>, <i>IN: output ids for variables</i>
2830  FILE * <b>fp</b> <i>IN: store file</i>
2831)
2832</pre>
2833<dd> Stores a node to file in either test or binary mode.<l>
2834    In text mode a node is represented (on a text line basis) as
2835    <UL>
2836    <LI> node-index [var-extrainfo] var-index Then-index Else-index
2837    </UL>
2838   
2839    where all indexes are integer numbers and var-extrainfo
2840    (optional redundant field) is either an integer or a string
2841    (variable name). Node-index is redundant (due to the node
2842    ordering) but we keep it for readability.<p>
2843   
2844    In binary mode nodes are represented as a sequence of bytes,
2845    representing var-index, Then-index, and Else-index in an
2846    optimized way. Only the first byte (code) is mandatory.
2847    Integer indexes are represented in absolute or relative mode,
2848    where relative means offset wrt. a Then/Else node info.
2849    Suppose Var(NodeId), Then(NodeId) and Else(NodeId) represent
2850    infos about a given node.<p>
2851   
2852    The generic "NodeId" node is stored as
2853
2854    <UL>
2855    <LI> code-byte
2856    <LI> [var-info]
2857    <LI> [Then-info]
2858    <LI> [Else-info]
2859    </UL>
2860
2861    where code-byte contains bit fields
2862
2863    <UL>
2864    <LI>Unused  : 1 bit
2865    <LI>Variable: 2 bits, one of the following codes
2866    <UL>
2867    <LI>DDDMP_ABSOLUTE_ID   var-info = Var(NodeId) follows
2868    <LI>DDDMP_RELATIVE_ID   Var(NodeId) is represented in relative form as
2869        var-info = Min(Var(Then(NodeId)),Var(Else(NodeId))) -Var(NodeId)
2870    <LI>DDDMP_RELATIVE_1    No var-info follows, because
2871        Var(NodeId) = Min(Var(Then(NodeId)),Var(Else(NodeId)))-1
2872    <LI>DDDMP_TERMINAL      Node is a terminal, no var info required
2873    </UL>
2874    <LI>T       : 2 bits, with codes similar to V
2875    <UL>
2876    <LI>DDDMP_ABSOLUTE_ID   Then-info = Then(NodeId) follows
2877    <LI>DDDMP_RELATIVE_ID   Then(NodeId) is represented in relative form as
2878          Then-info = Nodeid-Then(NodeId)
2879    <LI>DDDMP_RELATIVE_1    No info on Then(NodeId) follows, because
2880          Then(NodeId) = NodeId-1
2881    <LI>DDDMP_TERMINAL Then Node is a terminal, no info required (for BDDs)
2882    </UL>
2883    <LI>Ecompl  : 1 bit, if 1 means complemented edge
2884    <LI>E       : 2 bits, with codes and meanings as for the Then edge
2885    </UL>
2886    var-info, Then-info, Else-info (if required) are represented as unsigned
2887    integer values on a sufficient set of bytes (MSByte first).
2888<p>
2889
2890<dd> <b>Side Effects</b> None
2891<p>
2892
2893<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreAdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreAdd.c</CODE></A>
2894
2895<dt><pre>
2896<A NAME="NodeStoreRecurBdd"></A>
2897static int <I></I>
2898<B>NodeStoreRecurBdd</B>(
2899  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2900  DdNode * <b>f</b>, <i>IN: DD node to be stored</i>
2901  int  <b>mode</b>, <i>IN: store mode</i>
2902  int * <b>supportids</b>, <i>IN: internal ids for variables</i>
2903  char ** <b>varnames</b>, <i>IN: names of variables: to be stored with nodes</i>
2904  int * <b>outids</b>, <i>IN: output ids for variables</i>
2905  FILE * <b>fp</b> <i>IN: store file</i>
2906)
2907</pre>
2908<dd> Stores a node to file in either test or binary mode.<l>
2909    In text mode a node is represented (on a text line basis) as
2910    <UL>
2911    <LI> node-index [var-extrainfo] var-index Then-index Else-index
2912    </UL>
2913   
2914    where all indexes are integer numbers and var-extrainfo
2915    (optional redundant field) is either an integer or a string
2916    (variable name). Node-index is redundant (due to the node
2917    ordering) but we keep it for readability.<p>
2918   
2919    In binary mode nodes are represented as a sequence of bytes,
2920    representing var-index, Then-index, and Else-index in an
2921    optimized way. Only the first byte (code) is mandatory.
2922    Integer indexes are represented in absolute or relative mode,
2923    where relative means offset wrt. a Then/Else node info.
2924    Suppose Var(NodeId), Then(NodeId) and Else(NodeId) represent
2925    infos about a given node.<p>
2926   
2927    The generic "NodeId" node is stored as
2928
2929    <UL>
2930    <LI> code-byte
2931    <LI> [var-info]
2932    <LI> [Then-info]
2933    <LI> [Else-info]
2934    </UL>
2935
2936    where code-byte contains bit fields
2937
2938    <UL>
2939    <LI>Unused  : 1 bit
2940    <LI>Variable: 2 bits, one of the following codes
2941    <UL>
2942    <LI>DDDMP_ABSOLUTE_ID   var-info = Var(NodeId) follows
2943    <LI>DDDMP_RELATIVE_ID   Var(NodeId) is represented in relative form as
2944        var-info = Min(Var(Then(NodeId)),Var(Else(NodeId))) -Var(NodeId)
2945    <LI>DDDMP_RELATIVE_1    No var-info follows, because
2946        Var(NodeId) = Min(Var(Then(NodeId)),Var(Else(NodeId)))-1
2947    <LI>DDDMP_TERMINAL      Node is a terminal, no var info required
2948    </UL>
2949    <LI>T       : 2 bits, with codes similar to V
2950    <UL>
2951    <LI>DDDMP_ABSOLUTE_ID   Then-info = Then(NodeId) follows
2952    <LI>DDDMP_RELATIVE_ID   Then(NodeId) is represented in relative form as
2953          Then-info = Nodeid-Then(NodeId)
2954    <LI>DDDMP_RELATIVE_1    No info on Then(NodeId) follows, because
2955          Then(NodeId) = NodeId-1
2956    <LI>DDDMP_TERMINAL Then Node is a terminal, no info required (for BDDs)
2957    </UL>
2958    <LI>Ecompl  : 1 bit, if 1 means complemented edge
2959    <LI>E       : 2 bits, with codes and meanings as for the Then edge
2960    </UL>
2961    var-info, Then-info, Else-info (if required) are represented as unsigned
2962    integer values on a sufficient set of bytes (MSByte first).
2963<p>
2964
2965<dd> <b>Side Effects</b> None
2966<p>
2967
2968<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreBdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreBdd.c</CODE></A>
2969
2970<dt><pre>
2971<A NAME="NodeTextStoreAdd"></A>
2972static int <I></I>
2973<B>NodeTextStoreAdd</B>(
2974  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
2975  DdNode * <b>f</b>, <i>IN: DD node to be stored</i>
2976  int  <b>mode</b>, <i>IN: store mode</i>
2977  int * <b>supportids</b>, <i>IN: internal ids for variables</i>
2978  char ** <b>varnames</b>, <i>IN: names of variables: to be stored with nodes</i>
2979  int * <b>outids</b>, <i>IN: output ids for variables</i>
2980  FILE * <b>fp</b>, <i>IN: Store file</i>
2981  int  <b>idf</b>, <i>IN: index of the current node</i>
2982  int  <b>vf</b>, <i>IN: variable of the current node</i>
2983  int  <b>idT</b>, <i>IN: index of the Then node</i>
2984  int  <b>idE</b> <i>IN: index of the Else node</i>
2985)
2986</pre>
2987<dd> Store 1 0 0 for the terminal node.
2988    Store id, left child pointer, right pointer for all the other nodes.
2989<p>
2990
2991<dd> <b>Side Effects</b> None
2992<p>
2993
2994<dd> <b>See Also</b> <code><a href="#NodeBinaryStore">NodeBinaryStore</a>
2995</code>
2996
2997<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreAdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreAdd.c</CODE></A>
2998
2999<dt><pre>
3000<A NAME="NodeTextStoreBdd"></A>
3001static int <I></I>
3002<B>NodeTextStoreBdd</B>(
3003  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3004  DdNode * <b>f</b>, <i>IN: DD node to be stored</i>
3005  int  <b>mode</b>, <i>IN: store mode</i>
3006  int * <b>supportids</b>, <i>IN: internal ids for variables</i>
3007  char ** <b>varnames</b>, <i>IN: names of variables: to be stored with nodes</i>
3008  int * <b>outids</b>, <i>IN: output ids for variables</i>
3009  FILE * <b>fp</b>, <i>IN: Store file</i>
3010  int  <b>idf</b>, <i>IN: index of the current node</i>
3011  int  <b>vf</b>, <i>IN: variable of the current node</i>
3012  int  <b>idT</b>, <i>IN: index of the Then node</i>
3013  int  <b>idE</b> <i>IN: index of the Else node</i>
3014)
3015</pre>
3016<dd> Store 1 0 0 for the terminal node.
3017    Store id, left child pointer, right pointer for all the other nodes.
3018<p>
3019
3020<dd> <b>Side Effects</b> None
3021<p>
3022
3023<dd> <b>See Also</b> <code><a href="#NodeBinaryStoreBdd">NodeBinaryStoreBdd</a>
3024</code>
3025
3026<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreBdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreBdd.c</CODE></A>
3027
3028<dt><pre>
3029<A NAME="NumberNodeRecurAdd"></A>
3030static int <I></I>
3031<B>NumberNodeRecurAdd</B>(
3032  DdNode * <b>f</b>, <i>IN: root of the BDD to be numbered</i>
3033  int  <b>id</b> <i>IN/OUT: index to be assigned to the node</i>
3034)
3035</pre>
3036<dd> Number nodes recursively in post-order.
3037    The "visited" flag is used with inverse polarity, because all nodes
3038    were set "visited" when removing them from unique.
3039<p>
3040
3041<dd> <b>Side Effects</b> "visited" flags are reset.
3042<p>
3043
3044<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>
3045
3046<dt><pre>
3047<A NAME="NumberNodeRecurBdd"></A>
3048static int <I></I>
3049<B>NumberNodeRecurBdd</B>(
3050  DdNode * <b>f</b>, <i>IN: root of the BDD to be numbered</i>
3051  int  <b>id</b> <i>IN/OUT: index to be assigned to the node</i>
3052)
3053</pre>
3054<dd> Number nodes recursively in post-order.
3055    The "visited" flag is used with inverse polarity, because all nodes
3056    were set "visited" when removing them from unique.
3057<p>
3058
3059<dd> <b>Side Effects</b> "visited" flags are reset.
3060<p>
3061
3062<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>
3063
3064<dt><pre>
3065<A NAME="NumberNodeRecurCnf"></A>
3066static int <I></I>
3067<B>NumberNodeRecurCnf</B>(
3068  DdNode * <b>f</b>, <i>IN: root of the BDD to be numbered</i>
3069  int * <b>cnfIds</b>, <i>IN: possible source for numbering</i>
3070  int  <b>id</b> <i>IN/OUT: possible source for numbering</i>
3071)
3072</pre>
3073<dd> Number nodes recursively in post-order.
3074    The "visited" flag is used with inverse polarity, because all nodes
3075    were set "visited" when removing them from unique.
3076<p>
3077
3078<dd> <b>Side Effects</b> "visited" flags are reset.
3079<p>
3080
3081<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
3082
3083<dt><pre>
3084<A NAME="NumberNodeRecurCnf"></A>
3085static int <I></I>
3086<B>NumberNodeRecurCnf</B>(
3087  DdNode * <b>f</b>, <i>IN: root of the BDD to be numbered</i>
3088  int * <b>cnfIds</b>, <i>IN: possible source for numbering</i>
3089  int  <b>id</b> <i>IN/OUT: possible source for numbering</i>
3090)
3091</pre>
3092<dd> Number nodes recursively in post-order.
3093    The "visited" flag is used with inverse polarity, because all nodes
3094    were set "visited" when removing them from unique.
3095<p>
3096
3097<dd> <b>Side Effects</b> "visited" flags are reset.
3098<p>
3099
3100<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
3101
3102<dt><pre>
3103<A NAME="NumberNodeRecur"></A>
3104static int <I></I>
3105<B>NumberNodeRecur</B>(
3106  DdNode * <b>f</b>, <i>IN: root of the BDD to be numbered</i>
3107  int  <b>id</b> <i>IN/OUT: index to be assigned to the node</i>
3108)
3109</pre>
3110<dd> Number nodes recursively in post-order.
3111    The "visited" flag is used with inverse polarity, because all nodes
3112    were set "visited" when removing them from unique.
3113<p>
3114
3115<dd> <b>Side Effects</b> "visited" flags are reset.
3116<p>
3117
3118<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>
3119
3120<dt><pre>
3121<A NAME="QsortStrcmp"></A>
3122int <I></I>
3123<B>QsortStrcmp</B>(
3124  const void * <b>ps1</b>, <i>IN: pointer to the first string</i>
3125  const void * <b>ps2</b> <i>IN: pointer to the second string</i>
3126)
3127</pre>
3128<dd> String compare for qsort
3129<p>
3130
3131<dd> <b>Side Effects</b> None
3132<p>
3133
3134<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>
3135
3136<dt><pre>
3137<A NAME="ReadByteBinary"></A>
3138static int <I></I>
3139<B>ReadByteBinary</B>(
3140  FILE * <b>fp</b>, <i>IN: file where to read the byte</i>
3141  unsigned char * <b>cp</b> <i>OUT: the read byte</i>
3142)
3143</pre>
3144<dd> inputs a byte to file fp. 0x00 has been used as escape character
3145    to filter <CR>, <LF> and <ctrl-Z>. This is done for
3146    compatibility between unix and dos/windows systems.
3147<p>
3148
3149<dd> <b>Side Effects</b> None
3150<p>
3151
3152<dd> <b>See Also</b> <code><a href="#WriteByteBinary()">WriteByteBinary()</a>
3153</code>
3154
3155<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpBinary.c"TARGET="ABSTRACT"><CODE>dddmpBinary.c</CODE></A>
3156
3157<dt><pre>
3158<A NAME="RemoveFromUniqueRecurAdd"></A>
3159static void <I></I>
3160<B>RemoveFromUniqueRecurAdd</B>(
3161  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3162  DdNode * <b>f</b> <i>IN: root of the BDD to be extracted</i>
3163)
3164</pre>
3165<dd> Removes a node from the unique table by locating the proper
3166    subtable and unlinking the node from it. It recurs on the
3167    children of the node. Constants remain untouched.
3168<p>
3169
3170<dd> <b>Side Effects</b> Nodes are left with the "visited" flag true.
3171<p>
3172
3173<dd> <b>See Also</b> <code><a href="#RestoreInUniqueRecurAdd">RestoreInUniqueRecurAdd</a>
3174()
3175</code>
3176
3177<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>
3178
3179<dt><pre>
3180<A NAME="RemoveFromUniqueRecurBdd"></A>
3181static void <I></I>
3182<B>RemoveFromUniqueRecurBdd</B>(
3183  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3184  DdNode * <b>f</b> <i>IN: root of the BDD to be extracted</i>
3185)
3186</pre>
3187<dd> Removes a node from the unique table by locating the proper
3188    subtable and unlinking the node from it. It recurs on the
3189    children of the node. Constants remain untouched.
3190<p>
3191
3192<dd> <b>Side Effects</b> Nodes are left with the "visited" flag true.
3193<p>
3194
3195<dd> <b>See Also</b> <code><a href="#RestoreInUniqueRecurBdd">RestoreInUniqueRecurBdd</a>
3196()
3197</code>
3198
3199<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>
3200
3201<dt><pre>
3202<A NAME="RemoveFromUniqueRecurCnf"></A>
3203static void <I></I>
3204<B>RemoveFromUniqueRecurCnf</B>(
3205  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3206  DdNode * <b>f</b> <i>IN: root of the BDD to be extracted</i>
3207)
3208</pre>
3209<dd> Removes a node from the unique table by locating the proper
3210    subtable and unlinking the node from it. It recurs on  on the
3211    children of the node. Constants remain untouched.
3212<p>
3213
3214<dd> <b>Side Effects</b> Nodes are left with the "visited" flag true.
3215<p>
3216
3217<dd> <b>See Also</b> <code><a href="#RestoreInUniqueRecurCnf()">RestoreInUniqueRecurCnf()</a>
3218</code>
3219
3220<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
3221
3222<dt><pre>
3223<A NAME="RemoveFromUniqueRecurCnf"></A>
3224static void <I></I>
3225<B>RemoveFromUniqueRecurCnf</B>(
3226  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3227  DdNode * <b>f</b> <i>IN: root of the BDD to be extracted</i>
3228)
3229</pre>
3230<dd> Removes a node from the unique table by locating the proper
3231    subtable and unlinking the node from it. It recurs on son nodes.
3232<p>
3233
3234<dd> <b>Side Effects</b> Nodes are left with the "visited" flag true.
3235<p>
3236
3237<dd> <b>See Also</b> <code><a href="#RestoreInUniqueRecurCnf()">RestoreInUniqueRecurCnf()</a>
3238</code>
3239
3240<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
3241
3242<dt><pre>
3243<A NAME="RemoveFromUniqueRecur"></A>
3244static void <I></I>
3245<B>RemoveFromUniqueRecur</B>(
3246  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3247  DdNode * <b>f</b> <i>IN: root of the BDD to be extracted</i>
3248)
3249</pre>
3250<dd> Removes a node from the unique table by locating the proper
3251    subtable and unlinking the node from it. It recurs on the
3252    children of the node.
3253<p>
3254
3255<dd> <b>Side Effects</b> Nodes are left with the "visited" flag true.
3256<p>
3257
3258<dd> <b>See Also</b> <code><a href="#RestoreInUniqueRecur()">RestoreInUniqueRecur()</a>
3259</code>
3260
3261<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>
3262
3263<dt><pre>
3264<A NAME="RestoreInUniqueRecurAdd"></A>
3265static void <I></I>
3266<B>RestoreInUniqueRecurAdd</B>(
3267  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3268  DdNode * <b>f</b> <i>IN: root of the BDD to be restored</i>
3269)
3270</pre>
3271<dd> Restores a node in unique table (recursively)
3272<p>
3273
3274<dd> <b>Side Effects</b> Nodes are not restored in the same order as before removal
3275<p>
3276
3277<dd> <b>See Also</b> <code><a href="#RemoveFromUniqueAdd">RemoveFromUniqueAdd</a>
3278()
3279</code>
3280
3281<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>
3282
3283<dt><pre>
3284<A NAME="RestoreInUniqueRecurBdd"></A>
3285static void <I></I>
3286<B>RestoreInUniqueRecurBdd</B>(
3287  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3288  DdNode * <b>f</b> <i>IN: root of the BDD to be restored</i>
3289)
3290</pre>
3291<dd> Restores a node in unique table (recursively)
3292<p>
3293
3294<dd> <b>Side Effects</b> Nodes are not restored in the same order as before removal
3295<p>
3296
3297<dd> <b>See Also</b> <code><a href="#RemoveFromUnique()">RemoveFromUnique()</a>
3298</code>
3299
3300<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>
3301
3302<dt><pre>
3303<A NAME="RestoreInUniqueRecurCnf"></A>
3304static void <I></I>
3305<B>RestoreInUniqueRecurCnf</B>(
3306  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3307  DdNode * <b>f</b> <i>IN: root of the BDD to be restored</i>
3308)
3309</pre>
3310<dd> Restores a node in unique table (recursive)
3311<p>
3312
3313<dd> <b>Side Effects</b> Nodes are not restored in the same order as before removal
3314<p>
3315
3316<dd> <b>See Also</b> <code><a href="#RemoveFromUnique()">RemoveFromUnique()</a>
3317</code>
3318
3319<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>
3320
3321<dt><pre>
3322<A NAME="RestoreInUniqueRecurCnf"></A>
3323static void <I></I>
3324<B>RestoreInUniqueRecurCnf</B>(
3325  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3326  DdNode * <b>f</b> <i>IN: root of the BDD to be restored</i>
3327)
3328</pre>
3329<dd> Restores a node in unique table (recursive)
3330<p>
3331
3332<dd> <b>Side Effects</b> Nodes are not restored in the same order as before removal
3333<p>
3334
3335<dd> <b>See Also</b> <code><a href="#RemoveFromUnique()">RemoveFromUnique()</a>
3336</code>
3337
3338<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>
3339
3340<dt><pre>
3341<A NAME="RestoreInUniqueRecur"></A>
3342static void <I></I>
3343<B>RestoreInUniqueRecur</B>(
3344  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3345  DdNode * <b>f</b> <i>IN: root of the BDD to be restored</i>
3346)
3347</pre>
3348<dd> Restores a node in unique table (recursively)
3349<p>
3350
3351<dd> <b>Side Effects</b> Nodes are not restored in the same order as before removal
3352<p>
3353
3354<dd> <b>See Also</b> <code><a href="#RemoveFromUnique()">RemoveFromUnique()</a>
3355</code>
3356
3357<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>
3358
3359<dt><pre>
3360<A NAME="StoreCnfBestNotSharedRecur"></A>
3361static int <I></I>
3362<B>StoreCnfBestNotSharedRecur</B>(
3363  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3364  DdNode * <b>node</b>, <i>IN: BDD to store</i>
3365  int  <b>idf</b>, <i>IN: Id to store</i>
3366  int * <b>bddIds</b>, <i>IN: BDD identifiers</i>
3367  int * <b>cnfIds</b>, <i>IN: corresponding CNF identifiers</i>
3368  FILE * <b>fp</b>, <i>IN: file pointer</i>
3369  int * <b>list</b>, <i>IN: temporary array to store cubes</i>
3370  int * <b>clauseN</b>, <i>OUT: number of stored clauses</i>
3371  int * <b>varMax</b> <i>OUT: maximum identifier of the variables created</i>
3372)
3373</pre>
3374<dd> Performs the recursive step of Print Best on Not Shared
3375    sub-BDDs, i.e., print out information for the nodes belonging to
3376    BDDs not shared (whose root has just one incoming edge).
3377<p>
3378
3379<dd> <b>Side Effects</b> None
3380<p>
3381
3382<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>
3383
3384<dt><pre>
3385<A NAME="StoreCnfBestSharedRecur"></A>
3386static int <I></I>
3387<B>StoreCnfBestSharedRecur</B>(
3388  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3389  DdNode * <b>node</b>, <i>IN: BDD to store</i>
3390  int * <b>bddIds</b>, <i>IN: BDD identifiers</i>
3391  int * <b>cnfIds</b>, <i>IN: corresponding CNF identifiers</i>
3392  FILE * <b>fp</b>, <i>IN: file pointer</i>
3393  int * <b>list</b>, <i>IN: temporary array to store cubes</i>
3394  int * <b>clauseN</b>, <i>OUT: number of stored clauses</i>
3395  int * <b>varMax</b> <i>OUT: maximum identifier of the variables created</i>
3396)
3397</pre>
3398<dd> Performs the recursive step of Print Best on Not Shared
3399    sub-BDDs, i.e., print out information for the nodes belonging to
3400    BDDs not shared (whose root has just one incoming edge).
3401<p>
3402
3403<dd> <b>Side Effects</b> None
3404<p>
3405
3406<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>
3407
3408<dt><pre>
3409<A NAME="StoreCnfBest"></A>
3410static int <I></I>
3411<B>StoreCnfBest</B>(
3412  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3413  DdNode ** <b>f</b>, <i>IN: array of BDDs to store</i>
3414  int  <b>rootN</b>, <i>IN: number of BDD in the array</i>
3415  int * <b>bddIds</b>, <i>IN: BDD identifiers</i>
3416  int * <b>cnfIds</b>, <i>IN: corresponding CNF identifiers</i>
3417  int  <b>idInitial</b>, <i>IN: initial value for numbering new CNF variables</i>
3418  FILE * <b>fp</b>, <i>IN: file pointer</i>
3419  int * <b>varMax</b>, <i>OUT: maximum identifier of the variables created</i>
3420  int * <b>clauseN</b>, <i>OUT: number of stored clauses</i>
3421  int * <b>rootStartLine</b> <i>OUT: line where root starts</i>
3422)
3423</pre>
3424<dd> Prints a disjoint sum of product cover for the function
3425    rooted at node intorducing cutting points whenever necessary.
3426    Each product corresponds to a path from node a leaf
3427    node different from the logical zero, and different from the
3428    background value. Uses the standard output.  Returns 1 if
3429    successful, 0 otherwise.
3430<p>
3431
3432<dd> <b>Side Effects</b> None
3433<p>
3434
3435<dd> <b>See Also</b> <code><a href="#StoreCnfMaxtermByMaxterm">StoreCnfMaxtermByMaxterm</a>
3436</code>
3437
3438<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>
3439
3440<dt><pre>
3441<A NAME="StoreCnfMaxtermByMaxtermRecur"></A>
3442static void <I></I>
3443<B>StoreCnfMaxtermByMaxtermRecur</B>(
3444  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3445  DdNode * <b>node</b>, <i>IN: BDD to store</i>
3446  int * <b>bddIds</b>, <i>IN: BDD identifiers</i>
3447  int * <b>cnfIds</b>, <i>IN: corresponding CNF identifiers</i>
3448  FILE * <b>fp</b>, <i>IN: file pointer</i>
3449  int * <b>list</b>, <i>IN: temporary array to store cubes</i>
3450  int * <b>clauseN</b>, <i>OUT: number of stored clauses</i>
3451  int * <b>varMax</b> <i>OUT: maximum identifier of the variables created</i>
3452)
3453</pre>
3454<dd> Performs the recursive step of Print Maxterm.
3455    Traverse a BDD a print out a cube in CNF format each time a terminal
3456    node is reached.
3457<p>
3458
3459<dd> <b>Side Effects</b> None
3460<p>
3461
3462<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>
3463
3464<dt><pre>
3465<A NAME="StoreCnfMaxtermByMaxterm"></A>
3466static int <I></I>
3467<B>StoreCnfMaxtermByMaxterm</B>(
3468  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3469  DdNode ** <b>f</b>, <i>IN: array of BDDs to store</i>
3470  int  <b>rootN</b>, <i>IN: number of BDDs in the array</i>
3471  int * <b>bddIds</b>, <i>IN: BDD Identifiers</i>
3472  int * <b>cnfIds</b>, <i>IN: corresponding CNF Identifiers</i>
3473  int  <b>idInitial</b>, <i>IN: initial value for numbering new CNF variables</i>
3474  FILE * <b>fp</b>, <i>IN: file pointer</i>
3475  int * <b>varMax</b>, <i>OUT: maximum identifier of the variables created</i>
3476  int * <b>clauseN</b>, <i>OUT: number of stored clauses</i>
3477  int * <b>rootStartLine</b> <i>OUT: line where root starts</i>
3478)
3479</pre>
3480<dd> Prints a disjoint sum of product cover for the function
3481    rooted at node. Each product corresponds to a path from node a
3482    leaf node different from the logical zero, and different from
3483    the background value. Uses the standard output.  Returns 1 if
3484    successful, 0 otherwise.
3485<p>
3486
3487<dd> <b>Side Effects</b> None
3488<p>
3489
3490<dd> <b>See Also</b> <code><a href="#StoreCnfBest">StoreCnfBest</a>
3491</code>
3492
3493<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>
3494
3495<dt><pre>
3496<A NAME="StoreCnfNodeByNodeRecur"></A>
3497static int <I></I>
3498<B>StoreCnfNodeByNodeRecur</B>(
3499  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3500  DdNode * <b>f</b>, <i>IN: BDD node to be stored</i>
3501  int * <b>bddIds</b>, <i>IN: BDD ids for variables</i>
3502  int * <b>cnfIds</b>, <i>IN: CNF ids for variables</i>
3503  FILE * <b>fp</b>, <i>IN: store file</i>
3504  int * <b>clauseN</b>, <i>OUT: number of clauses written in the CNF file</i>
3505  int * <b>varMax</b> <i>OUT: maximum value of id written in the CNF file</i>
3506)
3507</pre>
3508<dd> Performs the recursive step of Dddmp_bddStore.
3509    Traverse the BDD and store a CNF formula for each "terminal" node.
3510<p>
3511
3512<dd> <b>Side Effects</b> None
3513<p>
3514
3515<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>
3516
3517<dt><pre>
3518<A NAME="StoreCnfNodeByNode"></A>
3519static int <I></I>
3520<B>StoreCnfNodeByNode</B>(
3521  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3522  DdNode ** <b>f</b>, <i>IN: BDD array to be stored</i>
3523  int  <b>rootN</b>, <i>IN: number of BDDs in the array</i>
3524  int * <b>bddIds</b>, <i>IN: BDD ids for variables</i>
3525  int * <b>cnfIds</b>, <i>IN: CNF ids for variables</i>
3526  FILE * <b>fp</b>, <i>IN: store file</i>
3527  int * <b>clauseN</b>, <i>IN/OUT: number of clauses written in the CNF file</i>
3528  int * <b>varMax</b>, <i>IN/OUT: maximum value of id written in the CNF file</i>
3529  int * <b>rootStartLine</b> <i>OUT: CNF line where root starts</i>
3530)
3531</pre>
3532<dd> Store the BDD as CNF clauses.
3533    Use a multiplexer description for each BDD node.
3534<p>
3535
3536<dd> <b>Side Effects</b> None
3537<p>
3538
3539<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>
3540
3541<dt><pre>
3542<A NAME="StoreCnfOneNode"></A>
3543static int <I></I>
3544<B>StoreCnfOneNode</B>(
3545  DdNode * <b>f</b>, <i>IN: node to be stored</i>
3546  int  <b>idf</b>, <i>IN: node CNF Index</i>
3547  int  <b>vf</b>, <i>IN: node BDD Index</i>
3548  int  <b>idT</b>, <i>IN: Then CNF Index with sign = inverted edge</i>
3549  int  <b>idE</b>, <i>IN: Else CNF Index with sign = inverted edge</i>
3550  FILE * <b>fp</b>, <i>IN: store file</i>
3551  int * <b>clauseN</b>, <i>OUT: number of clauses</i>
3552  int * <b>varMax</b> <i>OUT: maximun Index of variable stored</i>
3553)
3554</pre>
3555<dd> Store One Single BDD Node translating it as a multiplexer.
3556<p>
3557
3558<dd> <b>Side Effects</b> None
3559<p>
3560
3561<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>
3562
3563<dt><pre>
3564<A NAME="WriteByteBinary"></A>
3565static int <I></I>
3566<B>WriteByteBinary</B>(
3567  FILE * <b>fp</b>, <i>IN: file where to write the byte</i>
3568  unsigned char  <b>c</b> <i>IN: the byte to be written</i>
3569)
3570</pre>
3571<dd> outputs a byte to file fp. Uses 0x00 as escape character
3572    to filter <CR>, <LF> and <ctrl-Z>.
3573    This is done for compatibility between unix and dos/windows systems.
3574<p>
3575
3576<dd> <b>Side Effects</b> None
3577<p>
3578
3579<dd> <b>See Also</b> <code><a href="#ReadByteBinary()">ReadByteBinary()</a>
3580</code>
3581
3582<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpBinary.c"TARGET="ABSTRACT"><CODE>dddmpBinary.c</CODE></A>
3583
3584<dt><pre>
3585<A NAME="printCubeCnf"></A>
3586static int <I></I>
3587<B>printCubeCnf</B>(
3588  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
3589  DdNode * <b>node</b>, <i>IN: BDD to store</i>
3590  int * <b>cnfIds</b>, <i>IN: CNF identifiers</i>
3591  FILE * <b>fp</b>, <i>IN: file pointer</i>
3592  int * <b>list</b>, <i>IN: temporary array to store cubes</i>
3593  int * <b>varMax</b> <i>OUT: maximum identifier of the variables created</i>
3594)
3595</pre>
3596<dd> Print One Cube in CNF Format.
3597    Return DDDMP_SUCCESS if something is printed out, DDDMP_FAILURE
3598    is nothing is printed out.
3599<p>
3600
3601<dd> <b>Side Effects</b> None
3602<p>
3603
3604<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>
3605
3606<dt><pre>
3607<A NAME=""></A>
3608 <I></I>
3609<B></B>(
3610   <b></b> <i></i>
3611)
3612</pre>
3613<dd> Checks for Warnings: If expr==1 it prints out the warning
3614    on stderr.
3615<p>
3616
3617<dd> <b>Side Effects</b> None
3618<p>
3619
3620<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmp.h"TARGET="ABSTRACT"><CODE>dddmp.h</CODE></A>
3621
3622<dt><pre>
3623<A NAME=""></A>
3624 <I></I>
3625<B></B>(
3626   <b></b> <i></i>
3627)
3628</pre>
3629<dd> Checks for fatal bugs and go to the label to deal with
3630    the error.
3631<p>
3632
3633<dd> <b>Side Effects</b> None
3634<p>
3635
3636<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmp.h"TARGET="ABSTRACT"><CODE>dddmp.h</CODE></A>
3637
3638<dt><pre>
3639<A NAME=""></A>
3640 <I></I>
3641<B></B>(
3642   <b></b> <i></i>
3643)
3644</pre>
3645<dd> Checks for fatal bugs and return the DDDMP_FAILURE flag.
3646<p>
3647
3648<dd> <b>Side Effects</b> None
3649<p>
3650
3651<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmp.h"TARGET="ABSTRACT"><CODE>dddmp.h</CODE></A>
3652
3653<dt><pre>
3654<A NAME=""></A>
3655 <I></I>
3656<B></B>(
3657   <b></b> <i></i>
3658)
3659</pre>
3660<dd> Conditional safety assertion. It prints out the file
3661    name and line number where the fatal error occurred.
3662    Messages are printed out on stderr.
3663<p>
3664
3665<dd> <b>Side Effects</b> None
3666<p>
3667
3668<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmp.h"TARGET="ABSTRACT"><CODE>dddmp.h</CODE></A>
3669
3670<dt><pre>
3671<A NAME=""></A>
3672 <I></I>
3673<B></B>(
3674   <b></b> <i></i>
3675)
3676</pre>
3677<dd> Memory Allocation Macro for DDDMP
3678<p>
3679
3680<dd> <b>Side Effects</b> None
3681<p>
3682
3683<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpInt.h"TARGET="ABSTRACT"><CODE>dddmpInt.h</CODE></A>
3684
3685<dt><pre>
3686<A NAME=""></A>
3687 <I></I>
3688<B></B>(
3689   <b></b> <i></i>
3690)
3691</pre>
3692<dd> Memory Free Macro for DDDMP
3693<p>
3694
3695<dd> <b>Side Effects</b> None
3696<p>
3697
3698<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpInt.h"TARGET="ABSTRACT"><CODE>dddmpInt.h</CODE></A>
3699
3700
3701</DL>
3702<HR>
3703Last updated on 1040218 17h14
3704</BODY></HTML>
Note: See TracBrowser for help on using the repository browser.