Previous  Up  Next

Module Tcons1

module Tcons1: sig .. end
type t = {
   mutable tcons0 : Tcons0.t;
   mutable env : Environment.t;
} 
type earray = {
   mutable tcons0_array : Tcons0.t array;
   mutable array_env : Environment.t;
}

APRON tree constraints and array of tree constraints of level 1

type typ = Lincons0.typ =
| EQ
| SUPEQ
| SUP
| DISEQ
| EQMOD of Scalar.t 
val make : 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 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 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 -> 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 tree expression constraint

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

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

Type array

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

Make an array of tree expression 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