From 5fa96ccb0b9f215e7fb4f7f5073675738ac11aa6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 18 Oct 2012 12:52:33 -0700 Subject: [PATCH] Renamed z3_dbg.dll to z3.dll Signed-off-by: Leonardo de Moura --- dll/dll.vcxproj | 15 +- dll/z3_dbg.def | 528 ------------------------------------------------ update_api.py | 8 +- 3 files changed, 8 insertions(+), 543 deletions(-) delete mode 100644 dll/z3_dbg.def diff --git a/dll/dll.vcxproj b/dll/dll.vcxproj index a38f94287..0b49c1479 100644 --- a/dll/dll.vcxproj +++ b/dll/dll.vcxproj @@ -1,4 +1,4 @@ - + @@ -264,8 +264,8 @@ AllRules.ruleset - z3_dbg - z3_dbg + z3 + z3 z3 z3 z3 @@ -292,8 +292,8 @@ EditAndContinue - $(OutDir)z3_dbg.dll - z3_dbg.def + $(OutDir)z3.dll + z3.def true $(TargetDir)z3_dll.pdb Windows @@ -319,8 +319,8 @@ ProgramDatabase - $(OutDir)z3_dbg.dll - z3_dbg.def + $(OutDir)z3.dll + z3.def true $(TargetDir)z3_dll.pdb Windows @@ -610,7 +610,6 @@ - diff --git a/dll/z3_dbg.def b/dll/z3_dbg.def deleted file mode 100644 index 3965675a7..000000000 --- a/dll/z3_dbg.def +++ /dev/null @@ -1,528 +0,0 @@ -LIBRARY "Z3_DBG" -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 diff --git a/update_api.py b/update_api.py index e22cd3c5f..82afb7cdb 100644 --- a/update_api.py +++ b/update_api.py @@ -200,9 +200,7 @@ def mk_z3tactics_py(): def mk_dll_defs(): pat1 = re.compile(".*Z3_API.*") z3def = open('dll%sz3.def' % os.sep, 'w') - z3dbgdef = open('dll%sz3_dbg.def' % os.sep, 'w') z3def.write('LIBRARY "Z3"\nEXPORTS\n') - z3dbgdef.write('LIBRARY "Z3_DBG"\nEXPORTS\n') num = 1 for api_file in API_FILES: api = open(api_file, 'r') @@ -215,7 +213,6 @@ def mk_dll_defs(): if w == 'Z3_API': f = words[i+1] z3def.write('\t%s @%s\n' % (f, num)) - z3dbgdef.write('\t%s @%s\n' % (f, num)) i = i + 1 num = num + 1 @@ -512,11 +509,8 @@ def mk_dotnet(): dotnet.write(' public delegate void Z3_error_handler(Z3_context c, Z3_error_code e);\n\n') dotnet.write(' public unsafe class LIB\n') dotnet.write(' {\n') - dotnet.write(' #if DEBUG\n' - ' const string Z3_DLL_NAME = \"z3_dbg.dll\";\n' - ' #else\n' ' const string Z3_DLL_NAME = \"z3.dll\";\n' - ' #endif\n\n'); + ' \n'); dotnet.write(' [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n') dotnet.write(' public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);\n\n') for name, result, params in _dotnet_decls: