From cd4b53500c6e49e9f1de0259dd6ebab4a45946ff Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 8 Mar 2019 10:13:46 +0000 Subject: [PATCH] avoid a few str copies + symbol hiding --- src/api/api_config_params.cpp | 2 +- src/api/api_context.cpp | 12 ++---------- src/api/api_context.h | 2 +- src/api/api_goal.cpp | 4 ++-- src/api/api_model.cpp | 2 +- src/api/api_seq.cpp | 3 +-- src/api/api_stats.cpp | 2 +- src/ast/rewriter/pb2bv_rewriter.cpp | 2 +- src/shell/main.cpp | 14 +++++++------- src/util/gparams.cpp | 4 ++-- src/util/prime_generator.cpp | 2 +- src/util/scoped_ctrl_c.cpp | 4 ++-- src/util/scoped_ctrl_c.h | 2 -- 13 files changed, 22 insertions(+), 33 deletions(-) diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp index 60d5fa556..1682fb707 100644 --- a/src/api/api_config_params.cpp +++ b/src/api/api_config_params.cpp @@ -48,7 +48,7 @@ extern "C" { env_params::updt_params(); } - std::string g_Z3_global_param_get_buffer; + static std::string g_Z3_global_param_get_buffer; Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) { memory::initialize(UINT_MAX); diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index a2492cb1a..71bebef73 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -155,8 +155,6 @@ namespace api { m_error_code = Z3_OK; } - - void context::check_searching() { if (m_searching) { set_error_code(Z3_INVALID_USAGE, "cannot use function while searching"); // TBD: error code could be fixed. @@ -168,8 +166,8 @@ namespace api { return const_cast(m_string_buffer.c_str()); } - char * context::mk_external_string(std::string const & str) { - m_string_buffer = str; + char * context::mk_external_string(std::string && str) { + m_string_buffer = std::move(str); return const_cast(m_string_buffer.c_str()); } @@ -466,17 +464,11 @@ extern "C" { } } - Z3_API char const * Z3_get_error_msg(Z3_context c, Z3_error_code err) { LOG_Z3_get_error_msg(c, err); return _get_error_msg(c, err); } - Z3_API char const * Z3_get_error_msg_ex(Z3_context c, Z3_error_code err) { - return Z3_get_error_msg(c, err); - } - - void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode) { Z3_TRY; LOG_Z3_set_ast_print_mode(c, mode); diff --git a/src/api/api_context.h b/src/api/api_context.h index aacd4edd3..8bd75aaa0 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -179,7 +179,7 @@ namespace api { // Store a copy of str in m_string_buffer, and return a reference to it. // This method is used to communicate local/internal strings with the "external world" char * mk_external_string(char const * str); - char * mk_external_string(std::string const & str); + char * mk_external_string(std::string && str); // Create a numeral of the given sort expr * mk_numeral_core(rational const & n, sort * s); diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp index c70d241e0..04c2945a9 100644 --- a/src/api/api_goal.cpp +++ b/src/api/api_goal.cpp @@ -189,7 +189,7 @@ extern "C" { std::string result = buffer.str(); SASSERT(result.size() > 0); result.resize(result.size()-1); - return mk_c(c)->mk_external_string(result); + return mk_c(c)->mk_external_string(std::move(result)); Z3_CATCH_RETURN(""); } @@ -207,7 +207,7 @@ extern "C" { std::string result = buffer.str(); SASSERT(result.size() > 0); result.resize(result.size()-1); - return mk_c(c)->mk_external_string(result); + return mk_c(c)->mk_external_string(std::move(result)); Z3_CATCH_RETURN(""); } diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 8fba5e9f6..812d80b23 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -478,7 +478,7 @@ extern "C" { model_v2_pp(buffer, *(to_model_ref(m)), p.partial()); result = buffer.str(); } - return mk_c(c)->mk_external_string(result); + return mk_c(c)->mk_external_string(std::move(result)); Z3_CATCH_RETURN(nullptr); } diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 19e298ee8..17264ad77 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -106,8 +106,7 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG, "expression is not a string literal"); return ""; } - std::string s = str.encode(); - return mk_c(c)->mk_external_string(s); + return mk_c(c)->mk_external_string(str.encode()); Z3_CATCH_RETURN(""); } diff --git a/src/api/api_stats.cpp b/src/api/api_stats.cpp index 3ff87039f..410118c9d 100644 --- a/src/api/api_stats.cpp +++ b/src/api/api_stats.cpp @@ -34,7 +34,7 @@ extern "C" { result = buffer.str(); SASSERT(result.size() > 0); result.resize(result.size()-1); - return mk_c(c)->mk_external_string(result); + return mk_c(c)->mk_external_string(std::move(result)); Z3_CATCH_RETURN(""); } diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 015372933..2a8681383 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -28,7 +28,7 @@ Notes: #include "util/uint_set.h" #include "util/gparams.h" -const unsigned g_primes[7] = { 2, 3, 5, 7, 11, 13, 17}; +static const unsigned g_primes[7] = { 2, 3, 5, 7, 11, 13, 17}; struct pb2bv_rewriter::imp { diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 260cf8a79..1d22ce9b6 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -41,14 +41,14 @@ Revision History: typedef enum { IN_UNSPECIFIED, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_LP, IN_Z3_LOG, IN_MPS } input_kind; -std::string g_aux_input_file; -char const * g_input_file = nullptr; -bool g_standard_input = false; -input_kind g_input_kind = IN_UNSPECIFIED; +static std::string g_aux_input_file; +static char const * g_input_file = nullptr; +static bool g_standard_input = false; +static input_kind g_input_kind = IN_UNSPECIFIED; bool g_display_statistics = false; -bool g_display_istatistics = false; +static bool g_display_istatistics = false; -void error(const char * msg) { +static void error(const char * msg) { std::cerr << "Error: " << msg << "\n"; std::cerr << "For usage information: z3 -h\n"; exit(ERR_CMD_LINE); @@ -114,7 +114,7 @@ void display_usage() { std::cout << "Use 'z3 -p' for the complete list of global and module parameters.\n"; } -void parse_cmd_line_args(int argc, char ** argv) { +static void parse_cmd_line_args(int argc, char ** argv) { long timeout = 0; int i = 1; char * eq_pos = nullptr; diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 6b5919f8e..ea9b3603c 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -25,7 +25,7 @@ extern void gparams_register_modules(); static char const * g_old_params_names[] = { "arith_adaptive","arith_adaptive_assertion_threshold","arith_adaptive_gcd","arith_adaptive_propagation_threshold","arith_add_binary_bounds","arith_blands_rule_threshold","arith_branch_cut_ratio","arith_dump_lemmas","arith_eager_eq_axioms","arith_eager_gcd","arith_eq_bounds","arith_euclidean_solver","arith_expand_eqs","arith_force_simplex","arith_gcd_test","arith_ignore_int","arith_lazy_adapter","arith_lazy_pivoting","arith_max_lemma_size","arith_process_all_eqs","arith_propagate_eqs","arith_propagation_mode","arith_propagation_threshold","arith_prop_strategy","arith_random_initial_value","arith_random_lower","arith_random_seed","arith_random_upper","arith_reflect","arith_skip_big_coeffs","arith_small_lemma_size","arith_solver","arith_stronger_lemmas","array_always_prop_upward","array_canonize","array_cg","array_delay_exp_axiom","array_extensional","array_laziness","array_lazy_ieq","array_lazy_ieq_delay","array_solver","array_weak","async_commands","at_labels_cex","auto_config","bb_eager","bb_ext_gates","bb_quantifiers","bin_clauses","bit2int","bv2int_distribute","bv_blast_max_size","bv_cc","bv_enable_int2bv_propagation","bv_lazy_le","bv_max_sharing","bv_reflect","bv_solver","case_split","check_at_labels","check_proof","cnf_factor","cnf_mode","context_simplifier","dack","dack_eq","dack_factor","dack_gc","dack_gc_inv_decay","dack_threshold","default_qid","default_table","default_table_checked","delay_units","delay_units_threshold","der","display_config","display_dot_proof","display_error_for_visual_studio","display_features","display_proof","display_unsat_core","distribute_forall","dt_lazy_splits","dump_goal_as_smt","elim_and","elim_bounds","elim_nlarith_quantifiers","elim_quantifiers","elim_term_ite","ematching","engine","eq_propagation","hi_div0","ignore_bad_patterns","ignore_setparameter","instruction_max","inst_gen","interactive","internalizer_nnf","lemma_gc_factor","lemma_gc_half","lemma_gc_initial","lemma_gc_new_clause_activity","lemma_gc_new_clause_relevancy","lemma_gc_new_old_ratio","lemma_gc_old_clause_activity","lemma_gc_old_clause_relevancy","lemma_gc_strategy","lift_ite","lookahead_diseq","macro_finder","max_conflicts","max_counterexamples","mbqi","mbqi_force_template","mbqi_max_cexs","mbqi_max_cexs_incr","mbqi_max_iterations","mbqi_trace","minimize_lemmas","model","model_compact","model_completion","model_display_arg_sort","model_hide_unused_partitions","model_on_final_check","model_on_timeout","model_partial","model_v1","model_v2","model_validate","new_core2th_eq","ng_lift_ite","nl_arith","nl_arith_branching","nl_arith_gb","nl_arith_gb_eqs","nl_arith_gb_perturbate","nl_arith_gb_threshold","nl_arith_max_degree","nl_arith_rounds","nnf_factor","nnf_ignore_labels","nnf_mode","nnf_sk_hack","order","order_var_weight","order_weights","phase_selection","pi_arith","pi_arith_weight","pi_avoid_skolems","pi_block_looop_patterns","pi_max_multi_patterns","pi_non_nested_arith_weight","pi_nopat_weight","pi_pull_quantifiers","pi_use_database","pi_warnings","pp_bounded","pp_bv_literals","pp_bv_neg","pp_decimal","pp_decimal_precision","pp_fixed_indent","pp_flat_assoc","pp_max_depth","pp_max_indent","pp_max_num_lines","pp_max_ribbon","pp_max_width","pp_min_alias_size","pp_simplify_implies","pp_single_line","precedence","precedence_gen","pre_demodulator","pre_simplifier","pre_simplify_expr","profile_res_sub","progress_sampling_freq","proof_mode","propagate_booleans","propagate_values","pull_cheap_ite_trees","pull_nested_quantifiers","qi_conservative_final_check","qi_cost","qi_eager_threshold","qi_lazy_instantiation","qi_lazy_quick_checker","qi_lazy_threshold","qi_max_eager_multi_patterns","qi_max_instances","qi_max_lazy_multi_pattern_matching","qi_new_gen","qi_profile","qi_profile_freq","qi_promote_unsat","qi_quick_checker","quasi_macros","random_case_split_freq","random_initial_activity","random_seed","recent_lemma_threshold","reduce_args","refine_inj_axiom","relevancy","relevancy_lemma","rel_case_split_order","restart_adaptive","restart_agility_threshold","restart_factor","restart_initial","restart_strategy","restricted_quasi_macros","simplify_clauses","smtlib2_compliant","smtlib_category","smtlib_dump_lemmas","smtlib_logic","smtlib_source_info","smtlib_trace_path","soft_timeout","solver","spc_bs","spc_es","spc_factor_subsumption_index_opt","spc_initial_subsumption_index_opt","spc_max_subsumption_index_features","spc_min_func_freq_subsumption_index","spc_num_iterations","spc_trace","statistics","strong_context_simplifier","tick","trace","trace_file_name","type_check","user_theory_persist_axioms","user_theory_preprocess_axioms","verbose","warning","well_sorted_check","z3_solver_ll_pp","z3_solver_smt_pp", nullptr }; -bool is_old_param_name(symbol const & name) { +static bool is_old_param_name(symbol const & name) { char const * const * it = g_old_params_names; while (*it) { if (name == *it) @@ -66,7 +66,7 @@ static char const * g_params_renames[] = { "pp_min_alias_size", "pp.min_alias_size", nullptr }; -char const * get_new_param_name(symbol const & p) { +static char const * get_new_param_name(symbol const & p) { char const * const * it = g_params_renames; while (*it) { if (p == *it) { diff --git a/src/util/prime_generator.cpp b/src/util/prime_generator.cpp index 6c0376e52..9d3936edf 100644 --- a/src/util/prime_generator.cpp +++ b/src/util/prime_generator.cpp @@ -96,7 +96,7 @@ uint64_t prime_generator::operator()(unsigned idx) { return m_primes[idx]; } -prime_generator g_prime_generator; +static prime_generator g_prime_generator; prime_iterator::prime_iterator(prime_generator * g):m_idx(0) { if (g == nullptr) { diff --git a/src/util/scoped_ctrl_c.cpp b/src/util/scoped_ctrl_c.cpp index 2dbbaec9b..e6214cfab 100644 --- a/src/util/scoped_ctrl_c.cpp +++ b/src/util/scoped_ctrl_c.cpp @@ -20,9 +20,9 @@ Revision History: #include #include "util/scoped_ctrl_c.h" -scoped_ctrl_c * scoped_ctrl_c::g_obj = nullptr; +static scoped_ctrl_c * g_obj = nullptr; -void scoped_ctrl_c::on_ctrl_c(int) { +static void on_ctrl_c(int) { if (g_obj->m_first) { g_obj->m_cancel_eh(CTRL_C_EH_CALLER); if (g_obj->m_once) { diff --git a/src/util/scoped_ctrl_c.h b/src/util/scoped_ctrl_c.h index b3abf0e26..654938bfc 100644 --- a/src/util/scoped_ctrl_c.h +++ b/src/util/scoped_ctrl_c.h @@ -29,8 +29,6 @@ struct scoped_ctrl_c { bool m_enabled; void (STD_CALL *m_old_handler)(int); scoped_ctrl_c * m_old_scoped_ctrl_c; - static scoped_ctrl_c * g_obj; - static void STD_CALL on_ctrl_c(int); public: // If once == true, then the cancel_eh is invoked only at the first Ctrl-C. // The next time, the old signal handler will take over.