package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
type term = Term.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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct