Module BitwuzlaDriver

include module type of struct include GenericSMTLIBDriver end
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 = GenericSMTLIBDriver.expr_of_string_sexpr_conv = {
  1. s_let : HString.t;
  2. s_forall : HString.t;
  3. s_exists : HString.t;
  4. s_div : HString.t;
  5. s_minus : HString.t;
  6. s_index : HString.t;
  7. s_as : HString.t;
  8. s_int_to_bv : HString.t;
  9. s_extract : HString.t;
  10. s_signext : HString.t;
  11. s_zeroext : HString.t;
  12. prime_symbol : HString.t option;
  13. s_define_fun : HString.t;
  14. s_declare_fun : HString.t;
  15. const_of_atom : (HString.t * Var.t) list -> HString.t -> Term.t;
  16. symbol_of_atom : HString.t -> Symbol.t;
  17. type_of_sexpr : HStringSExpr.t -> Type.t;
  18. expr_of_string_sexpr : expr_of_string_sexpr_conv -> (HString.t * Var.t) list -> HStringSExpr.t -> Term.t;
  19. 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 normalize_abstract_const_name : string -> HString.t -> HString.t
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 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 : (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 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 s_define_fun : HString.t
val cmd_line : 'a -> int -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> string array
val check_sat_limited_cmd : 'a -> 'b
val string_of_logic : TermLib.logic -> string
val pp_print_logic : Stdlib.Format.formatter -> TermLib.logic -> unit