package bddapron

  1. Overview
  2. Docs
package bddapron
Legend:
Library
Module
Module type
Parameter
Class
Class type
type (!'a, !'b, !'c, !'d) man = {
  1. typ : string;
  2. man : 'c;
  3. canonicalize : ?apron:bool -> 'c -> 'd -> unit;
  4. size : 'c -> 'd -> int;
  5. print : ?print_apron: ((int -> string) -> Format.formatter -> 'b Apron.Abstract0.t -> unit) -> 'a Env.t -> Format.formatter -> 'd -> unit;
  6. bottom : 'c -> 'a Env.t -> 'd;
  7. top : 'c -> 'a Env.t -> 'd;
  8. of_apron : 'c -> 'a Env.t -> 'b Apron.Abstract0.t -> 'd;
  9. of_bddapron : 'c -> 'a Env.t -> ('a Expr0.Bool.t * 'b Apron.Abstract0.t) list -> 'd;
  10. is_bottom : 'c -> 'd -> bool;
  11. is_top : 'c -> 'd -> bool;
  12. is_leq : 'c -> 'd -> 'd -> bool;
  13. is_eq : 'c -> 'd -> 'd -> bool;
  14. to_bddapron : 'c -> 'd -> ('a Expr0.Bool.t * 'b Apron.Abstract0.t) list;
  15. meet : 'c -> 'd -> 'd -> 'd;
  16. join : 'c -> 'd -> 'd -> 'd;
  17. meet_condition : 'c -> 'a Env.t -> 'a Cond.t -> 'd -> 'a Expr0.Bool.t -> 'd;
  18. assign_lexpr : ?relational:bool -> ?nodependency:bool -> 'c -> 'a Env.t -> 'a Cond.t -> 'd -> 'a list -> 'a Expr0.t list -> 'd option -> 'd;
  19. substitute_lexpr : 'c -> 'a Env.t -> 'a Cond.t -> 'd -> 'a list -> 'a Expr0.t list -> 'd option -> 'd;
  20. forget_list : 'c -> 'a Env.t -> 'd -> 'a list -> 'd;
  21. forall_bool_list : 'c -> 'a Env.t -> 'd -> 'a list -> 'd;
  22. widening : 'c -> 'd -> 'd -> 'd;
  23. widening_threshold : 'c -> 'd -> 'd -> Apron.Lincons0.t array -> 'd;
  24. apply_change : bottom:'d -> 'c -> 'd -> Env.change -> 'd;
  25. apply_permutation : 'c -> 'd -> (int array option * Apron.Dim.perm option) -> 'd;
}
type !'d t = 'd
val canonicalize : ?apron:bool -> ('a, 'b, 'c, 'd) man -> 'd t -> unit
val size : ('a, 'b, 'c, 'd) man -> 'd t -> int
val print : ?print_apron: ((int -> string) -> Format.formatter -> 'b Apron.Abstract0.t -> unit) -> ('a, 'b, 'c, 'd) man -> 'a Env.t -> Format.formatter -> 'd t -> unit
val bottom : ('a, 'b, 'c, 'd) man -> 'a Env.t -> 'd t
val top : ('a, 'b, 'c, 'd) man -> 'a Env.t -> 'd t
val of_apron : ('a, 'b, 'c, 'd) man -> 'a Env.t -> 'b Apron.Abstract0.t -> 'd t
val of_bddapron : ('a, 'b, 'c, 'd) man -> 'a Env.t -> ('a Expr0.Bool.t * 'b Apron.Abstract0.t) list -> 'd t
val is_bottom : ('a, 'b, 'c, 'd) man -> 'd t -> bool
val is_top : ('a, 'b, 'c, 'd) man -> 'd t -> bool
val is_leq : ('a, 'b, 'c, 'd) man -> 'd t -> 'd t -> bool
val is_eq : ('a, 'b, 'c, 'd) man -> 'd t -> 'd t -> bool
val to_bddapron : ('a, 'b, 'c, 'd) man -> 'd t -> ('a Expr0.Bool.t * 'b Apron.Abstract0.t) list
val meet : ('a, 'b, 'c, 'd) man -> 'd t -> 'd t -> 'd t
val join : ('a, 'b, 'c, 'd) man -> 'd t -> 'd t -> 'd t
val meet_condition : ('a, 'b, 'c, 'd) man -> 'a Env.t -> 'a Cond.t -> 'd t -> 'a Expr0.Bool.t -> 'd t
val assign_lexpr : ?relational:bool -> ?nodependency:bool -> ('a, 'b, 'c, 'd) man -> 'a Env.t -> 'a Cond.t -> 'd t -> 'a list -> 'a Expr0.t list -> 'd t option -> 'd t
val substitute_lexpr : ('a, 'b, 'c, 'd) man -> 'a Env.t -> 'a Cond.t -> 'd t -> 'a list -> 'a Expr0.t list -> 'd t option -> 'd t
val forget_list : ('a, 'b, 'c, 'd) man -> 'a Env.t -> 'd t -> 'a list -> 'd t
val forall_bool_list : ('a, 'b, 'c, 'd) man -> 'a Env.t -> 'd t -> 'a list -> 'd t
val widening : ('a, 'b, 'c, 'd) man -> 'd t -> 'd t -> 'd t
val widening_threshold : ('a, 'b, 'c, 'd) man -> 'd t -> 'd t -> Apron.Lincons0.t array -> 'd t
val apply_change : bottom:'d t -> ('a, 'b, 'c, 'd) man -> 'd t -> Env.change -> 'd t
val apply_permutation : ('a, 'b, 'c, 'd) man -> 'd t -> (int array option * Apron.Dim.perm option) -> 'd t
val man_get_apron : ('a, 'b, 'c, 'd) man -> 'b Apron.Manager.t
type (!'a, !'b) mtbdd = ('a, 'b, ('a, 'b) Mtbdddomain0.man, 'b Mtbdddomain0.t) man
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 * 'b Mtbdddomain0.t t) -> ('a, 'b, 'c, 'd) man * 'd t
val to_mtbdd : (('a, 'b, 'c, 'd) man * 'd t) -> ('a, 'b) mtbdd * 'b Mtbdddomain0.t t
type (!'a, !'b) bdd = ('a, 'b, ('a, 'b) Bdddomain0.man, 'b Bdddomain0.t) man
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 * 'b Bdddomain0.t t) -> ('a, 'b, 'c, 'd) man * 'd t
val to_bdd : (('a, 'b, 'c, 'd) man * 'd t) -> ('a, 'b) bdd * 'b Bdddomain0.t t