Previous  Up  Next

Module Cudd.Mtbdd


module Mtbdd: sig .. end
type 'a unique
Type of unique representants of MTBDD leaves of type 'a.

For technical reason, type 'a should not be implemented as a custom block with finalization function. (This is checked and the program aborts with an error message).

Use Cudd.Mtbddc module if your type does not fulfill this requirement. Mtbddc modules automatically encapsulate the value into a ML type.

type 'a t = 'a unique Cudd.Vdd.t
Type of MTBDDs.

Objects of this type contains both the top node of the MTBDD and the manager to which the node belongs. The manager can be retrieved with Cudd.Mtbdd.manager. Objects of this type are automatically garbage collected.

type 'a table = 'a unique Cudd.PWeakke.t
Hashtable to manage unique constants
val print_table : ?first:(unit, Format.formatter, unit) Pervasives.format ->
       ?sep:(unit, Format.formatter, unit) Pervasives.format ->
       ?last:(unit, Format.formatter, unit) Pervasives.format ->
       (Format.formatter -> 'a -> unit) ->
       Format.formatter -> 'a table -> unit
val make_table : hash:('a -> int) -> equal:('a -> 'a -> bool) -> 'a table
Building a table
val unique : 'a table -> 'a -> 'a unique
Building a unique constant
val get : 'a unique -> 'a
Type conversion (no computation)

type 'a mtbdd =
| Leaf of 'a unique (*Terminal value*)
| Ite of int * 'a t * 'a t (*Decision on CUDD variable*)
Public type for exploring the abstract type t

We refer to the modules Cudd.Add and Cudd.Vdd for the description of the interface.

Extractors


val manager : 'a t -> Cudd.Man.v Cudd.Man.t
Returns the manager associated to the MTBDD
val is_cst : 'a t -> bool
Is the MTBDD constant ?
val topvar : 'a t -> int
Returns the index of the top node of the MTBDD (65535 for a constant MTBDD)
val dthen : 'a t -> 'a t
Returns the positive subnode of the MTBDD
val delse : 'a t -> 'a t
Returns the negative subnode of the MTBDD
val cofactors : int -> 'a t -> 'a t * 'a t
Returns the positive and negative cofactor of the MTBDD wrt the variable
val cofactor : 'a t -> Cudd.Man.v Cudd.Bdd.t -> 'a t
cofactor mtbdd cube evaluates mtbbdd on the cube cube
val dval_u : 'a t -> 'a unique
val dval : 'a t -> 'a
Returns the value of the assumed constant MTBDD
val inspect : 'a t -> 'a mtbdd
Decompose the MTBDD

Supports


val support : 'a t -> Cudd.Man.v Cudd.Bdd.t
val supportsize : 'a t -> int
val is_var_in : int -> 'a t -> bool
val vectorsupport : 'a t array -> Cudd.Man.v Cudd.Bdd.t
val vectorsupport2 : Cudd.Man.v Cudd.Bdd.t array -> 'a t array -> Cudd.Man.v Cudd.Bdd.t

Classical operations


val cst_u : Cudd.Man.v Cudd.Man.t -> 'a unique -> 'a t
val cst : Cudd.Man.v Cudd.Man.t -> 'a table -> 'a -> 'a t
val ite : Cudd.Man.v Cudd.Bdd.t ->
       'a t -> 'a t -> 'a t
val ite_cst : Cudd.Man.v Cudd.Bdd.t ->
       'a t -> 'a t -> 'a t option
val eval_cst : 'a t -> Cudd.Man.v Cudd.Bdd.t -> 'a t option
val compose : int -> Cudd.Man.v Cudd.Bdd.t -> 'a t -> 'a t
val vectorcompose : ?memo:Cudd.Memo.t ->
       Cudd.Man.v Cudd.Bdd.t array -> 'a t -> 'a t

Logical tests


val is_equal : 'a t -> 'a t -> bool
val is_equal_when : 'a t -> 'a t -> Cudd.Man.v Cudd.Bdd.t -> bool
val is_eval_cst_u : 'a t -> Cudd.Man.v Cudd.Bdd.t -> 'a unique option
val is_ite_cst_u : Cudd.Man.v Cudd.Bdd.t ->
       'a t -> 'a t -> 'a unique option
val is_eval_cst : 'a t -> Cudd.Man.v Cudd.Bdd.t -> 'a option
val is_ite_cst : Cudd.Man.v Cudd.Bdd.t -> 'a t -> 'a t -> 'a option

Structural information


val size : 'a t -> int
val nbpaths : 'a t -> float
val nbnonzeropaths : 'a t -> float
val nbminterms : int -> 'a t -> float
val density : int -> 'a t -> float
val nbleaves : 'a t -> int

Variable mapping


val varmap : 'a t -> 'a t
val permute : ?memo:Cudd.Memo.t -> 'a t -> int array -> 'a t

Iterators


val iter_cube_u : (Cudd.Man.tbool array -> 'a unique -> unit) ->
       'a t -> unit
val iter_cube : (Cudd.Man.tbool array -> 'a -> unit) -> 'a t -> unit
val iter_node : ('a t -> unit) -> 'a t -> unit

Leaves and guards


val guard_of_node : 'a t -> 'a t -> Cudd.Man.v Cudd.Bdd.t
val guard_of_nonbackground : 'a t -> Cudd.Man.v Cudd.Bdd.t
val nodes_below_level : ?max:int -> 'a t -> int option -> 'a t array
val guard_of_leaf_u : 'a t -> 'a unique -> Cudd.Man.v Cudd.Bdd.t
Guard of the given leaf
val guard_of_leaf : 'a table -> 'a t -> 'a -> Cudd.Man.v Cudd.Bdd.t
val leaves_u : 'a t -> 'a unique array
Returns the set of leaf values (excluding the background value)
val leaves : 'a t -> 'a array
val pick_leaf_u : 'a t -> 'a unique
Picks (but not randomly) a non background leaf. Return None if the only leaf is the background leaf.
val pick_leaf : 'a t -> 'a
val guardleafs_u : 'a t -> (Cudd.Man.v Cudd.Bdd.t * 'a unique) array
Returns the set of leaf values together with their guard in the ADD
val guardleafs : 'a t -> (Cudd.Man.v Cudd.Bdd.t * 'a) array

Minimizations


val constrain : 'a t -> Cudd.Man.v Cudd.Bdd.t -> 'a t
val tdconstrain : 'a t -> Cudd.Man.v Cudd.Bdd.t -> 'a t
val restrict : 'a t -> Cudd.Man.v Cudd.Bdd.t -> 'a t
val tdrestrict : 'a t -> Cudd.Man.v Cudd.Bdd.t -> 'a t

Conversions



User operations



Two options:

Miscellaneous


val transfer : 'a t -> Cudd.Man.v Cudd.Man.t -> 'a t

Printing


val print__minterm : (Format.formatter -> 'a -> unit) ->
       Format.formatter -> 'a t -> unit
val print_minterm : (Format.formatter -> int -> unit) ->
       (Format.formatter -> 'a -> unit) ->
       Format.formatter -> 'a t -> unit
val print : (Format.formatter -> Cudd.Man.v Cudd.Bdd.t -> unit) ->
       (Format.formatter -> 'a -> unit) ->
       Format.formatter -> 'a t -> unit