package colibri2

  1. Overview
  2. Docs

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.