sig
  module Type :
    functor (X : Sig.X) ->
      sig
        type r = X.r
        type t
        val compare : t -> t -> int
        val hash : t -> int
        val create : (Num.num * r) list -> Num.num -> Ty.t -> t
        val add : t -> t -> t
        val sub : t -> t -> t
        val mult : t -> t -> t
        val mult_const : Num.num -> t -> t
        val div : t -> t -> t * bool
        val modulo : t -> t -> t
        val is_empty : t -> bool
        val find : r -> t -> Num.num
        val choose : t -> Num.num * r
        val subst : r -> t -> t -> t
        val remove : r -> t -> t
        val to_list : t -> (Num.num * r) list * Num.num
        val print : Format.formatter -> t -> unit
        val type_info : t -> Ty.t
        val is_monomial : t -> (Num.num * r * Num.num) option
        val ppmc_denominators : t -> Num.num
        val pgcd_numerators : t -> Num.num
        val normal_form : t -> t * Num.num * Num.num
        val normal_form_pos : t -> t * Num.num * Num.num
      end
  module Make :
    functor
      (X : Sig.X) (P : sig
                         type r = X.r
                         type t
                         val compare : t -> t -> int
                         val hash : t -> int
                         val create :
                           (Num.num * r) list -> Num.num -> Ty.t -> t
                         val add : t -> t -> t
                         val sub : t -> t -> t
                         val mult : t -> t -> t
                         val mult_const : Num.num -> t -> t
                         val div : t -> t -> t * bool
                         val modulo : t -> t -> t
                         val is_empty : t -> bool
                         val find : r -> t -> Num.num
                         val choose : t -> Num.num * r
                         val subst : r -> t -> t -> t
                         val remove : r -> t -> t
                         val to_list : t -> (Num.num * r) list * Num.num
                         val print : Format.formatter -> t -> unit
                         val type_info : t -> Ty.t
                         val is_monomial :
                           t -> (Num.num * r * Num.num) option
                         val ppmc_denominators : t -> Num.num
                         val pgcd_numerators : t -> Num.num
                         val normal_form : t -> t * Num.num * Num.num
                         val normal_form_pos : t -> t * Num.num * Num.num
                       end) (C : sig
                                   type t = P.t
                                   type r = X.r
                                   val extract : r -> t option
                                   val embed : t -> r
                                 end) ->
      sig
        type t = P.t
        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