package colibri2

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

Trigger

type inst_step =
  1. | NotSeen
  2. | Delayed
  3. | Instantiated
type t = private {
  1. id : int;
  2. pat : Pattern.t;
    (*

    The pattern on which to wait for a substitution

    *)
  3. pats : Pattern.t list;
    (*

    The other ones used to obtain a complete substitution

    *)
  4. checks : Pattern.t list;
    (*

    Guards for the existence of terms

    *)
  5. form : Colibri2_core.Ground.ClosedQuantifier.t;
    (*

    the body of the formula

    *)
  6. eager : bool;
    (*

    If it should be eagerly applied, otherwise wait for LastEffort

    *)
  7. substs : inst_step SubstTrie.t;
}
include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
include Colibri2_popop_lib.Popop_stdlib.OrderedHashedType with type t := t
val equal : t -> t -> bool
val hash_fold_t : t Base.Hash.folder
module S : Colibri2_popop_lib.Map_intf.Set with type 'a M.t = 'a M.t and type M.key = M.key
include Base.Hashtbl.Key.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
val sexp_of_t : t -> Sexplib0.Sexp.t
val hash : t -> int
val compute_top_triggers : _ Colibri2_core.Egraph.t -> Colibri2_core.Ground.ClosedQuantifier.t -> t list

Compute triggers, that should only add logical connective or equalities are new terms

val compute_all_triggers : _ Colibri2_core.Egraph.t -> Colibri2_core.Ground.ClosedQuantifier.t -> t list

Compute all the triggers whose patterns contain all the variables of the formula

return the triggers given by the user

type tri_callback =
  1. | Trigger of t
  2. | Callback of Callback.t
val pp_tri_callback : Ppx_deriving_runtime.Format.formatter -> tri_callback -> Ppx_deriving_runtime.unit
val show_tri_callback : tri_callback -> Ppx_deriving_runtime.string

Triggers that are only variables

Triggers sorted by their top symbol

val add_trigger : Colibri2_core.Egraph.wt -> t -> unit

Register a new trigger

val add_callback : Colibri2_core.Egraph.wt -> Callback.t -> unit

Register a new trigger

instantiate d tri subst instantiates the trigger tri with the substitution subst:

* now if the trigger is eager and the checks of the trigger exists when substituted by subst

* at last effort otherwise

val instantiate_many : Colibri2_core.Egraph.wt -> t -> Colibri2_core.Ground.Subst.S.t -> unit
val match_ : Colibri2_core.Egraph.wt -> t -> Colibri2_core.Node.t -> unit

match_ d tri n match the pattern of tri with n and instantiate tri with the resulting substitutions

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