`Goblint_lib.LinearTwoVarEqualityDomain`

OCaml implementation of the linear two-variable equality domain.

Abstract states in this domain are represented by structs containing an array and an apron environment. The arrays are modeled as proposed in the paper: Each variable is assigned to an index and each array element represents a linear relationship that must hold at the corresponding program point. The apron environment is hereby used to organize the order of columns and variables.

`module M = Messages`

`module Mpqf = SharedFunctions.Mpqf`

`module Rhs : sig ... end`

`module EqualitiesConjunction : sig ... end`

`module VarManagement : sig ... end`

`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 ExpressionBounds :
SharedFunctions.ConvBounds with type t = VarManagement.t
```

`module D : sig ... end`

`module D2 : RelationDomain.RD with type var = Apron.Var.t`