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