Module GenericSMTLIBDriver (.ml)

module GenericSMTLIBDriver: sig .. end

val cmd_line : 'a -> 'b -> 'c -> 'd -> 'e -> 'f array
val check_sat_limited_cmd : 'a -> 'b
val check_sat_assuming_cmd : 'a -> 'b
val check_sat_assuming_supported : unit -> 'a
val headers : unit -> 'a list
val prelude : 'a list
val trace_extension : string
val comment_delims : string * string
val bool_of_hstring : HString.t -> bool
type expr_of_string_sexpr_conv = {
   s_let : HString.t;
   s_forall : HString.t;
   s_exists : HString.t;
   s_div : HString.t;
   s_minus : HString.t;
   prime_symbol : HString.t option;
   s_define_fun : HString.t;
   s_declare_fun : HString.t;
   const_of_atom : (HString.t * Var.t) list -> HString.t -> Term.t;
   symbol_of_atom : HString.t -> Symbol.t;
   type_of_sexpr : HStringSExpr.t -> Type.t;
   expr_of_string_sexpr : expr_of_string_sexpr_conv ->
(HString.t * Var.t) list -> HStringSExpr.t -> Term.t
;
   expr_or_lambda_of_string_sexpr : expr_of_string_sexpr_conv ->
(HString.t * Var.t) list -> HStringSExpr.t -> HString.t * Model.value
;
}
val gen_bindings_of_string_sexpr : expr_of_string_sexpr_conv ->
(HString.t * Var.t) list ->
(Var.t * Term.t) list -> HStringSExpr.t list -> (Var.t * Term.t) list
val gen_bound_vars_of_string_sexpr : expr_of_string_sexpr_conv ->
'a -> Var.t list -> HStringSExpr.t list -> Var.t list
val gen_expr_of_string_sexpr' : expr_of_string_sexpr_conv ->
(HString.t * Var.t) list -> HStringSExpr.t -> Term.t
val gen_expr_or_lambda_of_string_sexpr' : expr_of_string_sexpr_conv ->
(HString.t * Var.t) list -> HStringSExpr.t -> HStringSExpr.atom * Model.value
val gen_expr_of_string_sexpr : expr_of_string_sexpr_conv -> HStringSExpr.t -> Term.t
val gen_expr_or_lambda_of_string_sexpr : expr_of_string_sexpr_conv ->
HStringSExpr.t -> HStringSExpr.atom * Model.value
val string_of_logic : TermLib.logic -> string
val pp_print_logic : Format.formatter -> TermLib.logic -> unit
val interpr_type : Type.t -> Type.t
val pp_print_sort : Format.formatter -> Type.t -> unit
val string_of_sort : Type.t -> string
val smtlib_string_symbol_list : (string * Symbol.t) list
val smtlib_reserved_word_list : HString.t list
val hstring_symbol_table : Symbol.t HString.HStringHashtbl.t
val pp_print_symbol_node : ?arity:'a -> Format.formatter -> Symbol.symbol -> unit
val pp_print_symbol : ?arity:'a -> Format.formatter -> Symbol.t -> unit
val string_of_symbol : ?arity:'a -> Symbol.t -> string
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
val is_select_hstring : HString.t -> bool
val symbol_of_smtlib_atom : HString.HStringHashtbl.key -> Symbol.t
val const_of_smtlib_atom : (HString.t * Var.t) list -> HString.t -> Term.t
val s_int : HString.t
val s_real : HString.t
val s_bool : HString.t
val s_array : unit -> HString.t
val type_of_smtlib_sexpr : HStringSExpr.t -> Type.t
val smtlib_string_sexpr_conv : expr_of_string_sexpr_conv
val expr_of_string_sexpr : HStringSExpr.t -> Term.t
val expr_or_lambda_of_string_sexpr : HStringSExpr.t -> HStringSExpr.atom * Model.value
val s_define_fun : HString.t