package colibri2

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type t

A scope for decision, allows to wait before adding decisions for terms. Used for propagating into a term without decisions

val create : _ Egraph.t -> t

Create a new group

val activate : _ Egraph.t -> t -> unit

val add_to_group : _ Egraph.t -> ThTerm.t -> t -> unit

Add a ThTerm.t to a group

val make_choosable : _ Egraph.t -> ThTerm.t -> unit

Register the decisions attached to the node, and will not delay them in the future

val add_to_group_of : _ Egraph.t -> ThTerm.t -> ThTerm.t -> unit

add_to_group_of d t1 t2 add t1 in the group of t2