type term = T.tval create : ?size:int -> unit -> tNew congruence.
a hint for the initial size of the hashtable.
val clear : t -> unitClear the content of the congruence. It is now equivalent to the empty congruence.
val push : t -> unitPush a checkpoint on the stack of the congruence. An equivalent call to pop will restore the congruence to its current state.
val pop : t -> unitval stack_size : t -> intIterate on terms that are explicitely 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
mk_less 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.
Returns true if the first term is strictly lower than the second one in the congruence
val cycles : t -> boolChecks whether there are cycles in inequalities.
true if calls to mk_eq and mk_less entail a cycle in the ordering (hence contradicting irreflexivity/transitivity of less)