package bddapron

  1. Overview
  2. Docs
package bddapron
Legend:
Library
Module
Module type
Parameter
Class
Class type
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