Module LinearTwoVarEqualityDomain.D

include module type of struct include Printable.Std end
val tag : 'a -> 'b
val arbitrary : unit -> 'a
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
include module type of struct include VarManagement end
module EConj = VarManagement.EConj
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
module Bounds = ExpressionBounds
module V = RelationDomain.V
module Arg : sig ... end
module Convert : sig ... end
type var = V.t
val name : unit -> string
val to_yojson : 'a -> 'b
val is_bot : t -> Ppx_deriving_runtime.bool

t.d is some empty array and env is empty

val top_of : GobApron.Environment.t -> t

forall x_i in env, x_i:=X_i+0

val top : unit -> t

env = \emptyset, d = Some(||)

val is_top : t -> bool

is_top returns true for top_of array and empty array; precondition: t.env and t.d are of same size

val is_top_env : t -> bool
val to_subscript : int -> string
val show_var : GobApron.Environment.t -> Apron.Dim.t -> string
val show : t -> string

prints the current variable equalities with resolved variable names

val pretty : unit -> t -> GoblintCil.Pretty.doc
val printXml : 'a BatInnerIO.output -> t -> unit
val eval_interval : 'a -> Bounds.t -> GobApron.Texpr1.t -> Z.t option * Z.t option
val meet_with_one_conj : t -> EConj.IntMap.key -> ((Z.t * Apron.Dim.t) option * Z.t * Z.t) -> t
val meet : t -> t -> t
val leq : t -> t -> bool
val join : t -> t -> t
val widen : t -> t -> t
val narrow : t -> t -> t
val pretty_diff : unit -> (t * t) -> GoblintCil.Pretty.doc
val forget_var : t -> Apron.Var.t -> t
val forget_vars : t -> Apron.Var.t list -> t
val assign_texpr : VarManagement.t -> Apron.Var.t -> GobApron.Texpr1.Expr.t -> t
val assign_exp : Queries.ask -> VarManagement.t -> GobApron.Var.t -> GoblintCil.Cil.exp -> bool Stdlib.Lazy.t -> t
val assign_var_parallel : t -> (GobApron.Var.t * GobApron.Var.t) list -> t
val assign_var_parallel_with : t -> (GobApron.Var.t * GobApron.Var.t) list -> unit
val assign_var_parallel' : t -> GobApron.Var.t list -> GobApron.Var.t list -> t
val substitute_exp : Queries.ask -> t -> GobApron.Var.t -> GoblintCil.Cil.exp -> bool Stdlib.Lazy.t -> t
val meet_tcons : 'a -> t -> GobApron.Tcons1.t -> GoblintCil.exp -> bool Stdlib.Lazy.t -> t
val unify : t -> t -> t
val assert_constraint : Queries.ask -> Bounds.t -> GoblintCil.Cil.exp -> bool -> bool Stdlib.Lazy.t -> t
val relift : 'a -> 'a
val invariant : t -> GobApron.Lincons1.t list

representation as C expression

This function returns all the equalities that are saved in our datastructure t.

Lincons -> linear constraint

val cil_exp_of_lincons1 : GobApron.Lincons1.t -> GoblintCil.Cil.exp option
type marshal = t
val marshal : 'a -> 'a
val unmarshal : 'a -> 'a