distr/dddmp/doc/dddmpAllDet.html

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