module Mtbddc:sig
..end
type 'a
capsule = private {
|
content : |
type 'a
unique
'a
.
Use this module rather than Cudd.Mtbdd
when 'a
is implemented as a
a custom block with finalization function.
type'a
t ='a unique Cudd.Vdd.t
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.Mtbddc.manager
. Objects of this type are
automatically garbage collected.
type'a
table ='a unique Cudd.PWeakke.t
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
val unique : 'a table -> 'a -> 'a unique
val get : 'a unique -> 'a
type 'a
mtbdd =
| |
Leaf of |
(* | Terminal value | *) |
| |
Ite of |
(* | Decision on CUDD variable | *) |
t
Cudd.Add
and Cudd.Vdd
for the description
of the interface.val manager : 'a t -> Cudd.Man.v Cudd.Man.t
val is_cst : 'a t -> bool
val topvar : 'a t -> int
val dthen : 'a t -> 'a t
val delse : 'a t -> 'a t
val cofactors : int -> 'a t -> 'a t * 'a t
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
val inspect : 'a t -> 'a mtbdd
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
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 : Cudd.Man.v Cudd.Bdd.t array -> 'a t -> 'a t
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
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
val varmap : 'a t -> 'a t
val permute : 'a t -> int array -> 'a t
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
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
val guard_of_leaf : 'a table -> 'a t -> 'a -> Cudd.Man.v Cudd.Bdd.t
val leaves_u : 'a t -> 'a unique array
val leaves : 'a t -> 'a array
val pick_leaf_u : 'a t -> 'a unique
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
val guardleafs : 'a t -> (Cudd.Man.v Cudd.Bdd.t * 'a) array
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
Cudd.Mapleaf
;Cudd.User
.val transfer : 'a t -> Cudd.Man.v Cudd.Man.t -> 'a t
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