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 set_arith_active : bool -> unit
  val set_sum_active : bool -> unit
end