package colibri2

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Attach a callback executed when different modifications of the Egraph happens

Same as Daemon but they are scheduled to run as soon as possible during the FixingModel phase

val attach_dom : _ Egraph.t -> ?thterm:ThTerm.t -> ?direct:bool -> Node.t -> 'a Dom.Kind.t -> (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) -> unit

attach_dom d ?direct n dom callback The callback is

val attach_any_dom : _ Egraph.t -> ?thterm:ThTerm.t -> 'a Dom.Kind.t -> (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) -> unit
val attach_value : _ Egraph.t -> ?thterm:ThTerm.t -> ?direct:bool -> Node.t -> ('a, 'b) Value.Kind.t -> (Egraph.rt -> Node.t -> 'b -> (Egraph.wt -> unit) option) -> unit
val attach_any_value : _ Egraph.t -> ?thterm:ThTerm.t -> ?direct:bool -> Node.t -> (Egraph.rt -> Node.t -> Value.t -> (Egraph.wt -> unit) option) -> unit
val attach_reg_any : _ Egraph.t -> ?thterm:ThTerm.t -> (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) -> unit
val attach_reg_node : _ Egraph.t -> ?thterm:ThTerm.t -> Node.t -> (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) -> unit
val attach_reg_sem : _ Egraph.t -> ?thterm:ThTerm.t -> ('a, 'b) ThTerm.Kind.t -> (Egraph.rt -> 'b -> (Egraph.wt -> unit) option) -> unit
val attach_reg_value : _ Egraph.t -> ?thterm:ThTerm.t -> ('a, 'b) Value.Kind.t -> (Egraph.rt -> 'b -> (Egraph.wt -> unit) option) -> unit
val attach_repr : _ Egraph.t -> ?thterm:ThTerm.t -> Node.t -> (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) -> unit
val attach_any_repr : _ Egraph.t -> ?thterm:ThTerm.t -> (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) -> unit
OCaml

Innovation. Community. Security.