package colibri2

  1. Overview
  2. Docs
type t

Normalizable terms

val name : string
include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
include Colibri2_popop_lib.Popop_stdlib.OrderedHashedType with type t := t
val equal : t -> t -> bool
val hash_fold_t : t Base.Hash.folder
module S : Colibri2_popop_lib.Map_intf.Set with type 'a M.t = 'a M.t and type M.key = M.key
include Base.Hashtbl.Key.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
val sexp_of_t : t -> Sexplib0.Sexp.t
val hash : t -> int
val of_one_node : Colibri2_core.Node.t -> t

Build a value that represent one node

val is_one_node : t -> Colibri2_core.Node.t option

Test if a value represents one node

val subst : t -> Colibri2_core.Node.t -> t -> t

subst p n q return the result of the substitution of n by q in p

val normalize : t -> f:(Colibri2_core.Node.t -> t) -> t

norm p ~f normalize p using f

type data

An abstract type to avoid translating the map to sets in nodes

nodes t returns the node which are present in t

val solve : t -> t -> t solve_total

solve t1 t2 solve the equation t1 = t2 by returning a substitution.

val set : Colibri2_core.Egraph.wt -> Colibri2_core.Node.t -> old_:t option -> new_:t -> unit

Called a new term equal to this node is found

OCaml

Innovation. Community. Security.