diff --git a/scripts/mk_make.py b/scripts/mk_make.py index a2ee92926..0d0891705 100644 --- a/scripts/mk_make.py +++ b/scripts/mk_make.py @@ -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() diff --git a/scripts/mk_util.py b/scripts/mk_util.py index bdf385031..9935413f3 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -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] diff --git a/src/api/dll/api_dll.def b/src/api/dll/api_dll.def deleted file mode 100644 index 8fc69bed1..000000000 --- a/src/api/dll/api_dll.def +++ /dev/null @@ -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