sig
  val cmd_line :
    TermLib.logic -> bool -> bool -> bool -> bool -> string array
  val check_sat_limited_cmd : int -> string
  val check_sat_assuming_supported : unit -> bool
  val check_sat_assuming_cmd : unit -> string
  val headers : unit -> string list
  val prelude : string list
  val trace_extension : string
  val comment_delims : string * string
  val interpr_type : Type.t -> Type.t
  val pp_print_sort : Format.formatter -> Type.t -> unit
  val string_of_sort : Type.t -> string
  val string_of_logic : TermLib.logic -> string
  val pp_print_logic : Format.formatter -> TermLib.logic -> unit
  val pp_print_symbol : ?arity:int -> Format.formatter -> Symbol.t -> unit
  val string_of_symbol : ?arity:int -> Symbol.t -> string
  val pp_print_expr : Format.formatter -> Term.t -> unit
  val print_expr : Term.t -> unit
  val string_of_expr : Term.t -> string
  val s_define_fun : HString.t
  val expr_of_string_sexpr : HStringSExpr.t -> Term.t
  val expr_or_lambda_of_string_sexpr :
    HStringSExpr.t -> HString.t * Model.value
end