distr/cudd/doc/cuddAllFile.html

   1 <HTML>
   2 <HEAD><TITLE>The cudd package: files</TITLE></HEAD>
   3 <BODY>
   4
   5 <DL>
   6  <DT> <A HREF="#cuddAddAbs.c"><CODE>cuddAddAbs.c</CODE></A>
   7  <DD> Quantification functions for ADDs.
   8  <DT> <A HREF="#cuddAddApply.c"><CODE>cuddAddApply.c</CODE></A>
   9  <DD> Apply functions for ADDs and their operators.
  10  <DT> <A HREF="#cuddAddFind.c"><CODE>cuddAddFind.c</CODE></A>
  11  <DD> Functions to find maximum and minimum in an ADD and to
  12   extract the i-th bit.
  13  <DT> <A HREF="#cuddAddInv.c"><CODE>cuddAddInv.c</CODE></A>
  14  <DD> Function to compute the scalar inverse of an ADD.
  15  <DT> <A HREF="#cuddAddIte.c"><CODE>cuddAddIte.c</CODE></A>
  16  <DD> ADD ITE function and satellites.
  17  <DT> <A HREF="#cuddAddNeg.c"><CODE>cuddAddNeg.c</CODE></A>
  18  <DD> Function to compute the negation of an ADD.
  19  <DT> <A HREF="#cuddAddWalsh.c"><CODE>cuddAddWalsh.c</CODE></A>
  20  <DD> Functions that generate Walsh matrices and residue
  21   functions in ADD form.
  22  <DT> <A HREF="#cuddAndAbs.c"><CODE>cuddAndAbs.c</CODE></A>
  23  <DD> Combined AND and existential abstraction for BDDs
  24  <DT> <A HREF="#cuddAnneal.c"><CODE>cuddAnneal.c</CODE></A>
  25  <DD> Reordering of DDs based on simulated annealing
  26  <DT> <A HREF="#cuddApa.c"><CODE>cuddApa.c</CODE></A>
  27  <DD> Arbitrary precision arithmetic functions.
  28  <DT> <A HREF="#cuddAPI.c"><CODE>cuddAPI.c</CODE></A>
  29  <DD> Application interface functions.
  30  <DT> <A HREF="#cuddApprox.c"><CODE>cuddApprox.c</CODE></A>
  31  <DD> Procedures to approximate a given BDD.
  32  <DT> <A HREF="#cuddBddAbs.c"><CODE>cuddBddAbs.c</CODE></A>
  33  <DD> Quantification functions for BDDs.
  34  <DT> <A HREF="#cuddBddCorr.c"><CODE>cuddBddCorr.c</CODE></A>
  35  <DD> Correlation between BDDs.
  36  <DT> <A HREF="#cuddBddIte.c"><CODE>cuddBddIte.c</CODE></A>
  37  <DD> BDD ITE function and satellites.
  38  <DT> <A HREF="#cuddBridge.c"><CODE>cuddBridge.c</CODE></A>
  39  <DD> Translation from BDD to ADD and vice versa and transfer between
  40   different managers.
  41  <DT> <A HREF="#cuddCache.c"><CODE>cuddCache.c</CODE></A>
  42  <DD> Functions for cache insertion and lookup.
  43  <DT> <A HREF="#cuddCheck.c"><CODE>cuddCheck.c</CODE></A>
  44  <DD> Functions to check consistency of data structures.
  45  <DT> <A HREF="#cuddClip.c"><CODE>cuddClip.c</CODE></A>
  46  <DD> Clipping functions.
  47  <DT> <A HREF="#cuddCof.c"><CODE>cuddCof.c</CODE></A>
  48  <DD> Cofactoring functions.
  49  <DT> <A HREF="#cuddCompose.c"><CODE>cuddCompose.c</CODE></A>
  50  <DD> Functional composition and variable permutation of DDs.
  51  <DT> <A HREF="#cuddDecomp.c"><CODE>cuddDecomp.c</CODE></A>
  52  <DD> Functions for BDD decomposition.
  53  <DT> <A HREF="#cuddEssent.c"><CODE>cuddEssent.c</CODE></A>
  54  <DD> Functions for the detection of essential variables.
  55  <DT> <A HREF="#cuddExact.c"><CODE>cuddExact.c</CODE></A>
  56  <DD> Functions for exact variable reordering.
  57  <DT> <A HREF="#cuddExport.c"><CODE>cuddExport.c</CODE></A>
  58  <DD> Export functions.
  59  <DT> <A HREF="#cuddGenCof.c"><CODE>cuddGenCof.c</CODE></A>
  60  <DD> Generalized cofactors for BDDs and ADDs.
  61  <DT> <A HREF="#cuddGenetic.c"><CODE>cuddGenetic.c</CODE></A>
  62  <DD> Genetic algorithm for variable reordering.
  63  <DT> <A HREF="#cuddGroup.c"><CODE>cuddGroup.c</CODE></A>
  64  <DD> Functions for group sifting.
  65  <DT> <A HREF="#cuddHarwell.c"><CODE>cuddHarwell.c</CODE></A>
  66  <DD> Function to read a matrix in Harwell format.
  67  <DT> <A HREF="#cuddInit.c"><CODE>cuddInit.c</CODE></A>
  68  <DD> Functions to initialize and shut down the DD manager.
  69  <DT> <A HREF="#cuddInteract.c"><CODE>cuddInteract.c</CODE></A>
  70  <DD> Functions to manipulate the variable interaction matrix.
  71  <DT> <A HREF="#cuddLCache.c"><CODE>cuddLCache.c</CODE></A>
  72  <DD> Functions for local caches.
  73  <DT> <A HREF="#cuddLevelQ.c"><CODE>cuddLevelQ.c</CODE></A>
  74  <DD> Procedure to manage level queues.
  75  <DT> <A HREF="#cuddLinear.c"><CODE>cuddLinear.c</CODE></A>
  76  <DD> Functions for DD reduction by linear transformations.
  77  <DT> <A HREF="#cuddLiteral.c"><CODE>cuddLiteral.c</CODE></A>
  78  <DD> Functions for manipulation of literal sets represented by
  79   BDDs.
  80  <DT> <A HREF="#cuddMatMult.c"><CODE>cuddMatMult.c</CODE></A>
  81  <DD> Matrix multiplication functions.
  82  <DT> <A HREF="#cuddPriority.c"><CODE>cuddPriority.c</CODE></A>
  83  <DD> Priority functions.
  84  <DT> <A HREF="#cuddRead.c"><CODE>cuddRead.c</CODE></A>
  85  <DD> Functions to read in a matrix
  86  <DT> <A HREF="#cuddRef.c"><CODE>cuddRef.c</CODE></A>
  87  <DD> Functions that manipulate the reference counts.
  88  <DT> <A HREF="#cuddReorder.c"><CODE>cuddReorder.c</CODE></A>
  89  <DD> Functions for dynamic variable reordering.
  90  <DT> <A HREF="#cuddSat.c"><CODE>cuddSat.c</CODE></A>
  91  <DD> Functions for the solution of satisfiability related
  92   problems.
  93  <DT> <A HREF="#cuddSign.c"><CODE>cuddSign.c</CODE></A>
  94  <DD> Computation of signatures.
  95  <DT> <A HREF="#cuddSolve.c"><CODE>cuddSolve.c</CODE></A>
  96  <DD> Boolean equation solver and related functions.
  97  <DT> <A HREF="#cuddSplit.c"><CODE>cuddSplit.c</CODE></A>
  98  <DD> Returns a subset of minterms from a boolean function.
  99  <DT> <A HREF="#cuddSubsetHB.c"><CODE>cuddSubsetHB.c</CODE></A>
 100  <DD> Procedure to subset the given BDD by choosing the heavier
 101                branches.
 102  <DT> <A HREF="#cuddSubsetSP.c"><CODE>cuddSubsetSP.c</CODE></A>
 103  <DD> Procedure to subset the given BDD choosing the shortest paths
 104             (largest cubes) in the BDD.
 105  <DT> <A HREF="#cuddSymmetry.c"><CODE>cuddSymmetry.c</CODE></A>
 106  <DD> Functions for symmetry-based variable reordering.
 107  <DT> <A HREF="#cuddTable.c"><CODE>cuddTable.c</CODE></A>
 108  <DD> Unique table management functions.
 109  <DT> <A HREF="#cuddUtil.c"><CODE>cuddUtil.c</CODE></A>
 110  <DD> Utility functions.
 111  <DT> <A HREF="#cuddWindow.c"><CODE>cuddWindow.c</CODE></A>
 112  <DD> Functions for variable reordering by window permutation.
 113  <DT> <A HREF="#cuddZddCount.c"><CODE>cuddZddCount.c</CODE></A>
 114  <DD> Procedures to count the number of minterms of a ZDD.
 115  <DT> <A HREF="#cuddZddFuncs.c"><CODE>cuddZddFuncs.c</CODE></A>
 116  <DD> Functions to manipulate covers represented as ZDDs.
 117  <DT> <A HREF="#cuddZddGroup.c"><CODE>cuddZddGroup.c</CODE></A>
 118  <DD> Functions for ZDD group sifting.
 119  <DT> <A HREF="#cuddZddIsop.c"><CODE>cuddZddIsop.c</CODE></A>
 120  <DD> Functions to find irredundant SOP covers as ZDDs from BDDs.
 121  <DT> <A HREF="#cuddZddLin.c"><CODE>cuddZddLin.c</CODE></A>
 122  <DD> Procedures for dynamic variable ordering of ZDDs.
 123  <DT> <A HREF="#cuddZddMisc.c"><CODE>cuddZddMisc.c</CODE></A>
 124  <DD> Miscellaneous utility functions for ZDDs.
 125  <DT> <A HREF="#cuddZddPort.c"><CODE>cuddZddPort.c</CODE></A>
 126  <DD> Functions that translate BDDs to ZDDs.
 127  <DT> <A HREF="#cuddZddReord.c"><CODE>cuddZddReord.c</CODE></A>
 128  <DD> Procedures for dynamic variable ordering of ZDDs.
 129  <DT> <A HREF="#cuddZddSetop.c"><CODE>cuddZddSetop.c</CODE></A>
 130  <DD> Set operations on ZDDs.
 131  <DT> <A HREF="#cuddZddSymm.c"><CODE>cuddZddSymm.c</CODE></A>
 132  <DD> Functions for symmetry-based ZDD variable reordering.
 133  <DT> <A HREF="#cuddZddUtil.c"><CODE>cuddZddUtil.c</CODE></A>
 134  <DD> Utility functions for ZDDs.
 135 </DL><HR>
 136 <A NAME="cuddAddAbs.c"><H1>cuddAddAbs.c</H1></A>
 137 Quantification functions for ADDs. <P>
 138 <B>By: Fabio Somenzi</B><P>
 139 External procedures included in this module:
 140                 <ul>
 141                 <li> Cudd_addExistAbstract()
 142                 <li> Cudd_addUnivAbstract()
 143                 <li> Cudd_addOrAbstract()
 144                 </ul>
 145         Internal procedures included in this module:
 146                 <ul>
 147                 <li> cuddAddExistAbstractRecur()
 148                 <li> cuddAddUnivAbstractRecur()
 149                 <li> cuddAddOrAbstractRecur()
 150                 </ul>
 151         Static procedures included in this module:
 152                 <ul>
 153                 <li> addCheckPositiveCube()
 154                 </ul> <P>
 155 <DL>
 156  <DT> <A HREF="cuddAllDet.html#Cudd_addExistAbstract" TARGET="MAIN"><CODE>Cudd_addExistAbstract()</CODE></A>
 157  <DD> Existentially Abstracts all the variables in cube from f.
 158
 159  <DT> <A HREF="cuddAllDet.html#Cudd_addUnivAbstract" TARGET="MAIN"><CODE>Cudd_addUnivAbstract()</CODE></A>
 160  <DD> Universally Abstracts all the variables in cube from f.
 161
 162  <DT> <A HREF="cuddAllDet.html#Cudd_addOrAbstract" TARGET="MAIN"><CODE>Cudd_addOrAbstract()</CODE></A>
 163  <DD> Disjunctively abstracts all the variables in cube from the
 164   0-1 ADD f.
 165
 166  <DT> <A HREF="cuddAllDet.html#cuddAddExistAbstractRecur" TARGET="MAIN"><CODE>cuddAddExistAbstractRecur()</CODE></A>
 167  <DD> Performs the recursive step of Cudd_addExistAbstract.
 168
 169  <DT> <A HREF="cuddAllDet.html#cuddAddUnivAbstractRecur" TARGET="MAIN"><CODE>cuddAddUnivAbstractRecur()</CODE></A>
 170  <DD> Performs the recursive step of Cudd_addUnivAbstract.
 171
 172  <DT> <A HREF="cuddAllDet.html#cuddAddOrAbstractRecur" TARGET="MAIN"><CODE>cuddAddOrAbstractRecur()</CODE></A>
 173  <DD> Performs the recursive step of Cudd_addOrAbstract.
 174
 175  <DT> <A HREF="cuddAllDet.html#addCheckPositiveCube" TARGET="MAIN"><CODE>addCheckPositiveCube()</CODE></A>
 176  <DD> Checks whether cube is an ADD representing the product
 177   of positive literals.
 178
 179 </DL>
 180 <HR>
 181 <A NAME="cuddAddApply.c"><H1>cuddAddApply.c</H1></A>
 182 Apply functions for ADDs and their operators. <P>
 183 <B>By: Fabio Somenzi</B><P>
 184 External procedures included in this module:
 185                 <ul>
 186                 <li> Cudd_addApply()
 187                 <li> Cudd_addMonadicApply()
 188                 <li> Cudd_addPlus()
 189                 <li> Cudd_addTimes()
 190                 <li> Cudd_addThreshold()
 191                 <li> Cudd_addSetNZ()
 192                 <li> Cudd_addDivide()
 193                 <li> Cudd_addMinus()
 194                 <li> Cudd_addMinimum()
 195                 <li> Cudd_addMaximum()
 196                 <li> Cudd_addOneZeroMaximum()
 197                 <li> Cudd_addDiff()
 198                 <li> Cudd_addAgreement()
 199                 <li> Cudd_addOr()
 200                 <li> Cudd_addNand()
 201                 <li> Cudd_addNor()
 202                 <li> Cudd_addXor()
 203                 <li> Cudd_addXnor()
 204                 </ul>
 205             Internal procedures included in this module:
 206                 <ul>
 207                 <li> cuddAddApplyRecur()
 208                 <li> cuddAddMonadicApplyRecur()
 209                 </ul> <P>
 210 <DL>
 211  <DT> <A HREF="cuddAllDet.html#Cudd_addApply" TARGET="MAIN"><CODE>Cudd_addApply()</CODE></A>
 212  <DD> Applies op to the corresponding discriminants of f and g.
 213
 214  <DT> <A HREF="cuddAllDet.html#Cudd_addPlus" TARGET="MAIN"><CODE>Cudd_addPlus()</CODE></A>
 215  <DD> Integer and floating point addition.
 216
 217  <DT> <A HREF="cuddAllDet.html#Cudd_addTimes" TARGET="MAIN"><CODE>Cudd_addTimes()</CODE></A>
 218  <DD> Integer and floating point multiplication.
 219
 220  <DT> <A HREF="cuddAllDet.html#Cudd_addThreshold" TARGET="MAIN"><CODE>Cudd_addThreshold()</CODE></A>
 221  <DD> f if f&gt;=g; 0 if f&lt;g.
 222
 223  <DT> <A HREF="cuddAllDet.html#Cudd_addSetNZ" TARGET="MAIN"><CODE>Cudd_addSetNZ()</CODE></A>
 224  <DD> This operator sets f to the value of g wherever g != 0.
 225
 226  <DT> <A HREF="cuddAllDet.html#Cudd_addDivide" TARGET="MAIN"><CODE>Cudd_addDivide()</CODE></A>
 227  <DD> Integer and floating point division.
 228
 229  <DT> <A HREF="cuddAllDet.html#Cudd_addMinus" TARGET="MAIN"><CODE>Cudd_addMinus()</CODE></A>
 230  <DD> Integer and floating point subtraction.
 231
 232  <DT> <A HREF="cuddAllDet.html#Cudd_addMinimum" TARGET="MAIN"><CODE>Cudd_addMinimum()</CODE></A>
 233  <DD> Integer and floating point min.
 234
 235  <DT> <A HREF="cuddAllDet.html#Cudd_addMaximum" TARGET="MAIN"><CODE>Cudd_addMaximum()</CODE></A>
 236  <DD> Integer and floating point max.
 237
 238  <DT> <A HREF="cuddAllDet.html#Cudd_addOneZeroMaximum" TARGET="MAIN"><CODE>Cudd_addOneZeroMaximum()</CODE></A>
 239  <DD> Returns 1 if f &gt; g and 0 otherwise.
 240
 241  <DT> <A HREF="cuddAllDet.html#Cudd_addDiff" TARGET="MAIN"><CODE>Cudd_addDiff()</CODE></A>
 242  <DD> Returns plusinfinity if f=g; returns min(f,g) if f!=g.
 243
 244  <DT> <A HREF="cuddAllDet.html#Cudd_addAgreement" TARGET="MAIN"><CODE>Cudd_addAgreement()</CODE></A>
 245  <DD> f if f==g; background if f!=g.
 246
 247  <DT> <A HREF="cuddAllDet.html#Cudd_addOr" TARGET="MAIN"><CODE>Cudd_addOr()</CODE></A>
 248  <DD> Disjunction of two 0-1 ADDs.
 249
 250  <DT> <A HREF="cuddAllDet.html#Cudd_addNand" TARGET="MAIN"><CODE>Cudd_addNand()</CODE></A>
 251  <DD> NAND of two 0-1 ADDs.
 252
 253  <DT> <A HREF="cuddAllDet.html#Cudd_addNor" TARGET="MAIN"><CODE>Cudd_addNor()</CODE></A>
 254  <DD> NOR of two 0-1 ADDs.
 255
 256  <DT> <A HREF="cuddAllDet.html#Cudd_addXor" TARGET="MAIN"><CODE>Cudd_addXor()</CODE></A>
 257  <DD> XOR of two 0-1 ADDs.
 258
 259  <DT> <A HREF="cuddAllDet.html#Cudd_addXnor" TARGET="MAIN"><CODE>Cudd_addXnor()</CODE></A>
 260  <DD> XNOR of two 0-1 ADDs.
 261
 262  <DT> <A HREF="cuddAllDet.html#Cudd_addMonadicApply" TARGET="MAIN"><CODE>Cudd_addMonadicApply()</CODE></A>
 263  <DD> Applies op to the discriminants of f.
 264
 265  <DT> <A HREF="cuddAllDet.html#Cudd_addLog" TARGET="MAIN"><CODE>Cudd_addLog()</CODE></A>
 266  <DD> Natural logarithm of an ADD.
 267
 268  <DT> <A HREF="cuddAllDet.html#cuddAddApplyRecur" TARGET="MAIN"><CODE>cuddAddApplyRecur()</CODE></A>
 269  <DD> Performs the recursive step of Cudd_addApply.
 270
 271  <DT> <A HREF="cuddAllDet.html#cuddAddMonadicApplyRecur" TARGET="MAIN"><CODE>cuddAddMonadicApplyRecur()</CODE></A>
 272  <DD> Performs the recursive step of Cudd_addMonadicApply.
 273
 274 </DL>
 275 <HR>
 276 <A NAME="cuddAddFind.c"><H1>cuddAddFind.c</H1></A>
 277 Functions to find maximum and minimum in an ADD and to
 278   extract the i-th bit. <P>
 279 <B>By: Fabio Somenzi</B><P>
 280 External procedures included in this module:
 281                 <ul>
 282                 <li> Cudd_addFindMax()
 283                 <li> Cudd_addFindMin()
 284                 <li> Cudd_addIthBit()
 285                 </ul>
 286                Static functions included in this module:
 287                 <ul>
 288                 <li> addDoIthBit()
 289                 </ul> <P>
 290 <DL>
 291  <DT> <A HREF="cuddAllDet.html#Cudd_addFindMax" TARGET="MAIN"><CODE>Cudd_addFindMax()</CODE></A>
 292  <DD> Finds the maximum discriminant of f.
 293
 294  <DT> <A HREF="cuddAllDet.html#Cudd_addFindMin" TARGET="MAIN"><CODE>Cudd_addFindMin()</CODE></A>
 295  <DD> Finds the minimum discriminant of f.
 296
 297  <DT> <A HREF="cuddAllDet.html#Cudd_addIthBit" TARGET="MAIN"><CODE>Cudd_addIthBit()</CODE></A>
 298  <DD> Extracts the i-th bit from an ADD.
 299
 300  <DT> <A HREF="cuddAllDet.html#addDoIthBit" TARGET="MAIN"><CODE>addDoIthBit()</CODE></A>
 301  <DD> Performs the recursive step for Cudd_addIthBit.
 302
 303 </DL>
 304 <HR>
 305 <A NAME="cuddAddInv.c"><H1>cuddAddInv.c</H1></A>
 306 Function to compute the scalar inverse of an ADD. <P>
 307 <B>By: Fabio Somenzi</B><P>
 308 External procedures included in this module:
 309                 <ul>
 310                 <li> Cudd_addScalarInverse()
 311                 </ul>
 312             Internal procedures included in this module:
 313                 <ul>
 314                 <li> cuddAddScalarInverseRecur()
 315                 </ul> <P>
 316 <DL>
 317  <DT> <A HREF="cuddAllDet.html#Cudd_addScalarInverse" TARGET="MAIN"><CODE>Cudd_addScalarInverse()</CODE></A>
 318  <DD> Computes the scalar inverse of an ADD.
 319
 320  <DT> <A HREF="cuddAllDet.html#cuddAddScalarInverseRecur" TARGET="MAIN"><CODE>cuddAddScalarInverseRecur()</CODE></A>
 321  <DD> Performs the recursive step of addScalarInverse.
 322
 323 </DL>
 324 <HR>
 325 <A NAME="cuddAddIte.c"><H1>cuddAddIte.c</H1></A>
 326 ADD ITE function and satellites. <P>
 327 <B>By: Fabio Somenzi</B><P>
 328 External procedures included in this module:
 329                 <ul>
 330                 <li> Cudd_addIte()
 331                 <li> Cudd_addIteConstant()
 332                 <li> Cudd_addEvalConst()
 333                 <li> Cudd_addCmpl()
 334                 <li> Cudd_addLeq()
 335                 </ul>
 336         Internal procedures included in this module:
 337                 <ul>
 338                 <li> cuddAddIteRecur()
 339                 <li> cuddAddCmplRecur()
 340                 </ul>
 341         Static procedures included in this module:
 342                 <ul>
 343                 <li> addVarToConst()
 344                 </ul> <P>
 345 <DL>
 346  <DT> <A HREF="cuddAllDet.html#Cudd_addIte" TARGET="MAIN"><CODE>Cudd_addIte()</CODE></A>
 347  <DD> Implements ITE(f,g,h).
 348
 349  <DT> <A HREF="cuddAllDet.html#Cudd_addIteConstant" TARGET="MAIN"><CODE>Cudd_addIteConstant()</CODE></A>
 350  <DD> Implements ITEconstant for ADDs.
 351
 352  <DT> <A HREF="cuddAllDet.html#Cudd_addEvalConst" TARGET="MAIN"><CODE>Cudd_addEvalConst()</CODE></A>
 353  <DD> Checks whether ADD g is constant whenever ADD f is 1.
 354
 355  <DT> <A HREF="cuddAllDet.html#Cudd_addCmpl" TARGET="MAIN"><CODE>Cudd_addCmpl()</CODE></A>
 356  <DD> Computes the complement of an ADD a la C language.
 357
 358  <DT> <A HREF="cuddAllDet.html#Cudd_addLeq" TARGET="MAIN"><CODE>Cudd_addLeq()</CODE></A>
 359  <DD> Determines whether f is less than or equal to g.
 360
 361  <DT> <A HREF="cuddAllDet.html#cuddAddIteRecur" TARGET="MAIN"><CODE>cuddAddIteRecur()</CODE></A>
 362  <DD> Implements the recursive step of Cudd_addIte(f,g,h).
 363
 364  <DT> <A HREF="cuddAllDet.html#cuddAddCmplRecur" TARGET="MAIN"><CODE>cuddAddCmplRecur()</CODE></A>
 365  <DD> Performs the recursive step of Cudd_addCmpl.
 366
 367  <DT> <A HREF="cuddAllDet.html#addVarToConst" TARGET="MAIN"><CODE>addVarToConst()</CODE></A>
 368  <DD> Replaces variables with constants if possible (part of
 369   canonical form).
 370
 371 </DL>
 372 <HR>
 373 <A NAME="cuddAddNeg.c"><H1>cuddAddNeg.c</H1></A>
 374 Function to compute the negation of an ADD. <P>
 375 <B>By: Fabio Somenzi, Balakrishna Kumthekar</B><P>
 376 External procedures included in this module:
 377                 <ul>
 378                 <li> Cudd_addNegate()
 379                 <li> Cudd_addRoundOff()
 380                 </ul>
 381         Internal procedures included in this module:
 382                 <ul>
 383                 <li> cuddAddNegateRecur()
 384                 <li> cuddAddRoundOffRecur()
 385                 </ul> <P>
 386 <DL>
 387  <DT> <A HREF="cuddAllDet.html#Cudd_addNegate" TARGET="MAIN"><CODE>Cudd_addNegate()</CODE></A>
 388  <DD> Computes the additive inverse of an ADD.
 389
 390  <DT> <A HREF="cuddAllDet.html#Cudd_addRoundOff" TARGET="MAIN"><CODE>Cudd_addRoundOff()</CODE></A>
 391  <DD> Rounds off the discriminants of an ADD.
 392
 393  <DT> <A HREF="cuddAllDet.html#cuddAddNegateRecur" TARGET="MAIN"><CODE>cuddAddNegateRecur()</CODE></A>
 394  <DD> Implements the recursive step of Cudd_addNegate.
 395
 396  <DT> <A HREF="cuddAllDet.html#cuddAddRoundOffRecur" TARGET="MAIN"><CODE>cuddAddRoundOffRecur()</CODE></A>
 397  <DD> Implements the recursive step of Cudd_addRoundOff.
 398
 399 </DL>
 400 <HR>
 401 <A NAME="cuddAddWalsh.c"><H1>cuddAddWalsh.c</H1></A>
 402 Functions that generate Walsh matrices and residue
 403   functions in ADD form. <P>
 404 <B>By: Fabio Somenzi</B><P>
 405 External procedures included in this module:
 406             <ul>
 407             <li> Cudd_addWalsh()
 408             <li> Cudd_addResidue()
 409             </ul>
 410         Static procedures included in this module:
 411             <ul>
 412             <li> addWalshInt()
 413             </ul> <P>
 414 <DL>
 415  <DT> <A HREF="cuddAllDet.html#Cudd_addWalsh" TARGET="MAIN"><CODE>Cudd_addWalsh()</CODE></A>
 416  <DD> Generates a Walsh matrix in ADD form.
 417
 418  <DT> <A HREF="cuddAllDet.html#Cudd_addResidue" TARGET="MAIN"><CODE>Cudd_addResidue()</CODE></A>
 419  <DD> Builds an ADD for the residue modulo m of an n-bit
 420   number.
 421
 422  <DT> <A HREF="cuddAllDet.html#addWalshInt" TARGET="MAIN"><CODE>addWalshInt()</CODE></A>
 423  <DD> Implements the recursive step of Cudd_addWalsh.
 424
 425 </DL>
 426 <HR>
 427 <A NAME="cuddAndAbs.c"><H1>cuddAndAbs.c</H1></A>
 428 Combined AND and existential abstraction for BDDs <P>
 429 <B>By: Fabio Somenzi</B><P>
 430 External procedures included in this module:
 431                 <ul>
 432                 <li> Cudd_bddAndAbstract()
 433                 <li> Cudd_bddAndAbstractLimit()
 434                 </ul>
 435             Internal procedures included in this module:
 436                 <ul>
 437                 <li> cuddBddAndAbstractRecur()
 438                 </ul> <P>
 439 <DL>
 440  <DT> <A HREF="cuddAllDet.html#Cudd_bddAndAbstract" TARGET="MAIN"><CODE>Cudd_bddAndAbstract()</CODE></A>
 441  <DD> Takes the AND of two BDDs and simultaneously abstracts the
 442   variables in cube.
 443
 444  <DT> <A HREF="cuddAllDet.html#Cudd_bddAndAbstractLimit" TARGET="MAIN"><CODE>Cudd_bddAndAbstractLimit()</CODE></A>
 445  <DD> Takes the AND of two BDDs and simultaneously abstracts the
 446   variables in cube.  Returns NULL if too many nodes are required.
 447
 448  <DT> <A HREF="cuddAllDet.html#cuddBddAndAbstractRecur" TARGET="MAIN"><CODE>cuddBddAndAbstractRecur()</CODE></A>
 449  <DD> Takes the AND of two BDDs and simultaneously abstracts the
 450   variables in cube.
 451
 452 </DL>
 453 <HR>
 454 <A NAME="cuddAnneal.c"><H1>cuddAnneal.c</H1></A>
 455 Reordering of DDs based on simulated annealing <P>
 456 <B>By: Jae-Young Jang, Jorgen Sivesind</B><P>
 457 Internal procedures included in this file:
 458                 <ul>
 459                 <li> cuddAnnealing()
 460                 </ul>
 461                Static procedures included in this file:
 462                 <ul>
 463                 <li> stopping_criterion()
 464                 <li> random_generator()
 465                 <li> ddExchange()
 466                 <li> ddJumpingAux()
 467                 <li> ddJumpingUp()
 468                 <li> ddJumpingDown()
 469                 <li> siftBackwardProb()
 470                 <li> copyOrder()
 471                 <li> restoreOrder()
 472                 </ul> <P>
 473 <DL>
 474  <DT> <A HREF="cuddAllDet.html#cuddAnnealing" TARGET="MAIN"><CODE>cuddAnnealing()</CODE></A>
 475  <DD> Get new variable-order by simulated annealing algorithm.
 476
 477  <DT> <A HREF="cuddAllDet.html#stopping_criterion" TARGET="MAIN"><CODE>stopping_criterion()</CODE></A>
 478  <DD> Checks termination condition.
 479
 480  <DT> <A HREF="cuddAllDet.html#random_generator" TARGET="MAIN"><CODE>random_generator()</CODE></A>
 481  <DD> Random number generator.
 482
 483  <DT> <A HREF="cuddAllDet.html#ddExchange" TARGET="MAIN"><CODE>ddExchange()</CODE></A>
 484  <DD> This function is for exchanging two variables, x and y.
 485
 486  <DT> <A HREF="cuddAllDet.html#ddJumpingAux" TARGET="MAIN"><CODE>ddJumpingAux()</CODE></A>
 487  <DD> Moves a variable to a specified position.
 488
 489  <DT> <A HREF="cuddAllDet.html#ddJumpingUp" TARGET="MAIN"><CODE>ddJumpingUp()</CODE></A>
 490  <DD> This function is for jumping up.
 491
 492  <DT> <A HREF="cuddAllDet.html#ddJumpingDown" TARGET="MAIN"><CODE>ddJumpingDown()</CODE></A>
 493  <DD> This function is for jumping down.
 494
 495  <DT> <A HREF="cuddAllDet.html#siftBackwardProb" TARGET="MAIN"><CODE>siftBackwardProb()</CODE></A>
 496  <DD> Returns the DD to the best position encountered during
 497   sifting if there was improvement.
 498
 499  <DT> <A HREF="cuddAllDet.html#copyOrder" TARGET="MAIN"><CODE>copyOrder()</CODE></A>
 500  <DD> Copies the current variable order to array.
 501
 502  <DT> <A HREF="cuddAllDet.html#restoreOrder" TARGET="MAIN"><CODE>restoreOrder()</CODE></A>
 503  <DD> Restores the variable order in array by a series of sifts up.
 504
 505 </DL>
 506 <HR>
 507 <A NAME="cuddApa.c"><H1>cuddApa.c</H1></A>
 508 Arbitrary precision arithmetic functions. <P>
 509 <B>By: Fabio Somenzi</B><P>
 510 External procedures included in this module:
 511                 <ul>
 512                 <li> Cudd_ApaNumberOfDigits()
 513                 <li> Cudd_NewApaNumber()
 514                 <li> Cudd_ApaCopy()
 515                 <li> Cudd_ApaAdd()
 516                 <li> Cudd_ApaSubtract()
 517                 <li> Cudd_ApaShortDivision()
 518                 <li> Cudd_ApaIntDivision()
 519                 <li> Cudd_ApaShiftRight()
 520                 <li> Cudd_ApaSetToLiteral()
 521                 <li> Cudd_ApaPowerOfTwo()
 522                 <li> Cudd_ApaCompare()
 523                 <li> Cudd_ApaCompareRatios()
 524                 <li> Cudd_ApaPrintHex()
 525                 <li> Cudd_ApaPrintDecimal()
 526                 <li> Cudd_ApaPrintExponential()
 527                 <li> Cudd_ApaCountMinterm()
 528                 <li> Cudd_ApaPrintMinterm()
 529                 <li> Cudd_ApaPrintMintermExp()
 530                 <li> Cudd_ApaPrintDensity()
 531                 </ul>
 532         Static procedures included in this module:
 533                 <ul>
 534                 <li> cuddApaCountMintermAux()
 535                 <li> cuddApaStCountfree()
 536                 </ul> <P>
 537 <DL>
 538  <DT> <A HREF="cuddAllDet.html#Cudd_ApaNumberOfDigits" TARGET="MAIN"><CODE>Cudd_ApaNumberOfDigits()</CODE></A>
 539  <DD> Finds the number of digits for an arbitrary precision
 540   integer.
 541
 542  <DT> <A HREF="cuddAllDet.html#Cudd_NewApaNumber" TARGET="MAIN"><CODE>Cudd_NewApaNumber()</CODE></A>
 543  <DD> Allocates memory for an arbitrary precision integer.
 544
 545  <DT> <A HREF="cuddAllDet.html#Cudd_ApaCopy" TARGET="MAIN"><CODE>Cudd_ApaCopy()</CODE></A>
 546  <DD> Makes a copy of an arbitrary precision integer.
 547
 548  <DT> <A HREF="cuddAllDet.html#Cudd_ApaAdd" TARGET="MAIN"><CODE>Cudd_ApaAdd()</CODE></A>
 549  <DD> Adds two arbitrary precision integers.
 550
 551  <DT> <A HREF="cuddAllDet.html#Cudd_ApaSubtract" TARGET="MAIN"><CODE>Cudd_ApaSubtract()</CODE></A>
 552  <DD> Subtracts two arbitrary precision integers.
 553
 554  <DT> <A HREF="cuddAllDet.html#Cudd_ApaShortDivision" TARGET="MAIN"><CODE>Cudd_ApaShortDivision()</CODE></A>
 555  <DD> Divides an arbitrary precision integer by a digit.
 556
 557  <DT> <A HREF="cuddAllDet.html#Cudd_ApaIntDivision" TARGET="MAIN"><CODE>Cudd_ApaIntDivision()</CODE></A>
 558  <DD> Divides an arbitrary precision integer by an integer.
 559
 560  <DT> <A HREF="cuddAllDet.html#Cudd_ApaShiftRight" TARGET="MAIN"><CODE>Cudd_ApaShiftRight()</CODE></A>
 561  <DD> Shifts right an arbitrary precision integer by one binary
 562   place.
 563
 564  <DT> <A HREF="cuddAllDet.html#Cudd_ApaSetToLiteral" TARGET="MAIN"><CODE>Cudd_ApaSetToLiteral()</CODE></A>
 565  <DD> Sets an arbitrary precision integer to a one-digit literal.
 566
 567  <DT> <A HREF="cuddAllDet.html#Cudd_ApaPowerOfTwo" TARGET="MAIN"><CODE>Cudd_ApaPowerOfTwo()</CODE></A>
 568  <DD> Sets an arbitrary precision integer to a power of two.
 569
 570  <DT> <A HREF="cuddAllDet.html#Cudd_ApaCompare" TARGET="MAIN"><CODE>Cudd_ApaCompare()</CODE></A>
 571  <DD> Compares two arbitrary precision integers.
 572
 573  <DT> <A HREF="cuddAllDet.html#Cudd_ApaCompareRatios" TARGET="MAIN"><CODE>Cudd_ApaCompareRatios()</CODE></A>
 574  <DD> Compares the ratios of two arbitrary precision integers to two
 575   unsigned ints.
 576
 577  <DT> <A HREF="cuddAllDet.html#Cudd_ApaPrintHex" TARGET="MAIN"><CODE>Cudd_ApaPrintHex()</CODE></A>
 578  <DD> Prints an arbitrary precision integer in hexadecimal format.
 579
 580  <DT> <A HREF="cuddAllDet.html#Cudd_ApaPrintDecimal" TARGET="MAIN"><CODE>Cudd_ApaPrintDecimal()</CODE></A>
 581  <DD> Prints an arbitrary precision integer in decimal format.
 582
 583  <DT> <A HREF="cuddAllDet.html#Cudd_ApaPrintExponential" TARGET="MAIN"><CODE>Cudd_ApaPrintExponential()</CODE></A>
 584  <DD> Prints an arbitrary precision integer in exponential format.
 585
 586  <DT> <A HREF="cuddAllDet.html#Cudd_ApaCountMinterm" TARGET="MAIN"><CODE>Cudd_ApaCountMinterm()</CODE></A>
 587  <DD> Counts the number of minterms of a DD.
 588
 589  <DT> <A HREF="cuddAllDet.html#Cudd_ApaPrintMinterm" TARGET="MAIN"><CODE>Cudd_ApaPrintMinterm()</CODE></A>
 590  <DD> Prints the number of minterms of a BDD or ADD using
 591   arbitrary precision arithmetic.
 592
 593  <DT> <A HREF="cuddAllDet.html#Cudd_ApaPrintMintermExp" TARGET="MAIN"><CODE>Cudd_ApaPrintMintermExp()</CODE></A>
 594  <DD> Prints the number of minterms of a BDD or ADD in exponential
 595   format using arbitrary precision arithmetic.
 596
 597  <DT> <A HREF="cuddAllDet.html#Cudd_ApaPrintDensity" TARGET="MAIN"><CODE>Cudd_ApaPrintDensity()</CODE></A>
 598  <DD> Prints the density of a BDD or ADD using
 599   arbitrary precision arithmetic.
 600
 601  <DT> <A HREF="cuddAllDet.html#cuddApaCountMintermAux" TARGET="MAIN"><CODE>cuddApaCountMintermAux()</CODE></A>
 602  <DD> Performs the recursive step of Cudd_ApaCountMinterm.
 603
 604  <DT> <A HREF="cuddAllDet.html#cuddApaStCountfree" TARGET="MAIN"><CODE>cuddApaStCountfree()</CODE></A>
 605  <DD> Frees the memory used to store the minterm counts recorded
 606   in the visited table.
 607
 608 </DL>
 609 <HR>
 610 <A NAME="cuddAPI.c"><H1>cuddAPI.c</H1></A>
 611 Application interface functions. <P>
 612 <B>By: Fabio Somenzi</B><P>
 613 External procedures included in this module:
 614                 <ul>
 615                 <li> Cudd_addNewVar()
 616                 <li> Cudd_addNewVarAtLevel()
 617                 <li> Cudd_bddNewVar()
 618                 <li> Cudd_bddNewVarAtLevel()
 619                 <li> Cudd_addIthVar()
 620                 <li> Cudd_bddIthVar()
 621                 <li> Cudd_zddIthVar()
 622                 <li> Cudd_zddVarsFromBddVars()
 623                 <li> Cudd_addConst()
 624                 <li> Cudd_IsNonConstant()
 625                 <li> Cudd_AutodynEnable()
 626                 <li> Cudd_AutodynDisable()
 627                 <li> Cudd_ReorderingStatus()
 628                 <li> Cudd_AutodynEnableZdd()
 629                 <li> Cudd_AutodynDisableZdd()
 630                 <li> Cudd_ReorderingStatusZdd()
 631                 <li> Cudd_zddRealignmentEnabled()
 632                 <li> Cudd_zddRealignEnable()
 633                 <li> Cudd_zddRealignDisable()
 634                 <li> Cudd_bddRealignmentEnabled()
 635                 <li> Cudd_bddRealignEnable()
 636                 <li> Cudd_bddRealignDisable()
 637                 <li> Cudd_ReadOne()
 638                 <li> Cudd_ReadZddOne()
 639                 <li> Cudd_ReadZero()
 640                 <li> Cudd_ReadLogicZero()
 641                 <li> Cudd_ReadPlusInfinity()
 642                 <li> Cudd_ReadMinusInfinity()
 643                 <li> Cudd_ReadBackground()
 644                 <li> Cudd_SetBackground()
 645                 <li> Cudd_ReadCacheSlots()
 646                 <li> Cudd_ReadCacheUsedSlots()
 647                 <li> Cudd_ReadCacheLookUps()
 648                 <li> Cudd_ReadCacheHits()
 649                 <li> Cudd_ReadMinHit()
 650                 <li> Cudd_SetMinHit()
 651                 <li> Cudd_ReadLooseUpTo()
 652                 <li> Cudd_SetLooseUpTo()
 653                 <li> Cudd_ReadMaxCache()
 654                 <li> Cudd_ReadMaxCacheHard()
 655                 <li> Cudd_SetMaxCacheHard()
 656                 <li> Cudd_ReadSize()
 657                 <li> Cudd_ReadSlots()
 658                 <li> Cudd_ReadUsedSlots()
 659                 <li> Cudd_ExpectedUsedSlots()
 660                 <li> Cudd_ReadKeys()
 661                 <li> Cudd_ReadDead()
 662                 <li> Cudd_ReadMinDead()
 663                 <li> Cudd_ReadReorderings()
 664                 <li> Cudd_ReadReorderingTime()
 665                 <li> Cudd_ReadGarbageCollections()
 666                 <li> Cudd_ReadGarbageCollectionTime()
 667                 <li> Cudd_ReadNodesFreed()
 668                 <li> Cudd_ReadNodesDropped()
 669                 <li> Cudd_ReadUniqueLookUps()
 670                 <li> Cudd_ReadUniqueLinks()
 671                 <li> Cudd_ReadSiftMaxVar()
 672                 <li> Cudd_SetSiftMaxVar()
 673                 <li> Cudd_ReadMaxGrowth()
 674                 <li> Cudd_SetMaxGrowth()
 675                 <li> Cudd_ReadMaxGrowthAlternate()
 676                 <li> Cudd_SetMaxGrowthAlternate()
 677                 <li> Cudd_ReadReorderingCycle()
 678                 <li> Cudd_SetReorderingCycle()
 679                 <li> Cudd_ReadTree()
 680                 <li> Cudd_SetTree()
 681                 <li> Cudd_FreeTree()
 682                 <li> Cudd_ReadZddTree()
 683                 <li> Cudd_SetZddTree()
 684                 <li> Cudd_FreeZddTree()
 685                 <li> Cudd_NodeReadIndex()
 686                 <li> Cudd_ReadPerm()
 687                 <li> Cudd_ReadInvPerm()
 688                 <li> Cudd_ReadVars()
 689                 <li> Cudd_ReadEpsilon()
 690                 <li> Cudd_SetEpsilon()
 691                 <li> Cudd_ReadGroupCheck()
 692                 <li> Cudd_SetGroupcheck()
 693                 <li> Cudd_GarbageCollectionEnabled()
 694                 <li> Cudd_EnableGarbageCollection()
 695                 <li> Cudd_DisableGarbageCollection()
 696                 <li> Cudd_DeadAreCounted()
 697                 <li> Cudd_TurnOnCountDead()
 698                 <li> Cudd_TurnOffCountDead()
 699                 <li> Cudd_ReadRecomb()
 700                 <li> Cudd_SetRecomb()
 701                 <li> Cudd_ReadSymmviolation()
 702                 <li> Cudd_SetSymmviolation()
 703                 <li> Cudd_ReadArcviolation()
 704                 <li> Cudd_SetArcviolation()
 705                 <li> Cudd_ReadPopulationSize()
 706                 <li> Cudd_SetPopulationSize()
 707                 <li> Cudd_ReadNumberXovers()
 708                 <li> Cudd_SetNumberXovers()
 709                 <li> Cudd_ReadMemoryInUse()
 710                 <li> Cudd_PrintInfo()
 711                 <li> Cudd_ReadPeakNodeCount()
 712                 <li> Cudd_ReadPeakLiveNodeCount()
 713                 <li> Cudd_ReadNodeCount()
 714                 <li> Cudd_zddReadNodeCount()
 715                 <li> Cudd_AddHook()
 716                 <li> Cudd_RemoveHook()
 717                 <li> Cudd_IsInHook()
 718                 <li> Cudd_StdPreReordHook()
 719                 <li> Cudd_StdPostReordHook()
 720                 <li> Cudd_EnableReorderingReporting()
 721                 <li> Cudd_DisableReorderingReporting()
 722                 <li> Cudd_ReorderingReporting()
 723                 <li> Cudd_ReadErrorCode()
 724                 <li> Cudd_ClearErrorCode()
 725                 <li> Cudd_ReadStdout()
 726                 <li> Cudd_SetStdout()
 727                 <li> Cudd_ReadStderr()
 728                 <li> Cudd_SetStderr()
 729                 <li> Cudd_ReadNextReordering()
 730                 <li> Cudd_SetNextReordering()
 731                 <li> Cudd_ReadSwapSteps()
 732                 <li> Cudd_ReadMaxLive()
 733                 <li> Cudd_SetMaxLive()
 734                 <li> Cudd_ReadMaxMemory()
 735                 <li> Cudd_SetMaxMemory()
 736                 <li> Cudd_bddBindVar()
 737                 <li> Cudd_bddUnbindVar()
 738                 <li> Cudd_bddVarIsBound()
 739                 <li> Cudd_bddSetPiVar()
 740                 <li> Cudd_bddSetPsVar()
 741                 <li> Cudd_bddSetNsVar()
 742                 <li> Cudd_bddIsPiVar()
 743                 <li> Cudd_bddIsPsVar()
 744                 <li> Cudd_bddIsNsVar()
 745                 <li> Cudd_bddSetPairIndex()
 746                 <li> Cudd_bddReadPairIndex()
 747                 <li> Cudd_bddSetVarToBeGrouped()
 748                 <li> Cudd_bddSetVarHardGroup()
 749                 <li> Cudd_bddResetVarToBeGrouped()
 750                 <li> Cudd_bddIsVarToBeGrouped()
 751                 <li> Cudd_bddSetVarToBeUngrouped()
 752                 <li> Cudd_bddIsVarToBeUngrouped()
 753                 <li> Cudd_bddIsVarHardGroup()
 754                 </ul>
 755               Static procedures included in this module:
 756                 <ul>
 757                 <li> fixVarTree()
 758                 </ul> <P>
 759 <DL>
 760  <DT> <A HREF="cuddAllDet.html#Cudd_addNewVar" TARGET="MAIN"><CODE>Cudd_addNewVar()</CODE></A>
 761  <DD> Returns a new ADD variable.
 762
 763  <DT> <A HREF="cuddAllDet.html#Cudd_addNewVarAtLevel" TARGET="MAIN"><CODE>Cudd_addNewVarAtLevel()</CODE></A>
 764  <DD> Returns a new ADD variable at a specified level.
 765
 766  <DT> <A HREF="cuddAllDet.html#Cudd_bddNewVar" TARGET="MAIN"><CODE>Cudd_bddNewVar()</CODE></A>
 767  <DD> Returns a new BDD variable.
 768
 769  <DT> <A HREF="cuddAllDet.html#Cudd_bddNewVarAtLevel" TARGET="MAIN"><CODE>Cudd_bddNewVarAtLevel()</CODE></A>
 770  <DD> Returns a new BDD variable at a specified level.
 771
 772  <DT> <A HREF="cuddAllDet.html#Cudd_addIthVar" TARGET="MAIN"><CODE>Cudd_addIthVar()</CODE></A>
 773  <DD> Returns the ADD variable with index i.
 774
 775  <DT> <A HREF="cuddAllDet.html#Cudd_bddIthVar" TARGET="MAIN"><CODE>Cudd_bddIthVar()</CODE></A>
 776  <DD> Returns the BDD variable with index i.
 777
 778  <DT> <A HREF="cuddAllDet.html#Cudd_zddIthVar" TARGET="MAIN"><CODE>Cudd_zddIthVar()</CODE></A>
 779  <DD> Returns the ZDD variable with index i.
 780
 781  <DT> <A HREF="cuddAllDet.html#Cudd_zddVarsFromBddVars" TARGET="MAIN"><CODE>Cudd_zddVarsFromBddVars()</CODE></A>
 782  <DD> Creates one or more ZDD variables for each BDD variable.
 783
 784  <DT> <A HREF="cuddAllDet.html#Cudd_addConst" TARGET="MAIN"><CODE>Cudd_addConst()</CODE></A>
 785  <DD> Returns the ADD for constant c.
 786
 787  <DT> <A HREF="cuddAllDet.html#Cudd_IsNonConstant" TARGET="MAIN"><CODE>Cudd_IsNonConstant()</CODE></A>
 788  <DD> Returns 1 if a DD node is not constant.
 789
 790  <DT> <A HREF="cuddAllDet.html#Cudd_AutodynEnable" TARGET="MAIN"><CODE>Cudd_AutodynEnable()</CODE></A>
 791  <DD> Enables automatic dynamic reordering of BDDs and ADDs.
 792
 793  <DT> <A HREF="cuddAllDet.html#Cudd_AutodynDisable" TARGET="MAIN"><CODE>Cudd_AutodynDisable()</CODE></A>
 794  <DD> Disables automatic dynamic reordering.
 795
 796  <DT> <A HREF="cuddAllDet.html#Cudd_ReorderingStatus" TARGET="MAIN"><CODE>Cudd_ReorderingStatus()</CODE></A>
 797  <DD> Reports the status of automatic dynamic reordering of BDDs
 798   and ADDs.
 799
 800  <DT> <A HREF="cuddAllDet.html#Cudd_AutodynEnableZdd" TARGET="MAIN"><CODE>Cudd_AutodynEnableZdd()</CODE></A>
 801  <DD> Enables automatic dynamic reordering of ZDDs.
 802
 803  <DT> <A HREF="cuddAllDet.html#Cudd_AutodynDisableZdd" TARGET="MAIN"><CODE>Cudd_AutodynDisableZdd()</CODE></A>
 804  <DD> Disables automatic dynamic reordering of ZDDs.
 805
 806  <DT> <A HREF="cuddAllDet.html#Cudd_ReorderingStatusZdd" TARGET="MAIN"><CODE>Cudd_ReorderingStatusZdd()</CODE></A>
 807  <DD> Reports the status of automatic dynamic reordering of ZDDs.
 808
 809  <DT> <A HREF="cuddAllDet.html#Cudd_zddRealignmentEnabled" TARGET="MAIN"><CODE>Cudd_zddRealignmentEnabled()</CODE></A>
 810  <DD> Tells whether the realignment of ZDD order to BDD order is
 811   enabled.
 812
 813  <DT> <A HREF="cuddAllDet.html#Cudd_zddRealignEnable" TARGET="MAIN"><CODE>Cudd_zddRealignEnable()</CODE></A>
 814  <DD> Enables realignment of ZDD order to BDD order.
 815
 816  <DT> <A HREF="cuddAllDet.html#Cudd_zddRealignDisable" TARGET="MAIN"><CODE>Cudd_zddRealignDisable()</CODE></A>
 817  <DD> Disables realignment of ZDD order to BDD order.
 818
 819  <DT> <A HREF="cuddAllDet.html#Cudd_bddRealignmentEnabled" TARGET="MAIN"><CODE>Cudd_bddRealignmentEnabled()</CODE></A>
 820  <DD> Tells whether the realignment of BDD order to ZDD order is
 821   enabled.
 822
 823  <DT> <A HREF="cuddAllDet.html#Cudd_bddRealignEnable" TARGET="MAIN"><CODE>Cudd_bddRealignEnable()</CODE></A>
 824  <DD> Enables realignment of BDD order to ZDD order.
 825
 826  <DT> <A HREF="cuddAllDet.html#Cudd_bddRealignDisable" TARGET="MAIN"><CODE>Cudd_bddRealignDisable()</CODE></A>
 827  <DD> Disables realignment of ZDD order to BDD order.
 828
 829  <DT> <A HREF="cuddAllDet.html#Cudd_ReadOne" TARGET="MAIN"><CODE>Cudd_ReadOne()</CODE></A>
 830  <DD> Returns the one constant of the manager.
 831
 832  <DT> <A HREF="cuddAllDet.html#Cudd_ReadZddOne" TARGET="MAIN"><CODE>Cudd_ReadZddOne()</CODE></A>
 833  <DD> Returns the ZDD for the constant 1 function.
 834
 835  <DT> <A HREF="cuddAllDet.html#Cudd_ReadZero" TARGET="MAIN"><CODE>Cudd_ReadZero()</CODE></A>
 836  <DD> Returns the zero constant of the manager.
 837
 838  <DT> <A HREF="cuddAllDet.html#Cudd_ReadLogicZero" TARGET="MAIN"><CODE>Cudd_ReadLogicZero()</CODE></A>
 839  <DD> Returns the logic zero constant of the manager.
 840
 841  <DT> <A HREF="cuddAllDet.html#Cudd_ReadPlusInfinity" TARGET="MAIN"><CODE>Cudd_ReadPlusInfinity()</CODE></A>
 842  <DD> Reads the plus-infinity constant from the manager.
 843
 844  <DT> <A HREF="cuddAllDet.html#Cudd_ReadMinusInfinity" TARGET="MAIN"><CODE>Cudd_ReadMinusInfinity()</CODE></A>
 845  <DD> Reads the minus-infinity constant from the manager.
 846
 847  <DT> <A HREF="cuddAllDet.html#Cudd_ReadBackground" TARGET="MAIN"><CODE>Cudd_ReadBackground()</CODE></A>
 848  <DD> Reads the background constant of the manager.
 849
 850  <DT> <A HREF="cuddAllDet.html#Cudd_SetBackground" TARGET="MAIN"><CODE>Cudd_SetBackground()</CODE></A>
 851  <DD> Sets the background constant of the manager.
 852
 853  <DT> <A HREF="cuddAllDet.html#Cudd_ReadCacheSlots" TARGET="MAIN"><CODE>Cudd_ReadCacheSlots()</CODE></A>
 854  <DD> Reads the number of slots in the cache.
 855
 856  <DT> <A HREF="cuddAllDet.html#Cudd_ReadCacheUsedSlots" TARGET="MAIN"><CODE>Cudd_ReadCacheUsedSlots()</CODE></A>
 857  <DD> Reads the fraction of used slots in the cache.
 858
 859  <DT> <A HREF="cuddAllDet.html#Cudd_ReadCacheLookUps" TARGET="MAIN"><CODE>Cudd_ReadCacheLookUps()</CODE></A>
 860  <DD> Returns the number of cache look-ups.
 861
 862  <DT> <A HREF="cuddAllDet.html#Cudd_ReadCacheHits" TARGET="MAIN"><CODE>Cudd_ReadCacheHits()</CODE></A>
 863  <DD> Returns the number of cache hits.
 864
 865  <DT> <A HREF="cuddAllDet.html#Cudd_ReadRecursiveCalls" TARGET="MAIN"><CODE>Cudd_ReadRecursiveCalls()</CODE></A>
 866  <DD> Returns the number of recursive calls.
 867
 868  <DT> <A HREF="cuddAllDet.html#Cudd_ReadMinHit" TARGET="MAIN"><CODE>Cudd_ReadMinHit()</CODE></A>
 869  <DD> Reads the hit rate that causes resizinig of the computed
 870   table.
 871
 872  <DT> <A HREF="cuddAllDet.html#Cudd_SetMinHit" TARGET="MAIN"><CODE>Cudd_SetMinHit()</CODE></A>
 873  <DD> Sets the hit rate that causes resizinig of the computed
 874   table.
 875
 876  <DT> <A HREF="cuddAllDet.html#Cudd_ReadLooseUpTo" TARGET="MAIN"><CODE>Cudd_ReadLooseUpTo()</CODE></A>
 877  <DD> Reads the looseUpTo parameter of the manager.
 878
 879  <DT> <A HREF="cuddAllDet.html#Cudd_SetLooseUpTo" TARGET="MAIN"><CODE>Cudd_SetLooseUpTo()</CODE></A>
 880  <DD> Sets the looseUpTo parameter of the manager.
 881
 882  <DT> <A HREF="cuddAllDet.html#Cudd_ReadMaxCache" TARGET="MAIN"><CODE>Cudd_ReadMaxCache()</CODE></A>
 883  <DD> Returns the soft limit for the cache size.
 884
 885  <DT> <A HREF="cuddAllDet.html#Cudd_ReadMaxCacheHard" TARGET="MAIN"><CODE>Cudd_ReadMaxCacheHard()</CODE></A>
 886  <DD> Reads the maxCacheHard parameter of the manager.
 887
 888  <DT> <A HREF="cuddAllDet.html#Cudd_SetMaxCacheHard" TARGET="MAIN"><CODE>Cudd_SetMaxCacheHard()</CODE></A>
 889  <DD> Sets the maxCacheHard parameter of the manager.
 890
 891  <DT> <A HREF="cuddAllDet.html#Cudd_ReadSize" TARGET="MAIN"><CODE>Cudd_ReadSize()</CODE></A>
 892  <DD> Returns the number of BDD variables in existance.
 893
 894  <DT> <A HREF="cuddAllDet.html#Cudd_ReadZddSize" TARGET="MAIN"><CODE>Cudd_ReadZddSize()</CODE></A>
 895  <DD> Returns the number of ZDD variables in existance.
 896
 897  <DT> <A HREF="cuddAllDet.html#Cudd_ReadSlots" TARGET="MAIN"><CODE>Cudd_ReadSlots()</CODE></A>
 898  <DD> Returns the total number of slots of the unique table.
 899
 900  <DT> <A HREF="cuddAllDet.html#Cudd_ReadUsedSlots" TARGET="MAIN"><CODE>Cudd_ReadUsedSlots()</CODE></A>
 901  <DD> Reads the fraction of used slots in the unique table.
 902
 903  <DT> <A HREF="cuddAllDet.html#Cudd_ExpectedUsedSlots" TARGET="MAIN"><CODE>Cudd_ExpectedUsedSlots()</CODE></A>
 904  <DD> Computes the expected fraction of used slots in the unique
 905   table.
 906
 907  <DT> <A HREF="cuddAllDet.html#Cudd_ReadKeys" TARGET="MAIN"><CODE>Cudd_ReadKeys()</CODE></A>
 908  <DD> Returns the number of nodes in the unique table.
 909
 910  <DT> <A HREF="cuddAllDet.html#Cudd_ReadDead" TARGET="MAIN"><CODE>Cudd_ReadDead()</CODE></A>
 911  <DD> Returns the number of dead nodes in the unique table.
 912
 913  <DT> <A HREF="cuddAllDet.html#Cudd_ReadMinDead" TARGET="MAIN"><CODE>Cudd_ReadMinDead()</CODE></A>
 914  <DD> Reads the minDead parameter of the manager.
 915
 916  <DT> <A HREF="cuddAllDet.html#Cudd_ReadReorderings" TARGET="MAIN"><CODE>Cudd_ReadReorderings()</CODE></A>
 917  <DD> Returns the number of times reordering has occurred.
 918
 919  <DT> <A HREF="cuddAllDet.html#Cudd_ReadReorderingTime" TARGET="MAIN"><CODE>Cudd_ReadReorderingTime()</CODE></A>
 920  <DD> Returns the time spent in reordering.
 921
 922  <DT> <A HREF="cuddAllDet.html#Cudd_ReadGarbageCollections" TARGET="MAIN"><CODE>Cudd_ReadGarbageCollections()</CODE></A>
 923  <DD> Returns the number of times garbage collection has occurred.
 924
 925  <DT> <A HREF="cuddAllDet.html#Cudd_ReadGarbageCollectionTime" TARGET="MAIN"><CODE>Cudd_ReadGarbageCollectionTime()</CODE></A>
 926  <DD> Returns the time spent in garbage collection.
 927
 928  <DT> <A HREF="cuddAllDet.html#Cudd_ReadNodesFreed" TARGET="MAIN"><CODE>Cudd_ReadNodesFreed()</CODE></A>
 929  <DD> Returns the number of nodes freed.
 930
 931  <DT> <A HREF="cuddAllDet.html#Cudd_ReadNodesDropped" TARGET="MAIN"><CODE>Cudd_ReadNodesDropped()</CODE></A>
 932  <DD> Returns the number of nodes dropped.
 933
 934  <DT> <A HREF="cuddAllDet.html#Cudd_ReadUniqueLookUps" TARGET="MAIN"><CODE>Cudd_ReadUniqueLookUps()</CODE></A>
 935  <DD> Returns the number of look-ups in the unique table.
 936
 937  <DT> <A HREF="cuddAllDet.html#Cudd_ReadUniqueLinks" TARGET="MAIN"><CODE>Cudd_ReadUniqueLinks()</CODE></A>
 938  <DD> Returns the number of links followed in the unique table.
 939
 940  <DT> <A HREF="cuddAllDet.html#Cudd_ReadSiftMaxVar" TARGET="MAIN"><CODE>Cudd_ReadSiftMaxVar()</CODE></A>
 941  <DD> Reads the siftMaxVar parameter of the manager.
 942
 943  <DT> <A HREF="cuddAllDet.html#Cudd_SetSiftMaxVar" TARGET="MAIN"><CODE>Cudd_SetSiftMaxVar()</CODE></A>
 944  <DD> Sets the siftMaxVar parameter of the manager.
 945
 946  <DT> <A HREF="cuddAllDet.html#Cudd_ReadSiftMaxSwap" TARGET="MAIN"><CODE>Cudd_ReadSiftMaxSwap()</CODE></A>
 947  <DD> Reads the siftMaxSwap parameter of the manager.
 948
 949  <DT> <A HREF="cuddAllDet.html#Cudd_SetSiftMaxSwap" TARGET="MAIN"><CODE>Cudd_SetSiftMaxSwap()</CODE></A>
 950  <DD> Sets the siftMaxSwap parameter of the manager.
 951
 952  <DT> <A HREF="cuddAllDet.html#Cudd_ReadMaxGrowth" TARGET="MAIN"><CODE>Cudd_ReadMaxGrowth()</CODE></A>
 953  <DD> Reads the maxGrowth parameter of the manager.
 954
 955  <DT> <A HREF="cuddAllDet.html#Cudd_SetMaxGrowth" TARGET="MAIN"><CODE>Cudd_SetMaxGrowth()</CODE></A>
 956  <DD> Sets the maxGrowth parameter of the manager.
 957
 958  <DT> <A HREF="cuddAllDet.html#Cudd_ReadMaxGrowthAlternate" TARGET="MAIN"><CODE>Cudd_ReadMaxGrowthAlternate()</CODE></A>
 959  <DD> Reads the maxGrowthAlt parameter of the manager.
 960
 961  <DT> <A HREF="cuddAllDet.html#Cudd_SetMaxGrowthAlternate" TARGET="MAIN"><CODE>Cudd_SetMaxGrowthAlternate()</CODE></A>
 962  <DD> Sets the maxGrowthAlt parameter of the manager.
 963
 964  <DT> <A HREF="cuddAllDet.html#Cudd_ReadReorderingCycle" TARGET="MAIN"><CODE>Cudd_ReadReorderingCycle()</CODE></A>
 965  <DD> Reads the reordCycle parameter of the manager.
 966
 967  <DT> <A HREF="cuddAllDet.html#Cudd_SetReorderingCycle" TARGET="MAIN"><CODE>Cudd_SetReorderingCycle()</CODE></A>
 968  <DD> Sets the reordCycle parameter of the manager.
 969
 970  <DT> <A HREF="cuddAllDet.html#Cudd_ReadTree" TARGET="MAIN"><CODE>Cudd_ReadTree()</CODE></A>
 971  <DD> Returns the variable group tree of the manager.
 972
 973  <DT> <A HREF="cuddAllDet.html#Cudd_SetTree" TARGET="MAIN"><CODE>Cudd_SetTree()</CODE></A>
 974  <DD> Sets the variable group tree of the manager.
 975
 976  <DT> <A HREF="cuddAllDet.html#Cudd_FreeTree" TARGET="MAIN"><CODE>Cudd_FreeTree()</CODE></A>
 977  <DD> Frees the variable group tree of the manager.
 978
 979  <DT> <A HREF="cuddAllDet.html#Cudd_ReadZddTree" TARGET="MAIN"><CODE>Cudd_ReadZddTree()</CODE></A>
 980  <DD> Returns the variable group tree of the manager.
 981
 982  <DT> <A HREF="cuddAllDet.html#Cudd_SetZddTree" TARGET="MAIN"><CODE>Cudd_SetZddTree()</CODE></A>
 983  <DD> Sets the ZDD variable group tree of the manager.
 984
 985  <DT> <A HREF="cuddAllDet.html#Cudd_FreeZddTree" TARGET="MAIN"><CODE>Cudd_FreeZddTree()</CODE></A>
 986  <DD> Frees the variable group tree of the manager.
 987
 988  <DT> <A HREF="cuddAllDet.html#Cudd_NodeReadIndex" TARGET="MAIN"><CODE>Cudd_NodeReadIndex()</CODE></A>
 989  <DD> Returns the index of the node.
 990
 991  <DT> <A HREF="cuddAllDet.html#Cudd_ReadPerm" TARGET="MAIN"><CODE>Cudd_ReadPerm()</CODE></A>
 992  <DD> Returns the current position of the i-th variable in the
 993   order.
 994
 995  <DT> <A HREF="cuddAllDet.html#Cudd_ReadPermZdd" TARGET="MAIN"><CODE>Cudd_ReadPermZdd()</CODE></A>
 996  <DD> Returns the current position of the i-th ZDD variable in the
 997   order.
 998
 999  <DT> <A HREF="cuddAllDet.html#Cudd_ReadInvPerm" TARGET="MAIN"><CODE>Cudd_ReadInvPerm()</CODE></A>
1000  <DD> Returns the index of the variable currently in the i-th
1001   position of the order.
1002
1003  <DT> <A HREF="cuddAllDet.html#Cudd_ReadInvPermZdd" TARGET="MAIN"><CODE>Cudd_ReadInvPermZdd()</CODE></A>
1004  <DD> Returns the index of the ZDD variable currently in the i-th
1005   position of the order.
1006
1007  <DT> <A HREF="cuddAllDet.html#Cudd_ReadVars" TARGET="MAIN"><CODE>Cudd_ReadVars()</CODE></A>
1008  <DD> Returns the i-th element of the vars array.
1009
1010  <DT> <A HREF="cuddAllDet.html#Cudd_ReadEpsilon" TARGET="MAIN"><CODE>Cudd_ReadEpsilon()</CODE></A>
1011  <DD> Reads the epsilon parameter of the manager.
1012
1013  <DT> <A HREF="cuddAllDet.html#Cudd_SetEpsilon" TARGET="MAIN"><CODE>Cudd_SetEpsilon()</CODE></A>
1014  <DD> Sets the epsilon parameter of the manager to ep.
1015
1016  <DT> <A HREF="cuddAllDet.html#Cudd_ReadGroupcheck" TARGET="MAIN"><CODE>Cudd_ReadGroupcheck()</CODE></A>
1017  <DD> Reads the groupcheck parameter of the manager.
1018
1019  <DT> <A HREF="cuddAllDet.html#Cudd_SetGroupcheck" TARGET="MAIN"><CODE>Cudd_SetGroupcheck()</CODE></A>
1020  <DD> Sets the parameter groupcheck of the manager to gc.
1021
1022  <DT> <A HREF="cuddAllDet.html#Cudd_GarbageCollectionEnabled" TARGET="MAIN"><CODE>Cudd_GarbageCollectionEnabled()</CODE></A>
1023  <DD> Tells whether garbage collection is enabled.
1024
1025  <DT> <A HREF="cuddAllDet.html#Cudd_EnableGarbageCollection" TARGET="MAIN"><CODE>Cudd_EnableGarbageCollection()</CODE></A>
1026  <DD> Enables garbage collection.
1027
1028  <DT> <A HREF="cuddAllDet.html#Cudd_DisableGarbageCollection" TARGET="MAIN"><CODE>Cudd_DisableGarbageCollection()</CODE></A>
1029  <DD> Disables garbage collection.
1030
1031  <DT> <A HREF="cuddAllDet.html#Cudd_DeadAreCounted" TARGET="MAIN"><CODE>Cudd_DeadAreCounted()</CODE></A>
1032  <DD> Tells whether dead nodes are counted towards triggering
1033   reordering.
1034
1035  <DT> <A HREF="cuddAllDet.html#Cudd_TurnOnCountDead" TARGET="MAIN"><CODE>Cudd_TurnOnCountDead()</CODE></A>
1036  <DD> Causes the dead nodes to be counted towards triggering
1037   reordering.
1038
1039  <DT> <A HREF="cuddAllDet.html#Cudd_TurnOffCountDead" TARGET="MAIN"><CODE>Cudd_TurnOffCountDead()</CODE></A>
1040  <DD> Causes the dead nodes not to be counted towards triggering
1041   reordering.
1042
1043  <DT> <A HREF="cuddAllDet.html#Cudd_ReadRecomb" TARGET="MAIN"><CODE>Cudd_ReadRecomb()</CODE></A>
1044  <DD> Returns the current value of the recombination parameter used
1045   in group sifting.
1046
1047  <DT> <A HREF="cuddAllDet.html#Cudd_SetRecomb" TARGET="MAIN"><CODE>Cudd_SetRecomb()</CODE></A>
1048  <DD> Sets the value of the recombination parameter used in group
1049   sifting.
1050
1051  <DT> <A HREF="cuddAllDet.html#Cudd_ReadSymmviolation" TARGET="MAIN"><CODE>Cudd_ReadSymmviolation()</CODE></A>
1052  <DD> Returns the current value of the symmviolation parameter used
1053   in group sifting.
1054
1055  <DT> <A HREF="cuddAllDet.html#Cudd_SetSymmviolation" TARGET="MAIN"><CODE>Cudd_SetSymmviolation()</CODE></A>
1056  <DD> Sets the value of the symmviolation parameter used
1057   in group sifting.
1058
1059  <DT> <A HREF="cuddAllDet.html#Cudd_ReadArcviolation" TARGET="MAIN"><CODE>Cudd_ReadArcviolation()</CODE></A>
1060  <DD> Returns the current value of the arcviolation parameter used
1061   in group sifting.
1062
1063  <DT> <A HREF="cuddAllDet.html#Cudd_SetArcviolation" TARGET="MAIN"><CODE>Cudd_SetArcviolation()</CODE></A>
1064  <DD> Sets the value of the arcviolation parameter used
1065   in group sifting.
1066
1067  <DT> <A HREF="cuddAllDet.html#Cudd_ReadPopulationSize" TARGET="MAIN"><CODE>Cudd_ReadPopulationSize()</CODE></A>
1068  <DD> Reads the current size of the population used by the
1069   genetic algorithm for reordering.
1070
1071  <DT> <A HREF="cuddAllDet.html#Cudd_SetPopulationSize" TARGET="MAIN"><CODE>Cudd_SetPopulationSize()</CODE></A>
1072  <DD> Sets the size of the population used by the
1073   genetic algorithm for reordering.
1074
1075  <DT> <A HREF="cuddAllDet.html#Cudd_ReadNumberXovers" TARGET="MAIN"><CODE>Cudd_ReadNumberXovers()</CODE></A>
1076  <DD> Reads the current number of crossovers used by the
1077   genetic algorithm for reordering.
1078
1079  <DT> <A HREF="cuddAllDet.html#Cudd_SetNumberXovers" TARGET="MAIN"><CODE>Cudd_SetNumberXovers()</CODE></A>
1080  <DD> Sets the number of crossovers used by the
1081   genetic algorithm for reordering.
1082
1083  <DT> <A HREF="cuddAllDet.html#Cudd_ReadMemoryInUse" TARGET="MAIN"><CODE>Cudd_ReadMemoryInUse()</CODE></A>
1084  <DD> Returns the memory in use by the manager measured in bytes.
1085
1086  <DT> <A HREF="cuddAllDet.html#Cudd_PrintInfo" TARGET="MAIN"><CODE>Cudd_PrintInfo()</CODE></A>
1087  <DD> Prints out statistics and settings for a CUDD manager.
1088
1089  <DT> <A HREF="cuddAllDet.html#Cudd_ReadPeakNodeCount" TARGET="MAIN"><CODE>Cudd_ReadPeakNodeCount()</CODE></A>
1090  <DD> Reports the peak number of nodes.
1091
1092  <DT> <A HREF="cuddAllDet.html#Cudd_ReadPeakLiveNodeCount" TARGET="MAIN"><CODE>Cudd_ReadPeakLiveNodeCount()</CODE></A>
1093  <DD> Reports the peak number of live nodes.
1094
1095  <DT> <A HREF="cuddAllDet.html#Cudd_ReadNodeCount" TARGET="MAIN"><CODE>Cudd_ReadNodeCount()</CODE></A>
1096  <DD> Reports the number of nodes in BDDs and ADDs.
1097
1098  <DT> <A HREF="cuddAllDet.html#Cudd_zddReadNodeCount" TARGET="MAIN"><CODE>Cudd_zddReadNodeCount()</CODE></A>
1099  <DD> Reports the number of nodes in ZDDs.
1100
1101  <DT> <A HREF="cuddAllDet.html#Cudd_AddHook" TARGET="MAIN"><CODE>Cudd_AddHook()</CODE></A>
1102  <DD> Adds a function to a hook.
1103
1104  <DT> <A HREF="cuddAllDet.html#Cudd_RemoveHook" TARGET="MAIN"><CODE>Cudd_RemoveHook()</CODE></A>
1105  <DD> Removes a function from a hook.
1106
1107  <DT> <A HREF="cuddAllDet.html#Cudd_IsInHook" TARGET="MAIN"><CODE>Cudd_IsInHook()</CODE></A>
1108  <DD> Checks whether a function is in a hook.
1109
1110  <DT> <A HREF="cuddAllDet.html#Cudd_StdPreReordHook" TARGET="MAIN"><CODE>Cudd_StdPreReordHook()</CODE></A>
1111  <DD> Sample hook function to call before reordering.
1112
1113  <DT> <A HREF="cuddAllDet.html#Cudd_StdPostReordHook" TARGET="MAIN"><CODE>Cudd_StdPostReordHook()</CODE></A>
1114  <DD> Sample hook function to call after reordering.
1115
1116  <DT> <A HREF="cuddAllDet.html#Cudd_EnableReorderingReporting" TARGET="MAIN"><CODE>Cudd_EnableReorderingReporting()</CODE></A>
1117  <DD> Enables reporting of reordering stats.
1118
1119  <DT> <A HREF="cuddAllDet.html#Cudd_DisableReorderingReporting" TARGET="MAIN"><CODE>Cudd_DisableReorderingReporting()</CODE></A>
1120  <DD> Disables reporting of reordering stats.
1121
1122  <DT> <A HREF="cuddAllDet.html#Cudd_ReorderingReporting" TARGET="MAIN"><CODE>Cudd_ReorderingReporting()</CODE></A>
1123  <DD> Returns 1 if reporting of reordering stats is enabled.
1124
1125  <DT> <A HREF="cuddAllDet.html#Cudd_ReadErrorCode" TARGET="MAIN"><CODE>Cudd_ReadErrorCode()</CODE></A>
1126  <DD> Returns the code of the last error.
1127
1128  <DT> <A HREF="cuddAllDet.html#Cudd_ClearErrorCode" TARGET="MAIN"><CODE>Cudd_ClearErrorCode()</CODE></A>
1129  <DD> Clear the error code of a manager.
1130
1131  <DT> <A HREF="cuddAllDet.html#Cudd_ReadStdout" TARGET="MAIN"><CODE>Cudd_ReadStdout()</CODE></A>
1132  <DD> Reads the stdout of a manager.
1133
1134  <DT> <A HREF="cuddAllDet.html#Cudd_SetStdout" TARGET="MAIN"><CODE>Cudd_SetStdout()</CODE></A>
1135  <DD> Sets the stdout of a manager.
1136
1137  <DT> <A HREF="cuddAllDet.html#Cudd_ReadStderr" TARGET="MAIN"><CODE>Cudd_ReadStderr()</CODE></A>
1138  <DD> Reads the stderr of a manager.
1139
1140  <DT> <A HREF="cuddAllDet.html#Cudd_SetStderr" TARGET="MAIN"><CODE>Cudd_SetStderr()</CODE></A>
1141  <DD> Sets the stderr of a manager.
1142
1143  <DT> <A HREF="cuddAllDet.html#Cudd_ReadNextReordering" TARGET="MAIN"><CODE>Cudd_ReadNextReordering()</CODE></A>
1144  <DD> Returns the threshold for the next dynamic reordering.
1145
1146  <DT> <A HREF="cuddAllDet.html#Cudd_SetNextReordering" TARGET="MAIN"><CODE>Cudd_SetNextReordering()</CODE></A>
1147  <DD> Sets the threshold for the next dynamic reordering.
1148
1149  <DT> <A HREF="cuddAllDet.html#Cudd_ReadSwapSteps" TARGET="MAIN"><CODE>Cudd_ReadSwapSteps()</CODE></A>
1150  <DD> Reads the number of elementary reordering steps.
1151
1152  <DT> <A HREF="cuddAllDet.html#Cudd_ReadMaxLive" TARGET="MAIN"><CODE>Cudd_ReadMaxLive()</CODE></A>
1153  <DD> Reads the maximum allowed number of live nodes.
1154
1155  <DT> <A HREF="cuddAllDet.html#Cudd_SetMaxLive" TARGET="MAIN"><CODE>Cudd_SetMaxLive()</CODE></A>
1156  <DD> Sets the maximum allowed number of live nodes.
1157
1158  <DT> <A HREF="cuddAllDet.html#Cudd_ReadMaxMemory" TARGET="MAIN"><CODE>Cudd_ReadMaxMemory()</CODE></A>
1159  <DD> Reads the maximum allowed memory.
1160
1161  <DT> <A HREF="cuddAllDet.html#Cudd_SetMaxMemory" TARGET="MAIN"><CODE>Cudd_SetMaxMemory()</CODE></A>
1162  <DD> Sets the maximum allowed memory.
1163
1164  <DT> <A HREF="cuddAllDet.html#Cudd_bddBindVar" TARGET="MAIN"><CODE>Cudd_bddBindVar()</CODE></A>
1165  <DD> Prevents sifting of a variable.
1166
1167  <DT> <A HREF="cuddAllDet.html#Cudd_bddUnbindVar" TARGET="MAIN"><CODE>Cudd_bddUnbindVar()</CODE></A>
1168  <DD> Allows the sifting of a variable.
1169
1170  <DT> <A HREF="cuddAllDet.html#Cudd_bddVarIsBound" TARGET="MAIN"><CODE>Cudd_bddVarIsBound()</CODE></A>
1171  <DD> Tells whether a variable can be sifted.
1172
1173  <DT> <A HREF="cuddAllDet.html#Cudd_bddSetPiVar" TARGET="MAIN"><CODE>Cudd_bddSetPiVar()</CODE></A>
1174  <DD> Sets a variable type to primary input.
1175
1176  <DT> <A HREF="cuddAllDet.html#Cudd_bddSetPsVar" TARGET="MAIN"><CODE>Cudd_bddSetPsVar()</CODE></A>
1177  <DD> Sets a variable type to present state.
1178
1179  <DT> <A HREF="cuddAllDet.html#Cudd_bddSetNsVar" TARGET="MAIN"><CODE>Cudd_bddSetNsVar()</CODE></A>
1180  <DD> Sets a variable type to next state.
1181
1182  <DT> <A HREF="cuddAllDet.html#Cudd_bddIsPiVar" TARGET="MAIN"><CODE>Cudd_bddIsPiVar()</CODE></A>
1183  <DD> Checks whether a variable is primary input.
1184
1185  <DT> <A HREF="cuddAllDet.html#Cudd_bddIsPsVar" TARGET="MAIN"><CODE>Cudd_bddIsPsVar()</CODE></A>
1186  <DD> Checks whether a variable is present state.
1187
1188  <DT> <A HREF="cuddAllDet.html#Cudd_bddIsNsVar" TARGET="MAIN"><CODE>Cudd_bddIsNsVar()</CODE></A>
1189  <DD> Checks whether a variable is next state.
1190
1191  <DT> <A HREF="cuddAllDet.html#Cudd_bddSetPairIndex" TARGET="MAIN"><CODE>Cudd_bddSetPairIndex()</CODE></A>
1192  <DD> Sets a corresponding pair index for a given index.
1193
1194  <DT> <A HREF="cuddAllDet.html#Cudd_bddReadPairIndex" TARGET="MAIN"><CODE>Cudd_bddReadPairIndex()</CODE></A>
1195  <DD> Reads a corresponding pair index for a given index.
1196
1197  <DT> <A HREF="cuddAllDet.html#Cudd_bddSetVarToBeGrouped" TARGET="MAIN"><CODE>Cudd_bddSetVarToBeGrouped()</CODE></A>
1198  <DD> Sets a variable to be grouped.
1199
1200  <DT> <A HREF="cuddAllDet.html#Cudd_bddSetVarHardGroup" TARGET="MAIN"><CODE>Cudd_bddSetVarHardGroup()</CODE></A>
1201  <DD> Sets a variable to be a hard group.
1202
1203  <DT> <A HREF="cuddAllDet.html#Cudd_bddResetVarToBeGrouped" TARGET="MAIN"><CODE>Cudd_bddResetVarToBeGrouped()</CODE></A>
1204  <DD> Resets a variable not to be grouped.
1205
1206  <DT> <A HREF="cuddAllDet.html#Cudd_bddIsVarToBeGrouped" TARGET="MAIN"><CODE>Cudd_bddIsVarToBeGrouped()</CODE></A>
1207  <DD> Checks whether a variable is set to be grouped.
1208
1209  <DT> <A HREF="cuddAllDet.html#Cudd_bddSetVarToBeUngrouped" TARGET="MAIN"><CODE>Cudd_bddSetVarToBeUngrouped()</CODE></A>
1210  <DD> Sets a variable to be ungrouped.
1211
1212  <DT> <A HREF="cuddAllDet.html#Cudd_bddIsVarToBeUngrouped" TARGET="MAIN"><CODE>Cudd_bddIsVarToBeUngrouped()</CODE></A>
1213  <DD> Checks whether a variable is set to be ungrouped.
1214
1215  <DT> <A HREF="cuddAllDet.html#Cudd_bddIsVarHardGroup" TARGET="MAIN"><CODE>Cudd_bddIsVarHardGroup()</CODE></A>
1216  <DD> Checks whether a variable is set to be in a hard group.
1217
1218  <DT> <A HREF="cuddAllDet.html#fixVarTree" TARGET="MAIN"><CODE>fixVarTree()</CODE></A>
1219  <DD> Fixes a variable group tree.
1220
1221  <DT> <A HREF="cuddAllDet.html#addMultiplicityGroups" TARGET="MAIN"><CODE>addMultiplicityGroups()</CODE></A>
1222  <DD> Adds multiplicity groups to a ZDD variable group tree.
1223
1224 </DL>
1225 <HR>
1226 <A NAME="cuddApprox.c"><H1>cuddApprox.c</H1></A>
1227 Procedures to approximate a given BDD. <P>
1228 <B>By: Fabio Somenzi</B><P>
1229 External procedures provided by this module:
1230                 <ul>
1231                 <li> Cudd_UnderApprox()
1232                 <li> Cudd_OverApprox()
1233                 <li> Cudd_RemapUnderApprox()
1234                 <li> Cudd_RemapOverApprox()
1235                 <li> Cudd_BiasedUnderApprox()
1236                 <li> Cudd_BiasedOverApprox()
1237                 </ul>
1238                Internal procedures included in this module:
1239                 <ul>
1240                 <li> cuddUnderApprox()
1241                 <li> cuddRemapUnderApprox()
1242                 <li> cuddBiasedUnderApprox()
1243                 </ul>
1244                Static procedures included in this module:
1245                 <ul>
1246                 <li> gatherInfoAux()
1247                 <li> gatherInfo()
1248                 <li> computeSavings()
1249                 <li> UAmarkNodes()
1250                 <li> UAbuildSubset()
1251                 <li> updateRefs()
1252                 <li> RAmarkNodes()
1253                 <li> BAmarkNodes()
1254                 <li> RAbuildSubset()
1255                 </ul> <P>
1256 <P><B>See Also</B><A HREF="#cuddSubsetHB.c"><CODE>cuddSubsetHB.c</CODE></A>
1257 <A HREF="#cuddSubsetSP.c"><CODE>cuddSubsetSP.c</CODE></A>
1258 <A HREF="#cuddGenCof.c"><CODE>cuddGenCof.c</CODE></A>
1259 <DL>
1260  <DT> <A HREF="cuddAllDet.html#Cudd_UnderApprox" TARGET="MAIN"><CODE>Cudd_UnderApprox()</CODE></A>
1261  <DD> Extracts a dense subset from a BDD with Shiple's
1262   underapproximation method.
1263
1264  <DT> <A HREF="cuddAllDet.html#Cudd_OverApprox" TARGET="MAIN"><CODE>Cudd_OverApprox()</CODE></A>
1265  <DD> Extracts a dense superset from a BDD with Shiple's
1266   underapproximation method.
1267
1268  <DT> <A HREF="cuddAllDet.html#Cudd_RemapUnderApprox" TARGET="MAIN"><CODE>Cudd_RemapUnderApprox()</CODE></A>
1269  <DD> Extracts a dense subset from a BDD with the remapping
1270   underapproximation method.
1271
1272  <DT> <A HREF="cuddAllDet.html#Cudd_RemapOverApprox" TARGET="MAIN"><CODE>Cudd_RemapOverApprox()</CODE></A>
1273  <DD> Extracts a dense superset from a BDD with the remapping
1274   underapproximation method.
1275
1276  <DT> <A HREF="cuddAllDet.html#Cudd_BiasedUnderApprox" TARGET="MAIN"><CODE>Cudd_BiasedUnderApprox()</CODE></A>
1277  <DD> Extracts a dense subset from a BDD with the biased
1278   underapproximation method.
1279
1280  <DT> <A HREF="cuddAllDet.html#Cudd_BiasedOverApprox" TARGET="MAIN"><CODE>Cudd_BiasedOverApprox()</CODE></A>
1281  <DD> Extracts a dense superset from a BDD with the biased
1282   underapproximation method.
1283
1284  <DT> <A HREF="cuddAllDet.html#cuddUnderApprox" TARGET="MAIN"><CODE>cuddUnderApprox()</CODE></A>
1285  <DD> Applies Tom Shiple's underappoximation algorithm.
1286
1287  <DT> <A HREF="cuddAllDet.html#cuddRemapUnderApprox" TARGET="MAIN"><CODE>cuddRemapUnderApprox()</CODE></A>
1288  <DD> Applies the remapping underappoximation algorithm.
1289
1290  <DT> <A HREF="cuddAllDet.html#cuddBiasedUnderApprox" TARGET="MAIN"><CODE>cuddBiasedUnderApprox()</CODE></A>
1291  <DD> Applies the biased remapping underappoximation algorithm.
1292
1293  <DT> <A HREF="cuddAllDet.html#updateParity" TARGET="MAIN"><CODE>updateParity()</CODE></A>
1294  <DD> Recursively update the parity of the paths reaching a node.
1295
1296  <DT> <A HREF="cuddAllDet.html#gatherInfoAux" TARGET="MAIN"><CODE>gatherInfoAux()</CODE></A>
1297  <DD> Recursively counts minterms and computes reference counts
1298   of each node in the BDD.
1299
1300  <DT> <A HREF="cuddAllDet.html#gatherInfo" TARGET="MAIN"><CODE>gatherInfo()</CODE></A>
1301  <DD> Gathers information about each node.
1302
1303  <DT> <A HREF="cuddAllDet.html#computeSavings" TARGET="MAIN"><CODE>computeSavings()</CODE></A>
1304  <DD> Counts the nodes that would be eliminated if a given node
1305   were replaced by zero.
1306
1307  <DT> <A HREF="cuddAllDet.html#updateRefs" TARGET="MAIN"><CODE>updateRefs()</CODE></A>
1308  <DD> Update function reference counts.
1309
1310  <DT> <A HREF="cuddAllDet.html#UAmarkNodes" TARGET="MAIN"><CODE>UAmarkNodes()</CODE></A>
1311  <DD> Marks nodes for replacement by zero.
1312
1313  <DT> <A HREF="cuddAllDet.html#UAbuildSubset" TARGET="MAIN"><CODE>UAbuildSubset()</CODE></A>
1314  <DD> Builds the subset BDD.
1315
1316  <DT> <A HREF="cuddAllDet.html#RAmarkNodes" TARGET="MAIN"><CODE>RAmarkNodes()</CODE></A>
1317  <DD> Marks nodes for remapping.
1318
1319  <DT> <A HREF="cuddAllDet.html#BAmarkNodes" TARGET="MAIN"><CODE>BAmarkNodes()</CODE></A>
1320  <DD> Marks nodes for remapping.
1321
1322  <DT> <A HREF="cuddAllDet.html#RAbuildSubset" TARGET="MAIN"><CODE>RAbuildSubset()</CODE></A>
1323  <DD> Builds the subset BDD for cuddRemapUnderApprox.
1324
1325  <DT> <A HREF="cuddAllDet.html#BAapplyBias" TARGET="MAIN"><CODE>BAapplyBias()</CODE></A>
1326  <DD> Finds don't care nodes.
1327
1328 </DL>
1329 <HR>
1330 <A NAME="cuddBddAbs.c"><H1>cuddBddAbs.c</H1></A>
1331 Quantification functions for BDDs. <P>
1332 <B>By: Fabio Somenzi</B><P>
1333 External procedures included in this module:
1334                 <ul>
1335                 <li> Cudd_bddExistAbstract()
1336                 <li> Cudd_bddXorExistAbstract()
1337                 <li> Cudd_bddUnivAbstract()
1338                 <li> Cudd_bddBooleanDiff()
1339                 <li> Cudd_bddVarIsDependent()
1340                 </ul>
1341         Internal procedures included in this module:
1342                 <ul>
1343                 <li> cuddBddExistAbstractRecur()
1344                 <li> cuddBddXorExistAbstractRecur()
1345                 <li> cuddBddBooleanDiffRecur()
1346                 </ul>
1347         Static procedures included in this module:
1348                 <ul>
1349                 <li> bddCheckPositiveCube()
1350                 </ul> <P>
1351 <DL>
1352  <DT> <A HREF="cuddAllDet.html#Cudd_bddExistAbstract" TARGET="MAIN"><CODE>Cudd_bddExistAbstract()</CODE></A>
1353  <DD> Existentially abstracts all the variables in cube from f.
1354
1355  <DT> <A HREF="cuddAllDet.html#Cudd_bddXorExistAbstract" TARGET="MAIN"><CODE>Cudd_bddXorExistAbstract()</CODE></A>
1356  <DD> Takes the exclusive OR of two BDDs and simultaneously abstracts the
1357   variables in cube.
1358
1359  <DT> <A HREF="cuddAllDet.html#Cudd_bddUnivAbstract" TARGET="MAIN"><CODE>Cudd_bddUnivAbstract()</CODE></A>
1360  <DD> Universally abstracts all the variables in cube from f.
1361
1362  <DT> <A HREF="cuddAllDet.html#Cudd_bddBooleanDiff" TARGET="MAIN"><CODE>Cudd_bddBooleanDiff()</CODE></A>
1363  <DD> Computes the boolean difference of f with respect to x.
1364
1365  <DT> <A HREF="cuddAllDet.html#Cudd_bddVarIsDependent" TARGET="MAIN"><CODE>Cudd_bddVarIsDependent()</CODE></A>
1366  <DD> Checks whether a variable is dependent on others in a
1367   function.
1368
1369  <DT> <A HREF="cuddAllDet.html#cuddBddExistAbstractRecur" TARGET="MAIN"><CODE>cuddBddExistAbstractRecur()</CODE></A>
1370  <DD> Performs the recursive steps of Cudd_bddExistAbstract.
1371
1372  <DT> <A HREF="cuddAllDet.html#cuddBddXorExistAbstractRecur" TARGET="MAIN"><CODE>cuddBddXorExistAbstractRecur()</CODE></A>
1373  <DD> Takes the exclusive OR of two BDDs and simultaneously abstracts the
1374   variables in cube.
1375
1376  <DT> <A HREF="cuddAllDet.html#cuddBddBooleanDiffRecur" TARGET="MAIN"><CODE>cuddBddBooleanDiffRecur()</CODE></A>
1377  <DD> Performs the recursive steps of Cudd_bddBoleanDiff.
1378
1379  <DT> <A HREF="cuddAllDet.html#bddCheckPositiveCube" TARGET="MAIN"><CODE>bddCheckPositiveCube()</CODE></A>
1380  <DD> Checks whether cube is an BDD representing the product of
1381   positive literals.
1382
1383 </DL>
1384 <HR>
1385 <A NAME="cuddBddCorr.c"><H1>cuddBddCorr.c</H1></A>
1386 Correlation between BDDs. <P>
1387 <B>By: Fabio Somenzi</B><P>
1388 External procedures included in this module:
1389                 <ul>
1390                 <li> Cudd_bddCorrelation()
1391                 <li> Cudd_bddCorrelationWeights()
1392                 </ul>
1393             Static procedures included in this module:
1394                 <ul>
1395                 <li> bddCorrelationAux()
1396                 <li> bddCorrelationWeightsAux()
1397                 <li> CorrelCompare()
1398                 <li> CorrelHash()
1399                 <li> CorrelCleanUp()
1400                 </ul> <P>
1401 <DL>
1402  <DT> <A HREF="cuddAllDet.html#Cudd_bddCorrelation" TARGET="MAIN"><CODE>Cudd_bddCorrelation()</CODE></A>
1403  <DD> Computes the correlation of f and g.
1404
1405  <DT> <A HREF="cuddAllDet.html#Cudd_bddCorrelationWeights" TARGET="MAIN"><CODE>Cudd_bddCorrelationWeights()</CODE></A>
1406  <DD> Computes the correlation of f and g for given input
1407   probabilities.
1408
1409  <DT> <A HREF="cuddAllDet.html#bddCorrelationAux" TARGET="MAIN"><CODE>bddCorrelationAux()</CODE></A>
1410  <DD> Performs the recursive step of Cudd_bddCorrelation.
1411
1412  <DT> <A HREF="cuddAllDet.html#bddCorrelationWeightsAux" TARGET="MAIN"><CODE>bddCorrelationWeightsAux()</CODE></A>
1413  <DD> Performs the recursive step of Cudd_bddCorrelationWeigths.
1414
1415  <DT> <A HREF="cuddAllDet.html#CorrelCompare" TARGET="MAIN"><CODE>CorrelCompare()</CODE></A>
1416  <DD> Compares two hash table entries.
1417
1418  <DT> <A HREF="cuddAllDet.html#CorrelHash" TARGET="MAIN"><CODE>CorrelHash()</CODE></A>
1419  <DD> Hashes a hash table entry.
1420
1421  <DT> <A HREF="cuddAllDet.html#CorrelCleanUp" TARGET="MAIN"><CODE>CorrelCleanUp()</CODE></A>
1422  <DD> Frees memory associated with hash table.
1423
1424 </DL>
1425 <HR>
1426 <A NAME="cuddBddIte.c"><H1>cuddBddIte.c</H1></A>
1427 BDD ITE function and satellites. <P>
1428 <B>By: Fabio Somenzi</B><P>
1429 External procedures included in this module:
1430                 <ul>
1431                 <li> Cudd_bddIte()
1432                 <li> Cudd_bddIteConstant()
1433                 <li> Cudd_bddIntersect()
1434                 <li> Cudd_bddAnd()
1435                 <li> Cudd_bddAndLimit()
1436                 <li> Cudd_bddOr()
1437                 <li> Cudd_bddNand()
1438                 <li> Cudd_bddNor()
1439                 <li> Cudd_bddXor()
1440                 <li> Cudd_bddXnor()
1441                 <li> Cudd_bddLeq()
1442                 </ul>
1443        Internal procedures included in this module:
1444                 <ul>
1445                 <li> cuddBddIteRecur()
1446                 <li> cuddBddIntersectRecur()
1447                 <li> cuddBddAndRecur()
1448                 <li> cuddBddXorRecur()
1449                 </ul>
1450        Static procedures included in this module:
1451                 <ul>
1452                 <li> bddVarToConst()
1453                 <li> bddVarToCanonical()
1454                 <li> bddVarToCanonicalSimple()
1455                 </ul> <P>
1456 <DL>
1457  <DT> <A HREF="cuddAllDet.html#Cudd_bddIte" TARGET="MAIN"><CODE>Cudd_bddIte()</CODE></A>
1458  <DD> Implements ITE(f,g,h).
1459
1460  <DT> <A HREF="cuddAllDet.html#Cudd_bddIteConstant" TARGET="MAIN"><CODE>Cudd_bddIteConstant()</CODE></A>
1461  <DD> Implements ITEconstant(f,g,h).
1462
1463  <DT> <A HREF="cuddAllDet.html#Cudd_bddIntersect" TARGET="MAIN"><CODE>Cudd_bddIntersect()</CODE></A>
1464  <DD> Returns a function included in the intersection of f and g.
1465
1466  <DT> <A HREF="cuddAllDet.html#Cudd_bddAnd" TARGET="MAIN"><CODE>Cudd_bddAnd()</CODE></A>
1467  <DD> Computes the conjunction of two BDDs f and g.
1468
1469  <DT> <A HREF="cuddAllDet.html#Cudd_bddAndLimit" TARGET="MAIN"><CODE>Cudd_bddAndLimit()</CODE></A>
1470  <DD> Computes the conjunction of two BDDs f and g.  Returns
1471   NULL if too many nodes are required.
1472
1473  <DT> <A HREF="cuddAllDet.html#Cudd_bddOr" TARGET="MAIN"><CODE>Cudd_bddOr()</CODE></A>
1474  <DD> Computes the disjunction of two BDDs f and g.
1475
1476  <DT> <A HREF="cuddAllDet.html#Cudd_bddNand" TARGET="MAIN"><CODE>Cudd_bddNand()</CODE></A>
1477  <DD> Computes the NAND of two BDDs f and g.
1478
1479  <DT> <A HREF="cuddAllDet.html#Cudd_bddNor" TARGET="MAIN"><CODE>Cudd_bddNor()</CODE></A>
1480  <DD> Computes the NOR of two BDDs f and g.
1481
1482  <DT> <A HREF="cuddAllDet.html#Cudd_bddXor" TARGET="MAIN"><CODE>Cudd_bddXor()</CODE></A>
1483  <DD> Computes the exclusive OR of two BDDs f and g.
1484
1485  <DT> <A HREF="cuddAllDet.html#Cudd_bddXnor" TARGET="MAIN"><CODE>Cudd_bddXnor()</CODE></A>
1486  <DD> Computes the exclusive NOR of two BDDs f and g.
1487
1488  <DT> <A HREF="cuddAllDet.html#Cudd_bddLeq" TARGET="MAIN"><CODE>Cudd_bddLeq()</CODE></A>
1489  <DD> Determines whether f is less than or equal to g.
1490
1491  <DT> <A HREF="cuddAllDet.html#cuddBddIteRecur" TARGET="MAIN"><CODE>cuddBddIteRecur()</CODE></A>
1492  <DD> Implements the recursive step of Cudd_bddIte.
1493
1494  <DT> <A HREF="cuddAllDet.html#cuddBddIntersectRecur" TARGET="MAIN"><CODE>cuddBddIntersectRecur()</CODE></A>
1495  <DD> Implements the recursive step of Cudd_bddIntersect.
1496
1497  <DT> <A HREF="cuddAllDet.html#cuddBddAndRecur" TARGET="MAIN"><CODE>cuddBddAndRecur()</CODE></A>
1498  <DD> Implements the recursive step of Cudd_bddAnd.
1499
1500  <DT> <A HREF="cuddAllDet.html#cuddBddXorRecur" TARGET="MAIN"><CODE>cuddBddXorRecur()</CODE></A>
1501  <DD> Implements the recursive step of Cudd_bddXor.
1502
1503  <DT> <A HREF="cuddAllDet.html#bddVarToConst" TARGET="MAIN"><CODE>bddVarToConst()</CODE></A>
1504  <DD> Replaces variables with constants if possible.
1505
1506  <DT> <A HREF="cuddAllDet.html#bddVarToCanonical" TARGET="MAIN"><CODE>bddVarToCanonical()</CODE></A>
1507  <DD> Picks unique member from equiv expressions.
1508
1509  <DT> <A HREF="cuddAllDet.html#bddVarToCanonicalSimple" TARGET="MAIN"><CODE>bddVarToCanonicalSimple()</CODE></A>
1510  <DD> Picks unique member from equiv expressions.
1511
1512 </DL>
1513 <HR>
1514 <A NAME="cuddBridge.c"><H1>cuddBridge.c</H1></A>
1515 Translation from BDD to ADD and vice versa and transfer between
1516   different managers. <P>
1517 <B>By: Fabio Somenzi</B><P>
1518 External procedures included in this file:
1519             <ul>
1520             <li> Cudd_addBddThreshold()
1521             <li> Cudd_addBddStrictThreshold()
1522             <li> Cudd_addBddInterval()
1523             <li> Cudd_addBddIthBit()
1524             <li> Cudd_BddToAdd()
1525             <li> Cudd_addBddPattern()
1526             <li> Cudd_bddTransfer()
1527             </ul>
1528         Internal procedures included in this file:
1529             <ul>
1530             <li> cuddBddTransfer()
1531             <li> cuddAddBddDoPattern()
1532             </ul>
1533         Static procedures included in this file:
1534             <ul>
1535             <li> addBddDoThreshold()
1536             <li> addBddDoStrictThreshold()
1537             <li> addBddDoInterval()
1538             <li> addBddDoIthBit()
1539             <li> ddBddToAddRecur()
1540             <li> cuddBddTransferRecur()
1541             </ul> <P>
1542 <DL>
1543  <DT> <A HREF="cuddAllDet.html#Cudd_addBddThreshold" TARGET="MAIN"><CODE>Cudd_addBddThreshold()</CODE></A>
1544  <DD> Converts an ADD to a BDD.
1545
1546  <DT> <A HREF="cuddAllDet.html#Cudd_addBddStrictThreshold" TARGET="MAIN"><CODE>Cudd_addBddStrictThreshold()</CODE></A>
1547  <DD> Converts an ADD to a BDD.
1548
1549  <DT> <A HREF="cuddAllDet.html#Cudd_addBddInterval" TARGET="MAIN"><CODE>Cudd_addBddInterval()</CODE></A>
1550  <DD> Converts an ADD to a BDD.
1551
1552  <DT> <A HREF="cuddAllDet.html#Cudd_addBddIthBit" TARGET="MAIN"><CODE>Cudd_addBddIthBit()</CODE></A>
1553  <DD> Converts an ADD to a BDD by extracting the i-th bit from
1554   the leaves.
1555
1556  <DT> <A HREF="cuddAllDet.html#Cudd_BddToAdd" TARGET="MAIN"><CODE>Cudd_BddToAdd()</CODE></A>
1557  <DD> Converts a BDD to a 0-1 ADD.
1558
1559  <DT> <A HREF="cuddAllDet.html#Cudd_addBddPattern" TARGET="MAIN"><CODE>Cudd_addBddPattern()</CODE></A>
1560  <DD> Converts an ADD to a BDD.
1561
1562  <DT> <A HREF="cuddAllDet.html#Cudd_bddTransfer" TARGET="MAIN"><CODE>Cudd_bddTransfer()</CODE></A>
1563  <DD> Convert a BDD from a manager to another one.
1564
1565  <DT> <A HREF="cuddAllDet.html#cuddBddTransfer" TARGET="MAIN"><CODE>cuddBddTransfer()</CODE></A>
1566  <DD> Convert a BDD from a manager to another one.
1567
1568  <DT> <A HREF="cuddAllDet.html#cuddAddBddDoPattern" TARGET="MAIN"><CODE>cuddAddBddDoPattern()</CODE></A>
1569  <DD> Performs the recursive step for Cudd_addBddPattern.
1570
1571  <DT> <A HREF="cuddAllDet.html#addBddDoThreshold" TARGET="MAIN"><CODE>addBddDoThreshold()</CODE></A>
1572  <DD> Performs the recursive step for Cudd_addBddThreshold.
1573
1574  <DT> <A HREF="cuddAllDet.html#addBddDoStrictThreshold" TARGET="MAIN"><CODE>addBddDoStrictThreshold()</CODE></A>
1575  <DD> Performs the recursive step for Cudd_addBddStrictThreshold.
1576
1577  <DT> <A HREF="cuddAllDet.html#addBddDoInterval" TARGET="MAIN"><CODE>addBddDoInterval()</CODE></A>
1578  <DD> Performs the recursive step for Cudd_addBddInterval.
1579
1580  <DT> <A HREF="cuddAllDet.html#addBddDoIthBit" TARGET="MAIN"><CODE>addBddDoIthBit()</CODE></A>
1581  <DD> Performs the recursive step for Cudd_addBddIthBit.
1582
1583  <DT> <A HREF="cuddAllDet.html#ddBddToAddRecur" TARGET="MAIN"><CODE>ddBddToAddRecur()</CODE></A>
1584  <DD> Performs the recursive step for Cudd_BddToAdd.
1585
1586  <DT> <A HREF="cuddAllDet.html#cuddBddTransferRecur" TARGET="MAIN"><CODE>cuddBddTransferRecur()</CODE></A>
1587  <DD> Performs the recursive step of Cudd_bddTransfer.
1588
1589 </DL>
1590 <HR>
1591 <A NAME="cuddCache.c"><H1>cuddCache.c</H1></A>
1592 Functions for cache insertion and lookup. <P>
1593 <B>By: Fabio Somenzi</B><P>
1594 Internal procedures included in this module:
1595                 <ul>
1596                 <li> cuddInitCache()
1597                 <li> cuddCacheInsert()
1598                 <li> cuddCacheInsert2()
1599                 <li> cuddCacheLookup()
1600                 <li> cuddCacheLookupZdd()
1601                 <li> cuddCacheLookup2()
1602                 <li> cuddCacheLookup2Zdd()
1603                 <li> cuddConstantLookup()
1604                 <li> cuddCacheProfile()
1605                 <li> cuddCacheResize()
1606                 <li> cuddCacheFlush()
1607                 <li> cuddComputeFloorLog2()
1608                 </ul>
1609             Static procedures included in this module:
1610                 <ul>
1611                 </ul> <P>
1612 <DL>
1613  <DT> <A HREF="cuddAllDet.html#cuddInitCache" TARGET="MAIN"><CODE>cuddInitCache()</CODE></A>
1614  <DD> Initializes the computed table.
1615
1616  <DT> <A HREF="cuddAllDet.html#cuddCacheInsert" TARGET="MAIN"><CODE>cuddCacheInsert()</CODE></A>
1617  <DD> Inserts a result in the cache.
1618
1619  <DT> <A HREF="cuddAllDet.html#cuddCacheInsert2" TARGET="MAIN"><CODE>cuddCacheInsert2()</CODE></A>
1620  <DD> Inserts a result in the cache for a function with two
1621   operands.
1622
1623  <DT> <A HREF="cuddAllDet.html#cuddCacheInsert1" TARGET="MAIN"><CODE>cuddCacheInsert1()</CODE></A>
1624  <DD> Inserts a result in the cache for a function with two
1625   operands.
1626
1627  <DT> <A HREF="cuddAllDet.html#cuddCacheLookup" TARGET="MAIN"><CODE>cuddCacheLookup()</CODE></A>
1628  <DD> Looks up in the cache for the result of op applied to f,
1629   g, and h.
1630
1631  <DT> <A HREF="cuddAllDet.html#cuddCacheLookupZdd" TARGET="MAIN"><CODE>cuddCacheLookupZdd()</CODE></A>
1632  <DD> Looks up in the cache for the result of op applied to f,
1633   g, and h.
1634
1635  <DT> <A HREF="cuddAllDet.html#cuddCacheLookup2" TARGET="MAIN"><CODE>cuddCacheLookup2()</CODE></A>
1636  <DD> Looks up in the cache for the result of op applied to f
1637   and g.
1638
1639  <DT> <A HREF="cuddAllDet.html#cuddCacheLookup1" TARGET="MAIN"><CODE>cuddCacheLookup1()</CODE></A>
1640  <DD> Looks up in the cache for the result of op applied to f.
1641
1642  <DT> <A HREF="cuddAllDet.html#cuddCacheLookup2Zdd" TARGET="MAIN"><CODE>cuddCacheLookup2Zdd()</CODE></A>
1643  <DD> Looks up in the cache for the result of op applied to f
1644   and g.
1645
1646  <DT> <A HREF="cuddAllDet.html#cuddCacheLookup1Zdd" TARGET="MAIN"><CODE>cuddCacheLookup1Zdd()</CODE></A>
1647  <DD> Looks up in the cache for the result of op applied to f.
1648
1649  <DT> <A HREF="cuddAllDet.html#cuddConstantLookup" TARGET="MAIN"><CODE>cuddConstantLookup()</CODE></A>
1650  <DD> Looks up in the cache for the result of op applied to f,
1651   g, and h.
1652
1653  <DT> <A HREF="cuddAllDet.html#cuddCacheProfile" TARGET="MAIN"><CODE>cuddCacheProfile()</CODE></A>
1654  <DD> Computes and prints a profile of the cache usage.
1655
1656  <DT> <A HREF="cuddAllDet.html#cuddCacheResize" TARGET="MAIN"><CODE>cuddCacheResize()</CODE></A>
1657  <DD> Resizes the cache.
1658
1659  <DT> <A HREF="cuddAllDet.html#cuddCacheFlush" TARGET="MAIN"><CODE>cuddCacheFlush()</CODE></A>
1660  <DD> Flushes the cache.
1661
1662  <DT> <A HREF="cuddAllDet.html#cuddComputeFloorLog2" TARGET="MAIN"><CODE>cuddComputeFloorLog2()</CODE></A>
1663  <DD> Returns the floor of the logarithm to the base 2.
1664
1665 </DL>
1666 <HR>
1667 <A NAME="cuddCheck.c"><H1>cuddCheck.c</H1></A>
1668 Functions to check consistency of data structures. <P>
1669 <B>By: Fabio Somenzi</B><P>
1670 External procedures included in this module:
1671                 <ul>
1672                 <li> Cudd_DebugCheck()
1673                 <li> Cudd_CheckKeys()
1674                 </ul>
1675                Internal procedures included in this module:
1676                 <ul>
1677                 <li> cuddHeapProfile()
1678                 <li> cuddPrintNode()
1679                 <li> cuddPrintVarGroups()
1680                 </ul>
1681                Static procedures included in this module:
1682                 <ul>
1683                 <li> debugFindParent()
1684                 </ul> <P>
1685 <DL>
1686  <DT> <A HREF="cuddAllDet.html#Cudd_DebugCheck" TARGET="MAIN"><CODE>Cudd_DebugCheck()</CODE></A>
1687  <DD> Checks for inconsistencies in the DD heap.
1688
1689  <DT> <A HREF="cuddAllDet.html#Cudd_CheckKeys" TARGET="MAIN"><CODE>Cudd_CheckKeys()</CODE></A>
1690  <DD> Checks for several conditions that should not occur.
1691
1692  <DT> <A HREF="cuddAllDet.html#cuddHeapProfile" TARGET="MAIN"><CODE>cuddHeapProfile()</CODE></A>
1693  <DD> Prints information about the heap.
1694
1695  <DT> <A HREF="cuddAllDet.html#cuddPrintNode" TARGET="MAIN"><CODE>cuddPrintNode()</CODE></A>
1696  <DD> Prints out information on a node.
1697
1698  <DT> <A HREF="cuddAllDet.html#cuddPrintVarGroups" TARGET="MAIN"><CODE>cuddPrintVarGroups()</CODE></A>
1699  <DD> Prints the variable groups as a parenthesized list.
1700
1701  <DT> <A HREF="cuddAllDet.html#debugFindParent" TARGET="MAIN"><CODE>debugFindParent()</CODE></A>
1702  <DD> Searches the subtables above node for its parents.
1703
1704  <DT> <A HREF="cuddAllDet.html#debugCheckParent" TARGET="MAIN"><CODE>debugCheckParent()</CODE></A>
1705  <DD> Reports an error if a (dead) node has a non-dead parent.
1706
1707 </DL>
1708 <HR>
1709 <A NAME="cuddClip.c"><H1>cuddClip.c</H1></A>
1710 Clipping functions. <P>
1711 <B>By: Fabio Somenzi</B><P>
1712 External procedures included in this module:
1713                 <ul>
1714                 <li> Cudd_bddClippingAnd()
1715                 <li> Cudd_bddClippingAndAbstract()
1716                 </ul>
1717        Internal procedures included in this module:
1718                 <ul>
1719                 <li> cuddBddClippingAnd()
1720                 <li> cuddBddClippingAndAbstract()
1721                 </ul>
1722        Static procedures included in this module:
1723                 <ul>
1724                 <li> cuddBddClippingAndRecur()
1725                 <li> cuddBddClipAndAbsRecur()
1726                 </ul>
1727
1728   SeeAlso     [ <P>
1729 <DL>
1730  <DT> <A HREF="cuddAllDet.html#Cudd_bddClippingAnd" TARGET="MAIN"><CODE>Cudd_bddClippingAnd()</CODE></A>
1731  <DD> Approximates the conjunction of two BDDs f and g.
1732
1733  <DT> <A HREF="cuddAllDet.html#Cudd_bddClippingAndAbstract" TARGET="MAIN"><CODE>Cudd_bddClippingAndAbstract()</CODE></A>
1734  <DD> Approximates the conjunction of two BDDs f and g and
1735   simultaneously abstracts the variables in cube.
1736
1737  <DT> <A HREF="cuddAllDet.html#cuddBddClippingAnd" TARGET="MAIN"><CODE>cuddBddClippingAnd()</CODE></A>
1738  <DD> Approximates the conjunction of two BDDs f and g.
1739
1740  <DT> <A HREF="cuddAllDet.html#cuddBddClippingAndAbstract" TARGET="MAIN"><CODE>cuddBddClippingAndAbstract()</CODE></A>
1741  <DD> Approximates the conjunction of two BDDs f and g and
1742   simultaneously abstracts the variables in cube.
1743
1744  <DT> <A HREF="cuddAllDet.html#cuddBddClippingAndRecur" TARGET="MAIN"><CODE>cuddBddClippingAndRecur()</CODE></A>
1745  <DD> Implements the recursive step of Cudd_bddClippingAnd.
1746
1747  <DT> <A HREF="cuddAllDet.html#cuddBddClipAndAbsRecur" TARGET="MAIN"><CODE>cuddBddClipAndAbsRecur()</CODE></A>
1748  <DD> Approximates the AND of two BDDs and simultaneously abstracts the
1749   variables in cube.
1750
1751 </DL>
1752 <HR>
1753 <A NAME="cuddCof.c"><H1>cuddCof.c</H1></A>
1754 Cofactoring functions. <P>
1755 <B>By: Fabio Somenzi</B><P>
1756 External procedures included in this module:
1757                 <ul>
1758                 <li> Cudd_Cofactor()
1759                 </ul>
1760                Internal procedures included in this module:
1761                 <ul>
1762                 <li> cuddGetBranches()
1763                 <li> cuddCheckCube()
1764                 <li> cuddCofactorRecur()
1765                 </ul> <P>
1766 <DL>
1767  <DT> <A HREF="cuddAllDet.html#Cudd_Cofactor" TARGET="MAIN"><CODE>Cudd_Cofactor()</CODE></A>
1768  <DD> Computes the cofactor of f with respect to g.
1769
1770  <DT> <A HREF="cuddAllDet.html#cuddGetBranches" TARGET="MAIN"><CODE>cuddGetBranches()</CODE></A>
1771  <DD> Computes the children of g.
1772
1773  <DT> <A HREF="cuddAllDet.html#cuddCheckCube" TARGET="MAIN"><CODE>cuddCheckCube()</CODE></A>
1774  <DD> Checks whether g is the BDD of a cube.
1775
1776  <DT> <A HREF="cuddAllDet.html#cuddCofactorRecur" TARGET="MAIN"><CODE>cuddCofactorRecur()</CODE></A>
1777  <DD> Performs the recursive step of Cudd_Cofactor.
1778
1779 </DL>
1780 <HR>
1781 <A NAME="cuddCompose.c"><H1>cuddCompose.c</H1></A>
1782 Functional composition and variable permutation of DDs. <P>
1783 <B>By: Fabio Somenzi and Kavita Ravi</B><P>
1784 External procedures included in this module:
1785                 <ul>
1786                 <li> Cudd_bddCompose()
1787                 <li> Cudd_addCompose()
1788                 <li> Cudd_addPermute()
1789                 <li> Cudd_addSwapVariables()
1790                 <li> Cudd_bddPermute()
1791                 <li> Cudd_bddVarMap()
1792                 <li> Cudd_SetVarMap()
1793                 <li> Cudd_bddSwapVariables()
1794                 <li> Cudd_bddAdjPermuteX()
1795                 <li> Cudd_addVectorCompose()
1796                 <li> Cudd_addGeneralVectorCompose()
1797                 <li> Cudd_addNonSimCompose()
1798                 <li> Cudd_bddVectorCompose()
1799                 </ul>
1800                Internal procedures included in this module:
1801                 <ul>
1802                 <li> cuddBddComposeRecur()
1803                 <li> cuddAddComposeRecur()
1804                 </ul>
1805                Static procedures included in this module:
1806                 <ul>
1807                 <li> cuddAddPermuteRecur()
1808                 <li> cuddBddPermuteRecur()
1809                 <li> cuddBddVarMapRecur()
1810                 <li> cuddAddVectorComposeRecur()
1811                 <li> cuddAddGeneralVectorComposeRecur()
1812                 <li> cuddAddNonSimComposeRecur()
1813                 <li> cuddBddVectorComposeRecur()
1814                 <li> ddIsIthAddVar()
1815                 <li> ddIsIthAddVarPair()
1816                </ul>
1817   The permutation functions use a local cache because the results to
1818   be remembered depend on the permutation being applied.  Since the
1819   permutation is just an array, it cannot be stored in the global
1820   cache. There are different procedured for BDDs and ADDs. This is
1821   because bddPermuteRecur uses cuddBddIteRecur. If this were changed,
1822   the procedures could be merged. <P>
1823 <DL>
1824  <DT> <A HREF="cuddAllDet.html#Cudd_bddCompose" TARGET="MAIN"><CODE>Cudd_bddCompose()</CODE></A>
1825  <DD> Substitutes g for x_v in the BDD for f.
1826
1827  <DT> <A HREF="cuddAllDet.html#Cudd_addCompose" TARGET="MAIN"><CODE>Cudd_addCompose()</CODE></A>
1828  <DD> Substitutes g for x_v in the ADD for f.
1829
1830  <DT> <A HREF="cuddAllDet.html#Cudd_addPermute" TARGET="MAIN"><CODE>Cudd_addPermute()</CODE></A>
1831  <DD> Permutes the variables of an ADD.
1832
1833  <DT> <A HREF="cuddAllDet.html#Cudd_addSwapVariables" TARGET="MAIN"><CODE>Cudd_addSwapVariables()</CODE></A>
1834  <DD> Swaps two sets of variables of the same size (x and y) in
1835   the ADD f.
1836
1837  <DT> <A HREF="cuddAllDet.html#Cudd_bddPermute" TARGET="MAIN"><CODE>Cudd_bddPermute()</CODE></A>
1838  <DD> Permutes the variables of a BDD.
1839
1840  <DT> <A HREF="cuddAllDet.html#Cudd_bddVarMap" TARGET="MAIN"><CODE>Cudd_bddVarMap()</CODE></A>
1841  <DD> Remaps the variables of a BDD using the default variable map.
1842
1843  <DT> <A HREF="cuddAllDet.html#Cudd_SetVarMap" TARGET="MAIN"><CODE>Cudd_SetVarMap()</CODE></A>
1844  <DD> Registers a variable mapping with the manager.
1845
1846  <DT> <A HREF="cuddAllDet.html#Cudd_bddSwapVariables" TARGET="MAIN"><CODE>Cudd_bddSwapVariables()</CODE></A>
1847  <DD> Swaps two sets of variables of the same size (x and y) in
1848   the BDD f.
1849
1850  <DT> <A HREF="cuddAllDet.html#Cudd_bddAdjPermuteX" TARGET="MAIN"><CODE>Cudd_bddAdjPermuteX()</CODE></A>
1851  <DD> Rearranges a set of variables in the BDD B.
1852
1853  <DT> <A HREF="cuddAllDet.html#Cudd_addVectorCompose" TARGET="MAIN"><CODE>Cudd_addVectorCompose()</CODE></A>
1854  <DD> Composes an ADD with a vector of 0-1 ADDs.
1855
1856  <DT> <A HREF="cuddAllDet.html#Cudd_addGeneralVectorCompose" TARGET="MAIN"><CODE>Cudd_addGeneralVectorCompose()</CODE></A>
1857  <DD> Composes an ADD with a vector of ADDs.
1858
1859  <DT> <A HREF="cuddAllDet.html#Cudd_addNonSimCompose" TARGET="MAIN"><CODE>Cudd_addNonSimCompose()</CODE></A>
1860  <DD> Composes an ADD with a vector of 0-1 ADDs.
1861
1862  <DT> <A HREF="cuddAllDet.html#Cudd_bddVectorCompose" TARGET="MAIN"><CODE>Cudd_bddVectorCompose()</CODE></A>
1863  <DD> Composes a BDD with a vector of BDDs.
1864
1865  <DT> <A HREF="cuddAllDet.html#cuddBddComposeRecur" TARGET="MAIN"><CODE>cuddBddComposeRecur()</CODE></A>
1866  <DD> Performs the recursive step of Cudd_bddCompose.
1867
1868  <DT> <A HREF="cuddAllDet.html#cuddAddComposeRecur" TARGET="MAIN"><CODE>cuddAddComposeRecur()</CODE></A>
1869  <DD> Performs the recursive step of Cudd_addCompose.
1870
1871  <DT> <A HREF="cuddAllDet.html#cuddAddPermuteRecur" TARGET="MAIN"><CODE>cuddAddPermuteRecur()</CODE></A>
1872  <DD> Implements the recursive step of Cudd_addPermute.
1873
1874  <DT> <A HREF="cuddAllDet.html#cuddBddPermuteRecur" TARGET="MAIN"><CODE>cuddBddPermuteRecur()</CODE></A>
1875  <DD> Implements the recursive step of Cudd_bddPermute.
1876
1877  <DT> <A HREF="cuddAllDet.html#cuddBddVarMapRecur" TARGET="MAIN"><CODE>cuddBddVarMapRecur()</CODE></A>
1878  <DD> Implements the recursive step of Cudd_bddVarMap.
1879
1880  <DT> <A HREF="cuddAllDet.html#cuddAddVectorComposeRecur" TARGET="MAIN"><CODE>cuddAddVectorComposeRecur()</CODE></A>
1881  <DD> Performs the recursive step of Cudd_addVectorCompose.
1882
1883  <DT> <A HREF="cuddAllDet.html#cuddAddGeneralVectorComposeRecur" TARGET="MAIN"><CODE>cuddAddGeneralVectorComposeRecur()</CODE></A>
1884  <DD> Performs the recursive step of Cudd_addGeneralVectorCompose.
1885
1886  <DT> <A HREF="cuddAllDet.html#cuddAddNonSimComposeRecur" TARGET="MAIN"><CODE>cuddAddNonSimComposeRecur()</CODE></A>
1887  <DD> Performs the recursive step of Cudd_addNonSimCompose.
1888
1889  <DT> <A HREF="cuddAllDet.html#cuddBddVectorComposeRecur" TARGET="MAIN"><CODE>cuddBddVectorComposeRecur()</CODE></A>
1890  <DD> Performs the recursive step of Cudd_bddVectorCompose.
1891
1892  <DT> <A HREF="cuddAllDet.html#ddIsIthAddVar" TARGET="MAIN"><CODE>ddIsIthAddVar()</CODE></A>
1893  <DD> Comparison of a function to the i-th ADD variable.
1894
1895  <DT> <A HREF="cuddAllDet.html#ddIsIthAddVarPair" TARGET="MAIN"><CODE>ddIsIthAddVarPair()</CODE></A>
1896  <DD> Comparison of a pair of functions to the i-th ADD variable.
1897
1898 </DL>
1899 <HR>
1900 <A NAME="cuddDecomp.c"><H1>cuddDecomp.c</H1></A>
1901 Functions for BDD decomposition. <P>
1902 <B>By: Kavita Ravi, Fabio Somenzi</B><P>
1903 External procedures included in this file:
1904                 <ul>
1905                 <li> Cudd_bddApproxConjDecomp()
1906                 <li> Cudd_bddApproxDisjDecomp()
1907                 <li> Cudd_bddIterConjDecomp()
1908                 <li> Cudd_bddIterDisjDecomp()
1909                 <li> Cudd_bddGenConjDecomp()
1910                 <li> Cudd_bddGenDisjDecomp()
1911                 <li> Cudd_bddVarConjDecomp()
1912                 <li> Cudd_bddVarDisjDecomp()
1913                 </ul>
1914         Static procedures included in this module:
1915                 <ul>
1916                 <li> cuddConjunctsAux()
1917                 <li> CreateBotDist()
1918                 <li> BuildConjuncts()
1919                 <li> ConjunctsFree()
1920                 </ul> <P>
1921 <DL>
1922  <DT> <A HREF="cuddAllDet.html#Cudd_bddApproxConjDecomp" TARGET="MAIN"><CODE>Cudd_bddApproxConjDecomp()</CODE></A>
1923  <DD> Performs two-way conjunctive decomposition of a BDD.
1924
1925  <DT> <A HREF="cuddAllDet.html#Cudd_bddApproxDisjDecomp" TARGET="MAIN"><CODE>Cudd_bddApproxDisjDecomp()</CODE></A>
1926  <DD> Performs two-way disjunctive decomposition of a BDD.
1927
1928  <DT> <A HREF="cuddAllDet.html#Cudd_bddIterConjDecomp" TARGET="MAIN"><CODE>Cudd_bddIterConjDecomp()</CODE></A>
1929  <DD> Performs two-way conjunctive decomposition of a BDD.
1930
1931  <DT> <A HREF="cuddAllDet.html#Cudd_bddIterDisjDecomp" TARGET="MAIN"><CODE>Cudd_bddIterDisjDecomp()</CODE></A>
1932  <DD> Performs two-way disjunctive decomposition of a BDD.
1933
1934  <DT> <A HREF="cuddAllDet.html#Cudd_bddGenConjDecomp" TARGET="MAIN"><CODE>Cudd_bddGenConjDecomp()</CODE></A>
1935  <DD> Performs two-way conjunctive decomposition of a BDD.
1936
1937  <DT> <A HREF="cuddAllDet.html#Cudd_bddGenDisjDecomp" TARGET="MAIN"><CODE>Cudd_bddGenDisjDecomp()</CODE></A>
1938  <DD> Performs two-way disjunctive decomposition of a BDD.
1939
1940  <DT> <A HREF="cuddAllDet.html#Cudd_bddVarConjDecomp" TARGET="MAIN"><CODE>Cudd_bddVarConjDecomp()</CODE></A>
1941  <DD> Performs two-way conjunctive decomposition of a BDD.
1942
1943  <DT> <A HREF="cuddAllDet.html#Cudd_bddVarDisjDecomp" TARGET="MAIN"><CODE>Cudd_bddVarDisjDecomp()</CODE></A>
1944  <DD> Performs two-way disjunctive decomposition of a BDD.
1945
1946  <DT> <A HREF="cuddAllDet.html#CreateBotDist" TARGET="MAIN"><CODE>CreateBotDist()</CODE></A>
1947  <DD> Get longest distance of node from constant.
1948
1949  <DT> <A HREF="cuddAllDet.html#CountMinterms" TARGET="MAIN"><CODE>CountMinterms()</CODE></A>
1950  <DD> Count the number of minterms of each node ina a BDD and
1951   store it in a hash table.
1952
1953  <DT> <A HREF="cuddAllDet.html#ConjunctsFree" TARGET="MAIN"><CODE>ConjunctsFree()</CODE></A>
1954  <DD> Free factors structure
1955
1956  <DT> <A HREF="cuddAllDet.html#PairInTables" TARGET="MAIN"><CODE>PairInTables()</CODE></A>
1957  <DD> Check whether the given pair is in the tables.
1958
1959  <DT> <A HREF="cuddAllDet.html#CheckTablesCacheAndReturn" TARGET="MAIN"><CODE>CheckTablesCacheAndReturn()</CODE></A>
1960  <DD> Check the tables for the existence of pair and return one
1961   combination, cache the result.
1962
1963  <DT> <A HREF="cuddAllDet.html#PickOnePair" TARGET="MAIN"><CODE>PickOnePair()</CODE></A>
1964  <DD> Check the tables for the existence of pair and return one
1965   combination, store in cache.
1966
1967  <DT> <A HREF="cuddAllDet.html#CheckInTables" TARGET="MAIN"><CODE>CheckInTables()</CODE></A>
1968  <DD> Check if the two pairs exist in the table, If any of the
1969   conjuncts do exist, store in the cache and return the corresponding pair.
1970
1971  <DT> <A HREF="cuddAllDet.html#ZeroCase" TARGET="MAIN"><CODE>ZeroCase()</CODE></A>
1972  <DD> If one child is zero, do explicitly what Restrict does or better
1973
1974  <DT> <A HREF="cuddAllDet.html#BuildConjuncts" TARGET="MAIN"><CODE>BuildConjuncts()</CODE></A>
1975  <DD> Builds the conjuncts recursively, bottom up.
1976
1977  <DT> <A HREF="cuddAllDet.html#cuddConjunctsAux" TARGET="MAIN"><CODE>cuddConjunctsAux()</CODE></A>
1978  <DD> Procedure to compute two conjunctive factors of f and place in *c1 and *c2.
1979
1980 </DL>
1981 <HR>
1982 <A NAME="cuddEssent.c"><H1>cuddEssent.c</H1></A>
1983 Functions for the detection of essential variables. <P>
1984 <B>By: Fabio Somenzi</B><P>
1985 External procedures included in this file:
1986                 <ul>
1987                 <li> Cudd_FindEssential()
1988                 <li> Cudd_bddIsVarEssential()
1989                 <li> Cudd_FindTwoLiteralClauses()
1990                 <li> Cudd_ReadIthClause()
1991                 <li> Cudd_PrintTwoLiteralClauses()
1992                 <li> Cudd_tlcInfoFree()
1993                 </ul>
1994         Static procedures included in this module:
1995                 <ul>
1996                 <li> ddFindEssentialRecur()
1997                 <li> ddFindTwoLiteralClausesRecur()
1998                 <li> computeClauses()
1999                 <li> computeClausesWithUniverse()
2000                 <li> emptyClauseSet()
2001                 <li> sentinelp()
2002                 <li> equalp()
2003                 <li> beforep()
2004                 <li> oneliteralp()
2005                 <li> impliedp()
2006                 <li> bitVectorAlloc()
2007                 <li> bitVectorClear()
2008                 <li> bitVectorFree()
2009                 <li> bitVectorRead()
2010                 <li> bitVectorSet()
2011                 <li> tlcInfoAlloc()
2012                 </ul> <P>
2013 <DL>
2014  <DT> <A HREF="cuddAllDet.html#Cudd_FindEssential" TARGET="MAIN"><CODE>Cudd_FindEssential()</CODE></A>
2015  <DD> Finds the essential variables of a DD.
2016
2017  <DT> <A HREF="cuddAllDet.html#Cudd_bddIsVarEssential" TARGET="MAIN"><CODE>Cudd_bddIsVarEssential()</CODE></A>
2018  <DD> Determines whether a given variable is essential with a
2019   given phase in a BDD.
2020
2021  <DT> <A HREF="cuddAllDet.html#Cudd_FindTwoLiteralClauses" TARGET="MAIN"><CODE>Cudd_FindTwoLiteralClauses()</CODE></A>
2022  <DD> Finds the two literal clauses of a DD.
2023
2024  <DT> <A HREF="cuddAllDet.html#Cudd_ReadIthClause" TARGET="MAIN"><CODE>Cudd_ReadIthClause()</CODE></A>
2025  <DD> Accesses the i-th clause of a DD.
2026
2027  <DT> <A HREF="cuddAllDet.html#Cudd_PrintTwoLiteralClauses" TARGET="MAIN"><CODE>Cudd_PrintTwoLiteralClauses()</CODE></A>
2028  <DD> Prints the two literal clauses of a DD.
2029
2030  <DT> <A HREF="cuddAllDet.html#Cudd_tlcInfoFree" TARGET="MAIN"><CODE>Cudd_tlcInfoFree()</CODE></A>
2031  <DD> Frees a DdTlcInfo Structure.
2032
2033  <DT> <A HREF="cuddAllDet.html#ddFindEssentialRecur" TARGET="MAIN"><CODE>ddFindEssentialRecur()</CODE></A>
2034  <DD> Implements the recursive step of Cudd_FindEssential.
2035
2036  <DT> <A HREF="cuddAllDet.html#ddFindTwoLiteralClausesRecur" TARGET="MAIN"><CODE>ddFindTwoLiteralClausesRecur()</CODE></A>
2037  <DD> Implements the recursive step of Cudd_FindTwoLiteralClauses.
2038
2039  <DT> <A HREF="cuddAllDet.html#computeClauses" TARGET="MAIN"><CODE>computeClauses()</CODE></A>
2040  <DD> Computes the two-literal clauses for a node.
2041
2042  <DT> <A HREF="cuddAllDet.html#computeClausesWithUniverse" TARGET="MAIN"><CODE>computeClausesWithUniverse()</CODE></A>
2043  <DD> Computes the two-literal clauses for a node.
2044
2045  <DT> <A HREF="cuddAllDet.html#emptyClauseSet" TARGET="MAIN"><CODE>emptyClauseSet()</CODE></A>
2046  <DD> Returns an enpty set of clauses.
2047
2048  <DT> <A HREF="cuddAllDet.html#sentinelp" TARGET="MAIN"><CODE>sentinelp()</CODE></A>
2049  <DD> Returns true iff the argument is the sentinel clause.
2050
2051  <DT> <A HREF="cuddAllDet.html#equalp" TARGET="MAIN"><CODE>equalp()</CODE></A>
2052  <DD> Returns true iff the two arguments are identical clauses.
2053
2054  <DT> <A HREF="cuddAllDet.html#beforep" TARGET="MAIN"><CODE>beforep()</CODE></A>
2055  <DD> Returns true iff the first argument precedes the second in
2056   the clause order.
2057
2058  <DT> <A HREF="cuddAllDet.html#oneliteralp" TARGET="MAIN"><CODE>oneliteralp()</CODE></A>
2059  <DD> Returns true iff the argument is a one-literal clause.
2060
2061  <DT> <A HREF="cuddAllDet.html#impliedp" TARGET="MAIN"><CODE>impliedp()</CODE></A>
2062  <DD> Returns true iff either literal of a clause is in a set of
2063   literals.
2064
2065  <DT> <A HREF="cuddAllDet.html#bitVectorAlloc" TARGET="MAIN"><CODE>bitVectorAlloc()</CODE></A>
2066  <DD> Allocates a bit vector.
2067
2068  <DT> <A HREF="cuddAllDet.html#bitVectorClear" TARGET="MAIN"><CODE>bitVectorClear()</CODE></A>
2069  <DD> Clears a bit vector.
2070
2071  <DT> <A HREF="cuddAllDet.html#bitVectorFree" TARGET="MAIN"><CODE>bitVectorFree()</CODE></A>
2072  <DD> Frees a bit vector.
2073
2074  <DT> <A HREF="cuddAllDet.html#bitVectorRead" TARGET="MAIN"><CODE>bitVectorRead()</CODE></A>
2075  <DD> Returns the i-th entry of a bit vector.
2076
2077  <DT> <A HREF="cuddAllDet.html#bitVectorSet" TARGET="MAIN"><CODE>bitVectorSet()</CODE></A>
2078  <DD> Sets the i-th entry of a bit vector to a value.
2079
2080  <DT> <A HREF="cuddAllDet.html#tlcInfoAlloc" TARGET="MAIN"><CODE>tlcInfoAlloc()</CODE></A>
2081  <DD> Allocates a DdTlcInfo Structure.
2082
2083 </DL>
2084 <HR>
2085 <A NAME="cuddExact.c"><H1>cuddExact.c</H1></A>
2086 Functions for exact variable reordering. <P>
2087 <B>By: Cheng Hua, Fabio Somenzi</B><P>
2088 External procedures included in this file:
2089                 <ul>
2090                 </ul>
2091         Internal procedures included in this module:
2092                 <ul>
2093                 <li> cuddExact()
2094                 </ul>
2095         Static procedures included in this module:
2096                 <ul>
2097                 <li> getMaxBinomial()
2098                 <li> gcd()
2099                 <li> getMatrix()
2100                 <li> freeMatrix()
2101                 <li> getLevelKeys()
2102                 <li> ddShuffle()
2103                 <li> ddSiftUp()
2104                 <li> updateUB()
2105                 <li> ddCountRoots()
2106                 <li> ddClearGlobal()
2107                 <li> computeLB()
2108                 <li> updateEntry()
2109                 <li> pushDown()
2110                 <li> initSymmInfo()
2111                 </ul> <P>
2112 <DL>
2113  <DT> <A HREF="cuddAllDet.html#cuddExact" TARGET="MAIN"><CODE>cuddExact()</CODE></A>
2114  <DD> Exact variable ordering algorithm.
2115
2116  <DT> <A HREF="cuddAllDet.html#getMaxBinomial" TARGET="MAIN"><CODE>getMaxBinomial()</CODE></A>
2117  <DD> Returns the maximum value of (n choose k) for a given n.
2118
2119  <DT> <A HREF="cuddAllDet.html#gcd" TARGET="MAIN"><CODE>gcd()</CODE></A>
2120  <DD> Returns the gcd of two integers.
2121
2122  <DT> <A HREF="cuddAllDet.html#getMatrix" TARGET="MAIN"><CODE>getMatrix()</CODE></A>
2123  <DD> Allocates a two-dimensional matrix of ints.
2124
2125  <DT> <A HREF="cuddAllDet.html#freeMatrix" TARGET="MAIN"><CODE>freeMatrix()</CODE></A>
2126  <DD> Frees a two-dimensional matrix allocated by getMatrix.
2127
2128  <DT> <A HREF="cuddAllDet.html#getLevelKeys" TARGET="MAIN"><CODE>getLevelKeys()</CODE></A>
2129  <DD> Returns the number of nodes at one level of a unique table.
2130
2131  <DT> <A HREF="cuddAllDet.html#ddShuffle" TARGET="MAIN"><CODE>ddShuffle()</CODE></A>
2132  <DD> Reorders variables according to a given permutation.
2133
2134  <DT> <A HREF="cuddAllDet.html#ddSiftUp" TARGET="MAIN"><CODE>ddSiftUp()</CODE></A>
2135  <DD> Moves one variable up.
2136
2137  <DT> <A HREF="cuddAllDet.html#updateUB" TARGET="MAIN"><CODE>updateUB()</CODE></A>
2138  <DD> Updates the upper bound and saves the best order seen so far.
2139
2140  <DT> <A HREF="cuddAllDet.html#ddCountRoots" TARGET="MAIN"><CODE>ddCountRoots()</CODE></A>
2141  <DD> Counts the number of roots.
2142
2143  <DT> <A HREF="cuddAllDet.html#ddClearGlobal" TARGET="MAIN"><CODE>ddClearGlobal()</CODE></A>
2144  <DD> Scans the DD and clears the LSB of the next pointers.
2145
2146  <DT> <A HREF="cuddAllDet.html#computeLB" TARGET="MAIN"><CODE>computeLB()</CODE></A>
2147  <DD> Computes a lower bound on the size of a BDD.
2148
2149  <DT> <A HREF="cuddAllDet.html#updateEntry" TARGET="MAIN"><CODE>updateEntry()</CODE></A>
2150  <DD> Updates entry for a subset.
2151
2152  <DT> <A HREF="cuddAllDet.html#pushDown" TARGET="MAIN"><CODE>pushDown()</CODE></A>
2153  <DD> Pushes a variable in the order down to position "level."
2154
2155  <DT> <A HREF="cuddAllDet.html#initSymmInfo" TARGET="MAIN"><CODE>initSymmInfo()</CODE></A>
2156  <DD> Gathers symmetry information.
2157
2158  <DT> <A HREF="cuddAllDet.html#checkSymmInfo" TARGET="MAIN"><CODE>checkSymmInfo()</CODE></A>
2159  <DD> Check symmetry condition.
2160
2161 </DL>
2162 <HR>
2163 <A NAME="cuddExport.c"><H1>cuddExport.c</H1></A>
2164 Export functions. <P>
2165 <B>By: Fabio Somenzi</B><P>
2166 External procedures included in this module:
2167                 <ul>
2168                 <li> Cudd_DumpBlif()
2169                 <li> Cudd_DumpBlifBody()
2170                 <li> Cudd_DumpDot()
2171                 <li> Cudd_DumpDaVinci()
2172                 <li> Cudd_DumpDDcal()
2173                 <li> Cudd_DumpFactoredForm()
2174                 </ul>
2175         Internal procedures included in this module:
2176                 <ul>
2177                 </ul>
2178         Static procedures included in this module:
2179                 <ul>
2180                 <li> ddDoDumpBlif()
2181                 <li> ddDoDumpDaVinci()
2182                 <li> ddDoDumpDDcal()
2183                 <li> ddDoDumpFactoredForm()
2184                 </ul> <P>
2185 <DL>
2186  <DT> <A HREF="cuddAllDet.html#Cudd_DumpBlif" TARGET="MAIN"><CODE>Cudd_DumpBlif()</CODE></A>
2187  <DD> Writes a blif file representing the argument BDDs.
2188
2189  <DT> <A HREF="cuddAllDet.html#Cudd_DumpBlifBody" TARGET="MAIN"><CODE>Cudd_DumpBlifBody()</CODE></A>
2190  <DD> Writes a blif body representing the argument BDDs.
2191
2192  <DT> <A HREF="cuddAllDet.html#Cudd_DumpDot" TARGET="MAIN"><CODE>Cudd_DumpDot()</CODE></A>
2193  <DD> Writes a dot file representing the argument DDs.
2194
2195  <DT> <A HREF="cuddAllDet.html#Cudd_DumpDaVinci" TARGET="MAIN"><CODE>Cudd_DumpDaVinci()</CODE></A>
2196  <DD> Writes a daVinci file representing the argument BDDs.
2197
2198  <DT> <A HREF="cuddAllDet.html#Cudd_DumpDDcal" TARGET="MAIN"><CODE>Cudd_DumpDDcal()</CODE></A>
2199  <DD> Writes a DDcal file representing the argument BDDs.
2200
2201  <DT> <A HREF="cuddAllDet.html#Cudd_DumpFactoredForm" TARGET="MAIN"><CODE>Cudd_DumpFactoredForm()</CODE></A>
2202  <DD> Writes factored forms representing the argument BDDs.
2203
2204  <DT> <A HREF="cuddAllDet.html#ddDoDumpBlif" TARGET="MAIN"><CODE>ddDoDumpBlif()</CODE></A>
2205  <DD> Performs the recursive step of Cudd_DumpBlif.
2206
2207  <DT> <A HREF="cuddAllDet.html#ddDoDumpDaVinci" TARGET="MAIN"><CODE>ddDoDumpDaVinci()</CODE></A>
2208  <DD> Performs the recursive step of Cudd_DumpDaVinci.
2209
2210  <DT> <A HREF="cuddAllDet.html#ddDoDumpDDcal" TARGET="MAIN"><CODE>ddDoDumpDDcal()</CODE></A>
2211  <DD> Performs the recursive step of Cudd_DumpDDcal.
2212
2213  <DT> <A HREF="cuddAllDet.html#ddDoDumpFactoredForm" TARGET="MAIN"><CODE>ddDoDumpFactoredForm()</CODE></A>
2214  <DD> Performs the recursive step of Cudd_DumpFactoredForm.
2215
2216 </DL>
2217 <HR>
2218 <A NAME="cuddGenCof.c"><H1>cuddGenCof.c</H1></A>
2219 Generalized cofactors for BDDs and ADDs. <P>
2220 <B>By: Fabio Somenzi</B><P>
2221 External procedures included in this module:
2222                 <ul>
2223                 <li> Cudd_bddConstrain()
2224                 <li> Cudd_bddRestrict()
2225                 <li> Cudd_bddNPAnd()
2226                 <li> Cudd_addConstrain()
2227                 <li> Cudd_bddConstrainDecomp()
2228                 <li> Cudd_addRestrict()
2229                 <li> Cudd_bddCharToVect()
2230                 <li> Cudd_bddLICompaction()
2231                 <li> Cudd_bddSqueeze()
2232                 <li> Cudd_SubsetCompress()
2233                 <li> Cudd_SupersetCompress()
2234                 </ul>
2235             Internal procedures included in this module:
2236                 <ul>
2237                 <li> cuddBddConstrainRecur()
2238                 <li> cuddBddRestrictRecur()
2239                 <li> cuddBddNPAndRecur()
2240                 <li> cuddAddConstrainRecur()
2241                 <li> cuddAddRestrictRecur()
2242                 <li> cuddBddLICompaction()
2243                 </ul>
2244             Static procedures included in this module:
2245                 <ul>
2246                 <li> cuddBddConstrainDecomp()
2247                 <li> cuddBddCharToVect()
2248                 <li> cuddBddLICMarkEdges()
2249                 <li> cuddBddLICBuildResult()
2250                 <li> cuddBddSqueeze()
2251                 </ul> <P>
2252 <DL>
2253  <DT> <A HREF="cuddAllDet.html#Cudd_bddConstrain" TARGET="MAIN"><CODE>Cudd_bddConstrain()</CODE></A>
2254  <DD> Computes f constrain c.
2255
2256  <DT> <A HREF="cuddAllDet.html#Cudd_bddRestrict" TARGET="MAIN"><CODE>Cudd_bddRestrict()</CODE></A>
2257  <DD> BDD restrict according to Coudert and Madre's algorithm
2258   (ICCAD90).
2259
2260  <DT> <A HREF="cuddAllDet.html#Cudd_bddNPAnd" TARGET="MAIN"><CODE>Cudd_bddNPAnd()</CODE></A>
2261  <DD> Computes f non-polluting-and g.
2262
2263  <DT> <A HREF="cuddAllDet.html#Cudd_addConstrain" TARGET="MAIN"><CODE>Cudd_addConstrain()</CODE></A>
2264  <DD> Computes f constrain c for ADDs.
2265
2266  <DT> <A HREF="cuddAllDet.html#Cudd_bddConstrainDecomp" TARGET="MAIN"><CODE>Cudd_bddConstrainDecomp()</CODE></A>
2267  <DD> BDD conjunctive decomposition as in McMillan's CAV96 paper.
2268
2269  <DT> <A HREF="cuddAllDet.html#Cudd_addRestrict" TARGET="MAIN"><CODE>Cudd_addRestrict()</CODE></A>
2270  <DD> ADD restrict according to Coudert and Madre's algorithm
2271   (ICCAD90).
2272
2273  <DT> <A HREF="cuddAllDet.html#Cudd_bddCharToVect" TARGET="MAIN"><CODE>Cudd_bddCharToVect()</CODE></A>
2274  <DD> Computes a vector whose image equals a non-zero function.
2275
2276  <DT> <A HREF="cuddAllDet.html#Cudd_bddLICompaction" TARGET="MAIN"><CODE>Cudd_bddLICompaction()</CODE></A>
2277  <DD> Performs safe minimization of a BDD.
2278
2279  <DT> <A HREF="cuddAllDet.html#Cudd_bddSqueeze" TARGET="MAIN"><CODE>Cudd_bddSqueeze()</CODE></A>
2280  <DD> Finds a small BDD in a function interval.
2281
2282  <DT> <A HREF="cuddAllDet.html#Cudd_bddMinimize" TARGET="MAIN"><CODE>Cudd_bddMinimize()</CODE></A>
2283  <DD> Finds a small BDD that agrees with <code>f</code> over
2284   <code>c</code>.
2285
2286  <DT> <A HREF="cuddAllDet.html#Cudd_SubsetCompress" TARGET="MAIN"><CODE>Cudd_SubsetCompress()</CODE></A>
2287  <DD> Find a dense subset of BDD <code>f</code>.
2288
2289  <DT> <A HREF="cuddAllDet.html#Cudd_SupersetCompress" TARGET="MAIN"><CODE>Cudd_SupersetCompress()</CODE></A>
2290  <DD> Find a dense superset of BDD <code>f</code>.
2291
2292  <DT> <A HREF="cuddAllDet.html#cuddBddConstrainRecur" TARGET="MAIN"><CODE>cuddBddConstrainRecur()</CODE></A>
2293  <DD> Performs the recursive step of Cudd_bddConstrain.
2294
2295  <DT> <A HREF="cuddAllDet.html#cuddBddRestrictRecur" TARGET="MAIN"><CODE>cuddBddRestrictRecur()</CODE></A>
2296  <DD> Performs the recursive step of Cudd_bddRestrict.
2297
2298  <DT> <A HREF="cuddAllDet.html#cuddBddNPAndRecur" TARGET="MAIN"><CODE>cuddBddNPAndRecur()</CODE></A>
2299  <DD> Implements the recursive step of Cudd_bddAnd.
2300
2301  <DT> <A HREF="cuddAllDet.html#cuddAddConstrainRecur" TARGET="MAIN"><CODE>cuddAddConstrainRecur()</CODE></A>
2302  <DD> Performs the recursive step of Cudd_addConstrain.
2303
2304  <DT> <A HREF="cuddAllDet.html#cuddAddRestrictRecur" TARGET="MAIN"><CODE>cuddAddRestrictRecur()</CODE></A>
2305  <DD> Performs the recursive step of Cudd_addRestrict.
2306
2307  <DT> <A HREF="cuddAllDet.html#cuddBddLICompaction" TARGET="MAIN"><CODE>cuddBddLICompaction()</CODE></A>
2308  <DD> Performs safe minimization of a BDD.
2309
2310  <DT> <A HREF="cuddAllDet.html#cuddBddConstrainDecomp" TARGET="MAIN"><CODE>cuddBddConstrainDecomp()</CODE></A>
2311  <DD> Performs the recursive step of Cudd_bddConstrainDecomp.
2312
2313  <DT> <A HREF="cuddAllDet.html#cuddBddCharToVect" TARGET="MAIN"><CODE>cuddBddCharToVect()</CODE></A>
2314  <DD> Performs the recursive step of Cudd_bddCharToVect.
2315
2316  <DT> <A HREF="cuddAllDet.html#cuddBddLICMarkEdges" TARGET="MAIN"><CODE>cuddBddLICMarkEdges()</CODE></A>
2317  <DD> Performs the edge marking step of Cudd_bddLICompaction.
2318
2319  <DT> <A HREF="cuddAllDet.html#cuddBddLICBuildResult" TARGET="MAIN"><CODE>cuddBddLICBuildResult()</CODE></A>
2320  <DD> Builds the result of Cudd_bddLICompaction.
2321
2322  <DT> <A HREF="cuddAllDet.html#MarkCacheHash" TARGET="MAIN"><CODE>MarkCacheHash()</CODE></A>
2323  <DD> Hash function for the computed table of cuddBddLICMarkEdges.
2324
2325  <DT> <A HREF="cuddAllDet.html#MarkCacheCompare" TARGET="MAIN"><CODE>MarkCacheCompare()</CODE></A>
2326  <DD> Comparison function for the computed table of
2327   cuddBddLICMarkEdges.
2328
2329  <DT> <A HREF="cuddAllDet.html#MarkCacheCleanUp" TARGET="MAIN"><CODE>MarkCacheCleanUp()</CODE></A>
2330  <DD> Frees memory associated with computed table of
2331   cuddBddLICMarkEdges.
2332
2333  <DT> <A HREF="cuddAllDet.html#cuddBddSqueeze" TARGET="MAIN"><CODE>cuddBddSqueeze()</CODE></A>
2334  <DD> Performs the recursive step of Cudd_bddSqueeze.
2335
2336 </DL>
2337 <HR>
2338 <A NAME="cuddGenetic.c"><H1>cuddGenetic.c</H1></A>
2339 Genetic algorithm for variable reordering. <P>
2340 <B>By: Curt Musfeldt, Alan Shuler, Fabio Somenzi</B><P>
2341 Internal procedures included in this file:
2342                 <ul>
2343                 <li> cuddGa()
2344                 </ul>
2345         Static procedures included in this module:
2346                 <ul>
2347                 <li> make_random()
2348                 <li> sift_up()
2349                 <li> build_dd()
2350                 <li> largest()
2351                 <li> rand_int()
2352                 <li> array_hash()
2353                 <li> array_compare()
2354                 <li> find_best()
2355                 <li> find_average_fitness()
2356                 <li> PMX()
2357                 <li> roulette()
2358                 </ul>
2359
2360   The genetic algorithm implemented here is as follows.  We start with
2361   the current DD order.  We sift this order and use this as the
2362   reference DD.  We only keep 1 DD around for the entire process and
2363   simply rearrange the order of this DD, storing the various orders
2364   and their corresponding DD sizes.  We generate more random orders to
2365   build an initial population. This initial population is 3 times the
2366   number of variables, with a maximum of 120. Each random order is
2367   built (from the reference DD) and its size stored.  Each random
2368   order is also sifted to keep the DD sizes fairly small.  Then a
2369   crossover is performed between two orders (picked randomly) and the
2370   two resulting DDs are built and sifted.  For each new order, if its
2371   size is smaller than any DD in the population, it is inserted into
2372   the population and the DD with the largest number of nodes is thrown
2373   out. The crossover process happens up to 50 times, and at this point
2374   the DD in the population with the smallest size is chosen as the
2375   result.  This DD must then be built from the reference DD. <P>
2376 <DL>
2377  <DT> <A HREF="cuddAllDet.html#cuddGa" TARGET="MAIN"><CODE>cuddGa()</CODE></A>
2378  <DD> Genetic algorithm for DD reordering.
2379
2380  <DT> <A HREF="cuddAllDet.html#make_random" TARGET="MAIN"><CODE>make_random()</CODE></A>
2381  <DD> Generates the random sequences for the initial population.
2382
2383  <DT> <A HREF="cuddAllDet.html#sift_up" TARGET="MAIN"><CODE>sift_up()</CODE></A>
2384  <DD> Moves one variable up.
2385
2386  <DT> <A HREF="cuddAllDet.html#build_dd" TARGET="MAIN"><CODE>build_dd()</CODE></A>
2387  <DD> Builds a DD from a given order.
2388
2389  <DT> <A HREF="cuddAllDet.html#largest" TARGET="MAIN"><CODE>largest()</CODE></A>
2390  <DD> Finds the largest DD in the population.
2391
2392  <DT> <A HREF="cuddAllDet.html#rand_int" TARGET="MAIN"><CODE>rand_int()</CODE></A>
2393  <DD> Generates a random number between 0 and the integer a.
2394
2395  <DT> <A HREF="cuddAllDet.html#array_hash" TARGET="MAIN"><CODE>array_hash()</CODE></A>
2396  <DD> Hash function for the computed table.
2397
2398  <DT> <A HREF="cuddAllDet.html#array_compare" TARGET="MAIN"><CODE>array_compare()</CODE></A>
2399  <DD> Comparison function for the computed table.
2400
2401  <DT> <A HREF="cuddAllDet.html#find_best" TARGET="MAIN"><CODE>find_best()</CODE></A>
2402  <DD> Returns the index of the fittest individual.
2403
2404  <DT> <A HREF="cuddAllDet.html#find_average_fitness" TARGET="MAIN"><CODE>find_average_fitness()</CODE></A>
2405  <DD> Returns the average fitness of the population.
2406
2407  <DT> <A HREF="cuddAllDet.html#PMX" TARGET="MAIN"><CODE>PMX()</CODE></A>
2408  <DD> Performs the crossover between two parents.
2409
2410  <DT> <A HREF="cuddAllDet.html#roulette" TARGET="MAIN"><CODE>roulette()</CODE></A>
2411  <DD> Selects two parents with the roulette wheel method.
2412
2413 </DL>
2414 <HR>
2415 <A NAME="cuddGroup.c"><H1>cuddGroup.c</H1></A>
2416 Functions for group sifting. <P>
2417 <B>By: Shipra Panda, Fabio Somenzi</B><P>
2418 External procedures included in this file:
2419                 <ul>
2420                 <li> Cudd_MakeTreeNode()
2421                 </ul>
2422         Internal procedures included in this file:
2423                 <ul>
2424                 <li> cuddTreeSifting()
2425                 </ul>
2426         Static procedures included in this module:
2427                 <ul>
2428                 <li> ddTreeSiftingAux()
2429                 <li> ddCountInternalMtrNodes()
2430                 <li> ddReorderChildren()
2431                 <li> ddFindNodeHiLo()
2432                 <li> ddUniqueCompareGroup()
2433                 <li> ddGroupSifting()
2434                 <li> ddCreateGroup()
2435                 <li> ddGroupSiftingAux()
2436                 <li> ddGroupSiftingUp()
2437                 <li> ddGroupSiftingDown()
2438                 <li> ddGroupMove()
2439                 <li> ddGroupMoveBackward()
2440                 <li> ddGroupSiftingBackward()
2441                 <li> ddMergeGroups()
2442                 <li> ddDissolveGroup()
2443                 <li> ddNoCheck()
2444                 <li> ddSecDiffCheck()
2445                 <li> ddExtSymmCheck()
2446                 <li> ddVarGroupCheck()
2447                 <li> ddSetVarHandled()
2448                 <li> ddResetVarHandled()
2449                 <li> ddIsVarHandled()
2450                 </ul> <P>
2451 <DL>
2452  <DT> <A HREF="cuddAllDet.html#Cudd_MakeTreeNode" TARGET="MAIN"><CODE>Cudd_MakeTreeNode()</CODE></A>
2453  <DD> Creates a new variable group.
2454
2455  <DT> <A HREF="cuddAllDet.html#cuddTreeSifting" TARGET="MAIN"><CODE>cuddTreeSifting()</CODE></A>
2456  <DD> Tree sifting algorithm.
2457
2458  <DT> <A HREF="cuddAllDet.html#ddTreeSiftingAux" TARGET="MAIN"><CODE>ddTreeSiftingAux()</CODE></A>
2459  <DD> Visits the group tree and reorders each group.
2460
2461  <DT> <A HREF="cuddAllDet.html#ddCountInternalMtrNodes" TARGET="MAIN"><CODE>ddCountInternalMtrNodes()</CODE></A>
2462  <DD> Counts the number of internal nodes of the group tree.
2463
2464  <DT> <A HREF="cuddAllDet.html#ddReorderChildren" TARGET="MAIN"><CODE>ddReorderChildren()</CODE></A>
2465  <DD> Reorders the children of a group tree node according to
2466   the options.
2467
2468  <DT> <A HREF="cuddAllDet.html#ddFindNodeHiLo" TARGET="MAIN"><CODE>ddFindNodeHiLo()</CODE></A>
2469  <DD> Finds the lower and upper bounds of the group represented
2470   by treenode.
2471
2472  <DT> <A HREF="cuddAllDet.html#ddUniqueCompareGroup" TARGET="MAIN"><CODE>ddUniqueCompareGroup()</CODE></A>
2473  <DD> Comparison function used by qsort.
2474
2475  <DT> <A HREF="cuddAllDet.html#ddGroupSifting" TARGET="MAIN"><CODE>ddGroupSifting()</CODE></A>
2476  <DD> Sifts from treenode->low to treenode->high.
2477
2478  <DT> <A HREF="cuddAllDet.html#ddCreateGroup" TARGET="MAIN"><CODE>ddCreateGroup()</CODE></A>
2479  <DD> Creates a group encompassing variables from x to y in the
2480   DD table.
2481
2482  <DT> <A HREF="cuddAllDet.html#ddGroupSiftingAux" TARGET="MAIN"><CODE>ddGroupSiftingAux()</CODE></A>
2483  <DD> Sifts one variable up and down until it has taken all
2484   positions. Checks for aggregation.
2485
2486  <DT> <A HREF="cuddAllDet.html#ddGroupSiftingUp" TARGET="MAIN"><CODE>ddGroupSiftingUp()</CODE></A>
2487  <DD> Sifts up a variable until either it reaches position xLow
2488   or the size of the DD heap increases too much.
2489
2490  <DT> <A HREF="cuddAllDet.html#ddGroupSiftingDown" TARGET="MAIN"><CODE>ddGroupSiftingDown()</CODE></A>
2491  <DD> Sifts down a variable until it reaches position xHigh.
2492
2493  <DT> <A HREF="cuddAllDet.html#ddGroupMove" TARGET="MAIN"><CODE>ddGroupMove()</CODE></A>
2494  <DD> Swaps two groups and records the move.
2495
2496  <DT> <A HREF="cuddAllDet.html#ddGroupMoveBackward" TARGET="MAIN"><CODE>ddGroupMoveBackward()</CODE></A>
2497  <DD> Undoes the swap two groups.
2498
2499  <DT> <A HREF="cuddAllDet.html#ddGroupSiftingBackward" TARGET="MAIN"><CODE>ddGroupSiftingBackward()</CODE></A>
2500  <DD> Determines the best position for a variables and returns
2501   it there.
2502
2503  <DT> <A HREF="cuddAllDet.html#ddMergeGroups" TARGET="MAIN"><CODE>ddMergeGroups()</CODE></A>
2504  <DD> Merges groups in the DD table.
2505
2506  <DT> <A HREF="cuddAllDet.html#ddDissolveGroup" TARGET="MAIN"><CODE>ddDissolveGroup()</CODE></A>
2507  <DD> Dissolves a group in the DD table.
2508
2509  <DT> <A HREF="cuddAllDet.html#ddNoCheck" TARGET="MAIN"><CODE>ddNoCheck()</CODE></A>
2510  <DD> Pretends to check two variables for aggregation.
2511
2512  <DT> <A HREF="cuddAllDet.html#ddSecDiffCheck" TARGET="MAIN"><CODE>ddSecDiffCheck()</CODE></A>
2513  <DD> Checks two variables for aggregation.
2514
2515  <DT> <A HREF="cuddAllDet.html#ddExtSymmCheck" TARGET="MAIN"><CODE>ddExtSymmCheck()</CODE></A>
2516  <DD> Checks for extended symmetry of x and y.
2517
2518  <DT> <A HREF="cuddAllDet.html#ddVarGroupCheck" TARGET="MAIN"><CODE>ddVarGroupCheck()</CODE></A>
2519  <DD> Checks for grouping of x and y.
2520
2521  <DT> <A HREF="cuddAllDet.html#ddSetVarHandled" TARGET="MAIN"><CODE>ddSetVarHandled()</CODE></A>
2522  <DD> Sets a variable to already handled.
2523
2524  <DT> <A HREF="cuddAllDet.html#ddResetVarHandled" TARGET="MAIN"><CODE>ddResetVarHandled()</CODE></A>
2525  <DD> Resets a variable to be processed.
2526
2527  <DT> <A HREF="cuddAllDet.html#ddIsVarHandled" TARGET="MAIN"><CODE>ddIsVarHandled()</CODE></A>
2528  <DD> Checks whether a variables is already handled.
2529
2530 </DL>
2531 <HR>
2532 <A NAME="cuddHarwell.c"><H1>cuddHarwell.c</H1></A>
2533 Function to read a matrix in Harwell format. <P>
2534 <B>By: Fabio Somenzi</B><P>
2535 External procedures included in this module:
2536                 <ul>
2537                 <li> Cudd_addHarwell()
2538                 </ul> <P>
2539 <DL>
2540  <DT> <A HREF="cuddAllDet.html#Cudd_addHarwell" TARGET="MAIN"><CODE>Cudd_addHarwell()</CODE></A>
2541  <DD> Reads in a matrix in the format of the Harwell-Boeing
2542   benchmark suite.
2543
2544 </DL>
2545 <HR>
2546 <A NAME="cuddInit.c"><H1>cuddInit.c</H1></A>
2547 Functions to initialize and shut down the DD manager. <P>
2548 <B>By: Fabio Somenzi</B><P>
2549 External procedures included in this module:
2550                 <ul>
2551                 <li> Cudd_Init()
2552                 <li> Cudd_Quit()
2553                 </ul>
2554                Internal procedures included in this module:
2555                 <ul>
2556                 <li> cuddZddInitUniv()
2557                 <li> cuddZddFreeUniv()
2558                 </ul> <P>
2559 <DL>
2560  <DT> <A HREF="cuddAllDet.html#Cudd_Init" TARGET="MAIN"><CODE>Cudd_Init()</CODE></A>
2561  <DD> Creates a new DD manager.
2562
2563  <DT> <A HREF="cuddAllDet.html#Cudd_Quit" TARGET="MAIN"><CODE>Cudd_Quit()</CODE></A>
2564  <DD> Deletes resources associated with a DD manager.
2565
2566  <DT> <A HREF="cuddAllDet.html#cuddZddInitUniv" TARGET="MAIN"><CODE>cuddZddInitUniv()</CODE></A>
2567  <DD> Initializes the ZDD universe.
2568
2569  <DT> <A HREF="cuddAllDet.html#cuddZddFreeUniv" TARGET="MAIN"><CODE>cuddZddFreeUniv()</CODE></A>
2570  <DD> Frees the ZDD universe.
2571
2572 </DL>
2573 <HR>
2574 <A NAME="cuddInteract.c"><H1>cuddInteract.c</H1></A>
2575 Functions to manipulate the variable interaction matrix. <P>
2576 <B>By: Fabio Somenzi</B><P>
2577 Internal procedures included in this file:
2578         <ul>
2579         <li> cuddSetInteract()
2580         <li> cuddTestInteract()
2581         <li> cuddInitInteract()
2582         </ul>
2583   Static procedures included in this file:
2584         <ul>
2585         <li> ddSuppInteract()
2586         <li> ddClearLocal()
2587         <li> ddUpdateInteract()
2588         <li> ddClearGlobal()
2589         </ul>
2590   The interaction matrix tells whether two variables are
2591   both in the support of some function of the DD. The main use of the
2592   interaction matrix is in the in-place swapping. Indeed, if two
2593   variables do not interact, there is no arc connecting the two layers;
2594   therefore, the swap can be performed in constant time, without
2595   scanning the subtables. Another use of the interaction matrix is in
2596   the computation of the lower bounds for sifting. Finally, the
2597   interaction matrix can be used to speed up aggregation checks in
2598   symmetric and group sifting.<p>
2599   The computation of the interaction matrix is done with a series of
2600   depth-first searches. The searches start from those nodes that have
2601   only external references. The matrix is stored as a packed array of bits;
2602   since it is symmetric, only the upper triangle is kept in memory.
2603   As a final remark, we note that there may be variables that do
2604   intercat, but that for a given variable order have no arc connecting
2605   their layers when they are adjacent. <P>
2606 <DL>
2607  <DT> <A HREF="cuddAllDet.html#cuddSetInteract" TARGET="MAIN"><CODE>cuddSetInteract()</CODE></A>
2608  <DD> Set interaction matrix entries.
2609
2610  <DT> <A HREF="cuddAllDet.html#cuddTestInteract" TARGET="MAIN"><CODE>cuddTestInteract()</CODE></A>
2611  <DD> Test interaction matrix entries.
2612
2613  <DT> <A HREF="cuddAllDet.html#cuddInitInteract" TARGET="MAIN"><CODE>cuddInitInteract()</CODE></A>
2614  <DD> Initializes the interaction matrix.
2615
2616  <DT> <A HREF="cuddAllDet.html#ddSuppInteract" TARGET="MAIN"><CODE>ddSuppInteract()</CODE></A>
2617  <DD> Find the support of f.
2618
2619  <DT> <A HREF="cuddAllDet.html#ddClearLocal" TARGET="MAIN"><CODE>ddClearLocal()</CODE></A>
2620  <DD> Performs a DFS from f, clearing the LSB of the then pointers.
2621
2622  <DT> <A HREF="cuddAllDet.html#ddUpdateInteract" TARGET="MAIN"><CODE>ddUpdateInteract()</CODE></A>
2623  <DD> Marks as interacting all pairs of variables that appear in
2624   support.
2625
2626  <DT> <A HREF="cuddAllDet.html#ddClearGlobal" TARGET="MAIN"><CODE>ddClearGlobal()</CODE></A>
2627  <DD> Scans the DD and clears the LSB of the next pointers.
2628
2629 </DL>
2630 <HR>
2631 <A NAME="cuddLCache.c"><H1>cuddLCache.c</H1></A>
2632 Functions for local caches. <P>
2633 <B>By: Fabio Somenzi</B><P>
2634 Internal procedures included in this module:
2635                 <ul>
2636                 <li> cuddLocalCacheInit()
2637                 <li> cuddLocalCacheQuit()
2638                 <li> cuddLocalCacheInsert()
2639                 <li> cuddLocalCacheLookup()
2640                 <li> cuddLocalCacheClearDead()
2641                 <li> cuddLocalCacheClearAll()
2642                 <li> cuddLocalCacheProfile()
2643                 <li> cuddHashTableInit()
2644                 <li> cuddHashTableQuit()
2645                 <li> cuddHashTableInsert()
2646                 <li> cuddHashTableLookup()
2647                 <li> cuddHashTableInsert2()
2648                 <li> cuddHashTableLookup2()
2649                 <li> cuddHashTableInsert3()
2650                 <li> cuddHashTableLookup3()
2651                 </ul>
2652             Static procedures included in this module:
2653                 <ul>
2654                 <li> cuddLocalCacheResize()
2655                 <li> ddLCHash()
2656                 <li> cuddLocalCacheAddToList()
2657                 <li> cuddLocalCacheRemoveFromList()
2658                 <li> cuddHashTableResize()
2659                 <li> cuddHashTableAlloc()
2660                 </ul> <P>
2661 <DL>
2662  <DT> <A HREF="cuddAllDet.html#cuddLocalCacheInit" TARGET="MAIN"><CODE>cuddLocalCacheInit()</CODE></A>
2663  <DD> Initializes a local computed table.
2664
2665  <DT> <A HREF="cuddAllDet.html#cuddLocalCacheQuit" TARGET="MAIN"><CODE>cuddLocalCacheQuit()</CODE></A>
2666  <DD> Shuts down a local computed table.
2667
2668  <DT> <A HREF="cuddAllDet.html#cuddLocalCacheInsert" TARGET="MAIN"><CODE>cuddLocalCacheInsert()</CODE></A>
2669  <DD> Inserts a result in a local cache.
2670
2671  <DT> <A HREF="cuddAllDet.html#cuddLocalCacheLookup" TARGET="MAIN"><CODE>cuddLocalCacheLookup()</CODE></A>
2672  <DD> Looks up in a local cache.
2673
2674  <DT> <A HREF="cuddAllDet.html#cuddLocalCacheClearDead" TARGET="MAIN"><CODE>cuddLocalCacheClearDead()</CODE></A>
2675  <DD> Clears the dead entries of the local caches of a manager.
2676
2677  <DT> <A HREF="cuddAllDet.html#cuddLocalCacheClearAll" TARGET="MAIN"><CODE>cuddLocalCacheClearAll()</CODE></A>
2678  <DD> Clears the local caches of a manager.
2679
2680  <DT> <A HREF="cuddAllDet.html#cuddLocalCacheProfile" TARGET="MAIN"><CODE>cuddLocalCacheProfile()</CODE></A>
2681  <DD> Computes and prints a profile of a local cache usage.
2682
2683  <DT> <A HREF="cuddAllDet.html#cuddHashTableInit" TARGET="MAIN"><CODE>cuddHashTableInit()</CODE></A>
2684  <DD> Initializes a hash table.
2685
2686  <DT> <A HREF="cuddAllDet.html#cuddHashTableQuit" TARGET="MAIN"><CODE>cuddHashTableQuit()</CODE></A>
2687  <DD> Shuts down a hash table.
2688
2689  <DT> <A HREF="cuddAllDet.html#cuddHashTableInsert" TARGET="MAIN"><CODE>cuddHashTableInsert()</CODE></A>
2690  <DD> Inserts an item in a hash table.
2691
2692  <DT> <A HREF="cuddAllDet.html#cuddHashTableLookup" TARGET="MAIN"><CODE>cuddHashTableLookup()</CODE></A>
2693  <DD> Looks up a key in a hash table.
2694
2695  <DT> <A HREF="cuddAllDet.html#cuddHashTableInsert1" TARGET="MAIN"><CODE>cuddHashTableInsert1()</CODE></A>
2696  <DD> Inserts an item in a hash table.
2697
2698  <DT> <A HREF="cuddAllDet.html#cuddHashTableLookup1" TARGET="MAIN"><CODE>cuddHashTableLookup1()</CODE></A>
2699  <DD> Looks up a key consisting of one pointer in a hash table.
2700
2701  <DT> <A HREF="cuddAllDet.html#cuddHashTableInsert2" TARGET="MAIN"><CODE>cuddHashTableInsert2()</CODE></A>
2702  <DD> Inserts an item in a hash table.
2703
2704  <DT> <A HREF="cuddAllDet.html#cuddHashTableLookup2" TARGET="MAIN"><CODE>cuddHashTableLookup2()</CODE></A>
2705  <DD> Looks up a key consisting of two pointers in a hash table.
2706
2707  <DT> <A HREF="cuddAllDet.html#cuddHashTableInsert3" TARGET="MAIN"><CODE>cuddHashTableInsert3()</CODE></A>
2708  <DD> Inserts an item in a hash table.
2709
2710  <DT> <A HREF="cuddAllDet.html#cuddHashTableLookup3" TARGET="MAIN"><CODE>cuddHashTableLookup3()</CODE></A>
2711  <DD> Looks up a key consisting of three pointers in a hash table.
2712
2713  <DT> <A HREF="cuddAllDet.html#cuddLocalCacheResize" TARGET="MAIN"><CODE>cuddLocalCacheResize()</CODE></A>
2714  <DD> Resizes a local cache.
2715
2716  <DT> <A HREF="cuddAllDet.html#ddLCHash" TARGET="MAIN"><CODE>ddLCHash()</CODE></A>
2717  <DD> Computes the hash value for a local cache.
2718
2719  <DT> <A HREF="cuddAllDet.html#cuddLocalCacheAddToList" TARGET="MAIN"><CODE>cuddLocalCacheAddToList()</CODE></A>
2720  <DD> Inserts a local cache in the manager list.
2721
2722  <DT> <A HREF="cuddAllDet.html#cuddLocalCacheRemoveFromList" TARGET="MAIN"><CODE>cuddLocalCacheRemoveFromList()</CODE></A>
2723  <DD> Removes a local cache from the manager list.
2724
2725  <DT> <A HREF="cuddAllDet.html#cuddHashTableResize" TARGET="MAIN"><CODE>cuddHashTableResize()</CODE></A>
2726  <DD> Resizes a hash table.
2727
2728  <DT> <A HREF="cuddAllDet.html#cuddHashTableAlloc" TARGET="MAIN"><CODE>cuddHashTableAlloc()</CODE></A>
2729  <DD> Fast storage allocation for items in a hash table.
2730
2731 </DL>
2732 <HR>
2733 <A NAME="cuddLevelQ.c"><H1>cuddLevelQ.c</H1></A>
2734 Procedure to manage level queues. <P>
2735 <B>By: Fabio Somenzi</B><P>
2736 The functions in this file allow an application to
2737   easily manipulate a queue where nodes are prioritized by level. The
2738   emphasis is on efficiency. Therefore, the queue items can have
2739   variable size.  If the application does not need to attach
2740   information to the nodes, it can declare the queue items to be of
2741   type DdQueueItem. Otherwise, it can declare them to be of a
2742   structure type such that the first three fields are data
2743   pointers. The third pointer points to the node.  The first two
2744   pointers are used by the level queue functions. The remaining fields
2745   are initialized to 0 when a new item is created, and are then left
2746   to the exclusive use of the application. On the DEC Alphas the three
2747   pointers must be 32-bit pointers when CUDD is compiled with 32-bit
2748   pointers.  The level queue functions make sure that each node
2749   appears at most once in the queue. They do so by keeping a hash
2750   table where the node is used as key.  Queue items are recycled via a
2751   free list for efficiency.
2752
2753   Internal procedures provided by this module:
2754                 <ul>
2755                 <li> cuddLevelQueueInit()
2756                 <li> cuddLevelQueueQuit()
2757                 <li> cuddLevelQueueEnqueue()
2758                 <li> cuddLevelQueueDequeue()
2759                 </ul>
2760   Static procedures included in this module:
2761                 <ul>
2762                 <li> hashLookup()
2763                 <li> hashInsert()
2764                 <li> hashDelete()
2765                 <li> hashResize()
2766                 </ul> <P>
2767 <DL>
2768  <DT> <A HREF="cuddAllDet.html#cuddLevelQueueInit" TARGET="MAIN"><CODE>cuddLevelQueueInit()</CODE></A>
2769  <DD> Initializes a level queue.
2770
2771  <DT> <A HREF="cuddAllDet.html#cuddLevelQueueQuit" TARGET="MAIN"><CODE>cuddLevelQueueQuit()</CODE></A>
2772  <DD> Shuts down a level queue.
2773
2774  <DT> <A HREF="cuddAllDet.html#cuddLevelQueueEnqueue" TARGET="MAIN"><CODE>cuddLevelQueueEnqueue()</CODE></A>
2775  <DD> Inserts a new key in a level queue.
2776
2777  <DT> <A HREF="cuddAllDet.html#cuddLevelQueueDequeue" TARGET="MAIN"><CODE>cuddLevelQueueDequeue()</CODE></A>
2778  <DD> Remove an item from the front of a level queue.
2779
2780  <DT> <A HREF="cuddAllDet.html#hashLookup" TARGET="MAIN"><CODE>hashLookup()</CODE></A>
2781  <DD> Looks up a key in the hash table of a level queue.
2782
2783  <DT> <A HREF="cuddAllDet.html#hashInsert" TARGET="MAIN"><CODE>hashInsert()</CODE></A>
2784  <DD> Inserts an item in the hash table of a level queue.
2785
2786  <DT> <A HREF="cuddAllDet.html#hashDelete" TARGET="MAIN"><CODE>hashDelete()</CODE></A>
2787  <DD> Removes an item from the hash table of a level queue.
2788
2789  <DT> <A HREF="cuddAllDet.html#hashResize" TARGET="MAIN"><CODE>hashResize()</CODE></A>
2790  <DD> Resizes the hash table of a level queue.
2791
2792 </DL>
2793 <HR>
2794 <A NAME="cuddLinear.c"><H1>cuddLinear.c</H1></A>
2795 Functions for DD reduction by linear transformations. <P>
2796 <B>By: Fabio Somenzi</B><P>
2797 Internal procedures included in this module:
2798                 <ul>
2799                 <li> cuddLinearAndSifting()
2800                 <li> cuddLinearInPlace()
2801                 <li> cuddUpdateInteractionMatrix()
2802                 <li> cuddInitLinear()
2803                 <li> cuddResizeLinear()
2804                 </ul>
2805         Static procedures included in this module:
2806                 <ul>
2807                 <li> ddLinearUniqueCompare()
2808                 <li> ddLinearAndSiftingAux()
2809                 <li> ddLinearAndSiftingUp()
2810                 <li> ddLinearAndSiftingDown()
2811                 <li> ddLinearAndSiftingBackward()
2812                 <li> ddUndoMoves()
2813                 <li> cuddXorLinear()
2814                 </ul> <P>
2815 <DL>
2816  <DT> <A HREF="cuddAllDet.html#Cudd_PrintLinear" TARGET="MAIN"><CODE>Cudd_PrintLinear()</CODE></A>
2817  <DD> Prints the linear transform matrix.
2818
2819  <DT> <A HREF="cuddAllDet.html#Cudd_ReadLinear" TARGET="MAIN"><CODE>Cudd_ReadLinear()</CODE></A>
2820  <DD> Reads an entry of the linear transform matrix.
2821
2822  <DT> <A HREF="cuddAllDet.html#cuddLinearAndSifting" TARGET="MAIN"><CODE>cuddLinearAndSifting()</CODE></A>
2823  <DD> BDD reduction based on combination of sifting and linear
2824   transformations.
2825
2826  <DT> <A HREF="cuddAllDet.html#cuddLinearInPlace" TARGET="MAIN"><CODE>cuddLinearInPlace()</CODE></A>
2827  <DD> Linearly combines two adjacent variables.
2828
2829  <DT> <A HREF="cuddAllDet.html#cuddUpdateInteractionMatrix" TARGET="MAIN"><CODE>cuddUpdateInteractionMatrix()</CODE></A>
2830  <DD> Updates the interaction matrix.
2831
2832  <DT> <A HREF="cuddAllDet.html#cuddInitLinear" TARGET="MAIN"><CODE>cuddInitLinear()</CODE></A>
2833  <DD> Initializes the linear transform matrix.
2834
2835  <DT> <A HREF="cuddAllDet.html#cuddResizeLinear" TARGET="MAIN"><CODE>cuddResizeLinear()</CODE></A>
2836  <DD> Resizes the linear transform matrix.
2837
2838  <DT> <A HREF="cuddAllDet.html#ddLinearUniqueCompare" TARGET="MAIN"><CODE>ddLinearUniqueCompare()</CODE></A>
2839  <DD> Comparison function used by qsort.
2840
2841  <DT> <A HREF="cuddAllDet.html#ddLinearAndSiftingAux" TARGET="MAIN"><CODE>ddLinearAndSiftingAux()</CODE></A>
2842  <DD> Given xLow <= x <= xHigh moves x up and down between the
2843   boundaries.
2844
2845  <DT> <A HREF="cuddAllDet.html#ddLinearAndSiftingUp" TARGET="MAIN"><CODE>ddLinearAndSiftingUp()</CODE></A>
2846  <DD> Sifts a variable up and applies linear transformations.
2847
2848  <DT> <A HREF="cuddAllDet.html#ddLinearAndSiftingDown" TARGET="MAIN"><CODE>ddLinearAndSiftingDown()</CODE></A>
2849  <DD> Sifts a variable down and applies linear transformations.
2850
2851  <DT> <A HREF="cuddAllDet.html#ddLinearAndSiftingBackward" TARGET="MAIN"><CODE>ddLinearAndSiftingBackward()</CODE></A>
2852  <DD> Given a set of moves, returns the DD heap to the order
2853   giving the minimum size.
2854
2855  <DT> <A HREF="cuddAllDet.html#ddUndoMoves" TARGET="MAIN"><CODE>ddUndoMoves()</CODE></A>
2856  <DD> Given a set of moves, returns the DD heap to the order
2857   in effect before the moves.
2858
2859  <DT> <A HREF="cuddAllDet.html#cuddXorLinear" TARGET="MAIN"><CODE>cuddXorLinear()</CODE></A>
2860  <DD> XORs two rows of the linear transform matrix.
2861
2862 </DL>
2863 <HR>
2864 <A NAME="cuddLiteral.c"><H1>cuddLiteral.c</H1></A>
2865 Functions for manipulation of literal sets represented by
2866   BDDs. <P>
2867 <B>By: Fabio Somenzi</B><P>
2868 External procedures included in this file:
2869                 <ul>
2870                 <li> Cudd_bddLiteralSetIntersection()
2871                 </ul>
2872             Internal procedures included in this file:
2873                 <ul>
2874                 <li> cuddBddLiteralSetIntersectionRecur()
2875                 </ul> <P>
2876 <DL>
2877  <DT> <A HREF="cuddAllDet.html#Cudd_bddLiteralSetIntersection" TARGET="MAIN"><CODE>Cudd_bddLiteralSetIntersection()</CODE></A>
2878  <DD> Computes the intesection of two sets of literals
2879   represented as BDDs.
2880
2881  <DT> <A HREF="cuddAllDet.html#cuddBddLiteralSetIntersectionRecur" TARGET="MAIN"><CODE>cuddBddLiteralSetIntersectionRecur()</CODE></A>
2882  <DD> Performs the recursive step of
2883   Cudd_bddLiteralSetIntersection.
2884
2885 </DL>
2886 <HR>
2887 <A NAME="cuddMatMult.c"><H1>cuddMatMult.c</H1></A>
2888 Matrix multiplication functions. <P>
2889 <B>By: Fabio Somenzi</B><P>
2890 External procedures included in this module:
2891                 <ul>
2892                 <li> Cudd_addMatrixMultiply()
2893                 <li> Cudd_addTimesPlus()
2894                 <li> Cudd_addTriangle()
2895                 <li> Cudd_addOuterSum()
2896                 </ul>
2897         Static procedures included in this module:
2898                 <ul>
2899                 <li> addMMRecur()
2900                 <li> addTriangleRecur()
2901                 <li> cuddAddOuterSumRecur()
2902                 </ul> <P>
2903 <DL>
2904  <DT> <A HREF="cuddAllDet.html#Cudd_addMatrixMultiply" TARGET="MAIN"><CODE>Cudd_addMatrixMultiply()</CODE></A>
2905  <DD> Calculates the product of two matrices represented as
2906   ADDs.
2907
2908  <DT> <A HREF="cuddAllDet.html#Cudd_addTimesPlus" TARGET="MAIN"><CODE>Cudd_addTimesPlus()</CODE></A>
2909  <DD> Calculates the product of two matrices represented as
2910   ADDs.
2911
2912  <DT> <A HREF="cuddAllDet.html#Cudd_addTriangle" TARGET="MAIN"><CODE>Cudd_addTriangle()</CODE></A>
2913  <DD> Performs the triangulation step for the shortest path
2914   computation.
2915
2916  <DT> <A HREF="cuddAllDet.html#Cudd_addOuterSum" TARGET="MAIN"><CODE>Cudd_addOuterSum()</CODE></A>
2917  <DD> Takes the minimum of a matrix and the outer sum of two vectors.
2918
2919  <DT> <A HREF="cuddAllDet.html#addMMRecur" TARGET="MAIN"><CODE>addMMRecur()</CODE></A>
2920  <DD> Performs the recursive step of Cudd_addMatrixMultiply.
2921
2922  <DT> <A HREF="cuddAllDet.html#addTriangleRecur" TARGET="MAIN"><CODE>addTriangleRecur()</CODE></A>
2923  <DD> Performs the recursive step of Cudd_addTriangle.
2924
2925  <DT> <A HREF="cuddAllDet.html#cuddAddOuterSumRecur" TARGET="MAIN"><CODE>cuddAddOuterSumRecur()</CODE></A>
2926  <DD> Performs the recursive step of Cudd_addOuterSum.
2927
2928 </DL>
2929 <HR>
2930 <A NAME="cuddPriority.c"><H1>cuddPriority.c</H1></A>
2931 Priority functions. <P>
2932 <B>By: Fabio Somenzi</B><P>
2933 External procedures included in this file:
2934             <ul>
2935             <li> Cudd_PrioritySelect()
2936             <li> Cudd_Xgty()
2937             <li> Cudd_Xeqy()
2938             <li> Cudd_addXeqy()
2939             <li> Cudd_Dxygtdxz()
2940             <li> Cudd_Dxygtdyz()
2941             <li> Cudd_Inequality()
2942             <li> Cudd_Disequality()
2943             <li> Cudd_bddInterval()
2944             <li> Cudd_CProjection()
2945             <li> Cudd_addHamming()
2946             <li> Cudd_MinHammingDist()
2947             <li> Cudd_bddClosestCube()
2948             </ul>
2949         Internal procedures included in this module:
2950             <ul>
2951             <li> cuddCProjectionRecur()
2952             <li> cuddBddClosestCube()
2953             </ul>
2954         Static procedures included in this module:
2955             <ul>
2956             <li> cuddMinHammingDistRecur()
2957             <li> separateCube()
2958             <li> createResult()
2959             </ul> <P>
2960 <DL>
2961  <DT> <A HREF="cuddAllDet.html#Cudd_PrioritySelect" TARGET="MAIN"><CODE>Cudd_PrioritySelect()</CODE></A>
2962  <DD> Selects pairs from R using a priority function.
2963
2964  <DT> <A HREF="cuddAllDet.html#Cudd_Xgty" TARGET="MAIN"><CODE>Cudd_Xgty()</CODE></A>
2965  <DD> Generates a BDD for the function x &gt; y.
2966
2967  <DT> <A HREF="cuddAllDet.html#Cudd_Xeqy" TARGET="MAIN"><CODE>Cudd_Xeqy()</CODE></A>
2968  <DD> Generates a BDD for the function x==y.
2969
2970  <DT> <A HREF="cuddAllDet.html#Cudd_addXeqy" TARGET="MAIN"><CODE>Cudd_addXeqy()</CODE></A>
2971  <DD> Generates an ADD for the function x==y.
2972
2973  <DT> <A HREF="cuddAllDet.html#Cudd_Dxygtdxz" TARGET="MAIN"><CODE>Cudd_Dxygtdxz()</CODE></A>
2974  <DD> Generates a BDD for the function d(x,y) &gt; d(x,z).
2975
2976  <DT> <A HREF="cuddAllDet.html#Cudd_Dxygtdyz" TARGET="MAIN"><CODE>Cudd_Dxygtdyz()</CODE></A>
2977  <DD> Generates a BDD for the function d(x,y) &gt; d(y,z).
2978
2979  <DT> <A HREF="cuddAllDet.html#Cudd_Inequality" TARGET="MAIN"><CODE>Cudd_Inequality()</CODE></A>
2980  <DD> Generates a BDD for the function x - y &ge; c.
2981
2982  <DT> <A HREF="cuddAllDet.html#Cudd_Disequality" TARGET="MAIN"><CODE>Cudd_Disequality()</CODE></A>
2983  <DD> Generates a BDD for the function x - y != c.
2984
2985  <DT> <A HREF="cuddAllDet.html#Cudd_bddInterval" TARGET="MAIN"><CODE>Cudd_bddInterval()</CODE></A>
2986  <DD> Generates a BDD for the function lowerB &le; x &le; upperB.
2987
2988  <DT> <A HREF="cuddAllDet.html#Cudd_CProjection" TARGET="MAIN"><CODE>Cudd_CProjection()</CODE></A>
2989  <DD> Computes the compatible projection of R w.r.t. cube Y.
2990
2991  <DT> <A HREF="cuddAllDet.html#Cudd_addHamming" TARGET="MAIN"><CODE>Cudd_addHamming()</CODE></A>
2992  <DD> Computes the Hamming distance ADD.
2993
2994  <DT> <A HREF="cuddAllDet.html#Cudd_MinHammingDist" TARGET="MAIN"><CODE>Cudd_MinHammingDist()</CODE></A>
2995  <DD> Returns the minimum Hamming distance between f and minterm.
2996
2997  <DT> <A HREF="cuddAllDet.html#Cudd_bddClosestCube" TARGET="MAIN"><CODE>Cudd_bddClosestCube()</CODE></A>
2998  <DD> Finds a cube of f at minimum Hamming distance from g.
2999
3000  <DT> <A HREF="cuddAllDet.html#cuddCProjectionRecur" TARGET="MAIN"><CODE>cuddCProjectionRecur()</CODE></A>
3001  <DD> Performs the recursive step of Cudd_CProjection.
3002
3003  <DT> <A HREF="cuddAllDet.html#cuddBddClosestCube" TARGET="MAIN"><CODE>cuddBddClosestCube()</CODE></A>
3004  <DD> Performs the recursive step of Cudd_bddClosestCube.
3005
3006  <DT> <A HREF="cuddAllDet.html#cuddMinHammingDistRecur" TARGET="MAIN"><CODE>cuddMinHammingDistRecur()</CODE></A>
3007  <DD> Performs the recursive step of Cudd_MinHammingDist.
3008
3009  <DT> <A HREF="cuddAllDet.html#separateCube" TARGET="MAIN"><CODE>separateCube()</CODE></A>
3010  <DD> Separates cube from distance.
3011
3012  <DT> <A HREF="cuddAllDet.html#createResult" TARGET="MAIN"><CODE>createResult()</CODE></A>
3013  <DD> Builds a result for cache storage.
3014
3015 </DL>
3016 <HR>
3017 <A NAME="cuddRead.c"><H1>cuddRead.c</H1></A>
3018 Functions to read in a matrix <P>
3019 <B>By: Fabio Somenzi</B><P>
3020 External procedures included in this module:
3021                 <ul>
3022                 <li> Cudd_addRead()
3023                 <li> Cudd_bddRead()
3024                 </ul> <P>
3025 <P><B>See Also</B><A HREF="#cudd_addHarwell.c"><CODE>cudd_addHarwell.c</CODE></A>
3026 <DL>
3027  <DT> <A HREF="cuddAllDet.html#Cudd_addRead" TARGET="MAIN"><CODE>Cudd_addRead()</CODE></A>
3028  <DD> Reads in a sparse matrix.
3029
3030  <DT> <A HREF="cuddAllDet.html#Cudd_bddRead" TARGET="MAIN"><CODE>Cudd_bddRead()</CODE></A>
3031  <DD> Reads in a graph (without labels) given as a list of arcs.
3032
3033 </DL>
3034 <HR>
3035 <A NAME="cuddRef.c"><H1>cuddRef.c</H1></A>
3036 Functions that manipulate the reference counts. <P>
3037 <B>By: Fabio Somenzi</B><P>
3038 External procedures included in this module:
3039                     <ul>
3040                     <li> Cudd_Ref()
3041                     <li> Cudd_RecursiveDeref()
3042                     <li> Cudd_IterDerefBdd()
3043                     <li> Cudd_DelayedDerefBdd()
3044                     <li> Cudd_RecursiveDerefZdd()
3045                     <li> Cudd_Deref()
3046                     <li> Cudd_CheckZeroRef()
3047                     </ul>
3048                Internal procedures included in this module:
3049                     <ul>
3050                     <li> cuddReclaim()
3051                     <li> cuddReclaimZdd()
3052                     <li> cuddClearDeathRow()
3053                     <li> cuddShrinkDeathRow()
3054                     <li> cuddIsInDeathRow()
3055                     <li> cuddTimesInDeathRow()
3056                     </ul> <P>
3057 <DL>
3058  <DT> <A HREF="cuddAllDet.html#Cudd_Ref" TARGET="MAIN"><CODE>Cudd_Ref()</CODE></A>
3059  <DD> Increases the reference count of a node, if it is not
3060   saturated.
3061
3062  <DT> <A HREF="cuddAllDet.html#Cudd_RecursiveDeref" TARGET="MAIN"><CODE>Cudd_RecursiveDeref()</CODE></A>
3063  <DD> Decreases the reference count of node n.
3064
3065  <DT> <A HREF="cuddAllDet.html#Cudd_IterDerefBdd" TARGET="MAIN"><CODE>Cudd_IterDerefBdd()</CODE></A>
3066  <DD> Decreases the reference count of BDD node n.
3067
3068  <DT> <A HREF="cuddAllDet.html#Cudd_DelayedDerefBdd" TARGET="MAIN"><CODE>Cudd_DelayedDerefBdd()</CODE></A>
3069  <DD> Decreases the reference count of BDD node n.
3070
3071  <DT> <A HREF="cuddAllDet.html#Cudd_RecursiveDerefZdd" TARGET="MAIN"><CODE>Cudd_RecursiveDerefZdd()</CODE></A>
3072  <DD> Decreases the reference count of ZDD node n.
3073
3074  <DT> <A HREF="cuddAllDet.html#Cudd_Deref" TARGET="MAIN"><CODE>Cudd_Deref()</CODE></A>
3075  <DD> Decreases the reference count of node.
3076
3077  <DT> <A HREF="cuddAllDet.html#Cudd_CheckZeroRef" TARGET="MAIN"><CODE>Cudd_CheckZeroRef()</CODE></A>
3078  <DD> Checks the unique table for nodes with non-zero reference
3079   counts.
3080
3081  <DT> <A HREF="cuddAllDet.html#cuddReclaim" TARGET="MAIN"><CODE>cuddReclaim()</CODE></A>
3082  <DD> Brings children of a dead node back.
3083
3084  <DT> <A HREF="cuddAllDet.html#cuddReclaimZdd" TARGET="MAIN"><CODE>cuddReclaimZdd()</CODE></A>
3085  <DD> Brings children of a dead ZDD node back.
3086
3087  <DT> <A HREF="cuddAllDet.html#cuddShrinkDeathRow" TARGET="MAIN"><CODE>cuddShrinkDeathRow()</CODE></A>
3088  <DD> Shrinks the death row.
3089
3090  <DT> <A HREF="cuddAllDet.html#cuddClearDeathRow" TARGET="MAIN"><CODE>cuddClearDeathRow()</CODE></A>
3091  <DD> Clears the death row.
3092
3093  <DT> <A HREF="cuddAllDet.html#cuddIsInDeathRow" TARGET="MAIN"><CODE>cuddIsInDeathRow()</CODE></A>
3094  <DD> Checks whether a node is in the death row.
3095
3096  <DT> <A HREF="cuddAllDet.html#cuddTimesInDeathRow" TARGET="MAIN"><CODE>cuddTimesInDeathRow()</CODE></A>
3097  <DD> Counts how many times a node is in the death row.
3098
3099 </DL>
3100 <HR>
3101 <A NAME="cuddReorder.c"><H1>cuddReorder.c</H1></A>
3102 Functions for dynamic variable reordering. <P>
3103 <B>By: Shipra Panda, Bernard Plessier, Fabio Somenzi</B><P>
3104 External procedures included in this file:
3105                 <ul>
3106                 <li> Cudd_ReduceHeap()
3107                 <li> Cudd_ShuffleHeap()
3108                 </ul>
3109         Internal procedures included in this module:
3110                 <ul>
3111                 <li> cuddDynamicAllocNode()
3112                 <li> cuddSifting()
3113                 <li> cuddSwapping()
3114                 <li> cuddNextHigh()
3115                 <li> cuddNextLow()
3116                 <li> cuddSwapInPlace()
3117                 <li> cuddBddAlignToZdd()
3118                 </ul>
3119         Static procedures included in this module:
3120                 <ul>
3121                 <li> ddUniqueCompare()
3122                 <li> ddSwapAny()
3123                 <li> ddSiftingAux()
3124                 <li> ddSiftingUp()
3125                 <li> ddSiftingDown()
3126                 <li> ddSiftingBackward()
3127                 <li> ddReorderPreprocess()
3128                 <li> ddReorderPostprocess()
3129                 <li> ddShuffle()
3130                 <li> ddSiftUp()
3131                 <li> bddFixTree()
3132                 </ul> <P>
3133 <DL>
3134  <DT> <A HREF="cuddAllDet.html#Cudd_ReduceHeap" TARGET="MAIN"><CODE>Cudd_ReduceHeap()</CODE></A>
3135  <DD> Main dynamic reordering routine.
3136
3137  <DT> <A HREF="cuddAllDet.html#Cudd_ShuffleHeap" TARGET="MAIN"><CODE>Cudd_ShuffleHeap()</CODE></A>
3138  <DD> Reorders variables according to given permutation.
3139
3140  <DT> <A HREF="cuddAllDet.html#cuddDynamicAllocNode" TARGET="MAIN"><CODE>cuddDynamicAllocNode()</CODE></A>
3141  <DD> Dynamically allocates a Node.
3142
3143  <DT> <A HREF="cuddAllDet.html#cuddSifting" TARGET="MAIN"><CODE>cuddSifting()</CODE></A>
3144  <DD> Implementation of Rudell's sifting algorithm.
3145
3146  <DT> <A HREF="cuddAllDet.html#cuddSwapping" TARGET="MAIN"><CODE>cuddSwapping()</CODE></A>
3147  <DD> Reorders variables by a sequence of (non-adjacent) swaps.
3148
3149  <DT> <A HREF="cuddAllDet.html#cuddNextHigh" TARGET="MAIN"><CODE>cuddNextHigh()</CODE></A>
3150  <DD> Finds the next subtable with a larger index.
3151
3152  <DT> <A HREF="cuddAllDet.html#cuddNextLow" TARGET="MAIN"><CODE>cuddNextLow()</CODE></A>
3153  <DD> Finds the next subtable with a smaller index.
3154
3155  <DT> <A HREF="cuddAllDet.html#cuddSwapInPlace" TARGET="MAIN"><CODE>cuddSwapInPlace()</CODE></A>
3156  <DD> Swaps two adjacent variables.
3157
3158  <DT> <A HREF="cuddAllDet.html#cuddBddAlignToZdd" TARGET="MAIN"><CODE>cuddBddAlignToZdd()</CODE></A>
3159  <DD> Reorders BDD variables according to the order of the ZDD
3160   variables.
3161
3162  <DT> <A HREF="cuddAllDet.html#ddUniqueCompare" TARGET="MAIN"><CODE>ddUniqueCompare()</CODE></A>
3163  <DD> Comparison function used by qsort.
3164
3165  <DT> <A HREF="cuddAllDet.html#ddSwapAny" TARGET="MAIN"><CODE>ddSwapAny()</CODE></A>
3166  <DD> Swaps any two variables.
3167
3168  <DT> <A HREF="cuddAllDet.html#ddSiftingAux" TARGET="MAIN"><CODE>ddSiftingAux()</CODE></A>
3169  <DD> Given xLow <= x <= xHigh moves x up and down between the
3170   boundaries.
3171
3172  <DT> <A HREF="cuddAllDet.html#ddSiftingUp" TARGET="MAIN"><CODE>ddSiftingUp()</CODE></A>
3173  <DD> Sifts a variable up.
3174
3175  <DT> <A HREF="cuddAllDet.html#ddSiftingDown" TARGET="MAIN"><CODE>ddSiftingDown()</CODE></A>
3176  <DD> Sifts a variable down.
3177
3178  <DT> <A HREF="cuddAllDet.html#ddSiftingBackward" TARGET="MAIN"><CODE>ddSiftingBackward()</CODE></A>
3179  <DD> Given a set of moves, returns the DD heap to the position
3180   giving the minimum size.
3181
3182  <DT> <A HREF="cuddAllDet.html#ddReorderPreprocess" TARGET="MAIN"><CODE>ddReorderPreprocess()</CODE></A>
3183  <DD> Prepares the DD heap for dynamic reordering.
3184
3185  <DT> <A HREF="cuddAllDet.html#ddReorderPostprocess" TARGET="MAIN"><CODE>ddReorderPostprocess()</CODE></A>
3186  <DD> Cleans up at the end of reordering.
3187
3188  <DT> <A HREF="cuddAllDet.html#ddShuffle" TARGET="MAIN"><CODE>ddShuffle()</CODE></A>
3189  <DD> Reorders variables according to a given permutation.
3190
3191  <DT> <A HREF="cuddAllDet.html#ddSiftUp" TARGET="MAIN"><CODE>ddSiftUp()</CODE></A>
3192  <DD> Moves one variable up.
3193
3194  <DT> <A HREF="cuddAllDet.html#bddFixTree" TARGET="MAIN"><CODE>bddFixTree()</CODE></A>
3195  <DD> Fixes the BDD variable group tree after a shuffle.
3196
3197  <DT> <A HREF="cuddAllDet.html#ddUpdateMtrTree" TARGET="MAIN"><CODE>ddUpdateMtrTree()</CODE></A>
3198  <DD> Updates the BDD variable group tree before a shuffle.
3199
3200  <DT> <A HREF="cuddAllDet.html#ddCheckPermuation" TARGET="MAIN"><CODE>ddCheckPermuation()</CODE></A>
3201  <DD> Checks the BDD variable group tree before a shuffle.
3202
3203 </DL>
3204 <HR>
3205 <A NAME="cuddSat.c"><H1>cuddSat.c</H1></A>
3206 Functions for the solution of satisfiability related
3207   problems. <P>
3208 <B>By: Seh-Woong Jeong, Fabio Somenzi</B><P>
3209 External procedures included in this file:
3210                 <ul>
3211                 <li> Cudd_Eval()
3212                 <li> Cudd_ShortestPath()
3213                 <li> Cudd_LargestCube()
3214                 <li> Cudd_ShortestLength()
3215                 <li> Cudd_Decreasing()
3216                 <li> Cudd_Increasing()
3217                 <li> Cudd_EquivDC()
3218                 <li> Cudd_bddLeqUnless()
3219                 <li> Cudd_EqualSupNorm()
3220                 <li> Cudd_bddMakePrime()
3221                 </ul>
3222         Internal procedures included in this module:
3223                 <ul>
3224                 <li> cuddBddMakePrime()
3225                 </ul>
3226         Static procedures included in this module:
3227                 <ul>
3228                 <li> freePathPair()
3229                 <li> getShortest()
3230                 <li> getPath()
3231                 <li> getLargest()
3232                 <li> getCube()
3233                 </ul> <P>
3234 <DL>
3235  <DT> <A HREF="cuddAllDet.html#Cudd_Eval" TARGET="MAIN"><CODE>Cudd_Eval()</CODE></A>
3236  <DD> Returns the value of a DD for a given variable assignment.
3237
3238  <DT> <A HREF="cuddAllDet.html#Cudd_ShortestPath" TARGET="MAIN"><CODE>Cudd_ShortestPath()</CODE></A>
3239  <DD> Finds a shortest path in a DD.
3240
3241  <DT> <A HREF="cuddAllDet.html#Cudd_LargestCube" TARGET="MAIN"><CODE>Cudd_LargestCube()</CODE></A>
3242  <DD> Finds a largest cube in a DD.
3243
3244  <DT> <A HREF="cuddAllDet.html#Cudd_ShortestLength" TARGET="MAIN"><CODE>Cudd_ShortestLength()</CODE></A>
3245  <DD> Find the length of the shortest path(s) in a DD.
3246
3247  <DT> <A HREF="cuddAllDet.html#Cudd_Decreasing" TARGET="MAIN"><CODE>Cudd_Decreasing()</CODE></A>
3248  <DD> Determines whether a BDD is negative unate in a
3249   variable.
3250
3251  <DT> <A HREF="cuddAllDet.html#Cudd_Increasing" TARGET="MAIN"><CODE>Cudd_Increasing()</CODE></A>
3252  <DD> Determines whether a BDD is positive unate in a
3253   variable.
3254
3255  <DT> <A HREF="cuddAllDet.html#Cudd_EquivDC" TARGET="MAIN"><CODE>Cudd_EquivDC()</CODE></A>
3256  <DD> Tells whether F and G are identical wherever D is 0.
3257
3258  <DT> <A HREF="cuddAllDet.html#Cudd_bddLeqUnless" TARGET="MAIN"><CODE>Cudd_bddLeqUnless()</CODE></A>
3259  <DD> Tells whether f is less than of equal to G unless D is 1.
3260
3261  <DT> <A HREF="cuddAllDet.html#Cudd_EqualSupNorm" TARGET="MAIN"><CODE>Cudd_EqualSupNorm()</CODE></A>
3262  <DD> Compares two ADDs for equality within tolerance.
3263
3264  <DT> <A HREF="cuddAllDet.html#Cudd_bddMakePrime" TARGET="MAIN"><CODE>Cudd_bddMakePrime()</CODE></A>
3265  <DD> Expands cube to a prime implicant of f.
3266
3267  <DT> <A HREF="cuddAllDet.html#cuddBddMakePrime" TARGET="MAIN"><CODE>cuddBddMakePrime()</CODE></A>
3268  <DD> Performs the recursive step of Cudd_bddMakePrime.
3269
3270  <DT> <A HREF="cuddAllDet.html#freePathPair" TARGET="MAIN"><CODE>freePathPair()</CODE></A>
3271  <DD> Frees the entries of the visited symbol table.
3272
3273  <DT> <A HREF="cuddAllDet.html#getShortest" TARGET="MAIN"><CODE>getShortest()</CODE></A>
3274  <DD> Finds the length of the shortest path(s) in a DD.
3275
3276  <DT> <A HREF="cuddAllDet.html#getPath" TARGET="MAIN"><CODE>getPath()</CODE></A>
3277  <DD> Build a BDD for a shortest path of f.
3278
3279  <DT> <A HREF="cuddAllDet.html#getLargest" TARGET="MAIN"><CODE>getLargest()</CODE></A>
3280  <DD> Finds the size of the largest cube(s) in a DD.
3281
3282  <DT> <A HREF="cuddAllDet.html#getCube" TARGET="MAIN"><CODE>getCube()</CODE></A>
3283  <DD> Build a BDD for a largest cube of f.
3284
3285 </DL>
3286 <HR>
3287 <A NAME="cuddSign.c"><H1>cuddSign.c</H1></A>
3288 Computation of signatures. <P>
3289 <B>By: Fabio Somenzi</B><P>
3290 External procedures included in this module:
3291                     <ul>
3292                     <li> Cudd_CofMinterm();
3293                     </ul>
3294                 Static procedures included in this module:
3295                     <ul>
3296                     <li> ddCofMintermAux()
3297                     </ul> <P>
3298 <DL>
3299  <DT> <A HREF="cuddAllDet.html#Cudd_CofMinterm" TARGET="MAIN"><CODE>Cudd_CofMinterm()</CODE></A>
3300  <DD> Computes the fraction of minterms in the on-set of all the
3301   positive cofactors of a BDD or ADD.
3302
3303  <DT> <A HREF="cuddAllDet.html#ddCofMintermAux" TARGET="MAIN"><CODE>ddCofMintermAux()</CODE></A>
3304  <DD> Recursive Step for Cudd_CofMinterm function.
3305
3306 </DL>
3307 <HR>
3308 <A NAME="cuddSolve.c"><H1>cuddSolve.c</H1></A>
3309 Boolean equation solver and related functions. <P>
3310 <B>By: Balakrishna Kumthekar</B><P>
3311 External functions included in this modoule:
3312                 <ul>
3313                 <li> Cudd_SolveEqn()
3314                 <li> Cudd_VerifySol()
3315                 </ul>
3316         Internal functions included in this module:
3317                 <ul>
3318                 <li> cuddSolveEqnRecur()
3319                 <li> cuddVerifySol()
3320                 </ul> <P>
3321 <DL>
3322  <DT> <A HREF="cuddAllDet.html#Cudd_SolveEqn" TARGET="MAIN"><CODE>Cudd_SolveEqn()</CODE></A>
3323  <DD> Implements the solution of F(x,y) = 0.
3324
3325  <DT> <A HREF="cuddAllDet.html#Cudd_VerifySol" TARGET="MAIN"><CODE>Cudd_VerifySol()</CODE></A>
3326  <DD> Checks the solution of F(x,y) = 0.
3327
3328  <DT> <A HREF="cuddAllDet.html#cuddSolveEqnRecur" TARGET="MAIN"><CODE>cuddSolveEqnRecur()</CODE></A>
3329  <DD> Implements the recursive step of Cudd_SolveEqn.
3330
3331  <DT> <A HREF="cuddAllDet.html#cuddVerifySol" TARGET="MAIN"><CODE>cuddVerifySol()</CODE></A>
3332  <DD> Implements the recursive step of Cudd_VerifySol.
3333
3334 </DL>
3335 <HR>
3336 <A NAME="cuddSplit.c"><H1>cuddSplit.c</H1></A>
3337 Returns a subset of minterms from a boolean function. <P>
3338 <B>By: Balakrishna Kumthekar</B><P>
3339 External functions included in this modoule:
3340                 <ul>
3341                 <li> Cudd_SplitSet()
3342                 </ul>
3343         Internal functions included in this module:
3344                 <ul>
3345                 <li> cuddSplitSetRecur()
3346                 </u>
3347         Static functions included in this module:
3348                 <ul>
3349                 <li> selectMintermsFromUniverse()
3350                 <li> mintermsFromUniverse()
3351                 <li> bddAnnotateMintermCount()
3352                 </ul> <P>
3353 <DL>
3354  <DT> <A HREF="cuddAllDet.html#Cudd_SplitSet" TARGET="MAIN"><CODE>Cudd_SplitSet()</CODE></A>
3355  <DD> Returns m minterms from a BDD.
3356
3357  <DT> <A HREF="cuddAllDet.html#cuddSplitSetRecur" TARGET="MAIN"><CODE>cuddSplitSetRecur()</CODE></A>
3358  <DD> Implements the recursive step of Cudd_SplitSet.
3359
3360  <DT> <A HREF="cuddAllDet.html#selectMintermsFromUniverse" TARGET="MAIN"><CODE>selectMintermsFromUniverse()</CODE></A>
3361  <DD> This function prepares an array of variables which have not been
3362   encountered so far when traversing the procedure cuddSplitSetRecur.
3363
3364  <DT> <A HREF="cuddAllDet.html#mintermsFromUniverse" TARGET="MAIN"><CODE>mintermsFromUniverse()</CODE></A>
3365  <DD> Recursive procedure to extract n mintems from constant 1.
3366
3367  <DT> <A HREF="cuddAllDet.html#bddAnnotateMintermCount" TARGET="MAIN"><CODE>bddAnnotateMintermCount()</CODE></A>
3368  <DD> Annotates every node in the BDD node with its minterm count.
3369
3370 </DL>
3371 <HR>
3372 <A NAME="cuddSubsetHB.c"><H1>cuddSubsetHB.c</H1></A>
3373 Procedure to subset the given BDD by choosing the heavier
3374                branches. <P>
3375 <B>By: Kavita Ravi</B><P>
3376 External procedures provided by this module:
3377                 <ul>
3378                 <li> Cudd_SubsetHeavyBranch()
3379                 <li> Cudd_SupersetHeavyBranch()
3380                 </ul>
3381                Internal procedures included in this module:
3382                 <ul>
3383                 <li> cuddSubsetHeavyBranch()
3384                 </ul>
3385                Static procedures included in this module:
3386                 <ul>
3387                 <li> ResizeCountMintermPages();
3388                 <li> ResizeNodeDataPages()
3389                 <li> ResizeCountNodePages()
3390                 <li> SubsetCountMintermAux()
3391                 <li> SubsetCountMinterm()
3392                 <li> SubsetCountNodesAux()
3393                 <li> SubsetCountNodes()
3394                 <li> BuildSubsetBdd()
3395                 </ul> <P>
3396 <P><B>See Also</B><A HREF="#cuddSubsetSP.c"><CODE>cuddSubsetSP.c</CODE></A>
3397 <DL>
3398  <DT> <A HREF="cuddAllDet.html#Cudd_SubsetHeavyBranch" TARGET="MAIN"><CODE>Cudd_SubsetHeavyBranch()</CODE></A>
3399  <DD> Extracts a dense subset from a BDD with the heavy branch
3400   heuristic.
3401
3402  <DT> <A HREF="cuddAllDet.html#Cudd_SupersetHeavyBranch" TARGET="MAIN"><CODE>Cudd_SupersetHeavyBranch()</CODE></A>
3403  <DD> Extracts a dense superset from a BDD with the heavy branch
3404   heuristic.
3405
3406  <DT> <A HREF="cuddAllDet.html#cuddSubsetHeavyBranch" TARGET="MAIN"><CODE>cuddSubsetHeavyBranch()</CODE></A>
3407  <DD> The main procedure that returns a subset by choosing the heavier
3408   branch in the BDD.
3409
3410  <DT> <A HREF="cuddAllDet.html#ResizeNodeDataPages" TARGET="MAIN"><CODE>ResizeNodeDataPages()</CODE></A>
3411  <DD> Resize the number of pages allocated to store the node data.
3412
3413  <DT> <A HREF="cuddAllDet.html#ResizeCountMintermPages" TARGET="MAIN"><CODE>ResizeCountMintermPages()</CODE></A>
3414  <DD> Resize the number of pages allocated to store the minterm
3415   counts.
3416
3417  <DT> <A HREF="cuddAllDet.html#ResizeCountNodePages" TARGET="MAIN"><CODE>ResizeCountNodePages()</CODE></A>
3418  <DD> Resize the number of pages allocated to store the node counts.
3419
3420  <DT> <A HREF="cuddAllDet.html#SubsetCountMintermAux" TARGET="MAIN"><CODE>SubsetCountMintermAux()</CODE></A>
3421  <DD> Recursively counts minterms of each node in the DAG.
3422
3423  <DT> <A HREF="cuddAllDet.html#SubsetCountMinterm" TARGET="MAIN"><CODE>SubsetCountMinterm()</CODE></A>
3424  <DD> Counts minterms of each node in the DAG
3425
3426  <DT> <A HREF="cuddAllDet.html#SubsetCountNodesAux" TARGET="MAIN"><CODE>SubsetCountNodesAux()</CODE></A>
3427  <DD> Recursively counts the number of nodes under the dag.
3428   Also counts the number of nodes under the lighter child of
3429   this node.
3430
3431  <DT> <A HREF="cuddAllDet.html#SubsetCountNodes" TARGET="MAIN"><CODE>SubsetCountNodes()</CODE></A>
3432  <DD> Counts the nodes under the current node and its lighter child
3433
3434  <DT> <A HREF="cuddAllDet.html#StoreNodes" TARGET="MAIN"><CODE>StoreNodes()</CODE></A>
3435  <DD> Procedure to recursively store nodes that are retained in the subset.
3436
3437  <DT> <A HREF="cuddAllDet.html#BuildSubsetBdd" TARGET="MAIN"><CODE>BuildSubsetBdd()</CODE></A>
3438  <DD> Builds the subset BDD using the heavy branch method.
3439
3440 </DL>
3441 <HR>
3442 <A NAME="cuddSubsetSP.c"><H1>cuddSubsetSP.c</H1></A>
3443 Procedure to subset the given BDD choosing the shortest paths
3444             (largest cubes) in the BDD. <P>
3445 <B>By: Kavita Ravi</B><P>
3446 External procedures included in this module:
3447                 <ul>
3448                 <li> Cudd_SubsetShortPaths()
3449                 <li> Cudd_SupersetShortPaths()
3450                 </ul>
3451                 Internal procedures included in this module:
3452                 <ul>
3453                 <li> cuddSubsetShortPaths()
3454                 </ul>
3455                 Static procedures included in this module:
3456                 <ul>
3457                 <li> BuildSubsetBdd()
3458                 <li> CreatePathTable()
3459                 <li> AssessPathLength()
3460                 <li> CreateTopDist()
3461                 <li> CreateBotDist()
3462                 <li> ResizeNodeDistPages()
3463                 <li> ResizeQueuePages()
3464                 <li> stPathTableDdFree()
3465                 </ul> <P>
3466 <P><B>See Also</B><A HREF="#cuddSubsetHB.c"><CODE>cuddSubsetHB.c</CODE></A>
3467 <DL>
3468  <DT> <A HREF="cuddAllDet.html#Cudd_SubsetShortPaths" TARGET="MAIN"><CODE>Cudd_SubsetShortPaths()</CODE></A>
3469  <DD> Extracts a dense subset from a BDD with the shortest paths
3470   heuristic.
3471
3472  <DT> <A HREF="cuddAllDet.html#Cudd_SupersetShortPaths" TARGET="MAIN"><CODE>Cudd_SupersetShortPaths()</CODE></A>
3473  <DD> Extracts a dense superset from a BDD with the shortest paths
3474   heuristic.
3475
3476  <DT> <A HREF="cuddAllDet.html#cuddSubsetShortPaths" TARGET="MAIN"><CODE>cuddSubsetShortPaths()</CODE></A>
3477  <DD> The outermost procedure to return a subset of the given BDD
3478   with the shortest path lengths.
3479
3480  <DT> <A HREF="cuddAllDet.html#ResizeNodeDistPages" TARGET="MAIN"><CODE>ResizeNodeDistPages()</CODE></A>
3481  <DD> Resize the number of pages allocated to store the distances
3482   related to each node.
3483
3484  <DT> <A HREF="cuddAllDet.html#ResizeQueuePages" TARGET="MAIN"><CODE>ResizeQueuePages()</CODE></A>
3485  <DD> Resize the number of pages allocated to store nodes in the BFS
3486   traversal of the Bdd  .
3487
3488  <DT> <A HREF="cuddAllDet.html#CreateTopDist" TARGET="MAIN"><CODE>CreateTopDist()</CODE></A>
3489  <DD> Labels each node with its shortest distance from the root
3490
3491  <DT> <A HREF="cuddAllDet.html#CreateBotDist" TARGET="MAIN"><CODE>CreateBotDist()</CODE></A>
3492  <DD> Labels each node with the shortest distance from the constant.
3493
3494  <DT> <A HREF="cuddAllDet.html#CreatePathTable" TARGET="MAIN"><CODE>CreatePathTable()</CODE></A>
3495  <DD> The outer procedure to label each node with its shortest
3496   distance from the root and constant
3497
3498  <DT> <A HREF="cuddAllDet.html#AssessPathLength" TARGET="MAIN"><CODE>AssessPathLength()</CODE></A>
3499  <DD> Chooses the maximum allowable path length of nodes under the
3500   threshold.
3501
3502  <DT> <A HREF="cuddAllDet.html#BuildSubsetBdd" TARGET="MAIN"><CODE>BuildSubsetBdd()</CODE></A>
3503  <DD> Builds the BDD with nodes labeled with path length less than or equal to maxpath
3504
3505  <DT> <A HREF="cuddAllDet.html#stPathTableDdFree" TARGET="MAIN"><CODE>stPathTableDdFree()</CODE></A>
3506  <DD> Procedure to free te result dds stored in the NodeDist pages.
3507
3508 </DL>
3509 <HR>
3510 <A NAME="cuddSymmetry.c"><H1>cuddSymmetry.c</H1></A>
3511 Functions for symmetry-based variable reordering. <P>
3512 <B>By: Shipra Panda, Fabio Somenzi</B><P>
3513 External procedures included in this file:
3514                 <ul>
3515                 <li> Cudd_SymmProfile()
3516                 </ul>
3517         Internal procedures included in this module:
3518                 <ul>
3519                 <li> cuddSymmCheck()
3520                 <li> cuddSymmSifting()
3521                 <li> cuddSymmSiftingConv()
3522                 </ul>
3523         Static procedures included in this module:
3524                 <ul>
3525                 <li> ddSymmUniqueCompare()
3526                 <li> ddSymmSiftingAux()
3527                 <li> ddSymmSiftingConvAux()
3528                 <li> ddSymmSiftingUp()
3529                 <li> ddSymmSiftingDown()
3530                 <li> ddSymmGroupMove()
3531                 <li> ddSymmGroupMoveBackward()
3532                 <li> ddSymmSiftingBackward()
3533                 <li> ddSymmSummary()
3534                 </ul> <P>
3535 <DL>
3536  <DT> <A HREF="cuddAllDet.html#Cudd_SymmProfile" TARGET="MAIN"><CODE>Cudd_SymmProfile()</CODE></A>
3537  <DD> Prints statistics on symmetric variables.
3538
3539  <DT> <A HREF="cuddAllDet.html#cuddSymmCheck" TARGET="MAIN"><CODE>cuddSymmCheck()</CODE></A>
3540  <DD> Checks for symmetry of x and y.
3541
3542  <DT> <A HREF="cuddAllDet.html#cuddSymmSifting" TARGET="MAIN"><CODE>cuddSymmSifting()</CODE></A>
3543  <DD> Symmetric sifting algorithm.
3544
3545  <DT> <A HREF="cuddAllDet.html#cuddSymmSiftingConv" TARGET="MAIN"><CODE>cuddSymmSiftingConv()</CODE></A>
3546  <DD> Symmetric sifting to convergence algorithm.
3547
3548  <DT> <A HREF="cuddAllDet.html#ddSymmUniqueCompare" TARGET="MAIN"><CODE>ddSymmUniqueCompare()</CODE></A>
3549  <DD> Comparison function used by qsort.
3550
3551  <DT> <A HREF="cuddAllDet.html#ddSymmSiftingAux" TARGET="MAIN"><CODE>ddSymmSiftingAux()</CODE></A>
3552  <DD> Given xLow <= x <= xHigh moves x up and down between the
3553   boundaries.
3554
3555  <DT> <A HREF="cuddAllDet.html#ddSymmSiftingConvAux" TARGET="MAIN"><CODE>ddSymmSiftingConvAux()</CODE></A>
3556  <DD> Given xLow <= x <= xHigh moves x up and down between the
3557   boundaries.
3558
3559  <DT> <A HREF="cuddAllDet.html#ddSymmSiftingUp" TARGET="MAIN"><CODE>ddSymmSiftingUp()</CODE></A>
3560  <DD> Moves x up until either it reaches the bound (xLow) or
3561   the size of the DD heap increases too much.
3562
3563  <DT> <A HREF="cuddAllDet.html#ddSymmSiftingDown" TARGET="MAIN"><CODE>ddSymmSiftingDown()</CODE></A>
3564  <DD> Moves x down until either it reaches the bound (xHigh) or
3565   the size of the DD heap increases too much.
3566
3567  <DT> <A HREF="cuddAllDet.html#ddSymmGroupMove" TARGET="MAIN"><CODE>ddSymmGroupMove()</CODE></A>
3568  <DD> Swaps two groups.
3569
3570  <DT> <A HREF="cuddAllDet.html#ddSymmGroupMoveBackward" TARGET="MAIN"><CODE>ddSymmGroupMoveBackward()</CODE></A>
3571  <DD> Undoes the swap of two groups.
3572
3573  <DT> <A HREF="cuddAllDet.html#ddSymmSiftingBackward" TARGET="MAIN"><CODE>ddSymmSiftingBackward()</CODE></A>
3574  <DD> Given a set of moves, returns the DD heap to the position
3575   giving the minimum size.
3576
3577  <DT> <A HREF="cuddAllDet.html#ddSymmSummary" TARGET="MAIN"><CODE>ddSymmSummary()</CODE></A>
3578  <DD> Counts numbers of symmetric variables and symmetry
3579   groups.
3580
3581 </DL>
3582 <HR>
3583 <A NAME="cuddTable.c"><H1>cuddTable.c</H1></A>
3584 Unique table management functions. <P>
3585 <B>By: Fabio Somenzi</B><P>
3586 External procedures included in this module:
3587                 <ul>
3588                 <li> Cudd_Prime()
3589                 </ul>
3590         Internal procedures included in this module:
3591                 <ul>
3592                 <li> cuddAllocNode()
3593                 <li> cuddInitTable()
3594                 <li> cuddFreeTable()
3595                 <li> cuddGarbageCollect()
3596                 <li> cuddZddGetNode()
3597                 <li> cuddZddGetNodeIVO()
3598                 <li> cuddUniqueInter()
3599                 <li> cuddUniqueInterIVO()
3600                 <li> cuddUniqueInterZdd()
3601                 <li> cuddUniqueConst()
3602                 <li> cuddRehash()
3603                 <li> cuddShrinkSubtable()
3604                 <li> cuddInsertSubtables()
3605                 <li> cuddDestroySubtables()
3606                 <li> cuddResizeTableZdd()
3607                 <li> cuddSlowTableGrowth()
3608                 </ul>
3609         Static procedures included in this module:
3610                 <ul>
3611                 <li> ddRehashZdd()
3612                 <li> ddResizeTable()
3613                 <li> cuddFindParent()
3614                 <li> cuddOrderedInsert()
3615                 <li> cuddOrderedThread()
3616                 <li> cuddRotateLeft()
3617                 <li> cuddRotateRight()
3618                 <li> cuddDoRebalance()
3619                 <li> cuddCheckCollisionOrdering()
3620                 </ul> <P>
3621 <DL>
3622  <DT> <A HREF="cuddAllDet.html#Cudd_Prime" TARGET="MAIN"><CODE>Cudd_Prime()</CODE></A>
3623  <DD> Returns the next prime &gt;= p.
3624
3625  <DT> <A HREF="cuddAllDet.html#cuddAllocNode" TARGET="MAIN"><CODE>cuddAllocNode()</CODE></A>
3626  <DD> Fast storage allocation for DdNodes in the table.
3627
3628  <DT> <A HREF="cuddAllDet.html#cuddInitTable" TARGET="MAIN"><CODE>cuddInitTable()</CODE></A>
3629  <DD> Creates and initializes the unique table.
3630
3631  <DT> <A HREF="cuddAllDet.html#cuddFreeTable" TARGET="MAIN"><CODE>cuddFreeTable()</CODE></A>
3632  <DD> Frees the resources associated to a unique table.
3633
3634  <DT> <A HREF="cuddAllDet.html#cuddGarbageCollect" TARGET="MAIN"><CODE>cuddGarbageCollect()</CODE></A>
3635  <DD> Performs garbage collection on the unique tables.
3636
3637  <DT> <A HREF="cuddAllDet.html#cuddZddGetNode" TARGET="MAIN"><CODE>cuddZddGetNode()</CODE></A>
3638  <DD> Wrapper for cuddUniqueInterZdd.
3639
3640  <DT> <A HREF="cuddAllDet.html#cuddZddGetNodeIVO" TARGET="MAIN"><CODE>cuddZddGetNodeIVO()</CODE></A>
3641  <DD> Wrapper for cuddUniqueInterZdd that is independent of variable
3642   ordering.
3643
3644  <DT> <A HREF="cuddAllDet.html#cuddUniqueInter" TARGET="MAIN"><CODE>cuddUniqueInter()</CODE></A>
3645  <DD> Checks the unique table for the existence of an internal node.
3646
3647  <DT> <A HREF="cuddAllDet.html#cuddUniqueInterIVO" TARGET="MAIN"><CODE>cuddUniqueInterIVO()</CODE></A>
3648  <DD> Wrapper for cuddUniqueInter that is independent of variable
3649   ordering.
3650
3651  <DT> <A HREF="cuddAllDet.html#cuddUniqueInterZdd" TARGET="MAIN"><CODE>cuddUniqueInterZdd()</CODE></A>
3652  <DD> Checks the unique table for the existence of an internal
3653   ZDD node.
3654
3655  <DT> <A HREF="cuddAllDet.html#cuddUniqueConst" TARGET="MAIN"><CODE>cuddUniqueConst()</CODE></A>
3656  <DD> Checks the unique table for the existence of a constant node.
3657
3658  <DT> <A HREF="cuddAllDet.html#cuddRehash" TARGET="MAIN"><CODE>cuddRehash()</CODE></A>
3659  <DD> Rehashes a unique subtable.
3660
3661  <DT> <A HREF="cuddAllDet.html#cuddShrinkSubtable" TARGET="MAIN"><CODE>cuddShrinkSubtable()</CODE></A>
3662  <DD> Shrinks a subtable.
3663
3664  <DT> <A HREF="cuddAllDet.html#cuddInsertSubtables" TARGET="MAIN"><CODE>cuddInsertSubtables()</CODE></A>
3665  <DD> Inserts n new subtables in a unique table at level.
3666
3667  <DT> <A HREF="cuddAllDet.html#cuddDestroySubtables" TARGET="MAIN"><CODE>cuddDestroySubtables()</CODE></A>
3668  <DD> Destroys the n most recently created subtables in a unique table.
3669
3670  <DT> <A HREF="cuddAllDet.html#cuddResizeTableZdd" TARGET="MAIN"><CODE>cuddResizeTableZdd()</CODE></A>
3671  <DD> Increases the number of ZDD subtables in a unique table so
3672   that it meets or exceeds index.
3673
3674  <DT> <A HREF="cuddAllDet.html#cuddSlowTableGrowth" TARGET="MAIN"><CODE>cuddSlowTableGrowth()</CODE></A>
3675  <DD> Adjusts parameters of a table to slow down its growth.
3676
3677  <DT> <A HREF="cuddAllDet.html#ddRehashZdd" TARGET="MAIN"><CODE>ddRehashZdd()</CODE></A>
3678  <DD> Rehashes a ZDD unique subtable.
3679
3680  <DT> <A HREF="cuddAllDet.html#ddResizeTable" TARGET="MAIN"><CODE>ddResizeTable()</CODE></A>
3681  <DD> Increases the number of subtables in a unique table so
3682   that it meets or exceeds index.
3683
3684  <DT> <A HREF="cuddAllDet.html#cuddFindParent" TARGET="MAIN"><CODE>cuddFindParent()</CODE></A>
3685  <DD> Searches the subtables above node for a parent.
3686
3687  <DT> <A HREF="cuddAllDet.html#ddFixLimits" TARGET="MAIN"><CODE>ddFixLimits()</CODE></A>
3688  <DD> Adjusts the values of table limits.
3689
3690  <DT> <A HREF="cuddAllDet.html#cuddOrderedInsert" TARGET="MAIN"><CODE>cuddOrderedInsert()</CODE></A>
3691  <DD> Inserts a DdNode in a red/black search tree.
3692
3693  <DT> <A HREF="cuddAllDet.html#cuddOrderedThread" TARGET="MAIN"><CODE>cuddOrderedThread()</CODE></A>
3694  <DD> Threads all the nodes of a search tree into a linear list.
3695
3696  <DT> <A HREF="cuddAllDet.html#cuddRotateLeft" TARGET="MAIN"><CODE>cuddRotateLeft()</CODE></A>
3697  <DD> Performs the left rotation for red/black trees.
3698
3699  <DT> <A HREF="cuddAllDet.html#cuddRotateRight" TARGET="MAIN"><CODE>cuddRotateRight()</CODE></A>
3700  <DD> Performs the right rotation for red/black trees.
3701
3702  <DT> <A HREF="cuddAllDet.html#cuddDoRebalance" TARGET="MAIN"><CODE>cuddDoRebalance()</CODE></A>
3703  <DD> Rebalances a red/black tree.
3704
3705  <DT> <A HREF="cuddAllDet.html#ddPatchTree" TARGET="MAIN"><CODE>ddPatchTree()</CODE></A>
3706  <DD> Fixes a variable tree after the insertion of new subtables.
3707
3708  <DT> <A HREF="cuddAllDet.html#cuddCheckCollisionOrdering" TARGET="MAIN"><CODE>cuddCheckCollisionOrdering()</CODE></A>
3709  <DD> Checks whether a collision list is ordered.
3710
3711  <DT> <A HREF="cuddAllDet.html#ddReportRefMess" TARGET="MAIN"><CODE>ddReportRefMess()</CODE></A>
3712  <DD> Reports problem in garbage collection.
3713
3714 </DL>
3715 <HR>
3716 <A NAME="cuddUtil.c"><H1>cuddUtil.c</H1></A>
3717 Utility functions. <P>
3718 <B>By: Fabio Somenzi</B><P>
3719 External procedures included in this module:
3720                 <ul>
3721                 <li> Cudd_PrintMinterm()
3722                 <li> Cudd_bddPrintCover()
3723                 <li> Cudd_PrintDebug()
3724                 <li> Cudd_DagSize()
3725                 <li> Cudd_EstimateCofactor()
3726                 <li> Cudd_EstimateCofactorSimple()
3727                 <li> Cudd_SharingSize()
3728                 <li> Cudd_CountMinterm()
3729                 <li> Cudd_EpdCountMinterm()
3730                 <li> Cudd_CountPath()
3731                 <li> Cudd_CountPathsToNonZero()
3732                 <li> Cudd_Support()
3733                 <li> Cudd_SupportIndex()
3734                 <li> Cudd_SupportSize()
3735                 <li> Cudd_VectorSupport()
3736                 <li> Cudd_VectorSupportIndex()
3737                 <li> Cudd_VectorSupportSize()
3738                 <li> Cudd_ClassifySupport()
3739                 <li> Cudd_CountLeaves()
3740                 <li> Cudd_bddPickOneCube()
3741                 <li> Cudd_bddPickOneMinterm()
3742                 <li> Cudd_bddPickArbitraryMinterms()
3743                 <li> Cudd_SubsetWithMaskVars()
3744                 <li> Cudd_FirstCube()
3745                 <li> Cudd_NextCube()
3746                 <li> Cudd_bddComputeCube()
3747                 <li> Cudd_addComputeCube()
3748                 <li> Cudd_FirstNode()
3749                 <li> Cudd_NextNode()
3750                 <li> Cudd_GenFree()
3751                 <li> Cudd_IsGenEmpty()
3752                 <li> Cudd_IndicesToCube()
3753                 <li> Cudd_PrintVersion()
3754                 <li> Cudd_AverageDistance()
3755                 <li> Cudd_Random()
3756                 <li> Cudd_Srandom()
3757                 <li> Cudd_Density()
3758                 </ul>
3759         Internal procedures included in this module:
3760                 <ul>
3761                 <li> cuddP()
3762                 <li> cuddStCountfree()
3763                 <li> cuddCollectNodes()
3764                 <li> cuddNodeArray()
3765                 </ul>
3766         Static procedures included in this module:
3767                 <ul>
3768                 <li> dp2()
3769                 <li> ddPrintMintermAux()
3770                 <li> ddDagInt()
3771                 <li> ddCountMintermAux()
3772                 <li> ddEpdCountMintermAux()
3773                 <li> ddCountPathAux()
3774                 <li> ddSupportStep()
3775                 <li> ddClearFlag()
3776                 <li> ddLeavesInt()
3777                 <li> ddPickArbitraryMinterms()
3778                 <li> ddPickRepresentativeCube()
3779                 <li> ddEpdFree()
3780                 </ul> <P>
3781 <DL>
3782  <DT> <A HREF="cuddAllDet.html#Cudd_PrintMinterm" TARGET="MAIN"><CODE>Cudd_PrintMinterm()</CODE></A>
3783  <DD> Prints a disjoint sum of products.
3784
3785  <DT> <A HREF="cuddAllDet.html#Cudd_bddPrintCover" TARGET="MAIN"><CODE>Cudd_bddPrintCover()</CODE></A>
3786  <DD> Prints a sum of prime implicants of a BDD.
3787
3788  <DT> <A HREF="cuddAllDet.html#Cudd_PrintDebug" TARGET="MAIN"><CODE>Cudd_PrintDebug()</CODE></A>
3789  <DD> Prints to the standard output a DD and its statistics.
3790
3791  <DT> <A HREF="cuddAllDet.html#Cudd_DagSize" TARGET="MAIN"><CODE>Cudd_DagSize()</CODE></A>
3792  <DD> Counts the number of nodes in a DD.
3793
3794  <DT> <A HREF="cuddAllDet.html#Cudd_EstimateCofactor" TARGET="MAIN"><CODE>Cudd_EstimateCofactor()</CODE></A>
3795  <DD> Estimates the number of nodes in a cofactor of a DD.
3796
3797  <DT> <A HREF="cuddAllDet.html#Cudd_EstimateCofactorSimple" TARGET="MAIN"><CODE>Cudd_EstimateCofactorSimple()</CODE></A>
3798  <DD> Estimates the number of nodes in a cofactor of a DD.
3799
3800  <DT> <A HREF="cuddAllDet.html#Cudd_SharingSize" TARGET="MAIN"><CODE>Cudd_SharingSize()</CODE></A>
3801  <DD> Counts the number of nodes in an array of DDs.
3802
3803  <DT> <A HREF="cuddAllDet.html#Cudd_CountMinterm" TARGET="MAIN"><CODE>Cudd_CountMinterm()</CODE></A>
3804  <DD> Counts the number of minterms of a DD.
3805
3806  <DT> <A HREF="cuddAllDet.html#Cudd_CountPath" TARGET="MAIN"><CODE>Cudd_CountPath()</CODE></A>
3807  <DD> Counts the number of paths of a DD.
3808
3809  <DT> <A HREF="cuddAllDet.html#Cudd_EpdCountMinterm" TARGET="MAIN"><CODE>Cudd_EpdCountMinterm()</CODE></A>
3810  <DD> Counts the number of minterms of a DD with extended precision.
3811
3812  <DT> <A HREF="cuddAllDet.html#Cudd_CountPathsToNonZero" TARGET="MAIN"><CODE>Cudd_CountPathsToNonZero()</CODE></A>
3813  <DD> Counts the number of paths to a non-zero terminal of a DD.
3814
3815  <DT> <A HREF="cuddAllDet.html#Cudd_Support" TARGET="MAIN"><CODE>Cudd_Support()</CODE></A>
3816  <DD> Finds the variables on which a DD depends.
3817
3818  <DT> <A HREF="cuddAllDet.html#Cudd_SupportIndex" TARGET="MAIN"><CODE>Cudd_SupportIndex()</CODE></A>
3819  <DD> Finds the variables on which a DD depends.
3820
3821  <DT> <A HREF="cuddAllDet.html#Cudd_SupportSize" TARGET="MAIN"><CODE>Cudd_SupportSize()</CODE></A>
3822  <DD> Counts the variables on which a DD depends.
3823
3824  <DT> <A HREF="cuddAllDet.html#Cudd_VectorSupport" TARGET="MAIN"><CODE>Cudd_VectorSupport()</CODE></A>
3825  <DD> Finds the variables on which a set of DDs depends.
3826
3827  <DT> <A HREF="cuddAllDet.html#Cudd_VectorSupportIndex" TARGET="MAIN"><CODE>Cudd_VectorSupportIndex()</CODE></A>
3828  <DD> Finds the variables on which a set of DDs depends.
3829
3830  <DT> <A HREF="cuddAllDet.html#Cudd_VectorSupportSize" TARGET="MAIN"><CODE>Cudd_VectorSupportSize()</CODE></A>
3831  <DD> Counts the variables on which a set of DDs depends.
3832
3833  <DT> <A HREF="cuddAllDet.html#Cudd_ClassifySupport" TARGET="MAIN"><CODE>Cudd_ClassifySupport()</CODE></A>
3834  <DD> Classifies the variables in the support of two DDs.
3835
3836  <DT> <A HREF="cuddAllDet.html#Cudd_CountLeaves" TARGET="MAIN"><CODE>Cudd_CountLeaves()</CODE></A>
3837  <DD> Counts the number of leaves in a DD.
3838
3839  <DT> <A HREF="cuddAllDet.html#Cudd_bddPickOneCube" TARGET="MAIN"><CODE>Cudd_bddPickOneCube()</CODE></A>
3840  <DD> Picks one on-set cube randomly from the given DD.
3841
3842  <DT> <A HREF="cuddAllDet.html#Cudd_bddPickOneMinterm" TARGET="MAIN"><CODE>Cudd_bddPickOneMinterm()</CODE></A>
3843  <DD> Picks one on-set minterm randomly from the given DD.
3844
3845  <DT> <A HREF="cuddAllDet.html#Cudd_bddPickArbitraryMinterms" TARGET="MAIN"><CODE>Cudd_bddPickArbitraryMinterms()</CODE></A>
3846  <DD> Picks k on-set minterms evenly distributed from given DD.
3847
3848  <DT> <A HREF="cuddAllDet.html#Cudd_SubsetWithMaskVars" TARGET="MAIN"><CODE>Cudd_SubsetWithMaskVars()</CODE></A>
3849  <DD> Extracts a subset from a BDD.
3850
3851  <DT> <A HREF="cuddAllDet.html#Cudd_FirstCube" TARGET="MAIN"><CODE>Cudd_FirstCube()</CODE></A>
3852  <DD> Finds the first cube of a decision diagram.
3853
3854  <DT> <A HREF="cuddAllDet.html#Cudd_NextCube" TARGET="MAIN"><CODE>Cudd_NextCube()</CODE></A>
3855  <DD> Generates the next cube of a decision diagram onset.
3856
3857  <DT> <A HREF="cuddAllDet.html#Cudd_FirstPrime" TARGET="MAIN"><CODE>Cudd_FirstPrime()</CODE></A>
3858  <DD> Finds the first prime of a Boolean function.
3859
3860  <DT> <A HREF="cuddAllDet.html#Cudd_NextPrime" TARGET="MAIN"><CODE>Cudd_NextPrime()</CODE></A>
3861  <DD> Generates the next prime of a Boolean function.
3862
3863  <DT> <A HREF="cuddAllDet.html#Cudd_bddComputeCube" TARGET="MAIN"><CODE>Cudd_bddComputeCube()</CODE></A>
3864  <DD> Computes the cube of an array of BDD variables.
3865
3866  <DT> <A HREF="cuddAllDet.html#Cudd_addComputeCube" TARGET="MAIN"><CODE>Cudd_addComputeCube()</CODE></A>
3867  <DD> Computes the cube of an array of ADD variables.
3868
3869  <DT> <A HREF="cuddAllDet.html#Cudd_CubeArrayToBdd" TARGET="MAIN"><CODE>Cudd_CubeArrayToBdd()</CODE></A>
3870  <DD> Builds the BDD of a cube from a positional array.
3871
3872  <DT> <A HREF="cuddAllDet.html#Cudd_BddToCubeArray" TARGET="MAIN"><CODE>Cudd_BddToCubeArray()</CODE></A>
3873  <DD> Builds a positional array from the BDD of a cube.
3874
3875  <DT> <A HREF="cuddAllDet.html#Cudd_FirstNode" TARGET="MAIN"><CODE>Cudd_FirstNode()</CODE></A>
3876  <DD> Finds the first node of a decision diagram.
3877
3878  <DT> <A HREF="cuddAllDet.html#Cudd_NextNode" TARGET="MAIN"><CODE>Cudd_NextNode()</CODE></A>
3879  <DD> Finds the next node of a decision diagram.
3880
3881  <DT> <A HREF="cuddAllDet.html#Cudd_GenFree" TARGET="MAIN"><CODE>Cudd_GenFree()</CODE></A>
3882  <DD> Frees a CUDD generator.
3883
3884  <DT> <A HREF="cuddAllDet.html#Cudd_IsGenEmpty" TARGET="MAIN"><CODE>Cudd_IsGenEmpty()</CODE></A>
3885  <DD> Queries the status of a generator.
3886
3887  <DT> <A HREF="cuddAllDet.html#Cudd_IndicesToCube" TARGET="MAIN"><CODE>Cudd_IndicesToCube()</CODE></A>
3888  <DD> Builds a cube of BDD variables from an array of indices.
3889
3890  <DT> <A HREF="cuddAllDet.html#Cudd_PrintVersion" TARGET="MAIN"><CODE>Cudd_PrintVersion()</CODE></A>
3891  <DD> Prints the package version number.
3892
3893  <DT> <A HREF="cuddAllDet.html#Cudd_AverageDistance" TARGET="MAIN"><CODE>Cudd_AverageDistance()</CODE></A>
3894  <DD> Computes the average distance between adjacent nodes.
3895
3896  <DT> <A HREF="cuddAllDet.html#Cudd_Random" TARGET="MAIN"><CODE>Cudd_Random()</CODE></A>
3897  <DD> Portable random number generator.
3898
3899  <DT> <A HREF="cuddAllDet.html#Cudd_Srandom" TARGET="MAIN"><CODE>Cudd_Srandom()</CODE></A>
3900  <DD> Initializer for the portable random number generator.
3901
3902  <DT> <A HREF="cuddAllDet.html#Cudd_Density" TARGET="MAIN"><CODE>Cudd_Density()</CODE></A>
3903  <DD> Computes the density of a BDD or ADD.
3904
3905  <DT> <A HREF="cuddAllDet.html#Cudd_OutOfMem" TARGET="MAIN"><CODE>Cudd_OutOfMem()</CODE></A>
3906  <DD> Warns that a memory allocation failed.
3907
3908  <DT> <A HREF="cuddAllDet.html#cuddP" TARGET="MAIN"><CODE>cuddP()</CODE></A>
3909  <DD> Prints a DD to the standard output. One line per node is
3910   printed.
3911
3912  <DT> <A HREF="cuddAllDet.html#cuddStCountfree" TARGET="MAIN"><CODE>cuddStCountfree()</CODE></A>
3913  <DD> Frees the memory used to store the minterm counts recorded
3914   in the visited table.
3915
3916  <DT> <A HREF="cuddAllDet.html#cuddCollectNodes" TARGET="MAIN"><CODE>cuddCollectNodes()</CODE></A>
3917  <DD> Recursively collects all the nodes of a DD in a symbol
3918   table.
3919
3920  <DT> <A HREF="cuddAllDet.html#cuddNodeArray" TARGET="MAIN"><CODE>cuddNodeArray()</CODE></A>
3921  <DD> Recursively collects all the nodes of a DD in an array.
3922
3923  <DT> <A HREF="cuddAllDet.html#dp2" TARGET="MAIN"><CODE>dp2()</CODE></A>
3924  <DD> Performs the recursive step of cuddP.
3925
3926  <DT> <A HREF="cuddAllDet.html#ddPrintMintermAux" TARGET="MAIN"><CODE>ddPrintMintermAux()</CODE></A>
3927  <DD> Performs the recursive step of Cudd_PrintMinterm.
3928
3929  <DT> <A HREF="cuddAllDet.html#ddDagInt" TARGET="MAIN"><CODE>ddDagInt()</CODE></A>
3930  <DD> Performs the recursive step of Cudd_DagSize.
3931
3932  <DT> <A HREF="cuddAllDet.html#cuddNodeArrayRecur" TARGET="MAIN"><CODE>cuddNodeArrayRecur()</CODE></A>
3933  <DD> Performs the recursive step of cuddNodeArray.
3934
3935  <DT> <A HREF="cuddAllDet.html#cuddEstimateCofactor" TARGET="MAIN"><CODE>cuddEstimateCofactor()</CODE></A>
3936  <DD> Performs the recursive step of Cudd_CofactorEstimate.
3937
3938  <DT> <A HREF="cuddAllDet.html#cuddUniqueLookup" TARGET="MAIN"><CODE>cuddUniqueLookup()</CODE></A>
3939  <DD> Checks the unique table for the existence of an internal node.
3940
3941  <DT> <A HREF="cuddAllDet.html#cuddEstimateCofactorSimple" TARGET="MAIN"><CODE>cuddEstimateCofactorSimple()</CODE></A>
3942  <DD> Performs the recursive step of Cudd_CofactorEstimateSimple.
3943
3944  <DT> <A HREF="cuddAllDet.html#ddCountMintermAux" TARGET="MAIN"><CODE>ddCountMintermAux()</CODE></A>
3945  <DD> Performs the recursive step of Cudd_CountMinterm.
3946
3947  <DT> <A HREF="cuddAllDet.html#ddCountPathAux" TARGET="MAIN"><CODE>ddCountPathAux()</CODE></A>
3948  <DD> Performs the recursive step of Cudd_CountPath.
3949
3950  <DT> <A HREF="cuddAllDet.html#ddEpdCountMintermAux" TARGET="MAIN"><CODE>ddEpdCountMintermAux()</CODE></A>
3951  <DD> Performs the recursive step of Cudd_EpdCountMinterm.
3952
3953  <DT> <A HREF="cuddAllDet.html#ddCountPathsToNonZero" TARGET="MAIN"><CODE>ddCountPathsToNonZero()</CODE></A>
3954  <DD> Performs the recursive step of Cudd_CountPathsToNonZero.
3955
3956  <DT> <A HREF="cuddAllDet.html#ddSupportStep" TARGET="MAIN"><CODE>ddSupportStep()</CODE></A>
3957  <DD> Performs the recursive step of Cudd_Support.
3958
3959  <DT> <A HREF="cuddAllDet.html#ddClearFlag" TARGET="MAIN"><CODE>ddClearFlag()</CODE></A>
3960  <DD> Performs a DFS from f, clearing the LSB of the next
3961   pointers.
3962
3963  <DT> <A HREF="cuddAllDet.html#ddLeavesInt" TARGET="MAIN"><CODE>ddLeavesInt()</CODE></A>
3964  <DD> Performs the recursive step of Cudd_CountLeaves.
3965
3966  <DT> <A HREF="cuddAllDet.html#ddPickArbitraryMinterms" TARGET="MAIN"><CODE>ddPickArbitraryMinterms()</CODE></A>
3967  <DD> Performs the recursive step of Cudd_bddPickArbitraryMinterms.
3968
3969  <DT> <A HREF="cuddAllDet.html#ddPickRepresentativeCube" TARGET="MAIN"><CODE>ddPickRepresentativeCube()</CODE></A>
3970  <DD> Finds a representative cube of a BDD.
3971
3972  <DT> <A HREF="cuddAllDet.html#ddEpdFree" TARGET="MAIN"><CODE>ddEpdFree()</CODE></A>
3973  <DD> Frees the memory used to store the minterm counts recorded
3974   in the visited table.
3975
3976 </DL>
3977 <HR>
3978 <A NAME="cuddWindow.c"><H1>cuddWindow.c</H1></A>
3979 Functions for variable reordering by window permutation. <P>
3980 <B>By: Fabio Somenzi</B><P>
3981 Internal procedures included in this module:
3982                 <ul>
3983                 <li> cuddWindowReorder()
3984                 </ul>
3985         Static procedures included in this module:
3986                 <ul>
3987                 <li> ddWindow2()
3988                 <li> ddWindowConv2()
3989                 <li> ddPermuteWindow3()
3990                 <li> ddWindow3()
3991                 <li> ddWindowConv3()
3992                 <li> ddPermuteWindow4()
3993                 <li> ddWindow4()
3994                 <li> ddWindowConv4()
3995                 </ul> <P>
3996 <DL>
3997  <DT> <A HREF="cuddAllDet.html#cuddWindowReorder" TARGET="MAIN"><CODE>cuddWindowReorder()</CODE></A>
3998  <DD> Reorders by applying the method of the sliding window.
3999
4000  <DT> <A HREF="cuddAllDet.html#ddWindow2" TARGET="MAIN"><CODE>ddWindow2()</CODE></A>
4001  <DD> Reorders by applying a sliding window of width 2.
4002
4003  <DT> <A HREF="cuddAllDet.html#ddWindowConv2" TARGET="MAIN"><CODE>ddWindowConv2()</CODE></A>
4004  <DD> Reorders by repeatedly applying a sliding window of width 2.
4005
4006  <DT> <A HREF="cuddAllDet.html#ddPermuteWindow3" TARGET="MAIN"><CODE>ddPermuteWindow3()</CODE></A>
4007  <DD> Tries all the permutations of the three variables between
4008   x and x+2 and retains the best.
4009
4010  <DT> <A HREF="cuddAllDet.html#ddWindow3" TARGET="MAIN"><CODE>ddWindow3()</CODE></A>
4011  <DD> Reorders by applying a sliding window of width 3.
4012
4013  <DT> <A HREF="cuddAllDet.html#ddWindowConv3" TARGET="MAIN"><CODE>ddWindowConv3()</CODE></A>
4014  <DD> Reorders by repeatedly applying a sliding window of width 3.
4015
4016  <DT> <A HREF="cuddAllDet.html#ddPermuteWindow4" TARGET="MAIN"><CODE>ddPermuteWindow4()</CODE></A>
4017  <DD> Tries all the permutations of the four variables between w
4018   and w+3 and retains the best.
4019
4020  <DT> <A HREF="cuddAllDet.html#ddWindow4" TARGET="MAIN"><CODE>ddWindow4()</CODE></A>
4021  <DD> Reorders by applying a sliding window of width 4.
4022
4023  <DT> <A HREF="cuddAllDet.html#ddWindowConv4" TARGET="MAIN"><CODE>ddWindowConv4()</CODE></A>
4024  <DD> Reorders by repeatedly applying a sliding window of width 4.
4025
4026 </DL>
4027 <HR>
4028 <A NAME="cuddZddCount.c"><H1>cuddZddCount.c</H1></A>
4029 Procedures to count the number of minterms of a ZDD. <P>
4030 <B>By: Hyong-Kyoon Shin, In-Ho Moon</B><P>
4031 External procedures included in this module:
4032                     <ul>
4033                     <li> Cudd_zddCount();
4034                     <li> Cudd_zddCountDouble();
4035                     </ul>
4036                Internal procedures included in this module:
4037                     <ul>
4038                     </ul>
4039                Static procedures included in this module:
4040                     <ul>
4041                     <li> cuddZddCountStep();
4042                     <li> cuddZddCountDoubleStep();
4043                     <li> st_zdd_count_dbl_free()
4044                     <li> st_zdd_countfree()
4045                     </ul> <P>
4046 <DL>
4047  <DT> <A HREF="cuddAllDet.html#Cudd_zddCount" TARGET="MAIN"><CODE>Cudd_zddCount()</CODE></A>
4048  <DD> Counts the number of minterms in a ZDD.
4049
4050  <DT> <A HREF="cuddAllDet.html#Cudd_zddCountDouble" TARGET="MAIN"><CODE>Cudd_zddCountDouble()</CODE></A>
4051  <DD> Counts the number of minterms of a ZDD.
4052
4053  <DT> <A HREF="cuddAllDet.html#cuddZddCountStep" TARGET="MAIN"><CODE>cuddZddCountStep()</CODE></A>
4054  <DD> Performs the recursive step of Cudd_zddCount.
4055
4056  <DT> <A HREF="cuddAllDet.html#cuddZddCountDoubleStep" TARGET="MAIN"><CODE>cuddZddCountDoubleStep()</CODE></A>
4057  <DD> Performs the recursive step of Cudd_zddCountDouble.
4058
4059  <DT> <A HREF="cuddAllDet.html#st_zdd_countfree" TARGET="MAIN"><CODE>st_zdd_countfree()</CODE></A>
4060  <DD> Frees the memory associated with the computed table of
4061   Cudd_zddCount.
4062
4063  <DT> <A HREF="cuddAllDet.html#st_zdd_count_dbl_free" TARGET="MAIN"><CODE>st_zdd_count_dbl_free()</CODE></A>
4064  <DD> Frees the memory associated with the computed table of
4065   Cudd_zddCountDouble.
4066
4067 </DL>
4068 <HR>
4069 <A NAME="cuddZddFuncs.c"><H1>cuddZddFuncs.c</H1></A>
4070 Functions to manipulate covers represented as ZDDs. <P>
4071 <B>By: In-Ho Moon</B><P>
4072 External procedures included in this module:
4073                     <ul>
4074                     <li> Cudd_zddProduct();
4075                     <li> Cudd_zddUnateProduct();
4076                     <li> Cudd_zddWeakDiv();
4077                     <li> Cudd_zddWeakDivF();
4078                     <li> Cudd_zddDivide();
4079                     <li> Cudd_zddDivideF();
4080                     <li> Cudd_zddComplement();
4081                     </ul>
4082                Internal procedures included in this module:
4083                     <ul>
4084                     <li> cuddZddProduct();
4085                     <li> cuddZddUnateProduct();
4086                     <li> cuddZddWeakDiv();
4087                     <li> cuddZddWeakDivF();
4088                     <li> cuddZddDivide();
4089                     <li> cuddZddDivideF();
4090                     <li> cuddZddGetCofactors3()
4091                     <li> cuddZddGetCofactors2()
4092                     <li> cuddZddComplement();
4093                     <li> cuddZddGetPosVarIndex();
4094                     <li> cuddZddGetNegVarIndex();
4095                     <li> cuddZddGetPosVarLevel();
4096                     <li> cuddZddGetNegVarLevel();
4097                     </ul>
4098                Static procedures included in this module:
4099                     <ul>
4100                     </ul> <P>
4101 <DL>
4102  <DT> <A HREF="cuddAllDet.html#Cudd_zddProduct" TARGET="MAIN"><CODE>Cudd_zddProduct()</CODE></A>
4103  <DD> Computes the product of two covers represented by ZDDs.
4104
4105  <DT> <A HREF="cuddAllDet.html#Cudd_zddUnateProduct" TARGET="MAIN"><CODE>Cudd_zddUnateProduct()</CODE></A>
4106  <DD> Computes the product of two unate covers.
4107
4108  <DT> <A HREF="cuddAllDet.html#Cudd_zddWeakDiv" TARGET="MAIN"><CODE>Cudd_zddWeakDiv()</CODE></A>
4109  <DD> Applies weak division to two covers.
4110
4111  <DT> <A HREF="cuddAllDet.html#Cudd_zddDivide" TARGET="MAIN"><CODE>Cudd_zddDivide()</CODE></A>
4112  <DD> Computes the quotient of two unate covers.
4113
4114  <DT> <A HREF="cuddAllDet.html#Cudd_zddWeakDivF" TARGET="MAIN"><CODE>Cudd_zddWeakDivF()</CODE></A>
4115  <DD> Modified version of Cudd_zddWeakDiv.
4116
4117  <DT> <A HREF="cuddAllDet.html#Cudd_zddDivideF" TARGET="MAIN"><CODE>Cudd_zddDivideF()</CODE></A>
4118  <DD> Modified version of Cudd_zddDivide.
4119
4120  <DT> <A HREF="cuddAllDet.html#Cudd_zddComplement" TARGET="MAIN"><CODE>Cudd_zddComplement()</CODE></A>
4121  <DD> Computes a complement cover for a ZDD node.
4122
4123  <DT> <A HREF="cuddAllDet.html#cuddZddProduct" TARGET="MAIN"><CODE>cuddZddProduct()</CODE></A>
4124  <DD> Performs the recursive step of Cudd_zddProduct.
4125
4126  <DT> <A HREF="cuddAllDet.html#cuddZddUnateProduct" TARGET="MAIN"><CODE>cuddZddUnateProduct()</CODE></A>
4127  <DD> Performs the recursive step of Cudd_zddUnateProduct.
4128
4129  <DT> <A HREF="cuddAllDet.html#cuddZddWeakDiv" TARGET="MAIN"><CODE>cuddZddWeakDiv()</CODE></A>
4130  <DD> Performs the recursive step of Cudd_zddWeakDiv.
4131
4132  <DT> <A HREF="cuddAllDet.html#cuddZddWeakDivF" TARGET="MAIN"><CODE>cuddZddWeakDivF()</CODE></A>
4133  <DD> Performs the recursive step of Cudd_zddWeakDivF.
4134
4135  <DT> <A HREF="cuddAllDet.html#cuddZddDivide" TARGET="MAIN"><CODE>cuddZddDivide()</CODE></A>
4136  <DD> Performs the recursive step of Cudd_zddDivide.
4137
4138  <DT> <A HREF="cuddAllDet.html#cuddZddDivideF" TARGET="MAIN"><CODE>cuddZddDivideF()</CODE></A>
4139  <DD> Performs the recursive step of Cudd_zddDivideF.
4140
4141  <DT> <A HREF="cuddAllDet.html#cuddZddGetCofactors3" TARGET="MAIN"><CODE>cuddZddGetCofactors3()</CODE></A>
4142  <DD> Computes the three-way decomposition of f w.r.t. v.
4143
4144  <DT> <A HREF="cuddAllDet.html#cuddZddGetCofactors2" TARGET="MAIN"><CODE>cuddZddGetCofactors2()</CODE></A>
4145  <DD> Computes the two-way decomposition of f w.r.t. v.
4146
4147  <DT> <A HREF="cuddAllDet.html#cuddZddComplement" TARGET="MAIN"><CODE>cuddZddComplement()</CODE></A>
4148  <DD> Computes a complement of a ZDD node.
4149
4150  <DT> <A HREF="cuddAllDet.html#cuddZddGetPosVarIndex" TARGET="MAIN"><CODE>cuddZddGetPosVarIndex()</CODE></A>
4151  <DD> Returns the index of positive ZDD variable.
4152
4153  <DT> <A HREF="cuddAllDet.html#cuddZddGetNegVarIndex" TARGET="MAIN"><CODE>cuddZddGetNegVarIndex()</CODE></A>
4154  <DD> Returns the index of negative ZDD variable.
4155
4156  <DT> <A HREF="cuddAllDet.html#cuddZddGetPosVarLevel" TARGET="MAIN"><CODE>cuddZddGetPosVarLevel()</CODE></A>
4157  <DD> Returns the level of positive ZDD variable.
4158
4159  <DT> <A HREF="cuddAllDet.html#cuddZddGetNegVarLevel" TARGET="MAIN"><CODE>cuddZddGetNegVarLevel()</CODE></A>
4160  <DD> Returns the level of negative ZDD variable.
4161
4162 </DL>
4163 <HR>
4164 <A NAME="cuddZddGroup.c"><H1>cuddZddGroup.c</H1></A>
4165 Functions for ZDD group sifting. <P>
4166 <B>By: Fabio Somenzi</B><P>
4167 External procedures included in this file:
4168                 <ul>
4169                 <li> Cudd_MakeZddTreeNode()
4170                 </ul>
4171         Internal procedures included in this file:
4172                 <ul>
4173                 <li> cuddZddTreeSifting()
4174                 </ul>
4175         Static procedures included in this module:
4176                 <ul>
4177                 <li> zddTreeSiftingAux()
4178                 <li> zddCountInternalMtrNodes()
4179                 <li> zddReorderChildren()
4180                 <li> zddFindNodeHiLo()
4181                 <li> zddUniqueCompareGroup()
4182                 <li> zddGroupSifting()
4183                 <li> zddGroupSiftingAux()
4184                 <li> zddGroupSiftingUp()
4185                 <li> zddGroupSiftingDown()
4186                 <li> zddGroupMove()
4187                 <li> zddGroupMoveBackward()
4188                 <li> zddGroupSiftingBackward()
4189                 <li> zddMergeGroups()
4190                 </ul> <P>
4191 <DL>
4192  <DT> <A HREF="cuddAllDet.html#Cudd_MakeZddTreeNode" TARGET="MAIN"><CODE>Cudd_MakeZddTreeNode()</CODE></A>
4193  <DD> Creates a new ZDD variable group.
4194
4195  <DT> <A HREF="cuddAllDet.html#cuddZddTreeSifting" TARGET="MAIN"><CODE>cuddZddTreeSifting()</CODE></A>
4196  <DD> Tree sifting algorithm for ZDDs.
4197
4198  <DT> <A HREF="cuddAllDet.html#zddTreeSiftingAux" TARGET="MAIN"><CODE>zddTreeSiftingAux()</CODE></A>
4199  <DD> Visits the group tree and reorders each group.
4200
4201  <DT> <A HREF="cuddAllDet.html#zddCountInternalMtrNodes" TARGET="MAIN"><CODE>zddCountInternalMtrNodes()</CODE></A>
4202  <DD> Counts the number of internal nodes of the group tree.
4203
4204  <DT> <A HREF="cuddAllDet.html#zddReorderChildren" TARGET="MAIN"><CODE>zddReorderChildren()</CODE></A>
4205  <DD> Reorders the children of a group tree node according to
4206   the options.
4207
4208  <DT> <A HREF="cuddAllDet.html#zddFindNodeHiLo" TARGET="MAIN"><CODE>zddFindNodeHiLo()</CODE></A>
4209  <DD> Finds the lower and upper bounds of the group represented
4210   by treenode.
4211
4212  <DT> <A HREF="cuddAllDet.html#zddUniqueCompareGroup" TARGET="MAIN"><CODE>zddUniqueCompareGroup()</CODE></A>
4213  <DD> Comparison function used by qsort.
4214
4215  <DT> <A HREF="cuddAllDet.html#zddGroupSifting" TARGET="MAIN"><CODE>zddGroupSifting()</CODE></A>
4216  <DD> Sifts from treenode->low to treenode->high.
4217
4218  <DT> <A HREF="cuddAllDet.html#zddGroupSiftingAux" TARGET="MAIN"><CODE>zddGroupSiftingAux()</CODE></A>
4219  <DD> Sifts one variable up and down until it has taken all
4220   positions. Checks for aggregation.
4221
4222  <DT> <A HREF="cuddAllDet.html#zddGroupSiftingUp" TARGET="MAIN"><CODE>zddGroupSiftingUp()</CODE></A>
4223  <DD> Sifts up a variable until either it reaches position xLow
4224   or the size of the DD heap increases too much.
4225
4226  <DT> <A HREF="cuddAllDet.html#zddGroupSiftingDown" TARGET="MAIN"><CODE>zddGroupSiftingDown()</CODE></A>
4227  <DD> Sifts down a variable until it reaches position xHigh.
4228
4229  <DT> <A HREF="cuddAllDet.html#zddGroupMove" TARGET="MAIN"><CODE>zddGroupMove()</CODE></A>
4230  <DD> Swaps two groups and records the move.
4231
4232  <DT> <A HREF="cuddAllDet.html#zddGroupMoveBackward" TARGET="MAIN"><CODE>zddGroupMoveBackward()</CODE></A>
4233  <DD> Undoes the swap two groups.
4234
4235  <DT> <A HREF="cuddAllDet.html#zddGroupSiftingBackward" TARGET="MAIN"><CODE>zddGroupSiftingBackward()</CODE></A>
4236  <DD> Determines the best position for a variables and returns
4237   it there.
4238
4239  <DT> <A HREF="cuddAllDet.html#zddMergeGroups" TARGET="MAIN"><CODE>zddMergeGroups()</CODE></A>
4240  <DD> Merges groups in the DD table.
4241
4242 </DL>
4243 <HR>
4244 <A NAME="cuddZddIsop.c"><H1>cuddZddIsop.c</H1></A>
4245 Functions to find irredundant SOP covers as ZDDs from BDDs. <P>
4246 <B>By: In-Ho Moon</B><P>
4247 External procedures included in this module:
4248                     <ul>
4249                     <li> Cudd_bddIsop()
4250                     <li> Cudd_zddIsop()
4251                     <li> Cudd_MakeBddFromZddCover()
4252                     </ul>
4253                Internal procedures included in this module:
4254                     <ul>
4255                     <li> cuddBddIsop()
4256                     <li> cuddZddIsop()
4257                     <li> cuddMakeBddFromZddCover()
4258                     </ul>
4259                Static procedures included in this module:
4260                     <ul>
4261                     </ul> <P>
4262 <DL>
4263  <DT> <A HREF="cuddAllDet.html#Cudd_zddIsop" TARGET="MAIN"><CODE>Cudd_zddIsop()</CODE></A>
4264  <DD> Computes an ISOP in ZDD form from BDDs.
4265
4266  <DT> <A HREF="cuddAllDet.html#Cudd_bddIsop" TARGET="MAIN"><CODE>Cudd_bddIsop()</CODE></A>
4267  <DD> Computes a BDD in the interval between L and U with a
4268   simple sum-of-produuct cover.
4269
4270  <DT> <A HREF="cuddAllDet.html#Cudd_MakeBddFromZddCover" TARGET="MAIN"><CODE>Cudd_MakeBddFromZddCover()</CODE></A>
4271  <DD> Converts a ZDD cover to a BDD graph.
4272
4273  <DT> <A HREF="cuddAllDet.html#cuddZddIsop" TARGET="MAIN"><CODE>cuddZddIsop()</CODE></A>
4274  <DD> Performs the recursive step of Cudd_zddIsop.
4275
4276  <DT> <A HREF="cuddAllDet.html#cuddBddIsop" TARGET="MAIN"><CODE>cuddBddIsop()</CODE></A>
4277  <DD> Performs the recursive step of Cudd_bddIsop.
4278
4279  <DT> <A HREF="cuddAllDet.html#cuddMakeBddFromZddCover" TARGET="MAIN"><CODE>cuddMakeBddFromZddCover()</CODE></A>
4280  <DD> Converts a ZDD cover to a BDD graph.
4281
4282 </DL>
4283 <HR>
4284 <A NAME="cuddZddLin.c"><H1>cuddZddLin.c</H1></A>
4285 Procedures for dynamic variable ordering of ZDDs. <P>
4286 <B>By: Fabio Somenzi</B><P>
4287 Internal procedures included in this module:
4288                     <ul>
4289                     <li> cuddZddLinearSifting()
4290                     </ul>
4291                Static procedures included in this module:
4292                     <ul>
4293                     <li> cuddZddLinearInPlace()
4294                     <li> cuddZddLinerAux()
4295                     <li> cuddZddLinearUp()
4296                     <li> cuddZddLinearDown()
4297                     <li> cuddZddLinearBackward()
4298                     <li> cuddZddUndoMoves()
4299                     </ul> <P>
4300 <P><B>See Also</B><A HREF="#cuddLinear.c"><CODE>cuddLinear.c</CODE></A>
4301 <A HREF="#cuddZddReord.c"><CODE>cuddZddReord.c</CODE></A>
4302 <DL>
4303  <DT> <A HREF="cuddAllDet.html#cuddZddLinearSifting" TARGET="MAIN"><CODE>cuddZddLinearSifting()</CODE></A>
4304  <DD> Implementation of the linear sifting algorithm for ZDDs.
4305
4306  <DT> <A HREF="cuddAllDet.html#cuddZddLinearInPlace" TARGET="MAIN"><CODE>cuddZddLinearInPlace()</CODE></A>
4307  <DD> Linearly combines two adjacent variables.
4308
4309  <DT> <A HREF="cuddAllDet.html#cuddZddLinearAux" TARGET="MAIN"><CODE>cuddZddLinearAux()</CODE></A>
4310  <DD> Given xLow <= x <= xHigh moves x up and down between the
4311   boundaries.
4312
4313  <DT> <A HREF="cuddAllDet.html#cuddZddLinearUp" TARGET="MAIN"><CODE>cuddZddLinearUp()</CODE></A>
4314  <DD> Sifts a variable up applying the XOR transformation.
4315
4316  <DT> <A HREF="cuddAllDet.html#cuddZddLinearDown" TARGET="MAIN"><CODE>cuddZddLinearDown()</CODE></A>
4317  <DD> Sifts a variable down and applies the XOR transformation.
4318
4319  <DT> <A HREF="cuddAllDet.html#cuddZddLinearBackward" TARGET="MAIN"><CODE>cuddZddLinearBackward()</CODE></A>
4320  <DD> Given a set of moves, returns the ZDD heap to the position
4321   giving the minimum size.
4322
4323  <DT> <A HREF="cuddAllDet.html#cuddZddUndoMoves" TARGET="MAIN"><CODE>cuddZddUndoMoves()</CODE></A>
4324  <DD> Given a set of moves, returns the ZDD heap to the order
4325   in effect before the moves.
4326
4327 </DL>
4328 <HR>
4329 <A NAME="cuddZddMisc.c"><H1>cuddZddMisc.c</H1></A>
4330 Miscellaneous utility functions for ZDDs. <P>
4331 <B>By: Hyong-Kyoon Shin, In-Ho Moon</B><P>
4332 External procedures included in this module:
4333                     <ul>
4334                     <li> Cudd_zddDagSize()
4335                     <li> Cudd_zddCountMinterm()
4336                     <li> Cudd_zddPrintSubtable()
4337                     </ul>
4338                Internal procedures included in this module:
4339                     <ul>
4340                     </ul>
4341                Static procedures included in this module:
4342                     <ul>
4343                     <li> cuddZddDagInt()
4344                     </ul> <P>
4345 <DL>
4346  <DT> <A HREF="cuddAllDet.html#Cudd_zddDagSize" TARGET="MAIN"><CODE>Cudd_zddDagSize()</CODE></A>
4347  <DD> Counts the number of nodes in a ZDD.
4348
4349  <DT> <A HREF="cuddAllDet.html#Cudd_zddCountMinterm" TARGET="MAIN"><CODE>Cudd_zddCountMinterm()</CODE></A>
4350  <DD> Counts the number of minterms of a ZDD.
4351
4352  <DT> <A HREF="cuddAllDet.html#Cudd_zddPrintSubtable" TARGET="MAIN"><CODE>Cudd_zddPrintSubtable()</CODE></A>
4353  <DD> Prints the ZDD table.
4354
4355  <DT> <A HREF="cuddAllDet.html#cuddZddDagInt" TARGET="MAIN"><CODE>cuddZddDagInt()</CODE></A>
4356  <DD> Performs the recursive step of Cudd_zddDagSize.
4357
4358 </DL>
4359 <HR>
4360 <A NAME="cuddZddPort.c"><H1>cuddZddPort.c</H1></A>
4361 Functions that translate BDDs to ZDDs. <P>
4362 <B>By: Hyong-kyoon Shin, In-Ho Moon</B><P>
4363 External procedures included in this module:
4364                     <ul>
4365                     <li> Cudd_zddPortFromBdd()
4366                     <li> Cudd_zddPortToBdd()
4367                     </ul>
4368                Internal procedures included in this module:
4369                     <ul>
4370                     </ul>
4371                Static procedures included in this module:
4372                     <ul>
4373                     <li> zddPortFromBddStep()
4374                     <li> zddPortToBddStep()
4375                     </ul> <P>
4376 <DL>
4377  <DT> <A HREF="cuddAllDet.html#Cudd_zddPortFromBdd" TARGET="MAIN"><CODE>Cudd_zddPortFromBdd()</CODE></A>
4378  <DD> Converts a BDD into a ZDD.
4379
4380  <DT> <A HREF="cuddAllDet.html#Cudd_zddPortToBdd" TARGET="MAIN"><CODE>Cudd_zddPortToBdd()</CODE></A>
4381  <DD> Converts a ZDD into a BDD.
4382
4383  <DT> <A HREF="cuddAllDet.html#zddPortFromBddStep" TARGET="MAIN"><CODE>zddPortFromBddStep()</CODE></A>
4384  <DD> Performs the recursive step of Cudd_zddPortFromBdd.
4385
4386  <DT> <A HREF="cuddAllDet.html#zddPortToBddStep" TARGET="MAIN"><CODE>zddPortToBddStep()</CODE></A>
4387  <DD> Performs the recursive step of Cudd_zddPortToBdd.
4388
4389 </DL>
4390 <HR>
4391 <A NAME="cuddZddReord.c"><H1>cuddZddReord.c</H1></A>
4392 Procedures for dynamic variable ordering of ZDDs. <P>
4393 <B>By: Hyong-Kyoon Shin, In-Ho Moon</B><P>
4394 External procedures included in this module:
4395                     <ul>
4396                     <li> Cudd_zddReduceHeap()
4397                     <li> Cudd_zddShuffleHeap()
4398                     </ul>
4399                Internal procedures included in this module:
4400                     <ul>
4401                     <li> cuddZddAlignToBdd()
4402                     <li> cuddZddNextHigh()
4403                     <li> cuddZddNextLow()
4404                     <li> cuddZddUniqueCompare()
4405                     <li> cuddZddSwapInPlace()
4406                     <li> cuddZddSwapping()
4407                     <li> cuddZddSifting()
4408                     </ul>
4409                Static procedures included in this module:
4410                     <ul>
4411                     <li> zddSwapAny()
4412                     <li> cuddZddSiftingAux()
4413                     <li> cuddZddSiftingUp()
4414                     <li> cuddZddSiftingDown()
4415                     <li> cuddZddSiftingBackward()
4416                     <li> zddReorderPreprocess()
4417                     <li> zddReorderPostprocess()
4418                     <li> zddShuffle()
4419                     <li> zddSiftUp()
4420                     </ul> <P>
4421 <DL>
4422  <DT> <A HREF="cuddAllDet.html#Cudd_zddReduceHeap" TARGET="MAIN"><CODE>Cudd_zddReduceHeap()</CODE></A>
4423  <DD> Main dynamic reordering routine for ZDDs.
4424
4425  <DT> <A HREF="cuddAllDet.html#Cudd_zddShuffleHeap" TARGET="MAIN"><CODE>Cudd_zddShuffleHeap()</CODE></A>
4426  <DD> Reorders ZDD variables according to given permutation.
4427
4428  <DT> <A HREF="cuddAllDet.html#cuddZddAlignToBdd" TARGET="MAIN"><CODE>cuddZddAlignToBdd()</CODE></A>
4429  <DD> Reorders ZDD variables according to the order of the BDD
4430   variables.
4431
4432  <DT> <A HREF="cuddAllDet.html#cuddZddNextHigh" TARGET="MAIN"><CODE>cuddZddNextHigh()</CODE></A>
4433  <DD> Finds the next subtable with a larger index.
4434
4435  <DT> <A HREF="cuddAllDet.html#cuddZddNextLow" TARGET="MAIN"><CODE>cuddZddNextLow()</CODE></A>
4436  <DD> Finds the next subtable with a smaller index.
4437
4438  <DT> <A HREF="cuddAllDet.html#cuddZddUniqueCompare" TARGET="MAIN"><CODE>cuddZddUniqueCompare()</CODE></A>
4439  <DD> Comparison function used by qsort.
4440
4441  <DT> <A HREF="cuddAllDet.html#cuddZddSwapInPlace" TARGET="MAIN"><CODE>cuddZddSwapInPlace()</CODE></A>
4442  <DD> Swaps two adjacent variables.
4443
4444  <DT> <A HREF="cuddAllDet.html#cuddZddSwapping" TARGET="MAIN"><CODE>cuddZddSwapping()</CODE></A>
4445  <DD> Reorders variables by a sequence of (non-adjacent) swaps.
4446
4447  <DT> <A HREF="cuddAllDet.html#cuddZddSifting" TARGET="MAIN"><CODE>cuddZddSifting()</CODE></A>
4448  <DD> Implementation of Rudell's sifting algorithm.
4449
4450  <DT> <A HREF="cuddAllDet.html#zddSwapAny" TARGET="MAIN"><CODE>zddSwapAny()</CODE></A>
4451  <DD> Swaps any two variables.
4452
4453  <DT> <A HREF="cuddAllDet.html#cuddZddSiftingAux" TARGET="MAIN"><CODE>cuddZddSiftingAux()</CODE></A>
4454  <DD> Given xLow <= x <= xHigh moves x up and down between the
4455   boundaries.
4456
4457  <DT> <A HREF="cuddAllDet.html#cuddZddSiftingUp" TARGET="MAIN"><CODE>cuddZddSiftingUp()</CODE></A>
4458  <DD> Sifts a variable up.
4459
4460  <DT> <A HREF="cuddAllDet.html#cuddZddSiftingDown" TARGET="MAIN"><CODE>cuddZddSiftingDown()</CODE></A>
4461  <DD> Sifts a variable down.
4462
4463  <DT> <A HREF="cuddAllDet.html#cuddZddSiftingBackward" TARGET="MAIN"><CODE>cuddZddSiftingBackward()</CODE></A>
4464  <DD> Given a set of moves, returns the ZDD heap to the position
4465   giving the minimum size.
4466
4467  <DT> <A HREF="cuddAllDet.html#zddReorderPreprocess" TARGET="MAIN"><CODE>zddReorderPreprocess()</CODE></A>
4468  <DD> Prepares the ZDD heap for dynamic reordering.
4469
4470  <DT> <A HREF="cuddAllDet.html#zddReorderPostprocess" TARGET="MAIN"><CODE>zddReorderPostprocess()</CODE></A>
4471  <DD> Shrinks almost empty ZDD subtables at the end of reordering
4472   to guarantee that they have a reasonable load factor.
4473
4474  <DT> <A HREF="cuddAllDet.html#zddShuffle" TARGET="MAIN"><CODE>zddShuffle()</CODE></A>
4475  <DD> Reorders ZDD variables according to a given permutation.
4476
4477  <DT> <A HREF="cuddAllDet.html#zddSiftUp" TARGET="MAIN"><CODE>zddSiftUp()</CODE></A>
4478  <DD> Moves one ZDD variable up.
4479
4480  <DT> <A HREF="cuddAllDet.html#zddFixTree" TARGET="MAIN"><CODE>zddFixTree()</CODE></A>
4481  <DD> Fixes the ZDD variable group tree after a shuffle.
4482
4483 </DL>
4484 <HR>
4485 <A NAME="cuddZddSetop.c"><H1>cuddZddSetop.c</H1></A>
4486 Set operations on ZDDs. <P>
4487 <B>By: Hyong-Kyoon Shin, In-Ho Moon</B><P>
4488 External procedures included in this module:
4489                     <ul>
4490                     <li> Cudd_zddIte()
4491                     <li> Cudd_zddUnion()
4492                     <li> Cudd_zddIntersect()
4493                     <li> Cudd_zddDiff()
4494                     <li> Cudd_zddDiffConst()
4495                     <li> Cudd_zddSubset1()
4496                     <li> Cudd_zddSubset0()
4497                     <li> Cudd_zddChange()
4498                     </ul>
4499                Internal procedures included in this module:
4500                     <ul>
4501                     <li> cuddZddIte()
4502                     <li> cuddZddUnion()
4503                     <li> cuddZddIntersect()
4504                     <li> cuddZddDiff()
4505                     <li> cuddZddChangeAux()
4506                     <li> cuddZddSubset1()
4507                     <li> cuddZddSubset0()
4508                     </ul>
4509                Static procedures included in this module:
4510                     <ul>
4511                     <li> zdd_subset1_aux()
4512                     <li> zdd_subset0_aux()
4513                     <li> zddVarToConst()
4514                     </ul> <P>
4515 <DL>
4516  <DT> <A HREF="cuddAllDet.html#Cudd_zddIte" TARGET="MAIN"><CODE>Cudd_zddIte()</CODE></A>
4517  <DD> Computes the ITE of three ZDDs.
4518
4519  <DT> <A HREF="cuddAllDet.html#Cudd_zddUnion" TARGET="MAIN"><CODE>Cudd_zddUnion()</CODE></A>
4520  <DD> Computes the union of two ZDDs.
4521
4522  <DT> <A HREF="cuddAllDet.html#Cudd_zddIntersect" TARGET="MAIN"><CODE>Cudd_zddIntersect()</CODE></A>
4523  <DD> Computes the intersection of two ZDDs.
4524
4525  <DT> <A HREF="cuddAllDet.html#Cudd_zddDiff" TARGET="MAIN"><CODE>Cudd_zddDiff()</CODE></A>
4526  <DD> Computes the difference of two ZDDs.
4527
4528  <DT> <A HREF="cuddAllDet.html#Cudd_zddDiffConst" TARGET="MAIN"><CODE>Cudd_zddDiffConst()</CODE></A>
4529  <DD> Performs the inclusion test for ZDDs (P implies Q).
4530
4531  <DT> <A HREF="cuddAllDet.html#Cudd_zddSubset1" TARGET="MAIN"><CODE>Cudd_zddSubset1()</CODE></A>
4532  <DD> Computes the positive cofactor of a ZDD w.r.t. a variable.
4533
4534  <DT> <A HREF="cuddAllDet.html#Cudd_zddSubset0" TARGET="MAIN"><CODE>Cudd_zddSubset0()</CODE></A>
4535  <DD> Computes the negative cofactor of a ZDD w.r.t. a variable.
4536
4537  <DT> <A HREF="cuddAllDet.html#Cudd_zddChange" TARGET="MAIN"><CODE>Cudd_zddChange()</CODE></A>
4538  <DD> Substitutes a variable with its complement in a ZDD.
4539
4540  <DT> <A HREF="cuddAllDet.html#cuddZddIte" TARGET="MAIN"><CODE>cuddZddIte()</CODE></A>
4541  <DD> Performs the recursive step of Cudd_zddIte.
4542
4543  <DT> <A HREF="cuddAllDet.html#cuddZddUnion" TARGET="MAIN"><CODE>cuddZddUnion()</CODE></A>
4544  <DD> Performs the recursive step of Cudd_zddUnion.
4545
4546  <DT> <A HREF="cuddAllDet.html#cuddZddIntersect" TARGET="MAIN"><CODE>cuddZddIntersect()</CODE></A>
4547  <DD> Performs the recursive step of Cudd_zddIntersect.
4548
4549  <DT> <A HREF="cuddAllDet.html#cuddZddDiff" TARGET="MAIN"><CODE>cuddZddDiff()</CODE></A>
4550  <DD> Performs the recursive step of Cudd_zddDiff.
4551
4552  <DT> <A HREF="cuddAllDet.html#cuddZddChangeAux" TARGET="MAIN"><CODE>cuddZddChangeAux()</CODE></A>
4553  <DD> Performs the recursive step of Cudd_zddChange.
4554
4555  <DT> <A HREF="cuddAllDet.html#cuddZddSubset1" TARGET="MAIN"><CODE>cuddZddSubset1()</CODE></A>
4556  <DD> Computes the positive cofactor of a ZDD w.r.t. a variable.
4557
4558  <DT> <A HREF="cuddAllDet.html#cuddZddSubset0" TARGET="MAIN"><CODE>cuddZddSubset0()</CODE></A>
4559  <DD> Computes the negative cofactor of a ZDD w.r.t. a variable.
4560
4561  <DT> <A HREF="cuddAllDet.html#cuddZddChange" TARGET="MAIN"><CODE>cuddZddChange()</CODE></A>
4562  <DD> Substitutes a variable with its complement in a ZDD.
4563
4564  <DT> <A HREF="cuddAllDet.html#zdd_subset1_aux" TARGET="MAIN"><CODE>zdd_subset1_aux()</CODE></A>
4565  <DD> Performs the recursive step of Cudd_zddSubset1.
4566
4567  <DT> <A HREF="cuddAllDet.html#zdd_subset0_aux" TARGET="MAIN"><CODE>zdd_subset0_aux()</CODE></A>
4568  <DD> Performs the recursive step of Cudd_zddSubset0.
4569
4570  <DT> <A HREF="cuddAllDet.html#zddVarToConst" TARGET="MAIN"><CODE>zddVarToConst()</CODE></A>
4571  <DD> Replaces variables with constants if possible (part of
4572   canonical form).
4573
4574 </DL>
4575 <HR>
4576 <A NAME="cuddZddSymm.c"><H1>cuddZddSymm.c</H1></A>
4577 Functions for symmetry-based ZDD variable reordering. <P>
4578 <B>By: Hyong-Kyoon Shin, In-Ho Moon</B><P>
4579 External procedures included in this module:
4580                     <ul>
4581                     <li> Cudd_zddSymmProfile()
4582                     </ul>
4583                Internal procedures included in this module:
4584                     <ul>
4585                     <li> cuddZddSymmCheck()
4586                     <li> cuddZddSymmSifting()
4587                     <li> cuddZddSymmSiftingConv()
4588                     </ul>
4589                Static procedures included in this module:
4590                     <ul>
4591                     <li> cuddZddUniqueCompare()
4592                     <li> cuddZddSymmSiftingAux()
4593                     <li> cuddZddSymmSiftingConvAux()
4594                     <li> cuddZddSymmSifting_up()
4595                     <li> cuddZddSymmSifting_down()
4596                     <li> zdd_group_move()
4597                     <li> cuddZddSymmSiftingBackward()
4598                     <li> zdd_group_move_backward()
4599                     </ul> <P>
4600 <P><B>See Also</B><A HREF="#cuddSymmetry.c"><CODE>cuddSymmetry.c</CODE></A>
4601 <DL>
4602  <DT> <A HREF="cuddAllDet.html#Cudd_zddSymmProfile" TARGET="MAIN"><CODE>Cudd_zddSymmProfile()</CODE></A>
4603  <DD> Prints statistics on symmetric ZDD variables.
4604
4605  <DT> <A HREF="cuddAllDet.html#cuddZddSymmCheck" TARGET="MAIN"><CODE>cuddZddSymmCheck()</CODE></A>
4606  <DD> Checks for symmetry of x and y.
4607
4608  <DT> <A HREF="cuddAllDet.html#cuddZddSymmSifting" TARGET="MAIN"><CODE>cuddZddSymmSifting()</CODE></A>
4609  <DD> Symmetric sifting algorithm for ZDDs.
4610
4611  <DT> <A HREF="cuddAllDet.html#cuddZddSymmSiftingConv" TARGET="MAIN"><CODE>cuddZddSymmSiftingConv()</CODE></A>
4612  <DD> Symmetric sifting to convergence algorithm for ZDDs.
4613
4614  <DT> <A HREF="cuddAllDet.html#cuddZddSymmSiftingAux" TARGET="MAIN"><CODE>cuddZddSymmSiftingAux()</CODE></A>
4615  <DD> Given x_low <= x <= x_high moves x up and down between the
4616   boundaries.
4617
4618  <DT> <A HREF="cuddAllDet.html#cuddZddSymmSiftingConvAux" TARGET="MAIN"><CODE>cuddZddSymmSiftingConvAux()</CODE></A>
4619  <DD> Given x_low <= x <= x_high moves x up and down between the
4620   boundaries.
4621
4622  <DT> <A HREF="cuddAllDet.html#cuddZddSymmSifting_up" TARGET="MAIN"><CODE>cuddZddSymmSifting_up()</CODE></A>
4623  <DD> Moves x up until either it reaches the bound (x_low) or
4624   the size of the ZDD heap increases too much.
4625
4626  <DT> <A HREF="cuddAllDet.html#cuddZddSymmSifting_down" TARGET="MAIN"><CODE>cuddZddSymmSifting_down()</CODE></A>
4627  <DD> Moves x down until either it reaches the bound (x_high) or
4628   the size of the ZDD heap increases too much.
4629
4630  <DT> <A HREF="cuddAllDet.html#cuddZddSymmSiftingBackward" TARGET="MAIN"><CODE>cuddZddSymmSiftingBackward()</CODE></A>
4631  <DD> Given a set of moves, returns the ZDD heap to the position
4632   giving the minimum size.
4633
4634  <DT> <A HREF="cuddAllDet.html#zdd_group_move" TARGET="MAIN"><CODE>zdd_group_move()</CODE></A>
4635  <DD> Swaps two groups.
4636
4637  <DT> <A HREF="cuddAllDet.html#zdd_group_move_backward" TARGET="MAIN"><CODE>zdd_group_move_backward()</CODE></A>
4638  <DD> Undoes the swap of two groups.
4639
4640  <DT> <A HREF="cuddAllDet.html#cuddZddSymmSummary" TARGET="MAIN"><CODE>cuddZddSymmSummary()</CODE></A>
4641  <DD> Counts numbers of symmetric variables and symmetry
4642   groups.
4643
4644 </DL>
4645 <HR>
4646 <A NAME="cuddZddUtil.c"><H1>cuddZddUtil.c</H1></A>
4647 Utility functions for ZDDs. <P>
4648 <B>By: Hyong-Kyoon Shin, In-Ho Moon, Fabio Somenzi</B><P>
4649 External procedures included in this module:
4650                     <ul>
4651                     <li> Cudd_zddPrintMinterm()
4652                     <li> Cudd_zddPrintCover()
4653                     <li> Cudd_zddPrintDebug()
4654                     <li> Cudd_zddFirstPath()
4655                     <li> Cudd_zddNextPath()
4656                     <li> Cudd_zddCoverPathToString()
4657                     <li> Cudd_zddDumpDot()
4658                     </ul>
4659                Internal procedures included in this module:
4660                     <ul>
4661                     <li> cuddZddP()
4662                     </ul>
4663                Static procedures included in this module:
4664                     <ul>
4665                     <li> zp2()
4666                     <li> zdd_print_minterm_aux()
4667                     <li> zddPrintCoverAux()
4668                     </ul> <P>
4669 <DL>
4670  <DT> <A HREF="cuddAllDet.html#Cudd_zddPrintMinterm" TARGET="MAIN"><CODE>Cudd_zddPrintMinterm()</CODE></A>
4671  <DD> Prints a disjoint sum of product form for a ZDD.
4672
4673  <DT> <A HREF="cuddAllDet.html#Cudd_zddPrintCover" TARGET="MAIN"><CODE>Cudd_zddPrintCover()</CODE></A>
4674  <DD> Prints a sum of products from a ZDD representing a cover.
4675
4676  <DT> <A HREF="cuddAllDet.html#Cudd_zddPrintDebug" TARGET="MAIN"><CODE>Cudd_zddPrintDebug()</CODE></A>
4677  <DD> Prints to the standard output a ZDD and its statistics.
4678
4679  <DT> <A HREF="cuddAllDet.html#Cudd_zddFirstPath" TARGET="MAIN"><CODE>Cudd_zddFirstPath()</CODE></A>
4680  <DD> Finds the first path of a ZDD.
4681
4682  <DT> <A HREF="cuddAllDet.html#Cudd_zddNextPath" TARGET="MAIN"><CODE>Cudd_zddNextPath()</CODE></A>
4683  <DD> Generates the next path of a ZDD.
4684
4685  <DT> <A HREF="cuddAllDet.html#Cudd_zddCoverPathToString" TARGET="MAIN"><CODE>Cudd_zddCoverPathToString()</CODE></A>
4686  <DD> Converts a path of a ZDD representing a cover to a string.
4687
4688  <DT> <A HREF="cuddAllDet.html#Cudd_zddDumpDot" TARGET="MAIN"><CODE>Cudd_zddDumpDot()</CODE></A>
4689  <DD> Writes a dot file representing the argument ZDDs.
4690
4691  <DT> <A HREF="cuddAllDet.html#cuddZddP" TARGET="MAIN"><CODE>cuddZddP()</CODE></A>
4692  <DD> Prints a ZDD to the standard output. One line per node is
4693   printed.
4694
4695  <DT> <A HREF="cuddAllDet.html#zp2" TARGET="MAIN"><CODE>zp2()</CODE></A>
4696  <DD> Performs the recursive step of cuddZddP.
4697
4698  <DT> <A HREF="cuddAllDet.html#zdd_print_minterm_aux" TARGET="MAIN"><CODE>zdd_print_minterm_aux()</CODE></A>
4699  <DD> Performs the recursive step of Cudd_zddPrintMinterm.
4700
4701  <DT> <A HREF="cuddAllDet.html#zddPrintCoverAux" TARGET="MAIN"><CODE>zddPrintCoverAux()</CODE></A>
4702  <DD> Performs the recursive step of Cudd_zddPrintCover.
4703
4704 </DL>
4705 <HR>
4706 Last updated on 20090220 23h06
4707 </BODY></HTML>