Module Z3Driver

include module type of struct include GenericSMTLIBDriver end
val check_sat_assuming_cmd : 'a -> string
val check_sat_assuming_supported : unit -> bool
val prelude : 'a list
val trace_extension : string
val comment_delims : string * string
val bool_of_hstring : HString.t -> bool
val s_let : HString.t
val s_forall : HString.t
val s_exists : HString.t
val s_div : HString.t
val s_minus : HString.t
val s_index : HString.t
val s_as : HString.t
val s_const : HString.t
val s_int_to_bv : HString.t
val s_extract : HString.t
val s_signext : HString.t
val s_zeroext : HString.t
val s_define_fun : HString.t
val s_declare_fun : HString.t
type expr_of_string_sexpr_conv = GenericSMTLIBDriver.expr_of_string_sexpr_conv = {
  1. prime_symbol : HString.t option;
  2. const_of_atom : Var.t HSM.t -> HString.t -> Term.t;
  3. symbol_of_atom : HString.t -> Symbol.t;
  4. type_of_sexpr : HStringSExpr.t -> Type.t;
  5. expr_of_string_sexpr : expr_of_string_sexpr_conv -> Var.t HSM.t -> HStringSExpr.t -> Term.t;
  6. expr_or_lambda_of_string_sexpr : expr_of_string_sexpr_conv -> Var.t HSM.t -> HStringSExpr.t -> HString.t * Model.value;
}
val free_atoms : HSS.t -> HSS.t -> HStringSExpr.t -> HSS.t
val gen_bound_vars_of_string_sexpr : expr_of_string_sexpr_conv -> 'a -> Var.t list -> HStringSExpr.t list -> Var.t list
val normalize_abstract_const_name : string -> HString.t -> HString.t
val gen_expr_of_string_sexpr' : expr_of_string_sexpr_conv -> Var.t HSM.t -> HStringSExpr.t -> Term.t
val gen_expr_or_lambda_of_string_sexpr' : expr_of_string_sexpr_conv -> Var.t HSM.t -> 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 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:??? -> Stdlib.Format.formatter -> Symbol.symbol -> unit
val pp_print_symbol : ?arity:??? -> Stdlib.Format.formatter -> Symbol.t -> unit
val string_of_symbol : ?arity:??? -> 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 : Var.t HSM.t -> HSM.key -> Term.t
val s_int : HString.t
val s_real : HString.t
val s_bool : HString.t
val s_array : unit -> HString.t
val s_bitvector : 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 cmd_line : 'a -> int -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> string array
val check_sat_limited_cmd : int -> string
val headers : bool -> string list
val string_of_logic : TermLib.logic -> string
val pp_print_logic : Stdlib.Format.formatter -> TermLib.logic -> unit