package bddapron

  1. Overview
  2. Docs

Parameters

module Level0 : Level0

Signature

type ('a, 'b) man = ('a, 'b) Level0.man
type 'b t0 = 'b Level0.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