mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 18:45:33 +00:00
Code Activity

auto gen .def files

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-25 16:50:46 -07:00
parent 8ea3d3c7af
commit 67fe86ca18
3 changed files with 44 additions and 534 deletions
Download patch file Download diff file Expand all files Collapse all files

4
scripts/mk_make.py
View file

@ -62,14 +62,12 @@ add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig', 'muz_qe',
add_lib('api', ['portfolio', 'user_plugin'])
add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
add_exe('test', ['api', 'fuzzing'], exe_name='test-z3')
add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', dll_name='z3')
add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', dll_name='z3', export_files=['z3_api.h', 'z3_poly.h'])
add_dot_net_dll('dotnet', ['api_dll'], 'bindings/dotnet/Microsoft.Z3', dll_name='Microsoft.Z3', assembly_info_dir='Properties')
add_dot_net_dll('dotnetV3', ['api_dll'], 'bindings/dotnet/Microsoft.Z3V3', dll_name='Microsoft.Z3V3')
mk_auto_src()
update_version(4, 2, 0, 0)
#
mk_makefile()

46
scripts/mk_util.py
View file

@ -237,6 +237,10 @@ class Component:
# Return true if the component needs builder to generate an install_tactics.cpp file
def require_install_tactics(self):
return False
# Return true if the component needs a def file
def require_def_file(self):
return False
class LibComponent(Component):
def __init__(self, name, path, deps):
@ -317,11 +321,12 @@ class ExeComponent(Component):
return True
class DLLComponent(Component):
def __init__(self, name, dll_name, path, deps):
def __init__(self, name, dll_name, path, deps, export_files):
Component.__init__(self, name, path, deps)
if dll_name == None:
dll_name = name
self.dll_name = dll_name
self.export_files = export_files
def mk_makefile(self, out):
global _Name2Component
@ -364,6 +369,9 @@ class DLLComponent(Component):
def require_install_tactics(self):
return ('tactic' in self.deps) and ('cmd_context' in self.deps)
def require_def_file(self):
return IS_WINDOW and self.export_files
class DotNetDLLComponent(Component):
def __init__(self, name, dll_name, path, deps, assembly_info_dir):
Component.__init__(self, name, path, deps)
@ -405,8 +413,8 @@ def add_exe(name, deps=[], path=None, exe_name=None):
c = ExeComponent(name, exe_name, path, deps)
reg_component(name, c)
def add_dll(name, deps=[], path=None, dll_name=None):
c = DLLComponent(name, dll_name, path, deps)
def add_dll(name, deps=[], path=None, dll_name=None, export_files=[]):
c = DLLComponent(name, dll_name, path, deps, export_files)
reg_component(name, c)
def add_dot_net_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=None):
@ -484,6 +492,7 @@ def update_version(major, minor, build, revision):
if not ONLY_MAKEFILES:
mk_version_dot_h(major, minor, build, revision)
update_all_assembly_infos(major, minor, build, revision)
mk_def_files()
# Update files with the version number
def mk_version_dot_h(major, minor, build, revision):
@ -571,6 +580,7 @@ def ADD_PROBE(name, descr, cmd):
def mk_install_tactic_cpp(cnames, path):
global ADD_TACTIC_DATA, ADD_PROBE_DATA
ADD_TACTIC_DATA = []
ADD_PROBE_DATA = []
fullname = '%s/install_tactic.cpp' % path
fout = open(fullname, 'w')
fout.write('// Automatically generated file.\n')
@ -629,5 +639,35 @@ def mk_all_install_tactic_cpps():
cnames.append(c.name)
mk_install_tactic_cpp(cnames, c.src_dir)
# Generate a .def based on the files at c.export_files slot.
def mk_def_file(c):
pat1 = re.compile(".*Z3_API.*")
defname = '%s/%s.def' % (c.src_dir, c.name)
fout = open(defname, 'w')
fout.write('LIBRARY "%s"\nEXPORTS\n' % c.dll_name)
num = 1
for dot_h in c.export_files:
dot_h_c = c.find_file(dot_h, c.name)
api = open('%s/%s' % (dot_h_c.src_dir, dot_h), 'r')
for line in api:
m = pat1.match(line)
if m:
words = re.split('\W+', line)
i = 0
for w in words:
if w == 'Z3_API':
f = words[i+1]
fout.write('\t%s @%s\n' % (f, num))
i = i + 1
num = num + 1
if VERBOSE:
print "Generated '%s'" % defname
def mk_def_files():
if not ONLY_MAKEFILES:
for c in _Components:
if c.require_def_file():
mk_def_file(c)
def get_component(name):
return _Name2Component[name]

528
src/api/dll/api_dll.def
View file

@ -1,528 +0,0 @@
LIBRARY "Z3"
EXPORTS
Z3_mk_config @3
Z3_del_config @4
Z3_set_param_value @5
Z3_mk_context @6
Z3_mk_context_rc @7
Z3_del_context @8
Z3_inc_ref @9
Z3_dec_ref @10
Z3_update_param_value @11
Z3_get_param_value @12
Z3_interrupt @13
Z3_mk_params @14
Z3_params_inc_ref @15
Z3_params_dec_ref @16
Z3_params_set_bool @17
Z3_params_set_uint @18
Z3_params_set_double @19
Z3_params_set_symbol @20
Z3_params_to_string @21
Z3_params_validate @22
Z3_param_descrs_inc_ref @23
Z3_param_descrs_dec_ref @24
Z3_param_descrs_get_kind @25
Z3_param_descrs_size @26
Z3_param_descrs_get_name @27
Z3_param_descrs_to_string @28
Z3_mk_int_symbol @29
Z3_mk_string_symbol @30
Z3_mk_uninterpreted_sort @31
Z3_mk_bool_sort @32
Z3_mk_int_sort @33
Z3_mk_real_sort @34
Z3_mk_bv_sort @35
Z3_mk_finite_domain_sort @36
Z3_mk_array_sort @37
Z3_mk_tuple_sort @38
Z3_mk_enumeration_sort @39
Z3_mk_list_sort @40
Z3_mk_constructor @41
Z3_del_constructor @42
Z3_mk_datatype @43
Z3_mk_constructor_list @44
Z3_del_constructor_list @45
Z3_mk_datatypes @46
Z3_query_constructor @47
Z3_mk_func_decl @48
Z3_mk_app @49
Z3_mk_const @50
Z3_mk_fresh_func_decl @51
Z3_mk_fresh_const @52
Z3_mk_true @53
Z3_mk_false @54
Z3_mk_eq @55
Z3_mk_distinct @56
Z3_mk_not @57
Z3_mk_ite @58
Z3_mk_iff @59
Z3_mk_implies @60
Z3_mk_xor @61
Z3_mk_and @62
Z3_mk_or @63
Z3_mk_add @64
Z3_mk_mul @65
Z3_mk_sub @66
Z3_mk_unary_minus @67
Z3_mk_div @68
Z3_mk_mod @69
Z3_mk_rem @70
Z3_mk_power @71
Z3_mk_lt @72
Z3_mk_le @73
Z3_mk_gt @74
Z3_mk_ge @75
Z3_mk_int2real @76
Z3_mk_real2int @77
Z3_mk_is_int @78
Z3_mk_bvnot @79
Z3_mk_bvredand @80
Z3_mk_bvredor @81
Z3_mk_bvand @82
Z3_mk_bvor @83
Z3_mk_bvxor @84
Z3_mk_bvnand @85
Z3_mk_bvnor @86
Z3_mk_bvxnor @87
Z3_mk_bvneg @88
Z3_mk_bvadd @89
Z3_mk_bvsub @90
Z3_mk_bvmul @91
Z3_mk_bvudiv @92
Z3_mk_bvsdiv @93
Z3_mk_bvurem @94
Z3_mk_bvsrem @95
Z3_mk_bvsmod @96
Z3_mk_bvult @97
Z3_mk_bvslt @98
Z3_mk_bvule @99
Z3_mk_bvsle @100
Z3_mk_bvuge @101
Z3_mk_bvsge @102
Z3_mk_bvugt @103
Z3_mk_bvsgt @104
Z3_mk_concat @105
Z3_mk_extract @106
Z3_mk_sign_ext @107
Z3_mk_zero_ext @108
Z3_mk_repeat @109
Z3_mk_bvshl @110
Z3_mk_bvlshr @111
Z3_mk_bvashr @112
Z3_mk_rotate_left @113
Z3_mk_rotate_right @114
Z3_mk_ext_rotate_left @115
Z3_mk_ext_rotate_right @116
Z3_mk_int2bv @117
Z3_mk_bv2int @118
Z3_mk_bvadd_no_overflow @119
Z3_mk_bvadd_no_underflow @120
Z3_mk_bvsub_no_overflow @121
Z3_mk_bvsub_no_underflow @122
Z3_mk_bvsdiv_no_overflow @123
Z3_mk_bvneg_no_overflow @124
Z3_mk_bvmul_no_overflow @125
Z3_mk_bvmul_no_underflow @126
Z3_mk_select @127
Z3_mk_store @128
Z3_mk_const_array @129
Z3_mk_map @130
Z3_mk_array_default @131
Z3_mk_set_sort @132
Z3_mk_empty_set @133
Z3_mk_full_set @134
Z3_mk_set_add @135
Z3_mk_set_del @136
Z3_mk_set_union @137
Z3_mk_set_intersect @138
Z3_mk_set_difference @139
Z3_mk_set_complement @140
Z3_mk_set_member @141
Z3_mk_set_subset @142
Z3_mk_numeral @143
Z3_mk_real @144
Z3_mk_int @145
Z3_mk_unsigned_int @146
Z3_mk_int64 @147
Z3_mk_unsigned_int64 @148
Z3_mk_pattern @149
Z3_mk_bound @150
Z3_mk_forall @151
Z3_mk_exists @152
Z3_mk_quantifier @153
Z3_mk_quantifier_ex @154
Z3_mk_forall_const @155
Z3_mk_exists_const @156
Z3_mk_quantifier_const @157
Z3_mk_quantifier_const_ex @158
Z3_get_symbol_kind @159
Z3_get_symbol_int @160
Z3_get_symbol_string @161
Z3_get_sort_name @162
Z3_get_sort_id @163
Z3_sort_to_ast @164
Z3_is_eq_sort @165
Z3_get_sort_kind @166
Z3_get_bv_sort_size @167
Z3_get_finite_domain_sort_size @168
Z3_get_array_sort_domain @169
Z3_get_array_sort_range @170
Z3_get_tuple_sort_mk_decl @171
Z3_get_tuple_sort_num_fields @172
Z3_get_tuple_sort_field_decl @173
Z3_get_datatype_sort_num_constructors @174
Z3_get_datatype_sort_constructor @175
Z3_get_datatype_sort_recognizer @176
Z3_get_datatype_sort_constructor_accessor @177
Z3_get_relation_arity @178
Z3_get_relation_column @179
Z3_func_decl_to_ast @180
Z3_is_eq_func_decl @181
Z3_get_func_decl_id @182
Z3_get_decl_name @183
Z3_get_decl_kind @184
Z3_get_domain_size @185
Z3_get_arity @186
Z3_get_domain @187
Z3_get_range @188
Z3_get_decl_num_parameters @189
Z3_get_decl_parameter_kind @190
Z3_get_decl_int_parameter @191
Z3_get_decl_double_parameter @192
Z3_get_decl_symbol_parameter @193
Z3_get_decl_sort_parameter @194
Z3_get_decl_ast_parameter @195
Z3_get_decl_func_decl_parameter @196
Z3_get_decl_rational_parameter @197
Z3_app_to_ast @198
Z3_get_app_decl @199
Z3_get_app_num_args @200
Z3_get_app_arg @201
Z3_is_eq_ast @202
Z3_get_ast_id @203
Z3_get_ast_hash @204
Z3_get_sort @205
Z3_is_well_sorted @206
Z3_get_bool_value @207
Z3_get_ast_kind @208
Z3_is_app @209
Z3_is_numeral_ast @210
Z3_is_algebraic_number @211
Z3_to_app @212
Z3_to_func_decl @213
Z3_get_numeral_string @214
Z3_get_numeral_decimal_string @215
Z3_get_numerator @216
Z3_get_denominator @217
Z3_get_numeral_small @218
Z3_get_numeral_int @219
Z3_get_numeral_uint @220
Z3_get_numeral_uint64 @221
Z3_get_numeral_int64 @222
Z3_get_numeral_rational_int64 @223
Z3_get_algebraic_number_lower @224
Z3_get_algebraic_number_upper @225
Z3_pattern_to_ast @226
Z3_get_pattern_num_terms @227
Z3_get_pattern @228
Z3_get_index_value @229
Z3_is_quantifier_forall @230
Z3_get_quantifier_weight @231
Z3_get_quantifier_num_patterns @232
Z3_get_quantifier_pattern_ast @233
Z3_get_quantifier_num_no_patterns @234
Z3_get_quantifier_no_pattern_ast @235
Z3_get_quantifier_num_bound @236
Z3_get_quantifier_bound_name @237
Z3_get_quantifier_bound_sort @238
Z3_get_quantifier_body @239
Z3_simplify @240
Z3_simplify_ex @241
Z3_simplify_get_help @242
Z3_simplify_get_param_descrs @243
Z3_update_term @244
Z3_substitute @245
Z3_substitute_vars @246
Z3_translate @247
Z3_model_inc_ref @248
Z3_model_dec_ref @249
Z3_model_eval @250
Z3_model_get_const_interp @251
Z3_model_get_func_interp @252
Z3_model_get_num_consts @253
Z3_model_get_const_decl @254
Z3_model_get_num_funcs @255
Z3_model_get_func_decl @256
Z3_model_get_num_sorts @257
Z3_model_get_sort @258
Z3_model_get_sort_universe @259
Z3_is_as_array @260
Z3_get_as_array_func_decl @261
Z3_func_interp_inc_ref @262
Z3_func_interp_dec_ref @263
Z3_func_interp_get_num_entries @264
Z3_func_interp_get_entry @265
Z3_func_interp_get_else @266
Z3_func_interp_get_arity @267
Z3_func_entry_inc_ref @268
Z3_func_entry_dec_ref @269
Z3_func_entry_get_value @270
Z3_func_entry_get_num_args @271
Z3_func_entry_get_arg @272
Z3_open_log @273
Z3_append_log @274
Z3_close_log @275
Z3_toggle_warning_messages @276
Z3_set_ast_print_mode @277
Z3_ast_to_string @278
Z3_pattern_to_string @279
Z3_sort_to_string @280
Z3_func_decl_to_string @281
Z3_model_to_string @282
Z3_benchmark_to_smtlib_string @283
Z3_parse_smtlib2_string @284
Z3_parse_smtlib2_file @285
Z3_parse_smtlib_string @286
Z3_parse_smtlib_file @287
Z3_get_smtlib_num_formulas @288
Z3_get_smtlib_formula @289
Z3_get_smtlib_num_assumptions @290
Z3_get_smtlib_assumption @291
Z3_get_smtlib_num_decls @292
Z3_get_smtlib_decl @293
Z3_get_smtlib_num_sorts @294
Z3_get_smtlib_sort @295
Z3_get_smtlib_error @296
Z3_parse_z3_string @297
Z3_parse_z3_file @298
Z3_get_error_code @299
Z3_set_error_handler @300
Z3_set_error @301
Z3_get_error_msg @302
Z3_get_error_msg_ex @303
Z3_get_version @304
Z3_reset_memory @305
Z3_mk_theory @306
Z3_theory_get_ext_data @307
Z3_theory_mk_sort @308
Z3_theory_mk_value @309
Z3_theory_mk_constant @310
Z3_theory_mk_func_decl @311
Z3_theory_get_context @312
Z3_set_delete_callback @313
Z3_set_reduce_app_callback @314
Z3_set_reduce_eq_callback @315
Z3_set_reduce_distinct_callback @316
Z3_set_new_app_callback @317
Z3_set_new_elem_callback @318
Z3_set_init_search_callback @319
Z3_set_push_callback @320
Z3_set_pop_callback @321
Z3_set_restart_callback @322
Z3_set_reset_callback @323
Z3_set_final_check_callback @324
Z3_set_new_eq_callback @325
Z3_set_new_diseq_callback @326
Z3_set_new_assignment_callback @327
Z3_set_new_relevant_callback @328
Z3_theory_assert_axiom @329
Z3_theory_assume_eq @330
Z3_theory_enable_axiom_simplification @331
Z3_theory_get_eqc_root @332
Z3_theory_get_eqc_next @333
Z3_theory_get_num_parents @334
Z3_theory_get_parent @335
Z3_theory_is_value @336
Z3_theory_is_decl @337
Z3_theory_get_num_elems @338
Z3_theory_get_elem @339
Z3_theory_get_num_apps @340
Z3_theory_get_app @341
Z3_mk_fixedpoint @342
Z3_fixedpoint_inc_ref @343
Z3_fixedpoint_dec_ref @344
Z3_fixedpoint_add_rule @345
Z3_fixedpoint_add_fact @346
Z3_fixedpoint_assert @347
Z3_fixedpoint_query @348
Z3_fixedpoint_query_relations @349
Z3_fixedpoint_get_answer @350
Z3_fixedpoint_get_reason_unknown @351
Z3_fixedpoint_update_rule @352
Z3_fixedpoint_get_num_levels @353
Z3_fixedpoint_get_cover_delta @354
Z3_fixedpoint_add_cover @355
Z3_fixedpoint_get_statistics @356
Z3_fixedpoint_register_relation @357
Z3_fixedpoint_set_predicate_representation @358
Z3_fixedpoint_simplify_rules @359
Z3_fixedpoint_set_params @360
Z3_fixedpoint_get_help @361
Z3_fixedpoint_get_param_descrs @362
Z3_fixedpoint_to_string @363
Z3_fixedpoint_push @364
Z3_fixedpoint_pop @365
Z3_fixedpoint_init @366
Z3_fixedpoint_set_reduce_assign_callback @367
Z3_fixedpoint_set_reduce_app_callback @368
Z3_mk_ast_vector @369
Z3_ast_vector_inc_ref @370
Z3_ast_vector_dec_ref @371
Z3_ast_vector_size @372
Z3_ast_vector_get @373
Z3_ast_vector_set @374
Z3_ast_vector_resize @375
Z3_ast_vector_push @376
Z3_ast_vector_translate @377
Z3_ast_vector_to_string @378
Z3_mk_ast_map @379
Z3_ast_map_inc_ref @380
Z3_ast_map_dec_ref @381
Z3_ast_map_contains @382
Z3_ast_map_find @383
Z3_ast_map_insert @384
Z3_ast_map_erase @385
Z3_ast_map_reset @386
Z3_ast_map_size @387
Z3_ast_map_keys @388
Z3_ast_map_to_string @389
Z3_mk_goal @390
Z3_goal_inc_ref @391
Z3_goal_dec_ref @392
Z3_goal_precision @393
Z3_goal_assert @394
Z3_goal_inconsistent @395
Z3_goal_depth @396
Z3_goal_reset @397
Z3_goal_size @398
Z3_goal_formula @399
Z3_goal_num_exprs @400
Z3_goal_is_decided_sat @401
Z3_goal_is_decided_unsat @402
Z3_goal_translate @403
Z3_goal_to_string @404
Z3_mk_tactic @405
Z3_tactic_inc_ref @406
Z3_tactic_dec_ref @407
Z3_mk_probe @408
Z3_probe_inc_ref @409
Z3_probe_dec_ref @410
Z3_tactic_and_then @411
Z3_tactic_or_else @412
Z3_tactic_par_or @413
Z3_tactic_par_and_then @414
Z3_tactic_try_for @415
Z3_tactic_when @416
Z3_tactic_cond @417
Z3_tactic_repeat @418
Z3_tactic_skip @419
Z3_tactic_fail @420
Z3_tactic_fail_if @421
Z3_tactic_fail_if_not_decided @422
Z3_tactic_using_params @423
Z3_probe_const @424
Z3_probe_lt @425
Z3_probe_gt @426
Z3_probe_le @427
Z3_probe_ge @428
Z3_probe_eq @429
Z3_probe_and @430
Z3_probe_or @431
Z3_probe_not @432
Z3_get_num_tactics @433
Z3_get_tactic_name @434
Z3_get_num_probes @435
Z3_get_probe_name @436
Z3_tactic_get_help @437
Z3_tactic_get_param_descrs @438
Z3_tactic_get_descr @439
Z3_probe_get_descr @440
Z3_probe_apply @441
Z3_tactic_apply @442
Z3_tactic_apply_ex @443
Z3_apply_result_inc_ref @444
Z3_apply_result_dec_ref @445
Z3_apply_result_to_string @446
Z3_apply_result_get_num_subgoals @447
Z3_apply_result_get_subgoal @448
Z3_apply_result_convert_model @449
Z3_mk_solver @450
Z3_mk_simple_solver @451
Z3_mk_solver_for_logic @452
Z3_mk_solver_from_tactic @453
Z3_solver_get_help @454
Z3_solver_get_param_descrs @455
Z3_solver_set_params @456
Z3_solver_inc_ref @457
Z3_solver_dec_ref @458
Z3_solver_push @459
Z3_solver_pop @460
Z3_solver_reset @461
Z3_solver_get_num_scopes @462
Z3_solver_assert @463
Z3_solver_get_assertions @464
Z3_solver_check @465
Z3_solver_check_assumptions @466
Z3_solver_get_model @467
Z3_solver_get_proof @468
Z3_solver_get_unsat_core @469
Z3_solver_get_reason_unknown @470
Z3_solver_get_statistics @471
Z3_solver_to_string @472
Z3_stats_to_string @473
Z3_stats_inc_ref @474
Z3_stats_dec_ref @475
Z3_stats_size @476
Z3_stats_get_key @477
Z3_stats_is_uint @478
Z3_stats_is_double @479
Z3_stats_get_uint_value @480
Z3_stats_get_double_value @481
Z3_mk_injective_function @482
Z3_set_logic @483
Z3_push @484
Z3_pop @485
Z3_get_num_scopes @486
Z3_persist_ast @487
Z3_assert_cnstr @488
Z3_check_and_get_model @489
Z3_check @490
Z3_check_assumptions @491
Z3_get_implied_equalities @492
Z3_del_model @493
Z3_soft_check_cancel @494
Z3_get_search_failure @495
Z3_mk_label @496
Z3_get_relevant_labels @497
Z3_get_relevant_literals @498
Z3_get_guessed_literals @499
Z3_del_literals @500
Z3_get_num_literals @501
Z3_get_label_symbol @502
Z3_get_literal @503
Z3_disable_literal @504
Z3_block_literals @505
Z3_get_model_num_constants @506
Z3_get_model_constant @507
Z3_get_model_num_funcs @508
Z3_get_model_func_decl @509
Z3_eval_func_decl @510
Z3_is_array_value @511
Z3_get_array_value @512
Z3_get_model_func_else @513
Z3_get_model_func_num_entries @514
Z3_get_model_func_entry_num_args @515
Z3_get_model_func_entry_arg @516
Z3_get_model_func_entry_value @517
Z3_eval @518
Z3_eval_decl @519
Z3_context_to_string @520
Z3_statistics_to_string @521
Z3_get_context_assignment @522
Z3_mk_polynomial_manager @523
Z3_del_polynomial_manager @524
Z3_mk_zero_polynomial @525
Z3_polynomial_inc_ref @526
Z3_polynomial_dec_ref @527
Z3_polynomial_to_string @528