source: icGREP/icgrep-devel/cudd-2.5.1/dddmp/doc/dddmpAllFile.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: 31.4 KB
Line 
1<HTML>
2<HEAD><TITLE>The dddmp package: files</TITLE></HEAD>
3<BODY>
4
5<DL>
6 <DT> <A HREF="#dddmp.h"><CODE>dddmp.h</CODE></A>
7 <DD> External header file
8 <DT> <A HREF="#dddmpInt.h"><CODE>dddmpInt.h</CODE></A>
9 <DD> Internal header file
10 <DT> <A HREF="#dddmpBinary.c"><CODE>dddmpBinary.c</CODE></A>
11 <DD> Input and output BDD codes and integers from/to file
12 <DT> <A HREF="#dddmpConvert.c"><CODE>dddmpConvert.c</CODE></A>
13 <DD> Conversion between ASCII and binary formats
14 <DT> <A HREF="#dddmpDbg.c"><CODE>dddmpDbg.c</CODE></A>
15 <DD> Functions to display BDD files
16 <DT> <A HREF="#dddmpDdNodeBdd.c"><CODE>dddmpDdNodeBdd.c</CODE></A>
17 <DD> Functions to handle BDD node infos and numbering
18 <DT> <A HREF="#dddmpDdNodeCnf.c"><CODE>dddmpDdNodeCnf.c</CODE></A>
19 <DD> Functions to handle BDD node infos and numbering
20    while storing a CNF formula from a BDD or an array of BDDs
21 <DT> <A HREF="#dddmpLoad.c"><CODE>dddmpLoad.c</CODE></A>
22 <DD> Functions to read in bdds to file
23 <DT> <A HREF="#dddmpLoadCnf.c"><CODE>dddmpLoadCnf.c</CODE></A>
24 <DD> Functions to read in CNF from file as BDDs.
25 <DT> <A HREF="#dddmpNodeAdd.c"><CODE>dddmpNodeAdd.c</CODE></A>
26 <DD> Functions to handle ADD node infos and numbering
27 <DT> <A HREF="#dddmpNodeBdd.c"><CODE>dddmpNodeBdd.c</CODE></A>
28 <DD> Functions to handle BDD node infos and numbering
29 <DT> <A HREF="#dddmpNodeCnf.c"><CODE>dddmpNodeCnf.c</CODE></A>
30 <DD> Functions to handle BDD node infos and numbering
31    while storing a CNF formula from a BDD or an array of BDDs
32 <DT> <A HREF="#dddmpStoreAdd.c"><CODE>dddmpStoreAdd.c</CODE></A>
33 <DD> Functions to write ADDs to file.
34 <DT> <A HREF="#dddmpStoreBdd.c"><CODE>dddmpStoreBdd.c</CODE></A>
35 <DD> Functions to write BDDs to file.
36 <DT> <A HREF="#dddmpStoreCnf.c"><CODE>dddmpStoreCnf.c</CODE></A>
37 <DD> Functions to write out BDDs to file in a CNF format
38 <DT> <A HREF="#dddmpStoreMisc.c"><CODE>dddmpStoreMisc.c</CODE></A>
39 <DD> Functions to write out bdds to file in prefixed
40    and in Blif form.
41 <DT> <A HREF="#dddmpUtil.c"><CODE>dddmpUtil.c</CODE></A>
42 <DD> Util Functions for the dddmp package
43</DL><HR>
44<A NAME="dddmp.h"><H1>dddmp.h</H1></A>
45External header file <P>
46<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
47<DL>
48 <DT> <A HREF="dddmpAllDet.html#" TARGET="MAIN"><CODE>()</CODE></A>
49 <DD> Checks for fatal bugs
50
51 <DT> <A HREF="dddmpAllDet.html#" TARGET="MAIN"><CODE>()</CODE></A>
52 <DD> Checks for Warnings: If expr==1 it prints out the warning
53    on stderr.
54
55 <DT> <A HREF="dddmpAllDet.html#" TARGET="MAIN"><CODE>()</CODE></A>
56 <DD> Checks for fatal bugs and return the DDDMP_FAILURE flag.
57
58 <DT> <A HREF="dddmpAllDet.html#" TARGET="MAIN"><CODE>()</CODE></A>
59 <DD> Checks for fatal bugs and go to the label to deal with
60    the error.
61
62</DL>
63<HR>
64<A NAME="dddmpInt.h"><H1>dddmpInt.h</H1></A>
65Internal header file <P>
66<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
67<DL>
68 <DT> <A HREF="dddmpAllDet.html#" TARGET="MAIN"><CODE>()</CODE></A>
69 <DD> Memory Allocation Macro for DDDMP
70
71 <DT> <A HREF="dddmpAllDet.html#" TARGET="MAIN"><CODE>()</CODE></A>
72 <DD> Memory Free Macro for DDDMP
73
74</DL>
75<HR>
76<A NAME="dddmpBinary.c"><H1>dddmpBinary.c</H1></A>
77Input and output BDD codes and integers from/to file <P>
78<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
79Input and output BDD codes and integers from/to file
80    in binary mode.
81    DD node codes are written as one byte.
82    Integers of any length are written as sequences of "linked" bytes.
83    For each byte 7 bits are used for data and one (MSBit) as link with
84    a further byte (MSB = 1 means one more byte).
85    Low level read/write of bytes filter <CR>, <LF> and <ctrl-Z>
86    with escape sequences. <P>
87<DL>
88 <DT> <A HREF="dddmpAllDet.html#DddmpWriteCode" TARGET="MAIN"><CODE>DddmpWriteCode()</CODE></A>
89 <DD> Writes 1 byte node code
90
91 <DT> <A HREF="dddmpAllDet.html#DddmpReadCode" TARGET="MAIN"><CODE>DddmpReadCode()</CODE></A>
92 <DD> Reads a 1 byte node code
93
94 <DT> <A HREF="dddmpAllDet.html#DddmpWriteInt" TARGET="MAIN"><CODE>DddmpWriteInt()</CODE></A>
95 <DD> Writes a "packed integer"
96
97 <DT> <A HREF="dddmpAllDet.html#DddmpReadInt" TARGET="MAIN"><CODE>DddmpReadInt()</CODE></A>
98 <DD> Reads a "packed integer"
99
100 <DT> <A HREF="dddmpAllDet.html#WriteByteBinary" TARGET="MAIN"><CODE>WriteByteBinary()</CODE></A>
101 <DD> Writes a byte to file filtering <CR>, <LF> and <ctrl-Z>
102
103 <DT> <A HREF="dddmpAllDet.html#ReadByteBinary" TARGET="MAIN"><CODE>ReadByteBinary()</CODE></A>
104 <DD> Reads a byte from file with escaped <CR>, <LF> and <ctrl-Z>
105
106</DL>
107<HR>
108<A NAME="dddmpConvert.c"><H1>dddmpConvert.c</H1></A>
109Conversion between ASCII and binary formats <P>
110<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
111Conversion between ASCII and binary formats is presently
112    supported by loading a BDD in the source format and storing it
113    in the target one. We plan to introduce ad hoc procedures
114    avoiding explicit BDD node generation. <P>
115<DL>
116 <DT> <A HREF="dddmpAllDet.html#Dddmp_Text2Bin" TARGET="MAIN"><CODE>Dddmp_Text2Bin()</CODE></A>
117 <DD> Converts from ASCII to binary format
118
119 <DT> <A HREF="dddmpAllDet.html#Dddmp_Bin2Text" TARGET="MAIN"><CODE>Dddmp_Bin2Text()</CODE></A>
120 <DD> Converts from binary to ASCII format
121
122</DL>
123<HR>
124<A NAME="dddmpDbg.c"><H1>dddmpDbg.c</H1></A>
125Functions to display BDD files <P>
126<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
127Functions to display BDD files in binary format <P>
128<DL>
129 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddDisplayBinary" TARGET="MAIN"><CODE>Dddmp_cuddBddDisplayBinary()</CODE></A>
130 <DD> Display a binary dump file in a text file
131
132</DL>
133<HR>
134<A NAME="dddmpDdNodeBdd.c"><H1>dddmpDdNodeBdd.c</H1></A>
135Functions to handle BDD node infos and numbering <P>
136<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
137Functions to handle BDD node infos and numbering. <P>
138<DL>
139 <DT> <A HREF="dddmpAllDet.html#DddmpNumberDdNodes" TARGET="MAIN"><CODE>DddmpNumberDdNodes()</CODE></A>
140 <DD> Removes nodes from unique table and number them
141
142 <DT> <A HREF="dddmpAllDet.html#DddmpUnnumberDdNodes" TARGET="MAIN"><CODE>DddmpUnnumberDdNodes()</CODE></A>
143 <DD> Restores nodes in unique table, loosing numbering
144
145 <DT> <A HREF="dddmpAllDet.html#DddmpWriteNodeIndex" TARGET="MAIN"><CODE>DddmpWriteNodeIndex()</CODE></A>
146 <DD> Write index to node
147
148 <DT> <A HREF="dddmpAllDet.html#DddmpReadNodeIndex" TARGET="MAIN"><CODE>DddmpReadNodeIndex()</CODE></A>
149 <DD> Reads the index of a node
150
151 <DT> <A HREF="dddmpAllDet.html#DddmpVisited" TARGET="MAIN"><CODE>DddmpVisited()</CODE></A>
152 <DD> Returns true if node is visited
153
154 <DT> <A HREF="dddmpAllDet.html#DddmpSetVisited" TARGET="MAIN"><CODE>DddmpSetVisited()</CODE></A>
155 <DD> Marks a node as visited
156
157 <DT> <A HREF="dddmpAllDet.html#DddmpClearVisited" TARGET="MAIN"><CODE>DddmpClearVisited()</CODE></A>
158 <DD> Marks a node as not visited
159
160 <DT> <A HREF="dddmpAllDet.html#NumberNodeRecur" TARGET="MAIN"><CODE>NumberNodeRecur()</CODE></A>
161 <DD> Number nodes recursively in post-order
162
163 <DT> <A HREF="dddmpAllDet.html#RemoveFromUniqueRecur" TARGET="MAIN"><CODE>RemoveFromUniqueRecur()</CODE></A>
164 <DD> Removes a node from unique table
165
166 <DT> <A HREF="dddmpAllDet.html#RestoreInUniqueRecur" TARGET="MAIN"><CODE>RestoreInUniqueRecur()</CODE></A>
167 <DD> Restores a node in unique table
168
169</DL>
170<HR>
171<A NAME="dddmpDdNodeCnf.c"><H1>dddmpDdNodeCnf.c</H1></A>
172Functions to handle BDD node infos and numbering
173    while storing a CNF formula from a BDD or an array of BDDs <P>
174<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
175Functions to handle BDD node infos and numbering
176    while storing a CNF formula from a BDD or an array of BDDs. <P>
177<DL>
178 <DT> <A HREF="dddmpAllDet.html#DddmpNumberDdNodesCnf" TARGET="MAIN"><CODE>DddmpNumberDdNodesCnf()</CODE></A>
179 <DD> Removes nodes from unique table and numbers them
180
181 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesCountEdgesAndNumber" TARGET="MAIN"><CODE>DddmpDdNodesCountEdgesAndNumber()</CODE></A>
182 <DD> Removes nodes from unique table and numbers each node according
183    to the number of its incoming BDD edges.
184
185 <DT> <A HREF="dddmpAllDet.html#DddmpUnnumberDdNodesCnf" TARGET="MAIN"><CODE>DddmpUnnumberDdNodesCnf()</CODE></A>
186 <DD> Restores nodes in unique table, loosing numbering
187
188 <DT> <A HREF="dddmpAllDet.html#DddmpPrintBddAndNext" TARGET="MAIN"><CODE>DddmpPrintBddAndNext()</CODE></A>
189 <DD> Prints debug information
190
191 <DT> <A HREF="dddmpAllDet.html#DddmpWriteNodeIndexCnfBis" TARGET="MAIN"><CODE>DddmpWriteNodeIndexCnfBis()</CODE></A>
192 <DD> Write index to node
193
194 <DT> <A HREF="dddmpAllDet.html#DddmpWriteNodeIndexCnf" TARGET="MAIN"><CODE>DddmpWriteNodeIndexCnf()</CODE></A>
195 <DD> Write index to node
196
197 <DT> <A HREF="dddmpAllDet.html#DddmpReadNodeIndexCnf" TARGET="MAIN"><CODE>DddmpReadNodeIndexCnf()</CODE></A>
198 <DD> Reads the index of a node
199
200 <DT> <A HREF="dddmpAllDet.html#DddmpClearVisitedCnfRecur" TARGET="MAIN"><CODE>DddmpClearVisitedCnfRecur()</CODE></A>
201 <DD> Mark ALL nodes as not visited
202
203 <DT> <A HREF="dddmpAllDet.html#DddmpVisitedCnf" TARGET="MAIN"><CODE>DddmpVisitedCnf()</CODE></A>
204 <DD> Returns true if node is visited
205
206 <DT> <A HREF="dddmpAllDet.html#DddmpSetVisitedCnf" TARGET="MAIN"><CODE>DddmpSetVisitedCnf()</CODE></A>
207 <DD> Marks a node as visited
208
209 <DT> <A HREF="dddmpAllDet.html#DddmpClearVisitedCnf" TARGET="MAIN"><CODE>DddmpClearVisitedCnf()</CODE></A>
210 <DD> Marks a node as not visited
211
212 <DT> <A HREF="dddmpAllDet.html#NumberNodeRecurCnf" TARGET="MAIN"><CODE>NumberNodeRecurCnf()</CODE></A>
213 <DD> Number nodes recursively in post-order
214
215 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesCheckIncomingAndScanPath" TARGET="MAIN"><CODE>DddmpDdNodesCheckIncomingAndScanPath()</CODE></A>
216 <DD> Number nodes recursively in post-order
217
218 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesNumberEdgesRecur" TARGET="MAIN"><CODE>DddmpDdNodesNumberEdgesRecur()</CODE></A>
219 <DD> Number nodes recursively in post-order
220
221 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesResetCountRecur" TARGET="MAIN"><CODE>DddmpDdNodesResetCountRecur()</CODE></A>
222 <DD> Resets counter and visited flag for ALL nodes of a BDD
223
224 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesCountEdgesRecur" TARGET="MAIN"><CODE>DddmpDdNodesCountEdgesRecur()</CODE></A>
225 <DD> Counts the number of incoming edges for each node of a BDD
226
227 <DT> <A HREF="dddmpAllDet.html#RemoveFromUniqueRecurCnf" TARGET="MAIN"><CODE>RemoveFromUniqueRecurCnf()</CODE></A>
228 <DD> Removes a node from unique table
229
230 <DT> <A HREF="dddmpAllDet.html#RestoreInUniqueRecurCnf" TARGET="MAIN"><CODE>RestoreInUniqueRecurCnf()</CODE></A>
231 <DD> Restores a node in unique table
232
233 <DT> <A HREF="dddmpAllDet.html#DddmpPrintBddAndNextRecur" TARGET="MAIN"><CODE>DddmpPrintBddAndNextRecur()</CODE></A>
234 <DD> Prints debug info
235
236</DL>
237<HR>
238<A NAME="dddmpLoad.c"><H1>dddmpLoad.c</H1></A>
239Functions to read in bdds to file <P>
240<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
241Functions to read in bdds to file.  BDDs
242    are represended on file either in text or binary format under the
243    following rules.  A file contains a forest of BDDs (a vector of
244    Boolean functions).  BDD nodes are numbered with contiguous numbers,
245    from 1 to NNodes (total number of nodes on a file). 0 is not used to
246    allow negative node indexes for complemented edges.  A file contains
247    a header, including information about variables and roots to BDD
248    functions, followed by the list of nodes.  BDD nodes are listed
249    according to their numbering, and in the present implementation
250    numbering follows a post-order strategy, in such a way that a node
251    is never listed before its Then/Else children. <P>
252<DL>
253 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddLoad" TARGET="MAIN"><CODE>Dddmp_cuddBddLoad()</CODE></A>
254 <DD> Reads a dump file representing the argument BDD.
255
256 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddArrayLoad" TARGET="MAIN"><CODE>Dddmp_cuddBddArrayLoad()</CODE></A>
257 <DD> Reads a dump file representing the argument BDDs.
258
259 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddAddLoad" TARGET="MAIN"><CODE>Dddmp_cuddAddLoad()</CODE></A>
260 <DD> Reads a dump file representing the argument ADD.
261
262 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddAddArrayLoad" TARGET="MAIN"><CODE>Dddmp_cuddAddArrayLoad()</CODE></A>
263 <DD> Reads a dump file representing the argument ADDs.
264
265 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddHeaderLoad" TARGET="MAIN"><CODE>Dddmp_cuddHeaderLoad()</CODE></A>
266 <DD> Reads the header of a dump file representing the argument BDDs
267
268 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayLoad" TARGET="MAIN"><CODE>DddmpCuddDdArrayLoad()</CODE></A>
269 <DD> Reads a dump file representing the argument BDDs.
270
271 <DT> <A HREF="dddmpAllDet.html#DddmpBddReadHeader" TARGET="MAIN"><CODE>DddmpBddReadHeader()</CODE></A>
272 <DD> Reads a the header of a dump file representing the
273    argument BDDs.
274
275 <DT> <A HREF="dddmpAllDet.html#DddmpFreeHeader" TARGET="MAIN"><CODE>DddmpFreeHeader()</CODE></A>
276 <DD> Frees the internal header structure.
277
278</DL>
279<HR>
280<A NAME="dddmpLoadCnf.c"><H1>dddmpLoadCnf.c</H1></A>
281Functions to read in CNF from file as BDDs. <P>
282<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
283Functions to read in CNF from file as BDDs. <P>
284<DL>
285 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddLoadCnf" TARGET="MAIN"><CODE>Dddmp_cuddBddLoadCnf()</CODE></A>
286 <DD> Reads a dump file in a CNF format.
287
288 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddArrayLoadCnf" TARGET="MAIN"><CODE>Dddmp_cuddBddArrayLoadCnf()</CODE></A>
289 <DD> Reads a dump file in a CNF format.
290
291 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddHeaderLoadCnf" TARGET="MAIN"><CODE>Dddmp_cuddHeaderLoadCnf()</CODE></A>
292 <DD> Reads the header of a dump file representing the argument BDDs
293
294 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayLoadCnf" TARGET="MAIN"><CODE>DddmpCuddDdArrayLoadCnf()</CODE></A>
295 <DD> Reads a dump file representing the argument BDDs in CNF
296     format.
297
298 <DT> <A HREF="dddmpAllDet.html#DddmpBddReadHeaderCnf" TARGET="MAIN"><CODE>DddmpBddReadHeaderCnf()</CODE></A>
299 <DD> Reads a the header of a dump file representing the argument
300    BDDs.
301
302 <DT> <A HREF="dddmpAllDet.html#DddmpFreeHeaderCnf" TARGET="MAIN"><CODE>DddmpFreeHeaderCnf()</CODE></A>
303 <DD> Frees the internal header structure.
304
305 <DT> <A HREF="dddmpAllDet.html#DddmpReadCnfClauses" TARGET="MAIN"><CODE>DddmpReadCnfClauses()</CODE></A>
306 <DD> Read the CNF clauses from the file in the standard DIMACS
307    format.
308
309 <DT> <A HREF="dddmpAllDet.html#DddmpCnfClauses2Bdd" TARGET="MAIN"><CODE>DddmpCnfClauses2Bdd()</CODE></A>
310 <DD> Transforms CNF clauses into BDDs.
311
312</DL>
313<HR>
314<A NAME="dddmpNodeAdd.c"><H1>dddmpNodeAdd.c</H1></A>
315Functions to handle ADD node infos and numbering <P>
316<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
317Functions to handle ADD node infos and numbering. <P>
318<DL>
319 <DT> <A HREF="dddmpAllDet.html#DddmpNumberAddNodes" TARGET="MAIN"><CODE>DddmpNumberAddNodes()</CODE></A>
320 <DD> Removes nodes from unique table and number them
321
322 <DT> <A HREF="dddmpAllDet.html#DddmpUnnumberAddNodes" TARGET="MAIN"><CODE>DddmpUnnumberAddNodes()</CODE></A>
323 <DD> Restores nodes in unique table, loosing numbering
324
325 <DT> <A HREF="dddmpAllDet.html#DddmpWriteNodeIndexAdd" TARGET="MAIN"><CODE>DddmpWriteNodeIndexAdd()</CODE></A>
326 <DD> Write index to node
327
328 <DT> <A HREF="dddmpAllDet.html#DddmpReadNodeIndexAdd" TARGET="MAIN"><CODE>DddmpReadNodeIndexAdd()</CODE></A>
329 <DD> Reads the index of a node
330
331 <DT> <A HREF="dddmpAllDet.html#DddmpVisitedAdd" TARGET="MAIN"><CODE>DddmpVisitedAdd()</CODE></A>
332 <DD> Returns true if node is visited
333
334 <DT> <A HREF="dddmpAllDet.html#DddmpSetVisitedAdd" TARGET="MAIN"><CODE>DddmpSetVisitedAdd()</CODE></A>
335 <DD> Marks a node as visited
336
337 <DT> <A HREF="dddmpAllDet.html#DddmpClearVisitedAdd" TARGET="MAIN"><CODE>DddmpClearVisitedAdd()</CODE></A>
338 <DD> Marks a node as not visited
339
340 <DT> <A HREF="dddmpAllDet.html#NumberNodeRecurAdd" TARGET="MAIN"><CODE>NumberNodeRecurAdd()</CODE></A>
341 <DD> Number nodes recursively in post-order
342
343 <DT> <A HREF="dddmpAllDet.html#RemoveFromUniqueRecurAdd" TARGET="MAIN"><CODE>RemoveFromUniqueRecurAdd()</CODE></A>
344 <DD> Removes a node from unique table
345
346 <DT> <A HREF="dddmpAllDet.html#RestoreInUniqueRecurAdd" TARGET="MAIN"><CODE>RestoreInUniqueRecurAdd()</CODE></A>
347 <DD> Restores a node in unique table
348
349</DL>
350<HR>
351<A NAME="dddmpNodeBdd.c"><H1>dddmpNodeBdd.c</H1></A>
352Functions to handle BDD node infos and numbering <P>
353<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
354Functions to handle BDD node infos and numbering. <P>
355<DL>
356 <DT> <A HREF="dddmpAllDet.html#DddmpNumberBddNodes" TARGET="MAIN"><CODE>DddmpNumberBddNodes()</CODE></A>
357 <DD> Removes nodes from unique table and number them
358
359 <DT> <A HREF="dddmpAllDet.html#DddmpUnnumberBddNodes" TARGET="MAIN"><CODE>DddmpUnnumberBddNodes()</CODE></A>
360 <DD> Restores nodes in unique table, loosing numbering
361
362 <DT> <A HREF="dddmpAllDet.html#DddmpWriteNodeIndexBdd" TARGET="MAIN"><CODE>DddmpWriteNodeIndexBdd()</CODE></A>
363 <DD> Write index to node
364
365 <DT> <A HREF="dddmpAllDet.html#DddmpReadNodeIndexBdd" TARGET="MAIN"><CODE>DddmpReadNodeIndexBdd()</CODE></A>
366 <DD> Reads the index of a node
367
368 <DT> <A HREF="dddmpAllDet.html#DddmpVisitedBdd" TARGET="MAIN"><CODE>DddmpVisitedBdd()</CODE></A>
369 <DD> Returns true if node is visited
370
371 <DT> <A HREF="dddmpAllDet.html#DddmpSetVisitedBdd" TARGET="MAIN"><CODE>DddmpSetVisitedBdd()</CODE></A>
372 <DD> Marks a node as visited
373
374 <DT> <A HREF="dddmpAllDet.html#DddmpClearVisitedBdd" TARGET="MAIN"><CODE>DddmpClearVisitedBdd()</CODE></A>
375 <DD> Marks a node as not visited
376
377 <DT> <A HREF="dddmpAllDet.html#NumberNodeRecurBdd" TARGET="MAIN"><CODE>NumberNodeRecurBdd()</CODE></A>
378 <DD> Number nodes recursively in post-order
379
380 <DT> <A HREF="dddmpAllDet.html#RemoveFromUniqueRecurBdd" TARGET="MAIN"><CODE>RemoveFromUniqueRecurBdd()</CODE></A>
381 <DD> Removes a node from unique table
382
383 <DT> <A HREF="dddmpAllDet.html#RestoreInUniqueRecurBdd" TARGET="MAIN"><CODE>RestoreInUniqueRecurBdd()</CODE></A>
384 <DD> Restores a node in unique table
385
386</DL>
387<HR>
388<A NAME="dddmpNodeCnf.c"><H1>dddmpNodeCnf.c</H1></A>
389Functions to handle BDD node infos and numbering
390    while storing a CNF formula from a BDD or an array of BDDs <P>
391<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
392Functions to handle BDD node infos and numbering
393    while storing a CNF formula from a BDD or an array of BDDs. <P>
394<DL>
395 <DT> <A HREF="dddmpAllDet.html#DddmpNumberDdNodesCnf" TARGET="MAIN"><CODE>DddmpNumberDdNodesCnf()</CODE></A>
396 <DD> Removes nodes from unique table and numbers them
397
398 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesCountEdgesAndNumber" TARGET="MAIN"><CODE>DddmpDdNodesCountEdgesAndNumber()</CODE></A>
399 <DD> Removes nodes from unique table and numbers each node according
400    to the number of its incoming BDD edges.
401
402 <DT> <A HREF="dddmpAllDet.html#DddmpUnnumberDdNodesCnf" TARGET="MAIN"><CODE>DddmpUnnumberDdNodesCnf()</CODE></A>
403 <DD> Restores nodes in unique table, loosing numbering
404
405 <DT> <A HREF="dddmpAllDet.html#DddmpPrintBddAndNext" TARGET="MAIN"><CODE>DddmpPrintBddAndNext()</CODE></A>
406 <DD> Prints debug information
407
408 <DT> <A HREF="dddmpAllDet.html#DddmpWriteNodeIndexCnf" TARGET="MAIN"><CODE>DddmpWriteNodeIndexCnf()</CODE></A>
409 <DD> Write index to node
410
411 <DT> <A HREF="dddmpAllDet.html#DddmpVisitedCnf" TARGET="MAIN"><CODE>DddmpVisitedCnf()</CODE></A>
412 <DD> Returns true if node is visited
413
414 <DT> <A HREF="dddmpAllDet.html#DddmpSetVisitedCnf" TARGET="MAIN"><CODE>DddmpSetVisitedCnf()</CODE></A>
415 <DD> Marks a node as visited
416
417 <DT> <A HREF="dddmpAllDet.html#DddmpReadNodeIndexCnf" TARGET="MAIN"><CODE>DddmpReadNodeIndexCnf()</CODE></A>
418 <DD> Reads the index of a node
419
420 <DT> <A HREF="dddmpAllDet.html#DddmpWriteNodeIndexCnfWithTerminalCheck" TARGET="MAIN"><CODE>DddmpWriteNodeIndexCnfWithTerminalCheck()</CODE></A>
421 <DD> Write index to node
422
423 <DT> <A HREF="dddmpAllDet.html#DddmpClearVisitedCnfRecur" TARGET="MAIN"><CODE>DddmpClearVisitedCnfRecur()</CODE></A>
424 <DD> Mark ALL nodes as not visited
425
426 <DT> <A HREF="dddmpAllDet.html#DddmpClearVisitedCnf" TARGET="MAIN"><CODE>DddmpClearVisitedCnf()</CODE></A>
427 <DD> Marks a node as not visited
428
429 <DT> <A HREF="dddmpAllDet.html#NumberNodeRecurCnf" TARGET="MAIN"><CODE>NumberNodeRecurCnf()</CODE></A>
430 <DD> Number nodes recursively in post-order
431
432 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesCheckIncomingAndScanPath" TARGET="MAIN"><CODE>DddmpDdNodesCheckIncomingAndScanPath()</CODE></A>
433 <DD> Number nodes recursively in post-order
434
435 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesNumberEdgesRecur" TARGET="MAIN"><CODE>DddmpDdNodesNumberEdgesRecur()</CODE></A>
436 <DD> Number nodes recursively in post-order
437
438 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesResetCountRecur" TARGET="MAIN"><CODE>DddmpDdNodesResetCountRecur()</CODE></A>
439 <DD> Resets counter and visited flag for ALL nodes of a BDD
440
441 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesCountEdgesRecur" TARGET="MAIN"><CODE>DddmpDdNodesCountEdgesRecur()</CODE></A>
442 <DD> Counts the number of incoming edges for each node of a BDD
443
444 <DT> <A HREF="dddmpAllDet.html#RemoveFromUniqueRecurCnf" TARGET="MAIN"><CODE>RemoveFromUniqueRecurCnf()</CODE></A>
445 <DD> Removes a node from unique table
446
447 <DT> <A HREF="dddmpAllDet.html#RestoreInUniqueRecurCnf" TARGET="MAIN"><CODE>RestoreInUniqueRecurCnf()</CODE></A>
448 <DD> Restores a node in unique table
449
450 <DT> <A HREF="dddmpAllDet.html#DddmpPrintBddAndNextRecur" TARGET="MAIN"><CODE>DddmpPrintBddAndNextRecur()</CODE></A>
451 <DD> Prints debug info
452
453</DL>
454<HR>
455<A NAME="dddmpStoreAdd.c"><H1>dddmpStoreAdd.c</H1></A>
456Functions to write ADDs to file. <P>
457<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
458Functions to write ADDs to file.
459    ADDs are represended on file either in text or binary format under the
460    following rules.  A file contains a forest of ADDs (a vector of
461    Boolean functions).  ADD nodes are numbered with contiguous numbers,
462    from 1 to NNodes (total number of nodes on a file). 0 is not used to
463    allow negative node indexes for complemented edges.  A file contains
464    a header, including information about variables and roots to ADD
465    functions, followed by the list of nodes.
466    ADD nodes are listed according to their numbering, and in the present
467    implementation numbering follows a post-order strategy, in such a way
468    that a node is never listed before its Then/Else children. <P>
469<DL>
470 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddAddStore" TARGET="MAIN"><CODE>Dddmp_cuddAddStore()</CODE></A>
471 <DD> Writes a dump file representing the argument ADD.
472
473 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddAddArrayStore" TARGET="MAIN"><CODE>Dddmp_cuddAddArrayStore()</CODE></A>
474 <DD> Writes a dump file representing the argument Array of ADDs.
475
476 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStoreBdd" TARGET="MAIN"><CODE>DddmpCuddDdArrayStoreBdd()</CODE></A>
477 <DD> Writes a dump file representing the argument Array of
478    BDDs/ADDs.
479
480 <DT> <A HREF="dddmpAllDet.html#NodeStoreRecurAdd" TARGET="MAIN"><CODE>NodeStoreRecurAdd()</CODE></A>
481 <DD> Performs the recursive step of Dddmp_bddStore.
482
483 <DT> <A HREF="dddmpAllDet.html#NodeTextStoreAdd" TARGET="MAIN"><CODE>NodeTextStoreAdd()</CODE></A>
484 <DD> Store One Single Node in Text Format.
485
486</DL>
487<HR>
488<A NAME="dddmpStoreBdd.c"><H1>dddmpStoreBdd.c</H1></A>
489Functions to write BDDs to file. <P>
490<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
491Functions to write BDDs to file.
492    BDDs are represended on file either in text or binary format under the
493    following rules.  A file contains a forest of BDDs (a vector of
494    Boolean functions).  BDD nodes are numbered with contiguous numbers,
495    from 1 to NNodes (total number of nodes on a file). 0 is not used to
496    allow negative node indexes for complemented edges.  A file contains
497    a header, including information about variables and roots to BDD
498    functions, followed by the list of nodes.  BDD nodes are listed
499    according to their numbering, and in the present implementation
500    numbering follows a post-order strategy, in such a way that a node
501    is never listed before its Then/Else children. <P>
502<DL>
503 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddStore" TARGET="MAIN"><CODE>Dddmp_cuddBddStore()</CODE></A>
504 <DD> Writes a dump file representing the argument BDD.
505
506 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddArrayStore" TARGET="MAIN"><CODE>Dddmp_cuddBddArrayStore()</CODE></A>
507 <DD> Writes a dump file representing the argument Array of BDDs.
508
509 <DT> <A HREF="dddmpAllDet.html#DddmpCuddBddArrayStore" TARGET="MAIN"><CODE>DddmpCuddBddArrayStore()</CODE></A>
510 <DD> Writes a dump file representing the argument Array of
511    BDDs.
512
513 <DT> <A HREF="dddmpAllDet.html#NodeStoreRecurBdd" TARGET="MAIN"><CODE>NodeStoreRecurBdd()</CODE></A>
514 <DD> Performs the recursive step of Dddmp_bddStore.
515
516 <DT> <A HREF="dddmpAllDet.html#NodeTextStoreBdd" TARGET="MAIN"><CODE>NodeTextStoreBdd()</CODE></A>
517 <DD> Store One Single Node in Text Format.
518
519 <DT> <A HREF="dddmpAllDet.html#NodeBinaryStoreBdd" TARGET="MAIN"><CODE>NodeBinaryStoreBdd()</CODE></A>
520 <DD> Store One Single Node in Binary Format.
521
522</DL>
523<HR>
524<A NAME="dddmpStoreCnf.c"><H1>dddmpStoreCnf.c</H1></A>
525Functions to write out BDDs to file in a CNF format <P>
526<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
527Functions to write out BDDs to file in a CNF format. <P>
528<DL>
529 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddStoreCnf" TARGET="MAIN"><CODE>Dddmp_cuddBddStoreCnf()</CODE></A>
530 <DD> Writes a dump file representing the argument BDD in
531    a CNF format.
532
533 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddArrayStoreCnf" TARGET="MAIN"><CODE>Dddmp_cuddBddArrayStoreCnf()</CODE></A>
534 <DD> Writes a dump file representing the argument array of BDDs
535    in CNF format.
536
537 <DT> <A HREF="dddmpAllDet.html#DddmpCuddBddArrayStoreCnf" TARGET="MAIN"><CODE>DddmpCuddBddArrayStoreCnf()</CODE></A>
538 <DD> Writes a dump file representing the argument Array of
539    BDDs in the CNF standard format.
540
541 <DT> <A HREF="dddmpAllDet.html#StoreCnfNodeByNode" TARGET="MAIN"><CODE>StoreCnfNodeByNode()</CODE></A>
542 <DD> Store the BDD as CNF clauses.
543
544 <DT> <A HREF="dddmpAllDet.html#StoreCnfNodeByNodeRecur" TARGET="MAIN"><CODE>StoreCnfNodeByNodeRecur()</CODE></A>
545 <DD> Performs the recursive step of Dddmp_bddStore.
546
547 <DT> <A HREF="dddmpAllDet.html#StoreCnfOneNode" TARGET="MAIN"><CODE>StoreCnfOneNode()</CODE></A>
548 <DD> Store One Single BDD Node.
549
550 <DT> <A HREF="dddmpAllDet.html#StoreCnfMaxtermByMaxterm" TARGET="MAIN"><CODE>StoreCnfMaxtermByMaxterm()</CODE></A>
551 <DD> Prints a disjoint sum of products.
552
553 <DT> <A HREF="dddmpAllDet.html#StoreCnfBest" TARGET="MAIN"><CODE>StoreCnfBest()</CODE></A>
554 <DD> Prints a disjoint sum of products with intermediate
555    cutting points.
556
557 <DT> <A HREF="dddmpAllDet.html#StoreCnfMaxtermByMaxtermRecur" TARGET="MAIN"><CODE>StoreCnfMaxtermByMaxtermRecur()</CODE></A>
558 <DD> Performs the recursive step of Print Maxterm.
559
560 <DT> <A HREF="dddmpAllDet.html#StoreCnfBestNotSharedRecur" TARGET="MAIN"><CODE>StoreCnfBestNotSharedRecur()</CODE></A>
561 <DD> Performs the recursive step of Print Best on Not Shared
562    sub-BDDs.
563
564 <DT> <A HREF="dddmpAllDet.html#StoreCnfBestSharedRecur" TARGET="MAIN"><CODE>StoreCnfBestSharedRecur()</CODE></A>
565 <DD> Performs the recursive step of Print Best on Shared
566    sub-BDDs.
567
568 <DT> <A HREF="dddmpAllDet.html#printCubeCnf" TARGET="MAIN"><CODE>printCubeCnf()</CODE></A>
569 <DD> Print One Cube in CNF Format.
570
571</DL>
572<HR>
573<A NAME="dddmpStoreMisc.c"><H1>dddmpStoreMisc.c</H1></A>
574Functions to write out bdds to file in prefixed
575    and in Blif form. <P>
576<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
577Functions to write out bdds to file.
578    BDDs are represended on file in text format.
579    Each node is stored as a multiplexer in a prefix notation format for
580    the prefix notation file or in PLA format for the blif file. <P>
581<DL>
582 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddStorePrefix" TARGET="MAIN"><CODE>Dddmp_cuddBddStorePrefix()</CODE></A>
583 <DD> Writes a dump file representing the argument BDD in
584    a prefix notation.
585
586 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddArrayStorePrefix" TARGET="MAIN"><CODE>Dddmp_cuddBddArrayStorePrefix()</CODE></A>
587 <DD> Writes a dump file representing the argument BDD in
588    a prefix notation.
589
590 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddStoreBlif" TARGET="MAIN"><CODE>Dddmp_cuddBddStoreBlif()</CODE></A>
591 <DD> Writes a dump file representing the argument BDD in
592    a Blif/Exlif notation.
593
594 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddArrayStoreBlif" TARGET="MAIN"><CODE>Dddmp_cuddBddArrayStoreBlif()</CODE></A>
595 <DD> Writes a dump file representing the argument BDD in
596    a Blif/Exlif notation.
597
598 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddStoreSmv" TARGET="MAIN"><CODE>Dddmp_cuddBddStoreSmv()</CODE></A>
599 <DD> Writes a dump file representing the argument BDD in
600    a prefix notation.
601
602 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddArrayStoreSmv" TARGET="MAIN"><CODE>Dddmp_cuddBddArrayStoreSmv()</CODE></A>
603 <DD> Writes a dump file representing the argument BDD in
604    a prefix notation.
605
606 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStorePrefix" TARGET="MAIN"><CODE>DddmpCuddDdArrayStorePrefix()</CODE></A>
607 <DD> Internal function to writes a dump file representing the
608    argument BDD in a prefix notation.
609
610 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStorePrefixBody" TARGET="MAIN"><CODE>DddmpCuddDdArrayStorePrefixBody()</CODE></A>
611 <DD> Internal function to writes a dump file representing the
612    argument BDD in a prefix notation. Writes the body of the file.
613
614 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStorePrefixStep" TARGET="MAIN"><CODE>DddmpCuddDdArrayStorePrefixStep()</CODE></A>
615 <DD> Performs the recursive step of
616    DddmpCuddDdArrayStorePrefixBody.
617
618 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStoreBlif" TARGET="MAIN"><CODE>DddmpCuddDdArrayStoreBlif()</CODE></A>
619 <DD> Writes a blif file representing the argument BDDs.
620
621 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStoreBlifBody" TARGET="MAIN"><CODE>DddmpCuddDdArrayStoreBlifBody()</CODE></A>
622 <DD> Writes a blif body representing the argument BDDs.
623
624 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStoreBlifStep" TARGET="MAIN"><CODE>DddmpCuddDdArrayStoreBlifStep()</CODE></A>
625 <DD> Performs the recursive step of DddmpCuddDdArrayStoreBlif.
626
627 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStoreSmv" TARGET="MAIN"><CODE>DddmpCuddDdArrayStoreSmv()</CODE></A>
628 <DD> Internal function to writes a dump file representing the
629    argument BDD in a SMV notation.
630
631 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStoreSmvBody" TARGET="MAIN"><CODE>DddmpCuddDdArrayStoreSmvBody()</CODE></A>
632 <DD> Internal function to writes a dump file representing the
633    argument BDD in a SMV notation. Writes the body of the file.
634
635 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStoreSmvStep" TARGET="MAIN"><CODE>DddmpCuddDdArrayStoreSmvStep()</CODE></A>
636 <DD> Performs the recursive step of
637    DddmpCuddDdArrayStoreSmvBody.
638
639</DL>
640<HR>
641<A NAME="dddmpUtil.c"><H1>dddmpUtil.c</H1></A>
642Util Functions for the dddmp package <P>
643<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
644Functions to manipulate arrays. <P>
645<DL>
646 <DT> <A HREF="dddmpAllDet.html#QsortStrcmp" TARGET="MAIN"><CODE>QsortStrcmp()</CODE></A>
647 <DD> String compare for qsort
648
649 <DT> <A HREF="dddmpAllDet.html#FindVarname" TARGET="MAIN"><CODE>FindVarname()</CODE></A>
650 <DD> Performs binary search of a name within a sorted array
651
652 <DT> <A HREF="dddmpAllDet.html#DddmpStrDup" TARGET="MAIN"><CODE>DddmpStrDup()</CODE></A>
653 <DD> Duplicates a string
654
655 <DT> <A HREF="dddmpAllDet.html#DddmpStrArrayDup" TARGET="MAIN"><CODE>DddmpStrArrayDup()</CODE></A>
656 <DD> Duplicates an array of strings
657
658 <DT> <A HREF="dddmpAllDet.html#DddmpStrArrayRead" TARGET="MAIN"><CODE>DddmpStrArrayRead()</CODE></A>
659 <DD> Inputs an array of strings
660
661 <DT> <A HREF="dddmpAllDet.html#DddmpStrArrayWrite" TARGET="MAIN"><CODE>DddmpStrArrayWrite()</CODE></A>
662 <DD> Outputs an array of strings
663
664 <DT> <A HREF="dddmpAllDet.html#DddmpStrArrayFree" TARGET="MAIN"><CODE>DddmpStrArrayFree()</CODE></A>
665 <DD> Frees an array of strings
666
667 <DT> <A HREF="dddmpAllDet.html#DddmpIntArrayDup" TARGET="MAIN"><CODE>DddmpIntArrayDup()</CODE></A>
668 <DD> Duplicates an array of ints
669
670 <DT> <A HREF="dddmpAllDet.html#DddmpIntArrayRead" TARGET="MAIN"><CODE>DddmpIntArrayRead()</CODE></A>
671 <DD> Inputs an array of ints
672
673 <DT> <A HREF="dddmpAllDet.html#DddmpIntArrayWrite" TARGET="MAIN"><CODE>DddmpIntArrayWrite()</CODE></A>
674 <DD> Outputs an array of ints
675
676</DL>
677<HR>
678Last updated on 1040218 17h14
679</BODY></HTML>
Note: See TracBrowser for help on using the repository browser.