Module Abstract0

module Abstract0: sig .. end

type 'a t

APRON Abstract value of level 0

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

val set_gc : int -> unit

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 : (int -> string) -> Stdlib.Format.formatter -> 'a t -> unit

Print as a set of constraints

Serialization

Constructor, accessors, tests and property extraction

Basic constructors

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

Create a bottom (empty) value with the given number of integer and real variables

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

Create a top (universe) value with the given number of integer and real variables

val of_box : 'a Manager.t -> int -> int -> Interval.t array -> 'a t

Abstract an hypercube.

of_box man intdim realdim array abstracts an hypercube defined by the array of intervals of size intdim+realdim. If any interval is empty, the resulting abstract element is empty (bottom). In case of a 0-dimensional element (intdim+realdim=0), the abstract element is always top (not bottom).

Accessors

val dimension : 'a Manager.t -> 'a t -> Dim.dimension

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

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 2 abstract values should be compatible.

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

Equality test. The 2 abstract values should be compatible.

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

Does the abstract value satisfy the linear constraint ?

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

Does the abstract value satisfy the tree expression constraint ?

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

Does the abstract value satisfy the constraint dim in interval ?

val is_dimension_unconstrained : 'a Manager.t -> 'a t -> Dim.t -> bool

Is the dimension 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_dimension : 'a Manager.t -> 'a t -> Dim.t -> Interval.t

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

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

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

val to_box : 'a Manager.t -> 'a t -> Interval.t array

Convert the abstract value to an hypercube. In case of an empty (bottom) abstract element of size n, the array contains n empty intervals. For 0-dimensional abstract elements, the array has size 0, and it is impossible to distinguish a 0-dimensional bottom element from a 0-dimensional non-bottom (i.e., top) element. Converting it back to an abstract element with of_box will then always construct a 0-dimensional top element.

val to_lincons_array : 'a Manager.t -> 'a t -> Lincons0.t array

Convert the abstract value to a conjunction of linear constraints.

val to_tcons_array : 'a Manager.t -> 'a t -> Tcons0.t array

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

val to_generator_array : 'a Manager.t -> 'a t -> Generator0.t array

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 -> Lincons0.t array -> 'a t

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

val meet_tcons_array : 'a Manager.t -> 'a t -> Tcons0.t array -> 'a t

Meet of an abstract value with an array of tree expression 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 -> Generator0.t array -> '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 -> Lincons0.t array -> unit

val meet_tcons_array_with : 'a Manager.t -> 'a t -> Tcons0.t array -> unit

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

val add_ray_array_with : 'a Manager.t -> 'a t -> Generator0.t array -> unit

Assignements and Substitutions

val assign_linexpr_array : 'a Manager.t ->
       'a t ->
       Dim.t array -> Linexpr0.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 ->
       Dim.t array -> Linexpr0.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 ->
       Dim.t array -> Texpr0.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 ->
       Dim.t array -> Texpr0.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 ->
       Dim.t array -> Linexpr0.t array -> 'a t option -> unit

val substitute_linexpr_array_with : 'a Manager.t ->
       'a t ->
       Dim.t array -> Linexpr0.t array -> 'a t option -> unit

val assign_texpr_array_with : 'a Manager.t ->
       'a t ->
       Dim.t array -> Texpr0.t array -> 'a t option -> unit

val substitute_texpr_array_with : 'a Manager.t ->
       'a t ->
       Dim.t array -> Texpr0.t array -> 'a t option -> unit

Projections

These functions implements forgeting (existential quantification) of (array of) dimensions. 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 -> Dim.t array -> bool -> 'a t

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

Change and permutation of dimensions

val add_dimensions : 'a Manager.t -> 'a t -> Dim.change -> bool -> 'a t

val remove_dimensions : 'a Manager.t -> 'a t -> Dim.change -> 'a t

val apply_dimchange2 : 'a Manager.t -> 'a t -> Dim.change2 -> bool -> 'a t

val permute_dimensions : 'a Manager.t -> 'a t -> Dim.perm -> 'a t

Side-effect versions of the previous functions

val add_dimensions_with : 'a Manager.t -> 'a t -> Dim.change -> bool -> unit

val remove_dimensions_with : 'a Manager.t -> 'a t -> Dim.change -> unit

val apply_dimchange2_with : 'a Manager.t -> 'a t -> Dim.change2 -> bool -> unit

val permute_dimensions_with : 'a Manager.t -> 'a t -> Dim.perm option -> 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 -> Dim.t -> int -> 'a t

Expansion: expand a dim n expands the dimension dim into itself + n additional dimensions. It results in (n+1) unrelated dimensions having same relations with other dimensions. The (n+1) dimensions are put as follows:

original dimension dim
if the dimension is integer, the n additional dimensions are put at the end of integer dimensions; if it is real, at the end of the real dimensions.

val fold : 'a Manager.t -> 'a t -> Dim.t array -> 'a t

Folding: fold a tdim fold the dimensions in the array tdim of size n>=1 and put the result in the first dimension of the array. The other dimensions of the array are then removed (using ap_abstract0_permute_remove_dimensions).

val expand_with : 'a Manager.t -> 'a t -> Dim.t -> int -> unit

val fold_with : 'a Manager.t -> 'a t -> Dim.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 -> Lincons0.t array -> '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 -> int -> int -> Lincons0.t array -> 'a t

val of_tcons_array : 'a Manager.t -> int -> int -> Tcons0.t array -> 'a t

Abstract a conjunction of constraints

val assign_linexpr : 'a Manager.t ->
       'a t ->
       Dim.t -> Linexpr0.t -> 'a t option -> 'a t

val substitute_linexpr : 'a Manager.t ->
       'a t ->
       Dim.t -> Linexpr0.t -> 'a t option -> 'a t

val assign_texpr : 'a Manager.t ->
       'a t ->
       Dim.t -> Texpr0.t -> 'a t option -> 'a t

val substitute_texpr : 'a Manager.t ->
       'a t ->
       Dim.t -> Texpr0.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 -> Dim.t -> Linexpr0.t -> 'a t option -> unit

val substitute_linexpr_with : 'a Manager.t ->
       'a t -> Dim.t -> Linexpr0.t -> 'a t option -> unit

val assign_texpr_with : 'a Manager.t ->
       'a t -> Dim.t -> Texpr0.t -> 'a t option -> unit

val substitute_texpr_with : 'a Manager.t ->
       'a t -> Dim.t -> Texpr0.t -> 'a t option -> unit

Side-effect version of the previous functions

val print_array : ?first:(unit, Stdlib.Format.formatter, unit) Stdlib.format ->
       ?sep:(unit, Stdlib.Format.formatter, unit) Stdlib.format ->
       ?last:(unit, Stdlib.Format.formatter, unit) Stdlib.format ->
       (Stdlib.Format.formatter -> 'a -> unit) ->
       Stdlib.Format.formatter -> 'a array -> unit

General use