Module Abstract1

module Abstract1: sig .. end

type 'a t = {

	`mutable abstract0 : 'a Abstract0.t;`
	`mutable env : Environment.t;`

}

APRON Abstract values of level 1

The type parameter 'a allows to distinguish abstract values with different underlying abstract domains.

type box1 = {

	`mutable interval_array : Interval.t array;`
	`mutable box1_env : Environment.t;`

}

General management

Memory

val copy : 'a Manager.t -> 'a t -> 'a t

Copy a value

val size : 'a Manager.t -> 'a t -> int

Return the abstract size of a value

Control of internal representation

val minimize : 'a 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 Manager.t -> 'a t -> unit

Put the abstract value in canonical form. (not yet clear definition)

val hash : 'a Manager.t -> 'a t -> int

val approximate : 'a 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 Manager.t -> 'a t -> unit

Dump on the stdout C stream the internal representation of an abstract value, for debugging purposes

val print : Stdlib.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 Manager.t -> Environment.t -> 'a t

Create a bottom (empty) value defined on the given environment

val top : 'a Manager.t -> Environment.t -> 'a t

Create a top (universe) value defined on the given environment

val of_box : 'a Manager.t ->
       Environment.t -> Var.t array -> 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). If any interval is empty, the resulting abstract element is empty (bottom). In case of a 0-dimensional element (empty environment), the abstract element is always top (not bottom).

Accessors

val manager : 'a t -> 'a Manager.t

val env : 'a t -> Environment.t

val abstract0 : 'a t -> 'a Abstract0.t

Return resp. the underlying manager, environment and abstract value of level 0

Tests

NOTE: Abstract elements are not totally ordered. As of 0.9.15, they do not implement the polymorphic compare function to avoid confusion. As a consequence, the polymorphic =, <=, etc. operators cannot be used. Use is_eq and is_leq instead.

val is_bottom : 'a Manager.t -> 'a t -> bool

Emptiness test

val is_top : 'a Manager.t -> 'a t -> bool

Universality test

val is_leq : 'a Manager.t -> 'a t -> 'a t -> bool

Inclusion test. The two abstract values should be compatible.

val is_eq : 'a Manager.t -> 'a t -> 'a t -> bool

Equality test. The two abstract values should be compatible.

val sat_lincons : 'a Manager.t -> 'a t -> Lincons1.t -> bool

Does the abstract value satisfy the linear constraint ?

val sat_tcons : 'a Manager.t -> 'a t -> Tcons1.t -> bool

Does the abstract value satisfy the tree expression constraint ?

val sat_interval : 'a Manager.t -> 'a t -> Var.t -> Interval.t -> bool

Does the abstract value satisfy the constraint dim in interval?

val is_variable_unconstrained : 'a Manager.t -> 'a t -> 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 Manager.t -> 'a t -> Var.t -> Interval.t

Return the interval of variation of the variable in the abstract value.

val bound_linexpr : 'a Manager.t -> 'a t -> Linexpr1.t -> 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 Manager.t -> 'a t -> Texpr1.t -> Interval.t

Return the interval of variation of the tree expression in the abstract value.

val to_box : 'a Manager.t -> 'a t -> box1

Convert the abstract value to an hypercube . In case of an empty (bottom) abstract element, all the intervals in the returned box are empty. For abstract elements with empty environments (no variable), it is impossible to distinguish a bottom element from a top element. Converting the box back to an abstract element with of_box will then always construct a top element.

val to_lincons_array : 'a Manager.t -> 'a t -> 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 Manager.t -> 'a t -> Tcons1.earray

val to_generator_array : 'a Manager.t -> 'a t -> Generator1.earray

Convert the abstract value to a set of generators that defines it.

Operations

Meet and Join

val meet : 'a Manager.t -> 'a t -> 'a t -> 'a t

Meet of 2 abstract values.

val meet_array : 'a Manager.t -> 'a t array -> 'a t

Meet of a non empty array of abstract values.

val meet_lincons_array : 'a Manager.t -> 'a t -> Lincons1.earray -> 'a t

Meet of an abstract value with an array of linear constraints.

val meet_tcons_array : 'a Manager.t -> 'a t -> Tcons1.earray -> 'a t

Meet of an abstract value with an array of tree expressions constraints.

val join : 'a Manager.t -> 'a t -> 'a t -> 'a t

Join of 2 abstract values.

val join_array : 'a Manager.t -> 'a t array -> 'a t

Join of a non empty array of abstract values.

val add_ray_array : 'a Manager.t -> 'a t -> 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 Manager.t -> 'a t -> 'a t -> unit

val meet_lincons_array_with : 'a Manager.t -> 'a t -> Lincons1.earray -> unit

val meet_tcons_array_with : 'a Manager.t -> 'a t -> Tcons1.earray -> unit

val join_with : 'a Manager.t -> 'a t -> 'a t -> unit

val add_ray_array_with : 'a Manager.t -> 'a t -> Generator1.earray -> unit

Assignement and Substitutions

val assign_linexpr_array : 'a Manager.t ->
       'a t ->
       Var.t array -> 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 Manager.t ->
       'a t ->
       Var.t array -> 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 Manager.t ->
       'a t ->
       Var.t array -> 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 Manager.t ->
       'a t ->
       Var.t array -> 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 Manager.t ->
       'a t ->
       Var.t array -> Linexpr1.t array -> 'a t option -> unit

val substitute_linexpr_array_with : 'a Manager.t ->
       'a t ->
       Var.t array -> Linexpr1.t array -> 'a t option -> unit

val assign_texpr_array_with : 'a Manager.t ->
       'a t ->
       Var.t array -> Texpr1.t array -> 'a t option -> unit

val substitute_texpr_array_with : 'a Manager.t ->
       'a t ->
       Var.t array -> 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 Manager.t -> 'a t -> Var.t array -> bool -> 'a t

val forget_array_with : 'a Manager.t -> 'a t -> Var.t array -> bool -> unit

Change and permutation of dimensions

val change_environment : 'a Manager.t -> 'a t -> Environment.t -> bool -> 'a t

Change the environment 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 the former.

val minimize_environment : 'a 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 Manager.t ->
       'a t -> Var.t array -> 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 Manager.t -> 'a t -> Environment.t -> bool -> unit

val minimize_environment_with : 'a Manager.t -> 'a t -> unit

val rename_array_with : 'a Manager.t -> 'a t -> Var.t array -> 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,

expand P(x,y,z) z w = P(x,y,z) inter P(x,y,w) if z is expanded in z and w
fold Q(x,y,z,w) z w = exists w:Q(x,y,z,w) union (exist z:Q(x,y,z,w))(z<-w) if z and w are folded onto z

val expand : 'a Manager.t -> 'a t -> Var.t -> 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 environment.

val fold : 'a Manager.t -> 'a t -> 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 Manager.t -> 'a t -> Var.t -> Var.t array -> unit

val fold_with : 'a Manager.t -> 'a t -> Var.t array -> unit

Widening

val widening : 'a 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 Manager.t ->
       'a t -> 'a t -> Lincons1.earray -> 'a t

Closure operation

val closure : 'a Manager.t -> 'a t -> 'a t

Closure: transform strict constraints into non-strict ones.

val closure_with : 'a Manager.t -> 'a t -> unit

Side-effect version

Additional operations

val of_lincons_array : 'a Manager.t -> Environment.t -> Lincons1.earray -> 'a t

val of_tcons_array : 'a Manager.t -> Environment.t -> Tcons1.earray -> 'a t

Abstract a conjunction of constraints

val assign_linexpr : 'a Manager.t ->
       'a t ->
       Var.t -> Linexpr1.t -> 'a t option -> 'a t

val substitute_linexpr : 'a Manager.t ->
       'a t ->
       Var.t -> Linexpr1.t -> 'a t option -> 'a t

val assign_texpr : 'a Manager.t ->
       'a t ->
       Var.t -> Texpr1.t -> 'a t option -> 'a t

val substitute_texpr : 'a Manager.t ->
       'a t ->
       Var.t -> Texpr1.t -> 'a t option -> 'a t

Assignement/Substitution of a single dimension by a single expression

val assign_linexpr_with : 'a Manager.t ->
       'a t -> Var.t -> Linexpr1.t -> 'a t option -> unit

val substitute_linexpr_with : 'a Manager.t ->
       'a t -> Var.t -> Linexpr1.t -> 'a t option -> unit

val assign_texpr_with : 'a Manager.t ->
       'a t -> Var.t -> Texpr1.t -> 'a t option -> unit

val substitute_texpr_with : 'a Manager.t ->
       'a t -> Var.t -> Texpr1.t -> 'a t option -> unit

Side-effect version of the previous functions

val unify : 'a Manager.t -> 'a t -> 'a t -> 'a t

Unification of 2 abstract values on their least common environment

val unify_with : 'a Manager.t -> 'a t -> 'a t -> unit

Side-effect version