2 <head><title>cudd package abstract
</title></head>
6 <!-- Function Abstracts -->
9 <dt> <a href=
"cuddAllDet.html#Cudd_AddHook" TARGET=
"MAIN"><code>Cudd_AddHook()
</code></a>
10 <dd> Adds a function to a hook.
12 <dt> <a href=
"cuddAllDet.html#Cudd_ApaAdd" TARGET=
"MAIN"><code>Cudd_ApaAdd()
</code></a>
13 <dd> Adds two arbitrary precision integers.
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
19 <dt> <a href=
"cuddAllDet.html#Cudd_ApaCompare" TARGET=
"MAIN"><code>Cudd_ApaCompare()
</code></a>
20 <dd> Compares two arbitrary precision integers.
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.
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.
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.
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
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.
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.
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.
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.
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.
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.
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.
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.
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
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.
69 <dt> <a href=
"cuddAllDet.html#Cudd_ApaSubtract" TARGET=
"MAIN"><code>Cudd_ApaSubtract()
</code></a>
70 <dd> Subtracts two arbitrary precision integers.
72 <dt> <a href=
"cuddAllDet.html#Cudd_AutodynDisableZdd" TARGET=
"MAIN"><code>Cudd_AutodynDisableZdd()
</code></a>
73 <dd> Disables automatic dynamic reordering of ZDDs.
75 <dt> <a href=
"cuddAllDet.html#Cudd_AutodynDisable" TARGET=
"MAIN"><code>Cudd_AutodynDisable()
</code></a>
76 <dd> Disables automatic dynamic reordering.
78 <dt> <a href=
"cuddAllDet.html#Cudd_AutodynEnableZdd" TARGET=
"MAIN"><code>Cudd_AutodynEnableZdd()
</code></a>
79 <dd> Enables automatic dynamic reordering of ZDDs.
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.
84 <dt> <a href=
"cuddAllDet.html#Cudd_AverageDistance" TARGET=
"MAIN"><code>Cudd_AverageDistance()
</code></a>
85 <dd> Computes the average distance between adjacent nodes.
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.
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.
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.
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.
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.
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.
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
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.
114 <dt> <a href=
"cuddAllDet.html#Cudd_ClearErrorCode" TARGET=
"MAIN"><code>Cudd_ClearErrorCode()
</code></a>
115 <dd> Clear the error code of a manager.
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.
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.
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.
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.
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.
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.
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.
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.
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
146 <dt> <a href=
"cuddAllDet.html#Cudd_DebugCheck" TARGET=
"MAIN"><code>Cudd_DebugCheck()
</code></a>
147 <dd> Checks for inconsistencies in the DD heap.
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
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.
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.
159 <dt> <a href=
"cuddAllDet.html#Cudd_Deref" TARGET=
"MAIN"><code>Cudd_Deref()
</code></a>
160 <dd> Decreases the reference count of node.
162 <dt> <a href=
"cuddAllDet.html#Cudd_DisableGarbageCollection" TARGET=
"MAIN"><code>Cudd_DisableGarbageCollection()
</code></a>
163 <dd> Disables garbage collection.
165 <dt> <a href=
"cuddAllDet.html#Cudd_DisableReorderingReporting" TARGET=
"MAIN"><code>Cudd_DisableReorderingReporting()
</code></a>
166 <dd> Disables reporting of reordering stats.
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.
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.
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.
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.
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.
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.
186 <dt> <a href=
"cuddAllDet.html#Cudd_DumpFactoredForm" TARGET=
"MAIN"><code>Cudd_DumpFactoredForm()
</code></a>
187 <dd> Writes factored forms representing the argument BDDs.
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)
> d(x,z).
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)
> d(y,z).
195 <dt> <a href=
"cuddAllDet.html#Cudd_EnableGarbageCollection" TARGET=
"MAIN"><code>Cudd_EnableGarbageCollection()
</code></a>
196 <dd> Enables garbage collection.
198 <dt> <a href=
"cuddAllDet.html#Cudd_EnableReorderingReporting" TARGET=
"MAIN"><code>Cudd_EnableReorderingReporting()
</code></a>
199 <dd> Enables reporting of reordering stats.
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.
204 <dt> <a href=
"cuddAllDet.html#Cudd_EqualSupNorm" TARGET=
"MAIN"><code>Cudd_EqualSupNorm()
</code></a>
205 <dd> Compares two ADDs for equality within tolerance.
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.
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.
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.
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.
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
223 <dt> <a href=
"cuddAllDet.html#Cudd_FindEssential" TARGET=
"MAIN"><code>Cudd_FindEssential()
</code></a>
224 <dd> Finds the essential variables of a DD.
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.
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.
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.
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.
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.
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.
244 <dt> <a href=
"cuddAllDet.html#Cudd_GarbageCollectionEnabled" TARGET=
"MAIN"><code>Cudd_GarbageCollectionEnabled()
</code></a>
245 <dd> Tells whether garbage collection is enabled.
247 <dt> <a href=
"cuddAllDet.html#Cudd_GenFree" TARGET=
"MAIN"><code>Cudd_GenFree()
</code></a>
248 <dd> Frees a CUDD generator.
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
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.
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
≥ c.
260 <dt> <a href=
"cuddAllDet.html#Cudd_Init" TARGET=
"MAIN"><code>Cudd_Init()
</code></a>
261 <dd> Creates a new DD manager.
263 <dt> <a href=
"cuddAllDet.html#Cudd_IsGenEmpty" TARGET=
"MAIN"><code>Cudd_IsGenEmpty()
</code></a>
264 <dd> Queries the status of a generator.
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.
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.
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.
275 <dt> <a href=
"cuddAllDet.html#Cudd_LargestCube" TARGET=
"MAIN"><code>Cudd_LargestCube()
</code></a>
276 <dd> Finds a largest cube in a DD.
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.
281 <dt> <a href=
"cuddAllDet.html#Cudd_MakeTreeNode" TARGET=
"MAIN"><code>Cudd_MakeTreeNode()
</code></a>
282 <dd> Creates a new variable group.
284 <dt> <a href=
"cuddAllDet.html#Cudd_MakeZddTreeNode" TARGET=
"MAIN"><code>Cudd_MakeZddTreeNode()
</code></a>
285 <dd> Creates a new ZDD variable group.
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.
290 <dt> <a href=
"cuddAllDet.html#Cudd_NewApaNumber" TARGET=
"MAIN"><code>Cudd_NewApaNumber()
</code></a>
291 <dd> Allocates memory for an arbitrary precision integer.
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.
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.
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.
302 <dt> <a href=
"cuddAllDet.html#Cudd_NodeReadIndex" TARGET=
"MAIN"><code>Cudd_NodeReadIndex()
</code></a>
303 <dd> Returns the index of the node.
305 <dt> <a href=
"cuddAllDet.html#Cudd_OutOfMem" TARGET=
"MAIN"><code>Cudd_OutOfMem()
</code></a>
306 <dd> Warns that a memory allocation failed.
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.
312 <dt> <a href=
"cuddAllDet.html#Cudd_Prime" TARGET=
"MAIN"><code>Cudd_Prime()
</code></a>
313 <dd> Returns the next prime
>= p.
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.
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.
321 <dt> <a href=
"cuddAllDet.html#Cudd_PrintLinear" TARGET=
"MAIN"><code>Cudd_PrintLinear()
</code></a>
322 <dd> Prints the linear transform matrix.
324 <dt> <a href=
"cuddAllDet.html#Cudd_PrintMinterm" TARGET=
"MAIN"><code>Cudd_PrintMinterm()
</code></a>
325 <dd> Prints a disjoint sum of products.
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.
330 <dt> <a href=
"cuddAllDet.html#Cudd_PrintVersion" TARGET=
"MAIN"><code>Cudd_PrintVersion()
</code></a>
331 <dd> Prints the package version number.
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.
336 <dt> <a href=
"cuddAllDet.html#Cudd_Quit" TARGET=
"MAIN"><code>Cudd_Quit()
</code></a>
337 <dd> Deletes resources associated with a DD manager.
339 <dt> <a href=
"cuddAllDet.html#Cudd_Random" TARGET=
"MAIN"><code>Cudd_Random()
</code></a>
340 <dd> Portable random number generator.
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
346 <dt> <a href=
"cuddAllDet.html#Cudd_ReadBackground" TARGET=
"MAIN"><code>Cudd_ReadBackground()
</code></a>
347 <dd> Reads the background constant of the manager.
349 <dt> <a href=
"cuddAllDet.html#Cudd_ReadCacheHits" TARGET=
"MAIN"><code>Cudd_ReadCacheHits()
</code></a>
350 <dd> Returns the number of cache hits.
352 <dt> <a href=
"cuddAllDet.html#Cudd_ReadCacheLookUps" TARGET=
"MAIN"><code>Cudd_ReadCacheLookUps()
</code></a>
353 <dd> Returns the number of cache look-ups.
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.
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.
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.
364 <dt> <a href=
"cuddAllDet.html#Cudd_ReadEpsilon" TARGET=
"MAIN"><code>Cudd_ReadEpsilon()
</code></a>
365 <dd> Reads the epsilon parameter of the manager.
367 <dt> <a href=
"cuddAllDet.html#Cudd_ReadErrorCode" TARGET=
"MAIN"><code>Cudd_ReadErrorCode()
</code></a>
368 <dd> Returns the code of the last error.
370 <dt> <a href=
"cuddAllDet.html#Cudd_ReadGarbageCollectionTime" TARGET=
"MAIN"><code>Cudd_ReadGarbageCollectionTime()
</code></a>
371 <dd> Returns the time spent in garbage collection.
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.
376 <dt> <a href=
"cuddAllDet.html#Cudd_ReadGroupcheck" TARGET=
"MAIN"><code>Cudd_ReadGroupcheck()
</code></a>
377 <dd> Reads the groupcheck parameter of the manager.
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.
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.
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.
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.
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.
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.
399 <dt> <a href=
"cuddAllDet.html#Cudd_ReadLooseUpTo" TARGET=
"MAIN"><code>Cudd_ReadLooseUpTo()
</code></a>
400 <dd> Reads the looseUpTo parameter of the manager.
402 <dt> <a href=
"cuddAllDet.html#Cudd_ReadMaxCacheHard" TARGET=
"MAIN"><code>Cudd_ReadMaxCacheHard()
</code></a>
403 <dd> Reads the maxCacheHard parameter of the manager.
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.
408 <dt> <a href=
"cuddAllDet.html#Cudd_ReadMaxGrowthAlternate" TARGET=
"MAIN"><code>Cudd_ReadMaxGrowthAlternate()
</code></a>
409 <dd> Reads the maxGrowthAlt parameter of the manager.
411 <dt> <a href=
"cuddAllDet.html#Cudd_ReadMaxGrowth" TARGET=
"MAIN"><code>Cudd_ReadMaxGrowth()
</code></a>
412 <dd> Reads the maxGrowth parameter of the manager.
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.
417 <dt> <a href=
"cuddAllDet.html#Cudd_ReadMaxMemory" TARGET=
"MAIN"><code>Cudd_ReadMaxMemory()
</code></a>
418 <dd> Reads the maximum allowed memory.
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.
423 <dt> <a href=
"cuddAllDet.html#Cudd_ReadMinDead" TARGET=
"MAIN"><code>Cudd_ReadMinDead()
</code></a>
424 <dd> Reads the minDead parameter of the manager.
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
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.
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.
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.
439 <dt> <a href=
"cuddAllDet.html#Cudd_ReadNodesDropped" TARGET=
"MAIN"><code>Cudd_ReadNodesDropped()
</code></a>
440 <dd> Returns the number of nodes dropped.
442 <dt> <a href=
"cuddAllDet.html#Cudd_ReadNodesFreed" TARGET=
"MAIN"><code>Cudd_ReadNodesFreed()
</code></a>
443 <dd> Returns the number of nodes freed.
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.
449 <dt> <a href=
"cuddAllDet.html#Cudd_ReadOne" TARGET=
"MAIN"><code>Cudd_ReadOne()
</code></a>
450 <dd> Returns the one constant of the manager.
452 <dt> <a href=
"cuddAllDet.html#Cudd_ReadPeakLiveNodeCount" TARGET=
"MAIN"><code>Cudd_ReadPeakLiveNodeCount()
</code></a>
453 <dd> Reports the peak number of live nodes.
455 <dt> <a href=
"cuddAllDet.html#Cudd_ReadPeakNodeCount" TARGET=
"MAIN"><code>Cudd_ReadPeakNodeCount()
</code></a>
456 <dd> Reports the peak number of nodes.
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
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
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.
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.
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
477 <dt> <a href=
"cuddAllDet.html#Cudd_ReadRecursiveCalls" TARGET=
"MAIN"><code>Cudd_ReadRecursiveCalls()
</code></a>
478 <dd> Returns the number of recursive calls.
480 <dt> <a href=
"cuddAllDet.html#Cudd_ReadReorderingCycle" TARGET=
"MAIN"><code>Cudd_ReadReorderingCycle()
</code></a>
481 <dd> Reads the reordCycle parameter of the manager.
483 <dt> <a href=
"cuddAllDet.html#Cudd_ReadReorderingTime" TARGET=
"MAIN"><code>Cudd_ReadReorderingTime()
</code></a>
484 <dd> Returns the time spent in reordering.
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.
489 <dt> <a href=
"cuddAllDet.html#Cudd_ReadSiftMaxSwap" TARGET=
"MAIN"><code>Cudd_ReadSiftMaxSwap()
</code></a>
490 <dd> Reads the siftMaxSwap parameter of the manager.
492 <dt> <a href=
"cuddAllDet.html#Cudd_ReadSiftMaxVar" TARGET=
"MAIN"><code>Cudd_ReadSiftMaxVar()
</code></a>
493 <dd> Reads the siftMaxVar parameter of the manager.
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.
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.
501 <dt> <a href=
"cuddAllDet.html#Cudd_ReadStderr" TARGET=
"MAIN"><code>Cudd_ReadStderr()
</code></a>
502 <dd> Reads the stderr of a manager.
504 <dt> <a href=
"cuddAllDet.html#Cudd_ReadStdout" TARGET=
"MAIN"><code>Cudd_ReadStdout()
</code></a>
505 <dd> Reads the stdout of a manager.
507 <dt> <a href=
"cuddAllDet.html#Cudd_ReadSwapSteps" TARGET=
"MAIN"><code>Cudd_ReadSwapSteps()
</code></a>
508 <dd> Reads the number of elementary reordering steps.
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
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.
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.
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.
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.
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.
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.
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.
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.
538 <dt> <a href=
"cuddAllDet.html#Cudd_ReadZero" TARGET=
"MAIN"><code>Cudd_ReadZero()
</code></a>
539 <dd> Returns the zero constant of the manager.
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.
544 <dt> <a href=
"cuddAllDet.html#Cudd_RecursiveDeref" TARGET=
"MAIN"><code>Cudd_RecursiveDeref()
</code></a>
545 <dd> Decreases the reference count of node n.
547 <dt> <a href=
"cuddAllDet.html#Cudd_ReduceHeap" TARGET=
"MAIN"><code>Cudd_ReduceHeap()
</code></a>
548 <dd> Main dynamic reordering routine.
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
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.
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.
562 <dt> <a href=
"cuddAllDet.html#Cudd_RemoveHook" TARGET=
"MAIN"><code>Cudd_RemoveHook()
</code></a>
563 <dd> Removes a function from a hook.
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.
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.
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
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
579 <dt> <a href=
"cuddAllDet.html#Cudd_SetBackground" TARGET=
"MAIN"><code>Cudd_SetBackground()
</code></a>
580 <dd> Sets the background constant of the manager.
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.
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.
588 <dt> <a href=
"cuddAllDet.html#Cudd_SetLooseUpTo" TARGET=
"MAIN"><code>Cudd_SetLooseUpTo()
</code></a>
589 <dd> Sets the looseUpTo parameter of the manager.
591 <dt> <a href=
"cuddAllDet.html#Cudd_SetMaxCacheHard" TARGET=
"MAIN"><code>Cudd_SetMaxCacheHard()
</code></a>
592 <dd> Sets the maxCacheHard parameter of the manager.
594 <dt> <a href=
"cuddAllDet.html#Cudd_SetMaxGrowthAlternate" TARGET=
"MAIN"><code>Cudd_SetMaxGrowthAlternate()
</code></a>
595 <dd> Sets the maxGrowthAlt parameter of the manager.
597 <dt> <a href=
"cuddAllDet.html#Cudd_SetMaxGrowth" TARGET=
"MAIN"><code>Cudd_SetMaxGrowth()
</code></a>
598 <dd> Sets the maxGrowth parameter of the manager.
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.
603 <dt> <a href=
"cuddAllDet.html#Cudd_SetMaxMemory" TARGET=
"MAIN"><code>Cudd_SetMaxMemory()
</code></a>
604 <dd> Sets the maximum allowed memory.
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
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.
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.
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.
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
625 <dt> <a href=
"cuddAllDet.html#Cudd_SetReorderingCycle" TARGET=
"MAIN"><code>Cudd_SetReorderingCycle()
</code></a>
626 <dd> Sets the reordCycle parameter of the manager.
628 <dt> <a href=
"cuddAllDet.html#Cudd_SetSiftMaxSwap" TARGET=
"MAIN"><code>Cudd_SetSiftMaxSwap()
</code></a>
629 <dd> Sets the siftMaxSwap parameter of the manager.
631 <dt> <a href=
"cuddAllDet.html#Cudd_SetSiftMaxVar" TARGET=
"MAIN"><code>Cudd_SetSiftMaxVar()
</code></a>
632 <dd> Sets the siftMaxVar parameter of the manager.
634 <dt> <a href=
"cuddAllDet.html#Cudd_SetStderr" TARGET=
"MAIN"><code>Cudd_SetStderr()
</code></a>
635 <dd> Sets the stderr of a manager.
637 <dt> <a href=
"cuddAllDet.html#Cudd_SetStdout" TARGET=
"MAIN"><code>Cudd_SetStdout()
</code></a>
638 <dd> Sets the stdout of a manager.
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
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.
647 <dt> <a href=
"cuddAllDet.html#Cudd_SetVarMap" TARGET=
"MAIN"><code>Cudd_SetVarMap()
</code></a>
648 <dd> Registers a variable mapping with the manager.
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.
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.
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.
659 <dt> <a href=
"cuddAllDet.html#Cudd_ShortestPath" TARGET=
"MAIN"><code>Cudd_ShortestPath()
</code></a>
660 <dd> Finds a shortest path in a DD.
662 <dt> <a href=
"cuddAllDet.html#Cudd_ShuffleHeap" TARGET=
"MAIN"><code>Cudd_ShuffleHeap()
</code></a>
663 <dd> Reorders variables according to given permutation.
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.
668 <dt> <a href=
"cuddAllDet.html#Cudd_SplitSet" TARGET=
"MAIN"><code>Cudd_SplitSet()
</code></a>
669 <dd> Returns m minterms from a BDD.
671 <dt> <a href=
"cuddAllDet.html#Cudd_Srandom" TARGET=
"MAIN"><code>Cudd_Srandom()
</code></a>
672 <dd> Initializer for the portable random number generator.
674 <dt> <a href=
"cuddAllDet.html#Cudd_StdPostReordHook" TARGET=
"MAIN"><code>Cudd_StdPostReordHook()
</code></a>
675 <dd> Sample hook function to call after reordering.
677 <dt> <a href=
"cuddAllDet.html#Cudd_StdPreReordHook" TARGET=
"MAIN"><code>Cudd_StdPreReordHook()
</code></a>
678 <dd> Sample hook function to call before reordering.
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>.
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
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
691 <dt> <a href=
"cuddAllDet.html#Cudd_SubsetWithMaskVars" TARGET=
"MAIN"><code>Cudd_SubsetWithMaskVars()
</code></a>
692 <dd> Extracts a subset from a BDD.
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>.
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
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
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.
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.
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.
714 <dt> <a href=
"cuddAllDet.html#Cudd_SymmProfile" TARGET=
"MAIN"><code>Cudd_SymmProfile()
</code></a>
715 <dd> Prints statistics on symmetric variables.
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
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
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.
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.
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.
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.
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.
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.
744 <dt> <a href=
"cuddAllDet.html#Cudd_Xgty" TARGET=
"MAIN"><code>Cudd_Xgty()
</code></a>
745 <dd> Generates a BDD for the function x
> y.
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.
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.
753 <dt> <a href=
"cuddAllDet.html#Cudd_addBddInterval" TARGET=
"MAIN"><code>Cudd_addBddInterval()
</code></a>
754 <dd> Converts an ADD to a BDD.
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
760 <dt> <a href=
"cuddAllDet.html#Cudd_addBddPattern" TARGET=
"MAIN"><code>Cudd_addBddPattern()
</code></a>
761 <dd> Converts an ADD to a BDD.
763 <dt> <a href=
"cuddAllDet.html#Cudd_addBddStrictThreshold" TARGET=
"MAIN"><code>Cudd_addBddStrictThreshold()
</code></a>
764 <dd> Converts an ADD to a BDD.
766 <dt> <a href=
"cuddAllDet.html#Cudd_addBddThreshold" TARGET=
"MAIN"><code>Cudd_addBddThreshold()
</code></a>
767 <dd> Converts an ADD to a BDD.
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.
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.
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.
778 <dt> <a href=
"cuddAllDet.html#Cudd_addConstrain" TARGET=
"MAIN"><code>Cudd_addConstrain()
</code></a>
779 <dd> Computes f constrain c for ADDs.
781 <dt> <a href=
"cuddAllDet.html#Cudd_addConst" TARGET=
"MAIN"><code>Cudd_addConst()
</code></a>
782 <dd> Returns the ADD for constant c.
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.
787 <dt> <a href=
"cuddAllDet.html#Cudd_addDivide" TARGET=
"MAIN"><code>Cudd_addDivide()
</code></a>
788 <dd> Integer and floating point division.
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.
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.
796 <dt> <a href=
"cuddAllDet.html#Cudd_addFindMax" TARGET=
"MAIN"><code>Cudd_addFindMax()
</code></a>
797 <dd> Finds the maximum discriminant of f.
799 <dt> <a href=
"cuddAllDet.html#Cudd_addFindMin" TARGET=
"MAIN"><code>Cudd_addFindMin()
</code></a>
800 <dd> Finds the minimum discriminant of f.
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.
805 <dt> <a href=
"cuddAllDet.html#Cudd_addHamming" TARGET=
"MAIN"><code>Cudd_addHamming()
</code></a>
806 <dd> Computes the Hamming distance ADD.
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
812 <dt> <a href=
"cuddAllDet.html#Cudd_addIteConstant" TARGET=
"MAIN"><code>Cudd_addIteConstant()
</code></a>
813 <dd> Implements ITEconstant for ADDs.
815 <dt> <a href=
"cuddAllDet.html#Cudd_addIte" TARGET=
"MAIN"><code>Cudd_addIte()
</code></a>
816 <dd> Implements ITE(f,g,h).
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.
821 <dt> <a href=
"cuddAllDet.html#Cudd_addIthVar" TARGET=
"MAIN"><code>Cudd_addIthVar()
</code></a>
822 <dd> Returns the ADD variable with index i.
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.
827 <dt> <a href=
"cuddAllDet.html#Cudd_addLog" TARGET=
"MAIN"><code>Cudd_addLog()
</code></a>
828 <dd> Natural logarithm of an ADD.
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
834 <dt> <a href=
"cuddAllDet.html#Cudd_addMaximum" TARGET=
"MAIN"><code>Cudd_addMaximum()
</code></a>
835 <dd> Integer and floating point max.
837 <dt> <a href=
"cuddAllDet.html#Cudd_addMinimum" TARGET=
"MAIN"><code>Cudd_addMinimum()
</code></a>
838 <dd> Integer and floating point min.
840 <dt> <a href=
"cuddAllDet.html#Cudd_addMinus" TARGET=
"MAIN"><code>Cudd_addMinus()
</code></a>
841 <dd> Integer and floating point subtraction.
843 <dt> <a href=
"cuddAllDet.html#Cudd_addMonadicApply" TARGET=
"MAIN"><code>Cudd_addMonadicApply()
</code></a>
844 <dd> Applies op to the discriminants of f.
846 <dt> <a href=
"cuddAllDet.html#Cudd_addNand" TARGET=
"MAIN"><code>Cudd_addNand()
</code></a>
847 <dd> NAND of two
0-
1 ADDs.
849 <dt> <a href=
"cuddAllDet.html#Cudd_addNegate" TARGET=
"MAIN"><code>Cudd_addNegate()
</code></a>
850 <dd> Computes the additive inverse of an ADD.
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.
855 <dt> <a href=
"cuddAllDet.html#Cudd_addNewVar" TARGET=
"MAIN"><code>Cudd_addNewVar()
</code></a>
856 <dd> Returns a new ADD variable.
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.
861 <dt> <a href=
"cuddAllDet.html#Cudd_addNor" TARGET=
"MAIN"><code>Cudd_addNor()
</code></a>
862 <dd> NOR of two
0-
1 ADDs.
864 <dt> <a href=
"cuddAllDet.html#Cudd_addOneZeroMaximum" TARGET=
"MAIN"><code>Cudd_addOneZeroMaximum()
</code></a>
865 <dd> Returns
1 if f
> g and
0 otherwise.
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
871 <dt> <a href=
"cuddAllDet.html#Cudd_addOr" TARGET=
"MAIN"><code>Cudd_addOr()
</code></a>
872 <dd> Disjunction of two
0-
1 ADDs.
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.
877 <dt> <a href=
"cuddAllDet.html#Cudd_addPermute" TARGET=
"MAIN"><code>Cudd_addPermute()
</code></a>
878 <dd> Permutes the variables of an ADD.
880 <dt> <a href=
"cuddAllDet.html#Cudd_addPlus" TARGET=
"MAIN"><code>Cudd_addPlus()
</code></a>
881 <dd> Integer and floating point addition.
883 <dt> <a href=
"cuddAllDet.html#Cudd_addRead" TARGET=
"MAIN"><code>Cudd_addRead()
</code></a>
884 <dd> Reads in a sparse matrix.
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
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
894 <dt> <a href=
"cuddAllDet.html#Cudd_addRoundOff" TARGET=
"MAIN"><code>Cudd_addRoundOff()
</code></a>
895 <dd> Rounds off the discriminants of an ADD.
897 <dt> <a href=
"cuddAllDet.html#Cudd_addScalarInverse" TARGET=
"MAIN"><code>Cudd_addScalarInverse()
</code></a>
898 <dd> Computes the scalar inverse of an ADD.
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.
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
907 <dt> <a href=
"cuddAllDet.html#Cudd_addThreshold" TARGET=
"MAIN"><code>Cudd_addThreshold()
</code></a>
908 <dd> f if f
>=g;
0 if f
<g.
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
914 <dt> <a href=
"cuddAllDet.html#Cudd_addTimes" TARGET=
"MAIN"><code>Cudd_addTimes()
</code></a>
915 <dd> Integer and floating point multiplication.
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
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.
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.
927 <dt> <a href=
"cuddAllDet.html#Cudd_addWalsh" TARGET=
"MAIN"><code>Cudd_addWalsh()
</code></a>
928 <dd> Generates a Walsh matrix in ADD form.
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.
933 <dt> <a href=
"cuddAllDet.html#Cudd_addXnor" TARGET=
"MAIN"><code>Cudd_addXnor()
</code></a>
934 <dd> XNOR of two
0-
1 ADDs.
936 <dt> <a href=
"cuddAllDet.html#Cudd_addXor" TARGET=
"MAIN"><code>Cudd_addXor()
</code></a>
937 <dd> XOR of two
0-
1 ADDs.
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.
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.
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
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.
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.
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.
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.
963 <dt> <a href=
"cuddAllDet.html#Cudd_bddBindVar" TARGET=
"MAIN"><code>Cudd_bddBindVar()
</code></a>
964 <dd> Prevents sifting of a variable.
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.
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.
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.
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.
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.
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.
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.
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.
991 <dt> <a href=
"cuddAllDet.html#Cudd_bddConstrain" TARGET=
"MAIN"><code>Cudd_bddConstrain()
</code></a>
992 <dd> Computes f constrain c.
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
998 <dt> <a href=
"cuddAllDet.html#Cudd_bddCorrelation" TARGET=
"MAIN"><code>Cudd_bddCorrelation()
</code></a>
999 <dd> Computes the correlation of f and g.
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.
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.
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.
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.
1013 <dt> <a href=
"cuddAllDet.html#Cudd_bddInterval" TARGET=
"MAIN"><code>Cudd_bddInterval()
</code></a>
1014 <dd> Generates a BDD for the function lowerB
≤ x
≤ upperB.
1016 <dt> <a href=
"cuddAllDet.html#Cudd_bddIsNsVar" TARGET=
"MAIN"><code>Cudd_bddIsNsVar()
</code></a>
1017 <dd> Checks whether a variable is next state.
1019 <dt> <a href=
"cuddAllDet.html#Cudd_bddIsPiVar" TARGET=
"MAIN"><code>Cudd_bddIsPiVar()
</code></a>
1020 <dd> Checks whether a variable is primary input.
1022 <dt> <a href=
"cuddAllDet.html#Cudd_bddIsPsVar" TARGET=
"MAIN"><code>Cudd_bddIsPsVar()
</code></a>
1023 <dd> Checks whether a variable is present state.
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.
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.
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.
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.
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.
1042 <dt> <a href=
"cuddAllDet.html#Cudd_bddIteConstant" TARGET=
"MAIN"><code>Cudd_bddIteConstant()
</code></a>
1043 <dd> Implements ITEconstant(f,g,h).
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.
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.
1051 <dt> <a href=
"cuddAllDet.html#Cudd_bddIte" TARGET=
"MAIN"><code>Cudd_bddIte()
</code></a>
1052 <dd> Implements ITE(f,g,h).
1054 <dt> <a href=
"cuddAllDet.html#Cudd_bddIthVar" TARGET=
"MAIN"><code>Cudd_bddIthVar()
</code></a>
1055 <dd> Returns the BDD variable with index i.
1057 <dt> <a href=
"cuddAllDet.html#Cudd_bddLICompaction" TARGET=
"MAIN"><code>Cudd_bddLICompaction()
</code></a>
1058 <dd> Performs safe minimization of a BDD.
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.
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.
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.
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.
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
1077 <dt> <a href=
"cuddAllDet.html#Cudd_bddNPAnd" TARGET=
"MAIN"><code>Cudd_bddNPAnd()
</code></a>
1078 <dd> Computes f non-polluting-and g.
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.
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.
1086 <dt> <a href=
"cuddAllDet.html#Cudd_bddNewVar" TARGET=
"MAIN"><code>Cudd_bddNewVar()
</code></a>
1087 <dd> Returns a new BDD variable.
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.
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.
1095 <dt> <a href=
"cuddAllDet.html#Cudd_bddPermute" TARGET=
"MAIN"><code>Cudd_bddPermute()
</code></a>
1096 <dd> Permutes the variables of a BDD.
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.
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.
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.
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.
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.
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.
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.
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.
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
1126 <dt> <a href=
"cuddAllDet.html#Cudd_bddResetVarToBeGrouped" TARGET=
"MAIN"><code>Cudd_bddResetVarToBeGrouped()
</code></a>
1127 <dd> Resets a variable not to be grouped.
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
1133 <dt> <a href=
"cuddAllDet.html#Cudd_bddSetNsVar" TARGET=
"MAIN"><code>Cudd_bddSetNsVar()
</code></a>
1134 <dd> Sets a variable type to next state.
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.
1139 <dt> <a href=
"cuddAllDet.html#Cudd_bddSetPiVar" TARGET=
"MAIN"><code>Cudd_bddSetPiVar()
</code></a>
1140 <dd> Sets a variable type to primary input.
1142 <dt> <a href=
"cuddAllDet.html#Cudd_bddSetPsVar" TARGET=
"MAIN"><code>Cudd_bddSetPsVar()
</code></a>
1143 <dd> Sets a variable type to present state.
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.
1148 <dt> <a href=
"cuddAllDet.html#Cudd_bddSetVarToBeGrouped" TARGET=
"MAIN"><code>Cudd_bddSetVarToBeGrouped()
</code></a>
1149 <dd> Sets a variable to be grouped.
1151 <dt> <a href=
"cuddAllDet.html#Cudd_bddSetVarToBeUngrouped" TARGET=
"MAIN"><code>Cudd_bddSetVarToBeUngrouped()
</code></a>
1152 <dd> Sets a variable to be ungrouped.
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.
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
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.
1164 <dt> <a href=
"cuddAllDet.html#Cudd_bddUnbindVar" TARGET=
"MAIN"><code>Cudd_bddUnbindVar()
</code></a>
1165 <dd> Allows the sifting of a variable.
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.
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.
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.
1176 <dt> <a href=
"cuddAllDet.html#Cudd_bddVarIsBound" TARGET=
"MAIN"><code>Cudd_bddVarIsBound()
</code></a>
1177 <dd> Tells whether a variable can be sifted.
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
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.
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.
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.
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
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.
1199 <dt> <a href=
"cuddAllDet.html#Cudd_tlcInfoFree" TARGET=
"MAIN"><code>Cudd_tlcInfoFree()
</code></a>
1200 <dd> Frees a DdTlcInfo Structure.
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.
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.
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.
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.
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.
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.
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.
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).
1226 <dt> <a href=
"cuddAllDet.html#Cudd_zddDiff" TARGET=
"MAIN"><code>Cudd_zddDiff()
</code></a>
1227 <dd> Computes the difference of two ZDDs.
1229 <dt> <a href=
"cuddAllDet.html#Cudd_zddDivideF" TARGET=
"MAIN"><code>Cudd_zddDivideF()
</code></a>
1230 <dd> Modified version of Cudd_zddDivide.
1232 <dt> <a href=
"cuddAllDet.html#Cudd_zddDivide" TARGET=
"MAIN"><code>Cudd_zddDivide()
</code></a>
1233 <dd> Computes the quotient of two unate covers.
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.
1238 <dt> <a href=
"cuddAllDet.html#Cudd_zddFirstPath" TARGET=
"MAIN"><code>Cudd_zddFirstPath()
</code></a>
1239 <dd> Finds the first path of a ZDD.
1241 <dt> <a href=
"cuddAllDet.html#Cudd_zddIntersect" TARGET=
"MAIN"><code>Cudd_zddIntersect()
</code></a>
1242 <dd> Computes the intersection of two ZDDs.
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.
1247 <dt> <a href=
"cuddAllDet.html#Cudd_zddIte" TARGET=
"MAIN"><code>Cudd_zddIte()
</code></a>
1248 <dd> Computes the ITE of three ZDDs.
1250 <dt> <a href=
"cuddAllDet.html#Cudd_zddIthVar" TARGET=
"MAIN"><code>Cudd_zddIthVar()
</code></a>
1251 <dd> Returns the ZDD variable with index i.
1253 <dt> <a href=
"cuddAllDet.html#Cudd_zddNextPath" TARGET=
"MAIN"><code>Cudd_zddNextPath()
</code></a>
1254 <dd> Generates the next path of a ZDD.
1256 <dt> <a href=
"cuddAllDet.html#Cudd_zddPortFromBdd" TARGET=
"MAIN"><code>Cudd_zddPortFromBdd()
</code></a>
1257 <dd> Converts a BDD into a ZDD.
1259 <dt> <a href=
"cuddAllDet.html#Cudd_zddPortToBdd" TARGET=
"MAIN"><code>Cudd_zddPortToBdd()
</code></a>
1260 <dd> Converts a ZDD into a BDD.
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.
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.
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.
1271 <dt> <a href=
"cuddAllDet.html#Cudd_zddPrintSubtable" TARGET=
"MAIN"><code>Cudd_zddPrintSubtable()
</code></a>
1272 <dd> Prints the ZDD table.
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.
1277 <dt> <a href=
"cuddAllDet.html#Cudd_zddReadNodeCount" TARGET=
"MAIN"><code>Cudd_zddReadNodeCount()
</code></a>
1278 <dd> Reports the number of nodes in ZDDs.
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.
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.
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
1290 <dt> <a href=
"cuddAllDet.html#Cudd_zddReduceHeap" TARGET=
"MAIN"><code>Cudd_zddReduceHeap()
</code></a>
1291 <dd> Main dynamic reordering routine for ZDDs.
1293 <dt> <a href=
"cuddAllDet.html#Cudd_zddShuffleHeap" TARGET=
"MAIN"><code>Cudd_zddShuffleHeap()
</code></a>
1294 <dd> Reorders ZDD variables according to given permutation.
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.
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.
1302 <dt> <a href=
"cuddAllDet.html#Cudd_zddSymmProfile" TARGET=
"MAIN"><code>Cudd_zddSymmProfile()
</code></a>
1303 <dd> Prints statistics on symmetric ZDD variables.
1305 <dt> <a href=
"cuddAllDet.html#Cudd_zddUnateProduct" TARGET=
"MAIN"><code>Cudd_zddUnateProduct()
</code></a>
1306 <dd> Computes the product of two unate covers.
1308 <dt> <a href=
"cuddAllDet.html#Cudd_zddUnion" TARGET=
"MAIN"><code>Cudd_zddUnion()
</code></a>
1309 <dd> Computes the union of two ZDDs.
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.
1314 <dt> <a href=
"cuddAllDet.html#Cudd_zddWeakDivF" TARGET=
"MAIN"><code>Cudd_zddWeakDivF()
</code></a>
1315 <dd> Modified version of Cudd_zddWeakDiv.
1317 <dt> <a href=
"cuddAllDet.html#Cudd_zddWeakDiv" TARGET=
"MAIN"><code>Cudd_zddWeakDiv()
</code></a>
1318 <dd> Applies weak division to two covers.
1324 Last updated on
20090220 23h06