Module SemDiffLib.CongruenceClosureSolver

module F = Stdlib.Format
module Atom : sig ... end
type enode = {
  1. head : Atom.t;
  2. children : Atom.t list;
}
val equal_enode : enode -> enode -> bool
val hash_fold_enode : Ppx_hash_lib.Std.Hash.state -> enode -> Ppx_hash_lib.Std.Hash.state
val hash_enode : enode -> Ppx_hash_lib.Std.Hash.hash_value
type term =
  1. | Enode of enode
  2. | Atom of Atom.t
val pp_term : F.formatter -> term -> unit
type t
val pp_nested_term : ?depth:int -> t -> F.formatter -> Atom.t -> unit
val init : debug:bool -> t
type header = private Atom.t
val pp_header : F.formatter -> header -> unit
val mk_header : t -> string -> header
val mk_term : t -> header -> Atom.t list -> Atom.t
val unsafe_header_of_atom : Atom.t -> header
val merge : t -> Atom.t -> term -> unit
val is_equiv : t -> Atom.t -> Atom.t -> bool
val representative : t -> Atom.t -> Atom.t
val representative_of_header : t -> header -> Atom.t
val fold_term_roots : t -> header -> f:(Atom.t -> 'a -> 'a) -> init:'a -> 'a
val iter_app_roots : t -> f:(Atom.t -> unit) -> unit
val iter_term_roots : t -> header -> f:(Atom.t -> unit) -> unit
val set_diff : t -> diff_header:header -> resolved:Atom.t -> unit
val get_diff : t -> (header * Atom.t) option
val equiv_atoms : t -> Atom.t -> Atom.t list
val headers_with_arity : t -> (header * int) list
val get_enode : t -> Atom.t -> enode option
type app_equation = {
  1. atom : Atom.t;
  2. enode : enode;
}
val equiv_terms : t -> Atom.t -> app_equation list
val reset_update_count : t -> unit
val get_update_count : t -> int
val show_stats : t -> unit
val debug : t -> unit