# 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

TO BE DOCUMENTED

### 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`

#### Accessors

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

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

#### Tests

    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

    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

    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