apronext 1.0.4 (latest) · OCaml Package

This file is an extension for the Environment from the apron Library

Note : It only adds function, nothing is removed. Extensions are at the end of the module

type t = Apron.Environment.t

type typvar = Apron.Environment.typvar =

| INT
| REAL

val make : Apron.Var.t array -> Apron.Var.t array -> t

Making an environment from a set of integer and real variables. Raise Failure in case of name conflict.

val add : t -> Apron.Var.t array -> Apron.Var.t array -> t

Adding to an environment a set of integer and real variables. Raise Failure in case of name conflict.

val remove : t -> Apron.Var.t array -> t

Remove from an environment a set of variables. Raise Failure in case of non-existing variables.

val rename : t -> Apron.Var.t array -> Apron.Var.t array -> t

Renaming in an environment a set of variables. Raise Failure in case of interferences with the variables that are not renamed.

val rename_perm : 
  t ->
  Apron.Var.t array ->
  Apron.Var.t array ->
  t * Apron.Dim.perm

Similar to previous function, but returns also the permutation on dimensions induced by the renaming.

val lce : t -> t -> t

Compute the least common environment of 2 environment, that is, the environment composed of all the variables of the 2 environments. Raise Failure if the same variable has different types in the 2 environment.

val lce_change : 
  t ->
  t ->
  t * Apron.Dim.change option * Apron.Dim.change option

Similar to the previous function, but returns also the transformations required to convert from e1 (resp. e2) to the lce. If None is returned, this means that e1 (resp. e2) is identic to the lce.

val dimchange : t -> t -> Apron.Dim.change

dimchange e1 e2 computes the transformation for converting from an environment e1 to a superenvironment e2. Raises Failure if e2 is not a superenvironment.

val dimchange2 : t -> t -> Apron.Dim.change2

dimchange2 e1 e2 computes the transformation for converting from an environment e1 to a (compatible) environment e2, by first adding (some) variables of e2 and then removing (some) variables of e1. Raises Failure if the two environments are incompatible.

val equal : t -> t -> bool

Test equality if two environments

val compare : t -> t -> int

Compare two environment. compare env1 env2 return -2 if the environements are not compatible (a variable has different types in the 2 environements), -1 if env1 is a subset of env2, 0 if equality, +1 if env1 is a superset of env2, and +2 otherwise (the lce exists and is a strict superset of both)

val hash : t -> int

Hashing function for environments

val dimension : t -> Apron.Dim.dimension

Return the dimension of the environment

val size : t -> int

Return the size of the environment

val mem_var : t -> Apron.Var.t -> bool

Return true if the variable is present in the environment.

val typ_of_var : t -> Apron.Var.t -> typvar

Return the type of variables in the environment. If the variable does not belong to the environment, raise a Failure exception.

val vars : t -> Apron.Var.t array * Apron.Var.t array

Return the (lexicographically ordered) sets of integer and real variables in the environment

val var_of_dim : t -> Apron.Dim.t -> Apron.Var.t

Return the variable corresponding to the given dimension in the environment. Raise Failure is the dimension is out of the range of the environment (greater than or equal to dim env)

val dim_of_var : t -> Apron.Var.t -> Apron.Dim.t

Return the dimension associated to the given variable in the environment. Raise Failure if the variable does not belong to the environment.

val print : 
  ?first:(unit, Format.formatter, unit) format ->
  ?sep:(unit, Format.formatter, unit) format ->
  ?last:(unit, Format.formatter, unit) format ->
  Format.formatter ->
  t ->
  unit

Printing

Extensions

val make_s : string array -> string array -> t

environment build from variable string names

val empty : t

empty environment

exception DuplicateName of string

Exception to raise when adding a variable that alread exists in the environment

val add_check : t -> Apron.Var.t array -> Apron.Var.t array -> t

same as add but first check if the variables exist in the environement and raises DuplicateName is it is the case.

val add_one : (Apron.Var.t * typvar) -> t -> t

adds one variable to an environment according to its type

val add_one_s : (string * typvar) -> t -> t

same as add_one but with string instread of Var.t

val add_int : Apron.Var.t -> t -> t

adds an integer variable

val add_int_s : string -> t -> t

same as add_one but with string instread of Var.t

val add_real : Apron.Var.t -> t -> t

adds a real variable

val add_real_s : string -> t -> t

same as add_real but with string instread of Var.t

val join : t -> t -> t

join two environments

val fold : ('a -> Apron.Var.t -> 'a) -> 'a -> t -> 'a

Envrironment folding function

val iter : (Apron.Var.t -> unit) -> t -> unit

Iteration of a function over an environment

val get_ints : t -> Apron.Var.t array

returns the array of integer variables

val get_reals : t -> Apron.Var.t array

returns the array of real variables

package apronext

Extensions