Module Instances.Make

Parameters

module X : Theory.S

Signature

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 -> t -> tbox -> (Expr.t -> Expr.t -> bool) -> int -> instances * instances
val m_predicates : Util.matching_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