package apronext

  1. Overview
  2. Docs

This file is an extension for the Tcons1 module from the apron Library

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

type typ = Apron.Lincons0.typ =
  1. | EQ
  2. | SUPEQ
  3. | SUP
  4. | DISEQ
  5. | EQMOD of Apron.Scalar.t
val make : Apron.Texpr1.t -> typ -> t

Make a tree expression constraint. Modifying later the linear expression (not advisable) modifies correspondingly the tree expression constraint and conversely, except for changes of environements

val copy : t -> t

Copy (deep copy)

val string_of_typ : typ -> string

Convert a constraint type to a string (=,>=, or >)

val print : Stdlib.Format.formatter -> t -> unit

Print the tree expression constraint

val get_typ : t -> typ

Get the constraint type

val set_typ : t -> typ -> unit

Set the constraint type

val extend_environment : t -> Apron.Environment.t -> t

Change the environement of the constraint for a super-environement. Raise Failure if it is not the case

val extend_environment_with : t -> Apron.Environment.t -> unit

Side-effect version of the previous function

val get_env : t -> Apron.Environment.t

Get the environement of the tree expression constraint

val get_texpr1 : t -> Apron.Texpr1.t

Get the underlying linear expression. Modifying the linear expression (not advisable) modifies correspondingly the tree expression constraint and conversely, except for changes of environements

val get_tcons0 : t -> Apron.Tcons0.t

Get the underlying tree expression constraint of level 0. Modifying the constraint of level 0 (not advisable) modifies correspondingly the tree expression constraint and conversely, except for changes of environements

Type array

val array_make : Apron.Environment.t -> int -> Apron.Tcons1.earray

Make an array of tree expression constraints with the given size and defined on the given environement. The elements are initialized with the constraint 0=0.

val array_print : ?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 -> Apron.Tcons1.earray -> unit

Print an array of constraints

val array_length : Apron.Tcons1.earray -> int

Get the size of the array

Get the environment of the array

val array_get : Apron.Tcons1.earray -> int -> t

Get the element of the given index (which is not a copy)

val array_set : Apron.Tcons1.earray -> int -> t -> unit

Set the element of the given index (without any copy). The array and the constraint should be defined on the same environement; otherwise a Failure exception is raised.

val array_extend_environment : Apron.Tcons1.earray -> Apron.Environment.t -> Apron.Tcons1.earray

Change the environement of the array of constraints for a super-environement. Raise Failure if it is not the case

val array_extend_environment_with : Apron.Tcons1.earray -> Apron.Environment.t -> unit

Side-effect version of the previous function

Extensions

The following functions build the constraints corresponding to 'e1 op e2', where op is repectivelly (=,<>,>=,<=,>,<). The type underlying expression will be Real if left unspecified, and its rounding mode will be Near if left unspecified

val neg : t -> t

constraints negation; e.g : a >= b -> a < b

val splitdiseq : t -> t * t

split a = b into (a > b),(a < b)

Higher-order functions utilities

val array_fold : ('a -> t -> 'a) -> 'a -> Apron.Tcons1.earray -> 'a

fold function over generator.earay

val array_iter : (t -> unit) -> Apron.Tcons1.earray -> unit

iter function over generator.earay

val array_for_all : (t -> bool) -> Apron.Tcons1.earray -> bool

forall function over generator.earay

val array_exists : (t -> bool) -> Apron.Tcons1.earray -> bool

exists function over generator.earay

val array_to_list : Apron.Tcons1.earray -> t list

to list conversion

val array_of_list : t list -> Apron.Tcons1.earray

of list build