sig
type 'a unique
type 'a t = 'a Cudd.Mtbdd.unique Cudd.Vdd.t
type 'a table = 'a Cudd.Mtbdd.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 Cudd.Mtbdd.table -> unit
val make_table :
hash:('a -> int) -> equal:('a -> 'a -> bool) -> 'a Cudd.Mtbdd.table
val unique : 'a Cudd.Mtbdd.table -> 'a -> 'a Cudd.Mtbdd.unique
val get : 'a Cudd.Mtbdd.unique -> 'a
type 'a mtbdd =
Leaf of 'a Cudd.Mtbdd.unique
| Ite of int * 'a Cudd.Mtbdd.t * 'a Cudd.Mtbdd.t
external manager : 'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Man.t
= "camlidl_cudd_bdd_manager"
external is_cst : 'a Cudd.Mtbdd.t -> bool = "camlidl_cudd_bdd_is_cst"
external topvar : 'a Cudd.Mtbdd.t -> int = "camlidl_cudd_bdd_topvar"
external dthen : 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t
= "camlidl_cudd_add_dthen"
external delse : 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t
= "camlidl_cudd_add_delse"
external cofactors :
int -> 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t * 'a Cudd.Mtbdd.t
= "camlidl_cudd_add_cofactors"
external cofactor :
'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbdd.t
= "camlidl_cudd_add_cofactor"
val dval_u : 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.unique
val dval : 'a Cudd.Mtbdd.t -> 'a
val inspect : 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.mtbdd
external support : 'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t
= "camlidl_cudd_bdd_support"
external supportsize : 'a Cudd.Mtbdd.t -> int
= "camlidl_cudd_bdd_supportsize"
external is_var_in : int -> 'a Cudd.Mtbdd.t -> bool
= "camlidl_cudd_bdd_is_var_in"
external vectorsupport : 'a Cudd.Mtbdd.t array -> Cudd.Man.v Cudd.Bdd.t
= "camlidl_cudd_bdd_vectorsupport"
external vectorsupport2 :
Cudd.Man.v Cudd.Bdd.t array ->
'a Cudd.Mtbdd.t array -> Cudd.Man.v Cudd.Bdd.t
= "camlidl_cudd_add_vectorsupport2"
val cst_u :
Cudd.Man.v Cudd.Man.t -> 'a Cudd.Mtbdd.unique -> 'a Cudd.Mtbdd.t
val cst :
Cudd.Man.v Cudd.Man.t -> 'a Cudd.Mtbdd.table -> 'a -> 'a Cudd.Mtbdd.t
external ite :
Cudd.Man.v Cudd.Bdd.t ->
'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t
= "camlidl_cudd_add_ite"
external ite_cst :
Cudd.Man.v Cudd.Bdd.t ->
'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t option
= "camlidl_cudd_add_ite_cst"
external eval_cst :
'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbdd.t option
= "camlidl_cudd_add_eval_cst"
external compose :
int -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t
= "camlidl_cudd_add_compose"
val vectorcompose :
?memo:Cudd.Memo.t ->
Cudd.Man.v Cudd.Bdd.t array -> 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t
external is_equal : 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t -> bool
= "camlidl_cudd_bdd_is_equal"
external is_equal_when :
'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> bool
= "camlidl_cudd_bdd_is_equal_when"
val is_eval_cst_u :
'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbdd.unique option
val is_ite_cst_u :
Cudd.Man.v Cudd.Bdd.t ->
'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.unique option
val is_eval_cst : 'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a option
val is_ite_cst :
Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t -> 'a option
external size : 'a Cudd.Mtbdd.t -> int = "camlidl_cudd_bdd_size"
external nbpaths : 'a Cudd.Mtbdd.t -> float = "camlidl_cudd_bdd_nbpaths"
external nbnonzeropaths : 'a Cudd.Mtbdd.t -> float
= "camlidl_cudd_bdd_nbtruepaths"
external nbminterms : int -> 'a Cudd.Mtbdd.t -> float
= "camlidl_cudd_bdd_nbminterms"
external density : int -> 'a Cudd.Mtbdd.t -> float
= "camlidl_cudd_bdd_density"
external nbleaves : 'a Cudd.Mtbdd.t -> int = "camlidl_cudd_add_nbleaves"
external varmap : 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t
= "camlidl_cudd_add_varmap"
val permute :
?memo:Cudd.Memo.t -> 'a Cudd.Mtbdd.t -> int array -> 'a Cudd.Mtbdd.t
val iter_cube_u :
(Cudd.Man.tbool array -> 'a Cudd.Mtbdd.unique -> unit) ->
'a Cudd.Mtbdd.t -> unit
val iter_cube :
(Cudd.Man.tbool array -> 'a -> unit) -> 'a Cudd.Mtbdd.t -> unit
external iter_node : ('a Cudd.Mtbdd.t -> unit) -> 'a Cudd.Mtbdd.t -> unit
= "camlidl_cudd_iter_node"
external guard_of_node :
'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t
= "camlidl_cudd_add_guard_of_node"
external guard_of_nonbackground : 'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t
= "camlidl_cudd_add_guard_of_nonbackground"
val nodes_below_level :
?max:int -> 'a Cudd.Mtbdd.t -> int option -> 'a Cudd.Mtbdd.t array
val guard_of_leaf_u :
'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.unique -> Cudd.Man.v Cudd.Bdd.t
val guard_of_leaf :
'a Cudd.Mtbdd.table -> 'a Cudd.Mtbdd.t -> 'a -> Cudd.Man.v Cudd.Bdd.t
val leaves_u : 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.unique array
val leaves : 'a Cudd.Mtbdd.t -> 'a array
val pick_leaf_u : 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.unique
val pick_leaf : 'a Cudd.Mtbdd.t -> 'a
val guardleafs_u :
'a Cudd.Mtbdd.t -> (Cudd.Man.v Cudd.Bdd.t * 'a Cudd.Mtbdd.unique) array
val guardleafs : 'a Cudd.Mtbdd.t -> (Cudd.Man.v Cudd.Bdd.t * 'a) array
external constrain :
'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbdd.t
= "camlidl_cudd_add_constrain"
external tdconstrain :
'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbdd.t
= "camlidl_cudd_add_tdconstrain"
external restrict :
'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbdd.t
= "camlidl_cudd_add_restrict"
external tdrestrict :
'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbdd.t
= "camlidl_cudd_add_tdrestrict"
external transfer :
'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Man.t -> 'a Cudd.Mtbdd.t
= "camlidl_cudd_add_transfer"
val print__minterm :
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a Cudd.Mtbdd.t -> unit
val print_minterm :
(Format.formatter -> int -> unit) ->
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a Cudd.Mtbdd.t -> unit
val print :
(Format.formatter -> Cudd.Man.v Cudd.Bdd.t -> unit) ->
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a Cudd.Mtbdd.t -> unit
end