Module LinearTwoVarEqualityDomain.EqualitiesConjunction

module IntMap : sig ... end
type t = int * Rhs.t IntMap.t
val equal : t -> t -> Ppx_deriving_runtime.bool
val compare : t -> t -> Ppx_deriving_runtime.int
val show_formatted : (IntMap.key -> string) -> ((Z.t * IntMap.key) option * Z.t * Z.t) IntMap.t -> string
val show : ((Z.t * IntMap.key) option * Z.t * Z.t) IntMap.t -> string
val hash : (int * Rhs.t IntMap.t) -> int
val empty : unit -> int * 'a IntMap.t

creates a domain of dimension 0

val make_empty_conj : 'a -> 'a * 'b IntMap.t

creates a domain of dimension len without any valid equalities

val nontrivial : ('a * 'b IntMap.t) -> IntMap.key -> bool

trivial equalities are of the form var_i = var_i and are not kept explicitely in the sparse representation of EquanlitiesConjunction

val inverse : 'a -> ('b * 'c * Z.t * 'd) -> 'c * (('d * 'a) option * Z.t * 'b)

turn x = (cy+o)/d into y = (dx-o)/c

val get_rhs : ('a * ((Z.t * IntMap.key) option * Z.t * Z.t) IntMap.t) -> IntMap.key -> (Z.t * IntMap.key) option * Z.t * Z.t

sparse implementation of get rhs for lhs, but will default to no mapping for sparse entries

val set_rhs : ('a * Rhs.t IntMap.t) -> IntMap.key -> Rhs.t -> 'a * Rhs.t IntMap.t

set_rhs, staying loyal to immutable, sparse map underneath; do not attempt any normalization

val canonicalize_and_set : ('a * Rhs.t IntMap.t) -> IntMap.key -> ((Z.t * int) option * Z.t * Z.t) -> 'a * Rhs.t IntMap.t

canonicalize equation, and set_rhs, staying loyal to immutable, sparse map underneath

val copy : 'a -> 'a
val modify_variables_in_domain : (IntMap.key * ((Z.t * IntMap.key) option * Z.t * Z.t) IntMap.t) -> IntMap.key array -> (IntMap.key -> int -> IntMap.key) -> IntMap.key * ((Z.t * IntMap.key) option * Z.t * Z.t) IntMap.t
val is_empty : (int * 'a) -> bool

required by AbstractRelationalDomainRepresentation, true if dimension is zero

val is_top_array : (int option * Z.t) array -> bool
val is_top_con : ('a * 'b IntMap.t) -> bool
val forget_variable : ('a * Rhs.t IntMap.t) -> IntMap.key -> 'a * Rhs.t IntMap.t
val dim_add : Apron.Dim.change -> (IntMap.key * ((Z.t * IntMap.key) option * Z.t * Z.t) IntMap.t) -> IntMap.key * ((Z.t * IntMap.key) option * Z.t * Z.t) IntMap.t
val dim_remove : Apron.Dim.change -> (IntMap.key * Rhs.t IntMap.t) -> IntMap.key * Rhs.t IntMap.t
exception Contradiction
val meet_with_one_conj : ('a * ((Z.t * IntMap.key) option * Z.t * Z.t) IntMap.t) -> IntMap.key -> ((Z.t * IntMap.key) option * Z.t * Z.t) -> 'a * ((Z.t * IntMap.key) option * Z.t * Z.t) IntMap.t

affine transform variable i allover conj with transformer (Some (coeff,i)+offs)/divi