Module YicesDriver (.ml)

module YicesDriver: sig .. end

val cmd_line : 'a -> 'b -> 'c -> 'd -> 'e -> 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 : unit -> 'a list
val prelude : string list
val trace_extension : string
val comment_delims : string * string
val pp_print_type : Format.formatter -> Type.t -> unit
val pp_print_type_node : Format.formatter -> Type.kindtype -> unit
val pp_print_logic : 'a -> 'b -> 'c
val interpr_type : Type.t -> Type.t
val pp_print_sort : Format.formatter -> Type.t -> unit
val string_of_sort : Type.t -> string
val pp_print_sort : 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 -> Format.formatter -> Symbol.symbol -> unit
val pp_print_symbol : ?arity:int -> Format.formatter -> Symbol.t -> unit
val string_of_symbol : ?arity:int -> Symbol.t -> string
val pp_print_typed_var_list : int -> Format.formatter -> Type.t list -> unit
val pp_print_term' : int -> Format.formatter -> Term.T.t -> unit
val pp_print_let_bindings : int -> int -> Format.formatter -> Term.T.t list * Term.T.sort list -> unit
val pp_print_term : Format.formatter -> Term.T.t -> unit
val pp_print_expr : Format.formatter -> Term.T.t -> unit
val print_expr : Term.T.t -> unit
val string_of_expr : Term.T.t -> string