bddapron

Logico-numerical domain(s) based on BDDs and APRON
Legend:
Library
Module
Module type
Parameter
Class
Class type
Manual
Module Bddapron . Domain1
type (!'a, !'b, !'c, !'d) man = ( 'a, 'b, 'c, 'd ) Domain0.man
type (!'a, !'b) mtbdd = ( 'a, 'b, ( 'a, 'b ) Mtbdddomain0.man, 'b Mtbdddomain0.t ) man
type (!'a, !'b) bdd = ( 'a, 'b, ( 'a, 'b ) Bdddomain0.man, 'b Bdddomain0.t ) man
type (!'a, !'d) t = ( 'a Env.t, 'd ) Env.value
val canonicalize : ?apron:bool -> ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> unit
val print : ?print_apron: ( ( int -> string ) -> Format.formatter -> 'b Apron.Abstract0.t -> unit ) -> ( 'a, 'b, 'c, 'd ) man -> Format.formatter -> ( 'a, 'd ) t -> unit
val get_env : ( 'a, 'd ) t -> 'a Env.t
val to_level0 : ( 'a, 'd ) t -> 'd
val of_level0 : 'a Env.t -> 'd -> ( 'a, 'd ) t
val size : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> int
val bottom : ( 'a, 'b, 'c, 'd ) man -> 'a Env.t -> ( 'a, 'd ) t
val top : ( 'a, 'b, 'c, 'd ) man -> 'a Env.t -> ( 'a, 'd ) t
val of_apron : ( 'a, 'b, 'c, 'd ) man -> 'a Env.t -> 'b Apron.Abstract1.t -> ( 'a, 'd ) t
val of_bddapron : ( 'a, 'b, 'c, 'd ) man -> 'a Env.t -> ('a Expr1.Bool.t * 'b Apron.Abstract1.t) list -> ( 'a, 'd ) t
val is_bottom : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> bool
val is_top : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> bool
val is_leq : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> ( 'a, 'd ) t -> bool
val is_eq : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> ( 'a, 'd ) t -> bool
val to_bddapron : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> ('a Expr1.Bool.t * 'b Apron.Abstract1.t) list
val meet : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> ( 'a, 'd ) t -> ( 'a, 'd ) t
val join : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> ( 'a, 'd ) t -> ( 'a, 'd ) t
val meet_condition : ( 'a, 'b, 'c, 'd ) man -> 'a Cond.t -> ( 'a, 'd ) t -> 'a Expr1.Bool.t -> ( 'a, 'd ) t
val meet_condition2 : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> 'a Expr2.Bool.t -> ( 'a, 'd ) t
val assign_lexpr : ?relational:bool -> ?nodependency:bool -> ( 'a, 'b, 'c, 'd ) man -> 'a Cond.t -> ( 'a, 'd ) t -> 'a list -> 'a Expr1.t list -> ( 'a, 'd ) t option -> ( 'a, 'd ) t
val assign_listexpr2 : ?relational:bool -> ?nodependency:bool -> ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> 'a list -> 'a Expr2.List.t -> ( 'a, 'd ) t option -> ( 'a, 'd ) t
val substitute_lexpr : ( 'a, 'b, 'c, 'd ) man -> 'a Cond.t -> ( 'a, 'd ) t -> 'a list -> 'a Expr1.t list -> ( 'a, 'd ) t option -> ( 'a, 'd ) t
val substitute_listexpr2 : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> 'a list -> 'a Expr2.List.t -> ( 'a, 'd ) t option -> ( 'a, 'd ) t
val forget_list : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> 'a list -> ( 'a, 'd ) t
val widening : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> ( 'a, 'd ) t -> ( 'a, 'd ) t
val widening_threshold : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> ( 'a, 'd ) t -> Apron.Lincons1.earray -> ( 'a, 'd ) t
val change_environment : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> 'a Env.t -> ( 'a, 'd ) t
val unify : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> ( 'a, 'd ) t -> ( 'a, 'd ) t
val rename : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'd ) t -> ('a * 'a) list -> ( 'a, 'd ) t
val man_get_apron : ( 'a, 'b, 'c, 'd ) man -> 'b Apron.Manager.t
val mtbdd_of_mtbdddomain : ( 'a, 'b ) Mtbdddomain0.man -> ( 'a, 'b ) mtbdd
val make_mtbdd : ?global:bool -> 'b Apron.Manager.t -> ( 'a, 'b ) mtbdd
val man_is_mtbdd : ( 'a, 'b, 'c, 'd ) man -> bool
val man_of_mtbdd : ( 'a, 'b ) mtbdd -> ( 'a, 'b, 'c, 'd ) man
val man_to_mtbdd : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'b ) mtbdd
val of_mtbdd : (( 'a, 'b ) mtbdd * ( 'a, 'b Mtbdddomain0.t ) t) -> ( 'a, 'b, 'c, 'd ) man * ( 'a, 'd ) t
val to_mtbdd : (( 'a, 'b, 'c, 'd ) man * ( 'a, 'd ) t) -> ( 'a, 'b ) mtbdd * ( 'a, 'b Mtbdddomain0.t ) t
val bdd_of_bdddomain : ( 'a, 'b ) Bdddomain0.man -> ( 'a, 'b ) bdd
val make_bdd : 'b Apron.Manager.t -> ( 'a, 'b ) bdd
val man_is_bdd : ( 'a, 'b, 'c, 'd ) man -> bool
val man_of_bdd : ( 'a, 'b ) bdd -> ( 'a, 'b, 'c, 'd ) man
val man_to_bdd : ( 'a, 'b, 'c, 'd ) man -> ( 'a, 'b ) bdd
val of_bdd : (( 'a, 'b ) bdd * ( 'a, 'b Bdddomain0.t ) t) -> ( 'a, 'b, 'c, 'd ) man * ( 'a, 'd ) t
val to_bdd : (( 'a, 'b, 'c, 'd ) man * ( 'a, 'd ) t) -> ( 'a, 'b ) bdd * ( 'a, 'b Bdddomain0.t ) t