Module Abstract0


module Abstract0: sig .. end
APRON Abstract value of level 0

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) -> 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,


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:


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, Format.formatter, unit) Pervasives.format ->
?sep:(unit, Format.formatter, unit) Pervasives.format ->
?last:(unit, Format.formatter, unit) Pervasives.format ->
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a array -> unit
General use