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