Previous  Up  Next

Module Apron.Abstract1

module Abstract1: sig .. end
type 'a t = {
   mutable abstract0 :'a Apron.Abstract0.t;
   mutable env :Apron.Environment.t;
}
The type parameter 'a allows to distinguish abstract values with different underlying abstract domains.
type box1 = {
   mutable interval_array :Apron.Interval.t array;
   mutable box1_env :Apron.Environment.t;
}

General management



Memory


val copy : 'a Apron.Manager.t -> 'a t -> 'a t
Copy a value
val size : 'a Apron.Manager.t -> 'a t -> int
Return the abstract size of a value

Control of internal representation


val minimize : 'a Apron.Manager.t -> 'a t -> unit
Minimize the size of the representation of the value. This may result in a later recomputation of internal information.
val canonicalize : 'a Apron.Manager.t -> 'a t -> unit
Put the abstract value in canonical form. (not yet clear definition)
val hash : 'a Apron.Manager.t -> 'a t -> int
val approximate : 'a Apron.Manager.t -> 'a t -> int -> unit
approximate man abs alg perform some transformation on the abstract value, guided by the argument alg. The transformation may lose information. The argument alg overrides the field algorithm of the structure of type Manager.funopt associated to ap_abstract0_approximate (commodity feature).

Printing


val fdump : 'a Apron.Manager.t -> 'a t -> unit
Dump on the stdout C stream the internal representation of an abstract value, for debugging purposes
val print : Format.formatter -> 'a t -> unit
Print as a set of constraints

Serialization



Constructor, accessors, tests and property extraction



Basic constructors



All these functions request explicitly an environment in their arguments.
val bottom : 'a Apron.Manager.t -> Apron.Environment.t -> 'a t
Create a bottom (empty) value defined on the given environment
val top : 'a Apron.Manager.t -> Apron.Environment.t -> 'a t
Create a top (universe) value defined on the given environment
val of_box : 'a Apron.Manager.t ->
       Apron.Environment.t ->
       Apron.Var.t array -> Apron.Interval.t array -> 'a t
Abstract an hypercube.

of_box man env tvar tinterval abstracts an hypercube defined by the arrays tvar and tinterval. The result is defined on the environment env, which should contain all the variables in tvar (and defines their type)


Accessors


val manager : 'a t -> 'a Apron.Manager.t
val env : 'a t -> Apron.Environment.t
val abstract0 : 'a t -> 'a Apron.Abstract0.t
Return resp. the underlying manager, environment and abstract value of level 0

Tests


val is_bottom : 'a Apron.Manager.t -> 'a t -> bool
Emptiness test
val is_top : 'a Apron.Manager.t -> 'a t -> bool
Universality test
val is_leq : 'a Apron.Manager.t -> 'a t -> 'a t -> bool
Inclusion test. The 2 abstract values should be compatible.
val is_eq : 'a Apron.Manager.t -> 'a t -> 'a t -> bool
Equality test. The 2 abstract values should be compatible.
val sat_lincons : 'a Apron.Manager.t -> 'a t -> Apron.Lincons1.t -> bool
Does the abstract value satisfy the linear constraint ?
val sat_tcons : 'a Apron.Manager.t -> 'a t -> Apron.Tcons1.t -> bool
Does the abstract value satisfy the tree expression constraint ?
val sat_interval : 'a Apron.Manager.t ->
       'a t -> Apron.Var.t -> Apron.Interval.t -> bool
Does the abstract value satisfy the constraint dim in interval ?
val is_variable_unconstrained : 'a Apron.Manager.t -> 'a t -> Apron.Var.t -> bool
Is the variable unconstrained in the abstract value ? If yes, this means that the existential quantification of the dimension does not change the value.

Extraction of properties


val bound_variable : 'a Apron.Manager.t -> 'a t -> Apron.Var.t -> Apron.Interval.t
Return the interval of variation of the variable in the abstract value.
val bound_linexpr : 'a Apron.Manager.t ->
       'a t -> Apron.Linexpr1.t -> Apron.Interval.t
Return the interval of variation of the linear expression in the abstract value.

Implement a form of linear programming, where the argument linear expression is the one to optimize under the constraints induced by the abstract value.

val bound_texpr : 'a Apron.Manager.t ->
       'a t -> Apron.Texpr1.t -> Apron.Interval.t
Return the interval of variation of the tree expression in the abstract value.
val to_box : 'a Apron.Manager.t -> 'a t -> box1
Convert the abstract value to an hypercube
val to_lincons_array : 'a Apron.Manager.t -> 'a t -> Apron.Lincons1.earray
Convert the abstract value to a conjunction of linear constraints.

Convert the abstract value to a conjunction of tree expressions constraints.

val to_tcons_array : 'a Apron.Manager.t -> 'a t -> Apron.Tcons1.earray
val to_generator_array : 'a Apron.Manager.t -> 'a t -> Apron.Generator1.earray
Convert the abstract value to a set of generators that defines it.

Operations



Meet and Join


val meet : 'a Apron.Manager.t ->
       'a t -> 'a t -> 'a t
Meet of 2 abstract values.
val meet_array : 'a Apron.Manager.t -> 'a t array -> 'a t
Meet of a non empty array of abstract values.
val meet_lincons_array : 'a Apron.Manager.t ->
       'a t -> Apron.Lincons1.earray -> 'a t
Meet of an abstract value with an array of linear constraints.
val meet_tcons_array : 'a Apron.Manager.t ->
       'a t -> Apron.Tcons1.earray -> 'a t
Meet of an abstract value with an array of tree expressions constraints.
val join : 'a Apron.Manager.t ->
       'a t -> 'a t -> 'a t
Join of 2 abstract values.
val join_array : 'a Apron.Manager.t -> 'a t array -> 'a t
Join of a non empty array of abstract values.
val add_ray_array : 'a Apron.Manager.t ->
       'a t -> Apron.Generator1.earray -> 'a t
Add the array of generators to the abstract value (time elapse operator).

The generators should either lines or rays, not vertices.


Side-effect versions of the previous functions

val meet_with : 'a Apron.Manager.t -> 'a t -> 'a t -> unit
val meet_lincons_array_with : 'a Apron.Manager.t -> 'a t -> Apron.Lincons1.earray -> unit
val meet_tcons_array_with : 'a Apron.Manager.t -> 'a t -> Apron.Tcons1.earray -> unit
val join_with : 'a Apron.Manager.t -> 'a t -> 'a t -> unit
val add_ray_array_with : 'a Apron.Manager.t -> 'a t -> Apron.Generator1.earray -> unit

Assignement and Substitutions


val assign_linexpr_array : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t array ->
       Apron.Linexpr1.t array -> 'a t option -> 'a t
Parallel assignement of an array of dimensions by an array of same size of linear expressions
val substitute_linexpr_array : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t array ->
       Apron.Linexpr1.t array -> 'a t option -> 'a t
Parallel substitution of an array of dimensions by an array of same size of linear expressions
val assign_texpr_array : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t array ->
       Apron.Texpr1.t array -> 'a t option -> 'a t
Parallel assignement of an array of dimensions by an array of same size of tree expressions
val substitute_texpr_array : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t array ->
       Apron.Texpr1.t array -> 'a t option -> 'a t
Parallel substitution of an array of dimensions by an array of same size of tree expressions

Side-effect versions of the previous functions

val assign_linexpr_array_with : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t array ->
       Apron.Linexpr1.t array -> 'a t option -> unit
val substitute_linexpr_array_with : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t array ->
       Apron.Linexpr1.t array -> 'a t option -> unit
val assign_texpr_array_with : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t array ->
       Apron.Texpr1.t array -> 'a t option -> unit
val substitute_texpr_array_with : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t array ->
       Apron.Texpr1.t array -> 'a t option -> unit

Projections



These functions implements forgeting (existential quantification) of (array of) variables. Both functional and side-effect versions are provided. The Boolean, if true, adds a projection onto 0-plane.
val forget_array : 'a Apron.Manager.t ->
       'a t -> Apron.Var.t array -> bool -> 'a t
val forget_array_with : 'a Apron.Manager.t ->
       'a t -> Apron.Var.t array -> bool -> unit

Change and permutation of dimensions


val change_environment : 'a Apron.Manager.t ->
       'a t -> Apron.Environment.t -> bool -> 'a t
Change the environement of the abstract values.

Variables that are removed are first existentially quantified, and variables that are introduced are unconstrained. The Boolean, if true, adds a projection onto 0-plane for these ones.

val minimize_environment : 'a Apron.Manager.t -> 'a t -> 'a t
Remove from the environment of the abstract value and from the abstract value itself variables that are unconstrained in it.
val rename_array : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t array -> Apron.Var.t array -> 'a t
Parallel renaming of the environment of the abstract value.

The new variables should not interfere with the variables that are not renamed.

val change_environment_with : 'a Apron.Manager.t ->
       'a t -> Apron.Environment.t -> bool -> unit
val minimize_environment_with : 'a Apron.Manager.t -> 'a t -> unit
val rename_array_with : 'a Apron.Manager.t ->
       'a t -> Apron.Var.t array -> Apron.Var.t array -> unit

Expansion and folding of dimensions



These functions allows to expand one dimension into several ones having the same properties with respect to the other dimensions, and to fold several dimensions into one. Formally, 


val expand : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t -> Apron.Var.t array -> 'a t
Expansion: expand a var tvar expands the variable var into itself and the additional variables in tvar, which are given the same type as var.

It results in (n+1) unrelated variables having same relations with other variables. The additional variables are added to the environment of the argument for making the environment of the result, so they should not belong to the initial environement.

val fold : 'a Apron.Manager.t ->
       'a t -> Apron.Var.t array -> 'a t
Folding: fold a tvar fold the variables in the array tvar of size n>=1 and put the result in the first variable of the array. The other variables of the array are then removed, both from the environment and the abstract value.
val expand_with : 'a Apron.Manager.t ->
       'a t -> Apron.Var.t -> Apron.Var.t array -> unit
val fold_with : 'a Apron.Manager.t -> 'a t -> Apron.Var.t array -> unit

Widening


val widening : 'a Apron.Manager.t ->
       'a t -> 'a t -> 'a t
Widening. Assumes that the first abstract value is included in the second one.
val widening_threshold : 'a Apron.Manager.t ->
       'a t ->
       'a t -> Apron.Lincons1.earray -> 'a t

Closure operation


val closure : 'a Apron.Manager.t -> 'a t -> 'a t
Closure: transform strict constraints into non-strict ones.
val closure_with : 'a Apron.Manager.t -> 'a t -> unit
Side-effect version

Additional operations


val of_lincons_array : 'a Apron.Manager.t ->
       Apron.Environment.t -> Apron.Lincons1.earray -> 'a t
val of_tcons_array : 'a Apron.Manager.t ->
       Apron.Environment.t -> Apron.Tcons1.earray -> 'a t
Abstract a conjunction of constraints
val assign_linexpr : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t ->
       Apron.Linexpr1.t -> 'a t option -> 'a t
val substitute_linexpr : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t ->
       Apron.Linexpr1.t -> 'a t option -> 'a t
val assign_texpr : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t ->
       Apron.Texpr1.t -> 'a t option -> 'a t
val substitute_texpr : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t ->
       Apron.Texpr1.t -> 'a t option -> 'a t
Assignement/Substitution of a single dimension by a single expression
val assign_linexpr_with : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t -> Apron.Linexpr1.t -> 'a t option -> unit
val substitute_linexpr_with : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t -> Apron.Linexpr1.t -> 'a t option -> unit
val assign_texpr_with : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t -> Apron.Texpr1.t -> 'a t option -> unit
val substitute_texpr_with : 'a Apron.Manager.t ->
       'a t ->
       Apron.Var.t -> Apron.Texpr1.t -> 'a t option -> unit
Side-effect version of the previous functions
val unify : 'a Apron.Manager.t ->
       'a t -> 'a t -> 'a t
Unification of 2 abstract values on their least common environment
val unify_with : 'a Apron.Manager.t -> 'a t -> 'a t -> unit
Side-effect version