Previous  Up  Next

Module Bddapron.Mtbdddomain0

module Mtbdddomain0: sig .. end
type ('a, 'b) man = 'b Bddapron.ApronDD.man
BDDAPRON Manager. The type parameter 'b indicates the underlying APRON abstract domain, as in type 'b Apron.Abstract1.t
type 'b t = 'b Bddapron.ApronDD.t
BDDAPRON Abstract value.
val make_man : ?global:bool -> 'b Apron.Manager.t -> ('a, 'b) man
Makes a BDDAPRON manager from an APRON manager. If global=true (default: false), uses a global (persistent) BDD cache for the operations is_leq, join, meet and exist (internal).
val size : ('a, 'b) man -> 'b t -> int
Size of an abstract value in terms of number of nodes of the MTBDD.
val print : ?print_apron:((int -> string) ->
                     Format.formatter -> 'b Apron.Abstract0.t -> unit) ->
       'a Bddapron.Env.t -> Format.formatter -> 'b t -> unit
Printing function

Constructors, accessors, tests and property extraction



Basic constructor


val bottom : ('a, 'b) man ->
       'a Bddapron.Env.t -> 'b t
val top : ('a, 'b) man ->
       'a Bddapron.Env.t -> 'b t
val of_apron : ('a, 'b) man ->
       'a Bddapron.Env.t -> 'b Apron.Abstract0.t -> 'b t
val of_bddapron : ('a, 'b) man ->
       'a Bddapron.Env.t ->
       ('a Bddapron.Expr0.Bool.t * 'b Apron.Abstract0.t) list ->
       'b t

Tests


val is_bottom : ('a, 'b) man -> 'b t -> bool
val is_top : ('a, 'b) man -> 'b t -> bool
Emtpiness and Universality tests
val is_leq : ('a, 'b) man ->
       'b t -> 'b t -> bool
val is_eq : ('a, 'b) man ->
       'b t -> 'b t -> bool
Inclusion and equality tests

Extraction of properties


val to_bddapron : ('a, 'b) man ->
       'b t ->
       ('a Bddapron.Expr0.Bool.t * 'b Apron.Abstract0.t) list
Conversion to a disjunction of a conjunction of pair of a purely Boolean formula (without numerical constraints) and an APRON abstract value

Operations


val meet : ('a, 'b) man ->
       'b t ->
       'b t -> 'b t
val join : ('a, 'b) man ->
       'b t ->
       'b t -> 'b t
Meet and join
val meet_condition : ('a, 'b) man ->
       'a Bddapron.Env.t ->
       'a Bddapron.Cond.t ->
       'b t ->
       'a Bddapron.Expr0.Bool.t -> 'b t
Intersection with a Boolean expression (that may involve numerical constraints)
val assign_lexpr : ?relational:bool ->
       ?nodependency:bool ->
       ('a, 'b) man ->
       'a Bddapron.Env.t ->
       'a Bddapron.Cond.t ->
       'b t ->
       'a list ->
       'a Bddapron.Expr0.t list ->
       'b t option -> 'b t
val substitute_lexpr : ('a, 'b) man ->
       'a Bddapron.Env.t ->
       'a Bddapron.Cond.t ->
       'b t ->
       'a list ->
       'a Bddapron.Expr0.t list ->
       'b t option -> 'b t
Parallel assignement/substitution of a list of variables by a list of expressions
val forget_list : ('a, 'b) man ->
       'a Bddapron.Env.t ->
       'b t -> 'a list -> 'b t
Forget (existential quantification) a list of variables
val widening : ('a, 'b) man ->
       'b t ->
       'b t -> 'b t
val widening_threshold : ('a, 'b) man ->
       'b t ->
       'b t ->
       Apron.Lincons0.t array -> 'b t
Widening
val apply_change : bottom:'b t ->
       ('a, 'b) man ->
       'b t ->
       Bddapron.Env.change -> 'b t
val apply_permutation : ('a, 'b) man ->
       'b t ->
       int array option * Apron.Dim.perm option -> 'b t

Opened signature and Internal functions



We provide here the same functions and modules as before, but with opened types (this allows extensions). The functions above are actually derived from the functions below by just constraining their types. We provide here also more internal functions
module O: sig .. end