colibri2 0.4 (latest) · OCaml Package

Low level API

module Dem : Colibri2_stdlib.Keys.Key

Key with arity 1

type delay =

| Immediate
| Delayed_by of int
(*
Must be strictly positive
*)
| LastEffort of int
(*
After no propagation and decisions remains to be done
*)
| LastEffortUncontextual of int
(*
Same as before but could be moved as propagation before the time it is added
*)
| FixingModel

type enqueue =

| EnqRun : 'r Dem.t * 'r * ThTerm.t option -> enqueue
(*
Schedule a daemon run
*)
| EnqLast : 'r Dem.t * 'r * ThTerm.t option -> enqueue
(*
Same as EnqRun but remove the waiting event
*)
| EnqAlready : enqueue
(*
Don't run but keep the waiting event
*)
| EnqStopped : enqueue
(*
Stop and don't run
*)

type daemon_key =

val pp_daemon_key : daemon_key Fmt.t

module type T = sig ... end

val register : (module T) -> unit

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

package colibri2