module Z3::LowLevel

# File lib/z3/low_level_auto.rb, line 4
def add_const_interp(model, func_decl, ast) #=> :void
  VeryLowLevel.Z3_add_const_interp(_ctx_pointer, model._model, func_decl._ast, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 8
def add_func_interp(model, func_decl, ast) #=> :func_interp_pointer
  VeryLowLevel.Z3_add_func_interp(_ctx_pointer, model._model, func_decl._ast, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 12
def algebraic_add(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_algebraic_add(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 16
def algebraic_div(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_algebraic_div(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 20
def algebraic_eq(ast1, ast2) #=> :bool
  VeryLowLevel.Z3_algebraic_eq(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 24
def algebraic_ge(ast1, ast2) #=> :bool
  VeryLowLevel.Z3_algebraic_ge(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 28
def algebraic_get_i(ast) #=> :uint
  VeryLowLevel.Z3_algebraic_get_i(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 32
def algebraic_get_poly(ast) #=> :ast_vector_pointer
  VeryLowLevel.Z3_algebraic_get_poly(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 36
def algebraic_gt(ast1, ast2) #=> :bool
  VeryLowLevel.Z3_algebraic_gt(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 40
def algebraic_is_neg(ast) #=> :bool
  VeryLowLevel.Z3_algebraic_is_neg(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 44
def algebraic_is_pos(ast) #=> :bool
  VeryLowLevel.Z3_algebraic_is_pos(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 48
def algebraic_is_value(ast) #=> :bool
  VeryLowLevel.Z3_algebraic_is_value(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 52
def algebraic_is_zero(ast) #=> :bool
  VeryLowLevel.Z3_algebraic_is_zero(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 56
def algebraic_le(ast1, ast2) #=> :bool
  VeryLowLevel.Z3_algebraic_le(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 60
def algebraic_lt(ast1, ast2) #=> :bool
  VeryLowLevel.Z3_algebraic_lt(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 64
def algebraic_mul(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_algebraic_mul(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 68
def algebraic_neq(ast1, ast2) #=> :bool
  VeryLowLevel.Z3_algebraic_neq(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 72
def algebraic_power(ast, num) #=> :ast_pointer
  VeryLowLevel.Z3_algebraic_power(_ctx_pointer, ast._ast, num)
end

# File lib/z3/low_level_auto.rb, line 76
def algebraic_root(ast, num) #=> :ast_pointer
  VeryLowLevel.Z3_algebraic_root(_ctx_pointer, ast._ast, num)
end

# File lib/z3/low_level_auto.rb, line 80
def algebraic_sign(ast) #=> :int
  VeryLowLevel.Z3_algebraic_sign(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 84
def algebraic_sub(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_algebraic_sub(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 88
def apply_result_dec_ref(apply_result) #=> :void
  VeryLowLevel.Z3_apply_result_dec_ref(_ctx_pointer, apply_result._apply_result)
end

# File lib/z3/low_level_auto.rb, line 92
def apply_result_get_num_subgoals(apply_result) #=> :uint
  VeryLowLevel.Z3_apply_result_get_num_subgoals(_ctx_pointer, apply_result._apply_result)
end

# File lib/z3/low_level_auto.rb, line 96
def apply_result_get_subgoal(apply_result, num) #=> :goal_pointer
  VeryLowLevel.Z3_apply_result_get_subgoal(_ctx_pointer, apply_result._apply_result, num)
end

# File lib/z3/low_level_auto.rb, line 100
def apply_result_inc_ref(apply_result) #=> :void
  VeryLowLevel.Z3_apply_result_inc_ref(_ctx_pointer, apply_result._apply_result)
end

# File lib/z3/low_level_auto.rb, line 104
def apply_result_to_string(apply_result) #=> :string
  VeryLowLevel.Z3_apply_result_to_string(_ctx_pointer, apply_result._apply_result)
end

# File lib/z3/low_level_auto.rb, line 108
def ast_map_contains(ast_map, ast) #=> :bool
  VeryLowLevel.Z3_ast_map_contains(_ctx_pointer, ast_map._ast_map, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 112
def ast_map_dec_ref(ast_map) #=> :void
  VeryLowLevel.Z3_ast_map_dec_ref(_ctx_pointer, ast_map._ast_map)
end

# File lib/z3/low_level_auto.rb, line 116
def ast_map_erase(ast_map, ast) #=> :void
  VeryLowLevel.Z3_ast_map_erase(_ctx_pointer, ast_map._ast_map, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 120
def ast_map_find(ast_map, ast) #=> :ast_pointer
  VeryLowLevel.Z3_ast_map_find(_ctx_pointer, ast_map._ast_map, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 124
def ast_map_inc_ref(ast_map) #=> :void
  VeryLowLevel.Z3_ast_map_inc_ref(_ctx_pointer, ast_map._ast_map)
end

# File lib/z3/low_level_auto.rb, line 128
def ast_map_insert(ast_map, ast1, ast2) #=> :void
  VeryLowLevel.Z3_ast_map_insert(_ctx_pointer, ast_map._ast_map, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 132
def ast_map_keys(ast_map) #=> :ast_vector_pointer
  VeryLowLevel.Z3_ast_map_keys(_ctx_pointer, ast_map._ast_map)
end

# File lib/z3/low_level_auto.rb, line 136
def ast_map_reset(ast_map) #=> :void
  VeryLowLevel.Z3_ast_map_reset(_ctx_pointer, ast_map._ast_map)
end

# File lib/z3/low_level_auto.rb, line 140
def ast_map_size(ast_map) #=> :uint
  VeryLowLevel.Z3_ast_map_size(_ctx_pointer, ast_map._ast_map)
end

# File lib/z3/low_level_auto.rb, line 144
def ast_map_to_string(ast_map) #=> :string
  VeryLowLevel.Z3_ast_map_to_string(_ctx_pointer, ast_map._ast_map)
end

# File lib/z3/low_level_auto.rb, line 148
def ast_to_string(ast) #=> :string
  VeryLowLevel.Z3_ast_to_string(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 152
def ast_vector_dec_ref(ast_vector) #=> :void
  VeryLowLevel.Z3_ast_vector_dec_ref(_ctx_pointer, ast_vector)
end

# File lib/z3/low_level_auto.rb, line 156
def ast_vector_get(ast_vector, num) #=> :ast_pointer
  VeryLowLevel.Z3_ast_vector_get(_ctx_pointer, ast_vector, num)
end

# File lib/z3/low_level_auto.rb, line 160
def ast_vector_inc_ref(ast_vector) #=> :void
  VeryLowLevel.Z3_ast_vector_inc_ref(_ctx_pointer, ast_vector)
end

# File lib/z3/low_level_auto.rb, line 164
def ast_vector_push(ast_vector, ast) #=> :void
  VeryLowLevel.Z3_ast_vector_push(_ctx_pointer, ast_vector, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 168
def ast_vector_resize(ast_vector, num) #=> :void
  VeryLowLevel.Z3_ast_vector_resize(_ctx_pointer, ast_vector, num)
end

# File lib/z3/low_level_auto.rb, line 172
def ast_vector_set(ast_vector, num, ast) #=> :void
  VeryLowLevel.Z3_ast_vector_set(_ctx_pointer, ast_vector, num, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 176
def ast_vector_size(ast_vector) #=> :uint
  VeryLowLevel.Z3_ast_vector_size(_ctx_pointer, ast_vector)
end

# File lib/z3/low_level_auto.rb, line 180
def ast_vector_to_string(ast_vector) #=> :string
  VeryLowLevel.Z3_ast_vector_to_string(_ctx_pointer, ast_vector)
end

# File lib/z3/low_level_auto.rb, line 184
def ast_vector_translate(ast_vector, context) #=> :ast_vector_pointer
  VeryLowLevel.Z3_ast_vector_translate(_ctx_pointer, ast_vector, context._context)
end

# File lib/z3/low_level_auto.rb, line 188
def constructor_num_fields(constructor) #=> :uint
  VeryLowLevel.Z3_constructor_num_fields(_ctx_pointer, constructor._constructor)
end

# File lib/z3/low_level_auto.rb, line 192
def datatype_update_field(func_decl, ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_datatype_update_field(_ctx_pointer, func_decl._ast, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 196
def dec_ref(ast) #=> :void
  VeryLowLevel.Z3_dec_ref(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 200
def del_config(config) #=> :void
  VeryLowLevel.Z3_del_config(config._config)
end

# File lib/z3/low_level_auto.rb, line 204
def del_constructor(constructor) #=> :void
  VeryLowLevel.Z3_del_constructor(_ctx_pointer, constructor._constructor)
end

# File lib/z3/low_level_auto.rb, line 208
def del_constructor_list(constructor_list) #=> :void
  VeryLowLevel.Z3_del_constructor_list(_ctx_pointer, constructor_list._constructor_list)
end

# File lib/z3/low_level_auto.rb, line 212
def del_context #=> :void
  VeryLowLevel.Z3_del_context(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 216
def disable_trace(str) #=> :void
  VeryLowLevel.Z3_disable_trace(str)
end

# File lib/z3/low_level_auto.rb, line 220
def enable_concurrent_dec_ref #=> :void
  VeryLowLevel.Z3_enable_concurrent_dec_ref(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 224
def enable_trace(str) #=> :void
  VeryLowLevel.Z3_enable_trace(str)
end

# File lib/z3/low_level_auto.rb, line 228
def eval_smtlib2_string(str) #=> :string
  VeryLowLevel.Z3_eval_smtlib2_string(_ctx_pointer, str)
end

# File lib/z3/low_level_auto.rb, line 232
def finalize_memory #=> :void
  VeryLowLevel.Z3_finalize_memory()
end

# File lib/z3/low_level_auto.rb, line 236
def fixedpoint_add_cover(fixedpoint, num, func_decl, ast) #=> :void
  VeryLowLevel.Z3_fixedpoint_add_cover(_ctx_pointer, fixedpoint._fixedpoint, num, func_decl._ast, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 240
def fixedpoint_add_invariant(fixedpoint, func_decl, ast) #=> :void
  VeryLowLevel.Z3_fixedpoint_add_invariant(_ctx_pointer, fixedpoint._fixedpoint, func_decl._ast, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 244
def fixedpoint_add_rule(fixedpoint, ast, sym) #=> :void
  VeryLowLevel.Z3_fixedpoint_add_rule(_ctx_pointer, fixedpoint._fixedpoint, ast._ast, sym)
end

# File lib/z3/low_level_auto.rb, line 248
def fixedpoint_assert(fixedpoint, ast) #=> :void
  VeryLowLevel.Z3_fixedpoint_assert(_ctx_pointer, fixedpoint._fixedpoint, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 252
def fixedpoint_dec_ref(fixedpoint) #=> :void
  VeryLowLevel.Z3_fixedpoint_dec_ref(_ctx_pointer, fixedpoint._fixedpoint)
end

# File lib/z3/low_level_auto.rb, line 256
def fixedpoint_from_file(fixedpoint, str) #=> :ast_vector_pointer
  VeryLowLevel.Z3_fixedpoint_from_file(_ctx_pointer, fixedpoint._fixedpoint, str)
end

# File lib/z3/low_level_auto.rb, line 260
def fixedpoint_from_string(fixedpoint, str) #=> :ast_vector_pointer
  VeryLowLevel.Z3_fixedpoint_from_string(_ctx_pointer, fixedpoint._fixedpoint, str)
end

# File lib/z3/low_level_auto.rb, line 264
def fixedpoint_get_answer(fixedpoint) #=> :ast_pointer
  VeryLowLevel.Z3_fixedpoint_get_answer(_ctx_pointer, fixedpoint._fixedpoint)
end

# File lib/z3/low_level_auto.rb, line 268
def fixedpoint_get_assertions(fixedpoint) #=> :ast_vector_pointer
  VeryLowLevel.Z3_fixedpoint_get_assertions(_ctx_pointer, fixedpoint._fixedpoint)
end

# File lib/z3/low_level_auto.rb, line 272
def fixedpoint_get_cover_delta(fixedpoint, num, func_decl) #=> :ast_pointer
  VeryLowLevel.Z3_fixedpoint_get_cover_delta(_ctx_pointer, fixedpoint._fixedpoint, num, func_decl._ast)
end

# File lib/z3/low_level_auto.rb, line 276
def fixedpoint_get_ground_sat_answer(fixedpoint) #=> :ast_pointer
  VeryLowLevel.Z3_fixedpoint_get_ground_sat_answer(_ctx_pointer, fixedpoint._fixedpoint)
end

# File lib/z3/low_level_auto.rb, line 280
def fixedpoint_get_help(fixedpoint) #=> :string
  VeryLowLevel.Z3_fixedpoint_get_help(_ctx_pointer, fixedpoint._fixedpoint)
end

# File lib/z3/low_level_auto.rb, line 284
def fixedpoint_get_num_levels(fixedpoint, func_decl) #=> :uint
  VeryLowLevel.Z3_fixedpoint_get_num_levels(_ctx_pointer, fixedpoint._fixedpoint, func_decl._ast)
end

# File lib/z3/low_level_auto.rb, line 288
def fixedpoint_get_param_descrs(fixedpoint) #=> :param_descrs_pointer
  VeryLowLevel.Z3_fixedpoint_get_param_descrs(_ctx_pointer, fixedpoint._fixedpoint)
end

# File lib/z3/low_level_auto.rb, line 292
def fixedpoint_get_reachable(fixedpoint, func_decl) #=> :ast_pointer
  VeryLowLevel.Z3_fixedpoint_get_reachable(_ctx_pointer, fixedpoint._fixedpoint, func_decl._ast)
end

# File lib/z3/low_level_auto.rb, line 296
def fixedpoint_get_reason_unknown(fixedpoint) #=> :string
  VeryLowLevel.Z3_fixedpoint_get_reason_unknown(_ctx_pointer, fixedpoint._fixedpoint)
end

# File lib/z3/low_level_auto.rb, line 300
def fixedpoint_get_rule_names_along_trace(fixedpoint) #=> :symbol_pointer
  VeryLowLevel.Z3_fixedpoint_get_rule_names_along_trace(_ctx_pointer, fixedpoint._fixedpoint)
end

# File lib/z3/low_level_auto.rb, line 304
def fixedpoint_get_rules(fixedpoint) #=> :ast_vector_pointer
  VeryLowLevel.Z3_fixedpoint_get_rules(_ctx_pointer, fixedpoint._fixedpoint)
end

# File lib/z3/low_level_auto.rb, line 308
def fixedpoint_get_rules_along_trace(fixedpoint) #=> :ast_vector_pointer
  VeryLowLevel.Z3_fixedpoint_get_rules_along_trace(_ctx_pointer, fixedpoint._fixedpoint)
end

# File lib/z3/low_level_auto.rb, line 312
def fixedpoint_get_statistics(fixedpoint) #=> :stats_pointer
  VeryLowLevel.Z3_fixedpoint_get_statistics(_ctx_pointer, fixedpoint._fixedpoint)
end

# File lib/z3/low_level_auto.rb, line 316
def fixedpoint_inc_ref(fixedpoint) #=> :void
  VeryLowLevel.Z3_fixedpoint_inc_ref(_ctx_pointer, fixedpoint._fixedpoint)
end

# File lib/z3/low_level_auto.rb, line 320
def fixedpoint_query(fixedpoint, ast) #=> :int
  VeryLowLevel.Z3_fixedpoint_query(_ctx_pointer, fixedpoint._fixedpoint, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 324
def fixedpoint_query_from_lvl(fixedpoint, ast, num) #=> :int
  VeryLowLevel.Z3_fixedpoint_query_from_lvl(_ctx_pointer, fixedpoint._fixedpoint, ast._ast, num)
end

# File lib/z3/low_level_auto.rb, line 328
def fixedpoint_register_relation(fixedpoint, func_decl) #=> :void
  VeryLowLevel.Z3_fixedpoint_register_relation(_ctx_pointer, fixedpoint._fixedpoint, func_decl._ast)
end

# File lib/z3/low_level_auto.rb, line 332
def fixedpoint_set_params(fixedpoint, params) #=> :void
  VeryLowLevel.Z3_fixedpoint_set_params(_ctx_pointer, fixedpoint._fixedpoint, params._params)
end

# File lib/z3/low_level_auto.rb, line 336
def fixedpoint_update_rule(fixedpoint, ast, sym) #=> :void
  VeryLowLevel.Z3_fixedpoint_update_rule(_ctx_pointer, fixedpoint._fixedpoint, ast._ast, sym)
end

# File lib/z3/low_level_auto.rb, line 340
def fpa_get_ebits(sort) #=> :uint
  VeryLowLevel.Z3_fpa_get_ebits(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 344
def fpa_get_numeral_exponent_bv(ast, bool) #=> :ast_pointer
  VeryLowLevel.Z3_fpa_get_numeral_exponent_bv(_ctx_pointer, ast._ast, bool)
end

# File lib/z3/low_level_auto.rb, line 348
def fpa_get_numeral_exponent_string(ast, bool) #=> :string
  VeryLowLevel.Z3_fpa_get_numeral_exponent_string(_ctx_pointer, ast._ast, bool)
end

# File lib/z3/low_level_auto.rb, line 352
def fpa_get_numeral_sign_bv(ast) #=> :ast_pointer
  VeryLowLevel.Z3_fpa_get_numeral_sign_bv(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 356
def fpa_get_numeral_significand_bv(ast) #=> :ast_pointer
  VeryLowLevel.Z3_fpa_get_numeral_significand_bv(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 360
def fpa_get_numeral_significand_string(ast) #=> :string
  VeryLowLevel.Z3_fpa_get_numeral_significand_string(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 364
def fpa_get_sbits(sort) #=> :uint
  VeryLowLevel.Z3_fpa_get_sbits(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 368
def fpa_is_numeral_inf(ast) #=> :bool
  VeryLowLevel.Z3_fpa_is_numeral_inf(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 372
def fpa_is_numeral_nan(ast) #=> :bool
  VeryLowLevel.Z3_fpa_is_numeral_nan(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 376
def fpa_is_numeral_negative(ast) #=> :bool
  VeryLowLevel.Z3_fpa_is_numeral_negative(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 380
def fpa_is_numeral_normal(ast) #=> :bool
  VeryLowLevel.Z3_fpa_is_numeral_normal(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 384
def fpa_is_numeral_positive(ast) #=> :bool
  VeryLowLevel.Z3_fpa_is_numeral_positive(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 388
def fpa_is_numeral_subnormal(ast) #=> :bool
  VeryLowLevel.Z3_fpa_is_numeral_subnormal(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 392
def fpa_is_numeral_zero(ast) #=> :bool
  VeryLowLevel.Z3_fpa_is_numeral_zero(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 396
def func_entry_dec_ref(func_entry) #=> :void
  VeryLowLevel.Z3_func_entry_dec_ref(_ctx_pointer, func_entry._func_entry)
end

# File lib/z3/low_level_auto.rb, line 400
def func_entry_get_arg(func_entry, num) #=> :ast_pointer
  VeryLowLevel.Z3_func_entry_get_arg(_ctx_pointer, func_entry._func_entry, num)
end

# File lib/z3/low_level_auto.rb, line 404
def func_entry_get_num_args(func_entry) #=> :uint
  VeryLowLevel.Z3_func_entry_get_num_args(_ctx_pointer, func_entry._func_entry)
end

# File lib/z3/low_level_auto.rb, line 408
def func_entry_get_value(func_entry) #=> :ast_pointer
  VeryLowLevel.Z3_func_entry_get_value(_ctx_pointer, func_entry._func_entry)
end

# File lib/z3/low_level_auto.rb, line 412
def func_entry_inc_ref(func_entry) #=> :void
  VeryLowLevel.Z3_func_entry_inc_ref(_ctx_pointer, func_entry._func_entry)
end

# File lib/z3/low_level_auto.rb, line 416
def func_interp_add_entry(func_interp, ast_vector, ast) #=> :void
  VeryLowLevel.Z3_func_interp_add_entry(_ctx_pointer, func_interp._func_interp, ast_vector, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 420
def func_interp_dec_ref(func_interp) #=> :void
  VeryLowLevel.Z3_func_interp_dec_ref(_ctx_pointer, func_interp._func_interp)
end

# File lib/z3/low_level_auto.rb, line 424
def func_interp_get_arity(func_interp) #=> :uint
  VeryLowLevel.Z3_func_interp_get_arity(_ctx_pointer, func_interp._func_interp)
end

# File lib/z3/low_level_auto.rb, line 428
def func_interp_get_else(func_interp) #=> :ast_pointer
  VeryLowLevel.Z3_func_interp_get_else(_ctx_pointer, func_interp._func_interp)
end

# File lib/z3/low_level_auto.rb, line 432
def func_interp_get_entry(func_interp, num) #=> :func_entry_pointer
  VeryLowLevel.Z3_func_interp_get_entry(_ctx_pointer, func_interp._func_interp, num)
end

# File lib/z3/low_level_auto.rb, line 436
def func_interp_get_num_entries(func_interp) #=> :uint
  VeryLowLevel.Z3_func_interp_get_num_entries(_ctx_pointer, func_interp._func_interp)
end

# File lib/z3/low_level_auto.rb, line 440
def func_interp_inc_ref(func_interp) #=> :void
  VeryLowLevel.Z3_func_interp_inc_ref(_ctx_pointer, func_interp._func_interp)
end

# File lib/z3/low_level_auto.rb, line 444
def func_interp_set_else(func_interp, ast) #=> :void
  VeryLowLevel.Z3_func_interp_set_else(_ctx_pointer, func_interp._func_interp, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 448
def get_algebraic_number_lower(ast, num) #=> :ast_pointer
  VeryLowLevel.Z3_get_algebraic_number_lower(_ctx_pointer, ast._ast, num)
end

# File lib/z3/low_level_auto.rb, line 452
def get_algebraic_number_upper(ast, num) #=> :ast_pointer
  VeryLowLevel.Z3_get_algebraic_number_upper(_ctx_pointer, ast._ast, num)
end

# File lib/z3/low_level_auto.rb, line 456
def get_app_arg(app, num) #=> :ast_pointer
  VeryLowLevel.Z3_get_app_arg(_ctx_pointer, app._ast, num)
end

# File lib/z3/low_level_auto.rb, line 460
def get_app_decl(app) #=> :func_decl_pointer
  VeryLowLevel.Z3_get_app_decl(_ctx_pointer, app._ast)
end

# File lib/z3/low_level_auto.rb, line 464
def get_app_num_args(app) #=> :uint
  VeryLowLevel.Z3_get_app_num_args(_ctx_pointer, app._ast)
end

# File lib/z3/low_level_auto.rb, line 468
def get_arity(func_decl) #=> :uint
  VeryLowLevel.Z3_get_arity(_ctx_pointer, func_decl._ast)
end

# File lib/z3/low_level_auto.rb, line 472
def get_array_arity(sort) #=> :uint
  VeryLowLevel.Z3_get_array_arity(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 476
def get_array_sort_domain(sort) #=> :sort_pointer
  VeryLowLevel.Z3_get_array_sort_domain(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 480
def get_array_sort_domain_n(sort, num) #=> :sort_pointer
  VeryLowLevel.Z3_get_array_sort_domain_n(_ctx_pointer, sort._ast, num)
end

# File lib/z3/low_level_auto.rb, line 484
def get_array_sort_range(sort) #=> :sort_pointer
  VeryLowLevel.Z3_get_array_sort_range(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 488
def get_as_array_func_decl(ast) #=> :func_decl_pointer
  VeryLowLevel.Z3_get_as_array_func_decl(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 492
def get_ast_hash(ast) #=> :uint
  VeryLowLevel.Z3_get_ast_hash(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 496
def get_ast_id(ast) #=> :uint
  VeryLowLevel.Z3_get_ast_id(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 500
def get_ast_kind(ast) #=> :uint
  VeryLowLevel.Z3_get_ast_kind(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 504
def get_bool_value(ast) #=> :int
  VeryLowLevel.Z3_get_bool_value(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 508
def get_bv_sort_size(sort) #=> :uint
  VeryLowLevel.Z3_get_bv_sort_size(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 512
def get_datatype_sort_constructor(sort, num) #=> :func_decl_pointer
  VeryLowLevel.Z3_get_datatype_sort_constructor(_ctx_pointer, sort._ast, num)
end

# File lib/z3/low_level_auto.rb, line 516
def get_datatype_sort_constructor_accessor(sort, num1, num2) #=> :func_decl_pointer
  VeryLowLevel.Z3_get_datatype_sort_constructor_accessor(_ctx_pointer, sort._ast, num1, num2)
end

# File lib/z3/low_level_auto.rb, line 520
def get_datatype_sort_num_constructors(sort) #=> :uint
  VeryLowLevel.Z3_get_datatype_sort_num_constructors(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 524
def get_datatype_sort_recognizer(sort, num) #=> :func_decl_pointer
  VeryLowLevel.Z3_get_datatype_sort_recognizer(_ctx_pointer, sort._ast, num)
end

# File lib/z3/low_level_auto.rb, line 528
def get_decl_ast_parameter(func_decl, num) #=> :ast_pointer
  VeryLowLevel.Z3_get_decl_ast_parameter(_ctx_pointer, func_decl._ast, num)
end

# File lib/z3/low_level_auto.rb, line 532
def get_decl_double_parameter(func_decl, num) #=> :double
  VeryLowLevel.Z3_get_decl_double_parameter(_ctx_pointer, func_decl._ast, num)
end

# File lib/z3/low_level_auto.rb, line 536
def get_decl_func_decl_parameter(func_decl, num) #=> :func_decl_pointer
  VeryLowLevel.Z3_get_decl_func_decl_parameter(_ctx_pointer, func_decl._ast, num)
end

# File lib/z3/low_level_auto.rb, line 540
def get_decl_int_parameter(func_decl, num) #=> :int
  VeryLowLevel.Z3_get_decl_int_parameter(_ctx_pointer, func_decl._ast, num)
end

# File lib/z3/low_level_auto.rb, line 544
def get_decl_kind(func_decl) #=> :uint
  VeryLowLevel.Z3_get_decl_kind(_ctx_pointer, func_decl._ast)
end

# File lib/z3/low_level_auto.rb, line 548
def get_decl_name(func_decl) #=> :symbol_pointer
  VeryLowLevel.Z3_get_decl_name(_ctx_pointer, func_decl._ast)
end

# File lib/z3/low_level_auto.rb, line 552
def get_decl_num_parameters(func_decl) #=> :uint
  VeryLowLevel.Z3_get_decl_num_parameters(_ctx_pointer, func_decl._ast)
end

# File lib/z3/low_level_auto.rb, line 556
def get_decl_parameter_kind(func_decl, num) #=> :uint
  VeryLowLevel.Z3_get_decl_parameter_kind(_ctx_pointer, func_decl._ast, num)
end

# File lib/z3/low_level_auto.rb, line 560
def get_decl_rational_parameter(func_decl, num) #=> :string
  VeryLowLevel.Z3_get_decl_rational_parameter(_ctx_pointer, func_decl._ast, num)
end

# File lib/z3/low_level_auto.rb, line 564
def get_decl_sort_parameter(func_decl, num) #=> :sort_pointer
  VeryLowLevel.Z3_get_decl_sort_parameter(_ctx_pointer, func_decl._ast, num)
end

# File lib/z3/low_level_auto.rb, line 568
def get_decl_symbol_parameter(func_decl, num) #=> :symbol_pointer
  VeryLowLevel.Z3_get_decl_symbol_parameter(_ctx_pointer, func_decl._ast, num)
end

# File lib/z3/low_level_auto.rb, line 572
def get_denominator(ast) #=> :ast_pointer
  VeryLowLevel.Z3_get_denominator(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 576
def get_depth(ast) #=> :uint
  VeryLowLevel.Z3_get_depth(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 580
def get_domain(func_decl, num) #=> :sort_pointer
  VeryLowLevel.Z3_get_domain(_ctx_pointer, func_decl._ast, num)
end

# File lib/z3/low_level_auto.rb, line 584
def get_domain_size(func_decl) #=> :uint
  VeryLowLevel.Z3_get_domain_size(_ctx_pointer, func_decl._ast)
end

# File lib/z3/low_level_auto.rb, line 588
def get_error_code #=> :uint
  VeryLowLevel.Z3_get_error_code(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 592
def get_full_version #=> :string
  VeryLowLevel.Z3_get_full_version()
end

# File lib/z3/low_level_auto.rb, line 596
def get_func_decl_id(func_decl) #=> :uint
  VeryLowLevel.Z3_get_func_decl_id(_ctx_pointer, func_decl._ast)
end

# File lib/z3/low_level_auto.rb, line 600
def get_global_param_descrs #=> :param_descrs_pointer
  VeryLowLevel.Z3_get_global_param_descrs(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 604
def get_index_value(ast) #=> :uint
  VeryLowLevel.Z3_get_index_value(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 608
def get_num_probes #=> :uint
  VeryLowLevel.Z3_get_num_probes(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 612
def get_num_simplifiers #=> :uint
  VeryLowLevel.Z3_get_num_simplifiers(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 616
def get_num_tactics #=> :uint
  VeryLowLevel.Z3_get_num_tactics(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 620
def get_numeral_binary_string(ast) #=> :string
  VeryLowLevel.Z3_get_numeral_binary_string(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 624
def get_numeral_decimal_string(ast, num) #=> :string
  VeryLowLevel.Z3_get_numeral_decimal_string(_ctx_pointer, ast._ast, num)
end

# File lib/z3/low_level_auto.rb, line 628
def get_numeral_double(ast) #=> :double
  VeryLowLevel.Z3_get_numeral_double(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 632
def get_numeral_string(ast) #=> :string
  VeryLowLevel.Z3_get_numeral_string(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 636
def get_numerator(ast) #=> :ast_pointer
  VeryLowLevel.Z3_get_numerator(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 640
def get_pattern(pattern, num) #=> :ast_pointer
  VeryLowLevel.Z3_get_pattern(_ctx_pointer, pattern._ast, num)
end

# File lib/z3/low_level_auto.rb, line 644
def get_pattern_num_terms(pattern) #=> :uint
  VeryLowLevel.Z3_get_pattern_num_terms(_ctx_pointer, pattern._ast)
end

# File lib/z3/low_level_auto.rb, line 648
def get_probe_name(num) #=> :string
  VeryLowLevel.Z3_get_probe_name(_ctx_pointer, num)
end

# File lib/z3/low_level_auto.rb, line 652
def get_quantifier_body(ast) #=> :ast_pointer
  VeryLowLevel.Z3_get_quantifier_body(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 656
def get_quantifier_bound_name(ast, num) #=> :symbol_pointer
  VeryLowLevel.Z3_get_quantifier_bound_name(_ctx_pointer, ast._ast, num)
end

# File lib/z3/low_level_auto.rb, line 660
def get_quantifier_bound_sort(ast, num) #=> :sort_pointer
  VeryLowLevel.Z3_get_quantifier_bound_sort(_ctx_pointer, ast._ast, num)
end

# File lib/z3/low_level_auto.rb, line 664
def get_quantifier_id(ast) #=> :symbol_pointer
  VeryLowLevel.Z3_get_quantifier_id(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 668
def get_quantifier_no_pattern_ast(ast, num) #=> :ast_pointer
  VeryLowLevel.Z3_get_quantifier_no_pattern_ast(_ctx_pointer, ast._ast, num)
end

# File lib/z3/low_level_auto.rb, line 672
def get_quantifier_num_bound(ast) #=> :uint
  VeryLowLevel.Z3_get_quantifier_num_bound(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 676
def get_quantifier_num_no_patterns(ast) #=> :uint
  VeryLowLevel.Z3_get_quantifier_num_no_patterns(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 680
def get_quantifier_num_patterns(ast) #=> :uint
  VeryLowLevel.Z3_get_quantifier_num_patterns(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 684
def get_quantifier_pattern_ast(ast, num) #=> :pattern_pointer
  VeryLowLevel.Z3_get_quantifier_pattern_ast(_ctx_pointer, ast._ast, num)
end

# File lib/z3/low_level_auto.rb, line 688
def get_quantifier_skolem_id(ast) #=> :symbol_pointer
  VeryLowLevel.Z3_get_quantifier_skolem_id(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 692
def get_quantifier_weight(ast) #=> :uint
  VeryLowLevel.Z3_get_quantifier_weight(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 696
def get_range(func_decl) #=> :sort_pointer
  VeryLowLevel.Z3_get_range(_ctx_pointer, func_decl._ast)
end

# File lib/z3/low_level_auto.rb, line 700
def get_re_sort_basis(sort) #=> :sort_pointer
  VeryLowLevel.Z3_get_re_sort_basis(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 704
def get_relation_arity(sort) #=> :uint
  VeryLowLevel.Z3_get_relation_arity(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 708
def get_relation_column(sort, num) #=> :sort_pointer
  VeryLowLevel.Z3_get_relation_column(_ctx_pointer, sort._ast, num)
end

# File lib/z3/low_level_auto.rb, line 712
def get_seq_sort_basis(sort) #=> :sort_pointer
  VeryLowLevel.Z3_get_seq_sort_basis(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 716
def get_simplifier_name(num) #=> :string
  VeryLowLevel.Z3_get_simplifier_name(_ctx_pointer, num)
end

# File lib/z3/low_level_auto.rb, line 720
def get_sort(ast) #=> :sort_pointer
  VeryLowLevel.Z3_get_sort(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 724
def get_sort_id(sort) #=> :uint
  VeryLowLevel.Z3_get_sort_id(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 728
def get_sort_kind(sort) #=> :uint
  VeryLowLevel.Z3_get_sort_kind(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 732
def get_sort_name(sort) #=> :symbol_pointer
  VeryLowLevel.Z3_get_sort_name(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 736
def get_string_length(ast) #=> :uint
  VeryLowLevel.Z3_get_string_length(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 740
def get_symbol_int(sym) #=> :int
  VeryLowLevel.Z3_get_symbol_int(_ctx_pointer, sym)
end

# File lib/z3/low_level_auto.rb, line 744
def get_symbol_kind(sym) #=> :uint
  VeryLowLevel.Z3_get_symbol_kind(_ctx_pointer, sym)
end

# File lib/z3/low_level_auto.rb, line 748
def get_symbol_string(sym) #=> :string
  VeryLowLevel.Z3_get_symbol_string(_ctx_pointer, sym)
end

# File lib/z3/low_level_auto.rb, line 752
def get_tactic_name(num) #=> :string
  VeryLowLevel.Z3_get_tactic_name(_ctx_pointer, num)
end

# File lib/z3/low_level_auto.rb, line 756
def get_tuple_sort_field_decl(sort, num) #=> :func_decl_pointer
  VeryLowLevel.Z3_get_tuple_sort_field_decl(_ctx_pointer, sort._ast, num)
end

# File lib/z3/low_level_auto.rb, line 760
def get_tuple_sort_mk_decl(sort) #=> :func_decl_pointer
  VeryLowLevel.Z3_get_tuple_sort_mk_decl(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 764
def get_tuple_sort_num_fields(sort) #=> :uint
  VeryLowLevel.Z3_get_tuple_sort_num_fields(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 768
def global_param_reset_all #=> :void
  VeryLowLevel.Z3_global_param_reset_all()
end

# File lib/z3/low_level_auto.rb, line 772
def global_param_set(str1, str2) #=> :void
  VeryLowLevel.Z3_global_param_set(str1, str2)
end

# File lib/z3/low_level_auto.rb, line 776
def goal_assert(goal, ast) #=> :void
  VeryLowLevel.Z3_goal_assert(_ctx_pointer, goal._goal, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 780
def goal_convert_model(goal, model) #=> :model_pointer
  VeryLowLevel.Z3_goal_convert_model(_ctx_pointer, goal._goal, model._model)
end

# File lib/z3/low_level_auto.rb, line 784
def goal_dec_ref(goal) #=> :void
  VeryLowLevel.Z3_goal_dec_ref(_ctx_pointer, goal._goal)
end

# File lib/z3/low_level_auto.rb, line 788
def goal_depth(goal) #=> :uint
  VeryLowLevel.Z3_goal_depth(_ctx_pointer, goal._goal)
end

# File lib/z3/low_level_auto.rb, line 792
def goal_formula(goal, num) #=> :ast_pointer
  VeryLowLevel.Z3_goal_formula(_ctx_pointer, goal._goal, num)
end

# File lib/z3/low_level_auto.rb, line 796
def goal_inc_ref(goal) #=> :void
  VeryLowLevel.Z3_goal_inc_ref(_ctx_pointer, goal._goal)
end

# File lib/z3/low_level_auto.rb, line 800
def goal_inconsistent(goal) #=> :bool
  VeryLowLevel.Z3_goal_inconsistent(_ctx_pointer, goal._goal)
end

# File lib/z3/low_level_auto.rb, line 804
def goal_is_decided_sat(goal) #=> :bool
  VeryLowLevel.Z3_goal_is_decided_sat(_ctx_pointer, goal._goal)
end

# File lib/z3/low_level_auto.rb, line 808
def goal_is_decided_unsat(goal) #=> :bool
  VeryLowLevel.Z3_goal_is_decided_unsat(_ctx_pointer, goal._goal)
end

# File lib/z3/low_level_auto.rb, line 812
def goal_num_exprs(goal) #=> :uint
  VeryLowLevel.Z3_goal_num_exprs(_ctx_pointer, goal._goal)
end

# File lib/z3/low_level_auto.rb, line 816
def goal_precision(goal) #=> :uint
  VeryLowLevel.Z3_goal_precision(_ctx_pointer, goal._goal)
end

# File lib/z3/low_level_auto.rb, line 820
def goal_reset(goal) #=> :void
  VeryLowLevel.Z3_goal_reset(_ctx_pointer, goal._goal)
end

# File lib/z3/low_level_auto.rb, line 824
def goal_size(goal) #=> :uint
  VeryLowLevel.Z3_goal_size(_ctx_pointer, goal._goal)
end

# File lib/z3/low_level_auto.rb, line 828
def goal_to_dimacs_string(goal, bool) #=> :string
  VeryLowLevel.Z3_goal_to_dimacs_string(_ctx_pointer, goal._goal, bool)
end

# File lib/z3/low_level_auto.rb, line 832
def goal_to_string(goal) #=> :string
  VeryLowLevel.Z3_goal_to_string(_ctx_pointer, goal._goal)
end

# File lib/z3/low_level_auto.rb, line 836
def goal_translate(goal, context) #=> :goal_pointer
  VeryLowLevel.Z3_goal_translate(_ctx_pointer, goal._goal, context._context)
end

# File lib/z3/low_level_auto.rb, line 840
def inc_ref(ast) #=> :void
  VeryLowLevel.Z3_inc_ref(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 844
def interrupt #=> :void
  VeryLowLevel.Z3_interrupt(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 848
def is_algebraic_number(ast) #=> :bool
  VeryLowLevel.Z3_is_algebraic_number(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 852
def is_app(ast) #=> :bool
  VeryLowLevel.Z3_is_app(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 856
def is_as_array(ast) #=> :bool
  VeryLowLevel.Z3_is_as_array(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 860
def is_char_sort(sort) #=> :bool
  VeryLowLevel.Z3_is_char_sort(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 864
def is_eq_ast(ast1, ast2) #=> :bool
  VeryLowLevel.Z3_is_eq_ast(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 868
def is_eq_func_decl(func_decl1, func_decl2) #=> :bool
  VeryLowLevel.Z3_is_eq_func_decl(_ctx_pointer, func_decl1._ast, func_decl2._ast)
end

# File lib/z3/low_level_auto.rb, line 872
def is_eq_sort(sort1, sort2) #=> :bool
  VeryLowLevel.Z3_is_eq_sort(_ctx_pointer, sort1._ast, sort2._ast)
end

# File lib/z3/low_level_auto.rb, line 876
def is_ground(ast) #=> :bool
  VeryLowLevel.Z3_is_ground(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 880
def is_lambda(ast) #=> :bool
  VeryLowLevel.Z3_is_lambda(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 884
def is_numeral_ast(ast) #=> :bool
  VeryLowLevel.Z3_is_numeral_ast(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 888
def is_quantifier_exists(ast) #=> :bool
  VeryLowLevel.Z3_is_quantifier_exists(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 892
def is_quantifier_forall(ast) #=> :bool
  VeryLowLevel.Z3_is_quantifier_forall(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 896
def is_recursive_datatype_sort(sort) #=> :bool
  VeryLowLevel.Z3_is_recursive_datatype_sort(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 900
def is_well_sorted(ast) #=> :bool
  VeryLowLevel.Z3_is_well_sorted(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 904
def mk_abs(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_abs(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 908
def mk_array_default(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_array_default(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 912
def mk_array_sort(sort1, sort2) #=> :sort_pointer
  VeryLowLevel.Z3_mk_array_sort(_ctx_pointer, sort1._ast, sort2._ast)
end

# File lib/z3/low_level_auto.rb, line 916
def mk_as_array(func_decl) #=> :ast_pointer
  VeryLowLevel.Z3_mk_as_array(_ctx_pointer, func_decl._ast)
end

# File lib/z3/low_level_auto.rb, line 920
def mk_ast_map #=> :ast_map_pointer
  VeryLowLevel.Z3_mk_ast_map(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 924
def mk_ast_vector #=> :ast_vector_pointer
  VeryLowLevel.Z3_mk_ast_vector(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 928
def mk_bit2bool(num, ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bit2bool(_ctx_pointer, num, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 932
def mk_bool_sort #=> :sort_pointer
  VeryLowLevel.Z3_mk_bool_sort(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 936
def mk_bound(num, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bound(_ctx_pointer, num, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 940
def mk_bv2int(ast, bool) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bv2int(_ctx_pointer, ast._ast, bool)
end

# File lib/z3/low_level_auto.rb, line 944
def mk_bv_sort(num) #=> :sort_pointer
  VeryLowLevel.Z3_mk_bv_sort(_ctx_pointer, num)
end

# File lib/z3/low_level_auto.rb, line 948
def mk_bvadd(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvadd(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 952
def mk_bvadd_no_overflow(ast1, ast2, bool) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvadd_no_overflow(_ctx_pointer, ast1._ast, ast2._ast, bool)
end

# File lib/z3/low_level_auto.rb, line 956
def mk_bvadd_no_underflow(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvadd_no_underflow(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 960
def mk_bvand(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvand(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 964
def mk_bvashr(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvashr(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 968
def mk_bvlshr(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvlshr(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 972
def mk_bvmul(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvmul(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 976
def mk_bvmul_no_overflow(ast1, ast2, bool) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvmul_no_overflow(_ctx_pointer, ast1._ast, ast2._ast, bool)
end

# File lib/z3/low_level_auto.rb, line 980
def mk_bvmul_no_underflow(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvmul_no_underflow(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 984
def mk_bvnand(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvnand(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 988
def mk_bvneg(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvneg(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 992
def mk_bvneg_no_overflow(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvneg_no_overflow(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 996
def mk_bvnor(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvnor(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1000
def mk_bvnot(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvnot(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1004
def mk_bvor(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvor(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1008
def mk_bvredand(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvredand(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1012
def mk_bvredor(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvredor(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1016
def mk_bvsdiv(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsdiv(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1020
def mk_bvsdiv_no_overflow(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsdiv_no_overflow(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1024
def mk_bvsge(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsge(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1028
def mk_bvsgt(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsgt(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1032
def mk_bvshl(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvshl(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1036
def mk_bvsle(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsle(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1040
def mk_bvslt(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvslt(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1044
def mk_bvsmod(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsmod(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1048
def mk_bvsrem(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsrem(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1052
def mk_bvsub(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsub(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1056
def mk_bvsub_no_overflow(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsub_no_overflow(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1060
def mk_bvsub_no_underflow(ast1, ast2, bool) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsub_no_underflow(_ctx_pointer, ast1._ast, ast2._ast, bool)
end

# File lib/z3/low_level_auto.rb, line 1064
def mk_bvudiv(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvudiv(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1068
def mk_bvuge(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvuge(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1072
def mk_bvugt(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvugt(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1076
def mk_bvule(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvule(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1080
def mk_bvult(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvult(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1084
def mk_bvurem(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvurem(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1088
def mk_bvxnor(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvxnor(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1092
def mk_bvxor(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvxor(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1096
def mk_char(num) #=> :ast_pointer
  VeryLowLevel.Z3_mk_char(_ctx_pointer, num)
end

# File lib/z3/low_level_auto.rb, line 1100
def mk_char_from_bv(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_char_from_bv(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1104
def mk_char_is_digit(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_char_is_digit(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1108
def mk_char_le(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_char_le(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1112
def mk_char_sort #=> :sort_pointer
  VeryLowLevel.Z3_mk_char_sort(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 1116
def mk_char_to_bv(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_char_to_bv(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1120
def mk_char_to_int(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_char_to_int(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1124
def mk_concat(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_concat(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1128
def mk_config #=> :config_pointer
  VeryLowLevel.Z3_mk_config()
end

# File lib/z3/low_level_auto.rb, line 1132
def mk_const(sym, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_const(_ctx_pointer, sym, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 1136
def mk_const_array(sort, ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_const_array(_ctx_pointer, sort._ast, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1140
def mk_context_rc(config) #=> :ctx_pointer
  VeryLowLevel.Z3_mk_context_rc(config._config)
end

# File lib/z3/low_level_auto.rb, line 1144
def mk_datatype_sort(sym) #=> :sort_pointer
  VeryLowLevel.Z3_mk_datatype_sort(_ctx_pointer, sym)
end

# File lib/z3/low_level_auto.rb, line 1148
def mk_div(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_div(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1152
def mk_divides(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_divides(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1156
def mk_empty_set(sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_empty_set(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 1160
def mk_eq(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_eq(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1164
def mk_ext_rotate_left(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_ext_rotate_left(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1168
def mk_ext_rotate_right(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_ext_rotate_right(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1172
def mk_extract(num1, num2, ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_extract(_ctx_pointer, num1, num2, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1176
def mk_false #=> :ast_pointer
  VeryLowLevel.Z3_mk_false(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 1180
def mk_finite_domain_sort(sym, num) #=> :sort_pointer
  VeryLowLevel.Z3_mk_finite_domain_sort(_ctx_pointer, sym, num)
end

# File lib/z3/low_level_auto.rb, line 1184
def mk_fixedpoint #=> :fixedpoint_pointer
  VeryLowLevel.Z3_mk_fixedpoint(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 1188
def mk_fpa_abs(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_abs(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1192
def mk_fpa_add(ast1, ast2, ast3) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_add(_ctx_pointer, ast1._ast, ast2._ast, ast3._ast)
end

# File lib/z3/low_level_auto.rb, line 1196
def mk_fpa_div(ast1, ast2, ast3) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_div(_ctx_pointer, ast1._ast, ast2._ast, ast3._ast)
end

# File lib/z3/low_level_auto.rb, line 1200
def mk_fpa_eq(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_eq(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1204
def mk_fpa_fma(ast1, ast2, ast3, ast4) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_fma(_ctx_pointer, ast1._ast, ast2._ast, ast3._ast, ast4._ast)
end

# File lib/z3/low_level_auto.rb, line 1208
def mk_fpa_fp(ast1, ast2, ast3) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_fp(_ctx_pointer, ast1._ast, ast2._ast, ast3._ast)
end

# File lib/z3/low_level_auto.rb, line 1212
def mk_fpa_geq(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_geq(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1216
def mk_fpa_gt(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_gt(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1220
def mk_fpa_inf(sort, bool) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_inf(_ctx_pointer, sort._ast, bool)
end

# File lib/z3/low_level_auto.rb, line 1224
def mk_fpa_is_infinite(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_is_infinite(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1228
def mk_fpa_is_nan(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_is_nan(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1232
def mk_fpa_is_negative(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_is_negative(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1236
def mk_fpa_is_normal(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_is_normal(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1240
def mk_fpa_is_positive(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_is_positive(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1244
def mk_fpa_is_subnormal(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_is_subnormal(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1248
def mk_fpa_is_zero(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_is_zero(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1252
def mk_fpa_leq(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_leq(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1256
def mk_fpa_lt(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_lt(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1260
def mk_fpa_max(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_max(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1264
def mk_fpa_min(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_min(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1268
def mk_fpa_mul(ast1, ast2, ast3) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_mul(_ctx_pointer, ast1._ast, ast2._ast, ast3._ast)
end

# File lib/z3/low_level_auto.rb, line 1272
def mk_fpa_nan(sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_nan(_ctx_pointer, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 1276
def mk_fpa_neg(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_neg(_ctx_pointer, ast._ast)
end

# File lib/z3/low_level_auto.rb, line 1280
def mk_fpa_numeral_double(double, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_numeral_double(_ctx_pointer, double, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 1284
def mk_fpa_numeral_int(num, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_numeral_int(_ctx_pointer, num, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 1288
def mk_fpa_numeral_int64_uint64(bool, num1, num2, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_numeral_int64_uint64(_ctx_pointer, bool, num1, num2, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 1292
def mk_fpa_numeral_int_uint(bool, num1, num2, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_numeral_int_uint(_ctx_pointer, bool, num1, num2, sort._ast)
end

# File lib/z3/low_level_auto.rb, line 1296
def mk_fpa_rem(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_rem(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1300
def mk_fpa_round_nearest_ties_to_away #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_round_nearest_ties_to_away(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 1304
def mk_fpa_round_nearest_ties_to_even #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_round_nearest_ties_to_even(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 1308
def mk_fpa_round_to_integral(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_round_to_integral(_ctx_pointer, ast1._ast, ast2._ast)
end

# File lib/z3/low_level_auto.rb, line 1312
def mk_fpa_round_toward_negative #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_round_toward_negative(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 1316
def mk_fpa_round_toward_positive #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_round_toward_positive(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 1320
def mk_fpa_round_toward_zero #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_round_toward_zero(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 1324
def mk_fpa_rounding_mode_sort #=> :sort_pointer
  VeryLowLevel.Z3_mk_fpa_rounding_mode_sort(_ctx_pointer)
end

# File lib/z3/low_level_auto.rb, line 1328
def mk_fpa_sort(num1, num2) #=> :sort_pointer
  VeryLowLevel.Z3_mk_fpa_sort(_ctx_pointer, num1, num2)
end