sig
  module type S =
    sig
      type term
      type t
      val create : ?size:int -> unit -> Congruence.S.t
      val clear : Congruence.S.t -> unit
      val push : Congruence.S.t -> unit
      val pop : Congruence.S.t -> unit
      val stack_size : Congruence.S.t -> int
      val find : Congruence.S.t -> Congruence.S.term -> Congruence.S.term
      val iter :
        Congruence.S.t ->
        (mem:Congruence.S.term -> repr:Congruence.S.term -> unit) -> unit
      val iter_roots : Congruence.S.t -> (Congruence.S.term -> unit) -> unit
      val mk_eq :
        Congruence.S.t -> Congruence.S.term -> Congruence.S.term -> unit
      val mk_less :
        Congruence.S.t -> Congruence.S.term -> Congruence.S.term -> unit
      val is_eq :
        Congruence.S.t -> Congruence.S.term -> Congruence.S.term -> bool
      val is_less :
        Congruence.S.t -> Congruence.S.term -> Congruence.S.term -> bool
      val cycles : Congruence.S.t -> bool
    end
  module type TERM =
    sig
      type t
      val equal : Congruence.TERM.t -> Congruence.TERM.t -> bool
      val hash : Congruence.TERM.t -> int
      val subterms : Congruence.TERM.t -> Congruence.TERM.t list
      val update_subterms :
        Congruence.TERM.t -> Congruence.TERM.t list -> Congruence.TERM.t
    end
  module Make :
    functor (T : TERM) ->
      sig
        type term = T.t
        type t
        val create : ?size:int -> unit -> t
        val clear : t -> unit
        val push : t -> unit
        val pop : t -> unit
        val stack_size : t -> int
        val find : t -> term -> term
        val iter : t -> (mem:term -> repr:term -> unit) -> unit
        val iter_roots : t -> (term -> unit) -> unit
        val mk_eq : t -> term -> term -> unit
        val mk_less : t -> term -> term -> unit
        val is_eq : t -> term -> term -> bool
        val is_less : t -> term -> term -> bool
        val cycles : t -> bool
      end
  module FO :
    sig
      type term = FOTerm.t
      type t
      val create : ?size:int -> unit -> t
      val clear : t -> unit
      val push : t -> unit
      val pop : t -> unit
      val stack_size : t -> int
      val find : t -> term -> term
      val iter : t -> (mem:term -> repr:term -> unit) -> unit
      val iter_roots : t -> (term -> unit) -> unit
      val mk_eq : t -> term -> term -> unit
      val mk_less : t -> term -> term -> unit
      val is_eq : t -> term -> term -> bool
      val is_less : t -> term -> term -> bool
      val cycles : t -> bool
    end
end