package bddapron

  1. Overview
  2. Docs
exception Bddindex
type !'a typdef = [
  1. | `Benum of 'a array
]
type !'a typ = [
  1. | `Benum of 'a
  2. | `Bint of bool * int
  3. | `Bool
]
type 'a group_tree
type !'a symbol = {
  1. compare : 'a -> 'a -> int;
  2. marshal : 'a -> string;
  3. unmarshal : string -> 'a;
  4. mutable print : Format.formatter -> 'a -> unit;
}
type (!'a, !'b, !'c, !'d, !'e) t0 = {
  1. mutable cudd : 'd Cudd.Man.t;
  2. mutable typdef : ('a, 'c) PMappe.t;
  3. mutable vartyp : ('a, 'b) PMappe.t;
  4. mutable bddindex0 : int;
  5. mutable bddsize : int;
  6. mutable bddindex : int;
  7. mutable bddincr : int;
  8. mutable idcondvar : (int, 'a) PMappe.t;
  9. mutable vartid : ('a, int array) PMappe.t;
  10. mutable groups : 'a group_tree list;
  11. mutable print_external_idcondb : Format.formatter -> (int * bool) -> unit;
  12. mutable ext : 'e;
  13. symbol : 'a symbol;
  14. copy_ext : 'e -> 'e;
}
module O : sig ... end
type (!'a, !'d) t = ('a, 'a typ, 'a typdef, 'd, unit) O.t
val print_typ : (Format.formatter -> 'a -> unit) -> Format.formatter -> [> 'a typ ] -> unit
val print_typdef : (Format.formatter -> 'a -> unit) -> Format.formatter -> [> 'a typdef ] -> unit
val print_tid : Format.formatter -> int array -> unit
val print_idcondb : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> Format.formatter -> (int * bool) -> unit
val print_order : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> Format.formatter -> unit
val print : Format.formatter -> ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> unit
val marshal : 'a -> string
val unmarshal : string -> 'a
val make_symbol : ?compare:('a -> 'a -> int) -> ?marshal:('a -> string) -> ?unmarshal:(string -> 'a) -> (Format.formatter -> 'a -> unit) -> 'a symbol
val string_symbol : string symbol
val make : symbol:'a symbol -> ?bddindex0:int -> ?bddsize:int -> ?relational:bool -> 'd Cudd.Man.t -> ('a, 'd) t
val make_string : ?bddindex0:int -> ?bddsize:int -> ?relational:bool -> 'd Cudd.Man.t -> (string, 'd) t
val copy : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> ('a, 'b, 'c, 'd, 'e) O.t
val mem_typ : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> 'a -> bool
val mem_var : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> 'a -> bool
val mem_label : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> 'a -> bool
val typdef_of_typ : ('a, [> 'a typ ], [> 'a typdef ] as 'b, 'd, 'e) O.t -> 'a -> 'b
val typ_of_var : ('a, [> 'a typ ] as 'b, [> 'a typdef ], 'd, 'e) O.t -> 'a -> 'b
val vars : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> 'a PSette.t
val labels : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> 'a PSette.t
val add_typ_with : ('a, [> 'a typ ], [> 'a typdef ] as 'b, 'd, 'e) O.t -> 'a -> 'b -> unit
type packing = [
  1. | `None
  2. | `Normalize
  3. | `Pack
]
val add_vars_with : ('a, [> 'a typ ] as 'b, [> 'a typdef ], 'd, 'e) O.t -> ?booking_factor:int -> ?packing:packing -> ('a * 'b) list -> int array option
val remove_vars_with : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> 'a list -> int array option
val rename_vars_with : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> ('a * 'a) list -> int array option
val add_typ : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> 'a -> 'c -> ('a, 'b, 'c, 'd, 'e) O.t
val add_vars : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> ('a * 'b) list -> ('a, 'b, 'c, 'd, 'e) O.t
val remove_vars : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> 'a list -> ('a, 'b, 'c, 'd, 'e) O.t
val rename_vars : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> ('a * 'a) list -> ('a, 'b, 'c, 'd, 'e) O.t
val add_var_with : ('a, [> 'a typ ] as 'b, [> 'a typdef ], 'd, 'e) O.t -> ?booking_factor:int -> 'a -> 'b -> unit
val extend_with : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> int -> unit
type !'a group_tree_spec = [
  1. | `Fixed of 'a group_tree_spec list
  2. | `Reord of 'a group_tree_spec list
  3. | `Var of 'a
]
val group_vars_with : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> 'a group_tree_spec list -> int array
val iter_ordered : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> ('a -> int array -> unit) -> unit
val is_leq : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> ('a, 'b, 'c, 'd, 'e) O.t -> bool
val is_eq : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> ('a, 'b, 'c, 'd, 'e) O.t -> bool
val shift : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> int -> ('a, 'b, 'c, 'd, 'e) O.t
val lce : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> ('a, 'b, 'c, 'd, 'e) O.t -> ('a, 'b, 'c, 'd, 'e) O.t
val permutation12 : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> ('a, 'b, 'c, 'd, 'e) O.t -> int array
val permutation21 : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> ('a, 'b, 'c, 'd, 'e) O.t -> int array
type !'a change = {
  1. intro : int array option;
  2. remove : ('a Cudd.Bdd.t * int array) option;
}
val compute_change : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> ('a, 'b, 'c, 'd, 'e) O.t -> 'd change
val notfound : ('a, Format.formatter, unit, 'b) format4 -> 'a
type (!'a, !'b) value = {
  1. env : 'a;
  2. val0 : 'b;
}
val make_value : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> 'f -> (('a, 'b, 'c, 'd, 'e) O.t, 'f) value
val get_env : ('a, 'b) value -> 'a
val get_val0 : ('a, 'b) value -> 'b
val extend_environment : ('f -> int array -> 'f) -> (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t, 'f) value -> ('a, 'b, 'c, 'd, 'e) O.t -> (('a, 'b, 'c, 'd, 'e) O.t, 'f) value
val compare_idb : (int * bool) -> (int * bool) -> int
val pack_with : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> int array
val normalize_with : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> int array
val check_normalized : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> bool
val compose_permutation : int array -> int array -> int array
val compose_opermutation : int array option -> int array option -> int array option
val permutation_of_offset : int -> int -> int array
val check_var : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> 'a -> unit
val check_lvar : ('a, [> 'a typ ], [> 'a typdef ], 'd, 'e) O.t -> 'a list -> unit
val check_value : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> (('a, 'b, 'c, 'd, 'e) O.t, 'f) value -> unit
val check_value2 : (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t, 'f) value -> (('a, 'b, 'c, 'd, 'e) O.t, 'g) value -> unit
val check_value3 : (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t, 'f) value -> (('a, 'b, 'c, 'd, 'e) O.t, 'g) value -> (('a, 'b, 'c, 'd, 'e) O.t, 'h) value -> unit
val check_lvarvalue : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> ('a * (('a, 'b, 'c, 'd, 'e) O.t, 'f) value) list -> ('a * 'f) list
val check_lvalue : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> (('a, 'b, 'c, 'd, 'e) O.t, 'f) value list -> 'f list
val check_ovalue : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> (('a, 'b, 'c, 'd, 'e) O.t, 'f) value option -> 'f option
val mapunop : ('f -> 'g) -> (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t, 'f) value -> (('a, 'b, 'c, 'd, 'e) O.t, 'g) value
val mapbinop : ('f -> 'g -> 'h) -> (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t, 'f) value -> (('a, 'b, 'c, 'd, 'e) O.t, 'g) value -> (('a, 'b, 'c, 'd, 'e) O.t, 'h) value
val mapbinope : (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t -> 'f -> 'g -> 'h) -> (('a, 'b, 'c, 'd, 'e) O.t, 'f) value -> (('a, 'b, 'c, 'd, 'e) O.t, 'g) value -> (('a, 'b, 'c, 'd, 'e) O.t, 'h) value
val mapterop : ('f -> 'g -> 'h -> 'i) -> (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd, 'e) O.t, 'f) value -> (('a, 'b, 'c, 'd, 'e) O.t, 'g) value -> (('a, 'b, 'c, 'd, 'e) O.t, 'h) value -> (('a, 'b, 'c, 'd, 'e) O.t, 'i) value