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