Previous  Up  Next

Module Lincons1

module Lincons1: sig .. end
type t = {
   mutable lincons0 : Lincons0.t;
   mutable env : Environment.t;
} 
type earray = {
   mutable lincons0_array : Lincons0.t array;
   mutable array_env : Environment.t;
}

APRON Constraints and array of constraints of level 1

type typ = Lincons0.typ =
| EQ
| SUPEQ
| SUP
| DISEQ
| EQMOD of Scalar.t 
val make : Linexpr1.t -> typ -> t

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

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

val get_typ : t -> typ

Get the constraint type

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

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

val get_cst : t -> Coeff.t

Get the constant of the underlying linear expression

val set_typ : t -> typ -> unit

Set the constraint type

val set_list : t -> (Coeff.t * Var.t) list -> 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 -> (Coeff.t * Var.t) array -> Coeff.t option -> unit

Set simultaneously a number of coefficients, as set_list.

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

Set the constant of the underlying linear expression

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

Get the coefficient of the variable in the underlying linear expression

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

Set the coefficient of the variable in the underlying linear expression

val make_unsat : Environment.t -> t

Build the unsatisfiable constraint -1>=0

val is_unsat : t -> bool

Is the constraint not satisfiable ?

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

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

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

Side-effect version of the previous function

val get_env : t -> Environment.t

Get the environment of the linear constraint

val get_linexpr1 : t -> Linexpr1.t

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

val get_lincons0 : t -> 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 environments

Type array

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

Make an array of linear constraints with the given size and defined on the given environment. 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 -> earray -> unit

Print an array of constraints

val array_length : earray -> int

Get the size of the array

val array_get_env : earray -> Environment.t

Get the environment of the array

val array_get : earray -> int -> t

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

val array_set : 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 environment; otherwise a Failure exception is raised.

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

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

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

Side-effect version of the previous function