package colibri2

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type choice_state =

| DecNo
| DecTodo of (Egraph.wt -> unit) list

and t = {

choice : Egraph.wt -> choice_state;
prio : int;
print_cho : string;

}

val register : _ Egraph.t -> Ground.t -> t -> unit

register a decision that would be scheduled later. The choose_decision of the Cho will be called at that time to know if the decision is still needed. The decision will not be scheduled if the ground term is part of a group not activated.If no group have been specified at that point, the default is for the decision to be directly activated

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

Same as register but for ThTerm.t

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

register a decision not attached to a ground term

module Group : sig ... end