sig
  type t = Sym.sym * int
  and sym =
      Uninterp of Sym.uninterp
    | Arith of Sym.arith
    | Product of Sym.product
    | Coproduct of Sym.coproduct
    | Bv of Sym.bv
    | Pp of Sym.pprod
    | Cl of Sym.cl
    | Arrays of Sym.arrays
    | Propset of Sym.propset
  and uninterp = Name.t
  and arith = Num of Mpa.Q.t | Add | Multq of Mpa.Q.t
  and product = Cons | Car | Cdr
  and coproduct = In of Sym.direction | Out of Sym.direction
  and direction = Left | Right
  and arrays = Create | Select | Update
  and cl = Apply | S | K | I | C | Reify of Sym.t * int
  and propset = Empty | Full | Ite
  and bv = Const of Bitv.t | Conc of int * int | Sub of int * int * int
  and pprod = Mult
  and tsym = Sym.t
  val theory_of : Sym.t -> Th.t
  val eq : Sym.t -> Sym.t -> bool
  val cmp : Sym.t -> Sym.t -> int
  val hash : Sym.t -> int
  val pp : 'a Pretty.printer -> (Sym.t * 'a list) Pretty.printer
  module Uninterp :
    sig
      val get : Sym.t -> Sym.uninterp
      val make : Name.t -> Sym.t
      val is : Sym.t -> bool
      val pp : 'a Pretty.printer -> (Sym.uninterp * 'a list) Pretty.printer
    end
  module Arith :
    sig
      val mk_num : Mpa.Q.t -> Sym.t
      val mk_multq : Mpa.Q.t -> Sym.t
      val mk_add : Sym.t
      val get : Sym.t -> Sym.arith
      val is_num : Sym.t -> bool
      val is_multq : Sym.t -> bool
      val is_add : Sym.t -> bool
      val d_num : Sym.t -> Mpa.Q.t
      val d_multq : Sym.t -> Mpa.Q.t
      val pp : 'a Pretty.printer -> (Sym.arith * 'a list) Pretty.printer
    end
  module Product :
    sig
      val mk_cons : Sym.t
      val mk_car : Sym.t
      val mk_cdr : Sym.t
      val get : Sym.t -> Sym.product
      val is_cons : Sym.t -> bool
      val is_car : Sym.t -> bool
      val is_cdr : Sym.t -> bool
      val pp : 'a Pretty.printer -> (Sym.product * 'a list) Pretty.printer
    end
  module Coproduct :
    sig
      val mk_inl : Sym.t
      val mk_inr : Sym.t
      val mk_outl : Sym.t
      val mk_outr : Sym.t
      val get : Sym.t -> Sym.coproduct
      val is : Sym.t -> bool
      val is_inl : Sym.t -> bool
      val is_inr : Sym.t -> bool
      val is_outl : Sym.t -> bool
      val is_outr : Sym.t -> bool
      val pp : 'a Pretty.printer -> (Sym.coproduct * 'a list) Pretty.printer
    end
  module Pprod :
    sig
      val mk_mult : Sym.t
      val get : Sym.t -> Sym.pprod
      val is : Sym.t -> bool
      val is_mult : Sym.t -> bool
      val pp : 'a Pretty.printer -> (Sym.pprod * 'a list) Pretty.printer
    end
  module Bv :
    sig
      val get : Sym.t -> Sym.bv
      val mk_const : Bitv.t -> Sym.t
      val mk_conc : int -> int -> Sym.t
      val mk_sub : int -> int -> int -> Sym.t
      val is : Sym.t -> bool
      val is_const : Sym.t -> bool
      val is_conc : Sym.t -> bool
      val is_sub : Sym.t -> bool
      val d_const : Sym.t -> Bitv.t
      val d_conc : Sym.t -> int * int
      val d_sub : Sym.t -> int * int * int
      val width : Sym.bv -> int
      val pp : 'a Pretty.printer -> (Sym.bv * 'a list) Pretty.printer
    end
  module Array :
    sig
      val get : Sym.t -> Sym.arrays
      val mk_create : Sym.t
      val mk_select : Sym.t
      val mk_update : Sym.t
      val is : Sym.t -> bool
      val is_create : Sym.t -> bool
      val is_select : Sym.t -> bool
      val is_update : Sym.t -> bool
      val pp : 'a Pretty.printer -> (Sym.arrays * 'a list) Pretty.printer
    end
  module Cl :
    sig
      val get : Sym.t -> Sym.cl
      val apply : Sym.t
      val s : Sym.t
      val k : Sym.t
      val i : Sym.t
      val c : Sym.t
      val reify : Sym.tsym * int -> Sym.t
      val is : Sym.t -> bool
      val is_apply : Sym.t -> bool
      val is_s : Sym.t -> bool
      val is_k : Sym.t -> bool
      val is_i : Sym.t -> bool
      val is_c : Sym.t -> bool
      val is_reify : Sym.t -> bool
      val d_reify : Sym.t -> Sym.tsym * int
      val pp : 'a Pretty.printer -> (Sym.cl * 'a list) Pretty.printer
    end
  module Propset :
    sig
      val get : Sym.t -> Sym.propset
      val mk_empty : Sym.t
      val mk_full : Sym.t
      val mk_ite : Sym.t
      val is : Sym.t -> bool
      val is_empty : Sym.t -> bool
      val is_full : Sym.t -> bool
      val is_ite : Sym.t -> bool
      val pp : 'a Pretty.printer -> (Sym.propset * 'a list) Pretty.printer
    end
  val get : Sym.t -> Sym.sym
end