apronext 1.0.1 · OCaml Package

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 t = Apron.Tcons1.t

type typ = Apron.Lincons0.typ =

| EQ
| SUPEQ
| SUP
| DISEQ
| 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 : 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, Format.formatter, unit) format ->
  ?sep:(unit, Format.formatter, unit) format ->
  ?last:(unit, Format.formatter, unit) format ->
  Format.formatter ->
  Apron.Tcons1.earray ->
  unit

Print an array of constraints

val array_length : Apron.Tcons1.earray -> int

Get the size of the array

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

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

val eq : 
  ?typ:Apron.Texpr1.typ ->
  ?round:Apron.Texpr1.round ->
  Apron.Texpr1.t ->
  Apron.Texpr1.t ->
  t

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 diseq : 
  ?typ:Apron.Texpr1.typ ->
  ?round:Apron.Texpr1.round ->
  Apron.Texpr1.t ->
  Apron.Texpr1.t ->
  t

val geq : 
  ?typ:Apron.Texpr1.typ ->
  ?round:Apron.Texpr1.round ->
  Apron.Texpr1.t ->
  Apron.Texpr1.t ->
  t

val leq : 
  ?typ:Apron.Texpr1.typ ->
  ?round:Apron.Texpr1.round ->
  Apron.Texpr1.t ->
  Apron.Texpr1.t ->
  t

val gt : 
  ?typ:Apron.Texpr1.typ ->
  ?round:Apron.Texpr1.round ->
  Apron.Texpr1.t ->
  Apron.Texpr1.t ->
  t

val lt : 
  ?typ:Apron.Texpr1.typ ->
  ?round:Apron.Texpr1.round ->
  Apron.Texpr1.t ->
  Apron.Texpr1.t ->
  t

val neg_typ : typ -> typ

type of constraint negation; i.e : EQ -> DISEQ | SUP -> SUPEQ

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

package apronext

Type array

Extensions