package logtk

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Congruence.FOSource

Sourcetype term = Term.t
Sourcetype t

Represents a congruence

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

New congruence.

  • parameter size

    a hint for the initial size of the hashtable.

Sourceval 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.

Sourceval 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.

Sourceval add : t -> term -> t

Add the term to the congruence closure

Sourceval mk_eq : t -> term -> term -> t

mk_eq congruence t1 t2 asserts that t1 = t2 belongs to the congruence

Sourceval 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.

Sourceval pp_debug : t CCFormat.printer
OCaml

Innovation. Community. Security.