Module `YicesDriver`

val cmd_line : 'a -> int -> 'b -> 'c -> 'd -> 'e -> 'f -> string array
val check_sat_limited_cmd : 'a -> 'b
val check_sat_assuming_supported : unit -> bool
val check_sat_assuming_cmd : 'a -> 'b
val headers : 'a -> 'b list
val prelude : string list
val trace_extension : string
val comment_delims : string * string
val pp_print_type : Stdlib.Format.formatter -> Type.t -> unit
val pp_print_type_node : Stdlib.Format.formatter -> Type.kindtype -> unit
val pp_print_logic : 'a -> 'b -> 'c
val interpr_type : Type.t -> Type.t
val pp_print_sort : Stdlib.Format.formatter -> Type.t -> unit
val string_of_sort : Type.t -> string
val pp_print_sort : Stdlib.Format.formatter -> Type.t -> unit
val string_of_logic : 'a -> 'b
val s_int : HString.t
val s_real : HString.t
val s_bool : HString.t
val s_subrange : HString.t
val type_of_string_sexpr : HStringSExpr.t -> Type.t
val string_symbol_list : (string * Symbol.t) list
val reserved_word_list : HString.t list
val pp_print_symbol_node : ?⁠arity:int -> Stdlib.Format.formatter -> Symbol.symbol -> unit
val pp_print_symbol : ?⁠arity:int -> Stdlib.Format.formatter -> Symbol.t -> unit
val string_of_symbol : ?⁠arity:int -> Symbol.t -> string
val pp_print_typed_var_list : int -> Stdlib.Format.formatter -> Type.t list -> unit
val pp_print_term' : int -> Stdlib.Format.formatter -> Term.T.t -> unit
val pp_print_let_bindings : int -> int -> Stdlib.Format.formatter -> (Term.T.t list * Term.T.sort list) -> unit
val pp_print_term : Stdlib.Format.formatter -> Term.T.t -> unit
val pp_print_expr : Stdlib.Format.formatter -> Term.T.t -> unit
val print_expr : Term.T.t -> unit
val string_of_expr : Term.T.t -> string