Core types and algorithms for logic
Module Logtk . Congruence . Make


module T : TERM


type term = T.t
type t

Represents a congruence

val create : ?size:int -> unit -> t

New congruence.

  • parameter size

    a hint for the initial size of the hashtable.

val iter : t -> ( mem:term -> repr:term -> unit ) -> unit

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.

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 add : t -> term -> t

Add the term to the congruence closure

val mk_eq : t -> term -> term -> t

mk_eq 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 pp_debug : t CCFormat.printer