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

Parameters

module X : Arg

Signature

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 ->
  Matching_types.trigger_info list ->
  t

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

val max_term_depth : t -> int -> t

val add_triggers : 
  Util.matching_env ->
  t ->
  (Expr.t * int * Explanation.t) AltErgoLib.Expr.Map.t ->
  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 : 
  Util.matching_env ->
  t ->
  theory ->
  (Matching_types.trigger_info * Matching_types.gsubst list) list

val reinit_caches : unit -> unit

Empties the e-matching caches