sig
  module type S =
    sig
      type term
      type t
      val create : ?size:int -> unit -> LogtkCongruence.S.t
      val clear : LogtkCongruence.S.t -> unit
      val push : LogtkCongruence.S.t -> unit
      val pop : LogtkCongruence.S.t -> unit
      val stack_size : LogtkCongruence.S.t -> int
      val find :
        LogtkCongruence.S.t ->
        LogtkCongruence.S.term -> LogtkCongruence.S.term
      val iter :
        LogtkCongruence.S.t ->
        (mem:LogtkCongruence.S.term -> repr:LogtkCongruence.S.term -> unit) ->
        unit
      val iter_roots :
        LogtkCongruence.S.t -> (LogtkCongruence.S.term -> unit) -> unit
      val mk_eq :
        LogtkCongruence.S.t ->
        LogtkCongruence.S.term -> LogtkCongruence.S.term -> unit
      val mk_less :
        LogtkCongruence.S.t ->
        LogtkCongruence.S.term -> LogtkCongruence.S.term -> unit
      val is_eq :
        LogtkCongruence.S.t ->
        LogtkCongruence.S.term -> LogtkCongruence.S.term -> bool
      val is_less :
        LogtkCongruence.S.t ->
        LogtkCongruence.S.term -> LogtkCongruence.S.term -> bool
      val cycles : LogtkCongruence.S.t -> bool
    end
  module type TERM =
    sig
      type t
      val eq : LogtkCongruence.TERM.t -> LogtkCongruence.TERM.t -> bool
      val hash : LogtkCongruence.TERM.t -> int
      val subterms : LogtkCongruence.TERM.t -> LogtkCongruence.TERM.t list
      val update_subterms :
        LogtkCongruence.TERM.t ->
        LogtkCongruence.TERM.t list -> LogtkCongruence.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 = LogtkFOTerm.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 HO :
    sig
      type term = LogtkHOTerm.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