module Lincons1: sig .. end
APRON Constraints and array of constraints of level 1
type
}
type
}
APRON Constraints and array of constraints of level 1
type 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