Module LinearTwoVarEqualityDomain.VarManagement

VarManagement defines the type t of the affine equality domain (a record 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 simplified_monomials_from_texp that converts an apron expression into a list of monomials of reference variables and a constant offset

module EConj = EqualitiesConjunction
include sig ... end
type t = {
  1. mutable d : EConj.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
val dim_add : Apron.Dim.change -> (EConj.IntMap.key * ((Z.t * EConj.IntMap.key) option * Z.t * Z.t) EConj.IntMap.t) -> EConj.IntMap.key * ((Z.t * EConj.IntMap.key) option * Z.t * Z.t) EConj.IntMap.t
val size : t -> int
val monomials_from_texp : t -> Apron.Texpr1.expr -> ((Goblint_std.GobZ.t * Apron.Dim.t) option * Goblint_std.GobZ.t * Goblint_std.GobZ.t) list option

Parses a Texpr to obtain a (coefficient, variable) pair list to repr. a sum of a variables that have a coefficient. If variable is None, the coefficient represents a constant offset.

val simplified_monomials_from_texp : t -> GobApron.Texpr1.Expr.t -> ((Z.t * Batteries.Int.t * Z.t) list * (Z.t * Z.t)) option
val simplify_to_ref_and_offset : t -> GobApron.Texpr1.Expr.t -> ((Z.t * Batteries.Int.t) option * Z.t * Z.t) option