sig
  type answer = Yes of Explanation.t | No
  type 'a literal = LSem of 'a Literal.view | LTerm of Literal.LT.t
  type 'a input = 'a Literal.view * Literal.LT.t option * Explanation.t
  type 'a result = {
    assume : ('a Sig.literal * Explanation.t) list;
    remove : ('a Sig.literal * Explanation.t) list;
  }
  module type RELATION =
    sig
      type t
      type r
      val empty : unit -> Sig.RELATION.t
      val assume :
        Sig.RELATION.t ->
        Sig.RELATION.r Sig.input list ->
        Sig.RELATION.t * Sig.RELATION.r Sig.result
      val query : Sig.RELATION.t -> Sig.RELATION.r Sig.input -> Sig.answer
      val case_split :
        Sig.RELATION.t ->
        (Sig.RELATION.r Literal.view * Explanation.t * Num.num) list
      val add : Sig.RELATION.t -> Sig.RELATION.r -> Sig.RELATION.t
    end
  module type THEORY =
    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
  module type COMBINATOR =
    sig
      type r
      type th
      val extract : Sig.COMBINATOR.r -> Sig.COMBINATOR.th
      val make : Term.t -> Sig.COMBINATOR.r * Literal.LT.t list
      val type_info : Sig.COMBINATOR.r -> Ty.t
      val compare : Sig.COMBINATOR.r -> Sig.COMBINATOR.r -> int
      val leaves : Sig.COMBINATOR.r -> Sig.COMBINATOR.r list
      val subst :
        Sig.COMBINATOR.r ->
        Sig.COMBINATOR.r -> Sig.COMBINATOR.r -> Sig.COMBINATOR.r
      val solve :
        Sig.COMBINATOR.r ->
        Sig.COMBINATOR.r -> (Sig.COMBINATOR.r * Sig.COMBINATOR.r) list
      val empty_embedding : Term.t -> Sig.COMBINATOR.r
      val normal_form : Literal.LT.t -> Literal.LT.t
      val print : Format.formatter -> Sig.COMBINATOR.r -> unit
      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
  module type X =
    sig
      type r
      val make : Term.t -> Sig.X.r * Literal.LT.t list
      val type_info : Sig.X.r -> Ty.t
      val compare : Sig.X.r -> Sig.X.r -> int
      val equal : Sig.X.r -> Sig.X.r -> bool
      val hash : Sig.X.r -> int
      val leaves : Sig.X.r -> Sig.X.r list
      val subst : Sig.X.r -> Sig.X.r -> Sig.X.r -> Sig.X.r
      val solve : Sig.X.r -> Sig.X.r -> (Sig.X.r * Sig.X.r) list
      val term_embed : Term.t -> Sig.X.r
      val term_extract : Sig.X.r -> Term.t option
      val unsolvable : Sig.X.r -> bool
      val fully_interpreted : Symbols.t -> bool
      val print : Format.formatter -> Sig.X.r -> unit
      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
  module type C =
    sig
      type t
      type r
      val extract : Sig.C.r -> Sig.C.t option
      val embed : Sig.C.t -> Sig.C.r
    end
end