bddapron 2.3.2 · OCaml Package

type (!'a, !'b) man = ('a, 'b) Bdddomain0.man

type !'b t0 = 'b Bdddomain0.t

type (!'a, 'b) t = ('a Env.t, 'b t0) Env.value

val get_env : ('a, 'b) t -> 'a Env.t

val to_level0 : ('a, 'b) t -> 'b t0

val of_level0 : 'a Env.t -> 'b t0 -> ('a, 'b) t

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

val print : 
  ?print_apron:
    ((int -> string) -> Format.formatter -> 'b Apron.Abstract0.t -> unit) ->
  Format.formatter ->
  ('a, 'b) t ->
  unit

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

val top : ('a, 'b) man -> 'a Env.t -> ('a, 'b) t

val of_apron : ('a, 'b) man -> 'a Env.t -> 'b Apron.Abstract1.t -> ('a, 'b) t

val of_bddapron : 
  ('a, 'b) man ->
  'a Env.t ->
  ('a Expr1.Bool.t * 'b Apron.Abstract1.t) list ->
  ('a, 'b) t

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

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

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

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

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

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

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

val meet_condition : 
  ('a, 'b) man ->
  'a Cond.t ->
  ('a, 'b) t ->
  'a Expr1.Bool.t ->
  ('a, 'b) t

val meet_condition2 : 
  ('a, 'b) man ->
  ('a, 'b) t ->
  'a Expr2.Bool.t ->
  ('a, 'b) t

val assign_lexpr : 
  ?relational:bool ->
  ?nodependency:bool ->
  ('a, 'b) man ->
  'a Cond.t ->
  ('a, 'b) t ->
  'a list ->
  'a Expr1.t list ->
  ('a, 'b) t option ->
  ('a, 'b) t

val assign_listexpr2 : 
  ?relational:bool ->
  ?nodependency:bool ->
  ('a, 'b) man ->
  ('a, 'b) t ->
  'a list ->
  'a Expr2.List.t ->
  ('a, 'b) t option ->
  ('a, 'b) t

val substitute_lexpr : 
  ('a, 'b) man ->
  'a Cond.t ->
  ('a, 'b) t ->
  'a list ->
  'a Expr1.t list ->
  ('a, 'b) t option ->
  ('a, 'b) t

val substitute_listexpr2 : 
  ('a, 'b) man ->
  ('a, 'b) t ->
  'a list ->
  'a Expr2.List.t ->
  ('a, 'b) t option ->
  ('a, 'b) t

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

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

val widening_threshold : 
  ('a, 'b) man ->
  ('a, 'b) t ->
  ('a, 'b) t ->
  Apron.Lincons1.earray ->
  ('a, 'b) t

val change_environment : ('a, 'b) man -> ('a, 'b) t -> 'a Env.t -> ('a, 'b) t

val rename : ('a, 'b) man -> ('a, 'b) t -> ('a * 'a) list -> ('a, 'b) t

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

val make_man : 'b Apron.Manager.t -> ('a, 'b) man

val canonicalize : 
  ?apron:bool ->
  ?unique:bool ->
  ?disjoint:bool ->
  ('a, 'b) man ->
  ('a, 'b) t ->
  unit

package bddapron