bddapron

Logico-numerical domain(s) based on BDDs and APRON
Legend:
Library
Module
Module type
Parameter
Class
Class type
Manual
Module Bddapron . Bdddomain1
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