sig
  module CX :
    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
end