package colibri2

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Package contains no libraries

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

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 context : _ t -> Colibri2_stdlib.Context.creator

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

exception Contradiction

exception NotRegistered