Previous  Up  

Module Congruence.FO

module FO: S  with type term = FOTerm.t
type term 
type t
Represents a congruence
val create : ?size:int -> unit -> t
New congruence.
size : a hint for the initial size of the hashtable.
val clear : t -> unit
Clear the content of the congruence. It is now equivalent to the empty congruence.
val push : t -> unit
Push a checkpoint on the stack of the congruence. An equivalent call to Congruence.S.pop will restore the congruence to its current state.
val pop : t -> unit
Restore to the previous checkpoint.
Raises Invalid_argument if there is no checkpoint to restore to (ie if no call to Congruence.S.push matches this call to Congruence.S.pop)
val stack_size : t -> int
Number of calls to Congruence.S.push that lead to the current state of the congruence. Also, how many times Congruence.S.pop can be called.
val find : t -> term -> term
Current representative of this term
val iter : t ->
       (mem:term -> repr:term -> unit) -> unit
Iterate 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.

val iter_roots : t -> (term -> unit) -> unit
Iterate on the congruence classes' representative elements. Exactly one term per congruence class will be passed to the function.
val mk_eq : t -> term -> term -> unit
mk_eq congruence t1 t2 asserts that t1 = t2 belongs to the congruence
val mk_less : t -> term -> term -> unit
mk_less congruence t1 t2 asserts that t1 < t2 belongs to the congruence
val is_eq : t -> term -> term -> bool
Returns true if the two terms are equal in the congruence. This updates the congruence, because the two terms need to be added.
val is_less : t -> term -> term -> bool
Returns true if the first term is strictly lower than the second one in the congruence
val cycles : t -> bool
Checks whether there are cycles in inequalities.
Returns true if calls to mk_eq and mk_less entail a cycle in the ordering (hence contradicting irreflexivity/transitivity of less)