Make (p.alt-ergo-lib.2.4.0.doc.alt-ergo-lib.AltErgoLib.Matching.Make)

Parameters

module X : Arg

Signature

Sourcetype t

Sourcetype theory = X.t

Sourceval empty : t

val make : 
  max_t_depth:int ->
  Matching_types.info Expr.Map.t ->
  Expr.t list Expr.Map.t Symbols.Map.t ->
  Matching_types.trigger_info list ->
  t

Sourceval add_term : Matching_types.term_info -> Expr.t -> t -> t

Sourceval max_term_depth : t -> int -> t

Source

val add_triggers : 
  Util.matching_env ->
  t ->
  (Expr.t * int * Explanation.t) Expr.Map.t ->
  t

Source

val terms_info : 
  t ->
  Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t

Source

val query : 
  Util.matching_env ->
  t ->
  theory ->
  (Matching_types.trigger_info * Matching_types.gsubst list) list