Previous  Up  Next

Module Bddapron.Domain0

module Domain0: sig .. end

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 Bddapron.Env.t -> Format.formatter -> 'd -> unit;
   bottom :'c -> 'a Bddapron.Env.t -> 'd;
   top :'c -> 'a Bddapron.Env.t -> 'd;
   of_apron :'c -> 'a Bddapron.Env.t -> 'b Apron.Abstract0.t -> 'd;
   of_bddapron :'c ->
'a Bddapron.Env.t ->
('a Bddapron.Expr0.Bool.t * 'b Apron.Abstract0.t) list -> '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 Bddapron.Expr0.Bool.t * 'b Apron.Abstract0.t) list;
   meet :'c -> 'd -> 'd -> 'd;
   join :'c -> 'd -> 'd -> 'd;
   meet_condition :'c ->
'a Bddapron.Env.t ->
'a Bddapron.Cond.t -> 'd -> 'a Bddapron.Expr0.Bool.t -> 'd;
   assign_lexpr :?relational:bool ->
?nodependency:bool ->
'c ->
'a Bddapron.Env.t ->
'a Bddapron.Cond.t ->
'd -> 'a list -> 'a Bddapron.Expr0.t list -> 'd option -> 'd;
   substitute_lexpr :'c ->
'a Bddapron.Env.t ->
'a Bddapron.Cond.t ->
'd -> 'a list -> 'a Bddapron.Expr0.t list -> 'd option -> 'd;
   forget_list :'c -> 'a Bddapron.Env.t -> 'd -> 'a list -> 'd;
   widening :'c -> 'd -> 'd -> 'd;
   widening_threshold :'c -> 'd -> 'd -> Apron.Lincons0.t array -> 'd;
   apply_change :bottom:'d -> 'c -> 'd -> Bddapron.Env.change -> 'd;
   apply_permutation :'c -> 'd -> int array option * Apron.Dim.perm option -> 'd;
}
Type of generic managers. 


type 'd t = 'd
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 -> 'b Apron.Abstract0.t -> unit) ->
       ('a, 'b, 'c, 'd) man ->
       'a Bddapron.Env.t -> Format.formatter -> 'd t -> unit
val bottom : ('a, 'b, 'c, 'd) man ->
       'a Bddapron.Env.t -> 'd t
val top : ('a, 'b, 'c, 'd) man ->
       'a Bddapron.Env.t -> 'd t
val of_apron : ('a, 'b, 'c, 'd) man ->
       'a Bddapron.Env.t -> 'b Apron.Abstract0.t -> 'd t
val of_bddapron : ('a, 'b, 'c, 'd) man ->
       'a Bddapron.Env.t ->
       ('a Bddapron.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 Bddapron.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 Bddapron.Env.t ->
       'a Bddapron.Cond.t ->
       'd t -> 'a Bddapron.Expr0.Bool.t -> 'd t
val assign_lexpr : ?relational:bool ->
       ?nodependency:bool ->
       ('a, 'b, 'c, 'd) man ->
       'a Bddapron.Env.t ->
       'a Bddapron.Cond.t ->
       'd t ->
       'a list ->
       'a Bddapron.Expr0.t list ->
       'd t option -> 'd t
val substitute_lexpr : ('a, 'b, 'c, 'd) man ->
       'a Bddapron.Env.t ->
       'a Bddapron.Cond.t ->
       'd t ->
       'a list ->
       'a Bddapron.Expr0.t list ->
       'd t option -> 'd t
val forget_list : ('a, 'b, 'c, 'd) man ->
       'a Bddapron.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 -> Bddapron.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

Implementation based on Bddapron.Mtbdddomain0


type ('a, 'b) mtbdd = ('a, 'b, ('a, 'b) Bddapron.Mtbdddomain0.man, 'b Bddapron.Mtbdddomain0.t)
       man 
val mtbdd_of_mtbdddomain : ('a, 'b) Bddapron.Mtbdddomain0.man -> ('a, 'b) mtbdd
Make a mtbdd manager from an underlying BDDAPRON manager
val make_mtbdd : ?global:bool -> 'b Apron.Manager.t -> ('a, 'b) mtbdd
Make a mtbdd manager from an APRON 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 Bddapron.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 Bddapron.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 Bddapron.Bdddomain0


type ('a, 'b) bdd = ('a, 'b, ('a, 'b) Bddapron.Bdddomain0.man, 'b Bddapron.Bdddomain0.t)
       man 
val bdd_of_bdddomain : ('a, 'b) Bddapron.Bdddomain0.man -> ('a, 'b) bdd
Make a bdd manager from an underlying BDDAPRON manager
val make_bdd : 'b Apron.Manager.t -> ('a, 'b) bdd
Make a bdd manager from an APRON 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 Bddapron.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 Bddapron.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