Module Cudd.Bdd

module Bdd: sig .. end

type 'a t 
Abstract type for BDDs.

Objects of type 'a t contain both the top node of the BDD and the manager to which this node belongs. 'a, which is either Cudd.Man.d or Cudd.Man.v indicates the kind of manager to which the node belongs, see module Cudd.Man. The manager can be retrieved with Cudd.Bdd.manager. These objects are automatically garbage collected.

type 'a bdd = 
| Bool of bool (*Terminal value*)
| Ite of int * 'a t * 'a t (*Decision on CUDD variable*)
Public type for exploring the abstract type t
type dt = Cudd.Man.d t 
type vt = Cudd.Man.v t 
Shortcuts

Extractors


val manager : 'a t -> 'a Cudd.Man.t
Returns the manager associated to the BDD
val is_cst : 'a t -> bool
Cudd_IsConstant. Is the BDD constant ?
val is_complement : 'a t -> bool
Cudd_IsComplement. Is the BDD a complemented one ?
val topvar : 'a t -> int
Cudd_NodeReadIndex. Returns the index of the (top node of the) BDD (65535 for a constant BDD)
val dthen : 'a t -> 'a t
Cudd_T. Returns the positive subnode of the BDD
val delse : 'a t -> 'a t
Cudd_E. Returns the negative subnode of the BDD
val cofactors : int -> 'a t -> 'a t * 'a t
Returns the positive and negative cofactor of the BDD wrt the variable
val cofactor : 'a t -> 'a t -> 'a t
Cudd_Cofactor. cofactor bdd cube evaluates bdd on the cube cube
val inspect : 'a t -> 'a bdd
Decomposes the top node of the BDD

Supports


val support : 'a t -> 'a t
Cudd_Support. Returns the support of the BDD
val supportsize : 'a t -> int
Cudd_SupportSize. Returns the size of the support of the BDD
val is_var_in : int -> 'a t -> bool
Cuddaux_IsVarIn. Does the given variable belong the support of the BDD ?
val vectorsupport : 'a t array -> 'a t
Cudd_Cudd_VectorSupport. Returns the support of the array of BDDs.

Raises a Failure exception in case where the array is of size 0 (in such case, the manager is unknown, and we cannot return an empty support). This operation does not use the global cache, unlike Cudd.Bdd.support.


Manipulation of supports


val support_inter : 'a t -> 'a t -> 'a t
Cudd_bddLiteralSetIntersection. Intersection of supports
val support_union : 'a t -> 'a t -> 'a t
Cudd_bddAnd. Union of supports
val support_diff : 'a t -> 'a t -> 'a t
Cudd_Cofactor. Difference of supports
val list_of_support : 'a t -> int list
Converts a support into a list of variables

Constants and Variables


val dtrue : 'a Cudd.Man.t -> 'a t
Returns the true BDD
val dfalse : 'a Cudd.Man.t -> 'a t
Returns the false BDD
val ithvar : 'a Cudd.Man.t -> int -> 'a t
Cudd_bddIthVar. Returns the BDD equivalent to the variable of the given index.
val newvar : 'a Cudd.Man.t -> 'a t
Cudd_bddNewVar. Returns the BDD equivalent to the variable of the next unused index.
val newvar_at_level : 'a Cudd.Man.t -> int -> 'a t
Cudd_bddNewVarAtLevel. Returns the BDD equivalent to the variable of the next unused index and sets its level.

Logical tests


val is_true : 'a t -> bool
Is it a true BDD ?
val is_false : 'a t -> bool
Is it a false BDD ?
val is_equal : 'a t -> 'a t -> bool
Are the two BDDs equal ?
val is_leq : 'a t -> 'a t -> bool
Cudd_bddLeq. Does the first BDD implies the second one ?
val is_inter_empty : 'a t -> 'a t -> bool
Variation of Cudd_bddLeq. Is the intersection (conjunction) of the two BDDs non empty (false) ?
val is_equal_when : 'a t -> 'a t -> 'a t -> bool
Variation of Cudd_EquivDC. Are the two first BDDs equal when the third one (careset) is true ?
val is_leq_when : 'a t -> 'a t -> 'a t -> bool
Variation of Cudd_bddLeqUnless. Does the first BDD implies the second one when the third one (careset) is true ?
val is_included_in : 'a t -> 'a t -> bool
Cudd_bddLeq. Same as Cudd.Bdd.is_leq

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

val is_ite_cst : 'a t -> 'a t -> 'a t -> bool option
val is_var_dependent : int -> 'a t -> bool
Cudd_bddVarIsDependent. Is the given variable dependent on others in the BDD ?
val is_var_essential : int -> bool -> 'a t -> bool
Cudd_bddIsVarEssential. Is the given variable with the specified phase implied by the BDD ?

Structural information


val size : 'a t -> int
Cudd_DagSize. Size if the BDD as a graph (the number of nodes).
val nbpaths : 'a t -> float
Cudd_CountPath. Number of paths in the BDD from the root to the leaves.
val nbtruepaths : 'a t -> float
Cudd_CountPathsToNonZero. Number of paths in the BDD from the root to the true leaf.
val nbminterms : int -> 'a t -> float
Cudd_CountMinterm. Number of minterms of the BDD assuming that it depends on the given number of variables.
val density : int -> 'a t -> float
Cudd_Density. Density of the BDD, which is the ratio of the number of minterms to the number of nodes. The BDD is assumed to depend on nvars variables.

Logical operations


val dnot : 'a t -> 'a t
Cudd_Not. Negation
val dand : 'a t -> 'a t -> 'a t
Cudd_bddAnd. Conjunction/Intersection
val dor : 'a t -> 'a t -> 'a t
Cudd_bddOr. Disjunction/Union
val xor : 'a t -> 'a t -> 'a t
Cudd_bddXor. Exclusive union
val nand : 'a t -> 'a t -> 'a t
Cudd_bddNand.
val nor : 'a t -> 'a t -> 'a t
Cudd_bddNor.
val nxor : 'a t -> 'a t -> 'a t
Cudd_bddXnor. Equality
val eq : 'a t -> 'a t -> 'a t
Same as Cudd.Bdd.nxor
val ite : 'a t -> 'a t -> 'a t -> 'a t
Cudd_bddIte. If-then-else operation.
val ite_cst : 'a t -> 'a t -> 'a t -> 'a t option
Cudd_bddIteConstant. If-then-else operation that succeeds when the result is a node of the arguments.
val compose : int -> 'a t -> 'a t -> 'a t
Cudd_bddCompose. compose var f bdd substitutes the variable var with the function f in bdd.
val vectorcompose : ?memo:Cudd.Memo.t -> 'a t array -> 'a t -> 'a t
Cudd_bddVectorCompose. vectorcompose table bdd performs a parallel substitution of every variable var present in the manager by table.(var) in bdd. The size of table should be at least Cudd.Man.get_bddvar_nb. You can optionnally control the memoization policy, see Cudd.Memo.
val intersect : 'a t -> 'a t -> 'a t
Cudd_bddIntersect. Returns a BDD included in the intersection of the arguments.

Variable mapping


val varmap : 'a t -> 'a t
Cudd_bddVarMap. Permutes the variables as it has been specified with Cudd.Man.set_varmap.
val permute : ?memo:Cudd.Memo.t -> 'a t -> int array -> 'a t
Cudd_bddPermute. Permutes the variables as it is specified by permut (same format as in Cudd.Man.set_varmap). You can optionnally control the memoization policy, see Cudd.Memo.

Iterators


val iter_node : ('a t -> unit) -> 'a t -> unit
Cudd_ForeachNode. Apply the function f to each (regularized) node of the BDD.
val iter_cube : (Cudd.Man.tbool array -> unit) -> 'a t -> unit
Cudd_ForeachCube. Apply the function f to each cube of the BDD. The cubes are specified as arrays of elements of type Cudd.Man.tbool. The size of the arrays is equal to Cudd.Man.get_bddvar_nb, the number of variables present in the manager.
val iter_prime : (Cudd.Man.tbool array -> unit) -> 'a t -> 'a t -> unit
Cudd_ForeachPrime. Apply the function f to each prime covering the BDD interval. The first BDD argument is the lower bound, the second the upper bound (which may be equal to the lower bound). The primes are specified as arrays of elements of type Cudd.Man.tbool. The size of the arrays is equal to Cudd.Man.get_bddvar_nb, the number of variables present in the manager.

Quantifications


val exist : 'a t -> 'a t -> 'a t
Cudd_bddExistAbstract. exist supp bdd quantifies existentially the set of variables defined by supp in the BDD.
val forall : 'a t -> 'a t -> 'a t
Cudd_bddUnivAbstract. forall supp bdd quantifies universally the set of variables defined by supp in the BDD.
val existand : 'a t -> 'a t -> 'a t -> 'a t
Cudd_bddAndAbstract. Simultaneous existential quantification and intersection of BDDs. Logically, existand supp x y = exist supp (dand x y).
val existxor : 'a t -> 'a t -> 'a t -> 'a t
Cudd_bddXorExistAbstract. Simultaneous existential quantification and exclusive or of BDDs. Logically, existxor supp x y = exist supp (xor x y).
val booleandiff : 'a t -> int -> 'a t
Cudd_bddBooleanDiff. Boolean difference of the BDD with respect to the variable.

Cubes


val cube_of_bdd : 'a t -> 'a t
Cudd_FindEssential. Returns the smallest cube (in the sens of inclusion) included in the BDD.
val cube_of_minterm : 'a Cudd.Man.t -> Cudd.Man.tbool array -> 'a t
Cudd_CubeArrayToBdd. Converts a minterm to a BDD (which is a cube).
val list_of_cube : 'a t -> (int * bool) list
Converts a cube into a list of pairs of a variable and a phase.
val cube_union : 'a t -> 'a t -> 'a t
Cuddaux_bddCubeUnion. Computes the union of cubes, which is the smallest cube containing both the argument cubes.
val pick_minterm : 'a t -> Cudd.Man.tbool array
Cudd_bddPickOneCube. Picks randomly a minterm in the BDD.
val pick_cube_on_support : 'a t -> 'a t -> 'a t
Cudd_bddPickOneMinterm. pick_cube_on_support bdd supp picks randomly a minterm/cube in the BDD, in which all the variables in the support supp have a definite value.

The support argument should contain the support of the BDD (otherwise the result may be incorrect).

val pick_cubes_on_support : 'a t -> 'a t -> int -> 'a t array
Cudd_bddPickArbitraryMinterms. pick_cubes_on_support bdd supp nb picks randomly nb minterms/cubes in the BDD, in which all the variables in the support have a definite value. The support argument should contain the support of the BDD (otherwise the result may be incorrect).

Fails if the effective number of such minterms in the BDD is less than nb.


Minimizations



The 6 following functions are generalized cofactor operations. gencof f c returns a BDD that coincides with f whenever c is true (and which is hopefully smaller). constrain enjoys in addition strong properties (see papers from Madre and Coudert)
val constrain : 'a t -> 'a t -> 'a t
Cudd_bddConstrain.
val tdconstrain : 'a t -> 'a t -> 'a t
Cuddaux_bddTDConstrain.
val restrict : 'a t -> 'a t -> 'a t
Cuddaux_bddRestrict.
val tdrestrict : 'a t -> 'a t -> 'a t
Cuddaux_bddTDRestrict.
val minimize : 'a t -> 'a t -> 'a t
Cudd_bddMinimize.
val licompaction : 'a t -> 'a t -> 'a t
Cudd_bddLICompaction.
val squeeze : 'a t -> 'a t -> 'a t
Cudd_bddSqueeze. sqeeze lower upper returns a (smaller) BDD which is in the functional interval [lower,upper].

Approximations


val clippingand : 'a t -> 'a t -> int -> bool -> 'a t
Cudd_bddClippingAnd. clippingand f g maxdepth direction
val clippingexistand : 'a t ->
'a t -> 'a t -> int -> bool -> 'a t
Cudd_bddClippingAndAbstract. clippingexistand supp f g maxdepth direction (order of argulents changed).
val underapprox : int -> int -> bool -> float -> 'a t -> 'a t
Cudd_UnderApprox. underapprox nvars threshold safe quality f
val overapprox : int -> int -> bool -> float -> 'a t -> 'a t
Cudd_OverApprox. overapprox nvars threshold safe quality f
val remapunderapprox : int -> int -> float -> 'a t -> 'a t
Cudd_RemapUnderApprox. remapunderapprox nvars threshold quality f
val remapoverapprox : int -> int -> float -> 'a t -> 'a t
Cudd_RemapOverApprox. remapovererapprox nvars threshold quality f
val biasedunderapprox : int ->
int -> float -> float -> 'a t -> 'a t -> 'a t
Cudd_BiasedUnderApprox. biasedunderapprox nvars threshold quality1 quality0 f g
val biasedoverapprox : int ->
int -> float -> float -> 'a t -> 'a t -> 'a t
Cudd_BiasedOverApprox. biasedovererapprox nvars threshold quality1 quality0 f g

For the 4 next functions, the profile is XXcompress nvars threshold f.
val subsetcompress : int -> int -> 'a t -> 'a t
Cudd_SubsetCompress.
val supersetcompress : int -> int -> 'a t -> 'a t
Cudd_SupersetCompress.
val subsetHB : int -> int -> 'a t -> 'a t
Cudd_SubsetHeavyBranch.
val supersetHB : int -> int -> 'a t -> 'a t
Cudd_SupersetHeavyBranch.

For the 2 next functions, the profile is XXXsetSP nvars threshold hardlimit f.
val subsetSP : int -> int -> bool -> 'a t -> 'a t
Cudd_SubsetShortPaths.
val supersetSP : int -> int -> bool -> 'a t -> 'a t
Cudd_SupersetShortPaths.

The following functions perform two-way conjunctive (disjunctive) decomposition of a BDD. Returns a pair if successful, None if no decomposition has been found.
val approxconjdecomp : 'a t -> ('a t * 'a t) option
Cudd_bddApproxConjDecomp.

Cudd_bddApproxDisjDecomp.

val approxdisjdecomp : 'a t -> ('a t * 'a t) option
Cudd_bddIterConjDecomp.
val iterconjdecomp : 'a t -> ('a t * 'a t) option
Cudd_bddIterDisjDecomp.
val iterdisjdecomp : 'a t -> ('a t * 'a t) option
Cudd_bddGenConjDecomp.
val genconjdecomp : 'a t -> ('a t * 'a t) option
Cudd_bddGenDisjDecomp.
val gendisjdecomp : 'a t -> ('a t * 'a t) option
Cudd_bddVarConjDecomp.
val varconjdecomp : 'a t -> ('a t * 'a t) option
Cudd_bddVarDisjDecomp.
val vardisjdecomp : 'a t -> ('a t * 'a t) option

Miscellaneous


val transfer : 'a t -> 'b Cudd.Man.t -> 'b t
Cudd_bddTransfer. Transfers a BDD to a different manager.
val correlation : 'a t -> 'a t -> float
Cudd_bddCorrelation. Computes the correlation of f and g (if f=g, their correlation is 1, if f=not g, it is 0)
val correlationweights : 'a t -> 'a t -> float array -> float
Cudd_bddCorrelationWeights.

Printing


val _print : 'a t -> unit
Raw (C) printing function. The output may mix badly with the OCAML output.
val print__minterm : Format.formatter -> 'a t -> unit
Prints the minterms of the BDD in the same way as Cudd_Printminterm.
val print_minterm : (Format.formatter -> int -> unit) ->
Format.formatter -> 'a t -> unit
print_minterm bassoc fmt bdd prints the minterms of the BDD using bassoc to convert indices of variables to names.
val print : (Format.formatter -> int -> unit) ->
Format.formatter -> 'a t -> unit
Prints a BDD by recursively decomposing it as monomial followed by a tree.
val print_list : (Format.formatter -> int -> unit) ->
Format.formatter -> (int * bool) list -> unit