type term = Term.tval create : ?size:int -> unit -> tNew congruence.
a hint for the initial size of the hashtable.
Iterate on terms that are explicitly present in the congruence. The callback is given mem, the term itself, and repr, the current representative of the term mem.
Invariant: when calling iter cc f, if f ~mem ~repr is called, then find cc mem == repr holds.
Iterate on the congruence classes' representative elements. Exactly one term per congruence class will be passed to the function.
mk_eq congruence t1 t2 asserts that t1 = t2 belongs to the congruence
Returns true if the two terms are equal in the congruence. This updates the congruence, because the two terms need to be added.
val pp_debug : t CCFormat.printer