sig
  type t
  type r
  val name : string
  val is_mine_symb : Symbols.t -> bool
  val unsolvable : Sig.THEORY.t -> bool
  val make : Term.t -> Sig.THEORY.r * Literal.LT.t list
  val term_extract : Sig.THEORY.r -> Term.t option
  val type_info : Sig.THEORY.t -> Ty.t
  val embed : Sig.THEORY.r -> Sig.THEORY.t
  val leaves : Sig.THEORY.t -> Sig.THEORY.r list
  val subst : Sig.THEORY.r -> Sig.THEORY.r -> Sig.THEORY.t -> Sig.THEORY.r
  val compare : Sig.THEORY.t -> Sig.THEORY.t -> int
  val hash : Sig.THEORY.t -> int
  val solve :
    Sig.THEORY.r -> Sig.THEORY.r -> (Sig.THEORY.r * Sig.THEORY.r) list
  val print : Format.formatter -> Sig.THEORY.t -> unit
  val fully_interpreted : Symbols.t -> bool
  module Rel :
    sig
      type t
      type r = r
      val empty : unit -> t
      val assume : t -> r input list -> t * r result
      val query : t -> r input -> answer
      val case_split : t -> (r Literal.view * Explanation.t * Num.num) list
      val add : t -> r -> t
    end
end