distr/dddmp/doc/dddmpAllFile.html

   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>
  45 External 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>
  65 Internal 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>
  77 Input and output BDD codes and integers from/to file <P>
  78 <B>By: Gianpiero Cabodi and Stefano Quer</B><P>
  79 Input 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>
 109 Conversion between ASCII and binary formats <P>
 110 <B>By: Gianpiero Cabodi and Stefano Quer</B><P>
 111 Conversion 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>
 125 Functions to display BDD files <P>
 126 <B>By: Gianpiero Cabodi and Stefano Quer</B><P>
 127 Functions 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>
 135 Functions to handle BDD node infos and numbering <P>
 136 <B>By: Gianpiero Cabodi and Stefano Quer</B><P>
 137 Functions 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>
 172 Functions 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>
 175 Functions 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>
 239 Functions to read in bdds to file <P>
 240 <B>By: Gianpiero Cabodi and Stefano Quer</B><P>
 241 Functions 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>
 281 Functions to read in CNF from file as BDDs. <P>
 282 <B>By: Gianpiero Cabodi and Stefano Quer</B><P>
 283 Functions 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>
 315 Functions to handle ADD node infos and numbering <P>
 316 <B>By: Gianpiero Cabodi and Stefano Quer</B><P>
 317 Functions 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>
 352 Functions to handle BDD node infos and numbering <P>
 353 <B>By: Gianpiero Cabodi and Stefano Quer</B><P>
 354 Functions 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>
 389 Functions 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>
 392 Functions 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>
 456 Functions to write ADDs to file. <P>
 457 <B>By: Gianpiero Cabodi and Stefano Quer</B><P>
 458 Functions 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>
 489 Functions to write BDDs to file. <P>
 490 <B>By: Gianpiero Cabodi and Stefano Quer</B><P>
 491 Functions 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>
 525 Functions to write out BDDs to file in a CNF format <P>
 526 <B>By: Gianpiero Cabodi and Stefano Quer</B><P>
 527 Functions 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>
 574 Functions to write out bdds to file in prefixed
 575     and in Blif form. <P>
 576 <B>By: Gianpiero Cabodi and Stefano Quer</B><P>
 577 Functions 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>
 642 Util Functions for the dddmp package <P>
 643 <B>By: Gianpiero Cabodi and Stefano Quer</B><P>
 644 Functions 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>
 678 Last updated on 1040218 17h14
 679 </BODY></HTML>