C2PODomain (goblint.Goblint_lib.C2poDomain.C2PODomain)

include module type of struct include Printable.StdLeaf end

include module type of struct include Printable.Std end

val tag : 'a -> 'b

val arbitrary : unit -> 'a

val relift : 'a -> 'a

type t = CongruenceClosure.t

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

val hash : t -> int

val show : CongruenceClosure.t -> string

val name : unit -> string

type domain = t

include sig ... end

val pretty : unit -> domain -> Printable.Pretty.doc

val printXml : 'a BatInnerIO.output -> domain -> unit

val to_yojson : domain -> [> `String of string ]

val equal_standard : CongruenceClosure.t -> CongruenceClosure.t -> bool

val equal_normal_form : CongruenceClosure.t -> CongruenceClosure.t -> bool

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

val bot : unit -> 'a

val is_bot : 'a -> bool

val empty : unit -> CongruenceClosure.t

val init : unit -> CongruenceClosure.t

val top : unit -> CongruenceClosure.t

val is_top : CongruenceClosure.t -> bool

val join_f : 
  CongruenceClosure.t ->
  CongruenceClosure.t ->
  (CongruenceClosure.data ->
    CongruenceClosure.data ->
    CongruenceClosure.data * 'a) ->
  CongruenceClosure.t

val join : t -> t -> CongruenceClosure.t

val widen_automata : t -> t -> CongruenceClosure.t

val widen_eq_classes : 
  CongruenceClosure.t ->
  CongruenceClosure.t ->
  CongruenceClosure.t

val widen : t -> t -> CongruenceClosure.t

val meet : CongruenceClosure.t -> CongruenceClosure.t -> CongruenceClosure.t

val narrow : CongruenceClosure.t -> CongruenceClosure.t -> CongruenceClosure.t

val leq : CongruenceClosure.t -> CongruenceClosure.t -> bool

val pretty_diff : 
  unit ->
  (CongruenceClosure.t * CongruenceClosure.t) ->
  GoblintCil.Pretty.doc