sig
type +'a t
type 'a vdd = Leaf of 'a | Ite of int * 'a Cudd.Vdd.t * 'a Cudd.Vdd.t
external manager : 'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Man.t
= "camlidl_cudd_bdd_manager"
external is_cst : 'a Cudd.Vdd.t -> bool = "camlidl_cudd_bdd_is_cst"
external topvar : 'a Cudd.Vdd.t -> int = "camlidl_cudd_bdd_topvar"
external dthen : 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t = "camlidl_cudd_add_dthen"
external delse : 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t = "camlidl_cudd_add_delse"
external cofactors : int -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t * 'a Cudd.Vdd.t
= "camlidl_cudd_add_cofactors"
external cofactor : 'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Vdd.t
= "camlidl_cudd_add_cofactor"
external dval : 'a Cudd.Vdd.t -> 'a = "camlidl_cudd_avdd_dval"
external inspect : 'a Cudd.Vdd.t -> 'a Cudd.Vdd.vdd
= "camlidl_cudd_avdd_inspect"
external support : 'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t
= "camlidl_cudd_bdd_support"
external supportsize : 'a Cudd.Vdd.t -> int
= "camlidl_cudd_bdd_supportsize"
external is_var_in : int -> 'a Cudd.Vdd.t -> bool
= "camlidl_cudd_bdd_is_var_in"
external vectorsupport : 'a Cudd.Vdd.t array -> Cudd.Man.v Cudd.Bdd.t
= "camlidl_cudd_bdd_vectorsupport"
external vectorsupport2 :
Cudd.Man.v Cudd.Bdd.t array ->
'a Cudd.Vdd.t array -> Cudd.Man.v Cudd.Bdd.t
= "camlidl_cudd_add_vectorsupport2"
external cst : Cudd.Man.v Cudd.Man.t -> 'a -> 'a Cudd.Vdd.t
= "camlidl_cudd_avdd_cst"
val _background : Cudd.Man.v Cudd.Man.t -> 'a Cudd.Vdd.t
external ite :
Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t
= "camlidl_cudd_add_ite"
external ite_cst :
Cudd.Man.v Cudd.Bdd.t ->
'a Cudd.Vdd.t -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t option
= "camlidl_cudd_add_ite_cst"
external eval_cst :
'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Vdd.t option
= "camlidl_cudd_add_eval_cst"
external compose : int -> Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t
= "camlidl_cudd_add_compose"
val vectorcompose :
?memo:Cudd.Memo.t -> Cudd.Bdd.vt array -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t
external is_equal : 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t -> bool
= "camlidl_cudd_bdd_is_equal"
external is_equal_when :
'a Cudd.Vdd.t -> 'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> bool
= "camlidl_cudd_bdd_is_equal_when"
external is_eval_cst : 'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a option
= "camlidl_cudd_avdd_is_eval_cst"
external is_ite_cst :
Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t -> 'a option
= "camlidl_cudd_avdd_is_ite_cst"
external size : 'a Cudd.Vdd.t -> int = "camlidl_cudd_bdd_size"
external nbpaths : 'a Cudd.Vdd.t -> float = "camlidl_cudd_bdd_nbpaths"
external nbnonzeropaths : 'a Cudd.Vdd.t -> float
= "camlidl_cudd_bdd_nbtruepaths"
external nbminterms : int -> 'a Cudd.Vdd.t -> float
= "camlidl_cudd_bdd_nbminterms"
external density : int -> 'a Cudd.Vdd.t -> float
= "camlidl_cudd_bdd_density"
external nbleaves : 'a Cudd.Vdd.t -> int = "camlidl_cudd_add_nbleaves"
external varmap : 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t
= "camlidl_cudd_add_varmap"
val permute :
?memo:Cudd.Memo.t -> 'a Cudd.Vdd.t -> int array -> 'a Cudd.Vdd.t
external iter_cube :
(Cudd.Man.tbool array -> 'a -> unit) -> 'a Cudd.Vdd.t -> unit
= "camlidl_cudd_avdd_iter_cube"
external iter_node : ('a Cudd.Vdd.t -> unit) -> 'a Cudd.Vdd.t -> unit
= "camlidl_cudd_iter_node"
external guard_of_node :
'a Cudd.Vdd.t -> 'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t
= "camlidl_cudd_add_guard_of_node"
external guard_of_nonbackground : 'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t
= "camlidl_cudd_add_guard_of_nonbackground"
val nodes_below_level :
?max:int -> 'a Cudd.Vdd.t -> int option -> 'a Cudd.Vdd.t array
external guard_of_leaf : 'a Cudd.Vdd.t -> 'a -> Cudd.Man.v Cudd.Bdd.t
= "camlidl_cudd_avdd_guard_of_leaf"
external leaves : 'a Cudd.Vdd.t -> 'a array = "camlidl_cudd_avdd_leaves"
external pick_leaf : 'a Cudd.Vdd.t -> 'a = "camlidl_cudd_avdd_pick_leaf"
val guardleafs : 'a Cudd.Vdd.t -> (Cudd.Man.v Cudd.Bdd.t * 'a) array
external constrain :
'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Vdd.t
= "camlidl_cudd_add_constrain"
external tdconstrain :
'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Vdd.t
= "camlidl_cudd_add_tdconstrain"
external restrict : 'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Vdd.t
= "camlidl_cudd_add_restrict"
external tdrestrict :
'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Vdd.t
= "camlidl_cudd_add_tdrestrict"
external transfer : 'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Man.t -> 'a Cudd.Vdd.t
= "camlidl_cudd_add_transfer"
val print__minterm :
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a Cudd.Vdd.t -> unit
val print_minterm :
(Format.formatter -> int -> unit) ->
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a Cudd.Vdd.t -> unit
val print :
(Format.formatter -> Cudd.Man.v Cudd.Bdd.t -> unit) ->
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a Cudd.Vdd.t -> unit
end