Index of values

Be cautious, it is not type safe (if you use Cudd.Vdd.nodes_below_level, etc...: you can try to retrieve a constant value of some type and () value of the background value will be treated as another type.

Internal, do not use !

C printing function.

Raw (C) printing function.

Cudd_addPlus.

add t x adds x to t.

Cudd_addAgreement.

Combine the two previous operations.

Cudd_bddApproxConjDecomp.

Cudd_bddIterConjDecomp.

Returns the arity of the local cache.

Returns the arity of the hashtable

Cudd_ReorderingStatus.

Cuddaux_addIte/Cudd_addIte.

Cudd_BiasedOverApprox.

Cudd_BiasedUnderApprox.

Cudd_bddBooleanDiff.

Cudd_CheckKeys.

Remove all elements from the table.

Clears the content of the local cache.

Clears the content of the hashtable

Clears the content of all created hashtables

Cudd_bddClippingAnd.

Cudd_bddClippingAndAbstract.

Cudd_Cofactor.

cofactor mtbdd cube evaluates mtbbdd on the cube cube

cofactor mtbdd cube evaluates mtbbdd on the cube cube

Cudd_Cofactor.

Returns the positive and negative cofactor of the ADD wrt the variable

Returns the positive and negative cofactor of the MTBDD wrt the variable

Returns the positive and negative cofactor of the MTBDD wrt the variable

Returns the positive and negative cofactor of the BDD wrt the variable

combineexpansive ~default ~merge (guard,leaf) vdd = merge (Vdd.ite guard leaf default) vdd.

Generic function, instanciated above.

Generic function, instanciated above.

Functions similar to combineleaf_array, but in which the first (resp.

Generic function,.

combinetractive (guard,leaf) vdd = Vdd.ite guard leaf vdd.

Cuddaux_addCompose/Cudd_addCompose.

Cudd_bddCompose.

Cudd_bddConstrain.

Cudd_bddCorrelation.

Cudd_bddCorrelationWeights.

Count the number of elements in the table.

create n creates a new empty weak hash table, of initial size n.

create ~size:n arity create a hashtable of arity arity, of the optional size n

Creates local caches of the given arity, with initial size size and maximal size maxsize.

Cudd_addConst.

Cudd_FindEssential.

Cudd_CubeArrayToBdd.

Cuddaux_bddCubeUnion.

Cudd_bddAnd.

Cudd_DebugCheck.

Cudd_E.

Returns the negative subnode of the MTBDD

Returns the negative subnode of the MTBDD

Cudd_E.

Cudd_Density.

Cudd_Density.

Returns the false BDD

Cudd_addDiff.

Cudd_AutodynDisable.

Cudd_addDivide.

Cudd_Not.

Cudd_bddOr.

Cudd_T.

Returns the positive subnode of the MTBDD

Returns the positive subnode of the MTBDD

Cudd_T.

Returns the true BDD

Cudd_V.

Returns the value of the assumed constant MTBDD

Returns the value of the assumed constant MTBDD

Cudd_AutodynEnable.

Same as Cudd.Bdd.nxor

Cuddaux_addEvalConst/Cudd_addEvalConst.

Variation of Cudd_addExistAbstract.

Cudd_bddExistAbstract.

Cudd_bddAndAbstract.

Cudd_bddXorExistAbstract.

Same as above, but with \/ replaced by merge (supposed to be commutative and associative).

Same as above, but with \/ replaced by merge (supposed to be commutative and associative).

find t x returns an instance of x found in t.

find_all t x returns a list of all the instances of x found in t.

cuddCacheFlush.

fold f t init computes (f d1 (... (f dN init))) where d1 ... dN are the elements of t in some unspecified order.

Variation of Cudd_addUnivAbstract.

Cudd_bddUnivAbstract.

cuddGarbageCollect.

Cudd_bddGenDisjDecomp.

Cudd_bddVarConjDecomp.

Type conversion (no computation)

Type conversion (no computation)

Cudd_ReadArcviolation.

Cudd_ReadBackground.

Cudd_ReadSize.

Cudd_ReadCacheHits.

Cudd_ReadCacheLookUps.

Cudd_ReadCacheSlots.

Cudd_ReadCacheUsedSlots.

Cudd_ReadNumberXovers.

Cudd_ReadDead.

Cudd_ReadEpsilon.

Cudd_ReadErrorCode.

Cudd_ReadGarbageCollections.

Cudd_ReadGarbageCollectionTime.

Cudd_ReadGroupcheck.

Cudd_ReadKeys.

Cudd_ReadLinear.

Cudd_ReadLooseUpTo.

Cudd_ReadMaxCache.

Cudd_ReadMaxCacheHard.

Cudd_ReadMaxGrowth.

Cudd_ReadMaxGrowthAlternate.

Cudd_ReadMaxLive.

Cudd_ReadMaxMemory.

Cudd_ReadMinDead.

Cudd_ReadMinHit.

Cudd_ReadNextReordering.

Cudd_ReadNodeCount.

Cudd_ReadPeakNodeCount.

Cudd_ReadPopulationSize.

Cudd_ReadRecomb.

Cudd_ReadReorderingCycle.

Cudd_ReadReorderings.

Cudd_ReadReorderingTime.

Cudd_ReadSiftMaxSwap.

Cudd_ReadSiftMaxVar.

Cudd_ReadSlots.

Cudd_ReadSwapSteps.

Cudd_ReadSymmviolation.

Cudd_ReadUsedSlots.

Cudd_ReadZddSize.

Cudd_MakeTreeNode.

Guard of the given leaf

Guard of the given leaf

Guard of the given leaf

Guard of the given leaf

Cuddaux_addGuardOfNode.

Guard of non background leaves

Returns the set of leaf values together with their guard in the ADD

Returns the set of leaf values together with their guard in the ADD

Returns the set of leaf values together with their guard in the ADD

Returns the set of leaf values together with their guard in the ADD

Decomposes the top node of the ADD

Decompose the MTBDD

Decompose the MTBDD

Decomposes the top node of the BDD

Cudd_bddIntersect.

Cudd_IsComplement.

Cudd_IsConstant.

Is the MTBDD constant ?

Is the MTBDD constant ?

Cudd_IsConstant.

Equality test

Are the two BDDs equal ?

Variation of Cudd_EquivDC.

Variation of Cuddaux_addEvalConst/Cudd_addEvalConst.

Is it a false BDD ?

Cudd_bddLeq.

Variation of Cudd_bddLeq.

Is the result of ite constant, and if it is the case, what is its value ?

Cudd_addLeq.

Cudd_bddLeq.

Variation of Cudd_bddLeqUnless.

Is it a true BDD ?

Cudd_bddVarIsDependent.

Cudd_bddIsVarEssential.

Cuddaux_IsVarIn.

Cuddaux_IsVarIn.

Cudd_bddIte.

Cuddaux_addIteConstant/Cudd_addIteConstant.

Cudd_bddIteConstant.

iter f t calls f on each element of t, in some unspecified order.

Similar to Cudd.Bdd.iter_cube

Cudd_ForeachCube.

Similar to Cudd.Bdd.iter_node

Cudd_ForeachNode.

Cudd_ForeachPrime.

Cudd_bddIterDisjDecomp.

Cudd_bddGenConjDecomp.

Cudd_bddIthVar.

Returns the set of leaf values (excluding the background value)

Returns the set of leaf values (excluding the background value)

Returns the set of leaf values (excluding the background value)

Returns the set of leaf values (excluding the background value)

Cudd_ReadPerm.

Cudd_bddLICompaction.

Converts a cube into a list of pairs of a variable and a phase.

Converts a support into a list of variables

Cudd_addLog.

Make an existential quantification operation, with the given memoization policy, and the given underlying binary operation, assumed to be commutative and idempotent, that combines the two branch of the diagram when a decision is quantified out.

Making operations

Makes a binary operation, with the given memoization policy.

Makes a binary operation, with the given memoization policy.

Building a table

Building a table

Register a binary test, with the given memoization policy,

Variation of Cudd_Init.

Returns the manager associated to the ADD

Returns the manager associated to the MTBDD

Returns the manager associated to the MTBDD

Returns the manager associated to the BDD

Return the MTBDD \/ guard -> f leaf

Return the MTBDD \/ guard1 /\ guard2 -> f leaf1 leaf2

Variation of Cudd_addMatrixMultiply.

Cudd_addMaximum.

mem t x returns true if there is at least one instance of x in t, false otherwise.

merge t x returns an instance of x found in t if any, or else adds x to t and return x.

Variant of merge: merge_map t x f is equivalent to try find t x with Not_found -> let y = f x in add t y; Some y.

Cudd_addMinimum.

Cudd_bddMinimize.

Cudd_addTimes.

Cudd_bddNand.

Cudd_CountLeaves.

Cudd_CountMinterm.

Cudd_CountMinterm.

Cudd_CountPathsToNonZero.

Cudd_CountPath.

Cudd_CountPath.

Cudd_CountPathsToNonZero.

Cudd_bddNewVar.

Cudd_bddNewVarAtLevel.

Cuddaux_NodesBelowLevel.

Cuddaux_NodesBelowLevel.

Cudd_bddNor.

Cudd_bddXnor.

Cudd_BddToAdd.

Cudd_OverApprox.

Cudd_addPermute.

Variant with controllable memoization policy.

Cudd_bddPermute.

Cudd_bddPickOneMinterm.

Cudd_bddPickArbitraryMinterms.

Picks (but not randomly) a non background leaf.

Picks (but not randomly) a non background leaf.

Picks (but not randomly) a non background leaf.

Picks (but not randomly) a non background leaf.

Cudd_bddPickOneCube.

Prints a BDD by recursively decomposing it as monomial followed by a tree.

Printing function

Prints a BDD by recursively decomposing it as monomial followed by a tree.

Prints the minterms of the BDD in the same way as Cudd_Printminterm.

Prints the minterms of the BDD in the same way as Cudd_Printminterm.

Cudd_PrintInfo.

Parameter for printing functions: specify the maximum number of minterms to be printed.

print_minterm print_id print_leaf fmt bdd prints the minterms of the BDD using print_id to print indices of variables and print_leaf to print leaf values.

print_minterm bassoc fmt bdd prints the minterms of the BDD using bassoc to convert indices of variables to names.

Cudd_ReduceHeap.

Cudd_RemapOverApprox.

Cudd_RemapUnderApprox.

remove t x removes from t one instance of x.

If true, simplifies in some functions MTBDDs using Cudd.Mtbdd.restrict or Cudd.Mtbddc.restrict.

Cuddaux_bddRestrict.

Assuming that the new guards delivered by the function f are disjoint, return the MTBDD default \/ (\/ nguard -> nleaf) with (nguard,nleaf) = f guard leaf.

Assuming that the new guards delivered by the function f are disjoint, return the MTBDD default \/ (\/ nguard -> nleaf) with (nguard,nleaf) = f (guard1 /\ guard2) leaf1 leaf2.

Cudd_addSetNZ.

Cudd_SetArcviolation.

Variation of Cudd_SetBackground.

Cudd_SetNumberXovers.

Cudd_SetEpsilon.

set_gc max gc reordering performs several things: It sets the ratio used/max for BDDs abstract values to 1/max (see the OCaml manual for details). 1 000 000 is a good value., It also sets for all the future managers that will be created the hook function to be called before a CUDD garbage collection, and the hook function to be called before a CUDD reordering. You may typically specify a OCaml garbage collection function for both hooks, in order to make OCaml dereference unused nodes, thus allowing CUDD to remove them. Default values are Gc.full_major() for both hooks.

Cudd_SetGroupcheck.

Cudd_SetLooseUpTo.

Cudd_SetMaxCacheHard.

Cudd_SetMaxGrowth.

Cudd_SetMaxGrowthAlternate.

Cudd_SetMaxLive.

Cudd_SetMaxMemory.

Cudd_SetMinHit.

Cudd_SetNextReordering.

Cudd_SetPopulationSize.

(Cudd_SetRecomb.

Cudd_SetReorderingCycle.

Cudd_SetSiftMaxSwap.

Cudd_SetSiftMaxVar.

Cudd_SetSymmviolation.

Cuddaux_SetVarMap/Cudd_SetVarMap.

Cudd_ShuffleHeap.

Cudd_DagSize.

Cudd_DagSize.

Cudd_bddSqueeze.

Cudd_Srandom.

Return statistics on the table.

Printing functions

Cudd_addMinus.

Cudd_SubsetHeavyBranch.

Cudd_SubsetShortPaths.

Cudd_SubsetCompress.

Cudd_SupersetHeavyBranch.

Cudd_SupersetShortPaths.

Cudd_SupersetCompress.

Cudd_Support.

Cudd_Support.

Cudd_Cofactor.

Cudd_bddLiteralSetIntersection.

Cudd_bddAnd.

Cudd_SupportSize.

Cudd_SupportSize.

Internal table

Cuddaux_bddTDConstrain.

Cuddaux_bddTDRestrict.

Cudd_addThreshold.

Variation of Cudd_addTimesPlus.

Cudd_addBddPattern.

Cudd_addBddInterval.

Cudd_addBddStrictThreshold.

Cudd_addBddThreshold.

Cudd_NodeReadIndex.

Returns the index of the top node of the MTBDD (65535 for a constant MTBDD)

Returns the index of the top node of the MTBDD (65535 for a constant MTBDD)

Cudd_NodeReadIndex.

Cuddaux_addTransfer/Cudd_bddTransfer.

Cudd_bddTransfer.

Variation of Cudd_addTriangle.

Cudd_UnderApprox.

Cudd_FreeTree.

Building a unique constant

Building a unique constant

Cudd_ReadInvPerm.

Cudd_bddVarDisjDecomp.

Cuddaux_addVarMap/Cudd_bddVarMap.

Cudd_bddVarMap.

Cuddaux_addVectorCompose/Cudd_addVectorCompose.

Cudd_bddVectorCompose.

Cudd_VectorSupport.

Cudd_Cudd_VectorSupport.

Cudd_VectorSupport.

Cudd_bddXor.