bddapron 2.2.5 · OCaml Package

val meet_idcondb : 
  ('a, 'b) man ->
  ('a, [> 'a Env.typ ] as 'c, [> 'a Env.typdef ] as 'd, 'e) Env.O.t ->
  ('a, ('a, 'c, 'd, 'e) Env.O.t) Cond.O.t ->
  'b t ->
  (int * bool) ->
  'b t

val size : ('a, 'b) man -> 'b t -> int

val print : 
  ?print_apron:
    ((int -> string) -> Format.formatter -> 'b Apron.Abstract0.t -> unit) ->
  ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'e) Env.O.t ->
  Format.formatter ->
  'b t ->
  unit

val bottom : 
  ('a, 'b) man ->
  ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'e) Env.O.t ->
  'b t

val top : 
  ('a, 'b) man ->
  ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'e) Env.O.t ->
  'b t

val of_apron : 
  ('a, 'b) man ->
  ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'e) Env.O.t ->
  'b Apron.Abstract0.t ->
  'b t

val of_bddapron : 
  ('a, 'b) man ->
  ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'e) Env.O.t ->
  ('a Expr0.Bool.t * 'b Apron.Abstract0.t) list ->
  'b t

val is_bottom : ('a, 'b) man -> 'b t -> bool

val is_top : ('a, 'b) man -> 'b t -> bool

val is_leq : ('a, 'b) man -> 'b t -> 'b t -> bool

val is_eq : ('a, 'b) man -> 'b t -> 'b t -> bool

val to_bddapron : 
  ('a, 'b) man ->
  'b t ->
  ('a Expr0.Bool.t * 'b Apron.Abstract0.t) list

val meet : ('a, 'b) man -> 'b t -> 'b t -> 'b t

val join : ('a, 'b) man -> 'b t -> 'b t -> 'b t

val meet_cube : 
  ('a, 'b) man ->
  ('a, [> 'a Env.typ ] as 'c, [> 'a Env.typdef ] as 'd, 'e) Env.O.t ->
  ('a, ('a, 'c, 'd, 'e) Env.O.t) Cond.O.t ->
  'b t ->
  'b t ->
  'a Expr0.Bool.t ->
  'b t

val meet_condition : 
  ('a, 'b) man ->
  ('a, [> 'a Env.typ ] as 'c, [> 'a Env.typdef ] as 'd, 'e) Env.O.t ->
  ('a, ('a, 'c, 'd, 'e) Env.O.t) Cond.O.t ->
  'b t ->
  'a Expr0.Bool.t ->
  'b t

val assign_lexpr : 
  ?relational:bool ->
  ?nodependency:bool ->
  ('a, 'b) man ->
  ('a, [> 'a Env.typ ] as 'c, [> 'a Env.typdef ] as 'd, 'e) Env.O.t ->
  ('a, ('a, 'c, 'd, 'e) Env.O.t) Cond.O.t ->
  'b t ->
  'a list ->
  'a Expr0.t list ->
  'b t option ->
  'b t

val substitute_lexpr : 
  ('a, 'b) man ->
  ('a, [> 'a Env.typ ] as 'c, [> 'a Env.typdef ] as 'd, 'e) Env.O.t ->
  ('a, ('a, 'c, 'd, 'e) Env.O.t) Cond.O.t ->
  'b t ->
  'a list ->
  'a Expr0.t list ->
  'b t option ->
  'b t

val forget_list : 
  ('a, 'b) man ->
  ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'e) Env.O.t ->
  'b t ->
  'a list ->
  'b t

val forall_bool_list : 
  ('a, 'b) man ->
  ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'e) Env.O.t ->
  'b t ->
  'a list ->
  'b t

val widening : ('a, 'b) man -> 'b t -> 'b t -> 'b t

val widening_threshold : 
  ('a, 'b) man ->
  'b t ->
  'b t ->
  Apron.Lincons0.t array ->
  'b t

val apply_change : bottom:'b t -> ('a, 'b) man -> 'b t -> Env.change -> 'b t

val apply_permutation : 
  ('a, 'b) man ->
  'b t ->
  (int array option * Apron.Dim.perm option) ->
  'b t

package bddapron