distr/cudd/doc/cuddExtAbs.html

   1 <html>
   2 <head><title>cudd package abstract</title></head>
   3 <body>
   4
   5
   6 <!-- Function Abstracts -->
   7
   8 <dl>
   9 <dt> <a href="cuddAllDet.html#Cudd_AddHook" TARGET="MAIN"><code>Cudd_AddHook()</code></a>
  10 <dd> Adds a function to a hook.
  11
  12 <dt> <a href="cuddAllDet.html#Cudd_ApaAdd" TARGET="MAIN"><code>Cudd_ApaAdd()</code></a>
  13 <dd> Adds two arbitrary precision integers.
  14
  15 <dt> <a href="cuddAllDet.html#Cudd_ApaCompareRatios" TARGET="MAIN"><code>Cudd_ApaCompareRatios()</code></a>
  16 <dd> Compares the ratios of two arbitrary precision integers to two
  17   unsigned ints.
  18
  19 <dt> <a href="cuddAllDet.html#Cudd_ApaCompare" TARGET="MAIN"><code>Cudd_ApaCompare()</code></a>
  20 <dd> Compares two arbitrary precision integers.
  21
  22 <dt> <a href="cuddAllDet.html#Cudd_ApaCopy" TARGET="MAIN"><code>Cudd_ApaCopy()</code></a>
  23 <dd> Makes a copy of an arbitrary precision integer.
  24
  25 <dt> <a href="cuddAllDet.html#Cudd_ApaCountMinterm" TARGET="MAIN"><code>Cudd_ApaCountMinterm()</code></a>
  26 <dd> Counts the number of minterms of a DD.
  27
  28 <dt> <a href="cuddAllDet.html#Cudd_ApaIntDivision" TARGET="MAIN"><code>Cudd_ApaIntDivision()</code></a>
  29 <dd> Divides an arbitrary precision integer by an integer.
  30
  31 <dt> <a href="cuddAllDet.html#Cudd_ApaNumberOfDigits" TARGET="MAIN"><code>Cudd_ApaNumberOfDigits()</code></a>
  32 <dd> Finds the number of digits for an arbitrary precision
  33   integer.
  34
  35 <dt> <a href="cuddAllDet.html#Cudd_ApaPowerOfTwo" TARGET="MAIN"><code>Cudd_ApaPowerOfTwo()</code></a>
  36 <dd> Sets an arbitrary precision integer to a power of two.
  37
  38 <dt> <a href="cuddAllDet.html#Cudd_ApaPrintDecimal" TARGET="MAIN"><code>Cudd_ApaPrintDecimal()</code></a>
  39 <dd> Prints an arbitrary precision integer in decimal format.
  40
  41 <dt> <a href="cuddAllDet.html#Cudd_ApaPrintDensity" TARGET="MAIN"><code>Cudd_ApaPrintDensity()</code></a>
  42 <dd> Prints the density of a BDD or ADD using
  43   arbitrary precision arithmetic.
  44
  45 <dt> <a href="cuddAllDet.html#Cudd_ApaPrintExponential" TARGET="MAIN"><code>Cudd_ApaPrintExponential()</code></a>
  46 <dd> Prints an arbitrary precision integer in exponential format.
  47
  48 <dt> <a href="cuddAllDet.html#Cudd_ApaPrintHex" TARGET="MAIN"><code>Cudd_ApaPrintHex()</code></a>
  49 <dd> Prints an arbitrary precision integer in hexadecimal format.
  50
  51 <dt> <a href="cuddAllDet.html#Cudd_ApaPrintMintermExp" TARGET="MAIN"><code>Cudd_ApaPrintMintermExp()</code></a>
  52 <dd> Prints the number of minterms of a BDD or ADD in exponential
  53   format using arbitrary precision arithmetic.
  54
  55 <dt> <a href="cuddAllDet.html#Cudd_ApaPrintMinterm" TARGET="MAIN"><code>Cudd_ApaPrintMinterm()</code></a>
  56 <dd> Prints the number of minterms of a BDD or ADD using
  57   arbitrary precision arithmetic.
  58
  59 <dt> <a href="cuddAllDet.html#Cudd_ApaSetToLiteral" TARGET="MAIN"><code>Cudd_ApaSetToLiteral()</code></a>
  60 <dd> Sets an arbitrary precision integer to a one-digit literal.
  61
  62 <dt> <a href="cuddAllDet.html#Cudd_ApaShiftRight" TARGET="MAIN"><code>Cudd_ApaShiftRight()</code></a>
  63 <dd> Shifts right an arbitrary precision integer by one binary
  64   place.
  65
  66 <dt> <a href="cuddAllDet.html#Cudd_ApaShortDivision" TARGET="MAIN"><code>Cudd_ApaShortDivision()</code></a>
  67 <dd> Divides an arbitrary precision integer by a digit.
  68
  69 <dt> <a href="cuddAllDet.html#Cudd_ApaSubtract" TARGET="MAIN"><code>Cudd_ApaSubtract()</code></a>
  70 <dd> Subtracts two arbitrary precision integers.
  71
  72 <dt> <a href="cuddAllDet.html#Cudd_AutodynDisableZdd" TARGET="MAIN"><code>Cudd_AutodynDisableZdd()</code></a>
  73 <dd> Disables automatic dynamic reordering of ZDDs.
  74
  75 <dt> <a href="cuddAllDet.html#Cudd_AutodynDisable" TARGET="MAIN"><code>Cudd_AutodynDisable()</code></a>
  76 <dd> Disables automatic dynamic reordering.
  77
  78 <dt> <a href="cuddAllDet.html#Cudd_AutodynEnableZdd" TARGET="MAIN"><code>Cudd_AutodynEnableZdd()</code></a>
  79 <dd> Enables automatic dynamic reordering of ZDDs.
  80
  81 <dt> <a href="cuddAllDet.html#Cudd_AutodynEnable" TARGET="MAIN"><code>Cudd_AutodynEnable()</code></a>
  82 <dd> Enables automatic dynamic reordering of BDDs and ADDs.
  83
  84 <dt> <a href="cuddAllDet.html#Cudd_AverageDistance" TARGET="MAIN"><code>Cudd_AverageDistance()</code></a>
  85 <dd> Computes the average distance between adjacent nodes.
  86
  87 <dt> <a href="cuddAllDet.html#Cudd_BddToAdd" TARGET="MAIN"><code>Cudd_BddToAdd()</code></a>
  88 <dd> Converts a BDD to a 0-1 ADD.
  89
  90 <dt> <a href="cuddAllDet.html#Cudd_BddToCubeArray" TARGET="MAIN"><code>Cudd_BddToCubeArray()</code></a>
  91 <dd> Builds a positional array from the BDD of a cube.
  92
  93 <dt> <a href="cuddAllDet.html#Cudd_BiasedOverApprox" TARGET="MAIN"><code>Cudd_BiasedOverApprox()</code></a>
  94 <dd> Extracts a dense superset from a BDD with the biased
  95   underapproximation method.
  96
  97 <dt> <a href="cuddAllDet.html#Cudd_BiasedUnderApprox" TARGET="MAIN"><code>Cudd_BiasedUnderApprox()</code></a>
  98 <dd> Extracts a dense subset from a BDD with the biased
  99   underapproximation method.
 100
 101 <dt> <a href="cuddAllDet.html#Cudd_CProjection" TARGET="MAIN"><code>Cudd_CProjection()</code></a>
 102 <dd> Computes the compatible projection of R w.r.t. cube Y.
 103
 104 <dt> <a href="cuddAllDet.html#Cudd_CheckKeys" TARGET="MAIN"><code>Cudd_CheckKeys()</code></a>
 105 <dd> Checks for several conditions that should not occur.
 106
 107 <dt> <a href="cuddAllDet.html#Cudd_CheckZeroRef" TARGET="MAIN"><code>Cudd_CheckZeroRef()</code></a>
 108 <dd> Checks the unique table for nodes with non-zero reference
 109   counts.
 110
 111 <dt> <a href="cuddAllDet.html#Cudd_ClassifySupport" TARGET="MAIN"><code>Cudd_ClassifySupport()</code></a>
 112 <dd> Classifies the variables in the support of two DDs.
 113
 114 <dt> <a href="cuddAllDet.html#Cudd_ClearErrorCode" TARGET="MAIN"><code>Cudd_ClearErrorCode()</code></a>
 115 <dd> Clear the error code of a manager.
 116
 117 <dt> <a href="cuddAllDet.html#Cudd_CofMinterm" TARGET="MAIN"><code>Cudd_CofMinterm()</code></a>
 118 <dd> Computes the fraction of minterms in the on-set of all the
 119   positive cofactors of a BDD or ADD.
 120
 121 <dt> <a href="cuddAllDet.html#Cudd_Cofactor" TARGET="MAIN"><code>Cudd_Cofactor()</code></a>
 122 <dd> Computes the cofactor of f with respect to g.
 123
 124 <dt> <a href="cuddAllDet.html#Cudd_CountLeaves" TARGET="MAIN"><code>Cudd_CountLeaves()</code></a>
 125 <dd> Counts the number of leaves in a DD.
 126
 127 <dt> <a href="cuddAllDet.html#Cudd_CountMinterm" TARGET="MAIN"><code>Cudd_CountMinterm()</code></a>
 128 <dd> Counts the number of minterms of a DD.
 129
 130 <dt> <a href="cuddAllDet.html#Cudd_CountPathsToNonZero" TARGET="MAIN"><code>Cudd_CountPathsToNonZero()</code></a>
 131 <dd> Counts the number of paths to a non-zero terminal of a DD.
 132
 133 <dt> <a href="cuddAllDet.html#Cudd_CountPath" TARGET="MAIN"><code>Cudd_CountPath()</code></a>
 134 <dd> Counts the number of paths of a DD.
 135
 136 <dt> <a href="cuddAllDet.html#Cudd_CubeArrayToBdd" TARGET="MAIN"><code>Cudd_CubeArrayToBdd()</code></a>
 137 <dd> Builds the BDD of a cube from a positional array.
 138
 139 <dt> <a href="cuddAllDet.html#Cudd_DagSize" TARGET="MAIN"><code>Cudd_DagSize()</code></a>
 140 <dd> Counts the number of nodes in a DD.
 141
 142 <dt> <a href="cuddAllDet.html#Cudd_DeadAreCounted" TARGET="MAIN"><code>Cudd_DeadAreCounted()</code></a>
 143 <dd> Tells whether dead nodes are counted towards triggering
 144   reordering.
 145
 146 <dt> <a href="cuddAllDet.html#Cudd_DebugCheck" TARGET="MAIN"><code>Cudd_DebugCheck()</code></a>
 147 <dd> Checks for inconsistencies in the DD heap.
 148
 149 <dt> <a href="cuddAllDet.html#Cudd_Decreasing" TARGET="MAIN"><code>Cudd_Decreasing()</code></a>
 150 <dd> Determines whether a BDD is negative unate in a
 151   variable.
 152
 153 <dt> <a href="cuddAllDet.html#Cudd_DelayedDerefBdd" TARGET="MAIN"><code>Cudd_DelayedDerefBdd()</code></a>
 154 <dd> Decreases the reference count of BDD node n.
 155
 156 <dt> <a href="cuddAllDet.html#Cudd_Density" TARGET="MAIN"><code>Cudd_Density()</code></a>
 157 <dd> Computes the density of a BDD or ADD.
 158
 159 <dt> <a href="cuddAllDet.html#Cudd_Deref" TARGET="MAIN"><code>Cudd_Deref()</code></a>
 160 <dd> Decreases the reference count of node.
 161
 162 <dt> <a href="cuddAllDet.html#Cudd_DisableGarbageCollection" TARGET="MAIN"><code>Cudd_DisableGarbageCollection()</code></a>
 163 <dd> Disables garbage collection.
 164
 165 <dt> <a href="cuddAllDet.html#Cudd_DisableReorderingReporting" TARGET="MAIN"><code>Cudd_DisableReorderingReporting()</code></a>
 166 <dd> Disables reporting of reordering stats.
 167
 168 <dt> <a href="cuddAllDet.html#Cudd_Disequality" TARGET="MAIN"><code>Cudd_Disequality()</code></a>
 169 <dd> Generates a BDD for the function x - y != c.
 170
 171 <dt> <a href="cuddAllDet.html#Cudd_DumpBlifBody" TARGET="MAIN"><code>Cudd_DumpBlifBody()</code></a>
 172 <dd> Writes a blif body representing the argument BDDs.
 173
 174 <dt> <a href="cuddAllDet.html#Cudd_DumpBlif" TARGET="MAIN"><code>Cudd_DumpBlif()</code></a>
 175 <dd> Writes a blif file representing the argument BDDs.
 176
 177 <dt> <a href="cuddAllDet.html#Cudd_DumpDDcal" TARGET="MAIN"><code>Cudd_DumpDDcal()</code></a>
 178 <dd> Writes a DDcal file representing the argument BDDs.
 179
 180 <dt> <a href="cuddAllDet.html#Cudd_DumpDaVinci" TARGET="MAIN"><code>Cudd_DumpDaVinci()</code></a>
 181 <dd> Writes a daVinci file representing the argument BDDs.
 182
 183 <dt> <a href="cuddAllDet.html#Cudd_DumpDot" TARGET="MAIN"><code>Cudd_DumpDot()</code></a>
 184 <dd> Writes a dot file representing the argument DDs.
 185
 186 <dt> <a href="cuddAllDet.html#Cudd_DumpFactoredForm" TARGET="MAIN"><code>Cudd_DumpFactoredForm()</code></a>
 187 <dd> Writes factored forms representing the argument BDDs.
 188
 189 <dt> <a href="cuddAllDet.html#Cudd_Dxygtdxz" TARGET="MAIN"><code>Cudd_Dxygtdxz()</code></a>
 190 <dd> Generates a BDD for the function d(x,y) &gt; d(x,z).
 191
 192 <dt> <a href="cuddAllDet.html#Cudd_Dxygtdyz" TARGET="MAIN"><code>Cudd_Dxygtdyz()</code></a>
 193 <dd> Generates a BDD for the function d(x,y) &gt; d(y,z).
 194
 195 <dt> <a href="cuddAllDet.html#Cudd_EnableGarbageCollection" TARGET="MAIN"><code>Cudd_EnableGarbageCollection()</code></a>
 196 <dd> Enables garbage collection.
 197
 198 <dt> <a href="cuddAllDet.html#Cudd_EnableReorderingReporting" TARGET="MAIN"><code>Cudd_EnableReorderingReporting()</code></a>
 199 <dd> Enables reporting of reordering stats.
 200
 201 <dt> <a href="cuddAllDet.html#Cudd_EpdCountMinterm" TARGET="MAIN"><code>Cudd_EpdCountMinterm()</code></a>
 202 <dd> Counts the number of minterms of a DD with extended precision.
 203
 204 <dt> <a href="cuddAllDet.html#Cudd_EqualSupNorm" TARGET="MAIN"><code>Cudd_EqualSupNorm()</code></a>
 205 <dd> Compares two ADDs for equality within tolerance.
 206
 207 <dt> <a href="cuddAllDet.html#Cudd_EquivDC" TARGET="MAIN"><code>Cudd_EquivDC()</code></a>
 208 <dd> Tells whether F and G are identical wherever D is 0.
 209
 210 <dt> <a href="cuddAllDet.html#Cudd_EstimateCofactorSimple" TARGET="MAIN"><code>Cudd_EstimateCofactorSimple()</code></a>
 211 <dd> Estimates the number of nodes in a cofactor of a DD.
 212
 213 <dt> <a href="cuddAllDet.html#Cudd_EstimateCofactor" TARGET="MAIN"><code>Cudd_EstimateCofactor()</code></a>
 214 <dd> Estimates the number of nodes in a cofactor of a DD.
 215
 216 <dt> <a href="cuddAllDet.html#Cudd_Eval" TARGET="MAIN"><code>Cudd_Eval()</code></a>
 217 <dd> Returns the value of a DD for a given variable assignment.
 218
 219 <dt> <a href="cuddAllDet.html#Cudd_ExpectedUsedSlots" TARGET="MAIN"><code>Cudd_ExpectedUsedSlots()</code></a>
 220 <dd> Computes the expected fraction of used slots in the unique
 221   table.
 222
 223 <dt> <a href="cuddAllDet.html#Cudd_FindEssential" TARGET="MAIN"><code>Cudd_FindEssential()</code></a>
 224 <dd> Finds the essential variables of a DD.
 225
 226 <dt> <a href="cuddAllDet.html#Cudd_FindTwoLiteralClauses" TARGET="MAIN"><code>Cudd_FindTwoLiteralClauses()</code></a>
 227 <dd> Finds the two literal clauses of a DD.
 228
 229 <dt> <a href="cuddAllDet.html#Cudd_FirstCube" TARGET="MAIN"><code>Cudd_FirstCube()</code></a>
 230 <dd> Finds the first cube of a decision diagram.
 231
 232 <dt> <a href="cuddAllDet.html#Cudd_FirstNode" TARGET="MAIN"><code>Cudd_FirstNode()</code></a>
 233 <dd> Finds the first node of a decision diagram.
 234
 235 <dt> <a href="cuddAllDet.html#Cudd_FirstPrime" TARGET="MAIN"><code>Cudd_FirstPrime()</code></a>
 236 <dd> Finds the first prime of a Boolean function.
 237
 238 <dt> <a href="cuddAllDet.html#Cudd_FreeTree" TARGET="MAIN"><code>Cudd_FreeTree()</code></a>
 239 <dd> Frees the variable group tree of the manager.
 240
 241 <dt> <a href="cuddAllDet.html#Cudd_FreeZddTree" TARGET="MAIN"><code>Cudd_FreeZddTree()</code></a>
 242 <dd> Frees the variable group tree of the manager.
 243
 244 <dt> <a href="cuddAllDet.html#Cudd_GarbageCollectionEnabled" TARGET="MAIN"><code>Cudd_GarbageCollectionEnabled()</code></a>
 245 <dd> Tells whether garbage collection is enabled.
 246
 247 <dt> <a href="cuddAllDet.html#Cudd_GenFree" TARGET="MAIN"><code>Cudd_GenFree()</code></a>
 248 <dd> Frees a CUDD generator.
 249
 250 <dt> <a href="cuddAllDet.html#Cudd_Increasing" TARGET="MAIN"><code>Cudd_Increasing()</code></a>
 251 <dd> Determines whether a BDD is positive unate in a
 252   variable.
 253
 254 <dt> <a href="cuddAllDet.html#Cudd_IndicesToCube" TARGET="MAIN"><code>Cudd_IndicesToCube()</code></a>
 255 <dd> Builds a cube of BDD variables from an array of indices.
 256
 257 <dt> <a href="cuddAllDet.html#Cudd_Inequality" TARGET="MAIN"><code>Cudd_Inequality()</code></a>
 258 <dd> Generates a BDD for the function x - y &ge; c.
 259
 260 <dt> <a href="cuddAllDet.html#Cudd_Init" TARGET="MAIN"><code>Cudd_Init()</code></a>
 261 <dd> Creates a new DD manager.
 262
 263 <dt> <a href="cuddAllDet.html#Cudd_IsGenEmpty" TARGET="MAIN"><code>Cudd_IsGenEmpty()</code></a>
 264 <dd> Queries the status of a generator.
 265
 266 <dt> <a href="cuddAllDet.html#Cudd_IsInHook" TARGET="MAIN"><code>Cudd_IsInHook()</code></a>
 267 <dd> Checks whether a function is in a hook.
 268
 269 <dt> <a href="cuddAllDet.html#Cudd_IsNonConstant" TARGET="MAIN"><code>Cudd_IsNonConstant()</code></a>
 270 <dd> Returns 1 if a DD node is not constant.
 271
 272 <dt> <a href="cuddAllDet.html#Cudd_IterDerefBdd" TARGET="MAIN"><code>Cudd_IterDerefBdd()</code></a>
 273 <dd> Decreases the reference count of BDD node n.
 274
 275 <dt> <a href="cuddAllDet.html#Cudd_LargestCube" TARGET="MAIN"><code>Cudd_LargestCube()</code></a>
 276 <dd> Finds a largest cube in a DD.
 277
 278 <dt> <a href="cuddAllDet.html#Cudd_MakeBddFromZddCover" TARGET="MAIN"><code>Cudd_MakeBddFromZddCover()</code></a>
 279 <dd> Converts a ZDD cover to a BDD graph.
 280
 281 <dt> <a href="cuddAllDet.html#Cudd_MakeTreeNode" TARGET="MAIN"><code>Cudd_MakeTreeNode()</code></a>
 282 <dd> Creates a new variable group.
 283
 284 <dt> <a href="cuddAllDet.html#Cudd_MakeZddTreeNode" TARGET="MAIN"><code>Cudd_MakeZddTreeNode()</code></a>
 285 <dd> Creates a new ZDD variable group.
 286
 287 <dt> <a href="cuddAllDet.html#Cudd_MinHammingDist" TARGET="MAIN"><code>Cudd_MinHammingDist()</code></a>
 288 <dd> Returns the minimum Hamming distance between f and minterm.
 289
 290 <dt> <a href="cuddAllDet.html#Cudd_NewApaNumber" TARGET="MAIN"><code>Cudd_NewApaNumber()</code></a>
 291 <dd> Allocates memory for an arbitrary precision integer.
 292
 293 <dt> <a href="cuddAllDet.html#Cudd_NextCube" TARGET="MAIN"><code>Cudd_NextCube()</code></a>
 294 <dd> Generates the next cube of a decision diagram onset.
 295
 296 <dt> <a href="cuddAllDet.html#Cudd_NextNode" TARGET="MAIN"><code>Cudd_NextNode()</code></a>
 297 <dd> Finds the next node of a decision diagram.
 298
 299 <dt> <a href="cuddAllDet.html#Cudd_NextPrime" TARGET="MAIN"><code>Cudd_NextPrime()</code></a>
 300 <dd> Generates the next prime of a Boolean function.
 301
 302 <dt> <a href="cuddAllDet.html#Cudd_NodeReadIndex" TARGET="MAIN"><code>Cudd_NodeReadIndex()</code></a>
 303 <dd> Returns the index of the node.
 304
 305 <dt> <a href="cuddAllDet.html#Cudd_OutOfMem" TARGET="MAIN"><code>Cudd_OutOfMem()</code></a>
 306 <dd> Warns that a memory allocation failed.
 307
 308 <dt> <a href="cuddAllDet.html#Cudd_OverApprox" TARGET="MAIN"><code>Cudd_OverApprox()</code></a>
 309 <dd> Extracts a dense superset from a BDD with Shiple's
 310   underapproximation method.
 311
 312 <dt> <a href="cuddAllDet.html#Cudd_Prime" TARGET="MAIN"><code>Cudd_Prime()</code></a>
 313 <dd> Returns the next prime &gt;= p.
 314
 315 <dt> <a href="cuddAllDet.html#Cudd_PrintDebug" TARGET="MAIN"><code>Cudd_PrintDebug()</code></a>
 316 <dd> Prints to the standard output a DD and its statistics.
 317
 318 <dt> <a href="cuddAllDet.html#Cudd_PrintInfo" TARGET="MAIN"><code>Cudd_PrintInfo()</code></a>
 319 <dd> Prints out statistics and settings for a CUDD manager.
 320
 321 <dt> <a href="cuddAllDet.html#Cudd_PrintLinear" TARGET="MAIN"><code>Cudd_PrintLinear()</code></a>
 322 <dd> Prints the linear transform matrix.
 323
 324 <dt> <a href="cuddAllDet.html#Cudd_PrintMinterm" TARGET="MAIN"><code>Cudd_PrintMinterm()</code></a>
 325 <dd> Prints a disjoint sum of products.
 326
 327 <dt> <a href="cuddAllDet.html#Cudd_PrintTwoLiteralClauses" TARGET="MAIN"><code>Cudd_PrintTwoLiteralClauses()</code></a>
 328 <dd> Prints the two literal clauses of a DD.
 329
 330 <dt> <a href="cuddAllDet.html#Cudd_PrintVersion" TARGET="MAIN"><code>Cudd_PrintVersion()</code></a>
 331 <dd> Prints the package version number.
 332
 333 <dt> <a href="cuddAllDet.html#Cudd_PrioritySelect" TARGET="MAIN"><code>Cudd_PrioritySelect()</code></a>
 334 <dd> Selects pairs from R using a priority function.
 335
 336 <dt> <a href="cuddAllDet.html#Cudd_Quit" TARGET="MAIN"><code>Cudd_Quit()</code></a>
 337 <dd> Deletes resources associated with a DD manager.
 338
 339 <dt> <a href="cuddAllDet.html#Cudd_Random" TARGET="MAIN"><code>Cudd_Random()</code></a>
 340 <dd> Portable random number generator.
 341
 342 <dt> <a href="cuddAllDet.html#Cudd_ReadArcviolation" TARGET="MAIN"><code>Cudd_ReadArcviolation()</code></a>
 343 <dd> Returns the current value of the arcviolation parameter used
 344   in group sifting.
 345
 346 <dt> <a href="cuddAllDet.html#Cudd_ReadBackground" TARGET="MAIN"><code>Cudd_ReadBackground()</code></a>
 347 <dd> Reads the background constant of the manager.
 348
 349 <dt> <a href="cuddAllDet.html#Cudd_ReadCacheHits" TARGET="MAIN"><code>Cudd_ReadCacheHits()</code></a>
 350 <dd> Returns the number of cache hits.
 351
 352 <dt> <a href="cuddAllDet.html#Cudd_ReadCacheLookUps" TARGET="MAIN"><code>Cudd_ReadCacheLookUps()</code></a>
 353 <dd> Returns the number of cache look-ups.
 354
 355 <dt> <a href="cuddAllDet.html#Cudd_ReadCacheSlots" TARGET="MAIN"><code>Cudd_ReadCacheSlots()</code></a>
 356 <dd> Reads the number of slots in the cache.
 357
 358 <dt> <a href="cuddAllDet.html#Cudd_ReadCacheUsedSlots" TARGET="MAIN"><code>Cudd_ReadCacheUsedSlots()</code></a>
 359 <dd> Reads the fraction of used slots in the cache.
 360
 361 <dt> <a href="cuddAllDet.html#Cudd_ReadDead" TARGET="MAIN"><code>Cudd_ReadDead()</code></a>
 362 <dd> Returns the number of dead nodes in the unique table.
 363
 364 <dt> <a href="cuddAllDet.html#Cudd_ReadEpsilon" TARGET="MAIN"><code>Cudd_ReadEpsilon()</code></a>
 365 <dd> Reads the epsilon parameter of the manager.
 366
 367 <dt> <a href="cuddAllDet.html#Cudd_ReadErrorCode" TARGET="MAIN"><code>Cudd_ReadErrorCode()</code></a>
 368 <dd> Returns the code of the last error.
 369
 370 <dt> <a href="cuddAllDet.html#Cudd_ReadGarbageCollectionTime" TARGET="MAIN"><code>Cudd_ReadGarbageCollectionTime()</code></a>
 371 <dd> Returns the time spent in garbage collection.
 372
 373 <dt> <a href="cuddAllDet.html#Cudd_ReadGarbageCollections" TARGET="MAIN"><code>Cudd_ReadGarbageCollections()</code></a>
 374 <dd> Returns the number of times garbage collection has occurred.
 375
 376 <dt> <a href="cuddAllDet.html#Cudd_ReadGroupcheck" TARGET="MAIN"><code>Cudd_ReadGroupcheck()</code></a>
 377 <dd> Reads the groupcheck parameter of the manager.
 378
 379 <dt> <a href="cuddAllDet.html#Cudd_ReadInvPermZdd" TARGET="MAIN"><code>Cudd_ReadInvPermZdd()</code></a>
 380 <dd> Returns the index of the ZDD variable currently in the i-th
 381   position of the order.
 382
 383 <dt> <a href="cuddAllDet.html#Cudd_ReadInvPerm" TARGET="MAIN"><code>Cudd_ReadInvPerm()</code></a>
 384 <dd> Returns the index of the variable currently in the i-th
 385   position of the order.
 386
 387 <dt> <a href="cuddAllDet.html#Cudd_ReadIthClause" TARGET="MAIN"><code>Cudd_ReadIthClause()</code></a>
 388 <dd> Accesses the i-th clause of a DD.
 389
 390 <dt> <a href="cuddAllDet.html#Cudd_ReadKeys" TARGET="MAIN"><code>Cudd_ReadKeys()</code></a>
 391 <dd> Returns the number of nodes in the unique table.
 392
 393 <dt> <a href="cuddAllDet.html#Cudd_ReadLinear" TARGET="MAIN"><code>Cudd_ReadLinear()</code></a>
 394 <dd> Reads an entry of the linear transform matrix.
 395
 396 <dt> <a href="cuddAllDet.html#Cudd_ReadLogicZero" TARGET="MAIN"><code>Cudd_ReadLogicZero()</code></a>
 397 <dd> Returns the logic zero constant of the manager.
 398
 399 <dt> <a href="cuddAllDet.html#Cudd_ReadLooseUpTo" TARGET="MAIN"><code>Cudd_ReadLooseUpTo()</code></a>
 400 <dd> Reads the looseUpTo parameter of the manager.
 401
 402 <dt> <a href="cuddAllDet.html#Cudd_ReadMaxCacheHard" TARGET="MAIN"><code>Cudd_ReadMaxCacheHard()</code></a>
 403 <dd> Reads the maxCacheHard parameter of the manager.
 404
 405 <dt> <a href="cuddAllDet.html#Cudd_ReadMaxCache" TARGET="MAIN"><code>Cudd_ReadMaxCache()</code></a>
 406 <dd> Returns the soft limit for the cache size.
 407
 408 <dt> <a href="cuddAllDet.html#Cudd_ReadMaxGrowthAlternate" TARGET="MAIN"><code>Cudd_ReadMaxGrowthAlternate()</code></a>
 409 <dd> Reads the maxGrowthAlt parameter of the manager.
 410
 411 <dt> <a href="cuddAllDet.html#Cudd_ReadMaxGrowth" TARGET="MAIN"><code>Cudd_ReadMaxGrowth()</code></a>
 412 <dd> Reads the maxGrowth parameter of the manager.
 413
 414 <dt> <a href="cuddAllDet.html#Cudd_ReadMaxLive" TARGET="MAIN"><code>Cudd_ReadMaxLive()</code></a>
 415 <dd> Reads the maximum allowed number of live nodes.
 416
 417 <dt> <a href="cuddAllDet.html#Cudd_ReadMaxMemory" TARGET="MAIN"><code>Cudd_ReadMaxMemory()</code></a>
 418 <dd> Reads the maximum allowed memory.
 419
 420 <dt> <a href="cuddAllDet.html#Cudd_ReadMemoryInUse" TARGET="MAIN"><code>Cudd_ReadMemoryInUse()</code></a>
 421 <dd> Returns the memory in use by the manager measured in bytes.
 422
 423 <dt> <a href="cuddAllDet.html#Cudd_ReadMinDead" TARGET="MAIN"><code>Cudd_ReadMinDead()</code></a>
 424 <dd> Reads the minDead parameter of the manager.
 425
 426 <dt> <a href="cuddAllDet.html#Cudd_ReadMinHit" TARGET="MAIN"><code>Cudd_ReadMinHit()</code></a>
 427 <dd> Reads the hit rate that causes resizinig of the computed
 428   table.
 429
 430 <dt> <a href="cuddAllDet.html#Cudd_ReadMinusInfinity" TARGET="MAIN"><code>Cudd_ReadMinusInfinity()</code></a>
 431 <dd> Reads the minus-infinity constant from the manager.
 432
 433 <dt> <a href="cuddAllDet.html#Cudd_ReadNextReordering" TARGET="MAIN"><code>Cudd_ReadNextReordering()</code></a>
 434 <dd> Returns the threshold for the next dynamic reordering.
 435
 436 <dt> <a href="cuddAllDet.html#Cudd_ReadNodeCount" TARGET="MAIN"><code>Cudd_ReadNodeCount()</code></a>
 437 <dd> Reports the number of nodes in BDDs and ADDs.
 438
 439 <dt> <a href="cuddAllDet.html#Cudd_ReadNodesDropped" TARGET="MAIN"><code>Cudd_ReadNodesDropped()</code></a>
 440 <dd> Returns the number of nodes dropped.
 441
 442 <dt> <a href="cuddAllDet.html#Cudd_ReadNodesFreed" TARGET="MAIN"><code>Cudd_ReadNodesFreed()</code></a>
 443 <dd> Returns the number of nodes freed.
 444
 445 <dt> <a href="cuddAllDet.html#Cudd_ReadNumberXovers" TARGET="MAIN"><code>Cudd_ReadNumberXovers()</code></a>
 446 <dd> Reads the current number of crossovers used by the
 447   genetic algorithm for reordering.
 448
 449 <dt> <a href="cuddAllDet.html#Cudd_ReadOne" TARGET="MAIN"><code>Cudd_ReadOne()</code></a>
 450 <dd> Returns the one constant of the manager.
 451
 452 <dt> <a href="cuddAllDet.html#Cudd_ReadPeakLiveNodeCount" TARGET="MAIN"><code>Cudd_ReadPeakLiveNodeCount()</code></a>
 453 <dd> Reports the peak number of live nodes.
 454
 455 <dt> <a href="cuddAllDet.html#Cudd_ReadPeakNodeCount" TARGET="MAIN"><code>Cudd_ReadPeakNodeCount()</code></a>
 456 <dd> Reports the peak number of nodes.
 457
 458 <dt> <a href="cuddAllDet.html#Cudd_ReadPermZdd" TARGET="MAIN"><code>Cudd_ReadPermZdd()</code></a>
 459 <dd> Returns the current position of the i-th ZDD variable in the
 460   order.
 461
 462 <dt> <a href="cuddAllDet.html#Cudd_ReadPerm" TARGET="MAIN"><code>Cudd_ReadPerm()</code></a>
 463 <dd> Returns the current position of the i-th variable in the
 464   order.
 465
 466 <dt> <a href="cuddAllDet.html#Cudd_ReadPlusInfinity" TARGET="MAIN"><code>Cudd_ReadPlusInfinity()</code></a>
 467 <dd> Reads the plus-infinity constant from the manager.
 468
 469 <dt> <a href="cuddAllDet.html#Cudd_ReadPopulationSize" TARGET="MAIN"><code>Cudd_ReadPopulationSize()</code></a>
 470 <dd> Reads the current size of the population used by the
 471   genetic algorithm for reordering.
 472
 473 <dt> <a href="cuddAllDet.html#Cudd_ReadRecomb" TARGET="MAIN"><code>Cudd_ReadRecomb()</code></a>
 474 <dd> Returns the current value of the recombination parameter used
 475   in group sifting.
 476
 477 <dt> <a href="cuddAllDet.html#Cudd_ReadRecursiveCalls" TARGET="MAIN"><code>Cudd_ReadRecursiveCalls()</code></a>
 478 <dd> Returns the number of recursive calls.
 479
 480 <dt> <a href="cuddAllDet.html#Cudd_ReadReorderingCycle" TARGET="MAIN"><code>Cudd_ReadReorderingCycle()</code></a>
 481 <dd> Reads the reordCycle parameter of the manager.
 482
 483 <dt> <a href="cuddAllDet.html#Cudd_ReadReorderingTime" TARGET="MAIN"><code>Cudd_ReadReorderingTime()</code></a>
 484 <dd> Returns the time spent in reordering.
 485
 486 <dt> <a href="cuddAllDet.html#Cudd_ReadReorderings" TARGET="MAIN"><code>Cudd_ReadReorderings()</code></a>
 487 <dd> Returns the number of times reordering has occurred.
 488
 489 <dt> <a href="cuddAllDet.html#Cudd_ReadSiftMaxSwap" TARGET="MAIN"><code>Cudd_ReadSiftMaxSwap()</code></a>
 490 <dd> Reads the siftMaxSwap parameter of the manager.
 491
 492 <dt> <a href="cuddAllDet.html#Cudd_ReadSiftMaxVar" TARGET="MAIN"><code>Cudd_ReadSiftMaxVar()</code></a>
 493 <dd> Reads the siftMaxVar parameter of the manager.
 494
 495 <dt> <a href="cuddAllDet.html#Cudd_ReadSize" TARGET="MAIN"><code>Cudd_ReadSize()</code></a>
 496 <dd> Returns the number of BDD variables in existance.
 497
 498 <dt> <a href="cuddAllDet.html#Cudd_ReadSlots" TARGET="MAIN"><code>Cudd_ReadSlots()</code></a>
 499 <dd> Returns the total number of slots of the unique table.
 500
 501 <dt> <a href="cuddAllDet.html#Cudd_ReadStderr" TARGET="MAIN"><code>Cudd_ReadStderr()</code></a>
 502 <dd> Reads the stderr of a manager.
 503
 504 <dt> <a href="cuddAllDet.html#Cudd_ReadStdout" TARGET="MAIN"><code>Cudd_ReadStdout()</code></a>
 505 <dd> Reads the stdout of a manager.
 506
 507 <dt> <a href="cuddAllDet.html#Cudd_ReadSwapSteps" TARGET="MAIN"><code>Cudd_ReadSwapSteps()</code></a>
 508 <dd> Reads the number of elementary reordering steps.
 509
 510 <dt> <a href="cuddAllDet.html#Cudd_ReadSymmviolation" TARGET="MAIN"><code>Cudd_ReadSymmviolation()</code></a>
 511 <dd> Returns the current value of the symmviolation parameter used
 512   in group sifting.
 513
 514 <dt> <a href="cuddAllDet.html#Cudd_ReadTree" TARGET="MAIN"><code>Cudd_ReadTree()</code></a>
 515 <dd> Returns the variable group tree of the manager.
 516
 517 <dt> <a href="cuddAllDet.html#Cudd_ReadUniqueLinks" TARGET="MAIN"><code>Cudd_ReadUniqueLinks()</code></a>
 518 <dd> Returns the number of links followed in the unique table.
 519
 520 <dt> <a href="cuddAllDet.html#Cudd_ReadUniqueLookUps" TARGET="MAIN"><code>Cudd_ReadUniqueLookUps()</code></a>
 521 <dd> Returns the number of look-ups in the unique table.
 522
 523 <dt> <a href="cuddAllDet.html#Cudd_ReadUsedSlots" TARGET="MAIN"><code>Cudd_ReadUsedSlots()</code></a>
 524 <dd> Reads the fraction of used slots in the unique table.
 525
 526 <dt> <a href="cuddAllDet.html#Cudd_ReadVars" TARGET="MAIN"><code>Cudd_ReadVars()</code></a>
 527 <dd> Returns the i-th element of the vars array.
 528
 529 <dt> <a href="cuddAllDet.html#Cudd_ReadZddOne" TARGET="MAIN"><code>Cudd_ReadZddOne()</code></a>
 530 <dd> Returns the ZDD for the constant 1 function.
 531
 532 <dt> <a href="cuddAllDet.html#Cudd_ReadZddSize" TARGET="MAIN"><code>Cudd_ReadZddSize()</code></a>
 533 <dd> Returns the number of ZDD variables in existance.
 534
 535 <dt> <a href="cuddAllDet.html#Cudd_ReadZddTree" TARGET="MAIN"><code>Cudd_ReadZddTree()</code></a>
 536 <dd> Returns the variable group tree of the manager.
 537
 538 <dt> <a href="cuddAllDet.html#Cudd_ReadZero" TARGET="MAIN"><code>Cudd_ReadZero()</code></a>
 539 <dd> Returns the zero constant of the manager.
 540
 541 <dt> <a href="cuddAllDet.html#Cudd_RecursiveDerefZdd" TARGET="MAIN"><code>Cudd_RecursiveDerefZdd()</code></a>
 542 <dd> Decreases the reference count of ZDD node n.
 543
 544 <dt> <a href="cuddAllDet.html#Cudd_RecursiveDeref" TARGET="MAIN"><code>Cudd_RecursiveDeref()</code></a>
 545 <dd> Decreases the reference count of node n.
 546
 547 <dt> <a href="cuddAllDet.html#Cudd_ReduceHeap" TARGET="MAIN"><code>Cudd_ReduceHeap()</code></a>
 548 <dd> Main dynamic reordering routine.
 549
 550 <dt> <a href="cuddAllDet.html#Cudd_Ref" TARGET="MAIN"><code>Cudd_Ref()</code></a>
 551 <dd> Increases the reference count of a node, if it is not
 552   saturated.
 553
 554 <dt> <a href="cuddAllDet.html#Cudd_RemapOverApprox" TARGET="MAIN"><code>Cudd_RemapOverApprox()</code></a>
 555 <dd> Extracts a dense superset from a BDD with the remapping
 556   underapproximation method.
 557
 558 <dt> <a href="cuddAllDet.html#Cudd_RemapUnderApprox" TARGET="MAIN"><code>Cudd_RemapUnderApprox()</code></a>
 559 <dd> Extracts a dense subset from a BDD with the remapping
 560   underapproximation method.
 561
 562 <dt> <a href="cuddAllDet.html#Cudd_RemoveHook" TARGET="MAIN"><code>Cudd_RemoveHook()</code></a>
 563 <dd> Removes a function from a hook.
 564
 565 <dt> <a href="cuddAllDet.html#Cudd_ReorderingReporting" TARGET="MAIN"><code>Cudd_ReorderingReporting()</code></a>
 566 <dd> Returns 1 if reporting of reordering stats is enabled.
 567
 568 <dt> <a href="cuddAllDet.html#Cudd_ReorderingStatusZdd" TARGET="MAIN"><code>Cudd_ReorderingStatusZdd()</code></a>
 569 <dd> Reports the status of automatic dynamic reordering of ZDDs.
 570
 571 <dt> <a href="cuddAllDet.html#Cudd_ReorderingStatus" TARGET="MAIN"><code>Cudd_ReorderingStatus()</code></a>
 572 <dd> Reports the status of automatic dynamic reordering of BDDs
 573   and ADDs.
 574
 575 <dt> <a href="cuddAllDet.html#Cudd_SetArcviolation" TARGET="MAIN"><code>Cudd_SetArcviolation()</code></a>
 576 <dd> Sets the value of the arcviolation parameter used
 577   in group sifting.
 578
 579 <dt> <a href="cuddAllDet.html#Cudd_SetBackground" TARGET="MAIN"><code>Cudd_SetBackground()</code></a>
 580 <dd> Sets the background constant of the manager.
 581
 582 <dt> <a href="cuddAllDet.html#Cudd_SetEpsilon" TARGET="MAIN"><code>Cudd_SetEpsilon()</code></a>
 583 <dd> Sets the epsilon parameter of the manager to ep.
 584
 585 <dt> <a href="cuddAllDet.html#Cudd_SetGroupcheck" TARGET="MAIN"><code>Cudd_SetGroupcheck()</code></a>
 586 <dd> Sets the parameter groupcheck of the manager to gc.
 587
 588 <dt> <a href="cuddAllDet.html#Cudd_SetLooseUpTo" TARGET="MAIN"><code>Cudd_SetLooseUpTo()</code></a>
 589 <dd> Sets the looseUpTo parameter of the manager.
 590
 591 <dt> <a href="cuddAllDet.html#Cudd_SetMaxCacheHard" TARGET="MAIN"><code>Cudd_SetMaxCacheHard()</code></a>
 592 <dd> Sets the maxCacheHard parameter of the manager.
 593
 594 <dt> <a href="cuddAllDet.html#Cudd_SetMaxGrowthAlternate" TARGET="MAIN"><code>Cudd_SetMaxGrowthAlternate()</code></a>
 595 <dd> Sets the maxGrowthAlt parameter of the manager.
 596
 597 <dt> <a href="cuddAllDet.html#Cudd_SetMaxGrowth" TARGET="MAIN"><code>Cudd_SetMaxGrowth()</code></a>
 598 <dd> Sets the maxGrowth parameter of the manager.
 599
 600 <dt> <a href="cuddAllDet.html#Cudd_SetMaxLive" TARGET="MAIN"><code>Cudd_SetMaxLive()</code></a>
 601 <dd> Sets the maximum allowed number of live nodes.
 602
 603 <dt> <a href="cuddAllDet.html#Cudd_SetMaxMemory" TARGET="MAIN"><code>Cudd_SetMaxMemory()</code></a>
 604 <dd> Sets the maximum allowed memory.
 605
 606 <dt> <a href="cuddAllDet.html#Cudd_SetMinHit" TARGET="MAIN"><code>Cudd_SetMinHit()</code></a>
 607 <dd> Sets the hit rate that causes resizinig of the computed
 608   table.
 609
 610 <dt> <a href="cuddAllDet.html#Cudd_SetNextReordering" TARGET="MAIN"><code>Cudd_SetNextReordering()</code></a>
 611 <dd> Sets the threshold for the next dynamic reordering.
 612
 613 <dt> <a href="cuddAllDet.html#Cudd_SetNumberXovers" TARGET="MAIN"><code>Cudd_SetNumberXovers()</code></a>
 614 <dd> Sets the number of crossovers used by the
 615   genetic algorithm for reordering.
 616
 617 <dt> <a href="cuddAllDet.html#Cudd_SetPopulationSize" TARGET="MAIN"><code>Cudd_SetPopulationSize()</code></a>
 618 <dd> Sets the size of the population used by the
 619   genetic algorithm for reordering.
 620
 621 <dt> <a href="cuddAllDet.html#Cudd_SetRecomb" TARGET="MAIN"><code>Cudd_SetRecomb()</code></a>
 622 <dd> Sets the value of the recombination parameter used in group
 623   sifting.
 624
 625 <dt> <a href="cuddAllDet.html#Cudd_SetReorderingCycle" TARGET="MAIN"><code>Cudd_SetReorderingCycle()</code></a>
 626 <dd> Sets the reordCycle parameter of the manager.
 627
 628 <dt> <a href="cuddAllDet.html#Cudd_SetSiftMaxSwap" TARGET="MAIN"><code>Cudd_SetSiftMaxSwap()</code></a>
 629 <dd> Sets the siftMaxSwap parameter of the manager.
 630
 631 <dt> <a href="cuddAllDet.html#Cudd_SetSiftMaxVar" TARGET="MAIN"><code>Cudd_SetSiftMaxVar()</code></a>
 632 <dd> Sets the siftMaxVar parameter of the manager.
 633
 634 <dt> <a href="cuddAllDet.html#Cudd_SetStderr" TARGET="MAIN"><code>Cudd_SetStderr()</code></a>
 635 <dd> Sets the stderr of a manager.
 636
 637 <dt> <a href="cuddAllDet.html#Cudd_SetStdout" TARGET="MAIN"><code>Cudd_SetStdout()</code></a>
 638 <dd> Sets the stdout of a manager.
 639
 640 <dt> <a href="cuddAllDet.html#Cudd_SetSymmviolation" TARGET="MAIN"><code>Cudd_SetSymmviolation()</code></a>
 641 <dd> Sets the value of the symmviolation parameter used
 642   in group sifting.
 643
 644 <dt> <a href="cuddAllDet.html#Cudd_SetTree" TARGET="MAIN"><code>Cudd_SetTree()</code></a>
 645 <dd> Sets the variable group tree of the manager.
 646
 647 <dt> <a href="cuddAllDet.html#Cudd_SetVarMap" TARGET="MAIN"><code>Cudd_SetVarMap()</code></a>
 648 <dd> Registers a variable mapping with the manager.
 649
 650 <dt> <a href="cuddAllDet.html#Cudd_SetZddTree" TARGET="MAIN"><code>Cudd_SetZddTree()</code></a>
 651 <dd> Sets the ZDD variable group tree of the manager.
 652
 653 <dt> <a href="cuddAllDet.html#Cudd_SharingSize" TARGET="MAIN"><code>Cudd_SharingSize()</code></a>
 654 <dd> Counts the number of nodes in an array of DDs.
 655
 656 <dt> <a href="cuddAllDet.html#Cudd_ShortestLength" TARGET="MAIN"><code>Cudd_ShortestLength()</code></a>
 657 <dd> Find the length of the shortest path(s) in a DD.
 658
 659 <dt> <a href="cuddAllDet.html#Cudd_ShortestPath" TARGET="MAIN"><code>Cudd_ShortestPath()</code></a>
 660 <dd> Finds a shortest path in a DD.
 661
 662 <dt> <a href="cuddAllDet.html#Cudd_ShuffleHeap" TARGET="MAIN"><code>Cudd_ShuffleHeap()</code></a>
 663 <dd> Reorders variables according to given permutation.
 664
 665 <dt> <a href="cuddAllDet.html#Cudd_SolveEqn" TARGET="MAIN"><code>Cudd_SolveEqn()</code></a>
 666 <dd> Implements the solution of F(x,y) = 0.
 667
 668 <dt> <a href="cuddAllDet.html#Cudd_SplitSet" TARGET="MAIN"><code>Cudd_SplitSet()</code></a>
 669 <dd> Returns m minterms from a BDD.
 670
 671 <dt> <a href="cuddAllDet.html#Cudd_Srandom" TARGET="MAIN"><code>Cudd_Srandom()</code></a>
 672 <dd> Initializer for the portable random number generator.
 673
 674 <dt> <a href="cuddAllDet.html#Cudd_StdPostReordHook" TARGET="MAIN"><code>Cudd_StdPostReordHook()</code></a>
 675 <dd> Sample hook function to call after reordering.
 676
 677 <dt> <a href="cuddAllDet.html#Cudd_StdPreReordHook" TARGET="MAIN"><code>Cudd_StdPreReordHook()</code></a>
 678 <dd> Sample hook function to call before reordering.
 679
 680 <dt> <a href="cuddAllDet.html#Cudd_SubsetCompress" TARGET="MAIN"><code>Cudd_SubsetCompress()</code></a>
 681 <dd> Find a dense subset of BDD <code>f</code>.
 682
 683 <dt> <a href="cuddAllDet.html#Cudd_SubsetHeavyBranch" TARGET="MAIN"><code>Cudd_SubsetHeavyBranch()</code></a>
 684 <dd> Extracts a dense subset from a BDD with the heavy branch
 685   heuristic.
 686
 687 <dt> <a href="cuddAllDet.html#Cudd_SubsetShortPaths" TARGET="MAIN"><code>Cudd_SubsetShortPaths()</code></a>
 688 <dd> Extracts a dense subset from a BDD with the shortest paths
 689   heuristic.
 690
 691 <dt> <a href="cuddAllDet.html#Cudd_SubsetWithMaskVars" TARGET="MAIN"><code>Cudd_SubsetWithMaskVars()</code></a>
 692 <dd> Extracts a subset from a BDD.
 693
 694 <dt> <a href="cuddAllDet.html#Cudd_SupersetCompress" TARGET="MAIN"><code>Cudd_SupersetCompress()</code></a>
 695 <dd> Find a dense superset of BDD <code>f</code>.
 696
 697 <dt> <a href="cuddAllDet.html#Cudd_SupersetHeavyBranch" TARGET="MAIN"><code>Cudd_SupersetHeavyBranch()</code></a>
 698 <dd> Extracts a dense superset from a BDD with the heavy branch
 699   heuristic.
 700
 701 <dt> <a href="cuddAllDet.html#Cudd_SupersetShortPaths" TARGET="MAIN"><code>Cudd_SupersetShortPaths()</code></a>
 702 <dd> Extracts a dense superset from a BDD with the shortest paths
 703   heuristic.
 704
 705 <dt> <a href="cuddAllDet.html#Cudd_SupportIndex" TARGET="MAIN"><code>Cudd_SupportIndex()</code></a>
 706 <dd> Finds the variables on which a DD depends.
 707
 708 <dt> <a href="cuddAllDet.html#Cudd_SupportSize" TARGET="MAIN"><code>Cudd_SupportSize()</code></a>
 709 <dd> Counts the variables on which a DD depends.
 710
 711 <dt> <a href="cuddAllDet.html#Cudd_Support" TARGET="MAIN"><code>Cudd_Support()</code></a>
 712 <dd> Finds the variables on which a DD depends.
 713
 714 <dt> <a href="cuddAllDet.html#Cudd_SymmProfile" TARGET="MAIN"><code>Cudd_SymmProfile()</code></a>
 715 <dd> Prints statistics on symmetric variables.
 716
 717 <dt> <a href="cuddAllDet.html#Cudd_TurnOffCountDead" TARGET="MAIN"><code>Cudd_TurnOffCountDead()</code></a>
 718 <dd> Causes the dead nodes not to be counted towards triggering
 719   reordering.
 720
 721 <dt> <a href="cuddAllDet.html#Cudd_TurnOnCountDead" TARGET="MAIN"><code>Cudd_TurnOnCountDead()</code></a>
 722 <dd> Causes the dead nodes to be counted towards triggering
 723   reordering.
 724
 725 <dt> <a href="cuddAllDet.html#Cudd_UnderApprox" TARGET="MAIN"><code>Cudd_UnderApprox()</code></a>
 726 <dd> Extracts a dense subset from a BDD with Shiple's
 727   underapproximation method.
 728
 729 <dt> <a href="cuddAllDet.html#Cudd_VectorSupportIndex" TARGET="MAIN"><code>Cudd_VectorSupportIndex()</code></a>
 730 <dd> Finds the variables on which a set of DDs depends.
 731
 732 <dt> <a href="cuddAllDet.html#Cudd_VectorSupportSize" TARGET="MAIN"><code>Cudd_VectorSupportSize()</code></a>
 733 <dd> Counts the variables on which a set of DDs depends.
 734
 735 <dt> <a href="cuddAllDet.html#Cudd_VectorSupport" TARGET="MAIN"><code>Cudd_VectorSupport()</code></a>
 736 <dd> Finds the variables on which a set of DDs depends.
 737
 738 <dt> <a href="cuddAllDet.html#Cudd_VerifySol" TARGET="MAIN"><code>Cudd_VerifySol()</code></a>
 739 <dd> Checks the solution of F(x,y) = 0.
 740
 741 <dt> <a href="cuddAllDet.html#Cudd_Xeqy" TARGET="MAIN"><code>Cudd_Xeqy()</code></a>
 742 <dd> Generates a BDD for the function x==y.
 743
 744 <dt> <a href="cuddAllDet.html#Cudd_Xgty" TARGET="MAIN"><code>Cudd_Xgty()</code></a>
 745 <dd> Generates a BDD for the function x &gt; y.
 746
 747 <dt> <a href="cuddAllDet.html#Cudd_addAgreement" TARGET="MAIN"><code>Cudd_addAgreement()</code></a>
 748 <dd> f if f==g; background if f!=g.
 749
 750 <dt> <a href="cuddAllDet.html#Cudd_addApply" TARGET="MAIN"><code>Cudd_addApply()</code></a>
 751 <dd> Applies op to the corresponding discriminants of f and g.
 752
 753 <dt> <a href="cuddAllDet.html#Cudd_addBddInterval" TARGET="MAIN"><code>Cudd_addBddInterval()</code></a>
 754 <dd> Converts an ADD to a BDD.
 755
 756 <dt> <a href="cuddAllDet.html#Cudd_addBddIthBit" TARGET="MAIN"><code>Cudd_addBddIthBit()</code></a>
 757 <dd> Converts an ADD to a BDD by extracting the i-th bit from
 758   the leaves.
 759
 760 <dt> <a href="cuddAllDet.html#Cudd_addBddPattern" TARGET="MAIN"><code>Cudd_addBddPattern()</code></a>
 761 <dd> Converts an ADD to a BDD.
 762
 763 <dt> <a href="cuddAllDet.html#Cudd_addBddStrictThreshold" TARGET="MAIN"><code>Cudd_addBddStrictThreshold()</code></a>
 764 <dd> Converts an ADD to a BDD.
 765
 766 <dt> <a href="cuddAllDet.html#Cudd_addBddThreshold" TARGET="MAIN"><code>Cudd_addBddThreshold()</code></a>
 767 <dd> Converts an ADD to a BDD.
 768
 769 <dt> <a href="cuddAllDet.html#Cudd_addCmpl" TARGET="MAIN"><code>Cudd_addCmpl()</code></a>
 770 <dd> Computes the complement of an ADD a la C language.
 771
 772 <dt> <a href="cuddAllDet.html#Cudd_addCompose" TARGET="MAIN"><code>Cudd_addCompose()</code></a>
 773 <dd> Substitutes g for x_v in the ADD for f.
 774
 775 <dt> <a href="cuddAllDet.html#Cudd_addComputeCube" TARGET="MAIN"><code>Cudd_addComputeCube()</code></a>
 776 <dd> Computes the cube of an array of ADD variables.
 777
 778 <dt> <a href="cuddAllDet.html#Cudd_addConstrain" TARGET="MAIN"><code>Cudd_addConstrain()</code></a>
 779 <dd> Computes f constrain c for ADDs.
 780
 781 <dt> <a href="cuddAllDet.html#Cudd_addConst" TARGET="MAIN"><code>Cudd_addConst()</code></a>
 782 <dd> Returns the ADD for constant c.
 783
 784 <dt> <a href="cuddAllDet.html#Cudd_addDiff" TARGET="MAIN"><code>Cudd_addDiff()</code></a>
 785 <dd> Returns plusinfinity if f=g; returns min(f,g) if f!=g.
 786
 787 <dt> <a href="cuddAllDet.html#Cudd_addDivide" TARGET="MAIN"><code>Cudd_addDivide()</code></a>
 788 <dd> Integer and floating point division.
 789
 790 <dt> <a href="cuddAllDet.html#Cudd_addEvalConst" TARGET="MAIN"><code>Cudd_addEvalConst()</code></a>
 791 <dd> Checks whether ADD g is constant whenever ADD f is 1.
 792
 793 <dt> <a href="cuddAllDet.html#Cudd_addExistAbstract" TARGET="MAIN"><code>Cudd_addExistAbstract()</code></a>
 794 <dd> Existentially Abstracts all the variables in cube from f.
 795
 796 <dt> <a href="cuddAllDet.html#Cudd_addFindMax" TARGET="MAIN"><code>Cudd_addFindMax()</code></a>
 797 <dd> Finds the maximum discriminant of f.
 798
 799 <dt> <a href="cuddAllDet.html#Cudd_addFindMin" TARGET="MAIN"><code>Cudd_addFindMin()</code></a>
 800 <dd> Finds the minimum discriminant of f.
 801
 802 <dt> <a href="cuddAllDet.html#Cudd_addGeneralVectorCompose" TARGET="MAIN"><code>Cudd_addGeneralVectorCompose()</code></a>
 803 <dd> Composes an ADD with a vector of ADDs.
 804
 805 <dt> <a href="cuddAllDet.html#Cudd_addHamming" TARGET="MAIN"><code>Cudd_addHamming()</code></a>
 806 <dd> Computes the Hamming distance ADD.
 807
 808 <dt> <a href="cuddAllDet.html#Cudd_addHarwell" TARGET="MAIN"><code>Cudd_addHarwell()</code></a>
 809 <dd> Reads in a matrix in the format of the Harwell-Boeing
 810   benchmark suite.
 811
 812 <dt> <a href="cuddAllDet.html#Cudd_addIteConstant" TARGET="MAIN"><code>Cudd_addIteConstant()</code></a>
 813 <dd> Implements ITEconstant for ADDs.
 814
 815 <dt> <a href="cuddAllDet.html#Cudd_addIte" TARGET="MAIN"><code>Cudd_addIte()</code></a>
 816 <dd> Implements ITE(f,g,h).
 817
 818 <dt> <a href="cuddAllDet.html#Cudd_addIthBit" TARGET="MAIN"><code>Cudd_addIthBit()</code></a>
 819 <dd> Extracts the i-th bit from an ADD.
 820
 821 <dt> <a href="cuddAllDet.html#Cudd_addIthVar" TARGET="MAIN"><code>Cudd_addIthVar()</code></a>
 822 <dd> Returns the ADD variable with index i.
 823
 824 <dt> <a href="cuddAllDet.html#Cudd_addLeq" TARGET="MAIN"><code>Cudd_addLeq()</code></a>
 825 <dd> Determines whether f is less than or equal to g.
 826
 827 <dt> <a href="cuddAllDet.html#Cudd_addLog" TARGET="MAIN"><code>Cudd_addLog()</code></a>
 828 <dd> Natural logarithm of an ADD.
 829
 830 <dt> <a href="cuddAllDet.html#Cudd_addMatrixMultiply" TARGET="MAIN"><code>Cudd_addMatrixMultiply()</code></a>
 831 <dd> Calculates the product of two matrices represented as
 832   ADDs.
 833
 834 <dt> <a href="cuddAllDet.html#Cudd_addMaximum" TARGET="MAIN"><code>Cudd_addMaximum()</code></a>
 835 <dd> Integer and floating point max.
 836
 837 <dt> <a href="cuddAllDet.html#Cudd_addMinimum" TARGET="MAIN"><code>Cudd_addMinimum()</code></a>
 838 <dd> Integer and floating point min.
 839
 840 <dt> <a href="cuddAllDet.html#Cudd_addMinus" TARGET="MAIN"><code>Cudd_addMinus()</code></a>
 841 <dd> Integer and floating point subtraction.
 842
 843 <dt> <a href="cuddAllDet.html#Cudd_addMonadicApply" TARGET="MAIN"><code>Cudd_addMonadicApply()</code></a>
 844 <dd> Applies op to the discriminants of f.
 845
 846 <dt> <a href="cuddAllDet.html#Cudd_addNand" TARGET="MAIN"><code>Cudd_addNand()</code></a>
 847 <dd> NAND of two 0-1 ADDs.
 848
 849 <dt> <a href="cuddAllDet.html#Cudd_addNegate" TARGET="MAIN"><code>Cudd_addNegate()</code></a>
 850 <dd> Computes the additive inverse of an ADD.
 851
 852 <dt> <a href="cuddAllDet.html#Cudd_addNewVarAtLevel" TARGET="MAIN"><code>Cudd_addNewVarAtLevel()</code></a>
 853 <dd> Returns a new ADD variable at a specified level.
 854
 855 <dt> <a href="cuddAllDet.html#Cudd_addNewVar" TARGET="MAIN"><code>Cudd_addNewVar()</code></a>
 856 <dd> Returns a new ADD variable.
 857
 858 <dt> <a href="cuddAllDet.html#Cudd_addNonSimCompose" TARGET="MAIN"><code>Cudd_addNonSimCompose()</code></a>
 859 <dd> Composes an ADD with a vector of 0-1 ADDs.
 860
 861 <dt> <a href="cuddAllDet.html#Cudd_addNor" TARGET="MAIN"><code>Cudd_addNor()</code></a>
 862 <dd> NOR of two 0-1 ADDs.
 863
 864 <dt> <a href="cuddAllDet.html#Cudd_addOneZeroMaximum" TARGET="MAIN"><code>Cudd_addOneZeroMaximum()</code></a>
 865 <dd> Returns 1 if f &gt; g and 0 otherwise.
 866
 867 <dt> <a href="cuddAllDet.html#Cudd_addOrAbstract" TARGET="MAIN"><code>Cudd_addOrAbstract()</code></a>
 868 <dd> Disjunctively abstracts all the variables in cube from the
 869   0-1 ADD f.
 870
 871 <dt> <a href="cuddAllDet.html#Cudd_addOr" TARGET="MAIN"><code>Cudd_addOr()</code></a>
 872 <dd> Disjunction of two 0-1 ADDs.
 873
 874 <dt> <a href="cuddAllDet.html#Cudd_addOuterSum" TARGET="MAIN"><code>Cudd_addOuterSum()</code></a>
 875 <dd> Takes the minimum of a matrix and the outer sum of two vectors.
 876
 877 <dt> <a href="cuddAllDet.html#Cudd_addPermute" TARGET="MAIN"><code>Cudd_addPermute()</code></a>
 878 <dd> Permutes the variables of an ADD.
 879
 880 <dt> <a href="cuddAllDet.html#Cudd_addPlus" TARGET="MAIN"><code>Cudd_addPlus()</code></a>
 881 <dd> Integer and floating point addition.
 882
 883 <dt> <a href="cuddAllDet.html#Cudd_addRead" TARGET="MAIN"><code>Cudd_addRead()</code></a>
 884 <dd> Reads in a sparse matrix.
 885
 886 <dt> <a href="cuddAllDet.html#Cudd_addResidue" TARGET="MAIN"><code>Cudd_addResidue()</code></a>
 887 <dd> Builds an ADD for the residue modulo m of an n-bit
 888   number.
 889
 890 <dt> <a href="cuddAllDet.html#Cudd_addRestrict" TARGET="MAIN"><code>Cudd_addRestrict()</code></a>
 891 <dd> ADD restrict according to Coudert and Madre's algorithm
 892   (ICCAD90).
 893
 894 <dt> <a href="cuddAllDet.html#Cudd_addRoundOff" TARGET="MAIN"><code>Cudd_addRoundOff()</code></a>
 895 <dd> Rounds off the discriminants of an ADD.
 896
 897 <dt> <a href="cuddAllDet.html#Cudd_addScalarInverse" TARGET="MAIN"><code>Cudd_addScalarInverse()</code></a>
 898 <dd> Computes the scalar inverse of an ADD.
 899
 900 <dt> <a href="cuddAllDet.html#Cudd_addSetNZ" TARGET="MAIN"><code>Cudd_addSetNZ()</code></a>
 901 <dd> This operator sets f to the value of g wherever g != 0.
 902
 903 <dt> <a href="cuddAllDet.html#Cudd_addSwapVariables" TARGET="MAIN"><code>Cudd_addSwapVariables()</code></a>
 904 <dd> Swaps two sets of variables of the same size (x and y) in
 905   the ADD f.
 906
 907 <dt> <a href="cuddAllDet.html#Cudd_addThreshold" TARGET="MAIN"><code>Cudd_addThreshold()</code></a>
 908 <dd> f if f&gt;=g; 0 if f&lt;g.
 909
 910 <dt> <a href="cuddAllDet.html#Cudd_addTimesPlus" TARGET="MAIN"><code>Cudd_addTimesPlus()</code></a>
 911 <dd> Calculates the product of two matrices represented as
 912   ADDs.
 913
 914 <dt> <a href="cuddAllDet.html#Cudd_addTimes" TARGET="MAIN"><code>Cudd_addTimes()</code></a>
 915 <dd> Integer and floating point multiplication.
 916
 917 <dt> <a href="cuddAllDet.html#Cudd_addTriangle" TARGET="MAIN"><code>Cudd_addTriangle()</code></a>
 918 <dd> Performs the triangulation step for the shortest path
 919   computation.
 920
 921 <dt> <a href="cuddAllDet.html#Cudd_addUnivAbstract" TARGET="MAIN"><code>Cudd_addUnivAbstract()</code></a>
 922 <dd> Universally Abstracts all the variables in cube from f.
 923
 924 <dt> <a href="cuddAllDet.html#Cudd_addVectorCompose" TARGET="MAIN"><code>Cudd_addVectorCompose()</code></a>
 925 <dd> Composes an ADD with a vector of 0-1 ADDs.
 926
 927 <dt> <a href="cuddAllDet.html#Cudd_addWalsh" TARGET="MAIN"><code>Cudd_addWalsh()</code></a>
 928 <dd> Generates a Walsh matrix in ADD form.
 929
 930 <dt> <a href="cuddAllDet.html#Cudd_addXeqy" TARGET="MAIN"><code>Cudd_addXeqy()</code></a>
 931 <dd> Generates an ADD for the function x==y.
 932
 933 <dt> <a href="cuddAllDet.html#Cudd_addXnor" TARGET="MAIN"><code>Cudd_addXnor()</code></a>
 934 <dd> XNOR of two 0-1 ADDs.
 935
 936 <dt> <a href="cuddAllDet.html#Cudd_addXor" TARGET="MAIN"><code>Cudd_addXor()</code></a>
 937 <dd> XOR of two 0-1 ADDs.
 938
 939 <dt> <a href="cuddAllDet.html#Cudd_bddAdjPermuteX" TARGET="MAIN"><code>Cudd_bddAdjPermuteX()</code></a>
 940 <dd> Rearranges a set of variables in the BDD B.
 941
 942 <dt> <a href="cuddAllDet.html#Cudd_bddAndAbstractLimit" TARGET="MAIN"><code>Cudd_bddAndAbstractLimit()</code></a>
 943 <dd> Takes the AND of two BDDs and simultaneously abstracts the
 944   variables in cube.  Returns NULL if too many nodes are required.
 945
 946 <dt> <a href="cuddAllDet.html#Cudd_bddAndAbstract" TARGET="MAIN"><code>Cudd_bddAndAbstract()</code></a>
 947 <dd> Takes the AND of two BDDs and simultaneously abstracts the
 948   variables in cube.
 949
 950 <dt> <a href="cuddAllDet.html#Cudd_bddAndLimit" TARGET="MAIN"><code>Cudd_bddAndLimit()</code></a>
 951 <dd> Computes the conjunction of two BDDs f and g.  Returns
 952   NULL if too many nodes are required.
 953
 954 <dt> <a href="cuddAllDet.html#Cudd_bddAnd" TARGET="MAIN"><code>Cudd_bddAnd()</code></a>
 955 <dd> Computes the conjunction of two BDDs f and g.
 956
 957 <dt> <a href="cuddAllDet.html#Cudd_bddApproxConjDecomp" TARGET="MAIN"><code>Cudd_bddApproxConjDecomp()</code></a>
 958 <dd> Performs two-way conjunctive decomposition of a BDD.
 959
 960 <dt> <a href="cuddAllDet.html#Cudd_bddApproxDisjDecomp" TARGET="MAIN"><code>Cudd_bddApproxDisjDecomp()</code></a>
 961 <dd> Performs two-way disjunctive decomposition of a BDD.
 962
 963 <dt> <a href="cuddAllDet.html#Cudd_bddBindVar" TARGET="MAIN"><code>Cudd_bddBindVar()</code></a>
 964 <dd> Prevents sifting of a variable.
 965
 966 <dt> <a href="cuddAllDet.html#Cudd_bddBooleanDiff" TARGET="MAIN"><code>Cudd_bddBooleanDiff()</code></a>
 967 <dd> Computes the boolean difference of f with respect to x.
 968
 969 <dt> <a href="cuddAllDet.html#Cudd_bddCharToVect" TARGET="MAIN"><code>Cudd_bddCharToVect()</code></a>
 970 <dd> Computes a vector whose image equals a non-zero function.
 971
 972 <dt> <a href="cuddAllDet.html#Cudd_bddClippingAndAbstract" TARGET="MAIN"><code>Cudd_bddClippingAndAbstract()</code></a>
 973 <dd> Approximates the conjunction of two BDDs f and g and
 974   simultaneously abstracts the variables in cube.
 975
 976 <dt> <a href="cuddAllDet.html#Cudd_bddClippingAnd" TARGET="MAIN"><code>Cudd_bddClippingAnd()</code></a>
 977 <dd> Approximates the conjunction of two BDDs f and g.
 978
 979 <dt> <a href="cuddAllDet.html#Cudd_bddClosestCube" TARGET="MAIN"><code>Cudd_bddClosestCube()</code></a>
 980 <dd> Finds a cube of f at minimum Hamming distance from g.
 981
 982 <dt> <a href="cuddAllDet.html#Cudd_bddCompose" TARGET="MAIN"><code>Cudd_bddCompose()</code></a>
 983 <dd> Substitutes g for x_v in the BDD for f.
 984
 985 <dt> <a href="cuddAllDet.html#Cudd_bddComputeCube" TARGET="MAIN"><code>Cudd_bddComputeCube()</code></a>
 986 <dd> Computes the cube of an array of BDD variables.
 987
 988 <dt> <a href="cuddAllDet.html#Cudd_bddConstrainDecomp" TARGET="MAIN"><code>Cudd_bddConstrainDecomp()</code></a>
 989 <dd> BDD conjunctive decomposition as in McMillan's CAV96 paper.
 990
 991 <dt> <a href="cuddAllDet.html#Cudd_bddConstrain" TARGET="MAIN"><code>Cudd_bddConstrain()</code></a>
 992 <dd> Computes f constrain c.
 993
 994 <dt> <a href="cuddAllDet.html#Cudd_bddCorrelationWeights" TARGET="MAIN"><code>Cudd_bddCorrelationWeights()</code></a>
 995 <dd> Computes the correlation of f and g for given input
 996   probabilities.
 997
 998 <dt> <a href="cuddAllDet.html#Cudd_bddCorrelation" TARGET="MAIN"><code>Cudd_bddCorrelation()</code></a>
 999 <dd> Computes the correlation of f and g.
1000
1001 <dt> <a href="cuddAllDet.html#Cudd_bddExistAbstract" TARGET="MAIN"><code>Cudd_bddExistAbstract()</code></a>
1002 <dd> Existentially abstracts all the variables in cube from f.
1003
1004 <dt> <a href="cuddAllDet.html#Cudd_bddGenConjDecomp" TARGET="MAIN"><code>Cudd_bddGenConjDecomp()</code></a>
1005 <dd> Performs two-way conjunctive decomposition of a BDD.
1006
1007 <dt> <a href="cuddAllDet.html#Cudd_bddGenDisjDecomp" TARGET="MAIN"><code>Cudd_bddGenDisjDecomp()</code></a>
1008 <dd> Performs two-way disjunctive decomposition of a BDD.
1009
1010 <dt> <a href="cuddAllDet.html#Cudd_bddIntersect" TARGET="MAIN"><code>Cudd_bddIntersect()</code></a>
1011 <dd> Returns a function included in the intersection of f and g.
1012
1013 <dt> <a href="cuddAllDet.html#Cudd_bddInterval" TARGET="MAIN"><code>Cudd_bddInterval()</code></a>
1014 <dd> Generates a BDD for the function lowerB &le; x &le; upperB.
1015
1016 <dt> <a href="cuddAllDet.html#Cudd_bddIsNsVar" TARGET="MAIN"><code>Cudd_bddIsNsVar()</code></a>
1017 <dd> Checks whether a variable is next state.
1018
1019 <dt> <a href="cuddAllDet.html#Cudd_bddIsPiVar" TARGET="MAIN"><code>Cudd_bddIsPiVar()</code></a>
1020 <dd> Checks whether a variable is primary input.
1021
1022 <dt> <a href="cuddAllDet.html#Cudd_bddIsPsVar" TARGET="MAIN"><code>Cudd_bddIsPsVar()</code></a>
1023 <dd> Checks whether a variable is present state.
1024
1025 <dt> <a href="cuddAllDet.html#Cudd_bddIsVarEssential" TARGET="MAIN"><code>Cudd_bddIsVarEssential()</code></a>
1026 <dd> Determines whether a given variable is essential with a
1027   given phase in a BDD.
1028
1029 <dt> <a href="cuddAllDet.html#Cudd_bddIsVarHardGroup" TARGET="MAIN"><code>Cudd_bddIsVarHardGroup()</code></a>
1030 <dd> Checks whether a variable is set to be in a hard group.
1031
1032 <dt> <a href="cuddAllDet.html#Cudd_bddIsVarToBeGrouped" TARGET="MAIN"><code>Cudd_bddIsVarToBeGrouped()</code></a>
1033 <dd> Checks whether a variable is set to be grouped.
1034
1035 <dt> <a href="cuddAllDet.html#Cudd_bddIsVarToBeUngrouped" TARGET="MAIN"><code>Cudd_bddIsVarToBeUngrouped()</code></a>
1036 <dd> Checks whether a variable is set to be ungrouped.
1037
1038 <dt> <a href="cuddAllDet.html#Cudd_bddIsop" TARGET="MAIN"><code>Cudd_bddIsop()</code></a>
1039 <dd> Computes a BDD in the interval between L and U with a
1040   simple sum-of-produuct cover.
1041
1042 <dt> <a href="cuddAllDet.html#Cudd_bddIteConstant" TARGET="MAIN"><code>Cudd_bddIteConstant()</code></a>
1043 <dd> Implements ITEconstant(f,g,h).
1044
1045 <dt> <a href="cuddAllDet.html#Cudd_bddIterConjDecomp" TARGET="MAIN"><code>Cudd_bddIterConjDecomp()</code></a>
1046 <dd> Performs two-way conjunctive decomposition of a BDD.
1047
1048 <dt> <a href="cuddAllDet.html#Cudd_bddIterDisjDecomp" TARGET="MAIN"><code>Cudd_bddIterDisjDecomp()</code></a>
1049 <dd> Performs two-way disjunctive decomposition of a BDD.
1050
1051 <dt> <a href="cuddAllDet.html#Cudd_bddIte" TARGET="MAIN"><code>Cudd_bddIte()</code></a>
1052 <dd> Implements ITE(f,g,h).
1053
1054 <dt> <a href="cuddAllDet.html#Cudd_bddIthVar" TARGET="MAIN"><code>Cudd_bddIthVar()</code></a>
1055 <dd> Returns the BDD variable with index i.
1056
1057 <dt> <a href="cuddAllDet.html#Cudd_bddLICompaction" TARGET="MAIN"><code>Cudd_bddLICompaction()</code></a>
1058 <dd> Performs safe minimization of a BDD.
1059
1060 <dt> <a href="cuddAllDet.html#Cudd_bddLeqUnless" TARGET="MAIN"><code>Cudd_bddLeqUnless()</code></a>
1061 <dd> Tells whether f is less than of equal to G unless D is 1.
1062
1063 <dt> <a href="cuddAllDet.html#Cudd_bddLeq" TARGET="MAIN"><code>Cudd_bddLeq()</code></a>
1064 <dd> Determines whether f is less than or equal to g.
1065
1066 <dt> <a href="cuddAllDet.html#Cudd_bddLiteralSetIntersection" TARGET="MAIN"><code>Cudd_bddLiteralSetIntersection()</code></a>
1067 <dd> Computes the intesection of two sets of literals
1068   represented as BDDs.
1069
1070 <dt> <a href="cuddAllDet.html#Cudd_bddMakePrime" TARGET="MAIN"><code>Cudd_bddMakePrime()</code></a>
1071 <dd> Expands cube to a prime implicant of f.
1072
1073 <dt> <a href="cuddAllDet.html#Cudd_bddMinimize" TARGET="MAIN"><code>Cudd_bddMinimize()</code></a>
1074 <dd> Finds a small BDD that agrees with <code>f</code> over
1075   <code>c</code>.
1076
1077 <dt> <a href="cuddAllDet.html#Cudd_bddNPAnd" TARGET="MAIN"><code>Cudd_bddNPAnd()</code></a>
1078 <dd> Computes f non-polluting-and g.
1079
1080 <dt> <a href="cuddAllDet.html#Cudd_bddNand" TARGET="MAIN"><code>Cudd_bddNand()</code></a>
1081 <dd> Computes the NAND of two BDDs f and g.
1082
1083 <dt> <a href="cuddAllDet.html#Cudd_bddNewVarAtLevel" TARGET="MAIN"><code>Cudd_bddNewVarAtLevel()</code></a>
1084 <dd> Returns a new BDD variable at a specified level.
1085
1086 <dt> <a href="cuddAllDet.html#Cudd_bddNewVar" TARGET="MAIN"><code>Cudd_bddNewVar()</code></a>
1087 <dd> Returns a new BDD variable.
1088
1089 <dt> <a href="cuddAllDet.html#Cudd_bddNor" TARGET="MAIN"><code>Cudd_bddNor()</code></a>
1090 <dd> Computes the NOR of two BDDs f and g.
1091
1092 <dt> <a href="cuddAllDet.html#Cudd_bddOr" TARGET="MAIN"><code>Cudd_bddOr()</code></a>
1093 <dd> Computes the disjunction of two BDDs f and g.
1094
1095 <dt> <a href="cuddAllDet.html#Cudd_bddPermute" TARGET="MAIN"><code>Cudd_bddPermute()</code></a>
1096 <dd> Permutes the variables of a BDD.
1097
1098 <dt> <a href="cuddAllDet.html#Cudd_bddPickArbitraryMinterms" TARGET="MAIN"><code>Cudd_bddPickArbitraryMinterms()</code></a>
1099 <dd> Picks k on-set minterms evenly distributed from given DD.
1100
1101 <dt> <a href="cuddAllDet.html#Cudd_bddPickOneCube" TARGET="MAIN"><code>Cudd_bddPickOneCube()</code></a>
1102 <dd> Picks one on-set cube randomly from the given DD.
1103
1104 <dt> <a href="cuddAllDet.html#Cudd_bddPickOneMinterm" TARGET="MAIN"><code>Cudd_bddPickOneMinterm()</code></a>
1105 <dd> Picks one on-set minterm randomly from the given DD.
1106
1107 <dt> <a href="cuddAllDet.html#Cudd_bddPrintCover" TARGET="MAIN"><code>Cudd_bddPrintCover()</code></a>
1108 <dd> Prints a sum of prime implicants of a BDD.
1109
1110 <dt> <a href="cuddAllDet.html#Cudd_bddReadPairIndex" TARGET="MAIN"><code>Cudd_bddReadPairIndex()</code></a>
1111 <dd> Reads a corresponding pair index for a given index.
1112
1113 <dt> <a href="cuddAllDet.html#Cudd_bddRead" TARGET="MAIN"><code>Cudd_bddRead()</code></a>
1114 <dd> Reads in a graph (without labels) given as a list of arcs.
1115
1116 <dt> <a href="cuddAllDet.html#Cudd_bddRealignDisable" TARGET="MAIN"><code>Cudd_bddRealignDisable()</code></a>
1117 <dd> Disables realignment of ZDD order to BDD order.
1118
1119 <dt> <a href="cuddAllDet.html#Cudd_bddRealignEnable" TARGET="MAIN"><code>Cudd_bddRealignEnable()</code></a>
1120 <dd> Enables realignment of BDD order to ZDD order.
1121
1122 <dt> <a href="cuddAllDet.html#Cudd_bddRealignmentEnabled" TARGET="MAIN"><code>Cudd_bddRealignmentEnabled()</code></a>
1123 <dd> Tells whether the realignment of BDD order to ZDD order is
1124   enabled.
1125
1126 <dt> <a href="cuddAllDet.html#Cudd_bddResetVarToBeGrouped" TARGET="MAIN"><code>Cudd_bddResetVarToBeGrouped()</code></a>
1127 <dd> Resets a variable not to be grouped.
1128
1129 <dt> <a href="cuddAllDet.html#Cudd_bddRestrict" TARGET="MAIN"><code>Cudd_bddRestrict()</code></a>
1130 <dd> BDD restrict according to Coudert and Madre's algorithm
1131   (ICCAD90).
1132
1133 <dt> <a href="cuddAllDet.html#Cudd_bddSetNsVar" TARGET="MAIN"><code>Cudd_bddSetNsVar()</code></a>
1134 <dd> Sets a variable type to next state.
1135
1136 <dt> <a href="cuddAllDet.html#Cudd_bddSetPairIndex" TARGET="MAIN"><code>Cudd_bddSetPairIndex()</code></a>
1137 <dd> Sets a corresponding pair index for a given index.
1138
1139 <dt> <a href="cuddAllDet.html#Cudd_bddSetPiVar" TARGET="MAIN"><code>Cudd_bddSetPiVar()</code></a>
1140 <dd> Sets a variable type to primary input.
1141
1142 <dt> <a href="cuddAllDet.html#Cudd_bddSetPsVar" TARGET="MAIN"><code>Cudd_bddSetPsVar()</code></a>
1143 <dd> Sets a variable type to present state.
1144
1145 <dt> <a href="cuddAllDet.html#Cudd_bddSetVarHardGroup" TARGET="MAIN"><code>Cudd_bddSetVarHardGroup()</code></a>
1146 <dd> Sets a variable to be a hard group.
1147
1148 <dt> <a href="cuddAllDet.html#Cudd_bddSetVarToBeGrouped" TARGET="MAIN"><code>Cudd_bddSetVarToBeGrouped()</code></a>
1149 <dd> Sets a variable to be grouped.
1150
1151 <dt> <a href="cuddAllDet.html#Cudd_bddSetVarToBeUngrouped" TARGET="MAIN"><code>Cudd_bddSetVarToBeUngrouped()</code></a>
1152 <dd> Sets a variable to be ungrouped.
1153
1154 <dt> <a href="cuddAllDet.html#Cudd_bddSqueeze" TARGET="MAIN"><code>Cudd_bddSqueeze()</code></a>
1155 <dd> Finds a small BDD in a function interval.
1156
1157 <dt> <a href="cuddAllDet.html#Cudd_bddSwapVariables" TARGET="MAIN"><code>Cudd_bddSwapVariables()</code></a>
1158 <dd> Swaps two sets of variables of the same size (x and y) in
1159   the BDD f.
1160
1161 <dt> <a href="cuddAllDet.html#Cudd_bddTransfer" TARGET="MAIN"><code>Cudd_bddTransfer()</code></a>
1162 <dd> Convert a BDD from a manager to another one.
1163
1164 <dt> <a href="cuddAllDet.html#Cudd_bddUnbindVar" TARGET="MAIN"><code>Cudd_bddUnbindVar()</code></a>
1165 <dd> Allows the sifting of a variable.
1166
1167 <dt> <a href="cuddAllDet.html#Cudd_bddUnivAbstract" TARGET="MAIN"><code>Cudd_bddUnivAbstract()</code></a>
1168 <dd> Universally abstracts all the variables in cube from f.
1169
1170 <dt> <a href="cuddAllDet.html#Cudd_bddVarConjDecomp" TARGET="MAIN"><code>Cudd_bddVarConjDecomp()</code></a>
1171 <dd> Performs two-way conjunctive decomposition of a BDD.
1172
1173 <dt> <a href="cuddAllDet.html#Cudd_bddVarDisjDecomp" TARGET="MAIN"><code>Cudd_bddVarDisjDecomp()</code></a>
1174 <dd> Performs two-way disjunctive decomposition of a BDD.
1175
1176 <dt> <a href="cuddAllDet.html#Cudd_bddVarIsBound" TARGET="MAIN"><code>Cudd_bddVarIsBound()</code></a>
1177 <dd> Tells whether a variable can be sifted.
1178
1179 <dt> <a href="cuddAllDet.html#Cudd_bddVarIsDependent" TARGET="MAIN"><code>Cudd_bddVarIsDependent()</code></a>
1180 <dd> Checks whether a variable is dependent on others in a
1181   function.
1182
1183 <dt> <a href="cuddAllDet.html#Cudd_bddVarMap" TARGET="MAIN"><code>Cudd_bddVarMap()</code></a>
1184 <dd> Remaps the variables of a BDD using the default variable map.
1185
1186 <dt> <a href="cuddAllDet.html#Cudd_bddVectorCompose" TARGET="MAIN"><code>Cudd_bddVectorCompose()</code></a>
1187 <dd> Composes a BDD with a vector of BDDs.
1188
1189 <dt> <a href="cuddAllDet.html#Cudd_bddXnor" TARGET="MAIN"><code>Cudd_bddXnor()</code></a>
1190 <dd> Computes the exclusive NOR of two BDDs f and g.
1191
1192 <dt> <a href="cuddAllDet.html#Cudd_bddXorExistAbstract" TARGET="MAIN"><code>Cudd_bddXorExistAbstract()</code></a>
1193 <dd> Takes the exclusive OR of two BDDs and simultaneously abstracts the
1194   variables in cube.
1195
1196 <dt> <a href="cuddAllDet.html#Cudd_bddXor" TARGET="MAIN"><code>Cudd_bddXor()</code></a>
1197 <dd> Computes the exclusive OR of two BDDs f and g.
1198
1199 <dt> <a href="cuddAllDet.html#Cudd_tlcInfoFree" TARGET="MAIN"><code>Cudd_tlcInfoFree()</code></a>
1200 <dd> Frees a DdTlcInfo Structure.
1201
1202 <dt> <a href="cuddAllDet.html#Cudd_zddChange" TARGET="MAIN"><code>Cudd_zddChange()</code></a>
1203 <dd> Substitutes a variable with its complement in a ZDD.
1204
1205 <dt> <a href="cuddAllDet.html#Cudd_zddComplement" TARGET="MAIN"><code>Cudd_zddComplement()</code></a>
1206 <dd> Computes a complement cover for a ZDD node.
1207
1208 <dt> <a href="cuddAllDet.html#Cudd_zddCountDouble" TARGET="MAIN"><code>Cudd_zddCountDouble()</code></a>
1209 <dd> Counts the number of minterms of a ZDD.
1210
1211 <dt> <a href="cuddAllDet.html#Cudd_zddCountMinterm" TARGET="MAIN"><code>Cudd_zddCountMinterm()</code></a>
1212 <dd> Counts the number of minterms of a ZDD.
1213
1214 <dt> <a href="cuddAllDet.html#Cudd_zddCount" TARGET="MAIN"><code>Cudd_zddCount()</code></a>
1215 <dd> Counts the number of minterms in a ZDD.
1216
1217 <dt> <a href="cuddAllDet.html#Cudd_zddCoverPathToString" TARGET="MAIN"><code>Cudd_zddCoverPathToString()</code></a>
1218 <dd> Converts a path of a ZDD representing a cover to a string.
1219
1220 <dt> <a href="cuddAllDet.html#Cudd_zddDagSize" TARGET="MAIN"><code>Cudd_zddDagSize()</code></a>
1221 <dd> Counts the number of nodes in a ZDD.
1222
1223 <dt> <a href="cuddAllDet.html#Cudd_zddDiffConst" TARGET="MAIN"><code>Cudd_zddDiffConst()</code></a>
1224 <dd> Performs the inclusion test for ZDDs (P implies Q).
1225
1226 <dt> <a href="cuddAllDet.html#Cudd_zddDiff" TARGET="MAIN"><code>Cudd_zddDiff()</code></a>
1227 <dd> Computes the difference of two ZDDs.
1228
1229 <dt> <a href="cuddAllDet.html#Cudd_zddDivideF" TARGET="MAIN"><code>Cudd_zddDivideF()</code></a>
1230 <dd> Modified version of Cudd_zddDivide.
1231
1232 <dt> <a href="cuddAllDet.html#Cudd_zddDivide" TARGET="MAIN"><code>Cudd_zddDivide()</code></a>
1233 <dd> Computes the quotient of two unate covers.
1234
1235 <dt> <a href="cuddAllDet.html#Cudd_zddDumpDot" TARGET="MAIN"><code>Cudd_zddDumpDot()</code></a>
1236 <dd> Writes a dot file representing the argument ZDDs.
1237
1238 <dt> <a href="cuddAllDet.html#Cudd_zddFirstPath" TARGET="MAIN"><code>Cudd_zddFirstPath()</code></a>
1239 <dd> Finds the first path of a ZDD.
1240
1241 <dt> <a href="cuddAllDet.html#Cudd_zddIntersect" TARGET="MAIN"><code>Cudd_zddIntersect()</code></a>
1242 <dd> Computes the intersection of two ZDDs.
1243
1244 <dt> <a href="cuddAllDet.html#Cudd_zddIsop" TARGET="MAIN"><code>Cudd_zddIsop()</code></a>
1245 <dd> Computes an ISOP in ZDD form from BDDs.
1246
1247 <dt> <a href="cuddAllDet.html#Cudd_zddIte" TARGET="MAIN"><code>Cudd_zddIte()</code></a>
1248 <dd> Computes the ITE of three ZDDs.
1249
1250 <dt> <a href="cuddAllDet.html#Cudd_zddIthVar" TARGET="MAIN"><code>Cudd_zddIthVar()</code></a>
1251 <dd> Returns the ZDD variable with index i.
1252
1253 <dt> <a href="cuddAllDet.html#Cudd_zddNextPath" TARGET="MAIN"><code>Cudd_zddNextPath()</code></a>
1254 <dd> Generates the next path of a ZDD.
1255
1256 <dt> <a href="cuddAllDet.html#Cudd_zddPortFromBdd" TARGET="MAIN"><code>Cudd_zddPortFromBdd()</code></a>
1257 <dd> Converts a BDD into a ZDD.
1258
1259 <dt> <a href="cuddAllDet.html#Cudd_zddPortToBdd" TARGET="MAIN"><code>Cudd_zddPortToBdd()</code></a>
1260 <dd> Converts a ZDD into a BDD.
1261
1262 <dt> <a href="cuddAllDet.html#Cudd_zddPrintCover" TARGET="MAIN"><code>Cudd_zddPrintCover()</code></a>
1263 <dd> Prints a sum of products from a ZDD representing a cover.
1264
1265 <dt> <a href="cuddAllDet.html#Cudd_zddPrintDebug" TARGET="MAIN"><code>Cudd_zddPrintDebug()</code></a>
1266 <dd> Prints to the standard output a ZDD and its statistics.
1267
1268 <dt> <a href="cuddAllDet.html#Cudd_zddPrintMinterm" TARGET="MAIN"><code>Cudd_zddPrintMinterm()</code></a>
1269 <dd> Prints a disjoint sum of product form for a ZDD.
1270
1271 <dt> <a href="cuddAllDet.html#Cudd_zddPrintSubtable" TARGET="MAIN"><code>Cudd_zddPrintSubtable()</code></a>
1272 <dd> Prints the ZDD table.
1273
1274 <dt> <a href="cuddAllDet.html#Cudd_zddProduct" TARGET="MAIN"><code>Cudd_zddProduct()</code></a>
1275 <dd> Computes the product of two covers represented by ZDDs.
1276
1277 <dt> <a href="cuddAllDet.html#Cudd_zddReadNodeCount" TARGET="MAIN"><code>Cudd_zddReadNodeCount()</code></a>
1278 <dd> Reports the number of nodes in ZDDs.
1279
1280 <dt> <a href="cuddAllDet.html#Cudd_zddRealignDisable" TARGET="MAIN"><code>Cudd_zddRealignDisable()</code></a>
1281 <dd> Disables realignment of ZDD order to BDD order.
1282
1283 <dt> <a href="cuddAllDet.html#Cudd_zddRealignEnable" TARGET="MAIN"><code>Cudd_zddRealignEnable()</code></a>
1284 <dd> Enables realignment of ZDD order to BDD order.
1285
1286 <dt> <a href="cuddAllDet.html#Cudd_zddRealignmentEnabled" TARGET="MAIN"><code>Cudd_zddRealignmentEnabled()</code></a>
1287 <dd> Tells whether the realignment of ZDD order to BDD order is
1288   enabled.
1289
1290 <dt> <a href="cuddAllDet.html#Cudd_zddReduceHeap" TARGET="MAIN"><code>Cudd_zddReduceHeap()</code></a>
1291 <dd> Main dynamic reordering routine for ZDDs.
1292
1293 <dt> <a href="cuddAllDet.html#Cudd_zddShuffleHeap" TARGET="MAIN"><code>Cudd_zddShuffleHeap()</code></a>
1294 <dd> Reorders ZDD variables according to given permutation.
1295
1296 <dt> <a href="cuddAllDet.html#Cudd_zddSubset0" TARGET="MAIN"><code>Cudd_zddSubset0()</code></a>
1297 <dd> Computes the negative cofactor of a ZDD w.r.t. a variable.
1298
1299 <dt> <a href="cuddAllDet.html#Cudd_zddSubset1" TARGET="MAIN"><code>Cudd_zddSubset1()</code></a>
1300 <dd> Computes the positive cofactor of a ZDD w.r.t. a variable.
1301
1302 <dt> <a href="cuddAllDet.html#Cudd_zddSymmProfile" TARGET="MAIN"><code>Cudd_zddSymmProfile()</code></a>
1303 <dd> Prints statistics on symmetric ZDD variables.
1304
1305 <dt> <a href="cuddAllDet.html#Cudd_zddUnateProduct" TARGET="MAIN"><code>Cudd_zddUnateProduct()</code></a>
1306 <dd> Computes the product of two unate covers.
1307
1308 <dt> <a href="cuddAllDet.html#Cudd_zddUnion" TARGET="MAIN"><code>Cudd_zddUnion()</code></a>
1309 <dd> Computes the union of two ZDDs.
1310
1311 <dt> <a href="cuddAllDet.html#Cudd_zddVarsFromBddVars" TARGET="MAIN"><code>Cudd_zddVarsFromBddVars()</code></a>
1312 <dd> Creates one or more ZDD variables for each BDD variable.
1313
1314 <dt> <a href="cuddAllDet.html#Cudd_zddWeakDivF" TARGET="MAIN"><code>Cudd_zddWeakDivF()</code></a>
1315 <dd> Modified version of Cudd_zddWeakDiv.
1316
1317 <dt> <a href="cuddAllDet.html#Cudd_zddWeakDiv" TARGET="MAIN"><code>Cudd_zddWeakDiv()</code></a>
1318 <dd> Applies weak division to two covers.
1319
1320 </dl>
1321
1322 <hr>
1323
1324 Last updated on 20090220 23h06
1325 </body></html>