Module Yices2SMT2Driver

include GenericSMTLIBDriver
val cmd_line : 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h array
val check_sat_limited_cmd : 'a -> 'b
val check_sat_assuming_cmd : 'a -> string
val check_sat_assuming_supported : unit -> bool
val headers : 'a -> 'b 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 : Stdlib.Format.formatter -> TermLib.logic -> unit
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 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 -> Stdlib.Format.formatter -> Symbol.symbol -> unit
val pp_print_symbol : ?⁠arity:'a -> Stdlib.Format.formatter -> Symbol.t -> unit
val string_of_symbol : ?⁠arity:'a -> Symbol.t -> string
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
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
val cmd_line : [> `Inferred of TermLib.FeatureSet.t ] -> int -> 'a -> 'b -> 'c -> 'd -> 'e -> string array
val check_sat_limited_cmd : 'a -> 'b