z3.ml

(* File generated from z3.idl *)

type string_opt = string option
and symbol
and context
and ast
and sort = private ast
and func_decl = private ast
and app = private ast
and pattern = private ast
and model
and params
and param_descrs
and parser_context
and goal
and tactic
and simplifier
and probe
and stats
and solver
and ast_vector
and ast_map
and apply_result
and func_interp
and func_entry
and fixedpoint
and optimize
and rcf_num
and solver_callback
and symbol_opt = symbol option
and ast_opt = ast option
and model_opt = model option
and sort_opt = sort option
and func_interp_opt = func_interp option
and rcf_num_opt = rcf_num option
and config
and constructor
and constructor_list
and lbool =
  | L_FALSE
  | L_UNDEF
  | L_TRUE
and symbol_kind =
  | INT_SYMBOL
  | STRING_SYMBOL
and parameter_kind =
  | PARAMETER_INT
  | PARAMETER_DOUBLE
  | PARAMETER_RATIONAL
  | PARAMETER_SYMBOL
  | PARAMETER_SORT
  | PARAMETER_AST
  | PARAMETER_FUNC_DECL
  | PARAMETER_INTERNAL
  | PARAMETER_ZSTRING
and sort_kind =
  | UNINTERPRETED_SORT
  | BOOL_SORT
  | INT_SORT
  | REAL_SORT
  | BV_SORT
  | ARRAY_SORT
  | DATATYPE_SORT
  | RELATION_SORT
  | FINITE_DOMAIN_SORT
  | FLOATING_POINT_SORT
  | ROUNDING_MODE_SORT
  | SEQ_SORT
  | RE_SORT
  | CHAR_SORT
  | TYPE_VAR
  | UNKNOWN_SORT
and ast_kind =
  | NUMERAL_AST
  | APP_AST
  | VAR_AST
  | QUANTIFIER_AST
  | SORT_AST
  | FUNC_DECL_AST
  | UNKNOWN_AST
and decl_kind =
  | OP_TRUE
  | OP_FALSE
  | OP_EQ
  | OP_DISTINCT
  | OP_ITE
  | OP_AND
  | OP_OR
  | OP_IFF
  | OP_XOR
  | OP_NOT
  | OP_IMPLIES
  | OP_OEQ
  | OP_ANUM
  | OP_AGNUM
  | OP_LE
  | OP_GE
  | OP_LT
  | OP_GT
  | OP_ADD
  | OP_SUB
  | OP_UMINUS
  | OP_MUL
  | OP_DIV
  | OP_IDIV
  | OP_REM
  | OP_MOD
  | OP_TO_REAL
  | OP_TO_INT
  | OP_IS_INT
  | OP_POWER
  | OP_ABS
  | OP_STORE
  | OP_SELECT
  | OP_CONST_ARRAY
  | OP_ARRAY_MAP
  | OP_ARRAY_DEFAULT
  | OP_SET_UNION
  | OP_SET_INTERSECT
  | OP_SET_DIFFERENCE
  | OP_SET_COMPLEMENT
  | OP_SET_SUBSET
  | OP_AS_ARRAY
  | OP_ARRAY_EXT
  | OP_BNUM
  | OP_BIT1
  | OP_BIT0
  | OP_BNEG
  | OP_BADD
  | OP_BSUB
  | OP_BMUL
  | OP_BSDIV
  | OP_BUDIV
  | OP_BSREM
  | OP_BUREM
  | OP_BSMOD
  | OP_BSDIV0
  | OP_BUDIV0
  | OP_BSREM0
  | OP_BUREM0
  | OP_BSMOD0
  | OP_ULEQ
  | OP_SLEQ
  | OP_UGEQ
  | OP_SGEQ
  | OP_ULT
  | OP_SLT
  | OP_UGT
  | OP_SGT
  | OP_BAND
  | OP_BOR
  | OP_BNOT
  | OP_BXOR
  | OP_BNAND
  | OP_BNOR
  | OP_BXNOR
  | OP_CONCAT
  | OP_SIGN_EXT
  | OP_ZERO_EXT
  | OP_EXTRACT
  | OP_REPEAT
  | OP_BREDOR
  | OP_BREDAND
  | OP_BCOMP
  | OP_BSHL
  | OP_BLSHR
  | OP_BASHR
  | OP_ROTATE_LEFT
  | OP_ROTATE_RIGHT
  | OP_EXT_ROTATE_LEFT
  | OP_EXT_ROTATE_RIGHT
  | OP_BIT2BOOL
  | OP_INT2BV
  | OP_BV2INT
  | OP_SBV2INT
  | OP_CARRY
  | OP_XOR3
  | OP_BSMUL_NO_OVFL
  | OP_BUMUL_NO_OVFL
  | OP_BSMUL_NO_UDFL
  | OP_BSDIV_I
  | OP_BUDIV_I
  | OP_BSREM_I
  | OP_BUREM_I
  | OP_BSMOD_I
  | OP_PR_UNDEF
  | OP_PR_TRUE
  | OP_PR_ASSERTED
  | OP_PR_GOAL
  | OP_PR_MODUS_PONENS
  | OP_PR_REFLEXIVITY
  | OP_PR_SYMMETRY
  | OP_PR_TRANSITIVITY
  | OP_PR_TRANSITIVITY_STAR
  | OP_PR_MONOTONICITY
  | OP_PR_QUANT_INTRO
  | OP_PR_BIND
  | OP_PR_DISTRIBUTIVITY
  | OP_PR_AND_ELIM
  | OP_PR_NOT_OR_ELIM
  | OP_PR_REWRITE
  | OP_PR_REWRITE_STAR
  | OP_PR_PULL_QUANT
  | OP_PR_PUSH_QUANT
  | OP_PR_ELIM_UNUSED_VARS
  | OP_PR_DER
  | OP_PR_QUANT_INST
  | OP_PR_HYPOTHESIS
  | OP_PR_LEMMA
  | OP_PR_UNIT_RESOLUTION
  | OP_PR_IFF_TRUE
  | OP_PR_IFF_FALSE
  | OP_PR_COMMUTATIVITY
  | OP_PR_DEF_AXIOM
  | OP_PR_ASSUMPTION_ADD
  | OP_PR_LEMMA_ADD
  | OP_PR_REDUNDANT_DEL
  | OP_PR_CLAUSE_TRAIL
  | OP_PR_DEF_INTRO
  | OP_PR_APPLY_DEF
  | OP_PR_IFF_OEQ
  | OP_PR_NNF_POS
  | OP_PR_NNF_NEG
  | OP_PR_SKOLEMIZE
  | OP_PR_MODUS_PONENS_OEQ
  | OP_PR_TH_LEMMA
  | OP_PR_HYPER_RESOLVE
  | OP_RA_STORE
  | OP_RA_EMPTY
  | OP_RA_IS_EMPTY
  | OP_RA_JOIN
  | OP_RA_UNION
  | OP_RA_WIDEN
  | OP_RA_PROJECT
  | OP_RA_FILTER
  | OP_RA_NEGATION_FILTER
  | OP_RA_RENAME
  | OP_RA_COMPLEMENT
  | OP_RA_SELECT
  | OP_RA_CLONE
  | OP_FD_CONSTANT
  | OP_FD_LT
  | OP_SEQ_UNIT
  | OP_SEQ_EMPTY
  | OP_SEQ_CONCAT
  | OP_SEQ_PREFIX
  | OP_SEQ_SUFFIX
  | OP_SEQ_CONTAINS
  | OP_SEQ_EXTRACT
  | OP_SEQ_REPLACE
  | OP_SEQ_REPLACE_RE
  | OP_SEQ_REPLACE_RE_ALL
  | OP_SEQ_REPLACE_ALL
  | OP_SEQ_AT
  | OP_SEQ_NTH
  | OP_SEQ_LENGTH
  | OP_SEQ_INDEX
  | OP_SEQ_LAST_INDEX
  | OP_SEQ_TO_RE
  | OP_SEQ_IN_RE
  | OP_SEQ_MAP
  | OP_SEQ_MAPI
  | OP_SEQ_FOLDL
  | OP_SEQ_FOLDLI
  | OP_STR_TO_INT
  | OP_INT_TO_STR
  | OP_UBV_TO_STR
  | OP_SBV_TO_STR
  | OP_STR_TO_CODE
  | OP_STR_FROM_CODE
  | OP_STRING_LT
  | OP_STRING_LE
  | OP_RE_PLUS
  | OP_RE_STAR
  | OP_RE_OPTION
  | OP_RE_CONCAT
  | OP_RE_UNION
  | OP_RE_RANGE
  | OP_RE_DIFF
  | OP_RE_INTERSECT
  | OP_RE_LOOP
  | OP_RE_POWER
  | OP_RE_COMPLEMENT
  | OP_RE_EMPTY_SET
  | OP_RE_FULL_SET
  | OP_RE_FULL_CHAR_SET
  | OP_RE_OF_PRED
  | OP_RE_REVERSE
  | OP_RE_DERIVATIVE
  | OP_CHAR_CONST
  | OP_CHAR_LE
  | OP_CHAR_TO_INT
  | OP_CHAR_TO_BV
  | OP_CHAR_FROM_BV
  | OP_CHAR_IS_DIGIT
  | OP_LABEL
  | OP_LABEL_LIT
  | OP_DT_CONSTRUCTOR
  | OP_DT_RECOGNISER
  | OP_DT_IS
  | OP_DT_ACCESSOR
  | OP_DT_UPDATE_FIELD
  | OP_PB_AT_MOST
  | OP_PB_AT_LEAST
  | OP_PB_LE
  | OP_PB_GE
  | OP_PB_EQ
  | OP_SPECIAL_RELATION_LO
  | OP_SPECIAL_RELATION_PO
  | OP_SPECIAL_RELATION_PLO
  | OP_SPECIAL_RELATION_TO
  | OP_SPECIAL_RELATION_TC
  | OP_SPECIAL_RELATION_TRC
  | OP_FPA_RM_NEAREST_TIES_TO_EVEN
  | OP_FPA_RM_NEAREST_TIES_TO_AWAY
  | OP_FPA_RM_TOWARD_POSITIVE
  | OP_FPA_RM_TOWARD_NEGATIVE
  | OP_FPA_RM_TOWARD_ZERO
  | OP_FPA_NUM
  | OP_FPA_PLUS_INF
  | OP_FPA_MINUS_INF
  | OP_FPA_NAN
  | OP_FPA_PLUS_ZERO
  | OP_FPA_MINUS_ZERO
  | OP_FPA_ADD
  | OP_FPA_SUB
  | OP_FPA_NEG
  | OP_FPA_MUL
  | OP_FPA_DIV
  | OP_FPA_REM
  | OP_FPA_ABS
  | OP_FPA_MIN
  | OP_FPA_MAX
  | OP_FPA_FMA
  | OP_FPA_SQRT
  | OP_FPA_ROUND_TO_INTEGRAL
  | OP_FPA_EQ
  | OP_FPA_LT
  | OP_FPA_GT
  | OP_FPA_LE
  | OP_FPA_GE
  | OP_FPA_IS_NAN
  | OP_FPA_IS_INF
  | OP_FPA_IS_ZERO
  | OP_FPA_IS_NORMAL
  | OP_FPA_IS_SUBNORMAL
  | OP_FPA_IS_NEGATIVE
  | OP_FPA_IS_POSITIVE
  | OP_FPA_FP
  | OP_FPA_TO_FP
  | OP_FPA_TO_FP_UNSIGNED
  | OP_FPA_TO_UBV
  | OP_FPA_TO_SBV
  | OP_FPA_TO_REAL
  | OP_FPA_TO_IEEE_BV
  | OP_FPA_BVWRAP
  | OP_FPA_BV2RM
  | OP_INTERNAL
  | OP_RECURSIVE
  | OP_UNINTERPRETED
and param_kind =
  | PK_UINT
  | PK_BOOL
  | PK_DOUBLE
  | PK_SYMBOL
  | PK_STRING
  | PK_OTHER
  | PK_INVALID
and ast_print_mode =
  | PRINT_SMTLIB_FULL
  | PRINT_LOW_LEVEL
  | PRINT_SMTLIB2_COMPLIANT
and error_code =
  | OK
  | SORT_ERROR
  | IOB
  | INVALID_ARG
  | PARSER_ERROR
  | NO_PARSER
  | INVALID_PATTERN
  | MEMOUT_FAIL
  | FILE_ACCESS_ERROR
  | INTERNAL_FATAL
  | INVALID_USAGE
  | DEC_REF_ERROR
  | EXCEPTION
and goal_prec =
  | GOAL_PRECISE
  | GOAL_UNDER
  | GOAL_OVER
  | GOAL_UNDER_OVER


external ast_get_context : ast -> context = "get_context_z3_rc_val"
(** [ast_get_context a] is the [Z3.context] in which [a] was created. *)


external model_get_context : model -> context = "get_context_z3_rc_val"
(** [model_get_context m] is the [Z3.context] in which [m] was created. *)


external params_get_context : params -> context = "get_context_z3_rc_val"
(** [params_get_context p] is the [Z3.context] in which [p] was created. *)


external param_descrs_get_context : param_descrs -> context = "get_context_z3_rc_val"
(** [param_descrs_get_context p] is the [Z3.context] in which [p] was created. *)


external parser_context_get_context : parser_context -> context = "get_context_z3_rc_val"
(** [parser_context_get_context p] is the [Z3.context] in which [p] was created. *)


external goal_get_context : goal -> context = "get_context_z3_rc_val"
(** [goal_get_context g] is the [Z3.context] in which [g] was created. *)


external tactic_get_context : tactic -> context = "get_context_z3_rc_val"
(** [tactic_get_context t] is the [Z3.context] in which [t] was created. *)


external simplifier_get_context : simplifier -> context = "get_context_z3_rc_val"
(** [simplifier_get_context s] is the [Z3.context] in which [s] was created. *)


external probe_get_context : probe -> context = "get_context_z3_rc_val"
(** [probe_get_context p] is the [Z3.context] in which [p] was created. *)


external stats_get_context : stats -> context = "get_context_z3_rc_val"
(** [stats_get_context s] is the [Z3.context] in which [s] was created. *)


external solver_get_context : solver -> context = "get_context_z3_rc_val"
(** [solver_get_context s] is the [Z3.context] in which [s] was created. *)


external ast_vector_get_context : ast_vector -> context = "get_context_z3_rc_val"
(** [ast_vector_get_context a] is the [Z3.context] in which [a] was created. *)


external ast_map_get_context : ast_map -> context = "get_context_z3_rc_val"
(** [ast_map_get_context a] is the [Z3.context] in which [a] was created. *)


external apply_result_get_context : apply_result -> context = "get_context_z3_rc_val"
(** [apply_result_get_context a] is the [Z3.context] in which [a] was created. *)


external func_interp_get_context : func_interp -> context = "get_context_z3_rc_val"
(** [func_interp_get_context f] is the [Z3.context] in which [f] was created. *)


external func_entry_get_context : func_entry -> context = "get_context_z3_rc_val"
(** [func_entry_get_context f] is the [Z3.context] in which [f] was created. *)


external fixedpoint_get_context : fixedpoint -> context = "get_context_z3_rc_val"
(** [fixedpoint_get_context f] is the [Z3.context] in which [f] was created. *)


external optimize_get_context : optimize -> context = "get_context_z3_rc_val"
(** [optimize_get_context o] is the [Z3.context] in which [o] was created. *)


external rcf_num_get_context : rcf_num -> context = "get_context_z3_rc_val"
(** [rcf_num_get_context r] is the [Z3.context] in which [r] was created. *)

external global_param_set : string -> string -> unit
	= "camlidl_z3_Z3_global_param_set"

external global_param_reset_all : unit -> unit
	= "camlidl_z3_Z3_global_param_reset_all"

external global_param_get : string -> string_opt
	= "camlidl_z3_Z3_global_param_get"

external mk_config : unit -> config
	= "camlidl_z3_Z3_mk_config"

external del_config : config -> unit
	= "camlidl_z3_Z3_del_config"

external set_param_value : config -> string -> string -> unit
	= "camlidl_z3_Z3_set_param_value"

external update_param_value : context -> string -> string -> unit
	= "camlidl_z3_Z3_update_param_value"

external get_global_param_descrs : context -> param_descrs
	= "camlidl_z3_Z3_get_global_param_descrs"

external interrupt : context -> unit
	= "camlidl_z3_Z3_interrupt"

external enable_concurrent_dec_ref : context -> unit
	= "camlidl_z3_Z3_enable_concurrent_dec_ref"

external mk_params : context -> params
	= "camlidl_z3_Z3_mk_params"

external params_set_bool : context -> params -> symbol -> bool -> unit
	= "camlidl_z3_Z3_params_set_bool"

external params_set_uint : context -> params -> symbol -> int -> unit
	= "camlidl_z3_Z3_params_set_uint"

external params_set_double : context -> params -> symbol -> float -> unit
	= "camlidl_z3_Z3_params_set_double"

external params_set_symbol : context -> params -> symbol -> symbol -> unit
	= "camlidl_z3_Z3_params_set_symbol"

external params_to_string : context -> params -> string
	= "camlidl_z3_Z3_params_to_string"

external params_validate : context -> params -> param_descrs -> unit
	= "camlidl_z3_Z3_params_validate"

external param_descrs_get_kind : context -> param_descrs -> symbol -> param_kind
	= "camlidl_z3_Z3_param_descrs_get_kind"

external param_descrs_size : context -> param_descrs -> int
	= "camlidl_z3_Z3_param_descrs_size"

external param_descrs_get_name : context -> param_descrs -> int -> symbol
	= "camlidl_z3_Z3_param_descrs_get_name"

external param_descrs_get_documentation : context -> param_descrs -> symbol -> string
	= "camlidl_z3_Z3_param_descrs_get_documentation"

external param_descrs_to_string : context -> param_descrs -> string
	= "camlidl_z3_Z3_param_descrs_to_string"

external mk_int_symbol : context -> int -> symbol
	= "camlidl_z3_Z3_mk_int_symbol"

external mk_string_symbol : context -> string -> symbol
	= "camlidl_z3_Z3_mk_string_symbol"

external mk_uninterpreted_sort : context -> symbol -> sort
	= "camlidl_z3_Z3_mk_uninterpreted_sort"

external mk_type_variable : context -> symbol -> sort
	= "camlidl_z3_Z3_mk_type_variable"

external mk_bool_sort : context -> sort
	= "camlidl_z3_Z3_mk_bool_sort"

external mk_int_sort : context -> sort
	= "camlidl_z3_Z3_mk_int_sort"

external mk_real_sort : context -> sort
	= "camlidl_z3_Z3_mk_real_sort"

external mk_bv_sort : context -> int -> sort
	= "camlidl_z3_Z3_mk_bv_sort"

external mk_finite_domain_sort : context -> symbol -> int64 -> sort
	= "camlidl_z3_Z3_mk_finite_domain_sort"

external mk_array_sort : context -> sort -> sort -> sort
	= "camlidl_z3_Z3_mk_array_sort"

external mk_array_sort_n : context -> sort array -> sort -> sort
	= "camlidl_z3_Z3_mk_array_sort_n"

external mk_tuple_sort : context -> symbol -> symbol array -> sort array -> sort * func_decl * func_decl array
	= "camlidl_z3_Z3_mk_tuple_sort"

external mk_enumeration_sort : context -> symbol -> symbol array -> sort * func_decl array * func_decl array
	= "camlidl_z3_Z3_mk_enumeration_sort"

external mk_list_sort : context -> symbol -> sort -> sort * func_decl * func_decl * func_decl * func_decl * func_decl * func_decl
	= "camlidl_z3_Z3_mk_list_sort"

external mk_constructor : context -> symbol -> symbol -> symbol array -> sort_opt array -> int array -> constructor
	= "camlidl_z3_Z3_mk_constructor_bytecode" "camlidl_z3_Z3_mk_constructor"

external del_constructor : context -> constructor -> unit
	= "camlidl_z3_Z3_del_constructor"

external mk_polymorphic_datatype : context -> symbol -> sort array -> constructor array -> sort
	= "camlidl_z3_Z3_mk_polymorphic_datatype"

external mk_datatype_sort : context -> symbol -> sort array -> sort
	= "camlidl_z3_Z3_mk_datatype_sort"

external mk_constructor_list : context -> constructor array -> constructor_list
	= "camlidl_z3_Z3_mk_constructor_list"

external del_constructor_list : context -> constructor_list -> unit
	= "camlidl_z3_Z3_del_constructor_list"

external mk_datatypes : context -> symbol array -> constructor_list array -> sort array
	= "camlidl_z3_Z3_mk_datatypes"

external mk_func_decl : context -> symbol -> sort array -> sort -> func_decl
	= "camlidl_z3_Z3_mk_func_decl"

external mk_app : context -> func_decl -> ast array -> ast
	= "camlidl_z3_Z3_mk_app"

external mk_const : context -> symbol -> sort -> ast
	= "camlidl_z3_Z3_mk_const"

external mk_fresh_func_decl : context -> string -> sort array -> sort -> func_decl
	= "camlidl_z3_Z3_mk_fresh_func_decl"

external mk_fresh_const : context -> string -> sort -> ast
	= "camlidl_z3_Z3_mk_fresh_const"

external mk_rec_func_decl : context -> symbol -> sort array -> sort -> func_decl
	= "camlidl_z3_Z3_mk_rec_func_decl"

external add_rec_def : context -> func_decl -> ast array -> ast -> unit
	= "camlidl_z3_Z3_add_rec_def"

external mk_true : context -> ast
	= "camlidl_z3_Z3_mk_true"

external mk_false : context -> ast
	= "camlidl_z3_Z3_mk_false"

external mk_eq : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_eq"

external mk_distinct : context -> ast array -> ast
	= "camlidl_z3_Z3_mk_distinct"

external mk_not : context -> ast -> ast
	= "camlidl_z3_Z3_mk_not"

external mk_ite : context -> ast -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_ite"

external mk_iff : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_iff"

external mk_implies : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_implies"

external mk_xor : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_xor"

external mk_and : context -> ast array -> ast
	= "camlidl_z3_Z3_mk_and"

external mk_or : context -> ast array -> ast
	= "camlidl_z3_Z3_mk_or"

external mk_add : context -> ast array -> ast
	= "camlidl_z3_Z3_mk_add"

external mk_mul : context -> ast array -> ast
	= "camlidl_z3_Z3_mk_mul"

external mk_sub : context -> ast array -> ast
	= "camlidl_z3_Z3_mk_sub"

external mk_unary_minus : context -> ast -> ast
	= "camlidl_z3_Z3_mk_unary_minus"

external mk_div : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_div"

external mk_mod : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_mod"

external mk_rem : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_rem"

external mk_power : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_power"

external mk_abs : context -> ast -> ast
	= "camlidl_z3_Z3_mk_abs"

external mk_lt : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_lt"

external mk_le : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_le"

external mk_gt : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_gt"

external mk_ge : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_ge"

external mk_divides : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_divides"

external mk_int2real : context -> ast -> ast
	= "camlidl_z3_Z3_mk_int2real"

external mk_real2int : context -> ast -> ast
	= "camlidl_z3_Z3_mk_real2int"

external mk_is_int : context -> ast -> ast
	= "camlidl_z3_Z3_mk_is_int"

external mk_bvnot : context -> ast -> ast
	= "camlidl_z3_Z3_mk_bvnot"

external mk_bvredand : context -> ast -> ast
	= "camlidl_z3_Z3_mk_bvredand"

external mk_bvredor : context -> ast -> ast
	= "camlidl_z3_Z3_mk_bvredor"

external mk_bvand : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvand"

external mk_bvor : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvor"

external mk_bvxor : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvxor"

external mk_bvnand : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvnand"

external mk_bvnor : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvnor"

external mk_bvxnor : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvxnor"

external mk_bvneg : context -> ast -> ast
	= "camlidl_z3_Z3_mk_bvneg"

external mk_bvadd : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvadd"

external mk_bvsub : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvsub"

external mk_bvmul : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvmul"

external mk_bvudiv : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvudiv"

external mk_bvsdiv : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvsdiv"

external mk_bvurem : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvurem"

external mk_bvsrem : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvsrem"

external mk_bvsmod : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvsmod"

external mk_bvult : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvult"

external mk_bvslt : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvslt"

external mk_bvule : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvule"

external mk_bvsle : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvsle"

external mk_bvuge : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvuge"

external mk_bvsge : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvsge"

external mk_bvugt : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvugt"

external mk_bvsgt : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvsgt"

external mk_concat : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_concat"

external mk_extract : context -> int -> int -> ast -> ast
	= "camlidl_z3_Z3_mk_extract"

external mk_sign_ext : context -> int -> ast -> ast
	= "camlidl_z3_Z3_mk_sign_ext"

external mk_zero_ext : context -> int -> ast -> ast
	= "camlidl_z3_Z3_mk_zero_ext"

external mk_repeat : context -> int -> ast -> ast
	= "camlidl_z3_Z3_mk_repeat"

external mk_bit2bool : context -> int -> ast -> ast
	= "camlidl_z3_Z3_mk_bit2bool"

external mk_bvshl : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvshl"

external mk_bvlshr : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvlshr"

external mk_bvashr : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvashr"

external mk_rotate_left : context -> int -> ast -> ast
	= "camlidl_z3_Z3_mk_rotate_left"

external mk_rotate_right : context -> int -> ast -> ast
	= "camlidl_z3_Z3_mk_rotate_right"

external mk_ext_rotate_left : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_ext_rotate_left"

external mk_ext_rotate_right : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_ext_rotate_right"

external mk_int2bv : context -> int -> ast -> ast
	= "camlidl_z3_Z3_mk_int2bv"

external mk_bv2int : context -> ast -> bool -> ast
	= "camlidl_z3_Z3_mk_bv2int"

external mk_bvadd_no_overflow : context -> ast -> ast -> bool -> ast
	= "camlidl_z3_Z3_mk_bvadd_no_overflow"

external mk_bvadd_no_underflow : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvadd_no_underflow"

external mk_bvsub_no_overflow : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvsub_no_overflow"

external mk_bvsub_no_underflow : context -> ast -> ast -> bool -> ast
	= "camlidl_z3_Z3_mk_bvsub_no_underflow"

external mk_bvsdiv_no_overflow : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvsdiv_no_overflow"

external mk_bvneg_no_overflow : context -> ast -> ast
	= "camlidl_z3_Z3_mk_bvneg_no_overflow"

external mk_bvmul_no_overflow : context -> ast -> ast -> bool -> ast
	= "camlidl_z3_Z3_mk_bvmul_no_overflow"

external mk_bvmul_no_underflow : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_bvmul_no_underflow"

external mk_select : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_select"

external mk_select_n : context -> ast -> ast array -> ast
	= "camlidl_z3_Z3_mk_select_n"

external mk_store : context -> ast -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_store"

external mk_store_n : context -> ast -> ast array -> ast -> ast
	= "camlidl_z3_Z3_mk_store_n"

external mk_const_array : context -> sort -> ast -> ast
	= "camlidl_z3_Z3_mk_const_array"

external mk_map : context -> func_decl -> ast array -> ast
	= "camlidl_z3_Z3_mk_map"

external mk_array_default : context -> ast -> ast
	= "camlidl_z3_Z3_mk_array_default"

external mk_as_array : context -> func_decl -> ast
	= "camlidl_z3_Z3_mk_as_array"

external mk_set_sort : context -> sort -> sort
	= "camlidl_z3_Z3_mk_set_sort"

external mk_empty_set : context -> sort -> ast
	= "camlidl_z3_Z3_mk_empty_set"

external mk_full_set : context -> sort -> ast
	= "camlidl_z3_Z3_mk_full_set"

external mk_set_add : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_set_add"

external mk_set_del : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_set_del"

external mk_set_union : context -> ast array -> ast
	= "camlidl_z3_Z3_mk_set_union"

external mk_set_intersect : context -> ast array -> ast
	= "camlidl_z3_Z3_mk_set_intersect"

external mk_set_difference : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_set_difference"

external mk_set_complement : context -> ast -> ast
	= "camlidl_z3_Z3_mk_set_complement"

external mk_set_member : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_set_member"

external mk_set_subset : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_set_subset"

external mk_array_ext : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_array_ext"

external mk_numeral : context -> string -> sort -> ast
	= "camlidl_z3_Z3_mk_numeral"

external mk_real : context -> int -> int -> ast
	= "camlidl_z3_Z3_mk_real"

external mk_real_int64 : context -> int64 -> int64 -> ast
	= "camlidl_z3_Z3_mk_real_int64"

external mk_int : context -> int -> sort -> ast
	= "camlidl_z3_Z3_mk_int"

external mk_unsigned_int : context -> int -> sort -> ast
	= "camlidl_z3_Z3_mk_unsigned_int"

external mk_int64 : context -> int64 -> sort -> ast
	= "camlidl_z3_Z3_mk_int64"

external mk_unsigned_int64 : context -> int64 -> sort -> ast
	= "camlidl_z3_Z3_mk_unsigned_int64"

external mk_bv_numeral : context -> bool array -> ast
	= "camlidl_z3_Z3_mk_bv_numeral"

external mk_seq_sort : context -> sort -> sort
	= "camlidl_z3_Z3_mk_seq_sort"

external is_seq_sort : context -> sort -> bool
	= "camlidl_z3_Z3_is_seq_sort"

external get_seq_sort_basis : context -> sort -> sort
	= "camlidl_z3_Z3_get_seq_sort_basis"

external mk_re_sort : context -> sort -> sort
	= "camlidl_z3_Z3_mk_re_sort"

external is_re_sort : context -> sort -> bool
	= "camlidl_z3_Z3_is_re_sort"

external get_re_sort_basis : context -> sort -> sort
	= "camlidl_z3_Z3_get_re_sort_basis"

external mk_string_sort : context -> sort
	= "camlidl_z3_Z3_mk_string_sort"

external mk_char_sort : context -> sort
	= "camlidl_z3_Z3_mk_char_sort"

external is_string_sort : context -> sort -> bool
	= "camlidl_z3_Z3_is_string_sort"

external is_char_sort : context -> sort -> bool
	= "camlidl_z3_Z3_is_char_sort"

external mk_string : context -> string -> ast
	= "camlidl_z3_Z3_mk_string"

external mk_lstring : context -> int -> string -> ast
	= "camlidl_z3_Z3_mk_lstring"

external mk_u32string : context -> int array -> ast
	= "camlidl_z3_Z3_mk_u32string"

external is_string : context -> ast -> bool
	= "camlidl_z3_Z3_is_string"

external get_string : context -> ast -> string
	= "camlidl_z3_Z3_get_string"

external get_string_length : context -> ast -> int
	= "camlidl_z3_Z3_get_string_length"

external get_string_contents : context -> ast -> int -> int array
	= "camlidl_z3_Z3_get_string_contents"

external mk_seq_empty : context -> sort -> ast
	= "camlidl_z3_Z3_mk_seq_empty"

external mk_seq_unit : context -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_unit"

external mk_seq_concat : context -> ast array -> ast
	= "camlidl_z3_Z3_mk_seq_concat"

external mk_seq_prefix : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_prefix"

external mk_seq_suffix : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_suffix"

external mk_seq_contains : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_contains"

external mk_str_lt : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_str_lt"

external mk_str_le : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_str_le"

external mk_seq_extract : context -> ast -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_extract"

external mk_seq_replace : context -> ast -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_replace"

external mk_seq_replace_all : context -> ast -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_replace_all"

external mk_seq_replace_re : context -> ast -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_replace_re"

external mk_seq_replace_re_all : context -> ast -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_replace_re_all"

external mk_seq_at : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_at"

external mk_seq_nth : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_nth"

external mk_seq_length : context -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_length"

external mk_seq_index : context -> ast -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_index"

external mk_seq_last_index : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_last_index"

external mk_seq_map : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_map"

external mk_seq_mapi : context -> ast -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_mapi"

external mk_seq_foldl : context -> ast -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_foldl"

external mk_seq_foldli : context -> ast -> ast -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_foldli"

external mk_str_to_int : context -> ast -> ast
	= "camlidl_z3_Z3_mk_str_to_int"

external mk_int_to_str : context -> ast -> ast
	= "camlidl_z3_Z3_mk_int_to_str"

external mk_string_to_code : context -> ast -> ast
	= "camlidl_z3_Z3_mk_string_to_code"

external mk_string_from_code : context -> ast -> ast
	= "camlidl_z3_Z3_mk_string_from_code"

external mk_ubv_to_str : context -> ast -> ast
	= "camlidl_z3_Z3_mk_ubv_to_str"

external mk_sbv_to_str : context -> ast -> ast
	= "camlidl_z3_Z3_mk_sbv_to_str"

external mk_seq_to_re : context -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_to_re"

external mk_seq_in_re : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_seq_in_re"

external mk_re_plus : context -> ast -> ast
	= "camlidl_z3_Z3_mk_re_plus"

external mk_re_star : context -> ast -> ast
	= "camlidl_z3_Z3_mk_re_star"

external mk_re_option : context -> ast -> ast
	= "camlidl_z3_Z3_mk_re_option"

external mk_re_union : context -> ast array -> ast
	= "camlidl_z3_Z3_mk_re_union"

external mk_re_concat : context -> ast array -> ast
	= "camlidl_z3_Z3_mk_re_concat"

external mk_re_range : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_re_range"

external mk_re_allchar : context -> sort -> ast
	= "camlidl_z3_Z3_mk_re_allchar"

external mk_re_loop : context -> ast -> int -> int -> ast
	= "camlidl_z3_Z3_mk_re_loop"

external mk_re_power : context -> ast -> int -> ast
	= "camlidl_z3_Z3_mk_re_power"

external mk_re_intersect : context -> ast array -> ast
	= "camlidl_z3_Z3_mk_re_intersect"

external mk_re_complement : context -> ast -> ast
	= "camlidl_z3_Z3_mk_re_complement"

external mk_re_diff : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_re_diff"

external mk_re_empty : context -> sort -> ast
	= "camlidl_z3_Z3_mk_re_empty"

external mk_re_full : context -> sort -> ast
	= "camlidl_z3_Z3_mk_re_full"

external mk_char : context -> int -> ast
	= "camlidl_z3_Z3_mk_char"

external mk_char_le : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_char_le"

external mk_char_to_int : context -> ast -> ast
	= "camlidl_z3_Z3_mk_char_to_int"

external mk_char_to_bv : context -> ast -> ast
	= "camlidl_z3_Z3_mk_char_to_bv"

external mk_char_from_bv : context -> ast -> ast
	= "camlidl_z3_Z3_mk_char_from_bv"

external mk_char_is_digit : context -> ast -> ast
	= "camlidl_z3_Z3_mk_char_is_digit"

external mk_linear_order : context -> sort -> int -> func_decl
	= "camlidl_z3_Z3_mk_linear_order"

external mk_partial_order : context -> sort -> int -> func_decl
	= "camlidl_z3_Z3_mk_partial_order"

external mk_piecewise_linear_order : context -> sort -> int -> func_decl
	= "camlidl_z3_Z3_mk_piecewise_linear_order"

external mk_tree_order : context -> sort -> int -> func_decl
	= "camlidl_z3_Z3_mk_tree_order"

external mk_transitive_closure : context -> func_decl -> func_decl
	= "camlidl_z3_Z3_mk_transitive_closure"

external mk_pattern : context -> ast array -> pattern
	= "camlidl_z3_Z3_mk_pattern"

external mk_bound : context -> int -> sort -> ast
	= "camlidl_z3_Z3_mk_bound"

external mk_forall : context -> int -> pattern array -> sort array -> symbol array -> ast -> ast
	= "camlidl_z3_Z3_mk_forall_bytecode" "camlidl_z3_Z3_mk_forall"

external mk_exists : context -> int -> pattern array -> sort array -> symbol array -> ast -> ast
	= "camlidl_z3_Z3_mk_exists_bytecode" "camlidl_z3_Z3_mk_exists"

external mk_quantifier : context -> bool -> int -> pattern array -> sort array -> symbol array -> ast -> ast
	= "camlidl_z3_Z3_mk_quantifier_bytecode" "camlidl_z3_Z3_mk_quantifier"

external mk_quantifier_ex : context -> bool -> int -> symbol -> symbol -> pattern array -> ast array -> sort array -> symbol array -> ast -> ast
	= "camlidl_z3_Z3_mk_quantifier_ex_bytecode" "camlidl_z3_Z3_mk_quantifier_ex"

external mk_forall_const : context -> int -> app array -> pattern array -> ast -> ast
	= "camlidl_z3_Z3_mk_forall_const"

external mk_exists_const : context -> int -> app array -> pattern array -> ast -> ast
	= "camlidl_z3_Z3_mk_exists_const"

external mk_quantifier_const : context -> bool -> int -> app array -> pattern array -> ast -> ast
	= "camlidl_z3_Z3_mk_quantifier_const_bytecode" "camlidl_z3_Z3_mk_quantifier_const"

external mk_quantifier_const_ex : context -> bool -> int -> symbol -> symbol -> app array -> pattern array -> ast array -> ast -> ast
	= "camlidl_z3_Z3_mk_quantifier_const_ex_bytecode" "camlidl_z3_Z3_mk_quantifier_const_ex"

external mk_lambda : context -> sort array -> symbol array -> ast -> ast
	= "camlidl_z3_Z3_mk_lambda"

external mk_lambda_const : context -> app array -> ast -> ast
	= "camlidl_z3_Z3_mk_lambda_const"

external get_symbol_kind : context -> symbol -> symbol_kind
	= "camlidl_z3_Z3_get_symbol_kind"

external get_symbol_int : context -> symbol -> int
	= "camlidl_z3_Z3_get_symbol_int"

external get_symbol_string : context -> symbol -> string
	= "camlidl_z3_Z3_get_symbol_string"

external get_sort_name : context -> sort -> symbol
	= "camlidl_z3_Z3_get_sort_name"

external get_sort_id : context -> sort -> int
	= "camlidl_z3_Z3_get_sort_id"

external sort_to_ast : context -> sort -> ast
	= "camlidl_z3_Z3_sort_to_ast"

external is_eq_sort : context -> sort -> sort -> bool
	= "camlidl_z3_Z3_is_eq_sort"

external get_sort_kind : context -> sort -> sort_kind
	= "camlidl_z3_Z3_get_sort_kind"

external get_bv_sort_size : context -> sort -> int
	= "camlidl_z3_Z3_get_bv_sort_size"

external get_finite_domain_sort_size : context -> sort -> bool * int64
	= "camlidl_z3_Z3_get_finite_domain_sort_size"

external get_array_arity : context -> sort -> int
	= "camlidl_z3_Z3_get_array_arity"

external get_array_sort_domain : context -> sort -> sort
	= "camlidl_z3_Z3_get_array_sort_domain"

external get_array_sort_domain_n : context -> sort -> int -> sort
	= "camlidl_z3_Z3_get_array_sort_domain_n"

external get_array_sort_range : context -> sort -> sort
	= "camlidl_z3_Z3_get_array_sort_range"

external get_tuple_sort_mk_decl : context -> sort -> func_decl
	= "camlidl_z3_Z3_get_tuple_sort_mk_decl"

external get_tuple_sort_num_fields : context -> sort -> int
	= "camlidl_z3_Z3_get_tuple_sort_num_fields"

external get_tuple_sort_field_decl : context -> sort -> int -> func_decl
	= "camlidl_z3_Z3_get_tuple_sort_field_decl"

external is_recursive_datatype_sort : context -> sort -> bool
	= "camlidl_z3_Z3_is_recursive_datatype_sort"

external get_datatype_sort_num_constructors : context -> sort -> int
	= "camlidl_z3_Z3_get_datatype_sort_num_constructors"

external get_datatype_sort_constructor : context -> sort -> int -> func_decl
	= "camlidl_z3_Z3_get_datatype_sort_constructor"

external get_datatype_sort_recognizer : context -> sort -> int -> func_decl
	= "camlidl_z3_Z3_get_datatype_sort_recognizer"

external get_datatype_sort_constructor_accessor : context -> sort -> int -> int -> func_decl
	= "camlidl_z3_Z3_get_datatype_sort_constructor_accessor"

external datatype_update_field : context -> func_decl -> ast -> ast -> ast
	= "camlidl_z3_Z3_datatype_update_field"

external get_relation_arity : context -> sort -> int
	= "camlidl_z3_Z3_get_relation_arity"

external get_relation_column : context -> sort -> int -> sort
	= "camlidl_z3_Z3_get_relation_column"

external mk_atmost : context -> ast array -> int -> ast
	= "camlidl_z3_Z3_mk_atmost"

external mk_atleast : context -> ast array -> int -> ast
	= "camlidl_z3_Z3_mk_atleast"

external mk_pble : context -> ast array -> int array -> int -> ast
	= "camlidl_z3_Z3_mk_pble"

external mk_pbge : context -> ast array -> int array -> int -> ast
	= "camlidl_z3_Z3_mk_pbge"

external mk_pbeq : context -> ast array -> int array -> int -> ast
	= "camlidl_z3_Z3_mk_pbeq"

external func_decl_to_ast : context -> func_decl -> ast
	= "camlidl_z3_Z3_func_decl_to_ast"

external is_eq_func_decl : context -> func_decl -> func_decl -> bool
	= "camlidl_z3_Z3_is_eq_func_decl"

external get_func_decl_id : context -> func_decl -> int
	= "camlidl_z3_Z3_get_func_decl_id"

external get_decl_name : context -> func_decl -> symbol
	= "camlidl_z3_Z3_get_decl_name"

external get_decl_kind : context -> func_decl -> decl_kind
	= "camlidl_z3_Z3_get_decl_kind"

external get_domain_size : context -> func_decl -> int
	= "camlidl_z3_Z3_get_domain_size"

external get_domain : context -> func_decl -> int -> sort
	= "camlidl_z3_Z3_get_domain"

external get_range : context -> func_decl -> sort
	= "camlidl_z3_Z3_get_range"

external get_decl_num_parameters : context -> func_decl -> int
	= "camlidl_z3_Z3_get_decl_num_parameters"

external get_decl_parameter_kind : context -> func_decl -> int -> parameter_kind
	= "camlidl_z3_Z3_get_decl_parameter_kind"

external get_decl_int_parameter : context -> func_decl -> int -> int
	= "camlidl_z3_Z3_get_decl_int_parameter"

external get_decl_double_parameter : context -> func_decl -> int -> float
	= "camlidl_z3_Z3_get_decl_double_parameter"

external get_decl_symbol_parameter : context -> func_decl -> int -> symbol
	= "camlidl_z3_Z3_get_decl_symbol_parameter"

external get_decl_sort_parameter : context -> func_decl -> int -> sort
	= "camlidl_z3_Z3_get_decl_sort_parameter"

external get_decl_ast_parameter : context -> func_decl -> int -> ast
	= "camlidl_z3_Z3_get_decl_ast_parameter"

external get_decl_func_decl_parameter : context -> func_decl -> int -> func_decl
	= "camlidl_z3_Z3_get_decl_func_decl_parameter"

external get_decl_rational_parameter : context -> func_decl -> int -> string
	= "camlidl_z3_Z3_get_decl_rational_parameter"

external app_to_ast : context -> app -> ast
	= "camlidl_z3_Z3_app_to_ast"

external get_app_decl : context -> app -> func_decl
	= "camlidl_z3_Z3_get_app_decl"

external get_app_num_args : context -> app -> int
	= "camlidl_z3_Z3_get_app_num_args"

external get_app_arg : context -> app -> int -> ast
	= "camlidl_z3_Z3_get_app_arg"

external is_eq_ast : context -> ast -> ast -> bool
	= "camlidl_z3_Z3_is_eq_ast"

external get_ast_id : context -> ast -> int
	= "camlidl_z3_Z3_get_ast_id"

external get_ast_hash : context -> ast -> int
	= "camlidl_z3_Z3_get_ast_hash"

external get_sort : context -> ast -> sort
	= "camlidl_z3_Z3_get_sort"

external is_well_sorted : context -> ast -> bool
	= "camlidl_z3_Z3_is_well_sorted"

external get_bool_value : context -> ast -> lbool
	= "camlidl_z3_Z3_get_bool_value"

external get_ast_kind : context -> ast -> ast_kind
	= "camlidl_z3_Z3_get_ast_kind"

external is_app : context -> ast -> bool
	= "camlidl_z3_Z3_is_app"

external is_ground : context -> ast -> bool
	= "camlidl_z3_Z3_is_ground"

external get_depth : context -> ast -> int
	= "camlidl_z3_Z3_get_depth"

external is_numeral_ast : context -> ast -> bool
	= "camlidl_z3_Z3_is_numeral_ast"

external is_algebraic_number : context -> ast -> bool
	= "camlidl_z3_Z3_is_algebraic_number"

external to_app : context -> ast -> app
	= "camlidl_z3_Z3_to_app"

external to_func_decl : context -> ast -> func_decl
	= "camlidl_z3_Z3_to_func_decl"

external get_numeral_string : context -> ast -> string
	= "camlidl_z3_Z3_get_numeral_string"

external get_numeral_binary_string : context -> ast -> string
	= "camlidl_z3_Z3_get_numeral_binary_string"

external get_numeral_decimal_string : context -> ast -> int -> string
	= "camlidl_z3_Z3_get_numeral_decimal_string"

external get_numeral_double : context -> ast -> float
	= "camlidl_z3_Z3_get_numeral_double"

external get_numerator : context -> ast -> ast
	= "camlidl_z3_Z3_get_numerator"

external get_denominator : context -> ast -> ast
	= "camlidl_z3_Z3_get_denominator"

external get_numeral_int : context -> ast -> bool * int
	= "camlidl_z3_Z3_get_numeral_int"

external get_numeral_uint : context -> ast -> bool * int
	= "camlidl_z3_Z3_get_numeral_uint"

external get_numeral_uint64 : context -> ast -> bool * int64
	= "camlidl_z3_Z3_get_numeral_uint64"

external get_numeral_int64 : context -> ast -> bool * int64
	= "camlidl_z3_Z3_get_numeral_int64"

external get_numeral_rational_int64 : context -> ast -> bool * int64 * int64
	= "camlidl_z3_Z3_get_numeral_rational_int64"

external get_algebraic_number_lower : context -> ast -> int -> ast
	= "camlidl_z3_Z3_get_algebraic_number_lower"

external get_algebraic_number_upper : context -> ast -> int -> ast
	= "camlidl_z3_Z3_get_algebraic_number_upper"

external pattern_to_ast : context -> pattern -> ast
	= "camlidl_z3_Z3_pattern_to_ast"

external get_pattern_num_terms : context -> pattern -> int
	= "camlidl_z3_Z3_get_pattern_num_terms"

external get_pattern : context -> pattern -> int -> ast
	= "camlidl_z3_Z3_get_pattern"

external get_index_value : context -> ast -> int
	= "camlidl_z3_Z3_get_index_value"

external is_quantifier_forall : context -> ast -> bool
	= "camlidl_z3_Z3_is_quantifier_forall"

external is_quantifier_exists : context -> ast -> bool
	= "camlidl_z3_Z3_is_quantifier_exists"

external is_lambda : context -> ast -> bool
	= "camlidl_z3_Z3_is_lambda"

external get_quantifier_weight : context -> ast -> int
	= "camlidl_z3_Z3_get_quantifier_weight"

external get_quantifier_skolem_id : context -> ast -> symbol
	= "camlidl_z3_Z3_get_quantifier_skolem_id"

external get_quantifier_id : context -> ast -> symbol
	= "camlidl_z3_Z3_get_quantifier_id"

external get_quantifier_num_patterns : context -> ast -> int
	= "camlidl_z3_Z3_get_quantifier_num_patterns"

external get_quantifier_pattern_ast : context -> ast -> int -> pattern
	= "camlidl_z3_Z3_get_quantifier_pattern_ast"

external get_quantifier_num_no_patterns : context -> ast -> int
	= "camlidl_z3_Z3_get_quantifier_num_no_patterns"

external get_quantifier_no_pattern_ast : context -> ast -> int -> ast
	= "camlidl_z3_Z3_get_quantifier_no_pattern_ast"

external get_quantifier_num_bound : context -> ast -> int
	= "camlidl_z3_Z3_get_quantifier_num_bound"

external get_quantifier_bound_name : context -> ast -> int -> symbol
	= "camlidl_z3_Z3_get_quantifier_bound_name"

external get_quantifier_bound_sort : context -> ast -> int -> sort
	= "camlidl_z3_Z3_get_quantifier_bound_sort"

external get_quantifier_body : context -> ast -> ast
	= "camlidl_z3_Z3_get_quantifier_body"

external simplify : context -> ast -> ast
	= "camlidl_z3_Z3_simplify"

external simplify_ex : context -> ast -> params -> ast
	= "camlidl_z3_Z3_simplify_ex"

external simplify_get_help : context -> string
	= "camlidl_z3_Z3_simplify_get_help"

external simplify_get_param_descrs : context -> param_descrs
	= "camlidl_z3_Z3_simplify_get_param_descrs"

external update_term : context -> ast -> ast array -> ast
	= "camlidl_z3_Z3_update_term"

external substitute : context -> ast -> ast array -> ast array -> ast
	= "camlidl_z3_Z3_substitute"

external substitute_vars : context -> ast -> ast array -> ast
	= "camlidl_z3_Z3_substitute_vars"

external substitute_funs : context -> ast -> func_decl array -> ast array -> ast
	= "camlidl_z3_Z3_substitute_funs"

external translate : context -> ast -> context -> ast
	= "camlidl_z3_Z3_translate"

external mk_model : context -> model
	= "camlidl_z3_Z3_mk_model"

external model_eval : context -> model -> ast -> bool -> ast_opt
	= "camlidl_z3_Z3_model_eval"

external model_get_const_interp : context -> model -> func_decl -> ast_opt
	= "camlidl_z3_Z3_model_get_const_interp"

external model_has_interp : context -> model -> func_decl -> bool
	= "camlidl_z3_Z3_model_has_interp"

external model_get_func_interp : context -> model -> func_decl -> func_interp_opt
	= "camlidl_z3_Z3_model_get_func_interp"

external model_get_num_consts : context -> model -> int
	= "camlidl_z3_Z3_model_get_num_consts"

external model_get_const_decl : context -> model -> int -> func_decl
	= "camlidl_z3_Z3_model_get_const_decl"

external model_get_num_funcs : context -> model -> int
	= "camlidl_z3_Z3_model_get_num_funcs"

external model_get_func_decl : context -> model -> int -> func_decl
	= "camlidl_z3_Z3_model_get_func_decl"

external model_get_num_sorts : context -> model -> int
	= "camlidl_z3_Z3_model_get_num_sorts"

external model_get_sort : context -> model -> int -> sort
	= "camlidl_z3_Z3_model_get_sort"

external model_get_sort_universe : context -> model -> sort -> ast_vector
	= "camlidl_z3_Z3_model_get_sort_universe"

external model_translate : context -> model -> context -> model
	= "camlidl_z3_Z3_model_translate"

external is_as_array : context -> ast -> bool
	= "camlidl_z3_Z3_is_as_array"

external get_as_array_func_decl : context -> ast -> func_decl
	= "camlidl_z3_Z3_get_as_array_func_decl"

external add_func_interp : context -> model -> func_decl -> ast -> func_interp
	= "camlidl_z3_Z3_add_func_interp"

external add_const_interp : context -> model -> func_decl -> ast -> unit
	= "camlidl_z3_Z3_add_const_interp"

external func_interp_get_num_entries : context -> func_interp -> int
	= "camlidl_z3_Z3_func_interp_get_num_entries"

external func_interp_get_entry : context -> func_interp -> int -> func_entry
	= "camlidl_z3_Z3_func_interp_get_entry"

external func_interp_get_else : context -> func_interp -> ast
	= "camlidl_z3_Z3_func_interp_get_else"

external func_interp_set_else : context -> func_interp -> ast -> unit
	= "camlidl_z3_Z3_func_interp_set_else"

external func_interp_get_arity : context -> func_interp -> int
	= "camlidl_z3_Z3_func_interp_get_arity"

external func_interp_add_entry : context -> func_interp -> ast_vector -> ast -> unit
	= "camlidl_z3_Z3_func_interp_add_entry"

external func_entry_get_value : context -> func_entry -> ast
	= "camlidl_z3_Z3_func_entry_get_value"

external func_entry_get_num_args : context -> func_entry -> int
	= "camlidl_z3_Z3_func_entry_get_num_args"

external func_entry_get_arg : context -> func_entry -> int -> ast
	= "camlidl_z3_Z3_func_entry_get_arg"

external open_log : string -> bool
	= "camlidl_z3_Z3_open_log"

external append_log : string -> unit
	= "camlidl_z3_Z3_append_log"

external close_log : unit -> unit
	= "camlidl_z3_Z3_close_log"

external toggle_warning_messages : bool -> unit
	= "camlidl_z3_Z3_toggle_warning_messages"

external set_ast_print_mode : context -> ast_print_mode -> unit
	= "camlidl_z3_Z3_set_ast_print_mode"

external ast_to_string : context -> ast -> string
	= "camlidl_z3_Z3_ast_to_string"

external pattern_to_string : context -> pattern -> string
	= "camlidl_z3_Z3_pattern_to_string"

external sort_to_string : context -> sort -> string
	= "camlidl_z3_Z3_sort_to_string"

external func_decl_to_string : context -> func_decl -> string
	= "camlidl_z3_Z3_func_decl_to_string"

external model_to_string : context -> model -> string
	= "camlidl_z3_Z3_model_to_string"

external benchmark_to_smtlib_string : context -> string -> string -> string -> string -> ast array -> ast -> string
	= "camlidl_z3_Z3_benchmark_to_smtlib_string_bytecode" "camlidl_z3_Z3_benchmark_to_smtlib_string"

external parse_smtlib2_string : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> ast_vector
	= "camlidl_z3_Z3_parse_smtlib2_string_bytecode" "camlidl_z3_Z3_parse_smtlib2_string"

external parse_smtlib2_file : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> ast_vector
	= "camlidl_z3_Z3_parse_smtlib2_file_bytecode" "camlidl_z3_Z3_parse_smtlib2_file"

external eval_smtlib2_string : context -> string -> string
	= "camlidl_z3_Z3_eval_smtlib2_string"

external mk_parser_context : context -> parser_context
	= "camlidl_z3_Z3_mk_parser_context"

external parser_context_add_sort : context -> parser_context -> sort -> unit
	= "camlidl_z3_Z3_parser_context_add_sort"

external parser_context_add_decl : context -> parser_context -> func_decl -> unit
	= "camlidl_z3_Z3_parser_context_add_decl"

external parser_context_from_string : context -> parser_context -> string -> ast_vector
	= "camlidl_z3_Z3_parser_context_from_string"

external set_error : context -> error_code -> unit
	= "camlidl_z3_Z3_set_error"

external get_version : unit -> int * int * int * int
	= "camlidl_z3_Z3_get_version"

external get_full_version : unit -> string
	= "camlidl_z3_Z3_get_full_version"

external enable_trace : string -> unit
	= "camlidl_z3_Z3_enable_trace"

external disable_trace : string -> unit
	= "camlidl_z3_Z3_disable_trace"

external mk_goal : context -> bool -> bool -> bool -> goal
	= "camlidl_z3_Z3_mk_goal"

external goal_precision : context -> goal -> goal_prec
	= "camlidl_z3_Z3_goal_precision"

external goal_assert : context -> goal -> ast -> unit
	= "camlidl_z3_Z3_goal_assert"

external goal_inconsistent : context -> goal -> bool
	= "camlidl_z3_Z3_goal_inconsistent"

external goal_depth : context -> goal -> int
	= "camlidl_z3_Z3_goal_depth"

external goal_reset : context -> goal -> unit
	= "camlidl_z3_Z3_goal_reset"

external goal_size : context -> goal -> int
	= "camlidl_z3_Z3_goal_size"

external goal_formula : context -> goal -> int -> ast
	= "camlidl_z3_Z3_goal_formula"

external goal_num_exprs : context -> goal -> int
	= "camlidl_z3_Z3_goal_num_exprs"

external goal_is_decided_sat : context -> goal -> bool
	= "camlidl_z3_Z3_goal_is_decided_sat"

external goal_is_decided_unsat : context -> goal -> bool
	= "camlidl_z3_Z3_goal_is_decided_unsat"

external goal_translate : context -> goal -> context -> goal
	= "camlidl_z3_Z3_goal_translate"

external goal_convert_model : context -> goal -> model_opt -> model_opt
	= "camlidl_z3_Z3_goal_convert_model"

external goal_to_string : context -> goal -> string
	= "camlidl_z3_Z3_goal_to_string"

external goal_to_dimacs_string : context -> goal -> bool -> string
	= "camlidl_z3_Z3_goal_to_dimacs_string"

external mk_tactic : context -> string -> tactic
	= "camlidl_z3_Z3_mk_tactic"

external mk_probe : context -> string -> probe
	= "camlidl_z3_Z3_mk_probe"

external tactic_and_then : context -> tactic -> tactic -> tactic
	= "camlidl_z3_Z3_tactic_and_then"

external tactic_or_else : context -> tactic -> tactic -> tactic
	= "camlidl_z3_Z3_tactic_or_else"

external tactic_par_or : context -> tactic array -> tactic
	= "camlidl_z3_Z3_tactic_par_or"

external tactic_par_and_then : context -> tactic -> tactic -> tactic
	= "camlidl_z3_Z3_tactic_par_and_then"

external tactic_try_for : context -> tactic -> int -> tactic
	= "camlidl_z3_Z3_tactic_try_for"

external tactic_when : context -> probe -> tactic -> tactic
	= "camlidl_z3_Z3_tactic_when"

external tactic_cond : context -> probe -> tactic -> tactic -> tactic
	= "camlidl_z3_Z3_tactic_cond"

external tactic_repeat : context -> tactic -> int -> tactic
	= "camlidl_z3_Z3_tactic_repeat"

external tactic_skip : context -> tactic
	= "camlidl_z3_Z3_tactic_skip"

external tactic_fail : context -> tactic
	= "camlidl_z3_Z3_tactic_fail"

external tactic_fail_if : context -> probe -> tactic
	= "camlidl_z3_Z3_tactic_fail_if"

external tactic_fail_if_not_decided : context -> tactic
	= "camlidl_z3_Z3_tactic_fail_if_not_decided"

external tactic_using_params : context -> tactic -> params -> tactic
	= "camlidl_z3_Z3_tactic_using_params"

external mk_simplifier : context -> string -> simplifier
	= "camlidl_z3_Z3_mk_simplifier"

external solver_add_simplifier : context -> solver -> simplifier -> solver
	= "camlidl_z3_Z3_solver_add_simplifier"

external simplifier_and_then : context -> simplifier -> simplifier -> simplifier
	= "camlidl_z3_Z3_simplifier_and_then"

external simplifier_using_params : context -> simplifier -> params -> simplifier
	= "camlidl_z3_Z3_simplifier_using_params"

external get_num_simplifiers : context -> int
	= "camlidl_z3_Z3_get_num_simplifiers"

external get_simplifier_name : context -> int -> string
	= "camlidl_z3_Z3_get_simplifier_name"

external simplifier_get_help : context -> simplifier -> string
	= "camlidl_z3_Z3_simplifier_get_help"

external simplifier_get_param_descrs : context -> simplifier -> param_descrs
	= "camlidl_z3_Z3_simplifier_get_param_descrs"

external simplifier_get_descr : context -> string -> string
	= "camlidl_z3_Z3_simplifier_get_descr"

external probe_const : context -> float -> probe
	= "camlidl_z3_Z3_probe_const"

external probe_lt : context -> probe -> probe -> probe
	= "camlidl_z3_Z3_probe_lt"

external probe_gt : context -> probe -> probe -> probe
	= "camlidl_z3_Z3_probe_gt"

external probe_le : context -> probe -> probe -> probe
	= "camlidl_z3_Z3_probe_le"

external probe_ge : context -> probe -> probe -> probe
	= "camlidl_z3_Z3_probe_ge"

external probe_eq : context -> probe -> probe -> probe
	= "camlidl_z3_Z3_probe_eq"

external probe_and : context -> probe -> probe -> probe
	= "camlidl_z3_Z3_probe_and"

external probe_or : context -> probe -> probe -> probe
	= "camlidl_z3_Z3_probe_or"

external probe_not : context -> probe -> probe
	= "camlidl_z3_Z3_probe_not"

external get_num_tactics : context -> int
	= "camlidl_z3_Z3_get_num_tactics"

external get_tactic_name : context -> int -> string
	= "camlidl_z3_Z3_get_tactic_name"

external get_num_probes : context -> int
	= "camlidl_z3_Z3_get_num_probes"

external get_probe_name : context -> int -> string
	= "camlidl_z3_Z3_get_probe_name"

external tactic_get_help : context -> tactic -> string
	= "camlidl_z3_Z3_tactic_get_help"

external tactic_get_param_descrs : context -> tactic -> param_descrs
	= "camlidl_z3_Z3_tactic_get_param_descrs"

external tactic_get_descr : context -> string -> string
	= "camlidl_z3_Z3_tactic_get_descr"

external probe_get_descr : context -> string -> string
	= "camlidl_z3_Z3_probe_get_descr"

external probe_apply : context -> probe -> goal -> float
	= "camlidl_z3_Z3_probe_apply"

external tactic_apply : context -> tactic -> goal -> apply_result
	= "camlidl_z3_Z3_tactic_apply"

external tactic_apply_ex : context -> tactic -> goal -> params -> apply_result
	= "camlidl_z3_Z3_tactic_apply_ex"

external apply_result_to_string : context -> apply_result -> string
	= "camlidl_z3_Z3_apply_result_to_string"

external apply_result_get_num_subgoals : context -> apply_result -> int
	= "camlidl_z3_Z3_apply_result_get_num_subgoals"

external apply_result_get_subgoal : context -> apply_result -> int -> goal
	= "camlidl_z3_Z3_apply_result_get_subgoal"

external mk_solver : context -> solver
	= "camlidl_z3_Z3_mk_solver"

external mk_simple_solver : context -> solver
	= "camlidl_z3_Z3_mk_simple_solver"

external mk_solver_for_logic : context -> symbol -> solver
	= "camlidl_z3_Z3_mk_solver_for_logic"

external mk_solver_from_tactic : context -> tactic -> solver
	= "camlidl_z3_Z3_mk_solver_from_tactic"

external solver_translate : context -> solver -> context -> solver
	= "camlidl_z3_Z3_solver_translate"

external solver_import_model_converter : context -> solver -> solver -> unit
	= "camlidl_z3_Z3_solver_import_model_converter"

external solver_get_help : context -> solver -> string
	= "camlidl_z3_Z3_solver_get_help"

external solver_get_param_descrs : context -> solver -> param_descrs
	= "camlidl_z3_Z3_solver_get_param_descrs"

external solver_set_params : context -> solver -> params -> unit
	= "camlidl_z3_Z3_solver_set_params"

external solver_interrupt : context -> solver -> unit
	= "camlidl_z3_Z3_solver_interrupt"

external solver_push : context -> solver -> unit
	= "camlidl_z3_Z3_solver_push"

external solver_pop : context -> solver -> int -> unit
	= "camlidl_z3_Z3_solver_pop"

external solver_reset : context -> solver -> unit
	= "camlidl_z3_Z3_solver_reset"

external solver_get_num_scopes : context -> solver -> int
	= "camlidl_z3_Z3_solver_get_num_scopes"

external solver_assert : context -> solver -> ast -> unit
	= "camlidl_z3_Z3_solver_assert"

external solver_assert_and_track : context -> solver -> ast -> ast -> unit
	= "camlidl_z3_Z3_solver_assert_and_track"

external solver_from_file : context -> solver -> string -> unit
	= "camlidl_z3_Z3_solver_from_file"

external solver_from_string : context -> solver -> string -> unit
	= "camlidl_z3_Z3_solver_from_string"

external solver_get_assertions : context -> solver -> ast_vector
	= "camlidl_z3_Z3_solver_get_assertions"

external solver_get_units : context -> solver -> ast_vector
	= "camlidl_z3_Z3_solver_get_units"

external solver_get_trail : context -> solver -> ast_vector
	= "camlidl_z3_Z3_solver_get_trail"

external solver_get_non_units : context -> solver -> ast_vector
	= "camlidl_z3_Z3_solver_get_non_units"

external solver_get_levels : context -> solver -> ast_vector -> int -> int array
	= "camlidl_z3_Z3_solver_get_levels"

external solver_congruence_root : context -> solver -> ast -> ast
	= "camlidl_z3_Z3_solver_congruence_root"

external solver_congruence_next : context -> solver -> ast -> ast
	= "camlidl_z3_Z3_solver_congruence_next"

external solver_congruence_explain : context -> solver -> ast -> ast -> ast
	= "camlidl_z3_Z3_solver_congruence_explain"

external solver_solve_for : context -> solver -> ast_vector -> ast_vector -> ast_vector -> unit
	= "camlidl_z3_Z3_solver_solve_for"

external solver_next_split : context -> solver_callback -> ast -> int -> lbool -> bool
	= "camlidl_z3_Z3_solver_next_split"

external solver_propagate_declare : context -> symbol -> sort array -> sort -> func_decl
	= "camlidl_z3_Z3_solver_propagate_declare"

external solver_propagate_register : context -> solver -> ast -> unit
	= "camlidl_z3_Z3_solver_propagate_register"

external solver_propagate_register_cb : context -> solver_callback -> ast -> unit
	= "camlidl_z3_Z3_solver_propagate_register_cb"

external solver_propagate_consequence : context -> solver_callback -> ast array -> ast array -> ast array -> ast -> bool
	= "camlidl_z3_Z3_solver_propagate_consequence_bytecode" "camlidl_z3_Z3_solver_propagate_consequence"

external solver_set_initial_value : context -> solver -> ast -> ast -> unit
	= "camlidl_z3_Z3_solver_set_initial_value"

external solver_check : context -> solver -> lbool
	= "camlidl_z3_Z3_solver_check"

external solver_check_assumptions : context -> solver -> ast array -> lbool
	= "camlidl_z3_Z3_solver_check_assumptions"

external get_implied_equalities : context -> solver -> ast array -> lbool * int array
	= "camlidl_z3_Z3_get_implied_equalities"

external solver_get_consequences : context -> solver -> ast_vector -> ast_vector -> ast_vector -> lbool
	= "camlidl_z3_Z3_solver_get_consequences"

external solver_cube : context -> solver -> ast_vector -> int -> ast_vector
	= "camlidl_z3_Z3_solver_cube"

external solver_get_model : context -> solver -> model
	= "camlidl_z3_Z3_solver_get_model"

external solver_get_proof : context -> solver -> ast
	= "camlidl_z3_Z3_solver_get_proof"

external solver_get_unsat_core : context -> solver -> ast_vector
	= "camlidl_z3_Z3_solver_get_unsat_core"

external solver_get_reason_unknown : context -> solver -> string
	= "camlidl_z3_Z3_solver_get_reason_unknown"

external solver_get_statistics : context -> solver -> stats
	= "camlidl_z3_Z3_solver_get_statistics"

external solver_to_string : context -> solver -> string
	= "camlidl_z3_Z3_solver_to_string"

external solver_to_dimacs_string : context -> solver -> bool -> string
	= "camlidl_z3_Z3_solver_to_dimacs_string"

external stats_to_string : context -> stats -> string
	= "camlidl_z3_Z3_stats_to_string"

external stats_size : context -> stats -> int
	= "camlidl_z3_Z3_stats_size"

external stats_get_key : context -> stats -> int -> string
	= "camlidl_z3_Z3_stats_get_key"

external stats_is_uint : context -> stats -> int -> bool
	= "camlidl_z3_Z3_stats_is_uint"

external stats_is_double : context -> stats -> int -> bool
	= "camlidl_z3_Z3_stats_is_double"

external stats_get_uint_value : context -> stats -> int -> int
	= "camlidl_z3_Z3_stats_get_uint_value"

external stats_get_double_value : context -> stats -> int -> float
	= "camlidl_z3_Z3_stats_get_double_value"

external get_estimated_alloc_size : unit -> int64
	= "camlidl_z3_Z3_get_estimated_alloc_size"

external mk_ast_vector : context -> ast_vector
	= "camlidl_z3_Z3_mk_ast_vector"

external ast_vector_size : context -> ast_vector -> int
	= "camlidl_z3_Z3_ast_vector_size"

external ast_vector_get : context -> ast_vector -> int -> ast
	= "camlidl_z3_Z3_ast_vector_get"

external ast_vector_set : context -> ast_vector -> int -> ast -> unit
	= "camlidl_z3_Z3_ast_vector_set"

external ast_vector_resize : context -> ast_vector -> int -> unit
	= "camlidl_z3_Z3_ast_vector_resize"

external ast_vector_push : context -> ast_vector -> ast -> unit
	= "camlidl_z3_Z3_ast_vector_push"

external ast_vector_translate : context -> ast_vector -> context -> ast_vector
	= "camlidl_z3_Z3_ast_vector_translate"

external ast_vector_to_string : context -> ast_vector -> string
	= "camlidl_z3_Z3_ast_vector_to_string"

external mk_ast_map : context -> ast_map
	= "camlidl_z3_Z3_mk_ast_map"

external ast_map_contains : context -> ast_map -> ast -> bool
	= "camlidl_z3_Z3_ast_map_contains"

external ast_map_find : context -> ast_map -> ast -> ast
	= "camlidl_z3_Z3_ast_map_find"

external ast_map_insert : context -> ast_map -> ast -> ast -> unit
	= "camlidl_z3_Z3_ast_map_insert"

external ast_map_erase : context -> ast_map -> ast -> unit
	= "camlidl_z3_Z3_ast_map_erase"

external ast_map_reset : context -> ast_map -> unit
	= "camlidl_z3_Z3_ast_map_reset"

external ast_map_size : context -> ast_map -> int
	= "camlidl_z3_Z3_ast_map_size"

external ast_map_keys : context -> ast_map -> ast_vector
	= "camlidl_z3_Z3_ast_map_keys"

external ast_map_to_string : context -> ast_map -> string
	= "camlidl_z3_Z3_ast_map_to_string"

external algebraic_is_value : context -> ast -> bool
	= "camlidl_z3_Z3_algebraic_is_value"

external algebraic_is_pos : context -> ast -> bool
	= "camlidl_z3_Z3_algebraic_is_pos"

external algebraic_is_neg : context -> ast -> bool
	= "camlidl_z3_Z3_algebraic_is_neg"

external algebraic_is_zero : context -> ast -> bool
	= "camlidl_z3_Z3_algebraic_is_zero"

external algebraic_sign : context -> ast -> int
	= "camlidl_z3_Z3_algebraic_sign"

external algebraic_add : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_algebraic_add"

external algebraic_sub : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_algebraic_sub"

external algebraic_mul : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_algebraic_mul"

external algebraic_div : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_algebraic_div"

external algebraic_root : context -> ast -> int -> ast
	= "camlidl_z3_Z3_algebraic_root"

external algebraic_power : context -> ast -> int -> ast
	= "camlidl_z3_Z3_algebraic_power"

external algebraic_lt : context -> ast -> ast -> bool
	= "camlidl_z3_Z3_algebraic_lt"

external algebraic_gt : context -> ast -> ast -> bool
	= "camlidl_z3_Z3_algebraic_gt"

external algebraic_le : context -> ast -> ast -> bool
	= "camlidl_z3_Z3_algebraic_le"

external algebraic_ge : context -> ast -> ast -> bool
	= "camlidl_z3_Z3_algebraic_ge"

external algebraic_eq : context -> ast -> ast -> bool
	= "camlidl_z3_Z3_algebraic_eq"

external algebraic_neq : context -> ast -> ast -> bool
	= "camlidl_z3_Z3_algebraic_neq"

external algebraic_roots : context -> ast -> ast array -> ast_vector
	= "camlidl_z3_Z3_algebraic_roots"

external algebraic_eval : context -> ast -> ast array -> int
	= "camlidl_z3_Z3_algebraic_eval"

external algebraic_get_poly : context -> ast -> ast_vector
	= "camlidl_z3_Z3_algebraic_get_poly"

external algebraic_get_i : context -> ast -> int
	= "camlidl_z3_Z3_algebraic_get_i"

external polynomial_subresultants : context -> ast -> ast -> ast -> ast_vector
	= "camlidl_z3_Z3_polynomial_subresultants"

external rcf_mk_rational : context -> string -> rcf_num
	= "camlidl_z3_Z3_rcf_mk_rational"

external rcf_mk_small_int : context -> int -> rcf_num
	= "camlidl_z3_Z3_rcf_mk_small_int"

external rcf_mk_pi : context -> rcf_num
	= "camlidl_z3_Z3_rcf_mk_pi"

external rcf_mk_e : context -> rcf_num
	= "camlidl_z3_Z3_rcf_mk_e"

external rcf_mk_infinitesimal : context -> rcf_num
	= "camlidl_z3_Z3_rcf_mk_infinitesimal"

external rcf_add : context -> rcf_num -> rcf_num -> rcf_num
	= "camlidl_z3_Z3_rcf_add"

external rcf_sub : context -> rcf_num -> rcf_num -> rcf_num
	= "camlidl_z3_Z3_rcf_sub"

external rcf_mul : context -> rcf_num -> rcf_num -> rcf_num
	= "camlidl_z3_Z3_rcf_mul"

external rcf_div : context -> rcf_num -> rcf_num -> rcf_num
	= "camlidl_z3_Z3_rcf_div"

external rcf_neg : context -> rcf_num -> rcf_num
	= "camlidl_z3_Z3_rcf_neg"

external rcf_inv : context -> rcf_num -> rcf_num
	= "camlidl_z3_Z3_rcf_inv"

external rcf_power : context -> rcf_num -> int -> rcf_num
	= "camlidl_z3_Z3_rcf_power"

external rcf_lt : context -> rcf_num -> rcf_num -> bool
	= "camlidl_z3_Z3_rcf_lt"

external rcf_gt : context -> rcf_num -> rcf_num -> bool
	= "camlidl_z3_Z3_rcf_gt"

external rcf_le : context -> rcf_num -> rcf_num -> bool
	= "camlidl_z3_Z3_rcf_le"

external rcf_ge : context -> rcf_num -> rcf_num -> bool
	= "camlidl_z3_Z3_rcf_ge"

external rcf_eq : context -> rcf_num -> rcf_num -> bool
	= "camlidl_z3_Z3_rcf_eq"

external rcf_neq : context -> rcf_num -> rcf_num -> bool
	= "camlidl_z3_Z3_rcf_neq"

external rcf_num_to_string : context -> rcf_num -> bool -> bool -> string
	= "camlidl_z3_Z3_rcf_num_to_string"

external rcf_num_to_decimal_string : context -> rcf_num -> int -> string
	= "camlidl_z3_Z3_rcf_num_to_decimal_string"

external rcf_get_numerator_denominator : context -> rcf_num -> rcf_num * rcf_num
	= "camlidl_z3_Z3_rcf_get_numerator_denominator"

external rcf_is_rational : context -> rcf_num -> bool
	= "camlidl_z3_Z3_rcf_is_rational"

external rcf_is_algebraic : context -> rcf_num -> bool
	= "camlidl_z3_Z3_rcf_is_algebraic"

external rcf_is_infinitesimal : context -> rcf_num -> bool
	= "camlidl_z3_Z3_rcf_is_infinitesimal"

external rcf_is_transcendental : context -> rcf_num -> bool
	= "camlidl_z3_Z3_rcf_is_transcendental"

external rcf_extension_index : context -> rcf_num -> int
	= "camlidl_z3_Z3_rcf_extension_index"

external rcf_transcendental_name : context -> rcf_num -> symbol
	= "camlidl_z3_Z3_rcf_transcendental_name"

external rcf_infinitesimal_name : context -> rcf_num -> symbol
	= "camlidl_z3_Z3_rcf_infinitesimal_name"

external rcf_num_coefficients : context -> rcf_num -> int
	= "camlidl_z3_Z3_rcf_num_coefficients"

external rcf_coefficient : context -> rcf_num -> int -> rcf_num
	= "camlidl_z3_Z3_rcf_coefficient"

external rcf_interval : context -> rcf_num -> int * bool * bool * rcf_num_opt * bool * bool * rcf_num_opt
	= "camlidl_z3_Z3_rcf_interval"

external rcf_num_sign_conditions : context -> rcf_num -> int
	= "camlidl_z3_Z3_rcf_num_sign_conditions"

external rcf_sign_condition_sign : context -> rcf_num -> int -> int
	= "camlidl_z3_Z3_rcf_sign_condition_sign"

external rcf_num_sign_condition_coefficients : context -> rcf_num -> int -> int
	= "camlidl_z3_Z3_rcf_num_sign_condition_coefficients"

external rcf_sign_condition_coefficient : context -> rcf_num -> int -> int -> rcf_num
	= "camlidl_z3_Z3_rcf_sign_condition_coefficient"

external mk_fixedpoint : context -> fixedpoint
	= "camlidl_z3_Z3_mk_fixedpoint"

external fixedpoint_add_rule : context -> fixedpoint -> ast -> symbol -> unit
	= "camlidl_z3_Z3_fixedpoint_add_rule"

external fixedpoint_add_fact : context -> fixedpoint -> func_decl -> int array -> unit
	= "camlidl_z3_Z3_fixedpoint_add_fact"

external fixedpoint_assert : context -> fixedpoint -> ast -> unit
	= "camlidl_z3_Z3_fixedpoint_assert"

external fixedpoint_query : context -> fixedpoint -> ast -> lbool
	= "camlidl_z3_Z3_fixedpoint_query"

external fixedpoint_query_relations : context -> fixedpoint -> func_decl array -> lbool
	= "camlidl_z3_Z3_fixedpoint_query_relations"

external fixedpoint_get_answer : context -> fixedpoint -> ast
	= "camlidl_z3_Z3_fixedpoint_get_answer"

external fixedpoint_get_reason_unknown : context -> fixedpoint -> string
	= "camlidl_z3_Z3_fixedpoint_get_reason_unknown"

external fixedpoint_update_rule : context -> fixedpoint -> ast -> symbol -> unit
	= "camlidl_z3_Z3_fixedpoint_update_rule"

external fixedpoint_get_num_levels : context -> fixedpoint -> func_decl -> int
	= "camlidl_z3_Z3_fixedpoint_get_num_levels"

external fixedpoint_get_cover_delta : context -> fixedpoint -> int -> func_decl -> ast
	= "camlidl_z3_Z3_fixedpoint_get_cover_delta"

external fixedpoint_add_cover : context -> fixedpoint -> int -> func_decl -> ast -> unit
	= "camlidl_z3_Z3_fixedpoint_add_cover"

external fixedpoint_get_statistics : context -> fixedpoint -> stats
	= "camlidl_z3_Z3_fixedpoint_get_statistics"

external fixedpoint_register_relation : context -> fixedpoint -> func_decl -> unit
	= "camlidl_z3_Z3_fixedpoint_register_relation"

external fixedpoint_set_predicate_representation : context -> fixedpoint -> func_decl -> symbol array -> unit
	= "camlidl_z3_Z3_fixedpoint_set_predicate_representation"

external fixedpoint_get_rules : context -> fixedpoint -> ast_vector
	= "camlidl_z3_Z3_fixedpoint_get_rules"

external fixedpoint_get_assertions : context -> fixedpoint -> ast_vector
	= "camlidl_z3_Z3_fixedpoint_get_assertions"

external fixedpoint_set_params : context -> fixedpoint -> params -> unit
	= "camlidl_z3_Z3_fixedpoint_set_params"

external fixedpoint_get_help : context -> fixedpoint -> string
	= "camlidl_z3_Z3_fixedpoint_get_help"

external fixedpoint_get_param_descrs : context -> fixedpoint -> param_descrs
	= "camlidl_z3_Z3_fixedpoint_get_param_descrs"

external fixedpoint_to_string : context -> fixedpoint -> ast array -> string
	= "camlidl_z3_Z3_fixedpoint_to_string"

external fixedpoint_from_string : context -> fixedpoint -> string -> ast_vector
	= "camlidl_z3_Z3_fixedpoint_from_string"

external fixedpoint_from_file : context -> fixedpoint -> string -> ast_vector
	= "camlidl_z3_Z3_fixedpoint_from_file"

external mk_optimize : context -> optimize
	= "camlidl_z3_Z3_mk_optimize"

external optimize_assert : context -> optimize -> ast -> unit
	= "camlidl_z3_Z3_optimize_assert"

external optimize_assert_and_track : context -> optimize -> ast -> ast -> unit
	= "camlidl_z3_Z3_optimize_assert_and_track"

external optimize_assert_soft : context -> optimize -> ast -> string -> symbol_opt -> int
	= "camlidl_z3_Z3_optimize_assert_soft"

external optimize_maximize : context -> optimize -> ast -> int
	= "camlidl_z3_Z3_optimize_maximize"

external optimize_minimize : context -> optimize -> ast -> int
	= "camlidl_z3_Z3_optimize_minimize"

external optimize_push : context -> optimize -> unit
	= "camlidl_z3_Z3_optimize_push"

external optimize_pop : context -> optimize -> unit
	= "camlidl_z3_Z3_optimize_pop"

external optimize_set_initial_value : context -> optimize -> ast -> ast -> unit
	= "camlidl_z3_Z3_optimize_set_initial_value"

external optimize_check : context -> optimize -> ast array -> lbool
	= "camlidl_z3_Z3_optimize_check"

external optimize_get_reason_unknown : context -> optimize -> string
	= "camlidl_z3_Z3_optimize_get_reason_unknown"

external optimize_get_model : context -> optimize -> model
	= "camlidl_z3_Z3_optimize_get_model"

external optimize_get_unsat_core : context -> optimize -> ast_vector
	= "camlidl_z3_Z3_optimize_get_unsat_core"

external optimize_set_params : context -> optimize -> params -> unit
	= "camlidl_z3_Z3_optimize_set_params"

external optimize_get_param_descrs : context -> optimize -> param_descrs
	= "camlidl_z3_Z3_optimize_get_param_descrs"

external optimize_get_lower : context -> optimize -> int -> ast
	= "camlidl_z3_Z3_optimize_get_lower"

external optimize_get_upper : context -> optimize -> int -> ast
	= "camlidl_z3_Z3_optimize_get_upper"

external optimize_get_lower_as_vector : context -> optimize -> int -> ast_vector
	= "camlidl_z3_Z3_optimize_get_lower_as_vector"

external optimize_get_upper_as_vector : context -> optimize -> int -> ast_vector
	= "camlidl_z3_Z3_optimize_get_upper_as_vector"

external optimize_to_string : context -> optimize -> string
	= "camlidl_z3_Z3_optimize_to_string"

external optimize_from_string : context -> optimize -> string -> unit
	= "camlidl_z3_Z3_optimize_from_string"

external optimize_from_file : context -> optimize -> string -> unit
	= "camlidl_z3_Z3_optimize_from_file"

external optimize_get_help : context -> optimize -> string
	= "camlidl_z3_Z3_optimize_get_help"

external optimize_get_statistics : context -> optimize -> stats
	= "camlidl_z3_Z3_optimize_get_statistics"

external optimize_get_assertions : context -> optimize -> ast_vector
	= "camlidl_z3_Z3_optimize_get_assertions"

external optimize_get_objectives : context -> optimize -> ast_vector
	= "camlidl_z3_Z3_optimize_get_objectives"

external optimize_translate : context -> optimize -> context -> optimize
	= "camlidl_z3_Z3_optimize_translate"

external mk_fpa_rounding_mode_sort : context -> sort
	= "camlidl_z3_Z3_mk_fpa_rounding_mode_sort"

external mk_fpa_round_nearest_ties_to_even : context -> ast
	= "camlidl_z3_Z3_mk_fpa_round_nearest_ties_to_even"

external mk_fpa_rne : context -> ast
	= "camlidl_z3_Z3_mk_fpa_rne"

external mk_fpa_round_nearest_ties_to_away : context -> ast
	= "camlidl_z3_Z3_mk_fpa_round_nearest_ties_to_away"

external mk_fpa_rna : context -> ast
	= "camlidl_z3_Z3_mk_fpa_rna"

external mk_fpa_round_toward_positive : context -> ast
	= "camlidl_z3_Z3_mk_fpa_round_toward_positive"

external mk_fpa_rtp : context -> ast
	= "camlidl_z3_Z3_mk_fpa_rtp"

external mk_fpa_round_toward_negative : context -> ast
	= "camlidl_z3_Z3_mk_fpa_round_toward_negative"

external mk_fpa_rtn : context -> ast
	= "camlidl_z3_Z3_mk_fpa_rtn"

external mk_fpa_round_toward_zero : context -> ast
	= "camlidl_z3_Z3_mk_fpa_round_toward_zero"

external mk_fpa_rtz : context -> ast
	= "camlidl_z3_Z3_mk_fpa_rtz"

external mk_fpa_sort : context -> int -> int -> sort
	= "camlidl_z3_Z3_mk_fpa_sort"

external mk_fpa_sort_half : context -> sort
	= "camlidl_z3_Z3_mk_fpa_sort_half"

external mk_fpa_sort_16 : context -> sort
	= "camlidl_z3_Z3_mk_fpa_sort_16"

external mk_fpa_sort_single : context -> sort
	= "camlidl_z3_Z3_mk_fpa_sort_single"

external mk_fpa_sort_32 : context -> sort
	= "camlidl_z3_Z3_mk_fpa_sort_32"

external mk_fpa_sort_double : context -> sort
	= "camlidl_z3_Z3_mk_fpa_sort_double"

external mk_fpa_sort_64 : context -> sort
	= "camlidl_z3_Z3_mk_fpa_sort_64"

external mk_fpa_sort_quadruple : context -> sort
	= "camlidl_z3_Z3_mk_fpa_sort_quadruple"

external mk_fpa_sort_128 : context -> sort
	= "camlidl_z3_Z3_mk_fpa_sort_128"

external mk_fpa_nan : context -> sort -> ast
	= "camlidl_z3_Z3_mk_fpa_nan"

external mk_fpa_inf : context -> sort -> bool -> ast
	= "camlidl_z3_Z3_mk_fpa_inf"

external mk_fpa_zero : context -> sort -> bool -> ast
	= "camlidl_z3_Z3_mk_fpa_zero"

external mk_fpa_fp : context -> ast -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_fp"

external mk_fpa_numeral_float : context -> float -> sort -> ast
	= "camlidl_z3_Z3_mk_fpa_numeral_float"

external mk_fpa_numeral_double : context -> float -> sort -> ast
	= "camlidl_z3_Z3_mk_fpa_numeral_double"

external mk_fpa_numeral_int : context -> int -> sort -> ast
	= "camlidl_z3_Z3_mk_fpa_numeral_int"

external mk_fpa_numeral_int_uint : context -> bool -> int -> int -> sort -> ast
	= "camlidl_z3_Z3_mk_fpa_numeral_int_uint"

external mk_fpa_numeral_int64_uint64 : context -> bool -> int64 -> int64 -> sort -> ast
	= "camlidl_z3_Z3_mk_fpa_numeral_int64_uint64"

external mk_fpa_abs : context -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_abs"

external mk_fpa_neg : context -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_neg"

external mk_fpa_add : context -> ast -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_add"

external mk_fpa_sub : context -> ast -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_sub"

external mk_fpa_mul : context -> ast -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_mul"

external mk_fpa_div : context -> ast -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_div"

external mk_fpa_fma : context -> ast -> ast -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_fma"

external mk_fpa_sqrt : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_sqrt"

external mk_fpa_rem : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_rem"

external mk_fpa_round_to_integral : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_round_to_integral"

external mk_fpa_min : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_min"

external mk_fpa_max : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_max"

external mk_fpa_leq : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_leq"

external mk_fpa_lt : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_lt"

external mk_fpa_geq : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_geq"

external mk_fpa_gt : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_gt"

external mk_fpa_eq : context -> ast -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_eq"

external mk_fpa_is_normal : context -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_is_normal"

external mk_fpa_is_subnormal : context -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_is_subnormal"

external mk_fpa_is_zero : context -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_is_zero"

external mk_fpa_is_infinite : context -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_is_infinite"

external mk_fpa_is_nan : context -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_is_nan"

external mk_fpa_is_negative : context -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_is_negative"

external mk_fpa_is_positive : context -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_is_positive"

external mk_fpa_to_fp_bv : context -> ast -> sort -> ast
	= "camlidl_z3_Z3_mk_fpa_to_fp_bv"

external mk_fpa_to_fp_float : context -> ast -> ast -> sort -> ast
	= "camlidl_z3_Z3_mk_fpa_to_fp_float"

external mk_fpa_to_fp_real : context -> ast -> ast -> sort -> ast
	= "camlidl_z3_Z3_mk_fpa_to_fp_real"

external mk_fpa_to_fp_signed : context -> ast -> ast -> sort -> ast
	= "camlidl_z3_Z3_mk_fpa_to_fp_signed"

external mk_fpa_to_fp_unsigned : context -> ast -> ast -> sort -> ast
	= "camlidl_z3_Z3_mk_fpa_to_fp_unsigned"

external mk_fpa_to_ubv : context -> ast -> ast -> int -> ast
	= "camlidl_z3_Z3_mk_fpa_to_ubv"

external mk_fpa_to_sbv : context -> ast -> ast -> int -> ast
	= "camlidl_z3_Z3_mk_fpa_to_sbv"

external mk_fpa_to_real : context -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_to_real"

external fpa_get_ebits : context -> sort -> int
	= "camlidl_z3_Z3_fpa_get_ebits"

external fpa_get_sbits : context -> sort -> int
	= "camlidl_z3_Z3_fpa_get_sbits"

external fpa_is_numeral : context -> ast -> bool
	= "camlidl_z3_Z3_fpa_is_numeral"

external fpa_is_numeral_nan : context -> ast -> bool
	= "camlidl_z3_Z3_fpa_is_numeral_nan"

external fpa_is_numeral_inf : context -> ast -> bool
	= "camlidl_z3_Z3_fpa_is_numeral_inf"

external fpa_is_numeral_zero : context -> ast -> bool
	= "camlidl_z3_Z3_fpa_is_numeral_zero"

external fpa_is_numeral_normal : context -> ast -> bool
	= "camlidl_z3_Z3_fpa_is_numeral_normal"

external fpa_is_numeral_subnormal : context -> ast -> bool
	= "camlidl_z3_Z3_fpa_is_numeral_subnormal"

external fpa_is_numeral_positive : context -> ast -> bool
	= "camlidl_z3_Z3_fpa_is_numeral_positive"

external fpa_is_numeral_negative : context -> ast -> bool
	= "camlidl_z3_Z3_fpa_is_numeral_negative"

external fpa_get_numeral_sign_bv : context -> ast -> ast
	= "camlidl_z3_Z3_fpa_get_numeral_sign_bv"

external fpa_get_numeral_significand_bv : context -> ast -> ast
	= "camlidl_z3_Z3_fpa_get_numeral_significand_bv"

external fpa_get_numeral_sign : context -> ast -> bool
	= "camlidl_z3_Z3_fpa_get_numeral_sign"

external fpa_get_numeral_significand_string : context -> ast -> string
	= "camlidl_z3_Z3_fpa_get_numeral_significand_string"

external fpa_get_numeral_significand_uint64 : context -> ast -> int64
	= "camlidl_z3_Z3_fpa_get_numeral_significand_uint64"

external fpa_get_numeral_exponent_string : context -> ast -> bool -> string
	= "camlidl_z3_Z3_fpa_get_numeral_exponent_string"

external fpa_get_numeral_exponent_int64 : context -> ast -> bool -> int64
	= "camlidl_z3_Z3_fpa_get_numeral_exponent_int64"

external fpa_get_numeral_exponent_bv : context -> ast -> bool -> ast
	= "camlidl_z3_Z3_fpa_get_numeral_exponent_bv"

external mk_fpa_to_ieee_bv : context -> ast -> ast
	= "camlidl_z3_Z3_mk_fpa_to_ieee_bv"

external mk_fpa_to_fp_int_real : context -> ast -> ast -> ast -> sort -> ast
	= "camlidl_z3_Z3_mk_fpa_to_fp_int_real"

external fixedpoint_query_from_lvl : context -> fixedpoint -> ast -> int -> lbool
	= "camlidl_z3_Z3_fixedpoint_query_from_lvl"

external fixedpoint_get_ground_sat_answer : context -> fixedpoint -> ast
	= "camlidl_z3_Z3_fixedpoint_get_ground_sat_answer"

external fixedpoint_get_rules_along_trace : context -> fixedpoint -> ast_vector
	= "camlidl_z3_Z3_fixedpoint_get_rules_along_trace"

external fixedpoint_get_rule_names_along_trace : context -> fixedpoint -> symbol
	= "camlidl_z3_Z3_fixedpoint_get_rule_names_along_trace"

external fixedpoint_add_invariant : context -> fixedpoint -> func_decl -> ast -> unit
	= "camlidl_z3_Z3_fixedpoint_add_invariant"

external fixedpoint_get_reachable : context -> fixedpoint -> func_decl -> ast
	= "camlidl_z3_Z3_fixedpoint_get_reachable"

external qe_model_project : context -> model -> app array -> ast -> ast
	= "camlidl_z3_Z3_qe_model_project"

external qe_model_project_skolem : context -> model -> app array -> ast -> ast_map -> ast
	= "camlidl_z3_Z3_qe_model_project_skolem"

external qe_model_project_with_witness : context -> model -> app array -> ast -> ast_map -> ast
	= "camlidl_z3_Z3_qe_model_project_with_witness"

external model_extrapolate : context -> model -> ast -> ast
	= "camlidl_z3_Z3_model_extrapolate"

external qe_lite : context -> ast_vector -> ast -> ast
	= "camlidl_z3_Z3_qe_lite"

external get_lstring : context -> ast -> char array
	= "camlidl_z3_Z3_get_lstring"

external rcf_mk_roots : context -> rcf_num array -> rcf_num array
	= "camlidl_z3_Z3_rcf_mk_roots"


(** Raised when Z3 detects an error. [Fatal] exceptions are fatal: Z3 may be
    left in an inconsistent internal state. [Fatal] exceptions should not be
    caught except to perform minimal cleanup and exit. It is NOT safe to call
    any Z3 function after a [Fatal] exception has been raised. *)
exception Fatal of string
  [@warn_on_literal_pattern]


let () = Callback.register_exception "Z3.Fatal" (Fatal "")

external mk_context_rc : config -> context
	= "camlidl_z3_Z3_mk_context_rc"


let mk_context key_val_list =
  let cfg = mk_config() in
  List.iter (fun (k,v) -> set_param_value cfg k v) key_val_list ;
  let ctx = mk_context_rc cfg in
  del_config cfg ;
  ctx


let solver_get_levels ctx slv lits =
  solver_get_levels ctx slv lits (ast_vector_size ctx lits)


let mk_lstring ctx str = mk_lstring ctx (String.length str) str


(** A constructor of a datatype is described by: *)
type constructor_desc =
  { constructor_desc: symbol  (** Name of constructor function *)
  ; recognizer_desc: symbol  (** Name of recognizer function *)
  ; accessor_descs: (symbol * sort) array
        (** Names and sorts of fields / accessor functions *) }


module Array = struct
  include Array

  let init n ~f = init n f
  let iter xs ~f = iter f xs
  let map xs ~f = map f xs
  let mapi xs ~f = mapi f xs

  let find_mapi xs ~f =
    let rec loop f xs i =
      if i >= Array.length xs then None
      else
        match f i xs.(i) with
        | Some _ as x' -> x'
        | None -> loop f xs (i + 1)
    in
    loop f xs 0
end

let mk_polymorphic_datatype ctx param_names body =
  let params = Array.map ~f:(mk_type_variable ctx) param_names in
  (* uninterpreted "placeholder" sort to track where the recursive datatype
     sort ends up in the constructor_descs *)
  let placeholder_sort =
    mk_uninterpreted_sort ctx
      (get_decl_name ctx
         (mk_fresh_func_decl ctx "" [||] (mk_bool_sort ctx)) )
  in
  let name, ctor_descs = body params placeholder_sort in
  let ctors =
    Array.map ctor_descs
      ~f:(fun {constructor_desc; recognizer_desc; accessor_descs} ->
        let field_names = Array.map ~f:fst accessor_descs in
        let sort_refs = Array.make (Array.length accessor_descs) (-1) in
        let field_sorts =
          Array.mapi accessor_descs ~f:(fun i (_, sort_i) ->
              (* mk_constructor receives the recursive occurrences of the
                 datatype sort being defined separately from the other field
                 sorts. So if the sort of a field is the placeholder sort,
                 then record its index (0) in sort_refs and indicate the
                 field's sort is recursive using None. *)
              if is_eq_sort ctx sort_i placeholder_sort then (
                sort_refs.(i) <- 0 ;
                None )
              else Some sort_i )
        in
        mk_constructor ctx constructor_desc recognizer_desc field_names
          field_sorts sort_refs )
  in
  let _poly_sort = mk_polymorphic_datatype ctx name params ctors in
  Array.iter ~f:(del_constructor ctx) ctors ;
  fun param_sorts -> mk_datatype_sort ctx name param_sorts

let mk_datatype ctx body =
  mk_polymorphic_datatype ctx [||] (fun _ -> body) [||]

let mk_datatypes ctx bodies =
  (* uninterpreted "placeholder" sorts to track where the recursive datatype
     sorts end up in the constructor_descs *)
  let placeholder_sorts =
    Array.init (Array.length bodies) ~f:(fun _ ->
        mk_uninterpreted_sort ctx
          (get_decl_name ctx
             (mk_fresh_func_decl ctx "" [||] (mk_bool_sort ctx)) ) )
  in
  let dt_descs = Array.map ~f:(fun body -> body placeholder_sorts) bodies in
  let names = Array.map ~f:fst dt_descs in
  let ctorss =
    Array.map dt_descs ~f:(fun (_, ctor_descs) ->
        Array.map ctor_descs
          ~f:(fun {constructor_desc; recognizer_desc; accessor_descs} ->
            let field_names = Array.map ~f:fst accessor_descs in
            let sort_refs = Array.make (Array.length accessor_descs) (-1) in
            let field_sorts =
              Array.mapi accessor_descs ~f:(fun i (_, sort_i) ->
                  (* mk_constructor needs the recursive occurrences of the
                     datatype sorts being defined to be passed separately
                     from the other field sorts. So if the sort of a field
                     is one of the placeholder sorts, then record its index
                     in sort_refs and indicate the field's sort is recursive
                     using None. *)
                  match
                    Array.find_mapi placeholder_sorts ~f:(fun j sort0_j ->
                        if is_eq_sort ctx sort_i sort0_j then Some j
                        else None )
                  with
                  | Some j ->
                      sort_refs.(i) <- j ;
                      None
                  | None -> Some sort_i )
            in
            mk_constructor ctx constructor_desc recognizer_desc field_names
              field_sorts sort_refs ) )
  in
  let constructor_lists = Array.map ~f:(mk_constructor_list ctx) ctorss in
  let sorts = mk_datatypes ctx names constructor_lists in
  Array.iter ~f:(del_constructor_list ctx) constructor_lists ;
  Array.iter ~f:(Array.iter ~f:(del_constructor ctx)) ctorss ;
  sorts


external solver_propagate_init :
     push:(context -> solver_callback -> 'state -> unit)
  -> pop:(context -> solver_callback -> 'state -> int -> unit)
  -> fresh:(context -> 'state -> new_context:context -> 'state)
  -> ?fixed:
       (   context
        -> solver_callback
        -> 'state
        -> expr:ast
        -> value:ast
        -> unit )
  -> ?final:(context -> solver_callback -> 'state -> unit)
  -> ?eq:(context -> solver_callback -> 'state -> ast -> ast -> unit)
  -> ?diseq:(context -> solver_callback -> 'state -> ast -> ast -> unit)
  -> ?created:(context -> solver_callback -> 'state -> ast -> unit)
  -> ?decide:
       (context -> solver_callback -> 'state -> ast -> int -> bool -> unit)
  -> ?on_binding:
       (context -> solver_callback -> 'state -> ast -> ast -> bool)
  -> context
  -> solver
  -> 'state
  -> unit
  = "camlidl_z3_Z3_solver_propagate_init_bytecode" "camlidl_z3_Z3_solver_propagate_init"
(** Note that the bindings ensure callbacks are called with the correct
    [context]s, but [fresh] still receives both old and new [context]s in
    case the propagator-specific ['state] contains some [Z3] objects, which
    will need to be recreated in the new context, perhaps using
    [Z3.translate]. *)