Module: Z3::LowLevel

Defined in:
lib/z3/low_level.rb,
lib/z3/low_level_auto.rb

Class Method Summary collapse

Class Method Details

._ctx_pointer ⇒ Object 



96
97
98
 
# 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) ⇒ Object

> :void



4
5
6
 
# 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) ⇒ Object

> :func_interp_pointer



8
9
10
 
# 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) ⇒ Object

> :ast_pointer



12
13
14
 
# 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) ⇒ Object

> :ast_pointer



16
17
18
 
# 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) ⇒ Object

> :bool



20
21
22
 
# 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) ⇒ Object

> :bool



24
25
26
 
# 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) ⇒ Object

> :uint



28
29
30
 
# 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) ⇒ Object

> :ast_vector_pointer



32
33
34
 
# 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) ⇒ Object

> :bool



36
37
38
 
# 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) ⇒ Object

> :bool



40
41
42
 
# 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) ⇒ Object

> :bool



44
45
46
 
# 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) ⇒ Object

> :bool



48
49
50
 
# 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) ⇒ Object

> :bool



52
53
54
 
# 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) ⇒ Object

> :bool



56
57
58
 
# 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) ⇒ Object

> :bool



60
61
62
 
# 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) ⇒ Object

> :ast_pointer



64
65
66
 
# 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) ⇒ Object

> :bool



68
69
70
 
# 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) ⇒ Object

> :ast_pointer



72
73
74
 
# 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) ⇒ Object

> :ast_pointer



76
77
78
 
# 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) ⇒ Object

> :int



80
81
82
 
# 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) ⇒ Object

> :ast_pointer



84
85
86
 
# 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) ⇒ Object

> :void



88
89
90
 
# 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) ⇒ Object

> :uint



92
93
94
 
# 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) ⇒ Object

> :goal_pointer



96
97
98
 
# 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) ⇒ Object

> :void



100
101
102
 
# 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) ⇒ Object

> :string



104
105
106
 
# 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) ⇒ Object

> :bool



108
109
110
 
# 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) ⇒ Object

> :void



112
113
114
 
# 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) ⇒ Object

> :void



116
117
118
 
# 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) ⇒ Object

> :ast_pointer



120
121
122
 
# 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) ⇒ Object

> :void



124
125
126
 
# 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) ⇒ Object

> :void



128
129
130
 
# 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) ⇒ Object

> :ast_vector_pointer



132
133
134
 
# 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) ⇒ Object

> :void



136
137
138
 
# 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) ⇒ Object

> :uint



140
141
142
 
# 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) ⇒ Object

> :string



144
145
146
 
# 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) ⇒ Object

> :string



148
149
150
 
# 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) ⇒ Object

> :void



152
153
154
 
# 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) ⇒ Object

> :ast_pointer



156
157
158
 
# 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) ⇒ Object

> :void



160
161
162
 
# 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) ⇒ Object

> :void



164
165
166
 
# 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) ⇒ Object

> :void



168
169
170
 
# 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) ⇒ Object

> :void



172
173
174
 
# 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) ⇒ Object

> :uint



176
177
178
 
# 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) ⇒ Object

> :string



180
181
182
 
# 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) ⇒ Object

> :ast_vector_pointer



184
185
186
 
# 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) ⇒ Object

> :ast_pointer



188
189
190
 
# 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) ⇒ Object

> :void



192
193
194
 
# 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) ⇒ Object

> :void



196
197
198
 
# File 'lib/z3/low_level_auto.rb', line 196

def del_config(config) #=> :void
  VeryLowLevel.Z3_del_config(config._config)
end

.del_constructor(constructor) ⇒ Object

> :void



200
201
202
 
# 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) ⇒ Object

> :void



204
205
206
 
# 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 ⇒ Object

> :void



208
209
210
 
# File 'lib/z3/low_level_auto.rb', line 208

def del_context #=> :void
  VeryLowLevel.Z3_del_context(_ctx_pointer)
end

.disable_trace(str) ⇒ Object

> :void



212
213
214
 
# File 'lib/z3/low_level_auto.rb', line 212

def disable_trace(str) #=> :void
  VeryLowLevel.Z3_disable_trace(str)
end

.enable_trace(str) ⇒ Object

> :void



216
217
218
 
# File 'lib/z3/low_level_auto.rb', line 216

def enable_trace(str) #=> :void
  VeryLowLevel.Z3_enable_trace(str)
end

.eval_smtlib2_string(str) ⇒ Object

> :string



220
221
222
 
# 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 ⇒ Object

> :void



224
225
226
 
# 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) ⇒ Object

> :void



228
229
230
 
# 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) ⇒ Object

> :void



232
233
234
 
# 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) ⇒ Object

> :void



236
237
238
 
# 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) ⇒ Object

> :void



240
241
242
 
# 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) ⇒ Object

> :void



244
245
246
 
# 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) ⇒ Object

> :ast_vector_pointer



248
249
250
 
# 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) ⇒ Object

> :ast_vector_pointer



252
253
254
 
# 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) ⇒ Object

> :ast_pointer



256
257
258
 
# 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) ⇒ Object

> :ast_vector_pointer



260
261
262
 
# 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) ⇒ Object

> :ast_pointer



264
265
266
 
# 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) ⇒ Object

> :ast_pointer



268
269
270
 
# 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) ⇒ Object

> :string



272
273
274
 
# 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) ⇒ Object

> :uint



276
277
278
 
# 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) ⇒ Object

> :param_descrs_pointer



280
281
282
 
# 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) ⇒ Object

> :ast_pointer



284
285
286
 
# 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) ⇒ Object

> :string



288
289
290
 
# 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) ⇒ Object

> :symbol_pointer



292
293
294
 
# 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) ⇒ Object

> :ast_vector_pointer



296
297
298
 
# 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) ⇒ Object

> :ast_vector_pointer



300
301
302
 
# 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) ⇒ Object

> :stats_pointer



304
305
306
 
# 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) ⇒ Object

> :void



308
309
310
 
# 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) ⇒ Object

> :int



312
313
314
 
# 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) ⇒ Object

> :int



316
317
318
 
# 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) ⇒ Object

> :void



320
321
322
 
# 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) ⇒ Object

> :void



324
325
326
 
# 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) ⇒ Object

> :void



328
329
330
 
# 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) ⇒ Object

> :uint



332
333
334
 
# 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) ⇒ Object

> :ast_pointer



336
337
338
 
# 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) ⇒ Object

> :string



340
341
342
 
# 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) ⇒ Object

> :ast_pointer



344
345
346
 
# 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) ⇒ Object

> :ast_pointer



348
349
350
 
# 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) ⇒ Object

> :string



352
353
354
 
# 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) ⇒ Object

> :uint



356
357
358
 
# 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) ⇒ Object

> :bool



360
361
362
 
# 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) ⇒ Object

> :bool



364
365
366
 
# 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) ⇒ Object

> :bool



368
369
370
 
# 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) ⇒ Object

> :bool



372
373
374
 
# 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) ⇒ Object

> :bool



376
377
378
 
# 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) ⇒ Object

> :bool



380
381
382
 
# 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) ⇒ Object

> :bool



384
385
386
 
# 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) ⇒ Object

> :void



388
389
390
 
# 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) ⇒ Object

> :ast_pointer



392
393
394
 
# 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) ⇒ Object

> :uint



396
397
398
 
# 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) ⇒ Object

> :ast_pointer



400
401
402
 
# 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) ⇒ Object

> :void



404
405
406
 
# 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) ⇒ Object

> :void



408
409
410
 
# 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) ⇒ Object

> :void



412
413
414
 
# 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) ⇒ Object

> :uint



416
417
418
 
# 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) ⇒ Object

> :ast_pointer



420
421
422
 
# 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) ⇒ Object

> :func_entry_pointer



424
425
426
 
# 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) ⇒ Object

> :uint



428
429
430
 
# 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) ⇒ Object

> :void



432
433
434
 
# 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) ⇒ Object

> :void



436
437
438
 
# 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) ⇒ Object

> :ast_pointer



440
441
442
 
# 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) ⇒ Object

> :ast_pointer



444
445
446
 
# 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) ⇒ Object

> :ast_pointer



448
449
450
 
# 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) ⇒ Object

> :func_decl_pointer



452
453
454
 
# 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) ⇒ Object

> :uint



456
457
458
 
# 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) ⇒ Object

> :uint



460
461
462
 
# 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) ⇒ Object

> :sort_pointer



464
465
466
 
# 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) ⇒ Object

> :sort_pointer



468
469
470
 
# 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) ⇒ Object

> :func_decl_pointer



472
473
474
 
# 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) ⇒ Object

> :uint



476
477
478
 
# 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) ⇒ Object

> :uint



480
481
482
 
# 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) ⇒ Object

> :uint



484
485
486
 
# 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) ⇒ Object

> :int



488
489
490
 
# 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) ⇒ Object

> :uint



492
493
494
 
# 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) ⇒ Object

> :func_decl_pointer



496
497
498
 
# 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) ⇒ Object

> :func_decl_pointer



500
501
502
 
# 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) ⇒ Object

> :uint



504
505
506
 
# 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) ⇒ Object

> :func_decl_pointer



508
509
510
 
# 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) ⇒ Object

> :ast_pointer



512
513
514
 
# 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) ⇒ Object

> :double



516
517
518
 
# 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) ⇒ Object

> :func_decl_pointer



520
521
522
 
# 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) ⇒ Object

> :int



524
525
526
 
# 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) ⇒ Object

> :uint



528
529
530
 
# 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) ⇒ Object

> :symbol_pointer



532
533
534
 
# 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) ⇒ Object

> :uint



536
537
538
 
# 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) ⇒ Object

> :uint



540
541
542
 
# 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) ⇒ Object

> :string



544
545
546
 
# 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) ⇒ Object

> :sort_pointer



548
549
550
 
# 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) ⇒ Object

> :symbol_pointer



552
553
554
 
# 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) ⇒ Object

> :ast_pointer



556
557
558
 
# 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) ⇒ Object

> :sort_pointer



560
561
562
 
# 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) ⇒ Object

> :uint



564
565
566
 
# 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 ⇒ Object

> :uint



568
569
570
 
# 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 ⇒ Object

> :string



572
573
574
 
# 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) ⇒ Object

> :uint



576
577
578
 
# 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) ⇒ Object

> :uint



580
581
582
 
# 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 ⇒ Object

> :uint



584
585
586
 
# 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 ⇒ Object

> :uint



588
589
590
 
# 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) ⇒ Object

> :string



592
593
594
 
# 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) ⇒ Object

> :string



596
597
598
 
# 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) ⇒ Object

> :double



600
601
602
 
# 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) ⇒ Object

> :string



604
605
606
 
# 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) ⇒ Object

> :ast_pointer



608
609
610
 
# 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) ⇒ Object

> :ast_pointer



612
613
614
 
# 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) ⇒ Object

> :uint



616
617
618
 
# 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) ⇒ Object

> :string



620
621
622
 
# 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) ⇒ Object

> :ast_pointer



624
625
626
 
# 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) ⇒ Object

> :symbol_pointer



628
629
630
 
# 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) ⇒ Object

> :sort_pointer



632
633
634
 
# 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) ⇒ Object

> :ast_pointer



636
637
638
 
# 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) ⇒ Object

> :uint



640
641
642
 
# 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) ⇒ Object

> :uint



644
645
646
 
# 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) ⇒ Object

> :uint



648
649
650
 
# 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) ⇒ Object

> :pattern_pointer



652
653
654
 
# 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) ⇒ Object

> :uint



656
657
658
 
# 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) ⇒ Object

> :sort_pointer



660
661
662
 
# 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) ⇒ Object

> :sort_pointer



664
665
666
 
# 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) ⇒ Object

> :uint



668
669
670
 
# 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) ⇒ Object

> :sort_pointer



672
673
674
 
# 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) ⇒ Object

> :sort_pointer



676
677
678
 
# 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) ⇒ Object

> :sort_pointer



680
681
682
 
# 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) ⇒ Object

> :uint



684
685
686
 
# 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) ⇒ Object

> :uint



688
689
690
 
# 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) ⇒ Object

> :symbol_pointer



692
693
694
 
# 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) ⇒ Object

> :uint



696
697
698
 
# 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) ⇒ Object

> :int



700
701
702
 
# 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) ⇒ Object

> :uint



704
705
706
 
# 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) ⇒ Object

> :string



708
709
710
 
# 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) ⇒ Object

> :string



712
713
714
 
# 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) ⇒ Object

> :func_decl_pointer



716
717
718
 
# 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) ⇒ Object

> :func_decl_pointer



720
721
722
 
# 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) ⇒ Object

> :uint



724
725
726
 
# 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 ⇒ Object 



7
8
9
10
11
12
13
14
 
# 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 ⇒ Object

> :void



728
729
730
 
# 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) ⇒ Object

> :void



732
733
734
 
# 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) ⇒ Object

> :void



736
737
738
 
# 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) ⇒ Object

> :model_pointer



740
741
742
 
# 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) ⇒ Object

> :void



744
745
746
 
# 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) ⇒ Object

> :uint



748
749
750
 
# 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) ⇒ Object

> :ast_pointer



752
753
754
 
# 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) ⇒ Object

> :void



756
757
758
 
# 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) ⇒ Object

> :bool



760
761
762
 
# 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) ⇒ Object

> :bool



764
765
766
 
# 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) ⇒ Object

> :bool



768
769
770
 
# 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) ⇒ Object

> :uint



772
773
774
 
# 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) ⇒ Object

> :uint



776
777
778
 
# 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) ⇒ Object

> :void



780
781
782
 
# 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) ⇒ Object

> :uint



784
785
786
 
# 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) ⇒ Object

> :string



788
789
790
 
# 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) ⇒ Object

> :string



792
793
794
 
# 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) ⇒ Object

> :goal_pointer



796
797
798
 
# 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) ⇒ Object

> :void



800
801
802
 
# File 'lib/z3/low_level_auto.rb', line 800

def inc_ref(ast) #=> :void
  VeryLowLevel.Z3_inc_ref(_ctx_pointer, ast._ast)
end

.interrupt ⇒ Object

> :void



804
805
806
 
# File 'lib/z3/low_level_auto.rb', line 804

def interrupt #=> :void
  VeryLowLevel.Z3_interrupt(_ctx_pointer)
end

.is_algebraic_number(ast) ⇒ Object

> :bool



808
809
810
 
# 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) ⇒ Object

> :bool



812
813
814
 
# 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) ⇒ Object

> :bool



816
817
818
 
# 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) ⇒ Object

> :bool



820
821
822
 
# 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) ⇒ Object

> :bool



824
825
826
 
# 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) ⇒ Object

> :bool



828
829
830
 
# 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) ⇒ Object

> :bool



832
833
834
 
# 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) ⇒ Object

> :bool



836
837
838
 
# 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) ⇒ Object

> :bool



840
841
842
 
# 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) ⇒ Object

> :bool



844
845
846
 
# 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) ⇒ Object

> :bool



848
849
850
 
# 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) ⇒ Object

> :bool



852
853
854
 
# 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) ⇒ Object 



46
47
48
 
# 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) ⇒ Object 



34
35
36
 
# 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) ⇒ Object

> :ast_pointer



856
857
858
 
# 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) ⇒ Object

> :sort_pointer



860
861
862
 
# 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) ⇒ Object

> :ast_pointer



864
865
866
 
# 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 ⇒ Object

> :ast_map_pointer



868
869
870
 
# 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 ⇒ Object

> :ast_vector_pointer



872
873
874
 
# 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 ⇒ Object

> :sort_pointer



876
877
878
 
# 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) ⇒ Object

> :ast_pointer



880
881
882
 
# 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) ⇒ Object

> :ast_pointer



884
885
886
 
# 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) ⇒ Object

> :sort_pointer



888
889
890
 
# 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) ⇒ Object

> :ast_pointer



892
893
894
 
# 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) ⇒ Object

> :ast_pointer



896
897
898
 
# 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) ⇒ Object

> :ast_pointer



900
901
902
 
# 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) ⇒ Object

> :ast_pointer



904
905
906
 
# 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) ⇒ Object

> :ast_pointer



908
909
910
 
# 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) ⇒ Object

> :ast_pointer



912
913
914
 
# 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) ⇒ Object

> :ast_pointer



916
917
918
 
# 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) ⇒ Object

> :ast_pointer



920
921
922
 
# 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) ⇒ Object

> :ast_pointer



924
925
926
 
# 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) ⇒ Object

> :ast_pointer



928
929
930
 
# 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) ⇒ Object

> :ast_pointer



932
933
934
 
# 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) ⇒ Object

> :ast_pointer



936
937
938
 
# 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) ⇒ Object

> :ast_pointer



940
941
942
 
# 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) ⇒ Object

> :ast_pointer



944
945
946
 
# 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) ⇒ Object

> :ast_pointer



948
949
950
 
# 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) ⇒ Object

> :ast_pointer



952
953
954
 
# 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) ⇒ Object

> :ast_pointer



956
957
958
 
# 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) ⇒ Object

> :ast_pointer



960
961
962
 
# 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) ⇒ Object

> :ast_pointer



964
965
966
 
# 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) ⇒ Object

> :ast_pointer



968
969
970
 
# 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) ⇒ Object

> :ast_pointer



972
973
974
 
# 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) ⇒ Object

> :ast_pointer



976
977
978
 
# 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) ⇒ Object

> :ast_pointer



980
981
982
 
# 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) ⇒ Object

> :ast_pointer



984
985
986
 
# 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) ⇒ Object

> :ast_pointer



988
989
990
 
# 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) ⇒ Object

> :ast_pointer



992
993
994
 
# 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) ⇒ Object

> :ast_pointer



996
997
998
 
# 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) ⇒ Object

> :ast_pointer



1000
1001
1002
 
# 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) ⇒ Object

> :ast_pointer



1004
1005
1006
 
# 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) ⇒ Object

> :ast_pointer



1008
1009
1010
 
# 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) ⇒ Object

> :ast_pointer



1012
1013
1014
 
# 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) ⇒ Object

> :ast_pointer



1016
1017
1018
 
# 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) ⇒ Object

> :ast_pointer



1020
1021
1022
 
# 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) ⇒ Object

> :ast_pointer



1024
1025
1026
 
# 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) ⇒ Object

> :ast_pointer



1028
1029
1030
 
# 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) ⇒ Object

> :ast_pointer



1032
1033
1034
 
# 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) ⇒ Object

> :ast_pointer



1036
1037
1038
 
# 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) ⇒ Object

> :ast_pointer



1040
1041
1042
 
# 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) ⇒ Object

> :ast_pointer



1044
1045
1046
 
# 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) ⇒ Object

> :ast_pointer



1048
1049
1050
 
# 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 ⇒ Object

> :sort_pointer



1052
1053
1054
 
# 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) ⇒ Object

> :ast_pointer



1056
1057
1058
 
# 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) ⇒ Object

> :ast_pointer



1060
1061
1062
 
# 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) ⇒ Object

> :ast_pointer



1064
1065
1066
 
# 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 ⇒ Object

> :config_pointer



1068
1069
1070
 
# File 'lib/z3/low_level_auto.rb', line 1068

def mk_config #=> :config_pointer
  VeryLowLevel.Z3_mk_config()
end

.mk_const(sym, sort) ⇒ Object

> :ast_pointer



1072
1073
1074
 
# 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) ⇒ Object

> :ast_pointer



1076
1077
1078
 
# 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 ⇒ Object 



20
21
22
 
# 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) ⇒ Object

> :ctx_pointer



1080
1081
1082
 
# 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) ⇒ Object 



54
55
56
 
# 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) ⇒ Object

> :ast_pointer



1084
1085
1086
 
# 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) ⇒ Object

> :ast_pointer



1088
1089
1090
 
# 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) ⇒ Object

> :ast_pointer



1092
1093
1094
 
# 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) ⇒ Object

> :ast_pointer



1096
1097
1098
 
# 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) ⇒ Object

> :ast_pointer



1100
1101
1102
 
# 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) ⇒ Object

> :ast_pointer



1104
1105
1106
 
# 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) ⇒ Object

> :ast_pointer



1108
1109
1110
 
# 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 ⇒ Object

> :ast_pointer



1112
1113
1114
 
# 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) ⇒ Object

> :sort_pointer



1116
1117
1118
 
# 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 ⇒ Object

> :fixedpoint_pointer



1120
1121
1122
 
# 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) ⇒ Object

> :ast_pointer



1124
1125
1126
 
# 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) ⇒ Object

> :ast_pointer



1128
1129
1130
 
# 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) ⇒ Object

> :ast_pointer



1132
1133
1134
 
# 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) ⇒ Object

> :ast_pointer



1136
1137
1138
 
# 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) ⇒ Object

> :ast_pointer



1140
1141
1142
 
# 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) ⇒ Object

> :ast_pointer



1144
1145
1146
 
# 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) ⇒ Object

> :ast_pointer



1148
1149
1150
 
# 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) ⇒ Object

> :ast_pointer



1152
1153
1154
 
# 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) ⇒ Object

> :ast_pointer



1156
1157
1158
 
# 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) ⇒ Object

> :ast_pointer



1160
1161
1162
 
# 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) ⇒ Object

> :ast_pointer



1164
1165
1166
 
# 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) ⇒ Object

> :ast_pointer



1168
1169
1170
 
# 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) ⇒ Object

> :ast_pointer



1172
1173
1174
 
# 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) ⇒ Object

> :ast_pointer



1176
1177
1178
 
# 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) ⇒ Object

> :ast_pointer



1180
1181
1182
 
# 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) ⇒ Object

> :ast_pointer



1184
1185
1186
 
# 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) ⇒ Object

> :ast_pointer



1188
1189
1190
 
# 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) ⇒ Object

> :ast_pointer



1192
1193
1194
 
# 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) ⇒ Object

> :ast_pointer



1196
1197
1198
 
# 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) ⇒ Object

> :ast_pointer



1200
1201
1202
 
# 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) ⇒ Object

> :ast_pointer



1204
1205
1206
 
# 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) ⇒ Object

> :ast_pointer



1208
1209
1210
 
# 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) ⇒ Object

> :ast_pointer



1212
1213
1214
 
# 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) ⇒ Object

> :ast_pointer



1216
1217
1218
 
# 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) ⇒ Object

> :ast_pointer



1220
1221
1222
 
# 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) ⇒ Object

> :ast_pointer



1224
1225
1226
 
# 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) ⇒ Object

> :ast_pointer



1228
1229
1230
 
# 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) ⇒ Object

> :ast_pointer



1232
1233
1234
 
# 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 ⇒ Object

> :ast_pointer



1236
1237
1238
 
# 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 ⇒ Object

> :ast_pointer



1240
1241
1242
 
# 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) ⇒ Object

> :ast_pointer



1244
1245
1246
 
# 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 ⇒ Object

> :ast_pointer



1248
1249
1250
 
# 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 ⇒ Object

> :ast_pointer



1252
1253
1254
 
# 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 ⇒ Object

> :ast_pointer



1256
1257
1258
 
# 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 ⇒ Object

> :sort_pointer



1260
1261
1262
 
# 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) ⇒ Object

> :sort_pointer



1264
1265
1266
 
# 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 ⇒ Object

> :sort_pointer



1268
1269
1270
 
# 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 ⇒ Object

> :sort_pointer



1272
1273
1274
 
# 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 ⇒ Object

> :sort_pointer



1276
1277
1278
 
# 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 ⇒ Object

> :sort_pointer



1280
1281
1282
 
# 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 ⇒ Object

> :sort_pointer



1284
1285
1286
 
# 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 ⇒ Object

> :sort_pointer



1288
1289
1290
 
# 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 ⇒ Object

> :sort_pointer



1292
1293
1294
 
# 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 ⇒ Object

> :sort_pointer



1296
1297
1298
 
# 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) ⇒ Object

> :ast_pointer



1300
1301
1302
 
# 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) ⇒ Object

> :ast_pointer



1304
1305
1306
 
# 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) ⇒ Object

> :ast_pointer



1308
1309
1310
 
# 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) ⇒ Object

> :ast_pointer



1312
1313
1314
 
# 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) ⇒ Object

> :ast_pointer



1316
1317
1318
 
# 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) ⇒ Object

> :ast_pointer



1320
1321
1322
 
# 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) ⇒ Object

> :ast_pointer



1324
1325
1326
 
# 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) ⇒ Object

> :ast_pointer



1328
1329
1330
 
# 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) ⇒ Object

> :ast_pointer



1332
1333
1334
 
# 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) ⇒ Object

> :ast_pointer



1336
1337
1338
 
# 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) ⇒ Object

> :ast_pointer



1340
1341
1342
 
# 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) ⇒ Object

> :ast_pointer



1344
1345
1346
 
# 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) ⇒ Object

> :ast_pointer



1348
1349
1350
 
# 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) ⇒ Object

> :ast_pointer



1352
1353
1354
 
# 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) ⇒ Object

> :ast_pointer



1356
1357
1358
 
# 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) ⇒ Object

> :ast_pointer



1360
1361
1362
 
# 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) ⇒ Object

> :goal_pointer



1364
1365
1366
 
# 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) ⇒ Object

> :ast_pointer



1368
1369
1370
 
# 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) ⇒ Object

> :ast_pointer



1372
1373
1374
 
# 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) ⇒ Object

> :ast_pointer



1376
1377
1378
 
# 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) ⇒ Object

> :ast_pointer



1380
1381
1382
 
# 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) ⇒ Object

> :ast_pointer



1384
1385
1386
 
# 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) ⇒ Object

> :ast_pointer



1388
1389
1390
 
# 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) ⇒ Object

> :ast_pointer



1392
1393
1394
 
# 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 ⇒ Object

> :sort_pointer



1396
1397
1398
 
# 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) ⇒ Object

> :symbol_pointer



1400
1401
1402
 
# 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) ⇒ Object

> :ast_pointer



1404
1405
1406
 
# 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) ⇒ Object

> :ast_pointer



1408
1409
1410
 
# 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) ⇒ Object

> :ast_pointer



1412
1413
1414
 
# 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) ⇒ Object

> :ast_pointer



1416
1417
1418
 
# 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) ⇒ Object

> :func_decl_pointer



1420
1421
1422
 
# 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) ⇒ Object

> :ast_pointer



1424
1425
1426
 
# 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) ⇒ Object

> :ast_pointer



1428
1429
1430
 
# 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) ⇒ Object

> :ast_pointer



1432
1433
1434
 
# 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 ⇒ Object

> :model_pointer



1436
1437
1438
 
# File 'lib/z3/low_level_auto.rb', line 1436

def mk_model #=> :model_pointer
  VeryLowLevel.Z3_mk_model(_ctx_pointer)
end

.mk_mul(asts) ⇒ Object 



42
43
44
 
# 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) ⇒ Object

> :ast_pointer



1440
1441
1442
 
# 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) ⇒ Object

> :ast_pointer



1444
1445
1446
 
# 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 ⇒ Object

> :optimize_pointer



1448
1449
1450
 
# File 'lib/z3/low_level_auto.rb', line 1448

def mk_optimize #=> :optimize_pointer
  VeryLowLevel.Z3_mk_optimize(_ctx_pointer)
end

.mk_or(asts) ⇒ Object 



38
39
40
 
# 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 ⇒ Object

> :params_pointer



1452
1453
1454
 
# 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) ⇒ Object

> :func_decl_pointer



1456
1457
1458
 
# 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) ⇒ Object

> :func_decl_pointer



1460
1461
1462
 
# 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) ⇒ Object

> :ast_pointer



1464
1465
1466
 
# 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) ⇒ Object

> :probe_pointer



1468
1469
1470
 
# 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) ⇒ Object

> :ast_pointer



1472
1473
1474
 
# 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) ⇒ Object

> :ast_pointer



1476
1477
1478
 
# 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) ⇒ Object

> :ast_pointer



1480
1481
1482
 
# 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) ⇒ Object

> :ast_pointer



1484
1485
1486
 
# 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) ⇒ Object

> :ast_pointer



1488
1489
1490
 
# 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) ⇒ Object

> :ast_pointer



1492
1493
1494
 
# 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) ⇒ Object

> :ast_pointer



1496
1497
1498
 
# 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) ⇒ Object

> :ast_pointer



1500
1501
1502
 
# 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 ⇒ Object

> :sort_pointer



1504
1505
1506
 
# 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) ⇒ Object

> :ast_pointer



1508
1509
1510
 
# 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) ⇒ Object

> :ast_pointer



1512
1513
1514
 
# 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) ⇒ Object

> :ast_pointer



1516
1517
1518
 
# 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) ⇒ Object

> :ast_pointer



1520
1521
1522
 
# 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) ⇒ Object

> :ast_pointer



1524
1525
1526
 
# 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) ⇒ Object

> :ast_pointer



1528
1529
1530
 
# 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) ⇒ Object

> :ast_pointer



1532
1533
1534
 
# 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) ⇒ Object

> :ast_pointer



1536
1537
1538
 
# 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) ⇒ Object

> :ast_pointer



1540
1541
1542
 
# 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) ⇒ Object

> :ast_pointer



1544
1545
1546
 
# 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) ⇒ Object

> :ast_pointer



1548
1549
1550
 
# 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) ⇒ Object

> :ast_pointer



1552
1553
1554
 
# 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) ⇒ Object

> :ast_pointer



1556
1557
1558
 
# 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) ⇒ Object 



62
63
64
 
# 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) ⇒ Object

> :ast_pointer



1560
1561
1562
 
# 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) ⇒ Object

> :sort_pointer



1564
1565
1566
 
# 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) ⇒ Object

> :ast_pointer



1568
1569
1570
 
# 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) ⇒ Object 



58
59
60
 
# 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) ⇒ Object

> :ast_pointer



1572
1573
1574
 
# 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 ⇒ Object

> :solver_pointer



1576
1577
1578
 
# 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 ⇒ Object

> :solver_pointer



1580
1581
1582
 
# 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) ⇒ Object

> :solver_pointer



1584
1585
1586
 
# 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) ⇒ Object

> :solver_pointer



1588
1589
1590
 
# 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) ⇒ Object

> :ast_pointer



1592
1593
1594
 
# 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) ⇒ Object

> :ast_pointer



1596
1597
1598
 
# 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) ⇒ Object

> :ast_pointer



1600
1601
1602
 
# 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) ⇒ Object

> :ast_pointer



1604
1605
1606
 
# 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) ⇒ Object

> :symbol_pointer



1608
1609
1610
 
# 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) ⇒ Object 



50
51
52
 
# 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) ⇒ Object

> :tactic_pointer



1612
1613
1614
 
# 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) ⇒ Object

> :func_decl_pointer



1616
1617
1618
 
# 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) ⇒ Object

> :func_decl_pointer



1620
1621
1622
 
# 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 ⇒ Object

> :ast_pointer



1624
1625
1626
 
# 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) ⇒ Object

> :ast_pointer



1628
1629
1630
 
# 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) ⇒ Object

> :ast_pointer



1632
1633
1634
 
# 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) ⇒ Object

> :sort_pointer



1636
1637
1638
 
# 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) ⇒ Object

> :ast_pointer



1640
1641
1642
 
# 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) ⇒ Object

> :ast_pointer



1644
1645
1646
 
# 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) ⇒ Object

> :ast_pointer



1648
1649
1650
 
# 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) ⇒ Object

> :ast_pointer



1652
1653
1654
 
# 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) ⇒ Object

> :void



1656
1657
1658
 
# 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) ⇒ Object 



24
25
26
27
28
29
30
31
32
 
# 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) ⇒ Object

> :ast_pointer



1660
1661
1662
 
# 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) ⇒ Object

> :func_decl_pointer



1664
1665
1666
 
# 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) ⇒ Object

> :ast_pointer



1668
1669
1670
 
# 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) ⇒ Object

> :func_decl_pointer



1672
1673
1674
 
# 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) ⇒ Object

> :func_interp_pointer



1676
1677
1678
 
# 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) ⇒ Object

> :uint



1680
1681
1682
 
# 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) ⇒ Object

> :uint



1684
1685
1686
 
# 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) ⇒ Object

> :uint



1688
1689
1690
 
# 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) ⇒ Object

> :sort_pointer



1692
1693
1694
 
# 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) ⇒ Object

> :ast_vector_pointer



1696
1697
1698
 
# 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) ⇒ Object

> :bool



1700
1701
1702
 
# 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) ⇒ Object

> :void



1704
1705
1706
 
# 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) ⇒ Object

> :string



1708
1709
1710
 
# 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) ⇒ Object

> :model_pointer



1712
1713
1714
 
# 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) ⇒ Object

> :void



1716
1717
1718
 
# 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) ⇒ Object

> :void



1720
1721
1722
 
# 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) ⇒ Object

> :uint



1724
1725
1726
 
# 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) ⇒ Object 



66
67
68
 
# 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) ⇒ Object

> :void



1728
1729
1730
 
# 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) ⇒ Object

> :void



1732
1733
1734
 
# 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) ⇒ Object

> :void



1736
1737
1738
 
# 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) ⇒ Object

> :ast_vector_pointer



1740
1741
1742
 
# 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) ⇒ Object

> :string



1744
1745
1746
 
# 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) ⇒ Object

> :ast_pointer



1748
1749
1750
 
# 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) ⇒ Object

> :ast_vector_pointer



1752
1753
1754
 
# 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) ⇒ Object

> :model_pointer



1756
1757
1758
 
# 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) ⇒ Object

> :ast_vector_pointer



1760
1761
1762
 
# 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) ⇒ Object

> :param_descrs_pointer



1764
1765
1766
 
# 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) ⇒ Object

> :string



1768
1769
1770
 
# 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) ⇒ Object

> :stats_pointer



1772
1773
1774
 
# 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) ⇒ Object

> :ast_vector_pointer



1776
1777
1778
 
# 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) ⇒ Object

> :ast_pointer



1780
1781
1782
 
# 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) ⇒ Object

> :ast_vector_pointer



1784
1785
1786
 
# 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) ⇒ Object

> :void



1788
1789
1790
 
# 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) ⇒ Object

> :uint



1792
1793
1794
 
# 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) ⇒ Object

> :uint



1796
1797
1798
 
# 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) ⇒ Object

> :void



1800
1801
1802
 
# 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) ⇒ Object

> :void



1804
1805
1806
 
# 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) ⇒ Object

> :void



1808
1809
1810
 
# 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) ⇒ Object

> :string



1812
1813
1814
 
# 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) ⇒ Object

> :void



1816
1817
1818
 
# 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) ⇒ Object

> :uint



1820
1821
1822
 
# 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) ⇒ Object

> :symbol_pointer



1824
1825
1826
 
# 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) ⇒ Object

> :void



1828
1829
1830
 
# 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) ⇒ Object

> :uint



1832
1833
1834
 
# 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) ⇒ Object

> :string



1836
1837
1838
 
# 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) ⇒ Object

> :void



1840
1841
1842
 
# 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) ⇒ Object

> :void



1844
1845
1846
 
# 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) ⇒ Object

> :void



1848
1849
1850
 
# 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) ⇒ Object

> :void



1852
1853
1854
 
# 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) ⇒ Object

> :void



1856
1857
1858
 
# 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) ⇒ Object

> :void



1860
1861
1862
 
# 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) ⇒ Object

> :string



1864
1865
1866
 
# 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) ⇒ Object

> :void



1868
1869
1870
 
# 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) ⇒ Object

> :string



1872
1873
1874
 
# 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) ⇒ Object

> :ast_vector_pointer



1876
1877
1878
 
# 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) ⇒ Object

> :probe_pointer



1880
1881
1882
 
# 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) ⇒ Object

> :double



1884
1885
1886
 
# 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) ⇒ Object

> :probe_pointer



1888
1889
1890
 
# 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) ⇒ Object

> :void



1892
1893
1894
 
# 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) ⇒ Object

> :probe_pointer



1896
1897
1898
 
# 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) ⇒ Object

> :probe_pointer



1900
1901
1902
 
# 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) ⇒ Object

> :string



1904
1905
1906
 
# 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) ⇒ Object

> :probe_pointer



1908
1909
1910
 
# 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) ⇒ Object

> :void



1912
1913
1914
 
# 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) ⇒ Object

> :probe_pointer



1916
1917
1918
 
# 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) ⇒ Object

> :probe_pointer



1920
1921
1922
 
# 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) ⇒ Object

> :probe_pointer



1924
1925
1926
 
# 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) ⇒ Object

> :probe_pointer



1928
1929
1930
 
# 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) ⇒ Object

> :ast_pointer



1932
1933
1934
 
# 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) ⇒ Object

> :rcf_num_pointer



1936
1937
1938
 
# 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) ⇒ Object

> :void



1940
1941
1942
 
# 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) ⇒ Object

> :rcf_num_pointer



1944
1945
1946
 
# 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) ⇒ Object

> :bool



1948
1949
1950
 
# 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) ⇒ Object

> :bool



1952
1953
1954
 
# 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) ⇒ Object

> :bool



1956
1957
1958
 
# 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) ⇒ Object

> :rcf_num_pointer



1960
1961
1962
 
# 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) ⇒ Object

> :bool



1964
1965
1966
 
# 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) ⇒ Object

> :bool



1968
1969
1970
 
# 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 ⇒ Object

> :rcf_num_pointer



1972
1973
1974
 
# 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 ⇒ Object

> :rcf_num_pointer



1976
1977
1978
 
# 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 ⇒ Object

> :rcf_num_pointer



1980
1981
1982
 
# 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) ⇒ Object

> :rcf_num_pointer



1984
1985
1986
 
# 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) ⇒ Object

> :rcf_num_pointer



1988
1989
1990
 
# 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) ⇒ Object

> :rcf_num_pointer



1992
1993
1994
 
# 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) ⇒ Object

> :rcf_num_pointer



1996
1997
1998
 
# 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) ⇒ Object

> :bool



2000
2001
2002
 
# 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) ⇒ Object

> :string



2004
2005
2006
 
# 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) ⇒ Object

> :string



2008
2009
2010
 
# 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) ⇒ Object

> :rcf_num_pointer



2012
2013
2014
 
# 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) ⇒ Object

> :rcf_num_pointer



2016
2017
2018
 
# 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 ⇒ Object

> :void



2020
2021
2022
 
# File 'lib/z3/low_level_auto.rb', line 2020

def reset_memory #=> :void
  VeryLowLevel.Z3_reset_memory()
end

.set_error_handler(&block) ⇒ Object 



16
17
18
 
# 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) ⇒ Object

> :void



2024
2025
2026
 
# 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) ⇒ Object

> :ast_pointer



2028
2029
2030
 
# 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) ⇒ Object

> :ast_pointer



2032
2033
2034
 
# 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 ⇒ Object

> :string



2036
2037
2038
 
# 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 ⇒ Object

> :param_descrs_pointer



2040
2041
2042
 
# 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) ⇒ Object

> :void



2044
2045
2046
 
# 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) ⇒ Object

> :void



2048
2049
2050
 
# 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) ⇒ Object

> :int



2052
2053
2054
 
# 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) ⇒ Object

> :ast_vector_pointer



2056
2057
2058
 
# 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) ⇒ Object

> :void



2060
2061
2062
 
# 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) ⇒ Object

> :void



2064
2065
2066
 
# 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) ⇒ Object

> :void



2068
2069
2070
 
# 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) ⇒ Object

> :ast_vector_pointer



2072
2073
2074
 
# 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) ⇒ Object

> :int



2076
2077
2078
 
# 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) ⇒ Object

> :string



2080
2081
2082
 
# 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) ⇒ Object

> :model_pointer



2084
2085
2086
 
# 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) ⇒ Object

> :ast_vector_pointer



2088
2089
2090
 
# 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) ⇒ Object

> :uint



2092
2093
2094
 
# 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) ⇒ Object

> :param_descrs_pointer



2096
2097
2098
 
# 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) ⇒ Object

> :ast_pointer



2100
2101
2102
 
# 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) ⇒ Object

> :string



2104
2105
2106
 
# 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) ⇒ Object

> :stats_pointer



2108
2109
2110
 
# 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) ⇒ Object

> :ast_vector_pointer



2112
2113
2114
 
# 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) ⇒ Object

> :ast_vector_pointer



2116
2117
2118
 
# 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) ⇒ Object

> :ast_vector_pointer



2120
2121
2122
 
# 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) ⇒ Object

> :void



2124
2125
2126
 
# 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) ⇒ Object

> :void



2128
2129
2130
 
# 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) ⇒ Object

> :void



2132
2133
2134
 
# 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) ⇒ Object

> :void



2136
2137
2138
 
# 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) ⇒ Object

> :uint



2140
2141
2142
 
# 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) ⇒ Object

> :void



2144
2145
2146
 
# 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) ⇒ Object

> :void



2148
2149
2150
 
# 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) ⇒ Object

> :void



2152
2153
2154
 
# 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) ⇒ Object

> :string



2156
2157
2158
 
# 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) ⇒ Object

> :string



2160
2161
2162
 
# 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) ⇒ Object

> :void



2164
2165
2166
 
# 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) ⇒ Object

> :double



2168
2169
2170
 
# 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) ⇒ Object

> :string



2172
2173
2174
 
# 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) ⇒ Object

> :uint



2176
2177
2178
 
# 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) ⇒ Object

> :void



2180
2181
2182
 
# 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) ⇒ Object

> :bool



2184
2185
2186
 
# 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) ⇒ Object

> :bool



2188
2189
2190
 
# 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) ⇒ Object

> :uint



2192
2193
2194
 
# 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) ⇒ Object

> :string



2196
2197
2198
 
# 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) ⇒ Object

> :tactic_pointer



2200
2201
2202
 
# 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) ⇒ Object

> :apply_result_pointer



2204
2205
2206
 
# 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) ⇒ Object

> :apply_result_pointer



2208
2209
2210
 
# 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) ⇒ Object

> :tactic_pointer



2212
2213
2214
 
# 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) ⇒ Object

> :void



2216
2217
2218
 
# 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 ⇒ Object

> :tactic_pointer



2220
2221
2222
 
# 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) ⇒ Object

> :tactic_pointer



2224
2225
2226
 
# 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 ⇒ Object

> :tactic_pointer



2228
2229
2230
 
# 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) ⇒ Object

> :string



2232
2233
2234
 
# 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) ⇒ Object

> :string



2236
2237
2238
 
# 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) ⇒ Object

> :param_descrs_pointer



2240
2241
2242
 
# 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) ⇒ Object

> :void



2244
2245
2246
 
# 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) ⇒ Object

> :tactic_pointer



2248
2249
2250
 
# 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) ⇒ Object

> :tactic_pointer



2252
2253
2254
 
# 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) ⇒ Object

> :tactic_pointer



2256
2257
2258
 
# 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 ⇒ Object

> :tactic_pointer



2260
2261
2262
 
# 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) ⇒ Object

> :tactic_pointer



2264
2265
2266
 
# 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) ⇒ Object

> :tactic_pointer



2268
2269
2270
 
# 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) ⇒ Object

> :tactic_pointer



2272
2273
2274
 
# 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) ⇒ Object

> :void



2276
2277
2278
 
# 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) ⇒ Object

> :ast_pointer



2280
2281
2282
 
# 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) ⇒ Object

Should be private



72
73
74
75
76
77
 
# 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) ⇒ Object 



79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
 
# 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) ⇒ Object

> :void



2284
2285
2286
 
# 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