Module Lincons1


module Lincons1: sig .. end
APRON Constraints and array of constraints of level 1


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 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 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 environement of the constraint for a super-environement. 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 environement 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 environements
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 environements

Type array


val array_make : Environment.t -> int -> 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) Pervasives.format ->
?sep:(unit, Format.formatter, unit) Pervasives.format ->
?last:(unit, Format.formatter, unit) Pervasives.format ->
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 environement; otherwise a Failure exception is raised.
val array_extend_environment : earray -> Environment.t -> 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 : earray -> Environment.t -> unit
Side-effect version of the previous function