mlcuddidl 3.0.8 · OCaml Package

type !'a capsule = private {

content : 'a;

}

type 'a unique

type 'a t = 'a unique Vdd.t

type 'a table = 'a unique PWeakke.t

val print_table : 
  ?first:(unit, Format.formatter, unit) format ->
  ?sep:(unit, Format.formatter, unit) format ->
  ?last:(unit, Format.formatter, unit) 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 'a unique
| Ite of int * 'a t * 'a t

val manager : 'a t -> Man.v 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 -> Man.v Bdd.t -> 'a t

val dval_u : 'a t -> 'a unique

val dval : 'a t -> 'a

val inspect : 'a t -> 'a mtbdd

val support : 'a t -> Man.v Bdd.t

val supportsize : 'a t -> int

val is_var_in : int -> 'a t -> bool

val vectorsupport : 'a t array -> Man.v Bdd.t

val vectorsupport2 : Man.v Bdd.t array -> 'a t array -> Man.v Bdd.t

val cst_u : Man.v Man.t -> 'a unique -> 'a t

val cst : Man.v Man.t -> 'a table -> 'a -> 'a t

val ite : Man.v Bdd.t -> 'a t -> 'a t -> 'a t

val ite_cst : Man.v Bdd.t -> 'a t -> 'a t -> 'a t option

val eval_cst : 'a t -> Man.v Bdd.t -> 'a t option

val compose : int -> Man.v Bdd.t -> 'a t -> 'a t

val vectorcompose : Man.v Bdd.t array -> 'a t -> 'a t

val is_equal : 'a t -> 'a t -> bool

val is_equal_when : 'a t -> 'a t -> Man.v Bdd.t -> bool

val is_eval_cst_u : 'a t -> Man.v Bdd.t -> 'a unique option

val is_ite_cst_u : Man.v Bdd.t -> 'a t -> 'a t -> 'a unique option

val is_eval_cst : 'a t -> Man.v Bdd.t -> 'a option

val is_ite_cst : Man.v 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 : (Man.tbool array -> 'a unique -> unit) -> 'a t -> unit

val iter_cube : (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 -> Man.v Bdd.t

val guard_of_nonbackground : 'a t -> Man.v Bdd.t

val nodes_below_level : ?max:int -> 'a t -> int option -> 'a t array

val guard_of_leaf_u : 'a t -> 'a unique -> Man.v Bdd.t

val guard_of_leaf : 'a table -> 'a t -> 'a -> Man.v Bdd.t

val leaves_u : 'a t -> 'a unique array

val leaves : 'a t -> 'a array

val pick_leaf_u : 'a t -> 'a unique

val pick_leaf : 'a t -> 'a

val guardleafs_u : 'a t -> (Man.v Bdd.t * 'a unique) array

val guardleafs : 'a t -> (Man.v Bdd.t * 'a) array

val fold_guardleaves_u : 
  (Man.v Bdd.t -> 'a unique -> 'b -> 'b) ->
  'a t ->
  'b ->
  'b

val fold_guardleaves : (Man.v Bdd.t -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b

val constrain : 'a t -> Man.v Bdd.t -> 'a t

val tdconstrain : 'a t -> Man.v Bdd.t -> 'a t

val restrict : 'a t -> Man.v Bdd.t -> 'a t

val tdrestrict : 'a t -> Man.v Bdd.t -> 'a t

val transfer : 'a t -> Man.v 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 -> Man.v Bdd.t -> unit) ->
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  'a t ->
  unit

package mlcuddidl