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