package colibri2

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

Low level API

Create daemons

Key with arity 1

Register daemons

type delay =
  1. | Immediate
  2. | Delayed_by of int
    (*

    Must be strictly positive

    *)
  3. | LastEffort of int
    (*

    After no propagation and decisions remains to be done

    *)
  4. | LastEffortUncontextual of int
    (*

    Same as before but could be moved as propagation before the time it is added

    *)
  5. | FixingModel
type enqueue =
  1. | EnqRun : 'r Dem.t * 'r * ThTerm.t option -> enqueue
    (*

    Schedule a daemon run

    *)
  2. | EnqLast : 'r Dem.t * 'r * ThTerm.t option -> enqueue
    (*

    Same as EnqRun but remove the waiting event

    *)
  3. | EnqAlready : enqueue
    (*

    Don't run but keep the waiting event

    *)
  4. | EnqStopped : enqueue
    (*

    Stop and don't run

    *)
type daemon_key =
  1. | DaemonKey : 'runable Dem.t * 'runable * ThTerm.t option -> daemon_key
val pp_daemon_key : daemon_key Fmt.t
module type T = sig ... end
val register : (module T) -> unit

Attach daemons

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

wakeup when the dom of the node change

val attach_any_dom : _ Egraph.t -> 'a Dom.Kind.t -> (Egraph.rt -> Node.t -> enqueue) -> unit

wakeup when the dom of any node change

val attach_value : _ Egraph.t -> ?direct:bool -> Node.t -> ('a, 'b) Value.Kind.t -> (Egraph.rt -> Node.t -> 'b -> enqueue) -> unit

wakeup when a value is attached to this equivalence class

val attach_any_value : _ Egraph.t -> ?direct:bool -> Node.t -> (Egraph.rt -> Node.t -> Value.t -> enqueue) -> unit

wakeup when any kind of value is attached to this equivalence class

val attach_reg_any : _ Egraph.t -> (Egraph.rt -> Node.t -> enqueue) -> unit

wakeup when any node is registered

val attach_reg_node : _ Egraph.t -> Node.t -> (Egraph.rt -> Node.t -> enqueue) -> unit

wakeup when this node is registered

val attach_reg_sem : _ Egraph.t -> ('a, 'b) ThTerm.Kind.t -> (Egraph.rt -> 'b -> enqueue) -> unit

wakeup when a new semantical class is registered

val attach_reg_value : _ Egraph.t -> ('a, 'b) Value.Kind.t -> (Egraph.rt -> 'b -> enqueue) -> unit

wakeup when a new value is registered

val attach_repr : _ Egraph.t -> Node.t -> (Egraph.rt -> Node.t -> enqueue) -> unit

wakeup when it is not anymore the representative class

val attach_any_repr : _ Egraph.t -> (Egraph.rt -> Node.t -> enqueue) -> unit

wakeup when a node is not its representative class anymore

val new_pending_daemon : _ Egraph.t -> ?thterm:ThTerm.t -> 'a Dem.t -> 'a -> unit

register an event for later (immediate or not).

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct