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