sig
type 'a t
type 'a bdd = Bool of bool | Ite of int * 'a Cudd.Bdd.t * 'a Cudd.Bdd.t
type dt = Cudd.Man.d Cudd.Bdd.t
type vt = Cudd.Man.v Cudd.Bdd.t
external manager : 'a Cudd.Bdd.t -> 'a Cudd.Man.t
= "camlidl_cudd_bdd_manager"
external is_cst : 'a Cudd.Bdd.t -> bool = "camlidl_cudd_bdd_is_cst"
external is_complement : 'a Cudd.Bdd.t -> bool
= "camlidl_cudd_bdd_is_complement"
external topvar : 'a Cudd.Bdd.t -> int = "camlidl_cudd_bdd_topvar"
external dthen : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t = "camlidl_cudd_bdd_dthen"
external delse : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t = "camlidl_cudd_bdd_delse"
external cofactors : int -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t * 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_cofactors"
external cofactor : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_cofactor"
external inspect : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.bdd
= "camlidl_cudd_bdd_inspect"
external support : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_support"
external supportsize : 'a Cudd.Bdd.t -> int
= "camlidl_cudd_bdd_supportsize"
external is_var_in : int -> 'a Cudd.Bdd.t -> bool
= "camlidl_cudd_bdd_is_var_in"
external vectorsupport : 'a Cudd.Bdd.t array -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_vectorsupport"
external support_inter : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_support_inter"
external support_union : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_dand"
external support_diff : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_cofactor"
external list_of_support : 'a Cudd.Bdd.t -> int list
= "camlidl_cudd_list_of_support"
external dtrue : 'a Cudd.Man.t -> 'a Cudd.Bdd.t = "camlidl_cudd_bdd_dtrue"
external dfalse : 'a Cudd.Man.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_dfalse"
external ithvar : 'a Cudd.Man.t -> int -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_ithvar"
external newvar : 'a Cudd.Man.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_newvar"
external newvar_at_level : 'a Cudd.Man.t -> int -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_newvar_at_level"
external is_true : 'a Cudd.Bdd.t -> bool = "camlidl_cudd_bdd_is_true"
external is_false : 'a Cudd.Bdd.t -> bool = "camlidl_cudd_bdd_is_false"
external is_equal : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> bool
= "camlidl_cudd_bdd_is_equal"
external is_leq : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> bool
= "camlidl_cudd_bdd_is_leq"
external is_inter_empty : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> bool
= "camlidl_cudd_bdd_is_inter_empty"
external is_equal_when :
'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> bool
= "camlidl_cudd_bdd_is_equal_when"
external is_leq_when :
'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> bool
= "camlidl_cudd_bdd_is_leq_when"
val is_included_in : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> bool
external is_ite_cst :
'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> bool option
= "camlidl_cudd_bdd_is_ite_cst"
external is_var_dependent : int -> 'a Cudd.Bdd.t -> bool
= "camlidl_cudd_bdd_is_var_dependent"
external is_var_essential : int -> bool -> 'a Cudd.Bdd.t -> bool
= "camlidl_cudd_bdd_is_var_essential"
external size : 'a Cudd.Bdd.t -> int = "camlidl_cudd_bdd_size"
external nbpaths : 'a Cudd.Bdd.t -> float = "camlidl_cudd_bdd_nbpaths"
external nbtruepaths : 'a Cudd.Bdd.t -> float
= "camlidl_cudd_bdd_nbtruepaths"
external nbminterms : int -> 'a Cudd.Bdd.t -> float
= "camlidl_cudd_bdd_nbminterms"
external density : int -> 'a Cudd.Bdd.t -> float
= "camlidl_cudd_bdd_density"
external dnot : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t = "camlidl_cudd_bdd_dnot"
external dand : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_dand"
external dor : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_dor"
external xor : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_xor"
external nand : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_nand"
external nor : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_nor"
external nxor : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_nxor"
val eq : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
external ite :
'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_ite"
external ite_cst :
'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t option
= "camlidl_cudd_bdd_ite_cst"
external compose : int -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_compose"
val vectorcompose :
?memo:Cudd.Memo.t ->
'a Cudd.Bdd.t array -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
external intersect : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_intersect"
external varmap : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_varmap"
val permute :
?memo:Cudd.Memo.t -> 'a Cudd.Bdd.t -> int array -> 'a Cudd.Bdd.t
external iter_node : ('a Cudd.Bdd.t -> unit) -> 'a Cudd.Bdd.t -> unit
= "camlidl_cudd_iter_node"
external iter_cube :
(Cudd.Man.tbool array -> unit) -> 'a Cudd.Bdd.t -> unit
= "camlidl_cudd_bdd_iter_cube"
external iter_prime :
(Cudd.Man.tbool array -> unit) -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> unit
= "camlidl_cudd_bdd_iter_prime"
external exist : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_exist"
external forall : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_forall"
external existand :
'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_existand"
external existxor :
'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_existxor"
external booleandiff : 'a Cudd.Bdd.t -> int -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_booleandiff"
external cube_of_bdd : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_cube_of_bdd"
external cube_of_minterm :
'a Cudd.Man.t -> Cudd.Man.tbool array -> 'a Cudd.Bdd.t
= "camlidl_cudd_cube_of_minterm"
external list_of_cube : 'a Cudd.Bdd.t -> (int * bool) list
= "camlidl_cudd_list_of_cube"
external cube_union : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_cube_union"
external pick_minterm : 'a Cudd.Bdd.t -> Cudd.Man.tbool array
= "camlidl_cudd_pick_minterm"
external pick_cube_on_support :
'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_pick_cube_on_support"
external pick_cubes_on_support :
'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> int -> 'a Cudd.Bdd.t array
= "camlidl_cudd_pick_cubes_on_support"
external constrain : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_constrain"
external tdconstrain : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_tdconstrain"
external restrict : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_restrict"
external tdrestrict : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_tdrestrict"
external minimize : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_minimize"
external licompaction : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_licompaction"
external squeeze : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_squeeze"
external clippingand :
'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> int -> bool -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_clippingand"
external clippingexistand :
'a Cudd.Bdd.t ->
'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> int -> bool -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_clippingexistand"
external underapprox :
int -> int -> bool -> float -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_underapprox"
external overapprox :
int -> int -> bool -> float -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_overapprox"
external remapunderapprox :
int -> int -> float -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_remapunderapprox"
external remapoverapprox :
int -> int -> float -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_remapoverapprox"
external biasedunderapprox :
int ->
int -> float -> float -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_biasedunderapprox_bytecode"
"camlidl_cudd_bdd_biasedunderapprox"
external biasedoverapprox :
int ->
int -> float -> float -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_biasedoverapprox_bytecode"
"camlidl_cudd_bdd_biasedoverapprox"
external subsetcompress : int -> int -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_subsetcompress"
external supersetcompress : int -> int -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_supersetcompress"
external subsetHB : int -> int -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_subsetHB"
external supersetHB : int -> int -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_supersetHB"
external subsetSP : int -> int -> bool -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_subsetSP"
external supersetSP : int -> int -> bool -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
= "camlidl_cudd_bdd_supersetSP"
external approxconjdecomp :
'a Cudd.Bdd.t -> ('a Cudd.Bdd.t * 'a Cudd.Bdd.t) option
= "camlidl_cudd_bdd_approxconjdecomp"
external approxdisjdecomp :
'a Cudd.Bdd.t -> ('a Cudd.Bdd.t * 'a Cudd.Bdd.t) option
= "camlidl_cudd_bdd_approxdisjdecomp"
external iterconjdecomp :
'a Cudd.Bdd.t -> ('a Cudd.Bdd.t * 'a Cudd.Bdd.t) option
= "camlidl_cudd_bdd_iterconjdecomp"
external iterdisjdecomp :
'a Cudd.Bdd.t -> ('a Cudd.Bdd.t * 'a Cudd.Bdd.t) option
= "camlidl_cudd_bdd_iterdisjdecomp"
external genconjdecomp :
'a Cudd.Bdd.t -> ('a Cudd.Bdd.t * 'a Cudd.Bdd.t) option
= "camlidl_cudd_bdd_genconjdecomp"
external gendisjdecomp :
'a Cudd.Bdd.t -> ('a Cudd.Bdd.t * 'a Cudd.Bdd.t) option
= "camlidl_cudd_bdd_gendisjdecomp"
external varconjdecomp :
'a Cudd.Bdd.t -> ('a Cudd.Bdd.t * 'a Cudd.Bdd.t) option
= "camlidl_cudd_bdd_varconjdecomp"
external vardisjdecomp :
'a Cudd.Bdd.t -> ('a Cudd.Bdd.t * 'a Cudd.Bdd.t) option
= "camlidl_cudd_bdd_vardisjdecomp"
external transfer : 'a Cudd.Bdd.t -> 'b Cudd.Man.t -> 'b Cudd.Bdd.t
= "camlidl_cudd_bdd_transfer"
external correlation : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> float
= "camlidl_cudd_bdd_correlation"
external correlationweights :
'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> float array -> float
= "camlidl_cudd_bdd_correlationweights"
external _print : 'a Cudd.Bdd.t -> unit = "camlidl_cudd_print"
val print__minterm : Format.formatter -> 'a Cudd.Bdd.t -> unit
val print_minterm :
(Format.formatter -> int -> unit) ->
Format.formatter -> 'a Cudd.Bdd.t -> unit
val print :
(Format.formatter -> int -> unit) ->
Format.formatter -> 'a Cudd.Bdd.t -> unit
val print_list :
(Format.formatter -> int -> unit) ->
Format.formatter -> (int * bool) list -> unit
end