mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
Added API Z3_param_descrs_to_string
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
42c27b7a46
commit
f7bcd40137
|
|
@ -1132,6 +1132,9 @@ namespace Microsoft.Z3
|
||||||
[DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
|
[DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
|
||||||
public extern static IntPtr Z3_param_descrs_get_name(Z3_context a0, Z3_param_descrs a1, uint a2);
|
public extern static IntPtr Z3_param_descrs_get_name(Z3_context a0, Z3_param_descrs a1, uint a2);
|
||||||
|
|
||||||
|
[DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
|
||||||
|
public extern static IntPtr Z3_param_descrs_to_string(Z3_context a0, Z3_param_descrs a1);
|
||||||
|
|
||||||
[DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
|
[DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
|
||||||
public extern static void Z3_interrupt(Z3_context a0);
|
public extern static void Z3_interrupt(Z3_context a0);
|
||||||
|
|
||||||
|
|
@ -4293,6 +4296,14 @@ namespace Microsoft.Z3
|
||||||
return r;
|
return r;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
public static string Z3_param_descrs_to_string(Z3_context a0, Z3_param_descrs a1) {
|
||||||
|
IntPtr r = LIB.Z3_param_descrs_to_string(a0, a1);
|
||||||
|
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
|
||||||
|
if (err != Z3_error_code.Z3_OK)
|
||||||
|
throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
|
||||||
|
return Marshal.PtrToStringAnsi(r);
|
||||||
|
}
|
||||||
|
|
||||||
public static void Z3_interrupt(Z3_context a0) {
|
public static void Z3_interrupt(Z3_context a0) {
|
||||||
LIB.Z3_interrupt(a0);
|
LIB.Z3_interrupt(a0);
|
||||||
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
|
Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
|
||||||
|
|
|
||||||
989
dll/z3.def
989
dll/z3.def
|
|
@ -25,497 +25,498 @@ EXPORTS
|
||||||
Z3_param_descrs_get_kind @23
|
Z3_param_descrs_get_kind @23
|
||||||
Z3_param_descrs_size @24
|
Z3_param_descrs_size @24
|
||||||
Z3_param_descrs_get_name @25
|
Z3_param_descrs_get_name @25
|
||||||
Z3_mk_int_symbol @26
|
Z3_param_descrs_to_string @26
|
||||||
Z3_mk_string_symbol @27
|
Z3_mk_int_symbol @27
|
||||||
Z3_mk_uninterpreted_sort @28
|
Z3_mk_string_symbol @28
|
||||||
Z3_mk_bool_sort @29
|
Z3_mk_uninterpreted_sort @29
|
||||||
Z3_mk_int_sort @30
|
Z3_mk_bool_sort @30
|
||||||
Z3_mk_real_sort @31
|
Z3_mk_int_sort @31
|
||||||
Z3_mk_bv_sort @32
|
Z3_mk_real_sort @32
|
||||||
Z3_mk_finite_domain_sort @33
|
Z3_mk_bv_sort @33
|
||||||
Z3_mk_array_sort @34
|
Z3_mk_finite_domain_sort @34
|
||||||
Z3_mk_tuple_sort @35
|
Z3_mk_array_sort @35
|
||||||
Z3_mk_enumeration_sort @36
|
Z3_mk_tuple_sort @36
|
||||||
Z3_mk_list_sort @37
|
Z3_mk_enumeration_sort @37
|
||||||
Z3_mk_constructor @38
|
Z3_mk_list_sort @38
|
||||||
Z3_del_constructor @39
|
Z3_mk_constructor @39
|
||||||
Z3_mk_datatype @40
|
Z3_del_constructor @40
|
||||||
Z3_mk_constructor_list @41
|
Z3_mk_datatype @41
|
||||||
Z3_del_constructor_list @42
|
Z3_mk_constructor_list @42
|
||||||
Z3_mk_datatypes @43
|
Z3_del_constructor_list @43
|
||||||
Z3_query_constructor @44
|
Z3_mk_datatypes @44
|
||||||
Z3_mk_func_decl @45
|
Z3_query_constructor @45
|
||||||
Z3_mk_app @46
|
Z3_mk_func_decl @46
|
||||||
Z3_mk_const @47
|
Z3_mk_app @47
|
||||||
Z3_mk_fresh_func_decl @48
|
Z3_mk_const @48
|
||||||
Z3_mk_fresh_const @49
|
Z3_mk_fresh_func_decl @49
|
||||||
Z3_mk_true @50
|
Z3_mk_fresh_const @50
|
||||||
Z3_mk_false @51
|
Z3_mk_true @51
|
||||||
Z3_mk_eq @52
|
Z3_mk_false @52
|
||||||
Z3_mk_distinct @53
|
Z3_mk_eq @53
|
||||||
Z3_mk_not @54
|
Z3_mk_distinct @54
|
||||||
Z3_mk_ite @55
|
Z3_mk_not @55
|
||||||
Z3_mk_iff @56
|
Z3_mk_ite @56
|
||||||
Z3_mk_implies @57
|
Z3_mk_iff @57
|
||||||
Z3_mk_xor @58
|
Z3_mk_implies @58
|
||||||
Z3_mk_and @59
|
Z3_mk_xor @59
|
||||||
Z3_mk_or @60
|
Z3_mk_and @60
|
||||||
Z3_mk_add @61
|
Z3_mk_or @61
|
||||||
Z3_mk_mul @62
|
Z3_mk_add @62
|
||||||
Z3_mk_sub @63
|
Z3_mk_mul @63
|
||||||
Z3_mk_unary_minus @64
|
Z3_mk_sub @64
|
||||||
Z3_mk_div @65
|
Z3_mk_unary_minus @65
|
||||||
Z3_mk_mod @66
|
Z3_mk_div @66
|
||||||
Z3_mk_rem @67
|
Z3_mk_mod @67
|
||||||
Z3_mk_power @68
|
Z3_mk_rem @68
|
||||||
Z3_mk_lt @69
|
Z3_mk_power @69
|
||||||
Z3_mk_le @70
|
Z3_mk_lt @70
|
||||||
Z3_mk_gt @71
|
Z3_mk_le @71
|
||||||
Z3_mk_ge @72
|
Z3_mk_gt @72
|
||||||
Z3_mk_int2real @73
|
Z3_mk_ge @73
|
||||||
Z3_mk_real2int @74
|
Z3_mk_int2real @74
|
||||||
Z3_mk_is_int @75
|
Z3_mk_real2int @75
|
||||||
Z3_mk_bvnot @76
|
Z3_mk_is_int @76
|
||||||
Z3_mk_bvredand @77
|
Z3_mk_bvnot @77
|
||||||
Z3_mk_bvredor @78
|
Z3_mk_bvredand @78
|
||||||
Z3_mk_bvand @79
|
Z3_mk_bvredor @79
|
||||||
Z3_mk_bvor @80
|
Z3_mk_bvand @80
|
||||||
Z3_mk_bvxor @81
|
Z3_mk_bvor @81
|
||||||
Z3_mk_bvnand @82
|
Z3_mk_bvxor @82
|
||||||
Z3_mk_bvnor @83
|
Z3_mk_bvnand @83
|
||||||
Z3_mk_bvxnor @84
|
Z3_mk_bvnor @84
|
||||||
Z3_mk_bvneg @85
|
Z3_mk_bvxnor @85
|
||||||
Z3_mk_bvadd @86
|
Z3_mk_bvneg @86
|
||||||
Z3_mk_bvsub @87
|
Z3_mk_bvadd @87
|
||||||
Z3_mk_bvmul @88
|
Z3_mk_bvsub @88
|
||||||
Z3_mk_bvudiv @89
|
Z3_mk_bvmul @89
|
||||||
Z3_mk_bvsdiv @90
|
Z3_mk_bvudiv @90
|
||||||
Z3_mk_bvurem @91
|
Z3_mk_bvsdiv @91
|
||||||
Z3_mk_bvsrem @92
|
Z3_mk_bvurem @92
|
||||||
Z3_mk_bvsmod @93
|
Z3_mk_bvsrem @93
|
||||||
Z3_mk_bvult @94
|
Z3_mk_bvsmod @94
|
||||||
Z3_mk_bvslt @95
|
Z3_mk_bvult @95
|
||||||
Z3_mk_bvule @96
|
Z3_mk_bvslt @96
|
||||||
Z3_mk_bvsle @97
|
Z3_mk_bvule @97
|
||||||
Z3_mk_bvuge @98
|
Z3_mk_bvsle @98
|
||||||
Z3_mk_bvsge @99
|
Z3_mk_bvuge @99
|
||||||
Z3_mk_bvugt @100
|
Z3_mk_bvsge @100
|
||||||
Z3_mk_bvsgt @101
|
Z3_mk_bvugt @101
|
||||||
Z3_mk_concat @102
|
Z3_mk_bvsgt @102
|
||||||
Z3_mk_extract @103
|
Z3_mk_concat @103
|
||||||
Z3_mk_sign_ext @104
|
Z3_mk_extract @104
|
||||||
Z3_mk_zero_ext @105
|
Z3_mk_sign_ext @105
|
||||||
Z3_mk_repeat @106
|
Z3_mk_zero_ext @106
|
||||||
Z3_mk_bvshl @107
|
Z3_mk_repeat @107
|
||||||
Z3_mk_bvlshr @108
|
Z3_mk_bvshl @108
|
||||||
Z3_mk_bvashr @109
|
Z3_mk_bvlshr @109
|
||||||
Z3_mk_rotate_left @110
|
Z3_mk_bvashr @110
|
||||||
Z3_mk_rotate_right @111
|
Z3_mk_rotate_left @111
|
||||||
Z3_mk_ext_rotate_left @112
|
Z3_mk_rotate_right @112
|
||||||
Z3_mk_ext_rotate_right @113
|
Z3_mk_ext_rotate_left @113
|
||||||
Z3_mk_int2bv @114
|
Z3_mk_ext_rotate_right @114
|
||||||
Z3_mk_bv2int @115
|
Z3_mk_int2bv @115
|
||||||
Z3_mk_bvadd_no_overflow @116
|
Z3_mk_bv2int @116
|
||||||
Z3_mk_bvadd_no_underflow @117
|
Z3_mk_bvadd_no_overflow @117
|
||||||
Z3_mk_bvsub_no_overflow @118
|
Z3_mk_bvadd_no_underflow @118
|
||||||
Z3_mk_bvsub_no_underflow @119
|
Z3_mk_bvsub_no_overflow @119
|
||||||
Z3_mk_bvsdiv_no_overflow @120
|
Z3_mk_bvsub_no_underflow @120
|
||||||
Z3_mk_bvneg_no_overflow @121
|
Z3_mk_bvsdiv_no_overflow @121
|
||||||
Z3_mk_bvmul_no_overflow @122
|
Z3_mk_bvneg_no_overflow @122
|
||||||
Z3_mk_bvmul_no_underflow @123
|
Z3_mk_bvmul_no_overflow @123
|
||||||
Z3_mk_select @124
|
Z3_mk_bvmul_no_underflow @124
|
||||||
Z3_mk_store @125
|
Z3_mk_select @125
|
||||||
Z3_mk_const_array @126
|
Z3_mk_store @126
|
||||||
Z3_mk_map @127
|
Z3_mk_const_array @127
|
||||||
Z3_mk_array_default @128
|
Z3_mk_map @128
|
||||||
Z3_mk_set_sort @129
|
Z3_mk_array_default @129
|
||||||
Z3_mk_empty_set @130
|
Z3_mk_set_sort @130
|
||||||
Z3_mk_full_set @131
|
Z3_mk_empty_set @131
|
||||||
Z3_mk_set_add @132
|
Z3_mk_full_set @132
|
||||||
Z3_mk_set_del @133
|
Z3_mk_set_add @133
|
||||||
Z3_mk_set_union @134
|
Z3_mk_set_del @134
|
||||||
Z3_mk_set_intersect @135
|
Z3_mk_set_union @135
|
||||||
Z3_mk_set_difference @136
|
Z3_mk_set_intersect @136
|
||||||
Z3_mk_set_complement @137
|
Z3_mk_set_difference @137
|
||||||
Z3_mk_set_member @138
|
Z3_mk_set_complement @138
|
||||||
Z3_mk_set_subset @139
|
Z3_mk_set_member @139
|
||||||
Z3_mk_numeral @140
|
Z3_mk_set_subset @140
|
||||||
Z3_mk_real @141
|
Z3_mk_numeral @141
|
||||||
Z3_mk_int @142
|
Z3_mk_real @142
|
||||||
Z3_mk_unsigned_int @143
|
Z3_mk_int @143
|
||||||
Z3_mk_int64 @144
|
Z3_mk_unsigned_int @144
|
||||||
Z3_mk_unsigned_int64 @145
|
Z3_mk_int64 @145
|
||||||
Z3_mk_pattern @146
|
Z3_mk_unsigned_int64 @146
|
||||||
Z3_mk_bound @147
|
Z3_mk_pattern @147
|
||||||
Z3_mk_forall @148
|
Z3_mk_bound @148
|
||||||
Z3_mk_exists @149
|
Z3_mk_forall @149
|
||||||
Z3_mk_quantifier @150
|
Z3_mk_exists @150
|
||||||
Z3_mk_quantifier_ex @151
|
Z3_mk_quantifier @151
|
||||||
Z3_mk_forall_const @152
|
Z3_mk_quantifier_ex @152
|
||||||
Z3_mk_exists_const @153
|
Z3_mk_forall_const @153
|
||||||
Z3_mk_quantifier_const @154
|
Z3_mk_exists_const @154
|
||||||
Z3_mk_quantifier_const_ex @155
|
Z3_mk_quantifier_const @155
|
||||||
Z3_get_symbol_kind @156
|
Z3_mk_quantifier_const_ex @156
|
||||||
Z3_get_symbol_int @157
|
Z3_get_symbol_kind @157
|
||||||
Z3_get_symbol_string @158
|
Z3_get_symbol_int @158
|
||||||
Z3_get_sort_name @159
|
Z3_get_symbol_string @159
|
||||||
Z3_get_sort_id @160
|
Z3_get_sort_name @160
|
||||||
Z3_sort_to_ast @161
|
Z3_get_sort_id @161
|
||||||
Z3_is_eq_sort @162
|
Z3_sort_to_ast @162
|
||||||
Z3_get_sort_kind @163
|
Z3_is_eq_sort @163
|
||||||
Z3_get_bv_sort_size @164
|
Z3_get_sort_kind @164
|
||||||
Z3_get_finite_domain_sort_size @165
|
Z3_get_bv_sort_size @165
|
||||||
Z3_get_array_sort_domain @166
|
Z3_get_finite_domain_sort_size @166
|
||||||
Z3_get_array_sort_range @167
|
Z3_get_array_sort_domain @167
|
||||||
Z3_get_tuple_sort_mk_decl @168
|
Z3_get_array_sort_range @168
|
||||||
Z3_get_tuple_sort_num_fields @169
|
Z3_get_tuple_sort_mk_decl @169
|
||||||
Z3_get_tuple_sort_field_decl @170
|
Z3_get_tuple_sort_num_fields @170
|
||||||
Z3_get_datatype_sort_num_constructors @171
|
Z3_get_tuple_sort_field_decl @171
|
||||||
Z3_get_datatype_sort_constructor @172
|
Z3_get_datatype_sort_num_constructors @172
|
||||||
Z3_get_datatype_sort_recognizer @173
|
Z3_get_datatype_sort_constructor @173
|
||||||
Z3_get_datatype_sort_constructor_accessor @174
|
Z3_get_datatype_sort_recognizer @174
|
||||||
Z3_get_relation_arity @175
|
Z3_get_datatype_sort_constructor_accessor @175
|
||||||
Z3_get_relation_column @176
|
Z3_get_relation_arity @176
|
||||||
Z3_func_decl_to_ast @177
|
Z3_get_relation_column @177
|
||||||
Z3_is_eq_func_decl @178
|
Z3_func_decl_to_ast @178
|
||||||
Z3_get_func_decl_id @179
|
Z3_is_eq_func_decl @179
|
||||||
Z3_get_decl_name @180
|
Z3_get_func_decl_id @180
|
||||||
Z3_get_decl_kind @181
|
Z3_get_decl_name @181
|
||||||
Z3_get_domain_size @182
|
Z3_get_decl_kind @182
|
||||||
Z3_get_arity @183
|
Z3_get_domain_size @183
|
||||||
Z3_get_domain @184
|
Z3_get_arity @184
|
||||||
Z3_get_range @185
|
Z3_get_domain @185
|
||||||
Z3_get_decl_num_parameters @186
|
Z3_get_range @186
|
||||||
Z3_get_decl_parameter_kind @187
|
Z3_get_decl_num_parameters @187
|
||||||
Z3_get_decl_int_parameter @188
|
Z3_get_decl_parameter_kind @188
|
||||||
Z3_get_decl_double_parameter @189
|
Z3_get_decl_int_parameter @189
|
||||||
Z3_get_decl_symbol_parameter @190
|
Z3_get_decl_double_parameter @190
|
||||||
Z3_get_decl_sort_parameter @191
|
Z3_get_decl_symbol_parameter @191
|
||||||
Z3_get_decl_ast_parameter @192
|
Z3_get_decl_sort_parameter @192
|
||||||
Z3_get_decl_func_decl_parameter @193
|
Z3_get_decl_ast_parameter @193
|
||||||
Z3_get_decl_rational_parameter @194
|
Z3_get_decl_func_decl_parameter @194
|
||||||
Z3_app_to_ast @195
|
Z3_get_decl_rational_parameter @195
|
||||||
Z3_get_app_decl @196
|
Z3_app_to_ast @196
|
||||||
Z3_get_app_num_args @197
|
Z3_get_app_decl @197
|
||||||
Z3_get_app_arg @198
|
Z3_get_app_num_args @198
|
||||||
Z3_is_eq_ast @199
|
Z3_get_app_arg @199
|
||||||
Z3_get_ast_id @200
|
Z3_is_eq_ast @200
|
||||||
Z3_get_ast_hash @201
|
Z3_get_ast_id @201
|
||||||
Z3_get_sort @202
|
Z3_get_ast_hash @202
|
||||||
Z3_is_well_sorted @203
|
Z3_get_sort @203
|
||||||
Z3_get_bool_value @204
|
Z3_is_well_sorted @204
|
||||||
Z3_get_ast_kind @205
|
Z3_get_bool_value @205
|
||||||
Z3_is_app @206
|
Z3_get_ast_kind @206
|
||||||
Z3_is_numeral_ast @207
|
Z3_is_app @207
|
||||||
Z3_is_algebraic_number @208
|
Z3_is_numeral_ast @208
|
||||||
Z3_to_app @209
|
Z3_is_algebraic_number @209
|
||||||
Z3_to_func_decl @210
|
Z3_to_app @210
|
||||||
Z3_get_numeral_string @211
|
Z3_to_func_decl @211
|
||||||
Z3_get_numeral_decimal_string @212
|
Z3_get_numeral_string @212
|
||||||
Z3_get_numerator @213
|
Z3_get_numeral_decimal_string @213
|
||||||
Z3_get_denominator @214
|
Z3_get_numerator @214
|
||||||
Z3_get_numeral_small @215
|
Z3_get_denominator @215
|
||||||
Z3_get_numeral_int @216
|
Z3_get_numeral_small @216
|
||||||
Z3_get_numeral_uint @217
|
Z3_get_numeral_int @217
|
||||||
Z3_get_numeral_uint64 @218
|
Z3_get_numeral_uint @218
|
||||||
Z3_get_numeral_int64 @219
|
Z3_get_numeral_uint64 @219
|
||||||
Z3_get_numeral_rational_int64 @220
|
Z3_get_numeral_int64 @220
|
||||||
Z3_get_algebraic_number_lower @221
|
Z3_get_numeral_rational_int64 @221
|
||||||
Z3_get_algebraic_number_upper @222
|
Z3_get_algebraic_number_lower @222
|
||||||
Z3_pattern_to_ast @223
|
Z3_get_algebraic_number_upper @223
|
||||||
Z3_get_pattern_num_terms @224
|
Z3_pattern_to_ast @224
|
||||||
Z3_get_pattern @225
|
Z3_get_pattern_num_terms @225
|
||||||
Z3_get_index_value @226
|
Z3_get_pattern @226
|
||||||
Z3_is_quantifier_forall @227
|
Z3_get_index_value @227
|
||||||
Z3_get_quantifier_weight @228
|
Z3_is_quantifier_forall @228
|
||||||
Z3_get_quantifier_num_patterns @229
|
Z3_get_quantifier_weight @229
|
||||||
Z3_get_quantifier_pattern_ast @230
|
Z3_get_quantifier_num_patterns @230
|
||||||
Z3_get_quantifier_num_no_patterns @231
|
Z3_get_quantifier_pattern_ast @231
|
||||||
Z3_get_quantifier_no_pattern_ast @232
|
Z3_get_quantifier_num_no_patterns @232
|
||||||
Z3_get_quantifier_num_bound @233
|
Z3_get_quantifier_no_pattern_ast @233
|
||||||
Z3_get_quantifier_bound_name @234
|
Z3_get_quantifier_num_bound @234
|
||||||
Z3_get_quantifier_bound_sort @235
|
Z3_get_quantifier_bound_name @235
|
||||||
Z3_get_quantifier_body @236
|
Z3_get_quantifier_bound_sort @236
|
||||||
Z3_simplify @237
|
Z3_get_quantifier_body @237
|
||||||
Z3_simplify_ex @238
|
Z3_simplify @238
|
||||||
Z3_simplify_get_help @239
|
Z3_simplify_ex @239
|
||||||
Z3_simplify_get_param_descrs @240
|
Z3_simplify_get_help @240
|
||||||
Z3_update_term @241
|
Z3_simplify_get_param_descrs @241
|
||||||
Z3_substitute @242
|
Z3_update_term @242
|
||||||
Z3_substitute_vars @243
|
Z3_substitute @243
|
||||||
Z3_translate @244
|
Z3_substitute_vars @244
|
||||||
Z3_model_inc_ref @245
|
Z3_translate @245
|
||||||
Z3_model_dec_ref @246
|
Z3_model_inc_ref @246
|
||||||
Z3_model_eval @247
|
Z3_model_dec_ref @247
|
||||||
Z3_model_get_const_interp @248
|
Z3_model_eval @248
|
||||||
Z3_model_get_func_interp @249
|
Z3_model_get_const_interp @249
|
||||||
Z3_model_get_num_consts @250
|
Z3_model_get_func_interp @250
|
||||||
Z3_model_get_const_decl @251
|
Z3_model_get_num_consts @251
|
||||||
Z3_model_get_num_funcs @252
|
Z3_model_get_const_decl @252
|
||||||
Z3_model_get_func_decl @253
|
Z3_model_get_num_funcs @253
|
||||||
Z3_model_get_num_sorts @254
|
Z3_model_get_func_decl @254
|
||||||
Z3_model_get_sort @255
|
Z3_model_get_num_sorts @255
|
||||||
Z3_model_get_sort_universe @256
|
Z3_model_get_sort @256
|
||||||
Z3_is_as_array @257
|
Z3_model_get_sort_universe @257
|
||||||
Z3_get_as_array_func_decl @258
|
Z3_is_as_array @258
|
||||||
Z3_func_interp_inc_ref @259
|
Z3_get_as_array_func_decl @259
|
||||||
Z3_func_interp_dec_ref @260
|
Z3_func_interp_inc_ref @260
|
||||||
Z3_func_interp_get_num_entries @261
|
Z3_func_interp_dec_ref @261
|
||||||
Z3_func_interp_get_entry @262
|
Z3_func_interp_get_num_entries @262
|
||||||
Z3_func_interp_get_else @263
|
Z3_func_interp_get_entry @263
|
||||||
Z3_func_interp_get_arity @264
|
Z3_func_interp_get_else @264
|
||||||
Z3_func_entry_inc_ref @265
|
Z3_func_interp_get_arity @265
|
||||||
Z3_func_entry_dec_ref @266
|
Z3_func_entry_inc_ref @266
|
||||||
Z3_func_entry_get_value @267
|
Z3_func_entry_dec_ref @267
|
||||||
Z3_func_entry_get_num_args @268
|
Z3_func_entry_get_value @268
|
||||||
Z3_func_entry_get_arg @269
|
Z3_func_entry_get_num_args @269
|
||||||
Z3_open_log @270
|
Z3_func_entry_get_arg @270
|
||||||
Z3_append_log @271
|
Z3_open_log @271
|
||||||
Z3_close_log @272
|
Z3_append_log @272
|
||||||
Z3_toggle_warning_messages @273
|
Z3_close_log @273
|
||||||
Z3_set_ast_print_mode @274
|
Z3_toggle_warning_messages @274
|
||||||
Z3_ast_to_string @275
|
Z3_set_ast_print_mode @275
|
||||||
Z3_pattern_to_string @276
|
Z3_ast_to_string @276
|
||||||
Z3_sort_to_string @277
|
Z3_pattern_to_string @277
|
||||||
Z3_func_decl_to_string @278
|
Z3_sort_to_string @278
|
||||||
Z3_model_to_string @279
|
Z3_func_decl_to_string @279
|
||||||
Z3_benchmark_to_smtlib_string @280
|
Z3_model_to_string @280
|
||||||
Z3_parse_smtlib2_string @281
|
Z3_benchmark_to_smtlib_string @281
|
||||||
Z3_parse_smtlib2_file @282
|
Z3_parse_smtlib2_string @282
|
||||||
Z3_parse_smtlib_string @283
|
Z3_parse_smtlib2_file @283
|
||||||
Z3_parse_smtlib_file @284
|
Z3_parse_smtlib_string @284
|
||||||
Z3_get_smtlib_num_formulas @285
|
Z3_parse_smtlib_file @285
|
||||||
Z3_get_smtlib_formula @286
|
Z3_get_smtlib_num_formulas @286
|
||||||
Z3_get_smtlib_num_assumptions @287
|
Z3_get_smtlib_formula @287
|
||||||
Z3_get_smtlib_assumption @288
|
Z3_get_smtlib_num_assumptions @288
|
||||||
Z3_get_smtlib_num_decls @289
|
Z3_get_smtlib_assumption @289
|
||||||
Z3_get_smtlib_decl @290
|
Z3_get_smtlib_num_decls @290
|
||||||
Z3_get_smtlib_num_sorts @291
|
Z3_get_smtlib_decl @291
|
||||||
Z3_get_smtlib_sort @292
|
Z3_get_smtlib_num_sorts @292
|
||||||
Z3_get_smtlib_error @293
|
Z3_get_smtlib_sort @293
|
||||||
Z3_parse_z3_string @294
|
Z3_get_smtlib_error @294
|
||||||
Z3_parse_z3_file @295
|
Z3_parse_z3_string @295
|
||||||
Z3_get_error_code @296
|
Z3_parse_z3_file @296
|
||||||
Z3_set_error_handler @297
|
Z3_get_error_code @297
|
||||||
Z3_set_error @298
|
Z3_set_error_handler @298
|
||||||
Z3_get_error_msg @299
|
Z3_set_error @299
|
||||||
Z3_get_error_msg_ex @300
|
Z3_get_error_msg @300
|
||||||
Z3_get_version @301
|
Z3_get_error_msg_ex @301
|
||||||
Z3_reset_memory @302
|
Z3_get_version @302
|
||||||
Z3_mk_theory @303
|
Z3_reset_memory @303
|
||||||
Z3_theory_get_ext_data @304
|
Z3_mk_theory @304
|
||||||
Z3_theory_mk_sort @305
|
Z3_theory_get_ext_data @305
|
||||||
Z3_theory_mk_value @306
|
Z3_theory_mk_sort @306
|
||||||
Z3_theory_mk_constant @307
|
Z3_theory_mk_value @307
|
||||||
Z3_theory_mk_func_decl @308
|
Z3_theory_mk_constant @308
|
||||||
Z3_theory_get_context @309
|
Z3_theory_mk_func_decl @309
|
||||||
Z3_set_delete_callback @310
|
Z3_theory_get_context @310
|
||||||
Z3_set_reduce_app_callback @311
|
Z3_set_delete_callback @311
|
||||||
Z3_set_reduce_eq_callback @312
|
Z3_set_reduce_app_callback @312
|
||||||
Z3_set_reduce_distinct_callback @313
|
Z3_set_reduce_eq_callback @313
|
||||||
Z3_set_new_app_callback @314
|
Z3_set_reduce_distinct_callback @314
|
||||||
Z3_set_new_elem_callback @315
|
Z3_set_new_app_callback @315
|
||||||
Z3_set_init_search_callback @316
|
Z3_set_new_elem_callback @316
|
||||||
Z3_set_push_callback @317
|
Z3_set_init_search_callback @317
|
||||||
Z3_set_pop_callback @318
|
Z3_set_push_callback @318
|
||||||
Z3_set_restart_callback @319
|
Z3_set_pop_callback @319
|
||||||
Z3_set_reset_callback @320
|
Z3_set_restart_callback @320
|
||||||
Z3_set_final_check_callback @321
|
Z3_set_reset_callback @321
|
||||||
Z3_set_new_eq_callback @322
|
Z3_set_final_check_callback @322
|
||||||
Z3_set_new_diseq_callback @323
|
Z3_set_new_eq_callback @323
|
||||||
Z3_set_new_assignment_callback @324
|
Z3_set_new_diseq_callback @324
|
||||||
Z3_set_new_relevant_callback @325
|
Z3_set_new_assignment_callback @325
|
||||||
Z3_theory_assert_axiom @326
|
Z3_set_new_relevant_callback @326
|
||||||
Z3_theory_assume_eq @327
|
Z3_theory_assert_axiom @327
|
||||||
Z3_theory_enable_axiom_simplification @328
|
Z3_theory_assume_eq @328
|
||||||
Z3_theory_get_eqc_root @329
|
Z3_theory_enable_axiom_simplification @329
|
||||||
Z3_theory_get_eqc_next @330
|
Z3_theory_get_eqc_root @330
|
||||||
Z3_theory_get_num_parents @331
|
Z3_theory_get_eqc_next @331
|
||||||
Z3_theory_get_parent @332
|
Z3_theory_get_num_parents @332
|
||||||
Z3_theory_is_value @333
|
Z3_theory_get_parent @333
|
||||||
Z3_theory_is_decl @334
|
Z3_theory_is_value @334
|
||||||
Z3_theory_get_num_elems @335
|
Z3_theory_is_decl @335
|
||||||
Z3_theory_get_elem @336
|
Z3_theory_get_num_elems @336
|
||||||
Z3_theory_get_num_apps @337
|
Z3_theory_get_elem @337
|
||||||
Z3_theory_get_app @338
|
Z3_theory_get_num_apps @338
|
||||||
Z3_mk_fixedpoint @339
|
Z3_theory_get_app @339
|
||||||
Z3_fixedpoint_inc_ref @340
|
Z3_mk_fixedpoint @340
|
||||||
Z3_fixedpoint_dec_ref @341
|
Z3_fixedpoint_inc_ref @341
|
||||||
Z3_fixedpoint_add_rule @342
|
Z3_fixedpoint_dec_ref @342
|
||||||
Z3_fixedpoint_add_fact @343
|
Z3_fixedpoint_add_rule @343
|
||||||
Z3_fixedpoint_assert @344
|
Z3_fixedpoint_add_fact @344
|
||||||
Z3_fixedpoint_query @345
|
Z3_fixedpoint_assert @345
|
||||||
Z3_fixedpoint_query_relations @346
|
Z3_fixedpoint_query @346
|
||||||
Z3_fixedpoint_get_answer @347
|
Z3_fixedpoint_query_relations @347
|
||||||
Z3_fixedpoint_get_reason_unknown @348
|
Z3_fixedpoint_get_answer @348
|
||||||
Z3_fixedpoint_update_rule @349
|
Z3_fixedpoint_get_reason_unknown @349
|
||||||
Z3_fixedpoint_get_num_levels @350
|
Z3_fixedpoint_update_rule @350
|
||||||
Z3_fixedpoint_get_cover_delta @351
|
Z3_fixedpoint_get_num_levels @351
|
||||||
Z3_fixedpoint_add_cover @352
|
Z3_fixedpoint_get_cover_delta @352
|
||||||
Z3_fixedpoint_get_statistics @353
|
Z3_fixedpoint_add_cover @353
|
||||||
Z3_fixedpoint_register_relation @354
|
Z3_fixedpoint_get_statistics @354
|
||||||
Z3_fixedpoint_set_predicate_representation @355
|
Z3_fixedpoint_register_relation @355
|
||||||
Z3_fixedpoint_simplify_rules @356
|
Z3_fixedpoint_set_predicate_representation @356
|
||||||
Z3_fixedpoint_set_params @357
|
Z3_fixedpoint_simplify_rules @357
|
||||||
Z3_fixedpoint_get_help @358
|
Z3_fixedpoint_set_params @358
|
||||||
Z3_fixedpoint_get_param_descrs @359
|
Z3_fixedpoint_get_help @359
|
||||||
Z3_fixedpoint_to_string @360
|
Z3_fixedpoint_get_param_descrs @360
|
||||||
Z3_fixedpoint_push @361
|
Z3_fixedpoint_to_string @361
|
||||||
Z3_fixedpoint_pop @362
|
Z3_fixedpoint_push @362
|
||||||
Z3_fixedpoint_init @363
|
Z3_fixedpoint_pop @363
|
||||||
Z3_fixedpoint_set_reduce_assign_callback @364
|
Z3_fixedpoint_init @364
|
||||||
Z3_fixedpoint_set_reduce_app_callback @365
|
Z3_fixedpoint_set_reduce_assign_callback @365
|
||||||
Z3_mk_ast_vector @366
|
Z3_fixedpoint_set_reduce_app_callback @366
|
||||||
Z3_ast_vector_inc_ref @367
|
Z3_mk_ast_vector @367
|
||||||
Z3_ast_vector_dec_ref @368
|
Z3_ast_vector_inc_ref @368
|
||||||
Z3_ast_vector_size @369
|
Z3_ast_vector_dec_ref @369
|
||||||
Z3_ast_vector_get @370
|
Z3_ast_vector_size @370
|
||||||
Z3_ast_vector_set @371
|
Z3_ast_vector_get @371
|
||||||
Z3_ast_vector_resize @372
|
Z3_ast_vector_set @372
|
||||||
Z3_ast_vector_push @373
|
Z3_ast_vector_resize @373
|
||||||
Z3_ast_vector_translate @374
|
Z3_ast_vector_push @374
|
||||||
Z3_ast_vector_to_string @375
|
Z3_ast_vector_translate @375
|
||||||
Z3_mk_ast_map @376
|
Z3_ast_vector_to_string @376
|
||||||
Z3_ast_map_inc_ref @377
|
Z3_mk_ast_map @377
|
||||||
Z3_ast_map_dec_ref @378
|
Z3_ast_map_inc_ref @378
|
||||||
Z3_ast_map_contains @379
|
Z3_ast_map_dec_ref @379
|
||||||
Z3_ast_map_find @380
|
Z3_ast_map_contains @380
|
||||||
Z3_ast_map_insert @381
|
Z3_ast_map_find @381
|
||||||
Z3_ast_map_erase @382
|
Z3_ast_map_insert @382
|
||||||
Z3_ast_map_reset @383
|
Z3_ast_map_erase @383
|
||||||
Z3_ast_map_size @384
|
Z3_ast_map_reset @384
|
||||||
Z3_ast_map_keys @385
|
Z3_ast_map_size @385
|
||||||
Z3_ast_map_to_string @386
|
Z3_ast_map_keys @386
|
||||||
Z3_mk_goal @387
|
Z3_ast_map_to_string @387
|
||||||
Z3_goal_inc_ref @388
|
Z3_mk_goal @388
|
||||||
Z3_goal_dec_ref @389
|
Z3_goal_inc_ref @389
|
||||||
Z3_goal_precision @390
|
Z3_goal_dec_ref @390
|
||||||
Z3_goal_assert @391
|
Z3_goal_precision @391
|
||||||
Z3_goal_inconsistent @392
|
Z3_goal_assert @392
|
||||||
Z3_goal_depth @393
|
Z3_goal_inconsistent @393
|
||||||
Z3_goal_reset @394
|
Z3_goal_depth @394
|
||||||
Z3_goal_size @395
|
Z3_goal_reset @395
|
||||||
Z3_goal_formula @396
|
Z3_goal_size @396
|
||||||
Z3_goal_num_exprs @397
|
Z3_goal_formula @397
|
||||||
Z3_goal_is_decided_sat @398
|
Z3_goal_num_exprs @398
|
||||||
Z3_goal_is_decided_unsat @399
|
Z3_goal_is_decided_sat @399
|
||||||
Z3_goal_translate @400
|
Z3_goal_is_decided_unsat @400
|
||||||
Z3_goal_to_string @401
|
Z3_goal_translate @401
|
||||||
Z3_mk_tactic @402
|
Z3_goal_to_string @402
|
||||||
Z3_tactic_inc_ref @403
|
Z3_mk_tactic @403
|
||||||
Z3_tactic_dec_ref @404
|
Z3_tactic_inc_ref @404
|
||||||
Z3_mk_probe @405
|
Z3_tactic_dec_ref @405
|
||||||
Z3_probe_inc_ref @406
|
Z3_mk_probe @406
|
||||||
Z3_probe_dec_ref @407
|
Z3_probe_inc_ref @407
|
||||||
Z3_tactic_and_then @408
|
Z3_probe_dec_ref @408
|
||||||
Z3_tactic_or_else @409
|
Z3_tactic_and_then @409
|
||||||
Z3_tactic_par_or @410
|
Z3_tactic_or_else @410
|
||||||
Z3_tactic_par_and_then @411
|
Z3_tactic_par_or @411
|
||||||
Z3_tactic_try_for @412
|
Z3_tactic_par_and_then @412
|
||||||
Z3_tactic_when @413
|
Z3_tactic_try_for @413
|
||||||
Z3_tactic_cond @414
|
Z3_tactic_when @414
|
||||||
Z3_tactic_repeat @415
|
Z3_tactic_cond @415
|
||||||
Z3_tactic_skip @416
|
Z3_tactic_repeat @416
|
||||||
Z3_tactic_fail @417
|
Z3_tactic_skip @417
|
||||||
Z3_tactic_fail_if @418
|
Z3_tactic_fail @418
|
||||||
Z3_tactic_fail_if_not_decided @419
|
Z3_tactic_fail_if @419
|
||||||
Z3_tactic_using_params @420
|
Z3_tactic_fail_if_not_decided @420
|
||||||
Z3_probe_const @421
|
Z3_tactic_using_params @421
|
||||||
Z3_probe_lt @422
|
Z3_probe_const @422
|
||||||
Z3_probe_gt @423
|
Z3_probe_lt @423
|
||||||
Z3_probe_le @424
|
Z3_probe_gt @424
|
||||||
Z3_probe_ge @425
|
Z3_probe_le @425
|
||||||
Z3_probe_eq @426
|
Z3_probe_ge @426
|
||||||
Z3_probe_and @427
|
Z3_probe_eq @427
|
||||||
Z3_probe_or @428
|
Z3_probe_and @428
|
||||||
Z3_probe_not @429
|
Z3_probe_or @429
|
||||||
Z3_get_num_tactics @430
|
Z3_probe_not @430
|
||||||
Z3_get_tactic_name @431
|
Z3_get_num_tactics @431
|
||||||
Z3_get_num_probes @432
|
Z3_get_tactic_name @432
|
||||||
Z3_get_probe_name @433
|
Z3_get_num_probes @433
|
||||||
Z3_tactic_get_help @434
|
Z3_get_probe_name @434
|
||||||
Z3_tactic_get_param_descrs @435
|
Z3_tactic_get_help @435
|
||||||
Z3_tactic_get_descr @436
|
Z3_tactic_get_param_descrs @436
|
||||||
Z3_probe_get_descr @437
|
Z3_tactic_get_descr @437
|
||||||
Z3_probe_apply @438
|
Z3_probe_get_descr @438
|
||||||
Z3_tactic_apply @439
|
Z3_probe_apply @439
|
||||||
Z3_tactic_apply_ex @440
|
Z3_tactic_apply @440
|
||||||
Z3_apply_result_inc_ref @441
|
Z3_tactic_apply_ex @441
|
||||||
Z3_apply_result_dec_ref @442
|
Z3_apply_result_inc_ref @442
|
||||||
Z3_apply_result_to_string @443
|
Z3_apply_result_dec_ref @443
|
||||||
Z3_apply_result_get_num_subgoals @444
|
Z3_apply_result_to_string @444
|
||||||
Z3_apply_result_get_subgoal @445
|
Z3_apply_result_get_num_subgoals @445
|
||||||
Z3_apply_result_convert_model @446
|
Z3_apply_result_get_subgoal @446
|
||||||
Z3_mk_solver @447
|
Z3_apply_result_convert_model @447
|
||||||
Z3_mk_simple_solver @448
|
Z3_mk_solver @448
|
||||||
Z3_mk_solver_for_logic @449
|
Z3_mk_simple_solver @449
|
||||||
Z3_mk_solver_from_tactic @450
|
Z3_mk_solver_for_logic @450
|
||||||
Z3_solver_get_help @451
|
Z3_mk_solver_from_tactic @451
|
||||||
Z3_solver_get_param_descrs @452
|
Z3_solver_get_help @452
|
||||||
Z3_solver_set_params @453
|
Z3_solver_get_param_descrs @453
|
||||||
Z3_solver_inc_ref @454
|
Z3_solver_set_params @454
|
||||||
Z3_solver_dec_ref @455
|
Z3_solver_inc_ref @455
|
||||||
Z3_solver_push @456
|
Z3_solver_dec_ref @456
|
||||||
Z3_solver_pop @457
|
Z3_solver_push @457
|
||||||
Z3_solver_reset @458
|
Z3_solver_pop @458
|
||||||
Z3_solver_get_num_scopes @459
|
Z3_solver_reset @459
|
||||||
Z3_solver_assert @460
|
Z3_solver_get_num_scopes @460
|
||||||
Z3_solver_get_assertions @461
|
Z3_solver_assert @461
|
||||||
Z3_solver_check @462
|
Z3_solver_get_assertions @462
|
||||||
Z3_solver_check_assumptions @463
|
Z3_solver_check @463
|
||||||
Z3_solver_get_model @464
|
Z3_solver_check_assumptions @464
|
||||||
Z3_solver_get_proof @465
|
Z3_solver_get_model @465
|
||||||
Z3_solver_get_unsat_core @466
|
Z3_solver_get_proof @466
|
||||||
Z3_solver_get_reason_unknown @467
|
Z3_solver_get_unsat_core @467
|
||||||
Z3_solver_get_statistics @468
|
Z3_solver_get_reason_unknown @468
|
||||||
Z3_solver_to_string @469
|
Z3_solver_get_statistics @469
|
||||||
Z3_stats_to_string @470
|
Z3_solver_to_string @470
|
||||||
Z3_stats_inc_ref @471
|
Z3_stats_to_string @471
|
||||||
Z3_stats_dec_ref @472
|
Z3_stats_inc_ref @472
|
||||||
Z3_stats_size @473
|
Z3_stats_dec_ref @473
|
||||||
Z3_stats_get_key @474
|
Z3_stats_size @474
|
||||||
Z3_stats_is_uint @475
|
Z3_stats_get_key @475
|
||||||
Z3_stats_is_double @476
|
Z3_stats_is_uint @476
|
||||||
Z3_stats_get_uint_value @477
|
Z3_stats_is_double @477
|
||||||
Z3_stats_get_double_value @478
|
Z3_stats_get_uint_value @478
|
||||||
Z3_mk_injective_function @479
|
Z3_stats_get_double_value @479
|
||||||
Z3_set_logic @480
|
Z3_mk_injective_function @480
|
||||||
Z3_push @481
|
Z3_set_logic @481
|
||||||
Z3_pop @482
|
Z3_push @482
|
||||||
Z3_get_num_scopes @483
|
Z3_pop @483
|
||||||
Z3_persist_ast @484
|
Z3_get_num_scopes @484
|
||||||
Z3_assert_cnstr @485
|
Z3_persist_ast @485
|
||||||
Z3_check_and_get_model @486
|
Z3_assert_cnstr @486
|
||||||
Z3_check @487
|
Z3_check_and_get_model @487
|
||||||
Z3_check_assumptions @488
|
Z3_check @488
|
||||||
Z3_get_implied_equalities @489
|
Z3_check_assumptions @489
|
||||||
Z3_del_model @490
|
Z3_get_implied_equalities @490
|
||||||
Z3_soft_check_cancel @491
|
Z3_del_model @491
|
||||||
Z3_get_search_failure @492
|
Z3_soft_check_cancel @492
|
||||||
Z3_mk_label @493
|
Z3_get_search_failure @493
|
||||||
Z3_get_relevant_labels @494
|
Z3_mk_label @494
|
||||||
Z3_get_relevant_literals @495
|
Z3_get_relevant_labels @495
|
||||||
Z3_get_guessed_literals @496
|
Z3_get_relevant_literals @496
|
||||||
Z3_del_literals @497
|
Z3_get_guessed_literals @497
|
||||||
Z3_get_num_literals @498
|
Z3_del_literals @498
|
||||||
Z3_get_label_symbol @499
|
Z3_get_num_literals @499
|
||||||
Z3_get_literal @500
|
Z3_get_label_symbol @500
|
||||||
Z3_disable_literal @501
|
Z3_get_literal @501
|
||||||
Z3_block_literals @502
|
Z3_disable_literal @502
|
||||||
Z3_get_model_num_constants @503
|
Z3_block_literals @503
|
||||||
Z3_get_model_constant @504
|
Z3_get_model_num_constants @504
|
||||||
Z3_get_model_num_funcs @505
|
Z3_get_model_constant @505
|
||||||
Z3_get_model_func_decl @506
|
Z3_get_model_num_funcs @506
|
||||||
Z3_eval_func_decl @507
|
Z3_get_model_func_decl @507
|
||||||
Z3_is_array_value @508
|
Z3_eval_func_decl @508
|
||||||
Z3_get_array_value @509
|
Z3_is_array_value @509
|
||||||
Z3_get_model_func_else @510
|
Z3_get_array_value @510
|
||||||
Z3_get_model_func_num_entries @511
|
Z3_get_model_func_else @511
|
||||||
Z3_get_model_func_entry_num_args @512
|
Z3_get_model_func_num_entries @512
|
||||||
Z3_get_model_func_entry_arg @513
|
Z3_get_model_func_entry_num_args @513
|
||||||
Z3_get_model_func_entry_value @514
|
Z3_get_model_func_entry_arg @514
|
||||||
Z3_eval @515
|
Z3_get_model_func_entry_value @515
|
||||||
Z3_eval_decl @516
|
Z3_eval @516
|
||||||
Z3_context_to_string @517
|
Z3_eval_decl @517
|
||||||
Z3_statistics_to_string @518
|
Z3_context_to_string @518
|
||||||
Z3_get_context_assignment @519
|
Z3_statistics_to_string @519
|
||||||
|
Z3_get_context_assignment @520
|
||||||
|
|
|
||||||
989
dll/z3_dbg.def
989
dll/z3_dbg.def
|
|
@ -25,497 +25,498 @@ EXPORTS
|
||||||
Z3_param_descrs_get_kind @23
|
Z3_param_descrs_get_kind @23
|
||||||
Z3_param_descrs_size @24
|
Z3_param_descrs_size @24
|
||||||
Z3_param_descrs_get_name @25
|
Z3_param_descrs_get_name @25
|
||||||
Z3_mk_int_symbol @26
|
Z3_param_descrs_to_string @26
|
||||||
Z3_mk_string_symbol @27
|
Z3_mk_int_symbol @27
|
||||||
Z3_mk_uninterpreted_sort @28
|
Z3_mk_string_symbol @28
|
||||||
Z3_mk_bool_sort @29
|
Z3_mk_uninterpreted_sort @29
|
||||||
Z3_mk_int_sort @30
|
Z3_mk_bool_sort @30
|
||||||
Z3_mk_real_sort @31
|
Z3_mk_int_sort @31
|
||||||
Z3_mk_bv_sort @32
|
Z3_mk_real_sort @32
|
||||||
Z3_mk_finite_domain_sort @33
|
Z3_mk_bv_sort @33
|
||||||
Z3_mk_array_sort @34
|
Z3_mk_finite_domain_sort @34
|
||||||
Z3_mk_tuple_sort @35
|
Z3_mk_array_sort @35
|
||||||
Z3_mk_enumeration_sort @36
|
Z3_mk_tuple_sort @36
|
||||||
Z3_mk_list_sort @37
|
Z3_mk_enumeration_sort @37
|
||||||
Z3_mk_constructor @38
|
Z3_mk_list_sort @38
|
||||||
Z3_del_constructor @39
|
Z3_mk_constructor @39
|
||||||
Z3_mk_datatype @40
|
Z3_del_constructor @40
|
||||||
Z3_mk_constructor_list @41
|
Z3_mk_datatype @41
|
||||||
Z3_del_constructor_list @42
|
Z3_mk_constructor_list @42
|
||||||
Z3_mk_datatypes @43
|
Z3_del_constructor_list @43
|
||||||
Z3_query_constructor @44
|
Z3_mk_datatypes @44
|
||||||
Z3_mk_func_decl @45
|
Z3_query_constructor @45
|
||||||
Z3_mk_app @46
|
Z3_mk_func_decl @46
|
||||||
Z3_mk_const @47
|
Z3_mk_app @47
|
||||||
Z3_mk_fresh_func_decl @48
|
Z3_mk_const @48
|
||||||
Z3_mk_fresh_const @49
|
Z3_mk_fresh_func_decl @49
|
||||||
Z3_mk_true @50
|
Z3_mk_fresh_const @50
|
||||||
Z3_mk_false @51
|
Z3_mk_true @51
|
||||||
Z3_mk_eq @52
|
Z3_mk_false @52
|
||||||
Z3_mk_distinct @53
|
Z3_mk_eq @53
|
||||||
Z3_mk_not @54
|
Z3_mk_distinct @54
|
||||||
Z3_mk_ite @55
|
Z3_mk_not @55
|
||||||
Z3_mk_iff @56
|
Z3_mk_ite @56
|
||||||
Z3_mk_implies @57
|
Z3_mk_iff @57
|
||||||
Z3_mk_xor @58
|
Z3_mk_implies @58
|
||||||
Z3_mk_and @59
|
Z3_mk_xor @59
|
||||||
Z3_mk_or @60
|
Z3_mk_and @60
|
||||||
Z3_mk_add @61
|
Z3_mk_or @61
|
||||||
Z3_mk_mul @62
|
Z3_mk_add @62
|
||||||
Z3_mk_sub @63
|
Z3_mk_mul @63
|
||||||
Z3_mk_unary_minus @64
|
Z3_mk_sub @64
|
||||||
Z3_mk_div @65
|
Z3_mk_unary_minus @65
|
||||||
Z3_mk_mod @66
|
Z3_mk_div @66
|
||||||
Z3_mk_rem @67
|
Z3_mk_mod @67
|
||||||
Z3_mk_power @68
|
Z3_mk_rem @68
|
||||||
Z3_mk_lt @69
|
Z3_mk_power @69
|
||||||
Z3_mk_le @70
|
Z3_mk_lt @70
|
||||||
Z3_mk_gt @71
|
Z3_mk_le @71
|
||||||
Z3_mk_ge @72
|
Z3_mk_gt @72
|
||||||
Z3_mk_int2real @73
|
Z3_mk_ge @73
|
||||||
Z3_mk_real2int @74
|
Z3_mk_int2real @74
|
||||||
Z3_mk_is_int @75
|
Z3_mk_real2int @75
|
||||||
Z3_mk_bvnot @76
|
Z3_mk_is_int @76
|
||||||
Z3_mk_bvredand @77
|
Z3_mk_bvnot @77
|
||||||
Z3_mk_bvredor @78
|
Z3_mk_bvredand @78
|
||||||
Z3_mk_bvand @79
|
Z3_mk_bvredor @79
|
||||||
Z3_mk_bvor @80
|
Z3_mk_bvand @80
|
||||||
Z3_mk_bvxor @81
|
Z3_mk_bvor @81
|
||||||
Z3_mk_bvnand @82
|
Z3_mk_bvxor @82
|
||||||
Z3_mk_bvnor @83
|
Z3_mk_bvnand @83
|
||||||
Z3_mk_bvxnor @84
|
Z3_mk_bvnor @84
|
||||||
Z3_mk_bvneg @85
|
Z3_mk_bvxnor @85
|
||||||
Z3_mk_bvadd @86
|
Z3_mk_bvneg @86
|
||||||
Z3_mk_bvsub @87
|
Z3_mk_bvadd @87
|
||||||
Z3_mk_bvmul @88
|
Z3_mk_bvsub @88
|
||||||
Z3_mk_bvudiv @89
|
Z3_mk_bvmul @89
|
||||||
Z3_mk_bvsdiv @90
|
Z3_mk_bvudiv @90
|
||||||
Z3_mk_bvurem @91
|
Z3_mk_bvsdiv @91
|
||||||
Z3_mk_bvsrem @92
|
Z3_mk_bvurem @92
|
||||||
Z3_mk_bvsmod @93
|
Z3_mk_bvsrem @93
|
||||||
Z3_mk_bvult @94
|
Z3_mk_bvsmod @94
|
||||||
Z3_mk_bvslt @95
|
Z3_mk_bvult @95
|
||||||
Z3_mk_bvule @96
|
Z3_mk_bvslt @96
|
||||||
Z3_mk_bvsle @97
|
Z3_mk_bvule @97
|
||||||
Z3_mk_bvuge @98
|
Z3_mk_bvsle @98
|
||||||
Z3_mk_bvsge @99
|
Z3_mk_bvuge @99
|
||||||
Z3_mk_bvugt @100
|
Z3_mk_bvsge @100
|
||||||
Z3_mk_bvsgt @101
|
Z3_mk_bvugt @101
|
||||||
Z3_mk_concat @102
|
Z3_mk_bvsgt @102
|
||||||
Z3_mk_extract @103
|
Z3_mk_concat @103
|
||||||
Z3_mk_sign_ext @104
|
Z3_mk_extract @104
|
||||||
Z3_mk_zero_ext @105
|
Z3_mk_sign_ext @105
|
||||||
Z3_mk_repeat @106
|
Z3_mk_zero_ext @106
|
||||||
Z3_mk_bvshl @107
|
Z3_mk_repeat @107
|
||||||
Z3_mk_bvlshr @108
|
Z3_mk_bvshl @108
|
||||||
Z3_mk_bvashr @109
|
Z3_mk_bvlshr @109
|
||||||
Z3_mk_rotate_left @110
|
Z3_mk_bvashr @110
|
||||||
Z3_mk_rotate_right @111
|
Z3_mk_rotate_left @111
|
||||||
Z3_mk_ext_rotate_left @112
|
Z3_mk_rotate_right @112
|
||||||
Z3_mk_ext_rotate_right @113
|
Z3_mk_ext_rotate_left @113
|
||||||
Z3_mk_int2bv @114
|
Z3_mk_ext_rotate_right @114
|
||||||
Z3_mk_bv2int @115
|
Z3_mk_int2bv @115
|
||||||
Z3_mk_bvadd_no_overflow @116
|
Z3_mk_bv2int @116
|
||||||
Z3_mk_bvadd_no_underflow @117
|
Z3_mk_bvadd_no_overflow @117
|
||||||
Z3_mk_bvsub_no_overflow @118
|
Z3_mk_bvadd_no_underflow @118
|
||||||
Z3_mk_bvsub_no_underflow @119
|
Z3_mk_bvsub_no_overflow @119
|
||||||
Z3_mk_bvsdiv_no_overflow @120
|
Z3_mk_bvsub_no_underflow @120
|
||||||
Z3_mk_bvneg_no_overflow @121
|
Z3_mk_bvsdiv_no_overflow @121
|
||||||
Z3_mk_bvmul_no_overflow @122
|
Z3_mk_bvneg_no_overflow @122
|
||||||
Z3_mk_bvmul_no_underflow @123
|
Z3_mk_bvmul_no_overflow @123
|
||||||
Z3_mk_select @124
|
Z3_mk_bvmul_no_underflow @124
|
||||||
Z3_mk_store @125
|
Z3_mk_select @125
|
||||||
Z3_mk_const_array @126
|
Z3_mk_store @126
|
||||||
Z3_mk_map @127
|
Z3_mk_const_array @127
|
||||||
Z3_mk_array_default @128
|
Z3_mk_map @128
|
||||||
Z3_mk_set_sort @129
|
Z3_mk_array_default @129
|
||||||
Z3_mk_empty_set @130
|
Z3_mk_set_sort @130
|
||||||
Z3_mk_full_set @131
|
Z3_mk_empty_set @131
|
||||||
Z3_mk_set_add @132
|
Z3_mk_full_set @132
|
||||||
Z3_mk_set_del @133
|
Z3_mk_set_add @133
|
||||||
Z3_mk_set_union @134
|
Z3_mk_set_del @134
|
||||||
Z3_mk_set_intersect @135
|
Z3_mk_set_union @135
|
||||||
Z3_mk_set_difference @136
|
Z3_mk_set_intersect @136
|
||||||
Z3_mk_set_complement @137
|
Z3_mk_set_difference @137
|
||||||
Z3_mk_set_member @138
|
Z3_mk_set_complement @138
|
||||||
Z3_mk_set_subset @139
|
Z3_mk_set_member @139
|
||||||
Z3_mk_numeral @140
|
Z3_mk_set_subset @140
|
||||||
Z3_mk_real @141
|
Z3_mk_numeral @141
|
||||||
Z3_mk_int @142
|
Z3_mk_real @142
|
||||||
Z3_mk_unsigned_int @143
|
Z3_mk_int @143
|
||||||
Z3_mk_int64 @144
|
Z3_mk_unsigned_int @144
|
||||||
Z3_mk_unsigned_int64 @145
|
Z3_mk_int64 @145
|
||||||
Z3_mk_pattern @146
|
Z3_mk_unsigned_int64 @146
|
||||||
Z3_mk_bound @147
|
Z3_mk_pattern @147
|
||||||
Z3_mk_forall @148
|
Z3_mk_bound @148
|
||||||
Z3_mk_exists @149
|
Z3_mk_forall @149
|
||||||
Z3_mk_quantifier @150
|
Z3_mk_exists @150
|
||||||
Z3_mk_quantifier_ex @151
|
Z3_mk_quantifier @151
|
||||||
Z3_mk_forall_const @152
|
Z3_mk_quantifier_ex @152
|
||||||
Z3_mk_exists_const @153
|
Z3_mk_forall_const @153
|
||||||
Z3_mk_quantifier_const @154
|
Z3_mk_exists_const @154
|
||||||
Z3_mk_quantifier_const_ex @155
|
Z3_mk_quantifier_const @155
|
||||||
Z3_get_symbol_kind @156
|
Z3_mk_quantifier_const_ex @156
|
||||||
Z3_get_symbol_int @157
|
Z3_get_symbol_kind @157
|
||||||
Z3_get_symbol_string @158
|
Z3_get_symbol_int @158
|
||||||
Z3_get_sort_name @159
|
Z3_get_symbol_string @159
|
||||||
Z3_get_sort_id @160
|
Z3_get_sort_name @160
|
||||||
Z3_sort_to_ast @161
|
Z3_get_sort_id @161
|
||||||
Z3_is_eq_sort @162
|
Z3_sort_to_ast @162
|
||||||
Z3_get_sort_kind @163
|
Z3_is_eq_sort @163
|
||||||
Z3_get_bv_sort_size @164
|
Z3_get_sort_kind @164
|
||||||
Z3_get_finite_domain_sort_size @165
|
Z3_get_bv_sort_size @165
|
||||||
Z3_get_array_sort_domain @166
|
Z3_get_finite_domain_sort_size @166
|
||||||
Z3_get_array_sort_range @167
|
Z3_get_array_sort_domain @167
|
||||||
Z3_get_tuple_sort_mk_decl @168
|
Z3_get_array_sort_range @168
|
||||||
Z3_get_tuple_sort_num_fields @169
|
Z3_get_tuple_sort_mk_decl @169
|
||||||
Z3_get_tuple_sort_field_decl @170
|
Z3_get_tuple_sort_num_fields @170
|
||||||
Z3_get_datatype_sort_num_constructors @171
|
Z3_get_tuple_sort_field_decl @171
|
||||||
Z3_get_datatype_sort_constructor @172
|
Z3_get_datatype_sort_num_constructors @172
|
||||||
Z3_get_datatype_sort_recognizer @173
|
Z3_get_datatype_sort_constructor @173
|
||||||
Z3_get_datatype_sort_constructor_accessor @174
|
Z3_get_datatype_sort_recognizer @174
|
||||||
Z3_get_relation_arity @175
|
Z3_get_datatype_sort_constructor_accessor @175
|
||||||
Z3_get_relation_column @176
|
Z3_get_relation_arity @176
|
||||||
Z3_func_decl_to_ast @177
|
Z3_get_relation_column @177
|
||||||
Z3_is_eq_func_decl @178
|
Z3_func_decl_to_ast @178
|
||||||
Z3_get_func_decl_id @179
|
Z3_is_eq_func_decl @179
|
||||||
Z3_get_decl_name @180
|
Z3_get_func_decl_id @180
|
||||||
Z3_get_decl_kind @181
|
Z3_get_decl_name @181
|
||||||
Z3_get_domain_size @182
|
Z3_get_decl_kind @182
|
||||||
Z3_get_arity @183
|
Z3_get_domain_size @183
|
||||||
Z3_get_domain @184
|
Z3_get_arity @184
|
||||||
Z3_get_range @185
|
Z3_get_domain @185
|
||||||
Z3_get_decl_num_parameters @186
|
Z3_get_range @186
|
||||||
Z3_get_decl_parameter_kind @187
|
Z3_get_decl_num_parameters @187
|
||||||
Z3_get_decl_int_parameter @188
|
Z3_get_decl_parameter_kind @188
|
||||||
Z3_get_decl_double_parameter @189
|
Z3_get_decl_int_parameter @189
|
||||||
Z3_get_decl_symbol_parameter @190
|
Z3_get_decl_double_parameter @190
|
||||||
Z3_get_decl_sort_parameter @191
|
Z3_get_decl_symbol_parameter @191
|
||||||
Z3_get_decl_ast_parameter @192
|
Z3_get_decl_sort_parameter @192
|
||||||
Z3_get_decl_func_decl_parameter @193
|
Z3_get_decl_ast_parameter @193
|
||||||
Z3_get_decl_rational_parameter @194
|
Z3_get_decl_func_decl_parameter @194
|
||||||
Z3_app_to_ast @195
|
Z3_get_decl_rational_parameter @195
|
||||||
Z3_get_app_decl @196
|
Z3_app_to_ast @196
|
||||||
Z3_get_app_num_args @197
|
Z3_get_app_decl @197
|
||||||
Z3_get_app_arg @198
|
Z3_get_app_num_args @198
|
||||||
Z3_is_eq_ast @199
|
Z3_get_app_arg @199
|
||||||
Z3_get_ast_id @200
|
Z3_is_eq_ast @200
|
||||||
Z3_get_ast_hash @201
|
Z3_get_ast_id @201
|
||||||
Z3_get_sort @202
|
Z3_get_ast_hash @202
|
||||||
Z3_is_well_sorted @203
|
Z3_get_sort @203
|
||||||
Z3_get_bool_value @204
|
Z3_is_well_sorted @204
|
||||||
Z3_get_ast_kind @205
|
Z3_get_bool_value @205
|
||||||
Z3_is_app @206
|
Z3_get_ast_kind @206
|
||||||
Z3_is_numeral_ast @207
|
Z3_is_app @207
|
||||||
Z3_is_algebraic_number @208
|
Z3_is_numeral_ast @208
|
||||||
Z3_to_app @209
|
Z3_is_algebraic_number @209
|
||||||
Z3_to_func_decl @210
|
Z3_to_app @210
|
||||||
Z3_get_numeral_string @211
|
Z3_to_func_decl @211
|
||||||
Z3_get_numeral_decimal_string @212
|
Z3_get_numeral_string @212
|
||||||
Z3_get_numerator @213
|
Z3_get_numeral_decimal_string @213
|
||||||
Z3_get_denominator @214
|
Z3_get_numerator @214
|
||||||
Z3_get_numeral_small @215
|
Z3_get_denominator @215
|
||||||
Z3_get_numeral_int @216
|
Z3_get_numeral_small @216
|
||||||
Z3_get_numeral_uint @217
|
Z3_get_numeral_int @217
|
||||||
Z3_get_numeral_uint64 @218
|
Z3_get_numeral_uint @218
|
||||||
Z3_get_numeral_int64 @219
|
Z3_get_numeral_uint64 @219
|
||||||
Z3_get_numeral_rational_int64 @220
|
Z3_get_numeral_int64 @220
|
||||||
Z3_get_algebraic_number_lower @221
|
Z3_get_numeral_rational_int64 @221
|
||||||
Z3_get_algebraic_number_upper @222
|
Z3_get_algebraic_number_lower @222
|
||||||
Z3_pattern_to_ast @223
|
Z3_get_algebraic_number_upper @223
|
||||||
Z3_get_pattern_num_terms @224
|
Z3_pattern_to_ast @224
|
||||||
Z3_get_pattern @225
|
Z3_get_pattern_num_terms @225
|
||||||
Z3_get_index_value @226
|
Z3_get_pattern @226
|
||||||
Z3_is_quantifier_forall @227
|
Z3_get_index_value @227
|
||||||
Z3_get_quantifier_weight @228
|
Z3_is_quantifier_forall @228
|
||||||
Z3_get_quantifier_num_patterns @229
|
Z3_get_quantifier_weight @229
|
||||||
Z3_get_quantifier_pattern_ast @230
|
Z3_get_quantifier_num_patterns @230
|
||||||
Z3_get_quantifier_num_no_patterns @231
|
Z3_get_quantifier_pattern_ast @231
|
||||||
Z3_get_quantifier_no_pattern_ast @232
|
Z3_get_quantifier_num_no_patterns @232
|
||||||
Z3_get_quantifier_num_bound @233
|
Z3_get_quantifier_no_pattern_ast @233
|
||||||
Z3_get_quantifier_bound_name @234
|
Z3_get_quantifier_num_bound @234
|
||||||
Z3_get_quantifier_bound_sort @235
|
Z3_get_quantifier_bound_name @235
|
||||||
Z3_get_quantifier_body @236
|
Z3_get_quantifier_bound_sort @236
|
||||||
Z3_simplify @237
|
Z3_get_quantifier_body @237
|
||||||
Z3_simplify_ex @238
|
Z3_simplify @238
|
||||||
Z3_simplify_get_help @239
|
Z3_simplify_ex @239
|
||||||
Z3_simplify_get_param_descrs @240
|
Z3_simplify_get_help @240
|
||||||
Z3_update_term @241
|
Z3_simplify_get_param_descrs @241
|
||||||
Z3_substitute @242
|
Z3_update_term @242
|
||||||
Z3_substitute_vars @243
|
Z3_substitute @243
|
||||||
Z3_translate @244
|
Z3_substitute_vars @244
|
||||||
Z3_model_inc_ref @245
|
Z3_translate @245
|
||||||
Z3_model_dec_ref @246
|
Z3_model_inc_ref @246
|
||||||
Z3_model_eval @247
|
Z3_model_dec_ref @247
|
||||||
Z3_model_get_const_interp @248
|
Z3_model_eval @248
|
||||||
Z3_model_get_func_interp @249
|
Z3_model_get_const_interp @249
|
||||||
Z3_model_get_num_consts @250
|
Z3_model_get_func_interp @250
|
||||||
Z3_model_get_const_decl @251
|
Z3_model_get_num_consts @251
|
||||||
Z3_model_get_num_funcs @252
|
Z3_model_get_const_decl @252
|
||||||
Z3_model_get_func_decl @253
|
Z3_model_get_num_funcs @253
|
||||||
Z3_model_get_num_sorts @254
|
Z3_model_get_func_decl @254
|
||||||
Z3_model_get_sort @255
|
Z3_model_get_num_sorts @255
|
||||||
Z3_model_get_sort_universe @256
|
Z3_model_get_sort @256
|
||||||
Z3_is_as_array @257
|
Z3_model_get_sort_universe @257
|
||||||
Z3_get_as_array_func_decl @258
|
Z3_is_as_array @258
|
||||||
Z3_func_interp_inc_ref @259
|
Z3_get_as_array_func_decl @259
|
||||||
Z3_func_interp_dec_ref @260
|
Z3_func_interp_inc_ref @260
|
||||||
Z3_func_interp_get_num_entries @261
|
Z3_func_interp_dec_ref @261
|
||||||
Z3_func_interp_get_entry @262
|
Z3_func_interp_get_num_entries @262
|
||||||
Z3_func_interp_get_else @263
|
Z3_func_interp_get_entry @263
|
||||||
Z3_func_interp_get_arity @264
|
Z3_func_interp_get_else @264
|
||||||
Z3_func_entry_inc_ref @265
|
Z3_func_interp_get_arity @265
|
||||||
Z3_func_entry_dec_ref @266
|
Z3_func_entry_inc_ref @266
|
||||||
Z3_func_entry_get_value @267
|
Z3_func_entry_dec_ref @267
|
||||||
Z3_func_entry_get_num_args @268
|
Z3_func_entry_get_value @268
|
||||||
Z3_func_entry_get_arg @269
|
Z3_func_entry_get_num_args @269
|
||||||
Z3_open_log @270
|
Z3_func_entry_get_arg @270
|
||||||
Z3_append_log @271
|
Z3_open_log @271
|
||||||
Z3_close_log @272
|
Z3_append_log @272
|
||||||
Z3_toggle_warning_messages @273
|
Z3_close_log @273
|
||||||
Z3_set_ast_print_mode @274
|
Z3_toggle_warning_messages @274
|
||||||
Z3_ast_to_string @275
|
Z3_set_ast_print_mode @275
|
||||||
Z3_pattern_to_string @276
|
Z3_ast_to_string @276
|
||||||
Z3_sort_to_string @277
|
Z3_pattern_to_string @277
|
||||||
Z3_func_decl_to_string @278
|
Z3_sort_to_string @278
|
||||||
Z3_model_to_string @279
|
Z3_func_decl_to_string @279
|
||||||
Z3_benchmark_to_smtlib_string @280
|
Z3_model_to_string @280
|
||||||
Z3_parse_smtlib2_string @281
|
Z3_benchmark_to_smtlib_string @281
|
||||||
Z3_parse_smtlib2_file @282
|
Z3_parse_smtlib2_string @282
|
||||||
Z3_parse_smtlib_string @283
|
Z3_parse_smtlib2_file @283
|
||||||
Z3_parse_smtlib_file @284
|
Z3_parse_smtlib_string @284
|
||||||
Z3_get_smtlib_num_formulas @285
|
Z3_parse_smtlib_file @285
|
||||||
Z3_get_smtlib_formula @286
|
Z3_get_smtlib_num_formulas @286
|
||||||
Z3_get_smtlib_num_assumptions @287
|
Z3_get_smtlib_formula @287
|
||||||
Z3_get_smtlib_assumption @288
|
Z3_get_smtlib_num_assumptions @288
|
||||||
Z3_get_smtlib_num_decls @289
|
Z3_get_smtlib_assumption @289
|
||||||
Z3_get_smtlib_decl @290
|
Z3_get_smtlib_num_decls @290
|
||||||
Z3_get_smtlib_num_sorts @291
|
Z3_get_smtlib_decl @291
|
||||||
Z3_get_smtlib_sort @292
|
Z3_get_smtlib_num_sorts @292
|
||||||
Z3_get_smtlib_error @293
|
Z3_get_smtlib_sort @293
|
||||||
Z3_parse_z3_string @294
|
Z3_get_smtlib_error @294
|
||||||
Z3_parse_z3_file @295
|
Z3_parse_z3_string @295
|
||||||
Z3_get_error_code @296
|
Z3_parse_z3_file @296
|
||||||
Z3_set_error_handler @297
|
Z3_get_error_code @297
|
||||||
Z3_set_error @298
|
Z3_set_error_handler @298
|
||||||
Z3_get_error_msg @299
|
Z3_set_error @299
|
||||||
Z3_get_error_msg_ex @300
|
Z3_get_error_msg @300
|
||||||
Z3_get_version @301
|
Z3_get_error_msg_ex @301
|
||||||
Z3_reset_memory @302
|
Z3_get_version @302
|
||||||
Z3_mk_theory @303
|
Z3_reset_memory @303
|
||||||
Z3_theory_get_ext_data @304
|
Z3_mk_theory @304
|
||||||
Z3_theory_mk_sort @305
|
Z3_theory_get_ext_data @305
|
||||||
Z3_theory_mk_value @306
|
Z3_theory_mk_sort @306
|
||||||
Z3_theory_mk_constant @307
|
Z3_theory_mk_value @307
|
||||||
Z3_theory_mk_func_decl @308
|
Z3_theory_mk_constant @308
|
||||||
Z3_theory_get_context @309
|
Z3_theory_mk_func_decl @309
|
||||||
Z3_set_delete_callback @310
|
Z3_theory_get_context @310
|
||||||
Z3_set_reduce_app_callback @311
|
Z3_set_delete_callback @311
|
||||||
Z3_set_reduce_eq_callback @312
|
Z3_set_reduce_app_callback @312
|
||||||
Z3_set_reduce_distinct_callback @313
|
Z3_set_reduce_eq_callback @313
|
||||||
Z3_set_new_app_callback @314
|
Z3_set_reduce_distinct_callback @314
|
||||||
Z3_set_new_elem_callback @315
|
Z3_set_new_app_callback @315
|
||||||
Z3_set_init_search_callback @316
|
Z3_set_new_elem_callback @316
|
||||||
Z3_set_push_callback @317
|
Z3_set_init_search_callback @317
|
||||||
Z3_set_pop_callback @318
|
Z3_set_push_callback @318
|
||||||
Z3_set_restart_callback @319
|
Z3_set_pop_callback @319
|
||||||
Z3_set_reset_callback @320
|
Z3_set_restart_callback @320
|
||||||
Z3_set_final_check_callback @321
|
Z3_set_reset_callback @321
|
||||||
Z3_set_new_eq_callback @322
|
Z3_set_final_check_callback @322
|
||||||
Z3_set_new_diseq_callback @323
|
Z3_set_new_eq_callback @323
|
||||||
Z3_set_new_assignment_callback @324
|
Z3_set_new_diseq_callback @324
|
||||||
Z3_set_new_relevant_callback @325
|
Z3_set_new_assignment_callback @325
|
||||||
Z3_theory_assert_axiom @326
|
Z3_set_new_relevant_callback @326
|
||||||
Z3_theory_assume_eq @327
|
Z3_theory_assert_axiom @327
|
||||||
Z3_theory_enable_axiom_simplification @328
|
Z3_theory_assume_eq @328
|
||||||
Z3_theory_get_eqc_root @329
|
Z3_theory_enable_axiom_simplification @329
|
||||||
Z3_theory_get_eqc_next @330
|
Z3_theory_get_eqc_root @330
|
||||||
Z3_theory_get_num_parents @331
|
Z3_theory_get_eqc_next @331
|
||||||
Z3_theory_get_parent @332
|
Z3_theory_get_num_parents @332
|
||||||
Z3_theory_is_value @333
|
Z3_theory_get_parent @333
|
||||||
Z3_theory_is_decl @334
|
Z3_theory_is_value @334
|
||||||
Z3_theory_get_num_elems @335
|
Z3_theory_is_decl @335
|
||||||
Z3_theory_get_elem @336
|
Z3_theory_get_num_elems @336
|
||||||
Z3_theory_get_num_apps @337
|
Z3_theory_get_elem @337
|
||||||
Z3_theory_get_app @338
|
Z3_theory_get_num_apps @338
|
||||||
Z3_mk_fixedpoint @339
|
Z3_theory_get_app @339
|
||||||
Z3_fixedpoint_inc_ref @340
|
Z3_mk_fixedpoint @340
|
||||||
Z3_fixedpoint_dec_ref @341
|
Z3_fixedpoint_inc_ref @341
|
||||||
Z3_fixedpoint_add_rule @342
|
Z3_fixedpoint_dec_ref @342
|
||||||
Z3_fixedpoint_add_fact @343
|
Z3_fixedpoint_add_rule @343
|
||||||
Z3_fixedpoint_assert @344
|
Z3_fixedpoint_add_fact @344
|
||||||
Z3_fixedpoint_query @345
|
Z3_fixedpoint_assert @345
|
||||||
Z3_fixedpoint_query_relations @346
|
Z3_fixedpoint_query @346
|
||||||
Z3_fixedpoint_get_answer @347
|
Z3_fixedpoint_query_relations @347
|
||||||
Z3_fixedpoint_get_reason_unknown @348
|
Z3_fixedpoint_get_answer @348
|
||||||
Z3_fixedpoint_update_rule @349
|
Z3_fixedpoint_get_reason_unknown @349
|
||||||
Z3_fixedpoint_get_num_levels @350
|
Z3_fixedpoint_update_rule @350
|
||||||
Z3_fixedpoint_get_cover_delta @351
|
Z3_fixedpoint_get_num_levels @351
|
||||||
Z3_fixedpoint_add_cover @352
|
Z3_fixedpoint_get_cover_delta @352
|
||||||
Z3_fixedpoint_get_statistics @353
|
Z3_fixedpoint_add_cover @353
|
||||||
Z3_fixedpoint_register_relation @354
|
Z3_fixedpoint_get_statistics @354
|
||||||
Z3_fixedpoint_set_predicate_representation @355
|
Z3_fixedpoint_register_relation @355
|
||||||
Z3_fixedpoint_simplify_rules @356
|
Z3_fixedpoint_set_predicate_representation @356
|
||||||
Z3_fixedpoint_set_params @357
|
Z3_fixedpoint_simplify_rules @357
|
||||||
Z3_fixedpoint_get_help @358
|
Z3_fixedpoint_set_params @358
|
||||||
Z3_fixedpoint_get_param_descrs @359
|
Z3_fixedpoint_get_help @359
|
||||||
Z3_fixedpoint_to_string @360
|
Z3_fixedpoint_get_param_descrs @360
|
||||||
Z3_fixedpoint_push @361
|
Z3_fixedpoint_to_string @361
|
||||||
Z3_fixedpoint_pop @362
|
Z3_fixedpoint_push @362
|
||||||
Z3_fixedpoint_init @363
|
Z3_fixedpoint_pop @363
|
||||||
Z3_fixedpoint_set_reduce_assign_callback @364
|
Z3_fixedpoint_init @364
|
||||||
Z3_fixedpoint_set_reduce_app_callback @365
|
Z3_fixedpoint_set_reduce_assign_callback @365
|
||||||
Z3_mk_ast_vector @366
|
Z3_fixedpoint_set_reduce_app_callback @366
|
||||||
Z3_ast_vector_inc_ref @367
|
Z3_mk_ast_vector @367
|
||||||
Z3_ast_vector_dec_ref @368
|
Z3_ast_vector_inc_ref @368
|
||||||
Z3_ast_vector_size @369
|
Z3_ast_vector_dec_ref @369
|
||||||
Z3_ast_vector_get @370
|
Z3_ast_vector_size @370
|
||||||
Z3_ast_vector_set @371
|
Z3_ast_vector_get @371
|
||||||
Z3_ast_vector_resize @372
|
Z3_ast_vector_set @372
|
||||||
Z3_ast_vector_push @373
|
Z3_ast_vector_resize @373
|
||||||
Z3_ast_vector_translate @374
|
Z3_ast_vector_push @374
|
||||||
Z3_ast_vector_to_string @375
|
Z3_ast_vector_translate @375
|
||||||
Z3_mk_ast_map @376
|
Z3_ast_vector_to_string @376
|
||||||
Z3_ast_map_inc_ref @377
|
Z3_mk_ast_map @377
|
||||||
Z3_ast_map_dec_ref @378
|
Z3_ast_map_inc_ref @378
|
||||||
Z3_ast_map_contains @379
|
Z3_ast_map_dec_ref @379
|
||||||
Z3_ast_map_find @380
|
Z3_ast_map_contains @380
|
||||||
Z3_ast_map_insert @381
|
Z3_ast_map_find @381
|
||||||
Z3_ast_map_erase @382
|
Z3_ast_map_insert @382
|
||||||
Z3_ast_map_reset @383
|
Z3_ast_map_erase @383
|
||||||
Z3_ast_map_size @384
|
Z3_ast_map_reset @384
|
||||||
Z3_ast_map_keys @385
|
Z3_ast_map_size @385
|
||||||
Z3_ast_map_to_string @386
|
Z3_ast_map_keys @386
|
||||||
Z3_mk_goal @387
|
Z3_ast_map_to_string @387
|
||||||
Z3_goal_inc_ref @388
|
Z3_mk_goal @388
|
||||||
Z3_goal_dec_ref @389
|
Z3_goal_inc_ref @389
|
||||||
Z3_goal_precision @390
|
Z3_goal_dec_ref @390
|
||||||
Z3_goal_assert @391
|
Z3_goal_precision @391
|
||||||
Z3_goal_inconsistent @392
|
Z3_goal_assert @392
|
||||||
Z3_goal_depth @393
|
Z3_goal_inconsistent @393
|
||||||
Z3_goal_reset @394
|
Z3_goal_depth @394
|
||||||
Z3_goal_size @395
|
Z3_goal_reset @395
|
||||||
Z3_goal_formula @396
|
Z3_goal_size @396
|
||||||
Z3_goal_num_exprs @397
|
Z3_goal_formula @397
|
||||||
Z3_goal_is_decided_sat @398
|
Z3_goal_num_exprs @398
|
||||||
Z3_goal_is_decided_unsat @399
|
Z3_goal_is_decided_sat @399
|
||||||
Z3_goal_translate @400
|
Z3_goal_is_decided_unsat @400
|
||||||
Z3_goal_to_string @401
|
Z3_goal_translate @401
|
||||||
Z3_mk_tactic @402
|
Z3_goal_to_string @402
|
||||||
Z3_tactic_inc_ref @403
|
Z3_mk_tactic @403
|
||||||
Z3_tactic_dec_ref @404
|
Z3_tactic_inc_ref @404
|
||||||
Z3_mk_probe @405
|
Z3_tactic_dec_ref @405
|
||||||
Z3_probe_inc_ref @406
|
Z3_mk_probe @406
|
||||||
Z3_probe_dec_ref @407
|
Z3_probe_inc_ref @407
|
||||||
Z3_tactic_and_then @408
|
Z3_probe_dec_ref @408
|
||||||
Z3_tactic_or_else @409
|
Z3_tactic_and_then @409
|
||||||
Z3_tactic_par_or @410
|
Z3_tactic_or_else @410
|
||||||
Z3_tactic_par_and_then @411
|
Z3_tactic_par_or @411
|
||||||
Z3_tactic_try_for @412
|
Z3_tactic_par_and_then @412
|
||||||
Z3_tactic_when @413
|
Z3_tactic_try_for @413
|
||||||
Z3_tactic_cond @414
|
Z3_tactic_when @414
|
||||||
Z3_tactic_repeat @415
|
Z3_tactic_cond @415
|
||||||
Z3_tactic_skip @416
|
Z3_tactic_repeat @416
|
||||||
Z3_tactic_fail @417
|
Z3_tactic_skip @417
|
||||||
Z3_tactic_fail_if @418
|
Z3_tactic_fail @418
|
||||||
Z3_tactic_fail_if_not_decided @419
|
Z3_tactic_fail_if @419
|
||||||
Z3_tactic_using_params @420
|
Z3_tactic_fail_if_not_decided @420
|
||||||
Z3_probe_const @421
|
Z3_tactic_using_params @421
|
||||||
Z3_probe_lt @422
|
Z3_probe_const @422
|
||||||
Z3_probe_gt @423
|
Z3_probe_lt @423
|
||||||
Z3_probe_le @424
|
Z3_probe_gt @424
|
||||||
Z3_probe_ge @425
|
Z3_probe_le @425
|
||||||
Z3_probe_eq @426
|
Z3_probe_ge @426
|
||||||
Z3_probe_and @427
|
Z3_probe_eq @427
|
||||||
Z3_probe_or @428
|
Z3_probe_and @428
|
||||||
Z3_probe_not @429
|
Z3_probe_or @429
|
||||||
Z3_get_num_tactics @430
|
Z3_probe_not @430
|
||||||
Z3_get_tactic_name @431
|
Z3_get_num_tactics @431
|
||||||
Z3_get_num_probes @432
|
Z3_get_tactic_name @432
|
||||||
Z3_get_probe_name @433
|
Z3_get_num_probes @433
|
||||||
Z3_tactic_get_help @434
|
Z3_get_probe_name @434
|
||||||
Z3_tactic_get_param_descrs @435
|
Z3_tactic_get_help @435
|
||||||
Z3_tactic_get_descr @436
|
Z3_tactic_get_param_descrs @436
|
||||||
Z3_probe_get_descr @437
|
Z3_tactic_get_descr @437
|
||||||
Z3_probe_apply @438
|
Z3_probe_get_descr @438
|
||||||
Z3_tactic_apply @439
|
Z3_probe_apply @439
|
||||||
Z3_tactic_apply_ex @440
|
Z3_tactic_apply @440
|
||||||
Z3_apply_result_inc_ref @441
|
Z3_tactic_apply_ex @441
|
||||||
Z3_apply_result_dec_ref @442
|
Z3_apply_result_inc_ref @442
|
||||||
Z3_apply_result_to_string @443
|
Z3_apply_result_dec_ref @443
|
||||||
Z3_apply_result_get_num_subgoals @444
|
Z3_apply_result_to_string @444
|
||||||
Z3_apply_result_get_subgoal @445
|
Z3_apply_result_get_num_subgoals @445
|
||||||
Z3_apply_result_convert_model @446
|
Z3_apply_result_get_subgoal @446
|
||||||
Z3_mk_solver @447
|
Z3_apply_result_convert_model @447
|
||||||
Z3_mk_simple_solver @448
|
Z3_mk_solver @448
|
||||||
Z3_mk_solver_for_logic @449
|
Z3_mk_simple_solver @449
|
||||||
Z3_mk_solver_from_tactic @450
|
Z3_mk_solver_for_logic @450
|
||||||
Z3_solver_get_help @451
|
Z3_mk_solver_from_tactic @451
|
||||||
Z3_solver_get_param_descrs @452
|
Z3_solver_get_help @452
|
||||||
Z3_solver_set_params @453
|
Z3_solver_get_param_descrs @453
|
||||||
Z3_solver_inc_ref @454
|
Z3_solver_set_params @454
|
||||||
Z3_solver_dec_ref @455
|
Z3_solver_inc_ref @455
|
||||||
Z3_solver_push @456
|
Z3_solver_dec_ref @456
|
||||||
Z3_solver_pop @457
|
Z3_solver_push @457
|
||||||
Z3_solver_reset @458
|
Z3_solver_pop @458
|
||||||
Z3_solver_get_num_scopes @459
|
Z3_solver_reset @459
|
||||||
Z3_solver_assert @460
|
Z3_solver_get_num_scopes @460
|
||||||
Z3_solver_get_assertions @461
|
Z3_solver_assert @461
|
||||||
Z3_solver_check @462
|
Z3_solver_get_assertions @462
|
||||||
Z3_solver_check_assumptions @463
|
Z3_solver_check @463
|
||||||
Z3_solver_get_model @464
|
Z3_solver_check_assumptions @464
|
||||||
Z3_solver_get_proof @465
|
Z3_solver_get_model @465
|
||||||
Z3_solver_get_unsat_core @466
|
Z3_solver_get_proof @466
|
||||||
Z3_solver_get_reason_unknown @467
|
Z3_solver_get_unsat_core @467
|
||||||
Z3_solver_get_statistics @468
|
Z3_solver_get_reason_unknown @468
|
||||||
Z3_solver_to_string @469
|
Z3_solver_get_statistics @469
|
||||||
Z3_stats_to_string @470
|
Z3_solver_to_string @470
|
||||||
Z3_stats_inc_ref @471
|
Z3_stats_to_string @471
|
||||||
Z3_stats_dec_ref @472
|
Z3_stats_inc_ref @472
|
||||||
Z3_stats_size @473
|
Z3_stats_dec_ref @473
|
||||||
Z3_stats_get_key @474
|
Z3_stats_size @474
|
||||||
Z3_stats_is_uint @475
|
Z3_stats_get_key @475
|
||||||
Z3_stats_is_double @476
|
Z3_stats_is_uint @476
|
||||||
Z3_stats_get_uint_value @477
|
Z3_stats_is_double @477
|
||||||
Z3_stats_get_double_value @478
|
Z3_stats_get_uint_value @478
|
||||||
Z3_mk_injective_function @479
|
Z3_stats_get_double_value @479
|
||||||
Z3_set_logic @480
|
Z3_mk_injective_function @480
|
||||||
Z3_push @481
|
Z3_set_logic @481
|
||||||
Z3_pop @482
|
Z3_push @482
|
||||||
Z3_get_num_scopes @483
|
Z3_pop @483
|
||||||
Z3_persist_ast @484
|
Z3_get_num_scopes @484
|
||||||
Z3_assert_cnstr @485
|
Z3_persist_ast @485
|
||||||
Z3_check_and_get_model @486
|
Z3_assert_cnstr @486
|
||||||
Z3_check @487
|
Z3_check_and_get_model @487
|
||||||
Z3_check_assumptions @488
|
Z3_check @488
|
||||||
Z3_get_implied_equalities @489
|
Z3_check_assumptions @489
|
||||||
Z3_del_model @490
|
Z3_get_implied_equalities @490
|
||||||
Z3_soft_check_cancel @491
|
Z3_del_model @491
|
||||||
Z3_get_search_failure @492
|
Z3_soft_check_cancel @492
|
||||||
Z3_mk_label @493
|
Z3_get_search_failure @493
|
||||||
Z3_get_relevant_labels @494
|
Z3_mk_label @494
|
||||||
Z3_get_relevant_literals @495
|
Z3_get_relevant_labels @495
|
||||||
Z3_get_guessed_literals @496
|
Z3_get_relevant_literals @496
|
||||||
Z3_del_literals @497
|
Z3_get_guessed_literals @497
|
||||||
Z3_get_num_literals @498
|
Z3_del_literals @498
|
||||||
Z3_get_label_symbol @499
|
Z3_get_num_literals @499
|
||||||
Z3_get_literal @500
|
Z3_get_label_symbol @500
|
||||||
Z3_disable_literal @501
|
Z3_get_literal @501
|
||||||
Z3_block_literals @502
|
Z3_disable_literal @502
|
||||||
Z3_get_model_num_constants @503
|
Z3_block_literals @503
|
||||||
Z3_get_model_constant @504
|
Z3_get_model_num_constants @504
|
||||||
Z3_get_model_num_funcs @505
|
Z3_get_model_constant @505
|
||||||
Z3_get_model_func_decl @506
|
Z3_get_model_num_funcs @506
|
||||||
Z3_eval_func_decl @507
|
Z3_get_model_func_decl @507
|
||||||
Z3_is_array_value @508
|
Z3_eval_func_decl @508
|
||||||
Z3_get_array_value @509
|
Z3_is_array_value @509
|
||||||
Z3_get_model_func_else @510
|
Z3_get_array_value @510
|
||||||
Z3_get_model_func_num_entries @511
|
Z3_get_model_func_else @511
|
||||||
Z3_get_model_func_entry_num_args @512
|
Z3_get_model_func_num_entries @512
|
||||||
Z3_get_model_func_entry_arg @513
|
Z3_get_model_func_entry_num_args @513
|
||||||
Z3_get_model_func_entry_value @514
|
Z3_get_model_func_entry_arg @514
|
||||||
Z3_eval @515
|
Z3_get_model_func_entry_value @515
|
||||||
Z3_eval_decl @516
|
Z3_eval @516
|
||||||
Z3_context_to_string @517
|
Z3_eval_decl @517
|
||||||
Z3_statistics_to_string @518
|
Z3_context_to_string @518
|
||||||
Z3_get_context_assignment @519
|
Z3_statistics_to_string @519
|
||||||
|
Z3_get_context_assignment @520
|
||||||
|
|
|
||||||
|
|
@ -1100,6 +1100,7 @@ API('Z3_param_descrs_dec_ref', VOID, (_in(CONTEXT), _in(PARAM_DESCRS)))
|
||||||
API('Z3_param_descrs_get_kind', UINT, (_in(CONTEXT), _in(PARAM_DESCRS), _in(SYMBOL)))
|
API('Z3_param_descrs_get_kind', UINT, (_in(CONTEXT), _in(PARAM_DESCRS), _in(SYMBOL)))
|
||||||
API('Z3_param_descrs_size', UINT, (_in(CONTEXT), _in(PARAM_DESCRS)))
|
API('Z3_param_descrs_size', UINT, (_in(CONTEXT), _in(PARAM_DESCRS)))
|
||||||
API('Z3_param_descrs_get_name', SYMBOL, (_in(CONTEXT), _in(PARAM_DESCRS), _in(UINT)))
|
API('Z3_param_descrs_get_name', SYMBOL, (_in(CONTEXT), _in(PARAM_DESCRS), _in(UINT)))
|
||||||
|
API('Z3_param_descrs_to_string', STRING, (_in(CONTEXT), _in(PARAM_DESCRS)))
|
||||||
# New APIs
|
# New APIs
|
||||||
API('Z3_interrupt', VOID, (_in(CONTEXT),))
|
API('Z3_interrupt', VOID, (_in(CONTEXT),))
|
||||||
API('Z3_get_error_msg_ex', STRING, (_in(CONTEXT), _in(ERROR_CODE)))
|
API('Z3_get_error_msg_ex', STRING, (_in(CONTEXT), _in(ERROR_CODE)))
|
||||||
|
|
|
||||||
|
|
@ -2328,6 +2328,11 @@ void exec_Z3_param_descrs_get_name(z3_replayer & in) {
|
||||||
reinterpret_cast<Z3_param_descrs>(in.get_obj(1)),
|
reinterpret_cast<Z3_param_descrs>(in.get_obj(1)),
|
||||||
in.get_uint(2));
|
in.get_uint(2));
|
||||||
}
|
}
|
||||||
|
void exec_Z3_param_descrs_to_string(z3_replayer & in) {
|
||||||
|
Z3_param_descrs_to_string(
|
||||||
|
reinterpret_cast<Z3_context>(in.get_obj(0)),
|
||||||
|
reinterpret_cast<Z3_param_descrs>(in.get_obj(1)));
|
||||||
|
}
|
||||||
void exec_Z3_interrupt(z3_replayer & in) {
|
void exec_Z3_interrupt(z3_replayer & in) {
|
||||||
Z3_interrupt(
|
Z3_interrupt(
|
||||||
reinterpret_cast<Z3_context>(in.get_obj(0)));
|
reinterpret_cast<Z3_context>(in.get_obj(0)));
|
||||||
|
|
@ -3359,120 +3364,121 @@ void register_z3_replayer_cmds(z3_replayer & in) {
|
||||||
in.register_cmd(357, exec_Z3_param_descrs_get_kind);
|
in.register_cmd(357, exec_Z3_param_descrs_get_kind);
|
||||||
in.register_cmd(358, exec_Z3_param_descrs_size);
|
in.register_cmd(358, exec_Z3_param_descrs_size);
|
||||||
in.register_cmd(359, exec_Z3_param_descrs_get_name);
|
in.register_cmd(359, exec_Z3_param_descrs_get_name);
|
||||||
in.register_cmd(360, exec_Z3_interrupt);
|
in.register_cmd(360, exec_Z3_param_descrs_to_string);
|
||||||
in.register_cmd(361, exec_Z3_get_error_msg_ex);
|
in.register_cmd(361, exec_Z3_interrupt);
|
||||||
in.register_cmd(362, exec_Z3_translate);
|
in.register_cmd(362, exec_Z3_get_error_msg_ex);
|
||||||
in.register_cmd(363, exec_Z3_mk_goal);
|
in.register_cmd(363, exec_Z3_translate);
|
||||||
in.register_cmd(364, exec_Z3_goal_inc_ref);
|
in.register_cmd(364, exec_Z3_mk_goal);
|
||||||
in.register_cmd(365, exec_Z3_goal_dec_ref);
|
in.register_cmd(365, exec_Z3_goal_inc_ref);
|
||||||
in.register_cmd(366, exec_Z3_goal_precision);
|
in.register_cmd(366, exec_Z3_goal_dec_ref);
|
||||||
in.register_cmd(367, exec_Z3_goal_assert);
|
in.register_cmd(367, exec_Z3_goal_precision);
|
||||||
in.register_cmd(368, exec_Z3_goal_inconsistent);
|
in.register_cmd(368, exec_Z3_goal_assert);
|
||||||
in.register_cmd(369, exec_Z3_goal_depth);
|
in.register_cmd(369, exec_Z3_goal_inconsistent);
|
||||||
in.register_cmd(370, exec_Z3_goal_reset);
|
in.register_cmd(370, exec_Z3_goal_depth);
|
||||||
in.register_cmd(371, exec_Z3_goal_size);
|
in.register_cmd(371, exec_Z3_goal_reset);
|
||||||
in.register_cmd(372, exec_Z3_goal_formula);
|
in.register_cmd(372, exec_Z3_goal_size);
|
||||||
in.register_cmd(373, exec_Z3_goal_num_exprs);
|
in.register_cmd(373, exec_Z3_goal_formula);
|
||||||
in.register_cmd(374, exec_Z3_goal_is_decided_sat);
|
in.register_cmd(374, exec_Z3_goal_num_exprs);
|
||||||
in.register_cmd(375, exec_Z3_goal_is_decided_unsat);
|
in.register_cmd(375, exec_Z3_goal_is_decided_sat);
|
||||||
in.register_cmd(376, exec_Z3_goal_translate);
|
in.register_cmd(376, exec_Z3_goal_is_decided_unsat);
|
||||||
in.register_cmd(377, exec_Z3_goal_to_string);
|
in.register_cmd(377, exec_Z3_goal_translate);
|
||||||
in.register_cmd(378, exec_Z3_mk_tactic);
|
in.register_cmd(378, exec_Z3_goal_to_string);
|
||||||
in.register_cmd(379, exec_Z3_mk_probe);
|
in.register_cmd(379, exec_Z3_mk_tactic);
|
||||||
in.register_cmd(380, exec_Z3_tactic_inc_ref);
|
in.register_cmd(380, exec_Z3_mk_probe);
|
||||||
in.register_cmd(381, exec_Z3_tactic_dec_ref);
|
in.register_cmd(381, exec_Z3_tactic_inc_ref);
|
||||||
in.register_cmd(382, exec_Z3_probe_inc_ref);
|
in.register_cmd(382, exec_Z3_tactic_dec_ref);
|
||||||
in.register_cmd(383, exec_Z3_probe_dec_ref);
|
in.register_cmd(383, exec_Z3_probe_inc_ref);
|
||||||
in.register_cmd(384, exec_Z3_tactic_and_then);
|
in.register_cmd(384, exec_Z3_probe_dec_ref);
|
||||||
in.register_cmd(385, exec_Z3_tactic_or_else);
|
in.register_cmd(385, exec_Z3_tactic_and_then);
|
||||||
in.register_cmd(386, exec_Z3_tactic_par_or);
|
in.register_cmd(386, exec_Z3_tactic_or_else);
|
||||||
in.register_cmd(387, exec_Z3_tactic_par_and_then);
|
in.register_cmd(387, exec_Z3_tactic_par_or);
|
||||||
in.register_cmd(388, exec_Z3_tactic_try_for);
|
in.register_cmd(388, exec_Z3_tactic_par_and_then);
|
||||||
in.register_cmd(389, exec_Z3_tactic_when);
|
in.register_cmd(389, exec_Z3_tactic_try_for);
|
||||||
in.register_cmd(390, exec_Z3_tactic_cond);
|
in.register_cmd(390, exec_Z3_tactic_when);
|
||||||
in.register_cmd(391, exec_Z3_tactic_repeat);
|
in.register_cmd(391, exec_Z3_tactic_cond);
|
||||||
in.register_cmd(392, exec_Z3_tactic_skip);
|
in.register_cmd(392, exec_Z3_tactic_repeat);
|
||||||
in.register_cmd(393, exec_Z3_tactic_fail);
|
in.register_cmd(393, exec_Z3_tactic_skip);
|
||||||
in.register_cmd(394, exec_Z3_tactic_fail_if);
|
in.register_cmd(394, exec_Z3_tactic_fail);
|
||||||
in.register_cmd(395, exec_Z3_tactic_fail_if_not_decided);
|
in.register_cmd(395, exec_Z3_tactic_fail_if);
|
||||||
in.register_cmd(396, exec_Z3_tactic_using_params);
|
in.register_cmd(396, exec_Z3_tactic_fail_if_not_decided);
|
||||||
in.register_cmd(397, exec_Z3_probe_const);
|
in.register_cmd(397, exec_Z3_tactic_using_params);
|
||||||
in.register_cmd(398, exec_Z3_probe_lt);
|
in.register_cmd(398, exec_Z3_probe_const);
|
||||||
in.register_cmd(399, exec_Z3_probe_le);
|
in.register_cmd(399, exec_Z3_probe_lt);
|
||||||
in.register_cmd(400, exec_Z3_probe_gt);
|
in.register_cmd(400, exec_Z3_probe_le);
|
||||||
in.register_cmd(401, exec_Z3_probe_ge);
|
in.register_cmd(401, exec_Z3_probe_gt);
|
||||||
in.register_cmd(402, exec_Z3_probe_eq);
|
in.register_cmd(402, exec_Z3_probe_ge);
|
||||||
in.register_cmd(403, exec_Z3_probe_and);
|
in.register_cmd(403, exec_Z3_probe_eq);
|
||||||
in.register_cmd(404, exec_Z3_probe_or);
|
in.register_cmd(404, exec_Z3_probe_and);
|
||||||
in.register_cmd(405, exec_Z3_probe_not);
|
in.register_cmd(405, exec_Z3_probe_or);
|
||||||
in.register_cmd(406, exec_Z3_get_num_tactics);
|
in.register_cmd(406, exec_Z3_probe_not);
|
||||||
in.register_cmd(407, exec_Z3_get_tactic_name);
|
in.register_cmd(407, exec_Z3_get_num_tactics);
|
||||||
in.register_cmd(408, exec_Z3_get_num_probes);
|
in.register_cmd(408, exec_Z3_get_tactic_name);
|
||||||
in.register_cmd(409, exec_Z3_get_probe_name);
|
in.register_cmd(409, exec_Z3_get_num_probes);
|
||||||
in.register_cmd(410, exec_Z3_tactic_get_help);
|
in.register_cmd(410, exec_Z3_get_probe_name);
|
||||||
in.register_cmd(411, exec_Z3_tactic_get_param_descrs);
|
in.register_cmd(411, exec_Z3_tactic_get_help);
|
||||||
in.register_cmd(412, exec_Z3_tactic_get_descr);
|
in.register_cmd(412, exec_Z3_tactic_get_param_descrs);
|
||||||
in.register_cmd(413, exec_Z3_probe_get_descr);
|
in.register_cmd(413, exec_Z3_tactic_get_descr);
|
||||||
in.register_cmd(414, exec_Z3_probe_apply);
|
in.register_cmd(414, exec_Z3_probe_get_descr);
|
||||||
in.register_cmd(415, exec_Z3_tactic_apply);
|
in.register_cmd(415, exec_Z3_probe_apply);
|
||||||
in.register_cmd(416, exec_Z3_tactic_apply_ex);
|
in.register_cmd(416, exec_Z3_tactic_apply);
|
||||||
in.register_cmd(417, exec_Z3_apply_result_inc_ref);
|
in.register_cmd(417, exec_Z3_tactic_apply_ex);
|
||||||
in.register_cmd(418, exec_Z3_apply_result_dec_ref);
|
in.register_cmd(418, exec_Z3_apply_result_inc_ref);
|
||||||
in.register_cmd(419, exec_Z3_apply_result_to_string);
|
in.register_cmd(419, exec_Z3_apply_result_dec_ref);
|
||||||
in.register_cmd(420, exec_Z3_apply_result_get_num_subgoals);
|
in.register_cmd(420, exec_Z3_apply_result_to_string);
|
||||||
in.register_cmd(421, exec_Z3_apply_result_get_subgoal);
|
in.register_cmd(421, exec_Z3_apply_result_get_num_subgoals);
|
||||||
in.register_cmd(422, exec_Z3_apply_result_convert_model);
|
in.register_cmd(422, exec_Z3_apply_result_get_subgoal);
|
||||||
in.register_cmd(423, exec_Z3_mk_solver);
|
in.register_cmd(423, exec_Z3_apply_result_convert_model);
|
||||||
in.register_cmd(424, exec_Z3_mk_simple_solver);
|
in.register_cmd(424, exec_Z3_mk_solver);
|
||||||
in.register_cmd(425, exec_Z3_mk_solver_for_logic);
|
in.register_cmd(425, exec_Z3_mk_simple_solver);
|
||||||
in.register_cmd(426, exec_Z3_mk_solver_from_tactic);
|
in.register_cmd(426, exec_Z3_mk_solver_for_logic);
|
||||||
in.register_cmd(427, exec_Z3_solver_get_help);
|
in.register_cmd(427, exec_Z3_mk_solver_from_tactic);
|
||||||
in.register_cmd(428, exec_Z3_solver_get_param_descrs);
|
in.register_cmd(428, exec_Z3_solver_get_help);
|
||||||
in.register_cmd(429, exec_Z3_solver_set_params);
|
in.register_cmd(429, exec_Z3_solver_get_param_descrs);
|
||||||
in.register_cmd(430, exec_Z3_solver_inc_ref);
|
in.register_cmd(430, exec_Z3_solver_set_params);
|
||||||
in.register_cmd(431, exec_Z3_solver_dec_ref);
|
in.register_cmd(431, exec_Z3_solver_inc_ref);
|
||||||
in.register_cmd(432, exec_Z3_solver_push);
|
in.register_cmd(432, exec_Z3_solver_dec_ref);
|
||||||
in.register_cmd(433, exec_Z3_solver_pop);
|
in.register_cmd(433, exec_Z3_solver_push);
|
||||||
in.register_cmd(434, exec_Z3_solver_reset);
|
in.register_cmd(434, exec_Z3_solver_pop);
|
||||||
in.register_cmd(435, exec_Z3_solver_get_num_scopes);
|
in.register_cmd(435, exec_Z3_solver_reset);
|
||||||
in.register_cmd(436, exec_Z3_solver_assert);
|
in.register_cmd(436, exec_Z3_solver_get_num_scopes);
|
||||||
in.register_cmd(437, exec_Z3_solver_get_assertions);
|
in.register_cmd(437, exec_Z3_solver_assert);
|
||||||
in.register_cmd(438, exec_Z3_solver_check);
|
in.register_cmd(438, exec_Z3_solver_get_assertions);
|
||||||
in.register_cmd(439, exec_Z3_solver_check_assumptions);
|
in.register_cmd(439, exec_Z3_solver_check);
|
||||||
in.register_cmd(440, exec_Z3_solver_get_model);
|
in.register_cmd(440, exec_Z3_solver_check_assumptions);
|
||||||
in.register_cmd(441, exec_Z3_solver_get_proof);
|
in.register_cmd(441, exec_Z3_solver_get_model);
|
||||||
in.register_cmd(442, exec_Z3_solver_get_unsat_core);
|
in.register_cmd(442, exec_Z3_solver_get_proof);
|
||||||
in.register_cmd(443, exec_Z3_solver_get_reason_unknown);
|
in.register_cmd(443, exec_Z3_solver_get_unsat_core);
|
||||||
in.register_cmd(444, exec_Z3_solver_get_statistics);
|
in.register_cmd(444, exec_Z3_solver_get_reason_unknown);
|
||||||
in.register_cmd(445, exec_Z3_solver_to_string);
|
in.register_cmd(445, exec_Z3_solver_get_statistics);
|
||||||
in.register_cmd(446, exec_Z3_stats_to_string);
|
in.register_cmd(446, exec_Z3_solver_to_string);
|
||||||
in.register_cmd(447, exec_Z3_stats_inc_ref);
|
in.register_cmd(447, exec_Z3_stats_to_string);
|
||||||
in.register_cmd(448, exec_Z3_stats_dec_ref);
|
in.register_cmd(448, exec_Z3_stats_inc_ref);
|
||||||
in.register_cmd(449, exec_Z3_stats_size);
|
in.register_cmd(449, exec_Z3_stats_dec_ref);
|
||||||
in.register_cmd(450, exec_Z3_stats_get_key);
|
in.register_cmd(450, exec_Z3_stats_size);
|
||||||
in.register_cmd(451, exec_Z3_stats_is_uint);
|
in.register_cmd(451, exec_Z3_stats_get_key);
|
||||||
in.register_cmd(452, exec_Z3_stats_is_double);
|
in.register_cmd(452, exec_Z3_stats_is_uint);
|
||||||
in.register_cmd(453, exec_Z3_stats_get_uint_value);
|
in.register_cmd(453, exec_Z3_stats_is_double);
|
||||||
in.register_cmd(454, exec_Z3_stats_get_double_value);
|
in.register_cmd(454, exec_Z3_stats_get_uint_value);
|
||||||
in.register_cmd(455, exec_Z3_mk_ast_vector);
|
in.register_cmd(455, exec_Z3_stats_get_double_value);
|
||||||
in.register_cmd(456, exec_Z3_ast_vector_inc_ref);
|
in.register_cmd(456, exec_Z3_mk_ast_vector);
|
||||||
in.register_cmd(457, exec_Z3_ast_vector_dec_ref);
|
in.register_cmd(457, exec_Z3_ast_vector_inc_ref);
|
||||||
in.register_cmd(458, exec_Z3_ast_vector_size);
|
in.register_cmd(458, exec_Z3_ast_vector_dec_ref);
|
||||||
in.register_cmd(459, exec_Z3_ast_vector_get);
|
in.register_cmd(459, exec_Z3_ast_vector_size);
|
||||||
in.register_cmd(460, exec_Z3_ast_vector_set);
|
in.register_cmd(460, exec_Z3_ast_vector_get);
|
||||||
in.register_cmd(461, exec_Z3_ast_vector_resize);
|
in.register_cmd(461, exec_Z3_ast_vector_set);
|
||||||
in.register_cmd(462, exec_Z3_ast_vector_push);
|
in.register_cmd(462, exec_Z3_ast_vector_resize);
|
||||||
in.register_cmd(463, exec_Z3_ast_vector_translate);
|
in.register_cmd(463, exec_Z3_ast_vector_push);
|
||||||
in.register_cmd(464, exec_Z3_ast_vector_to_string);
|
in.register_cmd(464, exec_Z3_ast_vector_translate);
|
||||||
in.register_cmd(465, exec_Z3_mk_ast_map);
|
in.register_cmd(465, exec_Z3_ast_vector_to_string);
|
||||||
in.register_cmd(466, exec_Z3_ast_map_inc_ref);
|
in.register_cmd(466, exec_Z3_mk_ast_map);
|
||||||
in.register_cmd(467, exec_Z3_ast_map_dec_ref);
|
in.register_cmd(467, exec_Z3_ast_map_inc_ref);
|
||||||
in.register_cmd(468, exec_Z3_ast_map_contains);
|
in.register_cmd(468, exec_Z3_ast_map_dec_ref);
|
||||||
in.register_cmd(469, exec_Z3_ast_map_find);
|
in.register_cmd(469, exec_Z3_ast_map_contains);
|
||||||
in.register_cmd(470, exec_Z3_ast_map_insert);
|
in.register_cmd(470, exec_Z3_ast_map_find);
|
||||||
in.register_cmd(471, exec_Z3_ast_map_erase);
|
in.register_cmd(471, exec_Z3_ast_map_insert);
|
||||||
in.register_cmd(472, exec_Z3_ast_map_size);
|
in.register_cmd(472, exec_Z3_ast_map_erase);
|
||||||
in.register_cmd(473, exec_Z3_ast_map_reset);
|
in.register_cmd(473, exec_Z3_ast_map_size);
|
||||||
in.register_cmd(474, exec_Z3_ast_map_keys);
|
in.register_cmd(474, exec_Z3_ast_map_reset);
|
||||||
in.register_cmd(475, exec_Z3_ast_map_to_string);
|
in.register_cmd(475, exec_Z3_ast_map_keys);
|
||||||
|
in.register_cmd(476, exec_Z3_ast_map_to_string);
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -2570,23 +2570,29 @@ void log_Z3_param_descrs_get_name(Z3_context a0, Z3_param_descrs a1, unsigned a2
|
||||||
U(a2);
|
U(a2);
|
||||||
C(359);
|
C(359);
|
||||||
}
|
}
|
||||||
|
void log_Z3_param_descrs_to_string(Z3_context a0, Z3_param_descrs a1) {
|
||||||
|
R();
|
||||||
|
P(a0);
|
||||||
|
P(a1);
|
||||||
|
C(360);
|
||||||
|
}
|
||||||
void log_Z3_interrupt(Z3_context a0) {
|
void log_Z3_interrupt(Z3_context a0) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
C(360);
|
C(361);
|
||||||
}
|
}
|
||||||
void log_Z3_get_error_msg_ex(Z3_context a0, Z3_error_code a1) {
|
void log_Z3_get_error_msg_ex(Z3_context a0, Z3_error_code a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
U(static_cast<unsigned>(a1));
|
U(static_cast<unsigned>(a1));
|
||||||
C(361);
|
C(362);
|
||||||
}
|
}
|
||||||
void log_Z3_translate(Z3_context a0, Z3_ast a1, Z3_context a2) {
|
void log_Z3_translate(Z3_context a0, Z3_ast a1, Z3_context a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(362);
|
C(363);
|
||||||
}
|
}
|
||||||
void log_Z3_mk_goal(Z3_context a0, Z3_bool a1, Z3_bool a2, Z3_bool a3) {
|
void log_Z3_mk_goal(Z3_context a0, Z3_bool a1, Z3_bool a2, Z3_bool a3) {
|
||||||
R();
|
R();
|
||||||
|
|
@ -2594,144 +2600,144 @@ void log_Z3_mk_goal(Z3_context a0, Z3_bool a1, Z3_bool a2, Z3_bool a3) {
|
||||||
I(a1);
|
I(a1);
|
||||||
I(a2);
|
I(a2);
|
||||||
I(a3);
|
I(a3);
|
||||||
C(363);
|
C(364);
|
||||||
}
|
}
|
||||||
void log_Z3_goal_inc_ref(Z3_context a0, Z3_goal a1) {
|
void log_Z3_goal_inc_ref(Z3_context a0, Z3_goal a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(364);
|
C(365);
|
||||||
}
|
}
|
||||||
void log_Z3_goal_dec_ref(Z3_context a0, Z3_goal a1) {
|
void log_Z3_goal_dec_ref(Z3_context a0, Z3_goal a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(365);
|
C(366);
|
||||||
}
|
}
|
||||||
void log_Z3_goal_precision(Z3_context a0, Z3_goal a1) {
|
void log_Z3_goal_precision(Z3_context a0, Z3_goal a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(366);
|
C(367);
|
||||||
}
|
}
|
||||||
void log_Z3_goal_assert(Z3_context a0, Z3_goal a1, Z3_ast a2) {
|
void log_Z3_goal_assert(Z3_context a0, Z3_goal a1, Z3_ast a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(367);
|
C(368);
|
||||||
}
|
}
|
||||||
void log_Z3_goal_inconsistent(Z3_context a0, Z3_goal a1) {
|
void log_Z3_goal_inconsistent(Z3_context a0, Z3_goal a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(368);
|
C(369);
|
||||||
}
|
}
|
||||||
void log_Z3_goal_depth(Z3_context a0, Z3_goal a1) {
|
void log_Z3_goal_depth(Z3_context a0, Z3_goal a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(369);
|
C(370);
|
||||||
}
|
}
|
||||||
void log_Z3_goal_reset(Z3_context a0, Z3_goal a1) {
|
void log_Z3_goal_reset(Z3_context a0, Z3_goal a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(370);
|
C(371);
|
||||||
}
|
}
|
||||||
void log_Z3_goal_size(Z3_context a0, Z3_goal a1) {
|
void log_Z3_goal_size(Z3_context a0, Z3_goal a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(371);
|
C(372);
|
||||||
}
|
}
|
||||||
void log_Z3_goal_formula(Z3_context a0, Z3_goal a1, unsigned a2) {
|
void log_Z3_goal_formula(Z3_context a0, Z3_goal a1, unsigned a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
U(a2);
|
U(a2);
|
||||||
C(372);
|
C(373);
|
||||||
}
|
}
|
||||||
void log_Z3_goal_num_exprs(Z3_context a0, Z3_goal a1) {
|
void log_Z3_goal_num_exprs(Z3_context a0, Z3_goal a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(373);
|
C(374);
|
||||||
}
|
}
|
||||||
void log_Z3_goal_is_decided_sat(Z3_context a0, Z3_goal a1) {
|
void log_Z3_goal_is_decided_sat(Z3_context a0, Z3_goal a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(374);
|
C(375);
|
||||||
}
|
}
|
||||||
void log_Z3_goal_is_decided_unsat(Z3_context a0, Z3_goal a1) {
|
void log_Z3_goal_is_decided_unsat(Z3_context a0, Z3_goal a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(375);
|
C(376);
|
||||||
}
|
}
|
||||||
void log_Z3_goal_translate(Z3_context a0, Z3_goal a1, Z3_context a2) {
|
void log_Z3_goal_translate(Z3_context a0, Z3_goal a1, Z3_context a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(376);
|
C(377);
|
||||||
}
|
}
|
||||||
void log_Z3_goal_to_string(Z3_context a0, Z3_goal a1) {
|
void log_Z3_goal_to_string(Z3_context a0, Z3_goal a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(377);
|
C(378);
|
||||||
}
|
}
|
||||||
void log_Z3_mk_tactic(Z3_context a0, Z3_string a1) {
|
void log_Z3_mk_tactic(Z3_context a0, Z3_string a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
S(a1);
|
S(a1);
|
||||||
C(378);
|
C(379);
|
||||||
}
|
}
|
||||||
void log_Z3_mk_probe(Z3_context a0, Z3_string a1) {
|
void log_Z3_mk_probe(Z3_context a0, Z3_string a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
S(a1);
|
S(a1);
|
||||||
C(379);
|
C(380);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_inc_ref(Z3_context a0, Z3_tactic a1) {
|
void log_Z3_tactic_inc_ref(Z3_context a0, Z3_tactic a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(380);
|
C(381);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_dec_ref(Z3_context a0, Z3_tactic a1) {
|
void log_Z3_tactic_dec_ref(Z3_context a0, Z3_tactic a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(381);
|
C(382);
|
||||||
}
|
}
|
||||||
void log_Z3_probe_inc_ref(Z3_context a0, Z3_probe a1) {
|
void log_Z3_probe_inc_ref(Z3_context a0, Z3_probe a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(382);
|
C(383);
|
||||||
}
|
}
|
||||||
void log_Z3_probe_dec_ref(Z3_context a0, Z3_probe a1) {
|
void log_Z3_probe_dec_ref(Z3_context a0, Z3_probe a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(383);
|
C(384);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2) {
|
void log_Z3_tactic_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(384);
|
C(385);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_or_else(Z3_context a0, Z3_tactic a1, Z3_tactic a2) {
|
void log_Z3_tactic_or_else(Z3_context a0, Z3_tactic a1, Z3_tactic a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(385);
|
C(386);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_par_or(Z3_context a0, unsigned a1, Z3_tactic const * a2) {
|
void log_Z3_tactic_par_or(Z3_context a0, unsigned a1, Z3_tactic const * a2) {
|
||||||
R();
|
R();
|
||||||
|
|
@ -2739,28 +2745,28 @@ void log_Z3_tactic_par_or(Z3_context a0, unsigned a1, Z3_tactic const * a2) {
|
||||||
U(a1);
|
U(a1);
|
||||||
for (unsigned i = 0; i < a1; i++) { P(a2[i]); }
|
for (unsigned i = 0; i < a1; i++) { P(a2[i]); }
|
||||||
Ap(a1);
|
Ap(a1);
|
||||||
C(386);
|
C(387);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_par_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2) {
|
void log_Z3_tactic_par_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(387);
|
C(388);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_try_for(Z3_context a0, Z3_tactic a1, unsigned a2) {
|
void log_Z3_tactic_try_for(Z3_context a0, Z3_tactic a1, unsigned a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
U(a2);
|
U(a2);
|
||||||
C(388);
|
C(389);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_when(Z3_context a0, Z3_probe a1, Z3_tactic a2) {
|
void log_Z3_tactic_when(Z3_context a0, Z3_probe a1, Z3_tactic a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(389);
|
C(390);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_cond(Z3_context a0, Z3_probe a1, Z3_tactic a2, Z3_tactic a3) {
|
void log_Z3_tactic_cond(Z3_context a0, Z3_probe a1, Z3_tactic a2, Z3_tactic a3) {
|
||||||
R();
|
R();
|
||||||
|
|
@ -2768,163 +2774,163 @@ void log_Z3_tactic_cond(Z3_context a0, Z3_probe a1, Z3_tactic a2, Z3_tactic a3)
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
P(a3);
|
P(a3);
|
||||||
C(390);
|
C(391);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_repeat(Z3_context a0, Z3_tactic a1, unsigned a2) {
|
void log_Z3_tactic_repeat(Z3_context a0, Z3_tactic a1, unsigned a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
U(a2);
|
U(a2);
|
||||||
C(391);
|
C(392);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_skip(Z3_context a0) {
|
void log_Z3_tactic_skip(Z3_context a0) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
C(392);
|
C(393);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_fail(Z3_context a0) {
|
void log_Z3_tactic_fail(Z3_context a0) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
C(393);
|
C(394);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_fail_if(Z3_context a0, Z3_probe a1) {
|
void log_Z3_tactic_fail_if(Z3_context a0, Z3_probe a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(394);
|
C(395);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_fail_if_not_decided(Z3_context a0) {
|
void log_Z3_tactic_fail_if_not_decided(Z3_context a0) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
C(395);
|
C(396);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_using_params(Z3_context a0, Z3_tactic a1, Z3_params a2) {
|
void log_Z3_tactic_using_params(Z3_context a0, Z3_tactic a1, Z3_params a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(396);
|
C(397);
|
||||||
}
|
}
|
||||||
void log_Z3_probe_const(Z3_context a0, double a1) {
|
void log_Z3_probe_const(Z3_context a0, double a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
D(a1);
|
D(a1);
|
||||||
C(397);
|
C(398);
|
||||||
}
|
}
|
||||||
void log_Z3_probe_lt(Z3_context a0, Z3_probe a1, Z3_probe a2) {
|
void log_Z3_probe_lt(Z3_context a0, Z3_probe a1, Z3_probe a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(398);
|
C(399);
|
||||||
}
|
}
|
||||||
void log_Z3_probe_le(Z3_context a0, Z3_probe a1, Z3_probe a2) {
|
void log_Z3_probe_le(Z3_context a0, Z3_probe a1, Z3_probe a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(399);
|
C(400);
|
||||||
}
|
}
|
||||||
void log_Z3_probe_gt(Z3_context a0, Z3_probe a1, Z3_probe a2) {
|
void log_Z3_probe_gt(Z3_context a0, Z3_probe a1, Z3_probe a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(400);
|
C(401);
|
||||||
}
|
}
|
||||||
void log_Z3_probe_ge(Z3_context a0, Z3_probe a1, Z3_probe a2) {
|
void log_Z3_probe_ge(Z3_context a0, Z3_probe a1, Z3_probe a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(401);
|
C(402);
|
||||||
}
|
}
|
||||||
void log_Z3_probe_eq(Z3_context a0, Z3_probe a1, Z3_probe a2) {
|
void log_Z3_probe_eq(Z3_context a0, Z3_probe a1, Z3_probe a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(402);
|
C(403);
|
||||||
}
|
}
|
||||||
void log_Z3_probe_and(Z3_context a0, Z3_probe a1, Z3_probe a2) {
|
void log_Z3_probe_and(Z3_context a0, Z3_probe a1, Z3_probe a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(403);
|
C(404);
|
||||||
}
|
}
|
||||||
void log_Z3_probe_or(Z3_context a0, Z3_probe a1, Z3_probe a2) {
|
void log_Z3_probe_or(Z3_context a0, Z3_probe a1, Z3_probe a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(404);
|
C(405);
|
||||||
}
|
}
|
||||||
void log_Z3_probe_not(Z3_context a0, Z3_probe a1) {
|
void log_Z3_probe_not(Z3_context a0, Z3_probe a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(405);
|
C(406);
|
||||||
}
|
}
|
||||||
void log_Z3_get_num_tactics(Z3_context a0) {
|
void log_Z3_get_num_tactics(Z3_context a0) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
C(406);
|
C(407);
|
||||||
}
|
}
|
||||||
void log_Z3_get_tactic_name(Z3_context a0, unsigned a1) {
|
void log_Z3_get_tactic_name(Z3_context a0, unsigned a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
U(a1);
|
U(a1);
|
||||||
C(407);
|
C(408);
|
||||||
}
|
}
|
||||||
void log_Z3_get_num_probes(Z3_context a0) {
|
void log_Z3_get_num_probes(Z3_context a0) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
C(408);
|
C(409);
|
||||||
}
|
}
|
||||||
void log_Z3_get_probe_name(Z3_context a0, unsigned a1) {
|
void log_Z3_get_probe_name(Z3_context a0, unsigned a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
U(a1);
|
U(a1);
|
||||||
C(409);
|
C(410);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_get_help(Z3_context a0, Z3_tactic a1) {
|
void log_Z3_tactic_get_help(Z3_context a0, Z3_tactic a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(410);
|
C(411);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_get_param_descrs(Z3_context a0, Z3_tactic a1) {
|
void log_Z3_tactic_get_param_descrs(Z3_context a0, Z3_tactic a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(411);
|
C(412);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_get_descr(Z3_context a0, Z3_string a1) {
|
void log_Z3_tactic_get_descr(Z3_context a0, Z3_string a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
S(a1);
|
S(a1);
|
||||||
C(412);
|
C(413);
|
||||||
}
|
}
|
||||||
void log_Z3_probe_get_descr(Z3_context a0, Z3_string a1) {
|
void log_Z3_probe_get_descr(Z3_context a0, Z3_string a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
S(a1);
|
S(a1);
|
||||||
C(413);
|
C(414);
|
||||||
}
|
}
|
||||||
void log_Z3_probe_apply(Z3_context a0, Z3_probe a1, Z3_goal a2) {
|
void log_Z3_probe_apply(Z3_context a0, Z3_probe a1, Z3_goal a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(414);
|
C(415);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_apply(Z3_context a0, Z3_tactic a1, Z3_goal a2) {
|
void log_Z3_tactic_apply(Z3_context a0, Z3_tactic a1, Z3_goal a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(415);
|
C(416);
|
||||||
}
|
}
|
||||||
void log_Z3_tactic_apply_ex(Z3_context a0, Z3_tactic a1, Z3_goal a2, Z3_params a3) {
|
void log_Z3_tactic_apply_ex(Z3_context a0, Z3_tactic a1, Z3_goal a2, Z3_params a3) {
|
||||||
R();
|
R();
|
||||||
|
|
@ -2932,38 +2938,38 @@ void log_Z3_tactic_apply_ex(Z3_context a0, Z3_tactic a1, Z3_goal a2, Z3_params a
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
P(a3);
|
P(a3);
|
||||||
C(416);
|
C(417);
|
||||||
}
|
}
|
||||||
void log_Z3_apply_result_inc_ref(Z3_context a0, Z3_apply_result a1) {
|
void log_Z3_apply_result_inc_ref(Z3_context a0, Z3_apply_result a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(417);
|
C(418);
|
||||||
}
|
}
|
||||||
void log_Z3_apply_result_dec_ref(Z3_context a0, Z3_apply_result a1) {
|
void log_Z3_apply_result_dec_ref(Z3_context a0, Z3_apply_result a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(418);
|
C(419);
|
||||||
}
|
}
|
||||||
void log_Z3_apply_result_to_string(Z3_context a0, Z3_apply_result a1) {
|
void log_Z3_apply_result_to_string(Z3_context a0, Z3_apply_result a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(419);
|
C(420);
|
||||||
}
|
}
|
||||||
void log_Z3_apply_result_get_num_subgoals(Z3_context a0, Z3_apply_result a1) {
|
void log_Z3_apply_result_get_num_subgoals(Z3_context a0, Z3_apply_result a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(420);
|
C(421);
|
||||||
}
|
}
|
||||||
void log_Z3_apply_result_get_subgoal(Z3_context a0, Z3_apply_result a1, unsigned a2) {
|
void log_Z3_apply_result_get_subgoal(Z3_context a0, Z3_apply_result a1, unsigned a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
U(a2);
|
U(a2);
|
||||||
C(421);
|
C(422);
|
||||||
}
|
}
|
||||||
void log_Z3_apply_result_convert_model(Z3_context a0, Z3_apply_result a1, unsigned a2, Z3_model a3) {
|
void log_Z3_apply_result_convert_model(Z3_context a0, Z3_apply_result a1, unsigned a2, Z3_model a3) {
|
||||||
R();
|
R();
|
||||||
|
|
@ -2971,104 +2977,104 @@ void log_Z3_apply_result_convert_model(Z3_context a0, Z3_apply_result a1, unsign
|
||||||
P(a1);
|
P(a1);
|
||||||
U(a2);
|
U(a2);
|
||||||
P(a3);
|
P(a3);
|
||||||
C(422);
|
C(423);
|
||||||
}
|
}
|
||||||
void log_Z3_mk_solver(Z3_context a0) {
|
void log_Z3_mk_solver(Z3_context a0) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
C(423);
|
C(424);
|
||||||
}
|
}
|
||||||
void log_Z3_mk_simple_solver(Z3_context a0) {
|
void log_Z3_mk_simple_solver(Z3_context a0) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
C(424);
|
C(425);
|
||||||
}
|
}
|
||||||
void log_Z3_mk_solver_for_logic(Z3_context a0, Z3_symbol a1) {
|
void log_Z3_mk_solver_for_logic(Z3_context a0, Z3_symbol a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
Sy(a1);
|
Sy(a1);
|
||||||
C(425);
|
C(426);
|
||||||
}
|
}
|
||||||
void log_Z3_mk_solver_from_tactic(Z3_context a0, Z3_tactic a1) {
|
void log_Z3_mk_solver_from_tactic(Z3_context a0, Z3_tactic a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(426);
|
C(427);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_get_help(Z3_context a0, Z3_solver a1) {
|
void log_Z3_solver_get_help(Z3_context a0, Z3_solver a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(427);
|
C(428);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_get_param_descrs(Z3_context a0, Z3_solver a1) {
|
void log_Z3_solver_get_param_descrs(Z3_context a0, Z3_solver a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(428);
|
C(429);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_set_params(Z3_context a0, Z3_solver a1, Z3_params a2) {
|
void log_Z3_solver_set_params(Z3_context a0, Z3_solver a1, Z3_params a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(429);
|
C(430);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_inc_ref(Z3_context a0, Z3_solver a1) {
|
void log_Z3_solver_inc_ref(Z3_context a0, Z3_solver a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(430);
|
C(431);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_dec_ref(Z3_context a0, Z3_solver a1) {
|
void log_Z3_solver_dec_ref(Z3_context a0, Z3_solver a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(431);
|
C(432);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_push(Z3_context a0, Z3_solver a1) {
|
void log_Z3_solver_push(Z3_context a0, Z3_solver a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(432);
|
C(433);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_pop(Z3_context a0, Z3_solver a1, unsigned a2) {
|
void log_Z3_solver_pop(Z3_context a0, Z3_solver a1, unsigned a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
U(a2);
|
U(a2);
|
||||||
C(433);
|
C(434);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_reset(Z3_context a0, Z3_solver a1) {
|
void log_Z3_solver_reset(Z3_context a0, Z3_solver a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(434);
|
C(435);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_get_num_scopes(Z3_context a0, Z3_solver a1) {
|
void log_Z3_solver_get_num_scopes(Z3_context a0, Z3_solver a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(435);
|
C(436);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_assert(Z3_context a0, Z3_solver a1, Z3_ast a2) {
|
void log_Z3_solver_assert(Z3_context a0, Z3_solver a1, Z3_ast a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(436);
|
C(437);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_get_assertions(Z3_context a0, Z3_solver a1) {
|
void log_Z3_solver_get_assertions(Z3_context a0, Z3_solver a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(437);
|
C(438);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_check(Z3_context a0, Z3_solver a1) {
|
void log_Z3_solver_check(Z3_context a0, Z3_solver a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(438);
|
C(439);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_check_assumptions(Z3_context a0, Z3_solver a1, unsigned a2, Z3_ast const * a3) {
|
void log_Z3_solver_check_assumptions(Z3_context a0, Z3_solver a1, unsigned a2, Z3_ast const * a3) {
|
||||||
R();
|
R();
|
||||||
|
|
@ -3077,132 +3083,132 @@ void log_Z3_solver_check_assumptions(Z3_context a0, Z3_solver a1, unsigned a2, Z
|
||||||
U(a2);
|
U(a2);
|
||||||
for (unsigned i = 0; i < a2; i++) { P(a3[i]); }
|
for (unsigned i = 0; i < a2; i++) { P(a3[i]); }
|
||||||
Ap(a2);
|
Ap(a2);
|
||||||
C(439);
|
C(440);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_get_model(Z3_context a0, Z3_solver a1) {
|
void log_Z3_solver_get_model(Z3_context a0, Z3_solver a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(440);
|
C(441);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_get_proof(Z3_context a0, Z3_solver a1) {
|
void log_Z3_solver_get_proof(Z3_context a0, Z3_solver a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(441);
|
C(442);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_get_unsat_core(Z3_context a0, Z3_solver a1) {
|
void log_Z3_solver_get_unsat_core(Z3_context a0, Z3_solver a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(442);
|
C(443);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_get_reason_unknown(Z3_context a0, Z3_solver a1) {
|
void log_Z3_solver_get_reason_unknown(Z3_context a0, Z3_solver a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(443);
|
C(444);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_get_statistics(Z3_context a0, Z3_solver a1) {
|
void log_Z3_solver_get_statistics(Z3_context a0, Z3_solver a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(444);
|
C(445);
|
||||||
}
|
}
|
||||||
void log_Z3_solver_to_string(Z3_context a0, Z3_solver a1) {
|
void log_Z3_solver_to_string(Z3_context a0, Z3_solver a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(445);
|
C(446);
|
||||||
}
|
}
|
||||||
void log_Z3_stats_to_string(Z3_context a0, Z3_stats a1) {
|
void log_Z3_stats_to_string(Z3_context a0, Z3_stats a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(446);
|
C(447);
|
||||||
}
|
}
|
||||||
void log_Z3_stats_inc_ref(Z3_context a0, Z3_stats a1) {
|
void log_Z3_stats_inc_ref(Z3_context a0, Z3_stats a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(447);
|
C(448);
|
||||||
}
|
}
|
||||||
void log_Z3_stats_dec_ref(Z3_context a0, Z3_stats a1) {
|
void log_Z3_stats_dec_ref(Z3_context a0, Z3_stats a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(448);
|
C(449);
|
||||||
}
|
}
|
||||||
void log_Z3_stats_size(Z3_context a0, Z3_stats a1) {
|
void log_Z3_stats_size(Z3_context a0, Z3_stats a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(449);
|
C(450);
|
||||||
}
|
}
|
||||||
void log_Z3_stats_get_key(Z3_context a0, Z3_stats a1, unsigned a2) {
|
void log_Z3_stats_get_key(Z3_context a0, Z3_stats a1, unsigned a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
U(a2);
|
U(a2);
|
||||||
C(450);
|
C(451);
|
||||||
}
|
}
|
||||||
void log_Z3_stats_is_uint(Z3_context a0, Z3_stats a1, unsigned a2) {
|
void log_Z3_stats_is_uint(Z3_context a0, Z3_stats a1, unsigned a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
U(a2);
|
U(a2);
|
||||||
C(451);
|
C(452);
|
||||||
}
|
}
|
||||||
void log_Z3_stats_is_double(Z3_context a0, Z3_stats a1, unsigned a2) {
|
void log_Z3_stats_is_double(Z3_context a0, Z3_stats a1, unsigned a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
U(a2);
|
U(a2);
|
||||||
C(452);
|
C(453);
|
||||||
}
|
}
|
||||||
void log_Z3_stats_get_uint_value(Z3_context a0, Z3_stats a1, unsigned a2) {
|
void log_Z3_stats_get_uint_value(Z3_context a0, Z3_stats a1, unsigned a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
U(a2);
|
U(a2);
|
||||||
C(453);
|
C(454);
|
||||||
}
|
}
|
||||||
void log_Z3_stats_get_double_value(Z3_context a0, Z3_stats a1, unsigned a2) {
|
void log_Z3_stats_get_double_value(Z3_context a0, Z3_stats a1, unsigned a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
U(a2);
|
U(a2);
|
||||||
C(454);
|
C(455);
|
||||||
}
|
}
|
||||||
void log_Z3_mk_ast_vector(Z3_context a0) {
|
void log_Z3_mk_ast_vector(Z3_context a0) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
C(455);
|
C(456);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_vector_inc_ref(Z3_context a0, Z3_ast_vector a1) {
|
void log_Z3_ast_vector_inc_ref(Z3_context a0, Z3_ast_vector a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(456);
|
C(457);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_vector_dec_ref(Z3_context a0, Z3_ast_vector a1) {
|
void log_Z3_ast_vector_dec_ref(Z3_context a0, Z3_ast_vector a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(457);
|
C(458);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_vector_size(Z3_context a0, Z3_ast_vector a1) {
|
void log_Z3_ast_vector_size(Z3_context a0, Z3_ast_vector a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(458);
|
C(459);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_vector_get(Z3_context a0, Z3_ast_vector a1, unsigned a2) {
|
void log_Z3_ast_vector_get(Z3_context a0, Z3_ast_vector a1, unsigned a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
U(a2);
|
U(a2);
|
||||||
C(459);
|
C(460);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_vector_set(Z3_context a0, Z3_ast_vector a1, unsigned a2, Z3_ast a3) {
|
void log_Z3_ast_vector_set(Z3_context a0, Z3_ast_vector a1, unsigned a2, Z3_ast a3) {
|
||||||
R();
|
R();
|
||||||
|
|
@ -3210,65 +3216,65 @@ void log_Z3_ast_vector_set(Z3_context a0, Z3_ast_vector a1, unsigned a2, Z3_ast
|
||||||
P(a1);
|
P(a1);
|
||||||
U(a2);
|
U(a2);
|
||||||
P(a3);
|
P(a3);
|
||||||
C(460);
|
C(461);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_vector_resize(Z3_context a0, Z3_ast_vector a1, unsigned a2) {
|
void log_Z3_ast_vector_resize(Z3_context a0, Z3_ast_vector a1, unsigned a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
U(a2);
|
U(a2);
|
||||||
C(461);
|
C(462);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_vector_push(Z3_context a0, Z3_ast_vector a1, Z3_ast a2) {
|
void log_Z3_ast_vector_push(Z3_context a0, Z3_ast_vector a1, Z3_ast a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(462);
|
C(463);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_vector_translate(Z3_context a0, Z3_ast_vector a1, Z3_context a2) {
|
void log_Z3_ast_vector_translate(Z3_context a0, Z3_ast_vector a1, Z3_context a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(463);
|
C(464);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_vector_to_string(Z3_context a0, Z3_ast_vector a1) {
|
void log_Z3_ast_vector_to_string(Z3_context a0, Z3_ast_vector a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(464);
|
C(465);
|
||||||
}
|
}
|
||||||
void log_Z3_mk_ast_map(Z3_context a0) {
|
void log_Z3_mk_ast_map(Z3_context a0) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
C(465);
|
C(466);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_map_inc_ref(Z3_context a0, Z3_ast_map a1) {
|
void log_Z3_ast_map_inc_ref(Z3_context a0, Z3_ast_map a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(466);
|
C(467);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_map_dec_ref(Z3_context a0, Z3_ast_map a1) {
|
void log_Z3_ast_map_dec_ref(Z3_context a0, Z3_ast_map a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(467);
|
C(468);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_map_contains(Z3_context a0, Z3_ast_map a1, Z3_ast a2) {
|
void log_Z3_ast_map_contains(Z3_context a0, Z3_ast_map a1, Z3_ast a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(468);
|
C(469);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_map_find(Z3_context a0, Z3_ast_map a1, Z3_ast a2) {
|
void log_Z3_ast_map_find(Z3_context a0, Z3_ast_map a1, Z3_ast a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(469);
|
C(470);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_map_insert(Z3_context a0, Z3_ast_map a1, Z3_ast a2, Z3_ast a3) {
|
void log_Z3_ast_map_insert(Z3_context a0, Z3_ast_map a1, Z3_ast a2, Z3_ast a3) {
|
||||||
R();
|
R();
|
||||||
|
|
@ -3276,36 +3282,36 @@ void log_Z3_ast_map_insert(Z3_context a0, Z3_ast_map a1, Z3_ast a2, Z3_ast a3) {
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
P(a3);
|
P(a3);
|
||||||
C(470);
|
C(471);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_map_erase(Z3_context a0, Z3_ast_map a1, Z3_ast a2) {
|
void log_Z3_ast_map_erase(Z3_context a0, Z3_ast_map a1, Z3_ast a2) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
P(a2);
|
P(a2);
|
||||||
C(471);
|
C(472);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_map_size(Z3_context a0, Z3_ast_map a1) {
|
void log_Z3_ast_map_size(Z3_context a0, Z3_ast_map a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(472);
|
C(473);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_map_reset(Z3_context a0, Z3_ast_map a1) {
|
void log_Z3_ast_map_reset(Z3_context a0, Z3_ast_map a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(473);
|
C(474);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_map_keys(Z3_context a0, Z3_ast_map a1) {
|
void log_Z3_ast_map_keys(Z3_context a0, Z3_ast_map a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(474);
|
C(475);
|
||||||
}
|
}
|
||||||
void log_Z3_ast_map_to_string(Z3_context a0, Z3_ast_map a1) {
|
void log_Z3_ast_map_to_string(Z3_context a0, Z3_ast_map a1) {
|
||||||
R();
|
R();
|
||||||
P(a0);
|
P(a0);
|
||||||
P(a1);
|
P(a1);
|
||||||
C(475);
|
C(476);
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -741,6 +741,8 @@ void log_Z3_param_descrs_size(Z3_context a0, Z3_param_descrs a1);
|
||||||
#define LOG_Z3_param_descrs_size(_ARG0, _ARG1) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_param_descrs_size(_ARG0, _ARG1); }
|
#define LOG_Z3_param_descrs_size(_ARG0, _ARG1) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_param_descrs_size(_ARG0, _ARG1); }
|
||||||
void log_Z3_param_descrs_get_name(Z3_context a0, Z3_param_descrs a1, unsigned a2);
|
void log_Z3_param_descrs_get_name(Z3_context a0, Z3_param_descrs a1, unsigned a2);
|
||||||
#define LOG_Z3_param_descrs_get_name(_ARG0, _ARG1, _ARG2) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_param_descrs_get_name(_ARG0, _ARG1, _ARG2); }
|
#define LOG_Z3_param_descrs_get_name(_ARG0, _ARG1, _ARG2) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_param_descrs_get_name(_ARG0, _ARG1, _ARG2); }
|
||||||
|
void log_Z3_param_descrs_to_string(Z3_context a0, Z3_param_descrs a1);
|
||||||
|
#define LOG_Z3_param_descrs_to_string(_ARG0, _ARG1) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_param_descrs_to_string(_ARG0, _ARG1); }
|
||||||
void log_Z3_interrupt(Z3_context a0);
|
void log_Z3_interrupt(Z3_context a0);
|
||||||
#define LOG_Z3_interrupt(_ARG0) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_interrupt(_ARG0); }
|
#define LOG_Z3_interrupt(_ARG0) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_interrupt(_ARG0); }
|
||||||
void log_Z3_get_error_msg_ex(Z3_context a0, Z3_error_code a1);
|
void log_Z3_get_error_msg_ex(Z3_context a0, Z3_error_code a1);
|
||||||
|
|
|
||||||
|
|
@ -179,4 +179,21 @@ extern "C" {
|
||||||
Z3_CATCH_RETURN(0);
|
Z3_CATCH_RETURN(0);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p) {
|
||||||
|
Z3_TRY;
|
||||||
|
LOG_Z3_param_descrs_to_string(c, p);
|
||||||
|
RESET_ERROR_CODE();
|
||||||
|
std::ostringstream buffer;
|
||||||
|
buffer << "(";
|
||||||
|
unsigned sz = to_param_descrs_ptr(p)->size();
|
||||||
|
for (unsigned i = 0; i < sz; i++) {
|
||||||
|
if (i > 0)
|
||||||
|
buffer << ", ";
|
||||||
|
buffer << to_param_descrs_ptr(p)->get_param_name(i);
|
||||||
|
}
|
||||||
|
buffer << ")";
|
||||||
|
return mk_c(c)->mk_external_string(buffer.str());
|
||||||
|
Z3_CATCH_RETURN("");
|
||||||
|
}
|
||||||
|
|
||||||
};
|
};
|
||||||
|
|
|
||||||
|
|
@ -1456,6 +1456,12 @@ extern "C" {
|
||||||
*/
|
*/
|
||||||
Z3_symbol Z3_API Z3_param_descrs_get_name(__in Z3_context c, __in Z3_param_descrs p, __in unsigned i);
|
Z3_symbol Z3_API Z3_param_descrs_get_name(__in Z3_context c, __in Z3_param_descrs p, __in unsigned i);
|
||||||
|
|
||||||
|
/**
|
||||||
|
\brief Convert a parameter description set into a string. This function is mainly used for printing the
|
||||||
|
contents of a parameter description set.
|
||||||
|
*/
|
||||||
|
Z3_string Z3_API Z3_param_descrs_to_string(__in Z3_context c, __in Z3_param_descrs p);
|
||||||
|
|
||||||
/*@}*/
|
/*@}*/
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
|
|
|
||||||
13
python/z3.py
13
python/z3.py
|
|
@ -4421,18 +4421,7 @@ class ParamDescrsRef:
|
||||||
return self.get_kind(arg)
|
return self.get_kind(arg)
|
||||||
|
|
||||||
def __repr__(self):
|
def __repr__(self):
|
||||||
r = io.StringIO()
|
return Z3_param_descrs_to_string(self.ctx.ref(), self.descr)
|
||||||
first = True
|
|
||||||
r.write(u'(')
|
|
||||||
for i in range(self.size()):
|
|
||||||
if first:
|
|
||||||
first = False
|
|
||||||
else:
|
|
||||||
r.write(u' ')
|
|
||||||
r.write(u'%s' % self.get_name(i))
|
|
||||||
r.write(u')')
|
|
||||||
return r.getvalue()
|
|
||||||
|
|
||||||
|
|
||||||
#########################################
|
#########################################
|
||||||
#
|
#
|
||||||
|
|
|
||||||
|
|
@ -696,6 +696,8 @@ def init(PATH):
|
||||||
_lib.Z3_param_descrs_size.argtypes = [ContextObj, ParamDescrs]
|
_lib.Z3_param_descrs_size.argtypes = [ContextObj, ParamDescrs]
|
||||||
_lib.Z3_param_descrs_get_name.restype = Symbol
|
_lib.Z3_param_descrs_get_name.restype = Symbol
|
||||||
_lib.Z3_param_descrs_get_name.argtypes = [ContextObj, ParamDescrs, ctypes.c_uint]
|
_lib.Z3_param_descrs_get_name.argtypes = [ContextObj, ParamDescrs, ctypes.c_uint]
|
||||||
|
_lib.Z3_param_descrs_to_string.restype = ctypes.c_char_p
|
||||||
|
_lib.Z3_param_descrs_to_string.argtypes = [ContextObj, ParamDescrs]
|
||||||
_lib.Z3_interrupt.argtypes = [ContextObj]
|
_lib.Z3_interrupt.argtypes = [ContextObj]
|
||||||
_lib.Z3_get_error_msg_ex.restype = ctypes.c_char_p
|
_lib.Z3_get_error_msg_ex.restype = ctypes.c_char_p
|
||||||
_lib.Z3_get_error_msg_ex.argtypes = [ContextObj, ctypes.c_uint]
|
_lib.Z3_get_error_msg_ex.argtypes = [ContextObj, ctypes.c_uint]
|
||||||
|
|
@ -3341,6 +3343,13 @@ def Z3_param_descrs_get_name(a0, a1, a2):
|
||||||
raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
|
raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
|
||||||
return r
|
return r
|
||||||
|
|
||||||
|
def Z3_param_descrs_to_string(a0, a1):
|
||||||
|
r = lib().Z3_param_descrs_to_string(a0, a1)
|
||||||
|
err = lib().Z3_get_error_code(a0)
|
||||||
|
if err != Z3_OK:
|
||||||
|
raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
|
||||||
|
return r
|
||||||
|
|
||||||
def Z3_interrupt(a0):
|
def Z3_interrupt(a0):
|
||||||
lib().Z3_interrupt(a0)
|
lib().Z3_interrupt(a0)
|
||||||
err = lib().Z3_get_error_code(a0)
|
err = lib().Z3_get_error_code(a0)
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue