package logtk
-
logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
val create : ?size:int -> unit -> tNew congruence.
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 -> unitRestore to the previous checkpoint.
val 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.