bddapron 2.2.4 · OCaml Package

type !'a typdef = 'a Bdd.Env.typdef

type !'a typ = [

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

]

type !'a symbol = 'a Bdd.Env.symbol = {

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

}

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

mutable table : 'a Apronexpr.t Cudd.Mtbdd.table;
mutable eapron : Apron.Environment.t;
mutable aext : 'b;

}

type (!'a, !'b, !'c, !'d) t0 =
  ('a, 'b, 'c, Cudd.Man.v, ('a, 'd) ext) Bdd.Env.t0

module O : sig ... end

type !'a t = ('a, 'a typ, 'a typdef, 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_idcondb : 
  ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t ->
  Format.formatter ->
  (int * bool) ->
  unit

val print_order : 
  ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t ->
  Format.formatter ->
  unit

val print : 
  Format.formatter ->
  ('a, [> 'a typ ], [> 'a typdef ], 'd) 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 ->
  Cudd.Man.vt ->
  'a t

val make_string : 
  ?bddindex0:int ->
  ?bddsize:int ->
  ?relational:bool ->
  Cudd.Man.vt ->
  string t

val copy : 
  ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t ->
  ('a, 'b, 'c, 'd) O.t

val copy_ext : copy_aext:('b -> 'c) -> ('a, 'b) ext -> ('a, 'c) ext

val mem_typ : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> 'a -> bool

val mem_var : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> 'a -> bool

val mem_label : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> 'a -> bool

val typdef_of_typ : ('a, [> 'a typ ], [> 'a typdef ] as 'b, 'd) O.t -> 'a -> 'b

val typ_of_var : ('a, [> 'a typ ] as 'b, [> 'a typdef ], 'd) O.t -> 'a -> 'b

val vars : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> 'a PSette.t

val labels : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> 'a PSette.t

val apron : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> Apron.Environment.t

val add_typ_with : 
  ('a, [> 'a typ ], [> 'a typdef ] as 'b, 'd) O.t ->
  'a ->
  'b ->
  unit

val add_vars_with : 
  ('a, [> 'a typ ] as 'b, [> 'a typdef ], 'd) O.t ->
  ('a * 'b) list ->
  int array option

val remove_vars_with : 
  ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t ->
  'a list ->
  int array option

val rename_vars_with : 
  ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t ->
  ('a * 'a) list ->
  int array option * Apron.Dim.perm option

val add_typ : 
  ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t ->
  'a ->
  'c ->
  ('a, 'b, 'c, 'd) O.t

val add_vars : 
  ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t ->
  ('a * 'b) list ->
  ('a, 'b, 'c, 'd) O.t

val remove_vars : 
  ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t ->
  'a list ->
  ('a, 'b, 'c, 'd) O.t

val rename_vars : 
  ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t ->
  ('a * 'a) list ->
  ('a, 'b, 'c, 'd) O.t

val is_leq : 
  ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t ->
  ('a, 'b, 'c, 'd) O.t ->
  bool

val is_eq : 
  ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t ->
  ('a, 'b, 'c, 'd) O.t ->
  bool

val lce : 
  ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t ->
  ('a, 'b, 'c, 'd) O.t ->
  ('a, 'b, 'c, 'd) O.t

type change = {

cbdd : Cudd.Man.v Bdd.Env.change;
capron : Apron.Dim.change2;

}

val compute_change : 
  ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t ->
  ('a, 'b, 'c, 'd) O.t ->
  change

type (!'a, !'b) value = ('a, 'b) Bdd.Env.value = {

env : 'a;
val0 : 'b;

}

val make_value : 
  ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t ->
  'e ->
  (('a, 'b, 'c, 'd) O.t, 'e) value

val get_env : ('a, 'b) value -> 'a

val get_val0 : ('a, 'b) value -> 'b

val check_var : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> 'a -> unit

val check_lvar : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> 'a list -> unit

val check_value : 
  ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t ->
  (('a, 'b, 'c, 'd) O.t, 'e) value ->
  unit

val check_value2 : 
  (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t, 'e) value ->
  (('a, 'b, 'c, 'd) O.t, 'f) value ->
  unit

val check_value3 : 
  (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t, 'e) value ->
  (('a, 'b, 'c, 'd) O.t, 'f) value ->
  (('a, 'b, 'c, 'd) O.t, 'g) value ->
  unit

val check_lvarvalue : 
  ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t ->
  ('a * (('a, 'b, 'c, 'd) O.t, 'e) value) list ->
  ('a * 'e) list

val check_lvalue : 
  ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t ->
  (('a, 'b, 'c, 'd) O.t, 'e) value list ->
  'e list

val check_ovalue : 
  ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t ->
  (('a, 'b, 'c, 'd) O.t, 'e) value option ->
  'e option

val mapunop : 
  ('e -> 'f) ->
  (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t, 'e) value ->
  (('a, 'b, 'c, 'd) O.t, 'f) value

val mapbinop : 
  ('e -> 'f -> 'g) ->
  (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t, 'e) value ->
  (('a, 'b, 'c, 'd) O.t, 'f) value ->
  (('a, 'b, 'c, 'd) O.t, 'g) value

val mapbinope : 
  (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t -> 'e -> 'f -> 'g) ->
  (('a, 'b, 'c, 'd) O.t, 'e) value ->
  (('a, 'b, 'c, 'd) O.t, 'f) value ->
  (('a, 'b, 'c, 'd) O.t, 'g) value

val mapterop : 
  ('e -> 'f -> 'g -> 'h) ->
  (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t, 'e) value ->
  (('a, 'b, 'c, 'd) O.t, 'f) value ->
  (('a, 'b, 'c, 'd) O.t, 'g) value ->
  (('a, 'b, 'c, 'd) O.t, 'h) value

val var_of_aprondim : 
  ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t ->
  Apron.Dim.t ->
  'a

val aprondim_of_var : 
  ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t ->
  'a ->
  Apron.Dim.t

val string_of_aprondim : 
  ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t ->
  Apron.Dim.t ->
  string

package bddapron