colibri2 0.4 · OCaml Package

Trigger

type inst_step =

type t = private {

id : int;
pat : Pattern.t;
(*
The pattern on which to wait for a substitution
*)
pats : Pattern.t list;
(*
The other ones used to obtain a complete substitution
*)
checks : Pattern.t list;
(*
Guards for the existence of terms
*)
form : Colibri2_core.Ground.ClosedQuantifier.t;
(*
the body of the formula
*)
eager : bool;
(*
If it should be eagerly applied, otherwise wait for LastEffort
*)
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 pp : t Colibri2_popop_lib.Pp.pp

val hash_fold_t : t Base.Hash.folder

module M : Colibri2_popop_lib.Map_intf.PMap with type key = t

module S : 
  Colibri2_popop_lib.Map_intf.Set
    with type 'a M.t = 'a M.t
     and type M.key = M.key

module H : Colibri2_popop_lib.Exthtbl.Hashtbl.S with type key = t

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

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

return the triggers given by the user

type tri_callback =

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

val env_vars : tri_callback Colibri2_core.Datastructure.Push.t

Triggers that are only variables

val env_tri_by_apps : tri_callback Colibri2_stdlib.Context.Push.t F.EnvApps.t

Triggers sorted by their top symbol

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

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

val instantiate : 
  Colibri2_core.Egraph.wt ->
  t ->
  Colibri2_core.Ground.Subst.t ->
  unit

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

package colibri2