Make (alt-ergo-lib.AltErgoLib.Matching.Make)

Parameters

module X : Arg

type t

type theory = X.t

val empty : t

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

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

val max_term_depth : t -> int -> t

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

val query : 
  use_ematching:bool ->
  t ->
  Triggers.t ->
  theory ->
  (Matching_types.trigger_info * Matching_types.gsubst list) list

val reinit_caches : unit -> unit

Empties the e-matching caches