Represents a congruence

New congruence.

• parameter size

  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.

Add the term to the congruence closure

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.