package apronext

  1. Overview
  2. Docs

Module Apronext.LinconsextSource

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

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

type t = Apron.Lincons1.t
val make : Apron.Linexpr1.t -> Apron.Lincons1.typ -> t

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

val copy : t -> t

Copy (deep copy)

val string_of_typ : Apron.Lincons1.typ -> string

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

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

Print the linear constraint

val get_typ : t -> Apron.Lincons1.typ

Get the constraint type

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

Iter the function on the pair coefficient/variable of the underlying linear expression

val get_cst : t -> Apron.Coeff.t

Get the constant of the underlying linear expression

val set_typ : t -> Apron.Lincons1.typ -> unit

Set the constraint type

val set_list : t -> (Apron.Coeff.t * Apron.Var.t) list -> Apron.Coeff.t option -> unit

Set simultaneously a number of coefficients.

set_list expr [(c1,"x"); (c2,"y")] (Some cst) assigns coefficients c1 to variable "x", coefficient c2 to variable "y", and coefficient cst to the constant. If (Some cst) is replaced by None, the constant coefficient is not assigned.

val set_array : t -> (Apron.Coeff.t * Apron.Var.t) array -> Apron.Coeff.t option -> unit

Set simultaneously a number of coefficients, as set_list.

val set_cst : t -> Apron.Coeff.t -> unit

Set the constant of the underlying linear expression

val get_coeff : t -> Apron.Var.t -> Apron.Coeff.t

Get the coefficient of the variable in the underlying linear expression

val set_coeff : t -> Apron.Var.t -> Apron.Coeff.t -> unit

Set the coefficient of the variable in the underlying linear expression

val make_unsat : Apron.Environment.t -> t

Build the unsatisfiable constraint -1>=0

val is_unsat : t -> bool

Is the constraint not satisfiable ?

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 linear constraint

val get_linexpr1 : t -> Apron.Linexpr1.t

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

val get_lincons0 : t -> Apron.Lincons0.t

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

Type array

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

Make an array of linear 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.Lincons1.earray -> unit

Print an array of constraints

val array_length : Apron.Lincons1.earray -> int

Get the size of the array

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

Get the environment of the array

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

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

val array_set : Apron.Lincons1.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.Lincons1.earray -> Apron.Environment.t -> Apron.Lincons1.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.Lincons1.earray -> Apron.Environment.t -> unit

Side-effect version of the previous function

Extensions

Sourceval neg_typ : Apron.Lincons1.typ -> Apron.Lincons1.typ

type of constraint negation

Sourceval neg : t -> t

constraints negation : constructs a new constraint in opposite direction. e.g : a >= b -> a < b

Sourceval spliteq : t -> t * t

Equality splitting : split a = b into a >= b and a <= b. Raises Invalid_argument if the constraint is not an equality

Sourceval splitdiseq : t -> t * t

Disequality splitting split a <> b into a > b or a < b, Raises Invalid_argument if the constraint is not a disequality

Sourceval pp_print : Format.formatter -> t -> unit

Human readable pretty-printing

Higher-order functions utilities

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

fold f g l folds over the different monom of the linear expression l, with as an initial accumulato the value (g (get_cst l)).

Sourceval array_fold : ('a -> t -> 'a) -> 'a -> Apron.Lincons1.earray -> 'a

fold function over generator.earay

Sourceval array_iter : (t -> unit) -> Apron.Lincons1.earray -> unit

iter function over generator.earay

Sourceval array_for_all : (t -> bool) -> Apron.Lincons1.earray -> bool

forall function over generator.earay

Sourceval array_exists : (t -> bool) -> Apron.Lincons1.earray -> bool

exists function over generator.earay

Sourceval array_to_list : Apron.Lincons1.earray -> t list

to list conversion

Sourceval array_of_list : t list -> Apron.Lincons1.earray

of list build