Previous  Up  Next

Module Domain0


module Domain0: sig .. end
Boolean/Numerical domain: generic interface

Generic interface



Types



type ('a, 'b, 'c, 'd) man = {
   typ : string;
   man : 'c;
   canonicalize : ?apron:bool -> 'c -> 'd -> unit;
   size : 'c -> 'd -> int;
   print : ?print_apron:((int -> string) ->
Format.formatter -> 'b Apron.Abstract0.t -> unit) ->
'a Env.t -> Format.formatter -> 'd -> unit;
   bottom : 'c -> 'a Env.t -> 'd;
   top : 'c -> 'a Env.t -> 'd;
   of_apron : 'c -> 'a Env.t -> 'b Apron.Abstract0.t -> 'd;
   is_bottom : 'c -> 'd -> bool;
   is_top : 'c -> 'd -> bool;
   is_leq : 'c -> 'd -> 'd -> bool;
   is_eq : 'c -> 'd -> 'd -> bool;
   to_bddapron : 'c -> 'd -> ('a Expr0.Bool.t * 'b Apron.Abstract0.t) list;
   meet : 'c -> 'd -> 'd -> 'd;
   join : 'c -> 'd -> 'd -> 'd;
   meet_condition : 'c -> 'a Env.t -> 'a Cond.t -> 'd -> 'a Expr0.Bool.t -> 'd;
   assign_lexpr : ?relational:bool ->
?nodependency:bool ->
'c ->
'a Env.t -> 'a Cond.t -> 'd -> 'a list -> 'a Expr0.t list -> 'd option -> 'd;
   substitute_lexpr : 'c ->
'a Env.t -> 'a Cond.t -> 'd -> 'a list -> 'a Expr0.t list -> 'd option -> 'd;
   forget_list : 'c -> 'a Env.t -> 'd -> 'a list -> 'd;
   widening : 'c -> 'd -> 'd -> 'd;
   apply_change : bottom:'d -> 'c -> 'd -> Env.change -> 'd;
   apply_permutation : 'c -> 'd -> int array option * Apron.Dim.perm option -> 'd;
}
Type of generic managers. 


type 'a t = 'a
Type of generic abstract values

Functions


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 -> 'a Apron.Abstract0.t -> unit) ->
       ('b, 'a, 'c, 'd) man ->
       'b 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 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 widening : ('a, 'b, 'c, 'd) man -> 'd t -> 'd t -> 'd t
val apply_change : bottom:'a t ->
       ('b, 'c, 'd, 'a) man -> 'a t -> Env.change -> 'a t
val apply_permutation : ('a, 'b, 'c, 'd) man ->
       'd t -> int array option * Apron.Dim.perm option -> 'd t

Implementation based on Mtbdddomain0


type ('a, 'b) mtbdd = ('a, 'b, ('a, 'b) Mtbdddomain0.man, 'b Mtbdddomain0.t) man 
val make_mtbdd : ?global:bool -> 'a Apron.Manager.t -> ('b, 'a) mtbdd
Make a mtbdd manager

Type conversion functions


val man_is_mtbdd : ('a, 'b, 'c, 'd) man -> bool
Return true iff the argument manager is a mtbdd manager
val man_of_mtbdd : ('a, 'b) mtbdd -> ('a, 'b, 'c, 'd) man
Makes a mtbdd manager generic
val man_to_mtbdd : ('a, 'b, 'c, 'd) man -> ('a, 'b) mtbdd
Instanciate the type of a mtbdd manager. Raises Failure if the argument manager is not a mtbdd manager
val of_mtbdd : ('a, 'b) mtbdd * 'b Mtbdddomain0.t t ->
       ('a, 'b, 'c, 'd) man * 'd t
Makes a pair (mtbdd manager,mtbdd abstract value) generic
val to_mtbdd : ('a, 'b, 'c, 'd) man * 'd t ->
       ('a, 'b) mtbdd * 'b Mtbdddomain0.t t
Instanciate the type of a pair (mtbdd manager,mtbdd abstract value). Raises Failure if the argument manager is not a mtbdd manager

Implementation based on Bdddomain0


type ('a, 'b) bdd = ('a, 'b, ('a, 'b) Bdddomain0.man, 'b Bdddomain0.t) man 
val make_bdd : 'a Apron.Manager.t -> ('b, 'a) bdd
Make a bdd manager

Type conversion functions


val man_is_bdd : ('a, 'b, 'c, 'd) man -> bool
Return true iff the argument manager is a bdd manager
val man_of_bdd : ('a, 'b) bdd -> ('a, 'b, 'c, 'd) man
Makes a bdd manager generic
val man_to_bdd : ('a, 'b, 'c, 'd) man -> ('a, 'b) bdd
Instanciate the type of a bdd manager. Raises Failure if the argument manager is not a bdd manager
val of_bdd : ('a, 'b) bdd * 'b Bdddomain0.t t ->
       ('a, 'b, 'c, 'd) man * 'd t
Makes a pair (bdd manager,bdd abstract value) generic
val to_bdd : ('a, 'b, 'c, 'd) man * 'd t ->
       ('a, 'b) bdd * 'b Bdddomain0.t t
Instanciate the type of a pair (bdd manager,bdd abstract value). Raises Failure if the argument manager is not a bdd manager