module Z3::LowLevel

Public Class Methods

_ctx_pointer() click to toggle source
# File lib/z3/low_level.rb, line 96
def _ctx_pointer
  @_ctx_pointer ||= Z3::Context.instance._context
end
add_const_interp(model, func_decl, ast) click to toggle source
# 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
add_func_interp(model, func_decl, ast) click to toggle source
# 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
algebraic_add(ast1, ast2) click to toggle source
# 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
algebraic_div(ast1, ast2) click to toggle source
# 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
algebraic_eq(ast1, ast2) click to toggle source
# 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
algebraic_ge(ast1, ast2) click to toggle source
# 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
algebraic_get_i(ast) click to toggle source
# 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
algebraic_get_poly(ast) click to toggle source
# 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
algebraic_gt(ast1, ast2) click to toggle source
# 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
algebraic_is_neg(ast) click to toggle source
# 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
algebraic_is_pos(ast) click to toggle source
# 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
algebraic_is_value(ast) click to toggle source
# 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
algebraic_is_zero(ast) click to toggle source
# 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
algebraic_le(ast1, ast2) click to toggle source
# 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
algebraic_lt(ast1, ast2) click to toggle source
# 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
algebraic_mul(ast1, ast2) click to toggle source
# 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
algebraic_neq(ast1, ast2) click to toggle source
# 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
algebraic_power(ast, num) click to toggle source
# 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
algebraic_root(ast, num) click to toggle source
# 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
algebraic_sign(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 80
def algebraic_sign(ast) #=> :int
  VeryLowLevel.Z3_algebraic_sign(_ctx_pointer, ast._ast)
end
algebraic_sub(ast1, ast2) click to toggle source
# 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
apply_result_dec_ref(apply_result) click to toggle source
# 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
apply_result_get_num_subgoals(apply_result) click to toggle source
# 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
apply_result_get_subgoal(apply_result, num) click to toggle source
# 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
apply_result_inc_ref(apply_result) click to toggle source
# 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
apply_result_to_string(apply_result) click to toggle source
# 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
ast_map_contains(ast_map, ast) click to toggle source
# 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
ast_map_dec_ref(ast_map) click to toggle source
# 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
ast_map_erase(ast_map, ast) click to toggle source
# 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
ast_map_find(ast_map, ast) click to toggle source
# 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
ast_map_inc_ref(ast_map) click to toggle source
# 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
ast_map_insert(ast_map, ast1, ast2) click to toggle source
# 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
ast_map_keys(ast_map) click to toggle source
# 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
ast_map_reset(ast_map) click to toggle source
# 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
ast_map_size(ast_map) click to toggle source
# 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
ast_map_to_string(ast_map) click to toggle source
# 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
ast_to_string(ast) click to toggle source
# 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
ast_vector_dec_ref(ast_vector) click to toggle source
# 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
ast_vector_get(ast_vector, num) click to toggle source
# 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
ast_vector_inc_ref(ast_vector) click to toggle source
# 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
ast_vector_push(ast_vector, ast) click to toggle source
# 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
ast_vector_resize(ast_vector, num) click to toggle source
# 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
ast_vector_set(ast_vector, num, ast) click to toggle source
# 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
ast_vector_size(ast_vector) click to toggle source
# 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
ast_vector_to_string(ast_vector) click to toggle source
# 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
ast_vector_translate(ast_vector, context) click to toggle source
# 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
datatype_update_field(func_decl, ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 188
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
dec_ref(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 192
def dec_ref(ast) #=> :void
  VeryLowLevel.Z3_dec_ref(_ctx_pointer, ast._ast)
end
del_config(config) click to toggle source
# File lib/z3/low_level_auto.rb, line 196
def del_config(config) #=> :void
  VeryLowLevel.Z3_del_config(config._config)
end
del_constructor(constructor) click to toggle source
# File lib/z3/low_level_auto.rb, line 200
def del_constructor(constructor) #=> :void
  VeryLowLevel.Z3_del_constructor(_ctx_pointer, constructor._constructor)
end
del_constructor_list(constructor_list) click to toggle source
# File lib/z3/low_level_auto.rb, line 204
def del_constructor_list(constructor_list) #=> :void
  VeryLowLevel.Z3_del_constructor_list(_ctx_pointer, constructor_list._constructor_list)
end
del_context() click to toggle source
# File lib/z3/low_level_auto.rb, line 208
def del_context #=> :void
  VeryLowLevel.Z3_del_context(_ctx_pointer)
end
disable_trace(str) click to toggle source
# File lib/z3/low_level_auto.rb, line 212
def disable_trace(str) #=> :void
  VeryLowLevel.Z3_disable_trace(str)
end
enable_trace(str) click to toggle source
# File lib/z3/low_level_auto.rb, line 216
def enable_trace(str) #=> :void
  VeryLowLevel.Z3_enable_trace(str)
end
eval_smtlib2_string(str) click to toggle source
# File lib/z3/low_level_auto.rb, line 220
def eval_smtlib2_string(str) #=> :string
  VeryLowLevel.Z3_eval_smtlib2_string(_ctx_pointer, str)
end
finalize_memory() click to toggle source
# File lib/z3/low_level_auto.rb, line 224
def finalize_memory #=> :void
  VeryLowLevel.Z3_finalize_memory()
end
fixedpoint_add_cover(fixedpoint, num, func_decl, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 228
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
fixedpoint_add_invariant(fixedpoint, func_decl, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 232
def fixedpoint_add_invariant(fixedpoint, func_decl, ast) #=> :void
  VeryLowLevel.Z3_fixedpoint_add_invariant(_ctx_pointer, fixedpoint._fixedpoint, func_decl._ast, ast._ast)
end
fixedpoint_add_rule(fixedpoint, ast, sym) click to toggle source
# File lib/z3/low_level_auto.rb, line 236
def fixedpoint_add_rule(fixedpoint, ast, sym) #=> :void
  VeryLowLevel.Z3_fixedpoint_add_rule(_ctx_pointer, fixedpoint._fixedpoint, ast._ast, sym)
end
fixedpoint_assert(fixedpoint, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 240
def fixedpoint_assert(fixedpoint, ast) #=> :void
  VeryLowLevel.Z3_fixedpoint_assert(_ctx_pointer, fixedpoint._fixedpoint, ast._ast)
end
fixedpoint_dec_ref(fixedpoint) click to toggle source
# File lib/z3/low_level_auto.rb, line 244
def fixedpoint_dec_ref(fixedpoint) #=> :void
  VeryLowLevel.Z3_fixedpoint_dec_ref(_ctx_pointer, fixedpoint._fixedpoint)
end
fixedpoint_from_file(fixedpoint, str) click to toggle source
# File lib/z3/low_level_auto.rb, line 248
def fixedpoint_from_file(fixedpoint, str) #=> :ast_vector_pointer
  VeryLowLevel.Z3_fixedpoint_from_file(_ctx_pointer, fixedpoint._fixedpoint, str)
end
fixedpoint_from_string(fixedpoint, str) click to toggle source
# File lib/z3/low_level_auto.rb, line 252
def fixedpoint_from_string(fixedpoint, str) #=> :ast_vector_pointer
  VeryLowLevel.Z3_fixedpoint_from_string(_ctx_pointer, fixedpoint._fixedpoint, str)
end
fixedpoint_get_answer(fixedpoint) click to toggle source
# File lib/z3/low_level_auto.rb, line 256
def fixedpoint_get_answer(fixedpoint) #=> :ast_pointer
  VeryLowLevel.Z3_fixedpoint_get_answer(_ctx_pointer, fixedpoint._fixedpoint)
end
fixedpoint_get_assertions(fixedpoint) click to toggle source
# File lib/z3/low_level_auto.rb, line 260
def fixedpoint_get_assertions(fixedpoint) #=> :ast_vector_pointer
  VeryLowLevel.Z3_fixedpoint_get_assertions(_ctx_pointer, fixedpoint._fixedpoint)
end
fixedpoint_get_cover_delta(fixedpoint, num, func_decl) click to toggle source
# File lib/z3/low_level_auto.rb, line 264
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
fixedpoint_get_ground_sat_answer(fixedpoint) click to toggle source
# File lib/z3/low_level_auto.rb, line 268
def fixedpoint_get_ground_sat_answer(fixedpoint) #=> :ast_pointer
  VeryLowLevel.Z3_fixedpoint_get_ground_sat_answer(_ctx_pointer, fixedpoint._fixedpoint)
end
fixedpoint_get_help(fixedpoint) click to toggle source
# File lib/z3/low_level_auto.rb, line 272
def fixedpoint_get_help(fixedpoint) #=> :string
  VeryLowLevel.Z3_fixedpoint_get_help(_ctx_pointer, fixedpoint._fixedpoint)
end
fixedpoint_get_num_levels(fixedpoint, func_decl) click to toggle source
# File lib/z3/low_level_auto.rb, line 276
def fixedpoint_get_num_levels(fixedpoint, func_decl) #=> :uint
  VeryLowLevel.Z3_fixedpoint_get_num_levels(_ctx_pointer, fixedpoint._fixedpoint, func_decl._ast)
end
fixedpoint_get_param_descrs(fixedpoint) click to toggle source
# File lib/z3/low_level_auto.rb, line 280
def fixedpoint_get_param_descrs(fixedpoint) #=> :param_descrs_pointer
  VeryLowLevel.Z3_fixedpoint_get_param_descrs(_ctx_pointer, fixedpoint._fixedpoint)
end
fixedpoint_get_reachable(fixedpoint, func_decl) click to toggle source
# File lib/z3/low_level_auto.rb, line 284
def fixedpoint_get_reachable(fixedpoint, func_decl) #=> :ast_pointer
  VeryLowLevel.Z3_fixedpoint_get_reachable(_ctx_pointer, fixedpoint._fixedpoint, func_decl._ast)
end
fixedpoint_get_reason_unknown(fixedpoint) click to toggle source
# File lib/z3/low_level_auto.rb, line 288
def fixedpoint_get_reason_unknown(fixedpoint) #=> :string
  VeryLowLevel.Z3_fixedpoint_get_reason_unknown(_ctx_pointer, fixedpoint._fixedpoint)
end
fixedpoint_get_rule_names_along_trace(fixedpoint) click to toggle source
# File lib/z3/low_level_auto.rb, line 292
def fixedpoint_get_rule_names_along_trace(fixedpoint) #=> :symbol_pointer
  VeryLowLevel.Z3_fixedpoint_get_rule_names_along_trace(_ctx_pointer, fixedpoint._fixedpoint)
end
fixedpoint_get_rules(fixedpoint) click to toggle source
# File lib/z3/low_level_auto.rb, line 296
def fixedpoint_get_rules(fixedpoint) #=> :ast_vector_pointer
  VeryLowLevel.Z3_fixedpoint_get_rules(_ctx_pointer, fixedpoint._fixedpoint)
end
fixedpoint_get_rules_along_trace(fixedpoint) click to toggle source
# File lib/z3/low_level_auto.rb, line 300
def fixedpoint_get_rules_along_trace(fixedpoint) #=> :ast_vector_pointer
  VeryLowLevel.Z3_fixedpoint_get_rules_along_trace(_ctx_pointer, fixedpoint._fixedpoint)
end
fixedpoint_get_statistics(fixedpoint) click to toggle source
# File lib/z3/low_level_auto.rb, line 304
def fixedpoint_get_statistics(fixedpoint) #=> :stats_pointer
  VeryLowLevel.Z3_fixedpoint_get_statistics(_ctx_pointer, fixedpoint._fixedpoint)
end
fixedpoint_inc_ref(fixedpoint) click to toggle source
# File lib/z3/low_level_auto.rb, line 308
def fixedpoint_inc_ref(fixedpoint) #=> :void
  VeryLowLevel.Z3_fixedpoint_inc_ref(_ctx_pointer, fixedpoint._fixedpoint)
end
fixedpoint_query(fixedpoint, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 312
def fixedpoint_query(fixedpoint, ast) #=> :int
  VeryLowLevel.Z3_fixedpoint_query(_ctx_pointer, fixedpoint._fixedpoint, ast._ast)
end
fixedpoint_query_from_lvl(fixedpoint, ast, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 316
def fixedpoint_query_from_lvl(fixedpoint, ast, num) #=> :int
  VeryLowLevel.Z3_fixedpoint_query_from_lvl(_ctx_pointer, fixedpoint._fixedpoint, ast._ast, num)
end
fixedpoint_register_relation(fixedpoint, func_decl) click to toggle source
# File lib/z3/low_level_auto.rb, line 320
def fixedpoint_register_relation(fixedpoint, func_decl) #=> :void
  VeryLowLevel.Z3_fixedpoint_register_relation(_ctx_pointer, fixedpoint._fixedpoint, func_decl._ast)
end
fixedpoint_set_params(fixedpoint, params) click to toggle source
# File lib/z3/low_level_auto.rb, line 324
def fixedpoint_set_params(fixedpoint, params) #=> :void
  VeryLowLevel.Z3_fixedpoint_set_params(_ctx_pointer, fixedpoint._fixedpoint, params._params)
end
fixedpoint_update_rule(fixedpoint, ast, sym) click to toggle source
# File lib/z3/low_level_auto.rb, line 328
def fixedpoint_update_rule(fixedpoint, ast, sym) #=> :void
  VeryLowLevel.Z3_fixedpoint_update_rule(_ctx_pointer, fixedpoint._fixedpoint, ast._ast, sym)
end
fpa_get_ebits(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 332
def fpa_get_ebits(sort) #=> :uint
  VeryLowLevel.Z3_fpa_get_ebits(_ctx_pointer, sort._ast)
end
fpa_get_numeral_exponent_bv(ast, bool) click to toggle source
# File lib/z3/low_level_auto.rb, line 336
def fpa_get_numeral_exponent_bv(ast, bool) #=> :ast_pointer
  VeryLowLevel.Z3_fpa_get_numeral_exponent_bv(_ctx_pointer, ast._ast, bool)
end
fpa_get_numeral_exponent_string(ast, bool) click to toggle source
# File lib/z3/low_level_auto.rb, line 340
def fpa_get_numeral_exponent_string(ast, bool) #=> :string
  VeryLowLevel.Z3_fpa_get_numeral_exponent_string(_ctx_pointer, ast._ast, bool)
end
fpa_get_numeral_sign_bv(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 344
def fpa_get_numeral_sign_bv(ast) #=> :ast_pointer
  VeryLowLevel.Z3_fpa_get_numeral_sign_bv(_ctx_pointer, ast._ast)
end
fpa_get_numeral_significand_bv(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 348
def fpa_get_numeral_significand_bv(ast) #=> :ast_pointer
  VeryLowLevel.Z3_fpa_get_numeral_significand_bv(_ctx_pointer, ast._ast)
end
fpa_get_numeral_significand_string(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 352
def fpa_get_numeral_significand_string(ast) #=> :string
  VeryLowLevel.Z3_fpa_get_numeral_significand_string(_ctx_pointer, ast._ast)
end
fpa_get_sbits(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 356
def fpa_get_sbits(sort) #=> :uint
  VeryLowLevel.Z3_fpa_get_sbits(_ctx_pointer, sort._ast)
end
fpa_is_numeral_inf(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 360
def fpa_is_numeral_inf(ast) #=> :bool
  VeryLowLevel.Z3_fpa_is_numeral_inf(_ctx_pointer, ast._ast)
end
fpa_is_numeral_nan(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 364
def fpa_is_numeral_nan(ast) #=> :bool
  VeryLowLevel.Z3_fpa_is_numeral_nan(_ctx_pointer, ast._ast)
end
fpa_is_numeral_negative(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 368
def fpa_is_numeral_negative(ast) #=> :bool
  VeryLowLevel.Z3_fpa_is_numeral_negative(_ctx_pointer, ast._ast)
end
fpa_is_numeral_normal(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 372
def fpa_is_numeral_normal(ast) #=> :bool
  VeryLowLevel.Z3_fpa_is_numeral_normal(_ctx_pointer, ast._ast)
end
fpa_is_numeral_positive(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 376
def fpa_is_numeral_positive(ast) #=> :bool
  VeryLowLevel.Z3_fpa_is_numeral_positive(_ctx_pointer, ast._ast)
end
fpa_is_numeral_subnormal(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 380
def fpa_is_numeral_subnormal(ast) #=> :bool
  VeryLowLevel.Z3_fpa_is_numeral_subnormal(_ctx_pointer, ast._ast)
end
fpa_is_numeral_zero(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 384
def fpa_is_numeral_zero(ast) #=> :bool
  VeryLowLevel.Z3_fpa_is_numeral_zero(_ctx_pointer, ast._ast)
end
func_entry_dec_ref(func_entry) click to toggle source
# File lib/z3/low_level_auto.rb, line 388
def func_entry_dec_ref(func_entry) #=> :void
  VeryLowLevel.Z3_func_entry_dec_ref(_ctx_pointer, func_entry._func_entry)
end
func_entry_get_arg(func_entry, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 392
def func_entry_get_arg(func_entry, num) #=> :ast_pointer
  VeryLowLevel.Z3_func_entry_get_arg(_ctx_pointer, func_entry._func_entry, num)
end
func_entry_get_num_args(func_entry) click to toggle source
# File lib/z3/low_level_auto.rb, line 396
def func_entry_get_num_args(func_entry) #=> :uint
  VeryLowLevel.Z3_func_entry_get_num_args(_ctx_pointer, func_entry._func_entry)
end
func_entry_get_value(func_entry) click to toggle source
# File lib/z3/low_level_auto.rb, line 400
def func_entry_get_value(func_entry) #=> :ast_pointer
  VeryLowLevel.Z3_func_entry_get_value(_ctx_pointer, func_entry._func_entry)
end
func_entry_inc_ref(func_entry) click to toggle source
# File lib/z3/low_level_auto.rb, line 404
def func_entry_inc_ref(func_entry) #=> :void
  VeryLowLevel.Z3_func_entry_inc_ref(_ctx_pointer, func_entry._func_entry)
end
func_interp_add_entry(func_interp, ast_vector, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 408
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
func_interp_dec_ref(func_interp) click to toggle source
# File lib/z3/low_level_auto.rb, line 412
def func_interp_dec_ref(func_interp) #=> :void
  VeryLowLevel.Z3_func_interp_dec_ref(_ctx_pointer, func_interp._func_interp)
end
func_interp_get_arity(func_interp) click to toggle source
# File lib/z3/low_level_auto.rb, line 416
def func_interp_get_arity(func_interp) #=> :uint
  VeryLowLevel.Z3_func_interp_get_arity(_ctx_pointer, func_interp._func_interp)
end
func_interp_get_else(func_interp) click to toggle source
# File lib/z3/low_level_auto.rb, line 420
def func_interp_get_else(func_interp) #=> :ast_pointer
  VeryLowLevel.Z3_func_interp_get_else(_ctx_pointer, func_interp._func_interp)
end
func_interp_get_entry(func_interp, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 424
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
func_interp_get_num_entries(func_interp) click to toggle source
# File lib/z3/low_level_auto.rb, line 428
def func_interp_get_num_entries(func_interp) #=> :uint
  VeryLowLevel.Z3_func_interp_get_num_entries(_ctx_pointer, func_interp._func_interp)
end
func_interp_inc_ref(func_interp) click to toggle source
# File lib/z3/low_level_auto.rb, line 432
def func_interp_inc_ref(func_interp) #=> :void
  VeryLowLevel.Z3_func_interp_inc_ref(_ctx_pointer, func_interp._func_interp)
end
func_interp_set_else(func_interp, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 436
def func_interp_set_else(func_interp, ast) #=> :void
  VeryLowLevel.Z3_func_interp_set_else(_ctx_pointer, func_interp._func_interp, ast._ast)
end
get_algebraic_number_lower(ast, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 440
def get_algebraic_number_lower(ast, num) #=> :ast_pointer
  VeryLowLevel.Z3_get_algebraic_number_lower(_ctx_pointer, ast._ast, num)
end
get_algebraic_number_upper(ast, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 444
def get_algebraic_number_upper(ast, num) #=> :ast_pointer
  VeryLowLevel.Z3_get_algebraic_number_upper(_ctx_pointer, ast._ast, num)
end
get_app_arg(app, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 448
def get_app_arg(app, num) #=> :ast_pointer
  VeryLowLevel.Z3_get_app_arg(_ctx_pointer, app._ast, num)
end
get_app_decl(app) click to toggle source
# File lib/z3/low_level_auto.rb, line 452
def get_app_decl(app) #=> :func_decl_pointer
  VeryLowLevel.Z3_get_app_decl(_ctx_pointer, app._ast)
end
get_app_num_args(app) click to toggle source
# File lib/z3/low_level_auto.rb, line 456
def get_app_num_args(app) #=> :uint
  VeryLowLevel.Z3_get_app_num_args(_ctx_pointer, app._ast)
end
get_arity(func_decl) click to toggle source
# File lib/z3/low_level_auto.rb, line 460
def get_arity(func_decl) #=> :uint
  VeryLowLevel.Z3_get_arity(_ctx_pointer, func_decl._ast)
end
get_array_sort_domain(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 464
def get_array_sort_domain(sort) #=> :sort_pointer
  VeryLowLevel.Z3_get_array_sort_domain(_ctx_pointer, sort._ast)
end
get_array_sort_range(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 468
def get_array_sort_range(sort) #=> :sort_pointer
  VeryLowLevel.Z3_get_array_sort_range(_ctx_pointer, sort._ast)
end
get_as_array_func_decl(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 472
def get_as_array_func_decl(ast) #=> :func_decl_pointer
  VeryLowLevel.Z3_get_as_array_func_decl(_ctx_pointer, ast._ast)
end
get_ast_hash(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 476
def get_ast_hash(ast) #=> :uint
  VeryLowLevel.Z3_get_ast_hash(_ctx_pointer, ast._ast)
end
get_ast_id(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 480
def get_ast_id(ast) #=> :uint
  VeryLowLevel.Z3_get_ast_id(_ctx_pointer, ast._ast)
end
get_ast_kind(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 484
def get_ast_kind(ast) #=> :uint
  VeryLowLevel.Z3_get_ast_kind(_ctx_pointer, ast._ast)
end
get_bool_value(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 488
def get_bool_value(ast) #=> :int
  VeryLowLevel.Z3_get_bool_value(_ctx_pointer, ast._ast)
end
get_bv_sort_size(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 492
def get_bv_sort_size(sort) #=> :uint
  VeryLowLevel.Z3_get_bv_sort_size(_ctx_pointer, sort._ast)
end
get_datatype_sort_constructor(sort, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 496
def get_datatype_sort_constructor(sort, num) #=> :func_decl_pointer
  VeryLowLevel.Z3_get_datatype_sort_constructor(_ctx_pointer, sort._ast, num)
end
get_datatype_sort_constructor_accessor(sort, num1, num2) click to toggle source
# File lib/z3/low_level_auto.rb, line 500
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
get_datatype_sort_num_constructors(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 504
def get_datatype_sort_num_constructors(sort) #=> :uint
  VeryLowLevel.Z3_get_datatype_sort_num_constructors(_ctx_pointer, sort._ast)
end
get_datatype_sort_recognizer(sort, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 508
def get_datatype_sort_recognizer(sort, num) #=> :func_decl_pointer
  VeryLowLevel.Z3_get_datatype_sort_recognizer(_ctx_pointer, sort._ast, num)
end
get_decl_ast_parameter(func_decl, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 512
def get_decl_ast_parameter(func_decl, num) #=> :ast_pointer
  VeryLowLevel.Z3_get_decl_ast_parameter(_ctx_pointer, func_decl._ast, num)
end
get_decl_double_parameter(func_decl, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 516
def get_decl_double_parameter(func_decl, num) #=> :double
  VeryLowLevel.Z3_get_decl_double_parameter(_ctx_pointer, func_decl._ast, num)
end
get_decl_func_decl_parameter(func_decl, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 520
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
get_decl_int_parameter(func_decl, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 524
def get_decl_int_parameter(func_decl, num) #=> :int
  VeryLowLevel.Z3_get_decl_int_parameter(_ctx_pointer, func_decl._ast, num)
end
get_decl_kind(func_decl) click to toggle source
# File lib/z3/low_level_auto.rb, line 528
def get_decl_kind(func_decl) #=> :uint
  VeryLowLevel.Z3_get_decl_kind(_ctx_pointer, func_decl._ast)
end
get_decl_name(func_decl) click to toggle source
# File lib/z3/low_level_auto.rb, line 532
def get_decl_name(func_decl) #=> :symbol_pointer
  VeryLowLevel.Z3_get_decl_name(_ctx_pointer, func_decl._ast)
end
get_decl_num_parameters(func_decl) click to toggle source
# File lib/z3/low_level_auto.rb, line 536
def get_decl_num_parameters(func_decl) #=> :uint
  VeryLowLevel.Z3_get_decl_num_parameters(_ctx_pointer, func_decl._ast)
end
get_decl_parameter_kind(func_decl, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 540
def get_decl_parameter_kind(func_decl, num) #=> :uint
  VeryLowLevel.Z3_get_decl_parameter_kind(_ctx_pointer, func_decl._ast, num)
end
get_decl_rational_parameter(func_decl, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 544
def get_decl_rational_parameter(func_decl, num) #=> :string
  VeryLowLevel.Z3_get_decl_rational_parameter(_ctx_pointer, func_decl._ast, num)
end
get_decl_sort_parameter(func_decl, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 548
def get_decl_sort_parameter(func_decl, num) #=> :sort_pointer
  VeryLowLevel.Z3_get_decl_sort_parameter(_ctx_pointer, func_decl._ast, num)
end
get_decl_symbol_parameter(func_decl, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 552
def get_decl_symbol_parameter(func_decl, num) #=> :symbol_pointer
  VeryLowLevel.Z3_get_decl_symbol_parameter(_ctx_pointer, func_decl._ast, num)
end
get_denominator(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 556
def get_denominator(ast) #=> :ast_pointer
  VeryLowLevel.Z3_get_denominator(_ctx_pointer, ast._ast)
end
get_domain(func_decl, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 560
def get_domain(func_decl, num) #=> :sort_pointer
  VeryLowLevel.Z3_get_domain(_ctx_pointer, func_decl._ast, num)
end
get_domain_size(func_decl) click to toggle source
# File lib/z3/low_level_auto.rb, line 564
def get_domain_size(func_decl) #=> :uint
  VeryLowLevel.Z3_get_domain_size(_ctx_pointer, func_decl._ast)
end
get_error_code() click to toggle source
# File lib/z3/low_level_auto.rb, line 568
def get_error_code #=> :uint
  VeryLowLevel.Z3_get_error_code(_ctx_pointer)
end
get_full_version() click to toggle source
# File lib/z3/low_level_auto.rb, line 572
def get_full_version #=> :string
  VeryLowLevel.Z3_get_full_version()
end
get_func_decl_id(func_decl) click to toggle source
# File lib/z3/low_level_auto.rb, line 576
def get_func_decl_id(func_decl) #=> :uint
  VeryLowLevel.Z3_get_func_decl_id(_ctx_pointer, func_decl._ast)
end
get_index_value(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 580
def get_index_value(ast) #=> :uint
  VeryLowLevel.Z3_get_index_value(_ctx_pointer, ast._ast)
end
get_num_probes() click to toggle source
# File lib/z3/low_level_auto.rb, line 584
def get_num_probes #=> :uint
  VeryLowLevel.Z3_get_num_probes(_ctx_pointer)
end
get_num_tactics() click to toggle source
# File lib/z3/low_level_auto.rb, line 588
def get_num_tactics #=> :uint
  VeryLowLevel.Z3_get_num_tactics(_ctx_pointer)
end
get_numeral_binary_string(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 592
def get_numeral_binary_string(ast) #=> :string
  VeryLowLevel.Z3_get_numeral_binary_string(_ctx_pointer, ast._ast)
end
get_numeral_decimal_string(ast, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 596
def get_numeral_decimal_string(ast, num) #=> :string
  VeryLowLevel.Z3_get_numeral_decimal_string(_ctx_pointer, ast._ast, num)
end
get_numeral_double(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 600
def get_numeral_double(ast) #=> :double
  VeryLowLevel.Z3_get_numeral_double(_ctx_pointer, ast._ast)
end
get_numeral_string(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 604
def get_numeral_string(ast) #=> :string
  VeryLowLevel.Z3_get_numeral_string(_ctx_pointer, ast._ast)
end
get_numerator(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 608
def get_numerator(ast) #=> :ast_pointer
  VeryLowLevel.Z3_get_numerator(_ctx_pointer, ast._ast)
end
get_pattern(pattern, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 612
def get_pattern(pattern, num) #=> :ast_pointer
  VeryLowLevel.Z3_get_pattern(_ctx_pointer, pattern._ast, num)
end
get_pattern_num_terms(pattern) click to toggle source
# File lib/z3/low_level_auto.rb, line 616
def get_pattern_num_terms(pattern) #=> :uint
  VeryLowLevel.Z3_get_pattern_num_terms(_ctx_pointer, pattern._ast)
end
get_probe_name(num) click to toggle source
# File lib/z3/low_level_auto.rb, line 620
def get_probe_name(num) #=> :string
  VeryLowLevel.Z3_get_probe_name(_ctx_pointer, num)
end
get_quantifier_body(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 624
def get_quantifier_body(ast) #=> :ast_pointer
  VeryLowLevel.Z3_get_quantifier_body(_ctx_pointer, ast._ast)
end
get_quantifier_bound_name(ast, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 628
def get_quantifier_bound_name(ast, num) #=> :symbol_pointer
  VeryLowLevel.Z3_get_quantifier_bound_name(_ctx_pointer, ast._ast, num)
end
get_quantifier_bound_sort(ast, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 632
def get_quantifier_bound_sort(ast, num) #=> :sort_pointer
  VeryLowLevel.Z3_get_quantifier_bound_sort(_ctx_pointer, ast._ast, num)
end
get_quantifier_no_pattern_ast(ast, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 636
def get_quantifier_no_pattern_ast(ast, num) #=> :ast_pointer
  VeryLowLevel.Z3_get_quantifier_no_pattern_ast(_ctx_pointer, ast._ast, num)
end
get_quantifier_num_bound(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 640
def get_quantifier_num_bound(ast) #=> :uint
  VeryLowLevel.Z3_get_quantifier_num_bound(_ctx_pointer, ast._ast)
end
get_quantifier_num_no_patterns(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 644
def get_quantifier_num_no_patterns(ast) #=> :uint
  VeryLowLevel.Z3_get_quantifier_num_no_patterns(_ctx_pointer, ast._ast)
end
get_quantifier_num_patterns(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 648
def get_quantifier_num_patterns(ast) #=> :uint
  VeryLowLevel.Z3_get_quantifier_num_patterns(_ctx_pointer, ast._ast)
end
get_quantifier_pattern_ast(ast, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 652
def get_quantifier_pattern_ast(ast, num) #=> :pattern_pointer
  VeryLowLevel.Z3_get_quantifier_pattern_ast(_ctx_pointer, ast._ast, num)
end
get_quantifier_weight(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 656
def get_quantifier_weight(ast) #=> :uint
  VeryLowLevel.Z3_get_quantifier_weight(_ctx_pointer, ast._ast)
end
get_range(func_decl) click to toggle source
# File lib/z3/low_level_auto.rb, line 660
def get_range(func_decl) #=> :sort_pointer
  VeryLowLevel.Z3_get_range(_ctx_pointer, func_decl._ast)
end
get_re_sort_basis(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 664
def get_re_sort_basis(sort) #=> :sort_pointer
  VeryLowLevel.Z3_get_re_sort_basis(_ctx_pointer, sort._ast)
end
get_relation_arity(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 668
def get_relation_arity(sort) #=> :uint
  VeryLowLevel.Z3_get_relation_arity(_ctx_pointer, sort._ast)
end
get_relation_column(sort, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 672
def get_relation_column(sort, num) #=> :sort_pointer
  VeryLowLevel.Z3_get_relation_column(_ctx_pointer, sort._ast, num)
end
get_seq_sort_basis(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 676
def get_seq_sort_basis(sort) #=> :sort_pointer
  VeryLowLevel.Z3_get_seq_sort_basis(_ctx_pointer, sort._ast)
end
get_sort(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 680
def get_sort(ast) #=> :sort_pointer
  VeryLowLevel.Z3_get_sort(_ctx_pointer, ast._ast)
end
get_sort_id(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 684
def get_sort_id(sort) #=> :uint
  VeryLowLevel.Z3_get_sort_id(_ctx_pointer, sort._ast)
end
get_sort_kind(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 688
def get_sort_kind(sort) #=> :uint
  VeryLowLevel.Z3_get_sort_kind(_ctx_pointer, sort._ast)
end
get_sort_name(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 692
def get_sort_name(sort) #=> :symbol_pointer
  VeryLowLevel.Z3_get_sort_name(_ctx_pointer, sort._ast)
end
get_string_length(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 696
def get_string_length(ast) #=> :uint
  VeryLowLevel.Z3_get_string_length(_ctx_pointer, ast._ast)
end
get_symbol_int(sym) click to toggle source
# File lib/z3/low_level_auto.rb, line 700
def get_symbol_int(sym) #=> :int
  VeryLowLevel.Z3_get_symbol_int(_ctx_pointer, sym)
end
get_symbol_kind(sym) click to toggle source
# File lib/z3/low_level_auto.rb, line 704
def get_symbol_kind(sym) #=> :uint
  VeryLowLevel.Z3_get_symbol_kind(_ctx_pointer, sym)
end
get_symbol_string(sym) click to toggle source
# File lib/z3/low_level_auto.rb, line 708
def get_symbol_string(sym) #=> :string
  VeryLowLevel.Z3_get_symbol_string(_ctx_pointer, sym)
end
get_tactic_name(num) click to toggle source
# File lib/z3/low_level_auto.rb, line 712
def get_tactic_name(num) #=> :string
  VeryLowLevel.Z3_get_tactic_name(_ctx_pointer, num)
end
get_tuple_sort_field_decl(sort, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 716
def get_tuple_sort_field_decl(sort, num) #=> :func_decl_pointer
  VeryLowLevel.Z3_get_tuple_sort_field_decl(_ctx_pointer, sort._ast, num)
end
get_tuple_sort_mk_decl(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 720
def get_tuple_sort_mk_decl(sort) #=> :func_decl_pointer
  VeryLowLevel.Z3_get_tuple_sort_mk_decl(_ctx_pointer, sort._ast)
end
get_tuple_sort_num_fields(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 724
def get_tuple_sort_num_fields(sort) #=> :uint
  VeryLowLevel.Z3_get_tuple_sort_num_fields(_ctx_pointer, sort._ast)
end
get_version() click to toggle source
# File lib/z3/low_level.rb, line 7
def get_version
  a = FFI::MemoryPointer.new(:int)
  b = FFI::MemoryPointer.new(:int)
  c = FFI::MemoryPointer.new(:int)
  d = FFI::MemoryPointer.new(:int)
  Z3::VeryLowLevel.Z3_get_version(a, b, c, d)
  [a.get_uint(0), b.get_uint(0), c.get_uint(0), d.get_uint(0)]
end
global_param_reset_all() click to toggle source
# File lib/z3/low_level_auto.rb, line 728
def global_param_reset_all #=> :void
  VeryLowLevel.Z3_global_param_reset_all()
end
global_param_set(str1, str2) click to toggle source
# File lib/z3/low_level_auto.rb, line 732
def global_param_set(str1, str2) #=> :void
  VeryLowLevel.Z3_global_param_set(str1, str2)
end
goal_assert(goal, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 736
def goal_assert(goal, ast) #=> :void
  VeryLowLevel.Z3_goal_assert(_ctx_pointer, goal._goal, ast._ast)
end
goal_convert_model(goal, model) click to toggle source
# File lib/z3/low_level_auto.rb, line 740
def goal_convert_model(goal, model) #=> :model_pointer
  VeryLowLevel.Z3_goal_convert_model(_ctx_pointer, goal._goal, model._model)
end
goal_dec_ref(goal) click to toggle source
# File lib/z3/low_level_auto.rb, line 744
def goal_dec_ref(goal) #=> :void
  VeryLowLevel.Z3_goal_dec_ref(_ctx_pointer, goal._goal)
end
goal_depth(goal) click to toggle source
# File lib/z3/low_level_auto.rb, line 748
def goal_depth(goal) #=> :uint
  VeryLowLevel.Z3_goal_depth(_ctx_pointer, goal._goal)
end
goal_formula(goal, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 752
def goal_formula(goal, num) #=> :ast_pointer
  VeryLowLevel.Z3_goal_formula(_ctx_pointer, goal._goal, num)
end
goal_inc_ref(goal) click to toggle source
# File lib/z3/low_level_auto.rb, line 756
def goal_inc_ref(goal) #=> :void
  VeryLowLevel.Z3_goal_inc_ref(_ctx_pointer, goal._goal)
end
goal_inconsistent(goal) click to toggle source
# File lib/z3/low_level_auto.rb, line 760
def goal_inconsistent(goal) #=> :bool
  VeryLowLevel.Z3_goal_inconsistent(_ctx_pointer, goal._goal)
end
goal_is_decided_sat(goal) click to toggle source
# File lib/z3/low_level_auto.rb, line 764
def goal_is_decided_sat(goal) #=> :bool
  VeryLowLevel.Z3_goal_is_decided_sat(_ctx_pointer, goal._goal)
end
goal_is_decided_unsat(goal) click to toggle source
# File lib/z3/low_level_auto.rb, line 768
def goal_is_decided_unsat(goal) #=> :bool
  VeryLowLevel.Z3_goal_is_decided_unsat(_ctx_pointer, goal._goal)
end
goal_num_exprs(goal) click to toggle source
# File lib/z3/low_level_auto.rb, line 772
def goal_num_exprs(goal) #=> :uint
  VeryLowLevel.Z3_goal_num_exprs(_ctx_pointer, goal._goal)
end
goal_precision(goal) click to toggle source
# File lib/z3/low_level_auto.rb, line 776
def goal_precision(goal) #=> :uint
  VeryLowLevel.Z3_goal_precision(_ctx_pointer, goal._goal)
end
goal_reset(goal) click to toggle source
# File lib/z3/low_level_auto.rb, line 780
def goal_reset(goal) #=> :void
  VeryLowLevel.Z3_goal_reset(_ctx_pointer, goal._goal)
end
goal_size(goal) click to toggle source
# File lib/z3/low_level_auto.rb, line 784
def goal_size(goal) #=> :uint
  VeryLowLevel.Z3_goal_size(_ctx_pointer, goal._goal)
end
goal_to_dimacs_string(goal, bool) click to toggle source
# File lib/z3/low_level_auto.rb, line 788
def goal_to_dimacs_string(goal, bool) #=> :string
  VeryLowLevel.Z3_goal_to_dimacs_string(_ctx_pointer, goal._goal, bool)
end
goal_to_string(goal) click to toggle source
# File lib/z3/low_level_auto.rb, line 792
def goal_to_string(goal) #=> :string
  VeryLowLevel.Z3_goal_to_string(_ctx_pointer, goal._goal)
end
goal_translate(goal, context) click to toggle source
# File lib/z3/low_level_auto.rb, line 796
def goal_translate(goal, context) #=> :goal_pointer
  VeryLowLevel.Z3_goal_translate(_ctx_pointer, goal._goal, context._context)
end
inc_ref(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 800
def inc_ref(ast) #=> :void
  VeryLowLevel.Z3_inc_ref(_ctx_pointer, ast._ast)
end
interrupt() click to toggle source
# File lib/z3/low_level_auto.rb, line 804
def interrupt #=> :void
  VeryLowLevel.Z3_interrupt(_ctx_pointer)
end
is_algebraic_number(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 808
def is_algebraic_number(ast) #=> :bool
  VeryLowLevel.Z3_is_algebraic_number(_ctx_pointer, ast._ast)
end
is_app(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 812
def is_app(ast) #=> :bool
  VeryLowLevel.Z3_is_app(_ctx_pointer, ast._ast)
end
is_as_array(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 816
def is_as_array(ast) #=> :bool
  VeryLowLevel.Z3_is_as_array(_ctx_pointer, ast._ast)
end
is_char_sort(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 820
def is_char_sort(sort) #=> :bool
  VeryLowLevel.Z3_is_char_sort(_ctx_pointer, sort._ast)
end
is_eq_ast(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 824
def is_eq_ast(ast1, ast2) #=> :bool
  VeryLowLevel.Z3_is_eq_ast(_ctx_pointer, ast1._ast, ast2._ast)
end
is_eq_func_decl(func_decl1, func_decl2) click to toggle source
# File lib/z3/low_level_auto.rb, line 828
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
is_eq_sort(sort1, sort2) click to toggle source
# File lib/z3/low_level_auto.rb, line 832
def is_eq_sort(sort1, sort2) #=> :bool
  VeryLowLevel.Z3_is_eq_sort(_ctx_pointer, sort1._ast, sort2._ast)
end
is_lambda(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 836
def is_lambda(ast) #=> :bool
  VeryLowLevel.Z3_is_lambda(_ctx_pointer, ast._ast)
end
is_numeral_ast(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 840
def is_numeral_ast(ast) #=> :bool
  VeryLowLevel.Z3_is_numeral_ast(_ctx_pointer, ast._ast)
end
is_quantifier_exists(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 844
def is_quantifier_exists(ast) #=> :bool
  VeryLowLevel.Z3_is_quantifier_exists(_ctx_pointer, ast._ast)
end
is_quantifier_forall(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 848
def is_quantifier_forall(ast) #=> :bool
  VeryLowLevel.Z3_is_quantifier_forall(_ctx_pointer, ast._ast)
end
is_well_sorted(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 852
def is_well_sorted(ast) #=> :bool
  VeryLowLevel.Z3_is_well_sorted(_ctx_pointer, ast._ast)
end
mk_add(asts) click to toggle source
# File lib/z3/low_level.rb, line 46
def mk_add(asts)
  Z3::VeryLowLevel.Z3_mk_add(_ctx_pointer, asts.size, asts_vector(asts))
end
mk_and(asts) click to toggle source
# File lib/z3/low_level.rb, line 34
def mk_and(asts)
  Z3::VeryLowLevel.Z3_mk_and(_ctx_pointer, asts.size, asts_vector(asts))
end
mk_array_default(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 856
def mk_array_default(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_array_default(_ctx_pointer, ast._ast)
end
mk_array_sort(sort1, sort2) click to toggle source
# File lib/z3/low_level_auto.rb, line 860
def mk_array_sort(sort1, sort2) #=> :sort_pointer
  VeryLowLevel.Z3_mk_array_sort(_ctx_pointer, sort1._ast, sort2._ast)
end
mk_as_array(func_decl) click to toggle source
# File lib/z3/low_level_auto.rb, line 864
def mk_as_array(func_decl) #=> :ast_pointer
  VeryLowLevel.Z3_mk_as_array(_ctx_pointer, func_decl._ast)
end
mk_ast_map() click to toggle source
# File lib/z3/low_level_auto.rb, line 868
def mk_ast_map #=> :ast_map_pointer
  VeryLowLevel.Z3_mk_ast_map(_ctx_pointer)
end
mk_ast_vector() click to toggle source
# File lib/z3/low_level_auto.rb, line 872
def mk_ast_vector #=> :ast_vector_pointer
  VeryLowLevel.Z3_mk_ast_vector(_ctx_pointer)
end
mk_bool_sort() click to toggle source
# File lib/z3/low_level_auto.rb, line 876
def mk_bool_sort #=> :sort_pointer
  VeryLowLevel.Z3_mk_bool_sort(_ctx_pointer)
end
mk_bound(num, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 880
def mk_bound(num, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bound(_ctx_pointer, num, sort._ast)
end
mk_bv2int(ast, bool) click to toggle source
# File lib/z3/low_level_auto.rb, line 884
def mk_bv2int(ast, bool) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bv2int(_ctx_pointer, ast._ast, bool)
end
mk_bv_sort(num) click to toggle source
# File lib/z3/low_level_auto.rb, line 888
def mk_bv_sort(num) #=> :sort_pointer
  VeryLowLevel.Z3_mk_bv_sort(_ctx_pointer, num)
end
mk_bvadd(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 892
def mk_bvadd(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvadd(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvadd_no_overflow(ast1, ast2, bool) click to toggle source
# File lib/z3/low_level_auto.rb, line 896
def mk_bvadd_no_overflow(ast1, ast2, bool) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvadd_no_overflow(_ctx_pointer, ast1._ast, ast2._ast, bool)
end
mk_bvadd_no_underflow(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 900
def mk_bvadd_no_underflow(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvadd_no_underflow(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvand(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 904
def mk_bvand(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvand(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvashr(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 908
def mk_bvashr(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvashr(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvlshr(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 912
def mk_bvlshr(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvlshr(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvmul(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 916
def mk_bvmul(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvmul(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvmul_no_overflow(ast1, ast2, bool) click to toggle source
# File lib/z3/low_level_auto.rb, line 920
def mk_bvmul_no_overflow(ast1, ast2, bool) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvmul_no_overflow(_ctx_pointer, ast1._ast, ast2._ast, bool)
end
mk_bvmul_no_underflow(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 924
def mk_bvmul_no_underflow(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvmul_no_underflow(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvnand(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 928
def mk_bvnand(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvnand(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvneg(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 932
def mk_bvneg(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvneg(_ctx_pointer, ast._ast)
end
mk_bvneg_no_overflow(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 936
def mk_bvneg_no_overflow(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvneg_no_overflow(_ctx_pointer, ast._ast)
end
mk_bvnor(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 940
def mk_bvnor(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvnor(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvnot(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 944
def mk_bvnot(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvnot(_ctx_pointer, ast._ast)
end
mk_bvor(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 948
def mk_bvor(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvor(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvredand(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 952
def mk_bvredand(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvredand(_ctx_pointer, ast._ast)
end
mk_bvredor(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 956
def mk_bvredor(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvredor(_ctx_pointer, ast._ast)
end
mk_bvsdiv(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 960
def mk_bvsdiv(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsdiv(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvsdiv_no_overflow(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 964
def mk_bvsdiv_no_overflow(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsdiv_no_overflow(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvsge(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 968
def mk_bvsge(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsge(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvsgt(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 972
def mk_bvsgt(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsgt(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvshl(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 976
def mk_bvshl(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvshl(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvsle(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 980
def mk_bvsle(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsle(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvslt(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 984
def mk_bvslt(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvslt(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvsmod(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 988
def mk_bvsmod(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsmod(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvsrem(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 992
def mk_bvsrem(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsrem(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvsub(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 996
def mk_bvsub(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsub(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvsub_no_overflow(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1000
def mk_bvsub_no_overflow(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsub_no_overflow(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvsub_no_underflow(ast1, ast2, bool) click to toggle source
# File lib/z3/low_level_auto.rb, line 1004
def mk_bvsub_no_underflow(ast1, ast2, bool) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvsub_no_underflow(_ctx_pointer, ast1._ast, ast2._ast, bool)
end
mk_bvudiv(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1008
def mk_bvudiv(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvudiv(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvuge(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1012
def mk_bvuge(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvuge(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvugt(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1016
def mk_bvugt(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvugt(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvule(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1020
def mk_bvule(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvule(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvult(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1024
def mk_bvult(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvult(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvurem(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1028
def mk_bvurem(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvurem(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvxnor(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1032
def mk_bvxnor(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvxnor(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_bvxor(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1036
def mk_bvxor(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_bvxor(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_char_from_bv(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1040
def mk_char_from_bv(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_char_from_bv(_ctx_pointer, ast._ast)
end
mk_char_is_digit(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1044
def mk_char_is_digit(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_char_is_digit(_ctx_pointer, ast._ast)
end
mk_char_le(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1048
def mk_char_le(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_char_le(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_char_sort() click to toggle source
# File lib/z3/low_level_auto.rb, line 1052
def mk_char_sort #=> :sort_pointer
  VeryLowLevel.Z3_mk_char_sort(_ctx_pointer)
end
mk_char_to_bv(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1056
def mk_char_to_bv(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_char_to_bv(_ctx_pointer, ast._ast)
end
mk_char_to_int(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1060
def mk_char_to_int(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_char_to_int(_ctx_pointer, ast._ast)
end
mk_concat(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1064
def mk_concat(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_concat(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_config() click to toggle source
# File lib/z3/low_level_auto.rb, line 1068
def mk_config #=> :config_pointer
  VeryLowLevel.Z3_mk_config()
end
mk_const(sym, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1072
def mk_const(sym, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_const(_ctx_pointer, sym, sort._ast)
end
mk_const_array(sort, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1076
def mk_const_array(sort, ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_const_array(_ctx_pointer, sort._ast, ast._ast)
end
mk_context() click to toggle source
# File lib/z3/low_level.rb, line 20
def mk_context
  Z3::VeryLowLevel.Z3_mk_context(Z3::VeryLowLevel.Z3_mk_config)
end
mk_context_rc(config) click to toggle source
# File lib/z3/low_level_auto.rb, line 1080
def mk_context_rc(config) #=> :ctx_pointer
  VeryLowLevel.Z3_mk_context_rc(config._config)
end
mk_distinct(asts) click to toggle source
# File lib/z3/low_level.rb, line 54
def mk_distinct(asts)
  Z3::VeryLowLevel.Z3_mk_distinct(_ctx_pointer, asts.size, asts_vector(asts))
end
mk_div(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1084
def mk_div(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_div(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_divides(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1088
def mk_divides(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_divides(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_empty_set(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1092
def mk_empty_set(sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_empty_set(_ctx_pointer, sort._ast)
end
mk_eq(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1096
def mk_eq(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_eq(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_ext_rotate_left(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1100
def mk_ext_rotate_left(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_ext_rotate_left(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_ext_rotate_right(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1104
def mk_ext_rotate_right(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_ext_rotate_right(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_extract(num1, num2, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1108
def mk_extract(num1, num2, ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_extract(_ctx_pointer, num1, num2, ast._ast)
end
mk_false() click to toggle source
# File lib/z3/low_level_auto.rb, line 1112
def mk_false #=> :ast_pointer
  VeryLowLevel.Z3_mk_false(_ctx_pointer)
end
mk_finite_domain_sort(sym, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1116
def mk_finite_domain_sort(sym, num) #=> :sort_pointer
  VeryLowLevel.Z3_mk_finite_domain_sort(_ctx_pointer, sym, num)
end
mk_fixedpoint() click to toggle source
# File lib/z3/low_level_auto.rb, line 1120
def mk_fixedpoint #=> :fixedpoint_pointer
  VeryLowLevel.Z3_mk_fixedpoint(_ctx_pointer)
end
mk_fpa_abs(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1124
def mk_fpa_abs(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_abs(_ctx_pointer, ast._ast)
end
mk_fpa_add(ast1, ast2, ast3) click to toggle source
# File lib/z3/low_level_auto.rb, line 1128
def mk_fpa_add(ast1, ast2, ast3) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_add(_ctx_pointer, ast1._ast, ast2._ast, ast3._ast)
end
mk_fpa_div(ast1, ast2, ast3) click to toggle source
# File lib/z3/low_level_auto.rb, line 1132
def mk_fpa_div(ast1, ast2, ast3) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_div(_ctx_pointer, ast1._ast, ast2._ast, ast3._ast)
end
mk_fpa_eq(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1136
def mk_fpa_eq(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_eq(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_fpa_fma(ast1, ast2, ast3, ast4) click to toggle source
# File lib/z3/low_level_auto.rb, line 1140
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
mk_fpa_fp(ast1, ast2, ast3) click to toggle source
# File lib/z3/low_level_auto.rb, line 1144
def mk_fpa_fp(ast1, ast2, ast3) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_fp(_ctx_pointer, ast1._ast, ast2._ast, ast3._ast)
end
mk_fpa_geq(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1148
def mk_fpa_geq(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_geq(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_fpa_gt(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1152
def mk_fpa_gt(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_gt(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_fpa_inf(sort, bool) click to toggle source
# File lib/z3/low_level_auto.rb, line 1156
def mk_fpa_inf(sort, bool) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_inf(_ctx_pointer, sort._ast, bool)
end
mk_fpa_is_infinite(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1160
def mk_fpa_is_infinite(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_is_infinite(_ctx_pointer, ast._ast)
end
mk_fpa_is_nan(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1164
def mk_fpa_is_nan(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_is_nan(_ctx_pointer, ast._ast)
end
mk_fpa_is_negative(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1168
def mk_fpa_is_negative(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_is_negative(_ctx_pointer, ast._ast)
end
mk_fpa_is_normal(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1172
def mk_fpa_is_normal(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_is_normal(_ctx_pointer, ast._ast)
end
mk_fpa_is_positive(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1176
def mk_fpa_is_positive(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_is_positive(_ctx_pointer, ast._ast)
end
mk_fpa_is_subnormal(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1180
def mk_fpa_is_subnormal(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_is_subnormal(_ctx_pointer, ast._ast)
end
mk_fpa_is_zero(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1184
def mk_fpa_is_zero(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_is_zero(_ctx_pointer, ast._ast)
end
mk_fpa_leq(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1188
def mk_fpa_leq(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_leq(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_fpa_lt(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1192
def mk_fpa_lt(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_lt(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_fpa_max(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1196
def mk_fpa_max(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_max(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_fpa_min(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1200
def mk_fpa_min(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_min(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_fpa_mul(ast1, ast2, ast3) click to toggle source
# File lib/z3/low_level_auto.rb, line 1204
def mk_fpa_mul(ast1, ast2, ast3) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_mul(_ctx_pointer, ast1._ast, ast2._ast, ast3._ast)
end
mk_fpa_nan(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1208
def mk_fpa_nan(sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_nan(_ctx_pointer, sort._ast)
end
mk_fpa_neg(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1212
def mk_fpa_neg(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_neg(_ctx_pointer, ast._ast)
end
mk_fpa_numeral_double(double, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1216
def mk_fpa_numeral_double(double, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_numeral_double(_ctx_pointer, double, sort._ast)
end
mk_fpa_numeral_int(num, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1220
def mk_fpa_numeral_int(num, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_numeral_int(_ctx_pointer, num, sort._ast)
end
mk_fpa_numeral_int64_uint64(bool, num1, num2, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1224
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
mk_fpa_numeral_int_uint(bool, num1, num2, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1228
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
mk_fpa_rem(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1232
def mk_fpa_rem(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_rem(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_fpa_round_nearest_ties_to_away() click to toggle source
# File lib/z3/low_level_auto.rb, line 1236
def mk_fpa_round_nearest_ties_to_away #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_round_nearest_ties_to_away(_ctx_pointer)
end
mk_fpa_round_nearest_ties_to_even() click to toggle source
# File lib/z3/low_level_auto.rb, line 1240
def mk_fpa_round_nearest_ties_to_even #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_round_nearest_ties_to_even(_ctx_pointer)
end
mk_fpa_round_to_integral(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1244
def mk_fpa_round_to_integral(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_round_to_integral(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_fpa_round_toward_negative() click to toggle source
# File lib/z3/low_level_auto.rb, line 1248
def mk_fpa_round_toward_negative #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_round_toward_negative(_ctx_pointer)
end
mk_fpa_round_toward_positive() click to toggle source
# File lib/z3/low_level_auto.rb, line 1252
def mk_fpa_round_toward_positive #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_round_toward_positive(_ctx_pointer)
end
mk_fpa_round_toward_zero() click to toggle source
# File lib/z3/low_level_auto.rb, line 1256
def mk_fpa_round_toward_zero #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_round_toward_zero(_ctx_pointer)
end
mk_fpa_rounding_mode_sort() click to toggle source
# File lib/z3/low_level_auto.rb, line 1260
def mk_fpa_rounding_mode_sort #=> :sort_pointer
  VeryLowLevel.Z3_mk_fpa_rounding_mode_sort(_ctx_pointer)
end
mk_fpa_sort(num1, num2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1264
def mk_fpa_sort(num1, num2) #=> :sort_pointer
  VeryLowLevel.Z3_mk_fpa_sort(_ctx_pointer, num1, num2)
end
mk_fpa_sort_128() click to toggle source
# File lib/z3/low_level_auto.rb, line 1268
def mk_fpa_sort_128 #=> :sort_pointer
  VeryLowLevel.Z3_mk_fpa_sort_128(_ctx_pointer)
end
mk_fpa_sort_16() click to toggle source
# File lib/z3/low_level_auto.rb, line 1272
def mk_fpa_sort_16 #=> :sort_pointer
  VeryLowLevel.Z3_mk_fpa_sort_16(_ctx_pointer)
end
mk_fpa_sort_32() click to toggle source
# File lib/z3/low_level_auto.rb, line 1276
def mk_fpa_sort_32 #=> :sort_pointer
  VeryLowLevel.Z3_mk_fpa_sort_32(_ctx_pointer)
end
mk_fpa_sort_64() click to toggle source
# File lib/z3/low_level_auto.rb, line 1280
def mk_fpa_sort_64 #=> :sort_pointer
  VeryLowLevel.Z3_mk_fpa_sort_64(_ctx_pointer)
end
mk_fpa_sort_double() click to toggle source
# File lib/z3/low_level_auto.rb, line 1284
def mk_fpa_sort_double #=> :sort_pointer
  VeryLowLevel.Z3_mk_fpa_sort_double(_ctx_pointer)
end
mk_fpa_sort_half() click to toggle source
# File lib/z3/low_level_auto.rb, line 1288
def mk_fpa_sort_half #=> :sort_pointer
  VeryLowLevel.Z3_mk_fpa_sort_half(_ctx_pointer)
end
mk_fpa_sort_quadruple() click to toggle source
# File lib/z3/low_level_auto.rb, line 1292
def mk_fpa_sort_quadruple #=> :sort_pointer
  VeryLowLevel.Z3_mk_fpa_sort_quadruple(_ctx_pointer)
end
mk_fpa_sort_single() click to toggle source
# File lib/z3/low_level_auto.rb, line 1296
def mk_fpa_sort_single #=> :sort_pointer
  VeryLowLevel.Z3_mk_fpa_sort_single(_ctx_pointer)
end
mk_fpa_sqrt(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1300
def mk_fpa_sqrt(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_sqrt(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_fpa_sub(ast1, ast2, ast3) click to toggle source
# File lib/z3/low_level_auto.rb, line 1304
def mk_fpa_sub(ast1, ast2, ast3) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_sub(_ctx_pointer, ast1._ast, ast2._ast, ast3._ast)
end
mk_fpa_to_fp_bv(ast, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1308
def mk_fpa_to_fp_bv(ast, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_to_fp_bv(_ctx_pointer, ast._ast, sort._ast)
end
mk_fpa_to_fp_float(ast1, ast2, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1312
def mk_fpa_to_fp_float(ast1, ast2, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_to_fp_float(_ctx_pointer, ast1._ast, ast2._ast, sort._ast)
end
mk_fpa_to_fp_int_real(ast1, ast2, ast3, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1316
def mk_fpa_to_fp_int_real(ast1, ast2, ast3, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_to_fp_int_real(_ctx_pointer, ast1._ast, ast2._ast, ast3._ast, sort._ast)
end
mk_fpa_to_fp_real(ast1, ast2, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1320
def mk_fpa_to_fp_real(ast1, ast2, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_to_fp_real(_ctx_pointer, ast1._ast, ast2._ast, sort._ast)
end
mk_fpa_to_fp_signed(ast1, ast2, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1324
def mk_fpa_to_fp_signed(ast1, ast2, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_to_fp_signed(_ctx_pointer, ast1._ast, ast2._ast, sort._ast)
end
mk_fpa_to_fp_unsigned(ast1, ast2, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1328
def mk_fpa_to_fp_unsigned(ast1, ast2, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_to_fp_unsigned(_ctx_pointer, ast1._ast, ast2._ast, sort._ast)
end
mk_fpa_to_ieee_bv(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1332
def mk_fpa_to_ieee_bv(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_to_ieee_bv(_ctx_pointer, ast._ast)
end
mk_fpa_to_real(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1336
def mk_fpa_to_real(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_to_real(_ctx_pointer, ast._ast)
end
mk_fpa_to_sbv(ast1, ast2, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1340
def mk_fpa_to_sbv(ast1, ast2, num) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_to_sbv(_ctx_pointer, ast1._ast, ast2._ast, num)
end
mk_fpa_to_ubv(ast1, ast2, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1344
def mk_fpa_to_ubv(ast1, ast2, num) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_to_ubv(_ctx_pointer, ast1._ast, ast2._ast, num)
end
mk_fpa_zero(sort, bool) click to toggle source
# File lib/z3/low_level_auto.rb, line 1348
def mk_fpa_zero(sort, bool) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fpa_zero(_ctx_pointer, sort._ast, bool)
end
mk_fresh_const(str, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1352
def mk_fresh_const(str, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_fresh_const(_ctx_pointer, str, sort._ast)
end
mk_full_set(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1356
def mk_full_set(sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_full_set(_ctx_pointer, sort._ast)
end
mk_ge(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1360
def mk_ge(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_ge(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_goal(bool1, bool2, bool3) click to toggle source
# File lib/z3/low_level_auto.rb, line 1364
def mk_goal(bool1, bool2, bool3) #=> :goal_pointer
  VeryLowLevel.Z3_mk_goal(_ctx_pointer, bool1, bool2, bool3)
end
mk_gt(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1368
def mk_gt(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_gt(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_iff(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1372
def mk_iff(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_iff(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_implies(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1376
def mk_implies(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_implies(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_int(num, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1380
def mk_int(num, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_int(_ctx_pointer, num, sort._ast)
end
mk_int2bv(num, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1384
def mk_int2bv(num, ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_int2bv(_ctx_pointer, num, ast._ast)
end
mk_int2real(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1388
def mk_int2real(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_int2real(_ctx_pointer, ast._ast)
end
mk_int64(num, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1392
def mk_int64(num, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_int64(_ctx_pointer, num, sort._ast)
end
mk_int_sort() click to toggle source
# File lib/z3/low_level_auto.rb, line 1396
def mk_int_sort #=> :sort_pointer
  VeryLowLevel.Z3_mk_int_sort(_ctx_pointer)
end
mk_int_symbol(num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1400
def mk_int_symbol(num) #=> :symbol_pointer
  VeryLowLevel.Z3_mk_int_symbol(_ctx_pointer, num)
end
mk_int_to_str(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1404
def mk_int_to_str(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_int_to_str(_ctx_pointer, ast._ast)
end
mk_is_int(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1408
def mk_is_int(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_is_int(_ctx_pointer, ast._ast)
end
mk_ite(ast1, ast2, ast3) click to toggle source
# File lib/z3/low_level_auto.rb, line 1412
def mk_ite(ast1, ast2, ast3) #=> :ast_pointer
  VeryLowLevel.Z3_mk_ite(_ctx_pointer, ast1._ast, ast2._ast, ast3._ast)
end
mk_le(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1416
def mk_le(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_le(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_linear_order(sort, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1420
def mk_linear_order(sort, num) #=> :func_decl_pointer
  VeryLowLevel.Z3_mk_linear_order(_ctx_pointer, sort._ast, num)
end
mk_lstring(num, str) click to toggle source
# File lib/z3/low_level_auto.rb, line 1424
def mk_lstring(num, str) #=> :ast_pointer
  VeryLowLevel.Z3_mk_lstring(_ctx_pointer, num, str)
end
mk_lt(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1428
def mk_lt(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_lt(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_mod(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1432
def mk_mod(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_mod(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_model() click to toggle source
# File lib/z3/low_level_auto.rb, line 1436
def mk_model #=> :model_pointer
  VeryLowLevel.Z3_mk_model(_ctx_pointer)
end
mk_mul(asts) click to toggle source
# File lib/z3/low_level.rb, line 42
def mk_mul(asts)
  Z3::VeryLowLevel.Z3_mk_mul(_ctx_pointer, asts.size, asts_vector(asts))
end
mk_not(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1440
def mk_not(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_not(_ctx_pointer, ast._ast)
end
mk_numeral(str, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1444
def mk_numeral(str, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_numeral(_ctx_pointer, str, sort._ast)
end
mk_optimize() click to toggle source
# File lib/z3/low_level_auto.rb, line 1448
def mk_optimize #=> :optimize_pointer
  VeryLowLevel.Z3_mk_optimize(_ctx_pointer)
end
mk_or(asts) click to toggle source
# File lib/z3/low_level.rb, line 38
def mk_or(asts)
  Z3::VeryLowLevel.Z3_mk_or(_ctx_pointer, asts.size, asts_vector(asts))
end
mk_params() click to toggle source
# File lib/z3/low_level_auto.rb, line 1452
def mk_params #=> :params_pointer
  VeryLowLevel.Z3_mk_params(_ctx_pointer)
end
mk_partial_order(sort, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1456
def mk_partial_order(sort, num) #=> :func_decl_pointer
  VeryLowLevel.Z3_mk_partial_order(_ctx_pointer, sort._ast, num)
end
mk_piecewise_linear_order(sort, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1460
def mk_piecewise_linear_order(sort, num) #=> :func_decl_pointer
  VeryLowLevel.Z3_mk_piecewise_linear_order(_ctx_pointer, sort._ast, num)
end
mk_power(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1464
def mk_power(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_power(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_probe(str) click to toggle source
# File lib/z3/low_level_auto.rb, line 1468
def mk_probe(str) #=> :probe_pointer
  VeryLowLevel.Z3_mk_probe(_ctx_pointer, str)
end
mk_re_allchar(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1472
def mk_re_allchar(sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_re_allchar(_ctx_pointer, sort._ast)
end
mk_re_complement(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1476
def mk_re_complement(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_re_complement(_ctx_pointer, ast._ast)
end
mk_re_empty(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1480
def mk_re_empty(sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_re_empty(_ctx_pointer, sort._ast)
end
mk_re_full(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1484
def mk_re_full(sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_re_full(_ctx_pointer, sort._ast)
end
mk_re_loop(ast, num1, num2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1488
def mk_re_loop(ast, num1, num2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_re_loop(_ctx_pointer, ast._ast, num1, num2)
end
mk_re_range(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1492
def mk_re_range(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_re_range(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_real(num1, num2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1496
def mk_real(num1, num2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_real(_ctx_pointer, num1, num2)
end
mk_real2int(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1500
def mk_real2int(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_real2int(_ctx_pointer, ast._ast)
end
mk_real_sort() click to toggle source
# File lib/z3/low_level_auto.rb, line 1504
def mk_real_sort #=> :sort_pointer
  VeryLowLevel.Z3_mk_real_sort(_ctx_pointer)
end
mk_rem(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1508
def mk_rem(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_rem(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_repeat(num, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1512
def mk_repeat(num, ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_repeat(_ctx_pointer, num, ast._ast)
end
mk_rotate_left(num, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1516
def mk_rotate_left(num, ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_rotate_left(_ctx_pointer, num, ast._ast)
end
mk_rotate_right(num, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1520
def mk_rotate_right(num, ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_rotate_right(_ctx_pointer, num, ast._ast)
end
mk_sbv_to_str(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1524
def mk_sbv_to_str(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_sbv_to_str(_ctx_pointer, ast._ast)
end
mk_select(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1528
def mk_select(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_select(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_seq_last_index(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1532
def mk_seq_last_index(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_seq_last_index(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_seq_nth(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1536
def mk_seq_nth(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_seq_nth(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_set_add(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1540
def mk_set_add(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_set_add(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_set_complement(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1544
def mk_set_complement(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_set_complement(_ctx_pointer, ast._ast)
end
mk_set_del(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1548
def mk_set_del(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_set_del(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_set_difference(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1552
def mk_set_difference(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_set_difference(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_set_has_size(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1556
def mk_set_has_size(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_set_has_size(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_set_intersect(asts) click to toggle source
# File lib/z3/low_level.rb, line 62
def mk_set_intersect(asts)
  Z3::VeryLowLevel.Z3_mk_set_intersect(_ctx_pointer, asts.size, asts_vector(asts))
end
mk_set_member(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1560
def mk_set_member(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_set_member(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_set_sort(sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1564
def mk_set_sort(sort) #=> :sort_pointer
  VeryLowLevel.Z3_mk_set_sort(_ctx_pointer, sort._ast)
end
mk_set_subset(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1568
def mk_set_subset(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_set_subset(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_set_union(asts) click to toggle source
# File lib/z3/low_level.rb, line 58
def mk_set_union(asts)
  Z3::VeryLowLevel.Z3_mk_set_union(_ctx_pointer, asts.size, asts_vector(asts))
end
mk_sign_ext(num, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1572
def mk_sign_ext(num, ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_sign_ext(_ctx_pointer, num, ast._ast)
end
mk_simple_solver() click to toggle source
# File lib/z3/low_level_auto.rb, line 1576
def mk_simple_solver #=> :solver_pointer
  VeryLowLevel.Z3_mk_simple_solver(_ctx_pointer)
end
mk_solver() click to toggle source
# File lib/z3/low_level_auto.rb, line 1580
def mk_solver #=> :solver_pointer
  VeryLowLevel.Z3_mk_solver(_ctx_pointer)
end
mk_solver_for_logic(sym) click to toggle source
# File lib/z3/low_level_auto.rb, line 1584
def mk_solver_for_logic(sym) #=> :solver_pointer
  VeryLowLevel.Z3_mk_solver_for_logic(_ctx_pointer, sym)
end
mk_solver_from_tactic(tactic) click to toggle source
# File lib/z3/low_level_auto.rb, line 1588
def mk_solver_from_tactic(tactic) #=> :solver_pointer
  VeryLowLevel.Z3_mk_solver_from_tactic(_ctx_pointer, tactic._tactic)
end
mk_store(ast1, ast2, ast3) click to toggle source
# File lib/z3/low_level_auto.rb, line 1592
def mk_store(ast1, ast2, ast3) #=> :ast_pointer
  VeryLowLevel.Z3_mk_store(_ctx_pointer, ast1._ast, ast2._ast, ast3._ast)
end
mk_str_le(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1596
def mk_str_le(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_str_le(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_str_lt(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1600
def mk_str_lt(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_str_lt(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_str_to_int(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1604
def mk_str_to_int(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_str_to_int(_ctx_pointer, ast._ast)
end
mk_string_symbol(str) click to toggle source
# File lib/z3/low_level_auto.rb, line 1608
def mk_string_symbol(str) #=> :symbol_pointer
  VeryLowLevel.Z3_mk_string_symbol(_ctx_pointer, str)
end
mk_sub(asts) click to toggle source
# File lib/z3/low_level.rb, line 50
def mk_sub(asts)
  Z3::VeryLowLevel.Z3_mk_sub(_ctx_pointer, asts.size, asts_vector(asts))
end
mk_tactic(str) click to toggle source
# File lib/z3/low_level_auto.rb, line 1612
def mk_tactic(str) #=> :tactic_pointer
  VeryLowLevel.Z3_mk_tactic(_ctx_pointer, str)
end
mk_transitive_closure(func_decl) click to toggle source
# File lib/z3/low_level_auto.rb, line 1616
def mk_transitive_closure(func_decl) #=> :func_decl_pointer
  VeryLowLevel.Z3_mk_transitive_closure(_ctx_pointer, func_decl._ast)
end
mk_tree_order(sort, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1620
def mk_tree_order(sort, num) #=> :func_decl_pointer
  VeryLowLevel.Z3_mk_tree_order(_ctx_pointer, sort._ast, num)
end
mk_true() click to toggle source
# File lib/z3/low_level_auto.rb, line 1624
def mk_true #=> :ast_pointer
  VeryLowLevel.Z3_mk_true(_ctx_pointer)
end
mk_ubv_to_str(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1628
def mk_ubv_to_str(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_ubv_to_str(_ctx_pointer, ast._ast)
end
mk_unary_minus(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1632
def mk_unary_minus(ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_unary_minus(_ctx_pointer, ast._ast)
end
mk_uninterpreted_sort(sym) click to toggle source
# File lib/z3/low_level_auto.rb, line 1636
def mk_uninterpreted_sort(sym) #=> :sort_pointer
  VeryLowLevel.Z3_mk_uninterpreted_sort(_ctx_pointer, sym)
end
mk_unsigned_int(num, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1640
def mk_unsigned_int(num, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_unsigned_int(_ctx_pointer, num, sort._ast)
end
mk_unsigned_int64(num, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1644
def mk_unsigned_int64(num, sort) #=> :ast_pointer
  VeryLowLevel.Z3_mk_unsigned_int64(_ctx_pointer, num, sort._ast)
end
mk_xor(ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1648
def mk_xor(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_xor(_ctx_pointer, ast1._ast, ast2._ast)
end
mk_zero_ext(num, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1652
def mk_zero_ext(num, ast) #=> :ast_pointer
  VeryLowLevel.Z3_mk_zero_ext(_ctx_pointer, num, ast._ast)
end
model_dec_ref(model) click to toggle source
# File lib/z3/low_level_auto.rb, line 1656
def model_dec_ref(model) #=> :void
  VeryLowLevel.Z3_model_dec_ref(_ctx_pointer, model._model)
end
model_eval(model, ast, model_completion) click to toggle source
# File lib/z3/low_level.rb, line 24
def model_eval(model, ast, model_completion)
  rv_ptr = FFI::MemoryPointer.new(:pointer)
  result = Z3::VeryLowLevel.Z3_model_eval(_ctx_pointer, model._model, ast._ast, !!model_completion, rv_ptr) & 0xFF
  if result == 1
    rv_ptr.get_pointer(0)
  else
    raise Z3::Exception, "Evaluation of `#{ast}' failed"
  end
end
model_extrapolate(model, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1660
def model_extrapolate(model, ast) #=> :ast_pointer
  VeryLowLevel.Z3_model_extrapolate(_ctx_pointer, model._model, ast._ast)
end
model_get_const_decl(model, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1664
def model_get_const_decl(model, num) #=> :func_decl_pointer
  VeryLowLevel.Z3_model_get_const_decl(_ctx_pointer, model._model, num)
end
model_get_const_interp(model, func_decl) click to toggle source
# File lib/z3/low_level_auto.rb, line 1668
def model_get_const_interp(model, func_decl) #=> :ast_pointer
  VeryLowLevel.Z3_model_get_const_interp(_ctx_pointer, model._model, func_decl._ast)
end
model_get_func_decl(model, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1672
def model_get_func_decl(model, num) #=> :func_decl_pointer
  VeryLowLevel.Z3_model_get_func_decl(_ctx_pointer, model._model, num)
end
model_get_func_interp(model, func_decl) click to toggle source
# File lib/z3/low_level_auto.rb, line 1676
def model_get_func_interp(model, func_decl) #=> :func_interp_pointer
  VeryLowLevel.Z3_model_get_func_interp(_ctx_pointer, model._model, func_decl._ast)
end
model_get_num_consts(model) click to toggle source
# File lib/z3/low_level_auto.rb, line 1680
def model_get_num_consts(model) #=> :uint
  VeryLowLevel.Z3_model_get_num_consts(_ctx_pointer, model._model)
end
model_get_num_funcs(model) click to toggle source
# File lib/z3/low_level_auto.rb, line 1684
def model_get_num_funcs(model) #=> :uint
  VeryLowLevel.Z3_model_get_num_funcs(_ctx_pointer, model._model)
end
model_get_num_sorts(model) click to toggle source
# File lib/z3/low_level_auto.rb, line 1688
def model_get_num_sorts(model) #=> :uint
  VeryLowLevel.Z3_model_get_num_sorts(_ctx_pointer, model._model)
end
model_get_sort(model, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1692
def model_get_sort(model, num) #=> :sort_pointer
  VeryLowLevel.Z3_model_get_sort(_ctx_pointer, model._model, num)
end
model_get_sort_universe(model, sort) click to toggle source
# File lib/z3/low_level_auto.rb, line 1696
def model_get_sort_universe(model, sort) #=> :ast_vector_pointer
  VeryLowLevel.Z3_model_get_sort_universe(_ctx_pointer, model._model, sort._ast)
end
model_has_interp(model, func_decl) click to toggle source
# File lib/z3/low_level_auto.rb, line 1700
def model_has_interp(model, func_decl) #=> :bool
  VeryLowLevel.Z3_model_has_interp(_ctx_pointer, model._model, func_decl._ast)
end
model_inc_ref(model) click to toggle source
# File lib/z3/low_level_auto.rb, line 1704
def model_inc_ref(model) #=> :void
  VeryLowLevel.Z3_model_inc_ref(_ctx_pointer, model._model)
end
model_to_string(model) click to toggle source
# File lib/z3/low_level_auto.rb, line 1708
def model_to_string(model) #=> :string
  VeryLowLevel.Z3_model_to_string(_ctx_pointer, model._model)
end
model_translate(model, context) click to toggle source
# File lib/z3/low_level_auto.rb, line 1712
def model_translate(model, context) #=> :model_pointer
  VeryLowLevel.Z3_model_translate(_ctx_pointer, model._model, context._context)
end
optimize_assert(optimize, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1716
def optimize_assert(optimize, ast) #=> :void
  VeryLowLevel.Z3_optimize_assert(_ctx_pointer, optimize._optimize, ast._ast)
end
optimize_assert_and_track(optimize, ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1720
def optimize_assert_and_track(optimize, ast1, ast2) #=> :void
  VeryLowLevel.Z3_optimize_assert_and_track(_ctx_pointer, optimize._optimize, ast1._ast, ast2._ast)
end
optimize_assert_soft(optimize, ast, str, sym) click to toggle source
# File lib/z3/low_level_auto.rb, line 1724
def optimize_assert_soft(optimize, ast, str, sym) #=> :uint
  VeryLowLevel.Z3_optimize_assert_soft(_ctx_pointer, optimize._optimize, ast._ast, str, sym)
end
optimize_check(optimize, asts) click to toggle source
# File lib/z3/low_level.rb, line 66
def optimize_check(optimize, asts)
  Z3::VeryLowLevel.Z3_optimize_check(_ctx_pointer, optimize._optimize, asts.size, asts_vector(asts))
end
optimize_dec_ref(optimize) click to toggle source
# File lib/z3/low_level_auto.rb, line 1728
def optimize_dec_ref(optimize) #=> :void
  VeryLowLevel.Z3_optimize_dec_ref(_ctx_pointer, optimize._optimize)
end
optimize_from_file(optimize, str) click to toggle source
# File lib/z3/low_level_auto.rb, line 1732
def optimize_from_file(optimize, str) #=> :void
  VeryLowLevel.Z3_optimize_from_file(_ctx_pointer, optimize._optimize, str)
end
optimize_from_string(optimize, str) click to toggle source
# File lib/z3/low_level_auto.rb, line 1736
def optimize_from_string(optimize, str) #=> :void
  VeryLowLevel.Z3_optimize_from_string(_ctx_pointer, optimize._optimize, str)
end
optimize_get_assertions(optimize) click to toggle source
# File lib/z3/low_level_auto.rb, line 1740
def optimize_get_assertions(optimize) #=> :ast_vector_pointer
  VeryLowLevel.Z3_optimize_get_assertions(_ctx_pointer, optimize._optimize)
end
optimize_get_help(optimize) click to toggle source
# File lib/z3/low_level_auto.rb, line 1744
def optimize_get_help(optimize) #=> :string
  VeryLowLevel.Z3_optimize_get_help(_ctx_pointer, optimize._optimize)
end
optimize_get_lower(optimize, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1748
def optimize_get_lower(optimize, num) #=> :ast_pointer
  VeryLowLevel.Z3_optimize_get_lower(_ctx_pointer, optimize._optimize, num)
end
optimize_get_lower_as_vector(optimize, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1752
def optimize_get_lower_as_vector(optimize, num) #=> :ast_vector_pointer
  VeryLowLevel.Z3_optimize_get_lower_as_vector(_ctx_pointer, optimize._optimize, num)
end
optimize_get_model(optimize) click to toggle source
# File lib/z3/low_level_auto.rb, line 1756
def optimize_get_model(optimize) #=> :model_pointer
  VeryLowLevel.Z3_optimize_get_model(_ctx_pointer, optimize._optimize)
end
optimize_get_objectives(optimize) click to toggle source
# File lib/z3/low_level_auto.rb, line 1760
def optimize_get_objectives(optimize) #=> :ast_vector_pointer
  VeryLowLevel.Z3_optimize_get_objectives(_ctx_pointer, optimize._optimize)
end
optimize_get_param_descrs(optimize) click to toggle source
# File lib/z3/low_level_auto.rb, line 1764
def optimize_get_param_descrs(optimize) #=> :param_descrs_pointer
  VeryLowLevel.Z3_optimize_get_param_descrs(_ctx_pointer, optimize._optimize)
end
optimize_get_reason_unknown(optimize) click to toggle source
# File lib/z3/low_level_auto.rb, line 1768
def optimize_get_reason_unknown(optimize) #=> :string
  VeryLowLevel.Z3_optimize_get_reason_unknown(_ctx_pointer, optimize._optimize)
end
optimize_get_statistics(optimize) click to toggle source
# File lib/z3/low_level_auto.rb, line 1772
def optimize_get_statistics(optimize) #=> :stats_pointer
  VeryLowLevel.Z3_optimize_get_statistics(_ctx_pointer, optimize._optimize)
end
optimize_get_unsat_core(optimize) click to toggle source
# File lib/z3/low_level_auto.rb, line 1776
def optimize_get_unsat_core(optimize) #=> :ast_vector_pointer
  VeryLowLevel.Z3_optimize_get_unsat_core(_ctx_pointer, optimize._optimize)
end
optimize_get_upper(optimize, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1780
def optimize_get_upper(optimize, num) #=> :ast_pointer
  VeryLowLevel.Z3_optimize_get_upper(_ctx_pointer, optimize._optimize, num)
end
optimize_get_upper_as_vector(optimize, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1784
def optimize_get_upper_as_vector(optimize, num) #=> :ast_vector_pointer
  VeryLowLevel.Z3_optimize_get_upper_as_vector(_ctx_pointer, optimize._optimize, num)
end
optimize_inc_ref(optimize) click to toggle source
# File lib/z3/low_level_auto.rb, line 1788
def optimize_inc_ref(optimize) #=> :void
  VeryLowLevel.Z3_optimize_inc_ref(_ctx_pointer, optimize._optimize)
end
optimize_maximize(optimize, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1792
def optimize_maximize(optimize, ast) #=> :uint
  VeryLowLevel.Z3_optimize_maximize(_ctx_pointer, optimize._optimize, ast._ast)
end
optimize_minimize(optimize, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1796
def optimize_minimize(optimize, ast) #=> :uint
  VeryLowLevel.Z3_optimize_minimize(_ctx_pointer, optimize._optimize, ast._ast)
end
optimize_pop(optimize) click to toggle source
# File lib/z3/low_level_auto.rb, line 1800
def optimize_pop(optimize) #=> :void
  VeryLowLevel.Z3_optimize_pop(_ctx_pointer, optimize._optimize)
end
optimize_push(optimize) click to toggle source
# File lib/z3/low_level_auto.rb, line 1804
def optimize_push(optimize) #=> :void
  VeryLowLevel.Z3_optimize_push(_ctx_pointer, optimize._optimize)
end
optimize_set_params(optimize, params) click to toggle source
# File lib/z3/low_level_auto.rb, line 1808
def optimize_set_params(optimize, params) #=> :void
  VeryLowLevel.Z3_optimize_set_params(_ctx_pointer, optimize._optimize, params._params)
end
optimize_to_string(optimize) click to toggle source
# File lib/z3/low_level_auto.rb, line 1812
def optimize_to_string(optimize) #=> :string
  VeryLowLevel.Z3_optimize_to_string(_ctx_pointer, optimize._optimize)
end
param_descrs_dec_ref(param_descrs) click to toggle source
# File lib/z3/low_level_auto.rb, line 1816
def param_descrs_dec_ref(param_descrs) #=> :void
  VeryLowLevel.Z3_param_descrs_dec_ref(_ctx_pointer, param_descrs._param_descrs)
end
param_descrs_get_kind(param_descrs, sym) click to toggle source
# File lib/z3/low_level_auto.rb, line 1820
def param_descrs_get_kind(param_descrs, sym) #=> :uint
  VeryLowLevel.Z3_param_descrs_get_kind(_ctx_pointer, param_descrs._param_descrs, sym)
end
param_descrs_get_name(param_descrs, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1824
def param_descrs_get_name(param_descrs, num) #=> :symbol_pointer
  VeryLowLevel.Z3_param_descrs_get_name(_ctx_pointer, param_descrs._param_descrs, num)
end
param_descrs_inc_ref(param_descrs) click to toggle source
# File lib/z3/low_level_auto.rb, line 1828
def param_descrs_inc_ref(param_descrs) #=> :void
  VeryLowLevel.Z3_param_descrs_inc_ref(_ctx_pointer, param_descrs._param_descrs)
end
param_descrs_size(param_descrs) click to toggle source
# File lib/z3/low_level_auto.rb, line 1832
def param_descrs_size(param_descrs) #=> :uint
  VeryLowLevel.Z3_param_descrs_size(_ctx_pointer, param_descrs._param_descrs)
end
param_descrs_to_string(param_descrs) click to toggle source
# File lib/z3/low_level_auto.rb, line 1836
def param_descrs_to_string(param_descrs) #=> :string
  VeryLowLevel.Z3_param_descrs_to_string(_ctx_pointer, param_descrs._param_descrs)
end
params_dec_ref(params) click to toggle source
# File lib/z3/low_level_auto.rb, line 1840
def params_dec_ref(params) #=> :void
  VeryLowLevel.Z3_params_dec_ref(_ctx_pointer, params._params)
end
params_inc_ref(params) click to toggle source
# File lib/z3/low_level_auto.rb, line 1844
def params_inc_ref(params) #=> :void
  VeryLowLevel.Z3_params_inc_ref(_ctx_pointer, params._params)
end
params_set_bool(params, sym, bool) click to toggle source
# File lib/z3/low_level_auto.rb, line 1848
def params_set_bool(params, sym, bool) #=> :void
  VeryLowLevel.Z3_params_set_bool(_ctx_pointer, params._params, sym, bool)
end
params_set_double(params, sym, double) click to toggle source
# File lib/z3/low_level_auto.rb, line 1852
def params_set_double(params, sym, double) #=> :void
  VeryLowLevel.Z3_params_set_double(_ctx_pointer, params._params, sym, double)
end
params_set_symbol(params, sym1, sym2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1856
def params_set_symbol(params, sym1, sym2) #=> :void
  VeryLowLevel.Z3_params_set_symbol(_ctx_pointer, params._params, sym1, sym2)
end
params_set_uint(params, sym, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1860
def params_set_uint(params, sym, num) #=> :void
  VeryLowLevel.Z3_params_set_uint(_ctx_pointer, params._params, sym, num)
end
params_to_string(params) click to toggle source
# File lib/z3/low_level_auto.rb, line 1864
def params_to_string(params) #=> :string
  VeryLowLevel.Z3_params_to_string(_ctx_pointer, params._params)
end
params_validate(params, param_descrs) click to toggle source
# File lib/z3/low_level_auto.rb, line 1868
def params_validate(params, param_descrs) #=> :void
  VeryLowLevel.Z3_params_validate(_ctx_pointer, params._params, param_descrs._param_descrs)
end
pattern_to_string(pattern) click to toggle source
# File lib/z3/low_level_auto.rb, line 1872
def pattern_to_string(pattern) #=> :string
  VeryLowLevel.Z3_pattern_to_string(_ctx_pointer, pattern._ast)
end
polynomial_subresultants(ast1, ast2, ast3) click to toggle source
# File lib/z3/low_level_auto.rb, line 1876
def polynomial_subresultants(ast1, ast2, ast3) #=> :ast_vector_pointer
  VeryLowLevel.Z3_polynomial_subresultants(_ctx_pointer, ast1._ast, ast2._ast, ast3._ast)
end
probe_and(probe1, probe2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1880
def probe_and(probe1, probe2) #=> :probe_pointer
  VeryLowLevel.Z3_probe_and(_ctx_pointer, probe1._probe, probe2._probe)
end
probe_apply(probe, goal) click to toggle source
# File lib/z3/low_level_auto.rb, line 1884
def probe_apply(probe, goal) #=> :double
  VeryLowLevel.Z3_probe_apply(_ctx_pointer, probe._probe, goal._goal)
end
probe_const(double) click to toggle source
# File lib/z3/low_level_auto.rb, line 1888
def probe_const(double) #=> :probe_pointer
  VeryLowLevel.Z3_probe_const(_ctx_pointer, double)
end
probe_dec_ref(probe) click to toggle source
# File lib/z3/low_level_auto.rb, line 1892
def probe_dec_ref(probe) #=> :void
  VeryLowLevel.Z3_probe_dec_ref(_ctx_pointer, probe._probe)
end
probe_eq(probe1, probe2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1896
def probe_eq(probe1, probe2) #=> :probe_pointer
  VeryLowLevel.Z3_probe_eq(_ctx_pointer, probe1._probe, probe2._probe)
end
probe_ge(probe1, probe2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1900
def probe_ge(probe1, probe2) #=> :probe_pointer
  VeryLowLevel.Z3_probe_ge(_ctx_pointer, probe1._probe, probe2._probe)
end
probe_get_descr(str) click to toggle source
# File lib/z3/low_level_auto.rb, line 1904
def probe_get_descr(str) #=> :string
  VeryLowLevel.Z3_probe_get_descr(_ctx_pointer, str)
end
probe_gt(probe1, probe2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1908
def probe_gt(probe1, probe2) #=> :probe_pointer
  VeryLowLevel.Z3_probe_gt(_ctx_pointer, probe1._probe, probe2._probe)
end
probe_inc_ref(probe) click to toggle source
# File lib/z3/low_level_auto.rb, line 1912
def probe_inc_ref(probe) #=> :void
  VeryLowLevel.Z3_probe_inc_ref(_ctx_pointer, probe._probe)
end
probe_le(probe1, probe2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1916
def probe_le(probe1, probe2) #=> :probe_pointer
  VeryLowLevel.Z3_probe_le(_ctx_pointer, probe1._probe, probe2._probe)
end
probe_lt(probe1, probe2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1920
def probe_lt(probe1, probe2) #=> :probe_pointer
  VeryLowLevel.Z3_probe_lt(_ctx_pointer, probe1._probe, probe2._probe)
end
probe_not(probe) click to toggle source
# File lib/z3/low_level_auto.rb, line 1924
def probe_not(probe) #=> :probe_pointer
  VeryLowLevel.Z3_probe_not(_ctx_pointer, probe._probe)
end
probe_or(probe1, probe2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1928
def probe_or(probe1, probe2) #=> :probe_pointer
  VeryLowLevel.Z3_probe_or(_ctx_pointer, probe1._probe, probe2._probe)
end
qe_lite(ast_vector, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 1932
def qe_lite(ast_vector, ast) #=> :ast_pointer
  VeryLowLevel.Z3_qe_lite(_ctx_pointer, ast_vector, ast._ast)
end
rcf_add(num1, num2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1936
def rcf_add(num1, num2) #=> :rcf_num_pointer
  VeryLowLevel.Z3_rcf_add(_ctx_pointer, num1._rcf_num, num2._rcf_num)
end
rcf_del(num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1940
def rcf_del(num) #=> :void
  VeryLowLevel.Z3_rcf_del(_ctx_pointer, num._rcf_num)
end
rcf_div(num1, num2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1944
def rcf_div(num1, num2) #=> :rcf_num_pointer
  VeryLowLevel.Z3_rcf_div(_ctx_pointer, num1._rcf_num, num2._rcf_num)
end
rcf_eq(num1, num2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1948
def rcf_eq(num1, num2) #=> :bool
  VeryLowLevel.Z3_rcf_eq(_ctx_pointer, num1._rcf_num, num2._rcf_num)
end
rcf_ge(num1, num2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1952
def rcf_ge(num1, num2) #=> :bool
  VeryLowLevel.Z3_rcf_ge(_ctx_pointer, num1._rcf_num, num2._rcf_num)
end
rcf_gt(num1, num2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1956
def rcf_gt(num1, num2) #=> :bool
  VeryLowLevel.Z3_rcf_gt(_ctx_pointer, num1._rcf_num, num2._rcf_num)
end
rcf_inv(num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1960
def rcf_inv(num) #=> :rcf_num_pointer
  VeryLowLevel.Z3_rcf_inv(_ctx_pointer, num._rcf_num)
end
rcf_le(num1, num2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1964
def rcf_le(num1, num2) #=> :bool
  VeryLowLevel.Z3_rcf_le(_ctx_pointer, num1._rcf_num, num2._rcf_num)
end
rcf_lt(num1, num2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1968
def rcf_lt(num1, num2) #=> :bool
  VeryLowLevel.Z3_rcf_lt(_ctx_pointer, num1._rcf_num, num2._rcf_num)
end
rcf_mk_e() click to toggle source
# File lib/z3/low_level_auto.rb, line 1972
def rcf_mk_e #=> :rcf_num_pointer
  VeryLowLevel.Z3_rcf_mk_e(_ctx_pointer)
end
rcf_mk_infinitesimal() click to toggle source
# File lib/z3/low_level_auto.rb, line 1976
def rcf_mk_infinitesimal #=> :rcf_num_pointer
  VeryLowLevel.Z3_rcf_mk_infinitesimal(_ctx_pointer)
end
rcf_mk_pi() click to toggle source
# File lib/z3/low_level_auto.rb, line 1980
def rcf_mk_pi #=> :rcf_num_pointer
  VeryLowLevel.Z3_rcf_mk_pi(_ctx_pointer)
end
rcf_mk_rational(str) click to toggle source
# File lib/z3/low_level_auto.rb, line 1984
def rcf_mk_rational(str) #=> :rcf_num_pointer
  VeryLowLevel.Z3_rcf_mk_rational(_ctx_pointer, str)
end
rcf_mk_small_int(num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1988
def rcf_mk_small_int(num) #=> :rcf_num_pointer
  VeryLowLevel.Z3_rcf_mk_small_int(_ctx_pointer, num)
end
rcf_mul(num1, num2) click to toggle source
# File lib/z3/low_level_auto.rb, line 1992
def rcf_mul(num1, num2) #=> :rcf_num_pointer
  VeryLowLevel.Z3_rcf_mul(_ctx_pointer, num1._rcf_num, num2._rcf_num)
end
rcf_neg(num) click to toggle source
# File lib/z3/low_level_auto.rb, line 1996
def rcf_neg(num) #=> :rcf_num_pointer
  VeryLowLevel.Z3_rcf_neg(_ctx_pointer, num._rcf_num)
end
rcf_neq(num1, num2) click to toggle source
# File lib/z3/low_level_auto.rb, line 2000
def rcf_neq(num1, num2) #=> :bool
  VeryLowLevel.Z3_rcf_neq(_ctx_pointer, num1._rcf_num, num2._rcf_num)
end
rcf_num_to_decimal_string(num1, num2) click to toggle source
# File lib/z3/low_level_auto.rb, line 2004
def rcf_num_to_decimal_string(num1, num2) #=> :string
  VeryLowLevel.Z3_rcf_num_to_decimal_string(_ctx_pointer, num1._rcf_num, num2)
end
rcf_num_to_string(num, bool1, bool2) click to toggle source
# File lib/z3/low_level_auto.rb, line 2008
def rcf_num_to_string(num, bool1, bool2) #=> :string
  VeryLowLevel.Z3_rcf_num_to_string(_ctx_pointer, num._rcf_num, bool1, bool2)
end
rcf_power(num1, num2) click to toggle source
# File lib/z3/low_level_auto.rb, line 2012
def rcf_power(num1, num2) #=> :rcf_num_pointer
  VeryLowLevel.Z3_rcf_power(_ctx_pointer, num1._rcf_num, num2)
end
rcf_sub(num1, num2) click to toggle source
# File lib/z3/low_level_auto.rb, line 2016
def rcf_sub(num1, num2) #=> :rcf_num_pointer
  VeryLowLevel.Z3_rcf_sub(_ctx_pointer, num1._rcf_num, num2._rcf_num)
end
reset_memory() click to toggle source
# File lib/z3/low_level_auto.rb, line 2020
def reset_memory #=> :void
  VeryLowLevel.Z3_reset_memory()
end
set_error_handler(&block) click to toggle source
# File lib/z3/low_level.rb, line 16
def set_error_handler(&block)
  Z3::VeryLowLevel.Z3_set_error_handler(_ctx_pointer, block)
end
set_param_value(config, str1, str2) click to toggle source
# File lib/z3/low_level_auto.rb, line 2024
def set_param_value(config, str1, str2) #=> :void
  VeryLowLevel.Z3_set_param_value(config._config, str1, str2)
end
simplify(ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 2028
def simplify(ast) #=> :ast_pointer
  VeryLowLevel.Z3_simplify(_ctx_pointer, ast._ast)
end
simplify_ex(ast, params) click to toggle source
# File lib/z3/low_level_auto.rb, line 2032
def simplify_ex(ast, params) #=> :ast_pointer
  VeryLowLevel.Z3_simplify_ex(_ctx_pointer, ast._ast, params._params)
end
simplify_get_help() click to toggle source
# File lib/z3/low_level_auto.rb, line 2036
def simplify_get_help #=> :string
  VeryLowLevel.Z3_simplify_get_help(_ctx_pointer)
end
simplify_get_param_descrs() click to toggle source
# File lib/z3/low_level_auto.rb, line 2040
def simplify_get_param_descrs #=> :param_descrs_pointer
  VeryLowLevel.Z3_simplify_get_param_descrs(_ctx_pointer)
end
solver_assert(solver, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 2044
def solver_assert(solver, ast) #=> :void
  VeryLowLevel.Z3_solver_assert(_ctx_pointer, solver._solver, ast._ast)
end
solver_assert_and_track(solver, ast1, ast2) click to toggle source
# File lib/z3/low_level_auto.rb, line 2048
def solver_assert_and_track(solver, ast1, ast2) #=> :void
  VeryLowLevel.Z3_solver_assert_and_track(_ctx_pointer, solver._solver, ast1._ast, ast2._ast)
end
solver_check(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2052
def solver_check(solver) #=> :int
  VeryLowLevel.Z3_solver_check(_ctx_pointer, solver._solver)
end
solver_cube(solver, ast_vector, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 2056
def solver_cube(solver, ast_vector, num) #=> :ast_vector_pointer
  VeryLowLevel.Z3_solver_cube(_ctx_pointer, solver._solver, ast_vector, num)
end
solver_dec_ref(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2060
def solver_dec_ref(solver) #=> :void
  VeryLowLevel.Z3_solver_dec_ref(_ctx_pointer, solver._solver)
end
solver_from_file(solver, str) click to toggle source
# File lib/z3/low_level_auto.rb, line 2064
def solver_from_file(solver, str) #=> :void
  VeryLowLevel.Z3_solver_from_file(_ctx_pointer, solver._solver, str)
end
solver_from_string(solver, str) click to toggle source
# File lib/z3/low_level_auto.rb, line 2068
def solver_from_string(solver, str) #=> :void
  VeryLowLevel.Z3_solver_from_string(_ctx_pointer, solver._solver, str)
end
solver_get_assertions(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2072
def solver_get_assertions(solver) #=> :ast_vector_pointer
  VeryLowLevel.Z3_solver_get_assertions(_ctx_pointer, solver._solver)
end
solver_get_consequences(solver, ast_vector1, ast_vector2, ast_vector3) click to toggle source
# File lib/z3/low_level_auto.rb, line 2076
def solver_get_consequences(solver, ast_vector1, ast_vector2, ast_vector3) #=> :int
  VeryLowLevel.Z3_solver_get_consequences(_ctx_pointer, solver._solver, ast_vector1, ast_vector2, ast_vector3)
end
solver_get_help(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2080
def solver_get_help(solver) #=> :string
  VeryLowLevel.Z3_solver_get_help(_ctx_pointer, solver._solver)
end
solver_get_model(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2084
def solver_get_model(solver) #=> :model_pointer
  VeryLowLevel.Z3_solver_get_model(_ctx_pointer, solver._solver)
end
solver_get_non_units(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2088
def solver_get_non_units(solver) #=> :ast_vector_pointer
  VeryLowLevel.Z3_solver_get_non_units(_ctx_pointer, solver._solver)
end
solver_get_num_scopes(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2092
def solver_get_num_scopes(solver) #=> :uint
  VeryLowLevel.Z3_solver_get_num_scopes(_ctx_pointer, solver._solver)
end
solver_get_param_descrs(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2096
def solver_get_param_descrs(solver) #=> :param_descrs_pointer
  VeryLowLevel.Z3_solver_get_param_descrs(_ctx_pointer, solver._solver)
end
solver_get_proof(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2100
def solver_get_proof(solver) #=> :ast_pointer
  VeryLowLevel.Z3_solver_get_proof(_ctx_pointer, solver._solver)
end
solver_get_reason_unknown(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2104
def solver_get_reason_unknown(solver) #=> :string
  VeryLowLevel.Z3_solver_get_reason_unknown(_ctx_pointer, solver._solver)
end
solver_get_statistics(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2108
def solver_get_statistics(solver) #=> :stats_pointer
  VeryLowLevel.Z3_solver_get_statistics(_ctx_pointer, solver._solver)
end
solver_get_trail(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2112
def solver_get_trail(solver) #=> :ast_vector_pointer
  VeryLowLevel.Z3_solver_get_trail(_ctx_pointer, solver._solver)
end
solver_get_units(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2116
def solver_get_units(solver) #=> :ast_vector_pointer
  VeryLowLevel.Z3_solver_get_units(_ctx_pointer, solver._solver)
end
solver_get_unsat_core(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2120
def solver_get_unsat_core(solver) #=> :ast_vector_pointer
  VeryLowLevel.Z3_solver_get_unsat_core(_ctx_pointer, solver._solver)
end
solver_import_model_converter(solver1, solver2) click to toggle source
# File lib/z3/low_level_auto.rb, line 2124
def solver_import_model_converter(solver1, solver2) #=> :void
  VeryLowLevel.Z3_solver_import_model_converter(_ctx_pointer, solver1._solver, solver2._solver)
end
solver_inc_ref(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2128
def solver_inc_ref(solver) #=> :void
  VeryLowLevel.Z3_solver_inc_ref(_ctx_pointer, solver._solver)
end
solver_interrupt(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2132
def solver_interrupt(solver) #=> :void
  VeryLowLevel.Z3_solver_interrupt(_ctx_pointer, solver._solver)
end
solver_pop(solver, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 2136
def solver_pop(solver, num) #=> :void
  VeryLowLevel.Z3_solver_pop(_ctx_pointer, solver._solver, num)
end
solver_propagate_register(solver, ast) click to toggle source
# File lib/z3/low_level_auto.rb, line 2140
def solver_propagate_register(solver, ast) #=> :uint
  VeryLowLevel.Z3_solver_propagate_register(_ctx_pointer, solver._solver, ast._ast)
end
solver_push(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2144
def solver_push(solver) #=> :void
  VeryLowLevel.Z3_solver_push(_ctx_pointer, solver._solver)
end
solver_reset(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2148
def solver_reset(solver) #=> :void
  VeryLowLevel.Z3_solver_reset(_ctx_pointer, solver._solver)
end
solver_set_params(solver, params) click to toggle source
# File lib/z3/low_level_auto.rb, line 2152
def solver_set_params(solver, params) #=> :void
  VeryLowLevel.Z3_solver_set_params(_ctx_pointer, solver._solver, params._params)
end
solver_to_dimacs_string(solver, bool) click to toggle source
# File lib/z3/low_level_auto.rb, line 2156
def solver_to_dimacs_string(solver, bool) #=> :string
  VeryLowLevel.Z3_solver_to_dimacs_string(_ctx_pointer, solver._solver, bool)
end
solver_to_string(solver) click to toggle source
# File lib/z3/low_level_auto.rb, line 2160
def solver_to_string(solver) #=> :string
  VeryLowLevel.Z3_solver_to_string(_ctx_pointer, solver._solver)
end
stats_dec_ref(stats) click to toggle source
# File lib/z3/low_level_auto.rb, line 2164
def stats_dec_ref(stats) #=> :void
  VeryLowLevel.Z3_stats_dec_ref(_ctx_pointer, stats)
end
stats_get_double_value(stats, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 2168
def stats_get_double_value(stats, num) #=> :double
  VeryLowLevel.Z3_stats_get_double_value(_ctx_pointer, stats, num)
end
stats_get_key(stats, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 2172
def stats_get_key(stats, num) #=> :string
  VeryLowLevel.Z3_stats_get_key(_ctx_pointer, stats, num)
end
stats_get_uint_value(stats, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 2176
def stats_get_uint_value(stats, num) #=> :uint
  VeryLowLevel.Z3_stats_get_uint_value(_ctx_pointer, stats, num)
end
stats_inc_ref(stats) click to toggle source
# File lib/z3/low_level_auto.rb, line 2180
def stats_inc_ref(stats) #=> :void
  VeryLowLevel.Z3_stats_inc_ref(_ctx_pointer, stats)
end
stats_is_double(stats, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 2184
def stats_is_double(stats, num) #=> :bool
  VeryLowLevel.Z3_stats_is_double(_ctx_pointer, stats, num)
end
stats_is_uint(stats, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 2188
def stats_is_uint(stats, num) #=> :bool
  VeryLowLevel.Z3_stats_is_uint(_ctx_pointer, stats, num)
end
stats_size(stats) click to toggle source
# File lib/z3/low_level_auto.rb, line 2192
def stats_size(stats) #=> :uint
  VeryLowLevel.Z3_stats_size(_ctx_pointer, stats)
end
stats_to_string(stats) click to toggle source
# File lib/z3/low_level_auto.rb, line 2196
def stats_to_string(stats) #=> :string
  VeryLowLevel.Z3_stats_to_string(_ctx_pointer, stats)
end
tactic_and_then(tactic1, tactic2) click to toggle source
# File lib/z3/low_level_auto.rb, line 2200
def tactic_and_then(tactic1, tactic2) #=> :tactic_pointer
  VeryLowLevel.Z3_tactic_and_then(_ctx_pointer, tactic1._tactic, tactic2._tactic)
end
tactic_apply(tactic, goal) click to toggle source
# File lib/z3/low_level_auto.rb, line 2204
def tactic_apply(tactic, goal) #=> :apply_result_pointer
  VeryLowLevel.Z3_tactic_apply(_ctx_pointer, tactic._tactic, goal._goal)
end
tactic_apply_ex(tactic, goal, params) click to toggle source
# File lib/z3/low_level_auto.rb, line 2208
def tactic_apply_ex(tactic, goal, params) #=> :apply_result_pointer
  VeryLowLevel.Z3_tactic_apply_ex(_ctx_pointer, tactic._tactic, goal._goal, params._params)
end
tactic_cond(probe, tactic1, tactic2) click to toggle source
# File lib/z3/low_level_auto.rb, line 2212
def tactic_cond(probe, tactic1, tactic2) #=> :tactic_pointer
  VeryLowLevel.Z3_tactic_cond(_ctx_pointer, probe._probe, tactic1._tactic, tactic2._tactic)
end
tactic_dec_ref(tactic) click to toggle source
# File lib/z3/low_level_auto.rb, line 2216
def tactic_dec_ref(tactic) #=> :void
  VeryLowLevel.Z3_tactic_dec_ref(_ctx_pointer, tactic._tactic)
end
tactic_fail() click to toggle source
# File lib/z3/low_level_auto.rb, line 2220
def tactic_fail #=> :tactic_pointer
  VeryLowLevel.Z3_tactic_fail(_ctx_pointer)
end
tactic_fail_if(probe) click to toggle source
# File lib/z3/low_level_auto.rb, line 2224
def tactic_fail_if(probe) #=> :tactic_pointer
  VeryLowLevel.Z3_tactic_fail_if(_ctx_pointer, probe._probe)
end
tactic_fail_if_not_decided() click to toggle source
# File lib/z3/low_level_auto.rb, line 2228
def tactic_fail_if_not_decided #=> :tactic_pointer
  VeryLowLevel.Z3_tactic_fail_if_not_decided(_ctx_pointer)
end
tactic_get_descr(str) click to toggle source
# File lib/z3/low_level_auto.rb, line 2232
def tactic_get_descr(str) #=> :string
  VeryLowLevel.Z3_tactic_get_descr(_ctx_pointer, str)
end
tactic_get_help(tactic) click to toggle source
# File lib/z3/low_level_auto.rb, line 2236
def tactic_get_help(tactic) #=> :string
  VeryLowLevel.Z3_tactic_get_help(_ctx_pointer, tactic._tactic)
end
tactic_get_param_descrs(tactic) click to toggle source
# File lib/z3/low_level_auto.rb, line 2240
def tactic_get_param_descrs(tactic) #=> :param_descrs_pointer
  VeryLowLevel.Z3_tactic_get_param_descrs(_ctx_pointer, tactic._tactic)
end
tactic_inc_ref(tactic) click to toggle source
# File lib/z3/low_level_auto.rb, line 2244
def tactic_inc_ref(tactic) #=> :void
  VeryLowLevel.Z3_tactic_inc_ref(_ctx_pointer, tactic._tactic)
end
tactic_or_else(tactic1, tactic2) click to toggle source
# File lib/z3/low_level_auto.rb, line 2248
def tactic_or_else(tactic1, tactic2) #=> :tactic_pointer
  VeryLowLevel.Z3_tactic_or_else(_ctx_pointer, tactic1._tactic, tactic2._tactic)
end
tactic_par_and_then(tactic1, tactic2) click to toggle source
# File lib/z3/low_level_auto.rb, line 2252
def tactic_par_and_then(tactic1, tactic2) #=> :tactic_pointer
  VeryLowLevel.Z3_tactic_par_and_then(_ctx_pointer, tactic1._tactic, tactic2._tactic)
end
tactic_repeat(tactic, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 2256
def tactic_repeat(tactic, num) #=> :tactic_pointer
  VeryLowLevel.Z3_tactic_repeat(_ctx_pointer, tactic._tactic, num)
end
tactic_skip() click to toggle source
# File lib/z3/low_level_auto.rb, line 2260
def tactic_skip #=> :tactic_pointer
  VeryLowLevel.Z3_tactic_skip(_ctx_pointer)
end
tactic_try_for(tactic, num) click to toggle source
# File lib/z3/low_level_auto.rb, line 2264
def tactic_try_for(tactic, num) #=> :tactic_pointer
  VeryLowLevel.Z3_tactic_try_for(_ctx_pointer, tactic._tactic, num)
end
tactic_using_params(tactic, params) click to toggle source
# File lib/z3/low_level_auto.rb, line 2268
def tactic_using_params(tactic, params) #=> :tactic_pointer
  VeryLowLevel.Z3_tactic_using_params(_ctx_pointer, tactic._tactic, params._params)
end
tactic_when(probe, tactic) click to toggle source
# File lib/z3/low_level_auto.rb, line 2272
def tactic_when(probe, tactic) #=> :tactic_pointer
  VeryLowLevel.Z3_tactic_when(_ctx_pointer, probe._probe, tactic._tactic)
end
toggle_warning_messages(bool) click to toggle source
# File lib/z3/low_level_auto.rb, line 2276
def toggle_warning_messages(bool) #=> :void
  VeryLowLevel.Z3_toggle_warning_messages(bool)
end
translate(ast, context) click to toggle source
# File lib/z3/low_level_auto.rb, line 2280
def translate(ast, context) #=> :ast_pointer
  VeryLowLevel.Z3_translate(_ctx_pointer, ast._ast, context._context)
end
unpack_ast_vector(_ast_vector) click to toggle source

Should be private

# File lib/z3/low_level.rb, line 72
def unpack_ast_vector(_ast_vector)
  ast_vector_size(_ast_vector).times.map do |i|
    _ast = ast_vector_get(_ast_vector, i)
    Expr.new_from_pointer(_ast)
  end
end
unpack_statistics(_stats) click to toggle source
# File lib/z3/low_level.rb, line 79
def unpack_statistics(_stats)
  stats = {}
  stats_size(_stats).times.map do |i|
    key = stats_get_key(_stats, i)
    if stats_is_double(_stats, i)
      val = stats_get_double_value(_stats, i)
    elsif stats_is_uint(_stats, i)
      val = stats_get_uint_value(_stats, i)
    else
      raise Z3::Exception, "Stat is neither double nor uint, that's not supposed to happen"
    end
    raise Z3::Exception, "Key #{key} duplicated in stats" if stats.has_key?(key)
    stats[key] = val
  end
  stats
end
update_param_value(str1, str2) click to toggle source
# File lib/z3/low_level_auto.rb, line 2284
def update_param_value(str1, str2) #=> :void
  VeryLowLevel.Z3_update_param_value(_ctx_pointer, str1, str2)
end

Private Class Methods

asts_vector(args) click to toggle source
# File lib/z3/low_level.rb, line 102
def asts_vector(args)
  # raise if args.empty?
  c_args = FFI::MemoryPointer.new(:pointer, args.size)
  c_args.write_array_of_pointer args.map(&:_ast)
  c_args
end