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

Parameters

module X : Theory.S

type t

type tbox = X.t

type instances = (Expr.gformula * Explanation.t) list

val empty : t

val add_terms : t -> AltErgoLib.Expr.Set.t -> Expr.gformula -> t

val add_lemma : t -> Expr.gformula -> Explanation.t -> t

val add_predicate : 
  t ->
  guard:Expr.t ->
  name:string ->
  Expr.gformula ->
  Explanation.t ->
  t

val ground_pred_defn : Expr.t -> t -> (Expr.t * Expr.t * Explanation.t) option

val pop : t -> guard:Expr.t -> t

val m_lemmas : 
  Util.matching_env ->
  Util.triggers_env ->
  t ->
  tbox ->
  (Expr.t -> Expr.t -> bool) ->
  int ->
  instances * instances

val m_predicates : 
  Util.matching_env ->
  Util.triggers_env ->
  t ->
  tbox ->
  (Expr.t -> Expr.t -> bool) ->
  int ->
  instances * instances

val register_max_term_depth : t -> int -> t

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

val reinit_em_cache : unit -> unit

Reinitializes the E-matching functor instance's inner cache