Module AffineEqualityDomain.VarManagement

It defines the type t of the affine equality domain (a struct that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by RelationDomain.D2) such as add_vars remove_vars. Furthermore, it provides the function get_coeff_vec that parses an apron expression into a vector of coefficients if the apron expression has an affine form.

Parameters

Signature

module Vector : sig ... end
module Matrix : sig ... end
val dim_add : Apron.Dim.change -> Matrix.t -> Matrix.t
include sig ... end
type t = {
  1. mutable d : AffineEqualityMatrix(Vec)(Mx).t option;
  2. mutable env : GobApron.Environment.t;
}
val equal : t -> t -> Ppx_deriving_runtime.bool
val compare : t -> t -> Ppx_deriving_runtime.int
val hash : t -> int
val empty_env : GobApron.Environment.t
val bot : unit -> t
val get_env : t -> GobApron.Environment.t
val bot_env : t
val is_bot_env : t -> bool
val copy : t -> t
val dimchange2_add : t -> GobApron.Environment.t -> t
val dimchange2_remove : t -> GobApron.Environment.t -> t
val vars : t -> Apron.Var.t list
val add_vars : t -> Apron.Var.t list -> t
val remove_vars : t -> Apron.Var.t list -> t
val remove_vars_with : t -> Apron.Var.t list -> unit
val remove_filter : t -> (Apron.Var.t -> bool) -> t
val remove_filter_with : t -> (Apron.Var.t -> bool) -> unit
val keep_filter : t -> (Apron.Var.t -> bool) -> t
val keep_vars : t -> Apron.Var.t list -> t
val mem_var : t -> Apron.Var.t -> bool
include sig ... end
val (*:) : Mpqf.t -> Mpqf.t -> Mpqf.t
val (+:) : Mpqf.t -> Mpqf.t -> Mpqf.t
val (-:) : Mpqf.t -> Mpqf.t -> Mpqf.t
val (/:) : Mpqf.t -> Mpqf.t -> Mpqf.t
val (=:) : Mpqf.t -> Mpqf.t -> Ppx_deriving_runtime.bool
val (<>:) : Mpqf.t -> Mpqf.t -> bool
val (<:) : Mpqf.t -> Mpqf.t -> bool
val (>:) : Mpqf.t -> Mpqf.t -> bool
val (<=:) : Mpqf.t -> Mpqf.t -> bool
val (>=:) : Mpqf.t -> Mpqf.t -> bool
val of_int : int -> Mpqf.t

Get the constant from the vector if it is a constant

val to_constant_opt : Vector.t -> Mpqf.t option
val get_coeff_vec : t -> Apron.Texpr1.expr -> Vector.t option