sig
type t
type add = Leaf of float | Ite of int * Cudd.Add.t * Cudd.Add.t
external manager : Cudd.Add.t -> Cudd.Man.dt = "camlidl_cudd_bdd_manager"
external is_cst : Cudd.Add.t -> bool = "camlidl_cudd_bdd_is_cst"
external topvar : Cudd.Add.t -> int = "camlidl_cudd_bdd_topvar"
external dthen : Cudd.Add.t -> Cudd.Add.t = "camlidl_cudd_add_dthen"
external delse : Cudd.Add.t -> Cudd.Add.t = "camlidl_cudd_add_delse"
external dval : Cudd.Add.t -> float = "camlidl_cudd_avdd_dval"
external cofactors : int -> Cudd.Add.t -> Cudd.Add.t * Cudd.Add.t
= "camlidl_cudd_add_cofactors"
external cofactor : Cudd.Add.t -> Cudd.Bdd.dt -> Cudd.Add.t
= "camlidl_cudd_add_cofactor"
external inspect : Cudd.Add.t -> Cudd.Add.add = "camlidl_cudd_avdd_inspect"
external support : Cudd.Add.t -> Cudd.Bdd.dt = "camlidl_cudd_bdd_support"
external supportsize : Cudd.Add.t -> int = "camlidl_cudd_bdd_supportsize"
external is_var_in : int -> Cudd.Add.t -> bool
= "camlidl_cudd_bdd_is_var_in"
external vectorsupport : Cudd.Add.t array -> Cudd.Bdd.dt
= "camlidl_cudd_bdd_vectorsupport"
external vectorsupport2 :
Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Bdd.dt
= "camlidl_cudd_add_vectorsupport2"
external cst : Cudd.Man.dt -> float -> Cudd.Add.t = "camlidl_cudd_avdd_cst"
val background : Cudd.Man.dt -> Cudd.Add.t
external ite : Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_ite"
external ite_cst :
Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t option
= "camlidl_cudd_add_ite_cst"
external eval_cst : Cudd.Add.t -> Cudd.Bdd.dt -> Cudd.Add.t option
= "camlidl_cudd_add_eval_cst"
external compose : int -> Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_compose"
val vectorcompose :
?memo:Cudd.Memo.t -> Cudd.Bdd.dt array -> Cudd.Add.t -> Cudd.Add.t
external varmap : Cudd.Add.t -> Cudd.Add.t = "camlidl_cudd_add_varmap"
val permute : ?memo:Cudd.Memo.t -> Cudd.Add.t -> int array -> Cudd.Add.t
external is_equal : Cudd.Add.t -> Cudd.Add.t -> bool
= "camlidl_cudd_bdd_is_equal"
external is_equal_when : Cudd.Add.t -> Cudd.Add.t -> Cudd.Bdd.dt -> bool
= "camlidl_cudd_bdd_is_equal_when"
external is_eval_cst : Cudd.Add.t -> Cudd.Bdd.dt -> float option
= "camlidl_cudd_avdd_is_eval_cst"
external is_ite_cst :
Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t -> float option
= "camlidl_cudd_avdd_is_ite_cst"
external size : Cudd.Add.t -> int = "camlidl_cudd_bdd_size"
external nbpaths : Cudd.Add.t -> float = "camlidl_cudd_bdd_nbpaths"
external nbnonzeropaths : Cudd.Add.t -> float
= "camlidl_cudd_bdd_nbtruepaths"
external nbminterms : int -> Cudd.Add.t -> float
= "camlidl_cudd_bdd_nbminterms"
external density : int -> Cudd.Add.t -> float = "camlidl_cudd_bdd_density"
external nbleaves : Cudd.Add.t -> int = "camlidl_cudd_add_nbleaves"
external iter_cube :
(Cudd.Man.tbool array -> float -> unit) -> Cudd.Add.t -> unit
= "camlidl_cudd_avdd_iter_cube"
external iter_node : (Cudd.Add.t -> unit) -> Cudd.Add.t -> unit
= "camlidl_cudd_iter_node"
external guard_of_node : Cudd.Add.t -> Cudd.Add.t -> Cudd.Bdd.dt
= "camlidl_cudd_add_guard_of_node"
external guard_of_nonbackground : Cudd.Add.t -> Cudd.Bdd.dt
= "camlidl_cudd_add_guard_of_nonbackground"
external nodes_below_level :
Cudd.Add.t -> int option -> int -> Cudd.Add.t array
= "camlidl_cudd_avdd_nodes_below_level"
external guard_of_leaf : Cudd.Add.t -> float -> Cudd.Bdd.dt
= "camlidl_cudd_avdd_guard_of_leaf"
external leaves : Cudd.Add.t -> float array = "camlidl_cudd_avdd_leaves"
external pick_leaf : Cudd.Add.t -> float = "camlidl_cudd_avdd_pick_leaf"
val guardleafs : Cudd.Add.t -> (Cudd.Bdd.dt * float) array
external constrain : Cudd.Add.t -> Cudd.Bdd.dt -> Cudd.Add.t
= "camlidl_cudd_add_constrain"
external tdconstrain : Cudd.Add.t -> Cudd.Bdd.dt -> Cudd.Add.t
= "camlidl_cudd_add_tdconstrain"
external restrict : Cudd.Add.t -> Cudd.Bdd.dt -> Cudd.Add.t
= "camlidl_cudd_add_restrict"
external tdrestrict : Cudd.Add.t -> Cudd.Bdd.dt -> Cudd.Add.t
= "camlidl_cudd_add_tdrestrict"
external of_bdd : Cudd.Bdd.dt -> Cudd.Add.t = "camlidl_cudd_add_of_bdd"
external to_bdd : Cudd.Add.t -> Cudd.Bdd.dt = "camlidl_cudd_add_to_bdd"
external to_bdd_threshold : float -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_to_bdd_threshold"
external to_bdd_strictthreshold : float -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_to_bdd_strictthreshold"
external to_bdd_interval : float -> float -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_to_bdd_interval"
external exist : Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_exist"
external forall : Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_forall"
external is_leq : Cudd.Add.t -> Cudd.Add.t -> bool
= "camlidl_cudd_add_is_leq"
external add : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_add"
external sub : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_sub"
external mul : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_mul"
external div : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_div"
external min : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_min"
external max : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_max"
external agreement : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_agreement"
external diff : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_diff"
external threshold : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_threshold"
external setNZ : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_setNZ"
external log : Cudd.Add.t -> Cudd.Add.t = "camlidl_cudd_add_log"
external matrix_multiply :
int array -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_matrix_multiply"
external times_plus : int array -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_times_plus"
external triangle : int array -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
= "camlidl_cudd_add_triangle"
val mapleaf1 :
default:Cudd.Add.t ->
(Cudd.Bdd.dt -> float -> float) -> Cudd.Add.t -> Cudd.Add.t
val mapleaf2 :
default:Cudd.Add.t ->
(Cudd.Bdd.dt -> float -> float -> float) ->
Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
type op1 = (float, float) Cudd.Custom.op1
type op2 = (float, float, float) Cudd.Custom.op2
type op3 = (float, float, float, float) Cudd.Custom.op3
type opN = {
commonN : Cudd.Custom.common;
closureN : Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Add.t option;
arityNbdd : int;
}
type opG = {
commonG : Cudd.Custom.common;
arityGbdd : int;
closureG : Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Add.t option;
oclosureBeforeRec :
(int * bool ->
Cudd.Bdd.dt array ->
Cudd.Add.t array -> Cudd.Bdd.dt array * Cudd.Add.t array)
option;
oclosureIte : (int -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t) option;
}
type test2 = (float, float) Cudd.Custom.test2
type exist = float Cudd.Custom.exist
type existand = float Cudd.Custom.existand
type existop1 = (float, float) Cudd.Custom.existop1
type existandop1 = (float, float) Cudd.Custom.existandop1
val make_op1 : ?memo:Cudd.Memo.t -> (float -> float) -> Cudd.Add.op1
val make_op2 :
?memo:Cudd.Memo.t ->
?commutative:bool ->
?idempotent:bool ->
?special:(Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t option) ->
(float -> float -> float) -> Cudd.Add.op2
val make_op3 :
?memo:Cudd.Memo.t ->
?special:(Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t option) ->
(float -> float -> float -> float) -> Cudd.Add.op3
val make_opN :
?memo:Cudd.Memo.t ->
int ->
int ->
(Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Add.t option) ->
Cudd.Add.opN
val make_opG :
?memo:Cudd.Memo.t ->
?beforeRec:(int * bool ->
Cudd.Bdd.dt array ->
Cudd.Add.t array -> Cudd.Bdd.dt array * Cudd.Add.t array) ->
?ite:(int -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t) ->
int ->
int ->
(Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Add.t option) ->
Cudd.Add.opG
val make_test2 :
?memo:Cudd.Memo.t ->
?symetric:bool ->
?reflexive:bool ->
?special:(Cudd.Add.t -> Cudd.Add.t -> bool option) ->
(float -> float -> bool) -> Cudd.Add.test2
val make_exist : ?memo:Cudd.Memo.t -> Cudd.Add.op2 -> Cudd.Add.exist
val make_existand :
?memo:Cudd.Memo.t -> bottom:float -> Cudd.Add.op2 -> Cudd.Add.existand
val make_existop1 :
?memo:Cudd.Memo.t ->
op1:Cudd.Add.op1 -> Cudd.Add.op2 -> Cudd.Add.existop1
val make_existandop1 :
?memo:Cudd.Memo.t ->
op1:Cudd.Add.op1 -> bottom:float -> Cudd.Add.op2 -> Cudd.Add.existandop1
val clear_op1 : Cudd.Add.op1 -> unit
val clear_op2 : Cudd.Add.op2 -> unit
val clear_op3 : Cudd.Add.op3 -> unit
val clear_opN : Cudd.Add.opN -> unit
val clear_opG : Cudd.Add.opG -> unit
val clear_test2 : Cudd.Add.test2 -> unit
val clear_exist : Cudd.Add.exist -> unit
val clear_existand : Cudd.Add.existand -> unit
val clear_existop1 : Cudd.Add.existop1 -> unit
val clear_existandop1 : Cudd.Add.existandop1 -> unit
val apply_op1 : Cudd.Add.op1 -> Cudd.Add.t -> Cudd.Add.t
val apply_op2 : Cudd.Add.op2 -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
val apply_op3 : Cudd.Add.op3 -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
val apply_opN :
Cudd.Add.opN -> Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Add.t
val apply_opG :
Cudd.Add.opG -> Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Add.t
val apply_test2 : Cudd.Add.test2 -> Cudd.Add.t -> Cudd.Add.t -> bool
val apply_exist :
Cudd.Add.exist -> supp:Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t
val apply_existand :
Cudd.Add.existand ->
supp:Cudd.Bdd.dt -> Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t
val apply_existop1 :
Cudd.Add.existop1 -> supp:Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t
val apply_existandop1 :
Cudd.Add.existandop1 ->
supp:Cudd.Bdd.dt -> Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t
val map_op1 :
?memo:Cudd.Memo.t -> (float -> float) -> Cudd.Add.t -> Cudd.Add.t
val map_op2 :
?memo:Cudd.Memo.t ->
?commutative:bool ->
?idempotent:bool ->
?special:(Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t option) ->
(float -> float -> float) -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
val map_op3 :
?memo:Cudd.Memo.t ->
?special:(Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t option) ->
(float -> float -> float -> float) ->
Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
val map_opN :
?memo:Cudd.Memo.t ->
(Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Add.t option) ->
Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Add.t
val map_test2 :
?memo:Cudd.Memo.t ->
?symetric:bool ->
?reflexive:bool ->
?special:(Cudd.Add.t -> Cudd.Add.t -> bool option) ->
(float -> float -> bool) -> Cudd.Add.t -> Cudd.Add.t -> bool
external transfer : Cudd.Add.t -> Cudd.Man.d Cudd.Man.t -> Cudd.Add.t
= "camlidl_cudd_add_transfer"
external _print : Cudd.Add.t -> unit = "camlidl_cudd_print"
val print__minterm : Format.formatter -> Cudd.Add.t -> unit
val print_minterm :
(Format.formatter -> int -> unit) ->
(Format.formatter -> float -> unit) ->
Format.formatter -> Cudd.Add.t -> unit
val print :
(Format.formatter -> int -> unit) ->
(Format.formatter -> float -> unit) ->
Format.formatter -> Cudd.Add.t -> unit
end