package colibri2

  1. Overview
  2. Docs
package colibri2
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'a t
type rw
type wt = rw t

Egraph where its structure can be modified

type ro
type rt = ro t

Egraph where its structure can not be modified

val is_equal : _ t -> Node.t -> Node.t -> bool

Tests if two nodes are equal

val find_def : _ t -> Node.t -> Node.t

find_def d n finds the representative of the equivalence class of n

val find : _ t -> Node.t -> Node.t
val is_repr : _ t -> Node.t -> bool
val get_dom : _ t -> 'a Dom.Kind.t -> Node.t -> 'a option

get_dom d dom n returns the domain dom of the node n if it is set

val get_value : _ t -> Node.t -> Value.t option

get_value d n returns the value of the node n if set

The classes must have been registered
val is_registered : _ t -> Node.t -> bool

is_registered n tests if n is registered

val get_env : _ t -> 'a Env.Saved.t -> 'a

Can raise UninitializedEnv

val set_env : _ t -> 'a Env.Saved.t -> 'a -> unit
val get_unsaved_env : _ t -> 'a Env.Unsaved.t -> 'a
val register : _ t -> Node.t -> unit

Add a new node to register

val set_dom : rw t -> 'a Dom.Kind.t -> Node.t -> 'a -> unit

Immediate modifications

change the dom of the equivalence class

val unset_dom : rw t -> 'a Dom.Kind.t -> Node.t -> unit

remove the dom of the equivalence class

val set_thterm : rw t -> Node.t -> ThTerm.t -> unit

Delayed modifications

attach a theory term to an equivalence class

val set_value : rw t -> Node.t -> Value.t -> unit

attach value to an equivalence class

val merge : rw t -> Node.t -> Node.t -> unit

merge n1 n2 Asks to merge the equivalence class of n1 and n2

val contradiction : _ t -> 'a

raises Contradiction

exception Contradiction
exception NotRegistered
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