bddapron 2.3.1 · OCaml Package

exception Bddindex

type !'a typdef = [

| `Benum of 'a array

]

type !'a typ = [

| `Benum of 'a
| `Bint of bool * int
| `Bool

]

type 'a group_tree

type !'a symbol = {

compare : 'a -> 'a -> int;
marshal : 'a -> string;
unmarshal : string -> 'a;
mutable print : Format.formatter -> 'a -> unit;

}

type (!'a, !'b, !'c, !'d, !'e) t0 = {

mutable cudd : 'd Cudd.Man.t;
mutable typdef : ('a, 'c) PMappe.t;
mutable vartyp : ('a, 'b) PMappe.t;
mutable bddindex0 : int;
mutable bddsize : int;
mutable bddindex : int;
mutable bddincr : int;
mutable idcondvar : (int, 'a) PMappe.t;
mutable vartid : ('a, int array) PMappe.t;
mutable groups : 'a group_tree list;
mutable print_external_idcondb : Format.formatter -> (int * bool) -> unit;
mutable ext : 'e;
symbol : 'a symbol;
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 = [

| `None
| `Normalize
| `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 = [

| `Fixed of 'a group_tree_spec list
| `Reord of 'a group_tree_spec list
| `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 = {

intro : int array option;
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) Pervasives.format4 -> 'a

type (!'a, !'b) value = {

env : 'a;
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

package bddapron