Rhs (goblint.Goblint_lib.LinearTwoVarEqualityDomain.Rhs)

type t =
  (Goblint_std.GobZ.t * int) option * Goblint_std.GobZ.t * Goblint_std.GobZ.t

val equal : t -> t -> Ppx_deriving_runtime.bool

val compare : t -> t -> Ppx_deriving_runtime.int

val hash : t -> int

val var_zero : 'a -> (Z.t * 'a) option * Z.t * Z.t

val pretty_coeff : unit -> Z.t -> GoblintCil.Pretty.doc

val pretty_rhs_formatted : 
  (unit -> 'a -> GoblintCil.Pretty.doc) ->
  unit ->
  ((Z.t * 'a) option * Z.t * 'b) ->
  GoblintCil.Pretty.doc

val pretty : unit -> ((Z.t * int) option * Z.t * Z.t) -> GoblintCil.Pretty.doc

val canonicalize : 
  ((Z.t * 'a) option * Z.t * Z.t) ->
  (Z.t * 'a) option * Z.t * Z.t

factor out gcd from all terms, i.e. ax=by+c with a positive is the canonical form for adx+bdy+cd

val subst : 
  ((Z.t * 'a) option * Z.t * Z.t) ->
  'a ->
  ((Z.t * 'a) option * Z.t * Z.t) ->
  (Z.t * 'a) option * Z.t * Z.t

Substitute rhs for varx in rhs'