sig
  type term = Reasoner.term
  type ty = Reasoner.ty
  class type core =
    object
      method owns : Plugin.term -> bool
      method signature : Plugin.ty Libzipperposition.ID.Map.t
    end
  class type ['a] t =
    object
      method clauses : Reasoner.clause list
      method of_fact : Plugin.term -> 'a option
      method owns : term -> bool
      method signature : ty Libzipperposition.ID.Map.t
      method to_fact : 'a -> Plugin.term
    end
  type foclause = Encoding.foclause
  module Set :
    sig
      type t
      val empty : Plugin.Set.t
      val add : Plugin.Set.t -> Plugin.core -> Plugin.Set.t
      val signature : Plugin.Set.t -> Plugin.ty Libzipperposition.ID.Map.t
    end
  val holds : Plugin.foclause Plugin.t
  val axiom : (Libzipperposition.ID.t * Plugin.term list) Plugin.t
  val theory : (Libzipperposition.ID.t * Plugin.term list) Plugin.t
  val lemma : Plugin.foclause Plugin.t
  val pre_rewrite : (Plugin.term * Plugin.term) list Plugin.t
  val rewrite :
    (Libzipperposition.FOTerm.t * Libzipperposition.FOTerm.t) list Plugin.t
  module Base :
    sig
      val set : Plugin.Set.t
      val signature : Plugin.ty Libzipperposition.ID.Map.t
    end
  val facts : Reasoner.t -> 'a Plugin.t -> 'a Sequence.t
  val of_consequence : Reasoner.consequence -> 'a Plugin.t -> 'a option
  val of_consequences :
    Reasoner.consequence Sequence.t -> 'a Plugin.t -> 'a Sequence.t
end