sig
  type sort = Type.t
  type t = Term.t
  type var = Var.t
  type custom_arg = ArgString of string | ArgExpr of SMTExpr.t
  module type Conv =
    sig
      val smtsort_of_type : Type.t -> SMTExpr.sort
      val smtexpr_of_var : Var.t -> Term.t list -> SMTExpr.t
      val string_of_logic : TermLib.logic -> string
      val pp_print_logic : Format.formatter -> TermLib.logic -> unit
      val pp_print_sort : Format.formatter -> SMTExpr.sort -> unit
      val string_of_sort : SMTExpr.sort -> string
      val pp_print_expr : Format.formatter -> SMTExpr.t -> unit
      val print_expr : SMTExpr.t -> unit
      val string_of_expr : SMTExpr.t -> string
      val smtexpr_of_term : SMTExpr.t -> SMTExpr.t
      val quantified_smtexpr_of_term :
        bool -> Var.t list -> SMTExpr.t -> SMTExpr.t
      val var_term_of_smtexpr : SMTExpr.t -> SMTExpr.t
      val term_of_smtexpr : SMTExpr.t -> SMTExpr.t
      val pp_print_custom_arg :
        Format.formatter -> SMTExpr.custom_arg -> unit
      val string_of_custom_arg : SMTExpr.custom_arg -> string
    end
  module Converter : functor (D : SolverDriver.S-> Conv
end