distr/dddmp/doc/dddmpExtDet.html

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