mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-14 04:41:48 +00:00
Code Activity

Eliminate unnecessary copy operations in function parameters and range-based loops (#8589)

Browse source
This commit is contained in:
Copilot 2026-02-11 21:14:32 +00:00 • committed by GitHub
parent f76c30b3bd
commit 20fef3f449
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
11 changed files with 34 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/lar_solver.cpp
View file

@ -1583,7 +1583,7 @@ namespace lp {
}
}
void lar_solver::set_variable_name(lpvar vi, std::string name) {
void lar_solver::set_variable_name(lpvar vi, const std::string& name) {
m_imp->m_var_register.set_name(vi, name);
}

2
src/math/lp/lar_solver.h
View file

@ -457,7 +457,7 @@ public:
void get_rid_of_inf_eps();
void get_model_do_not_care_about_diff_vars(std::unordered_map<lpvar, mpq>& variable_values) const;
std::string get_variable_name(lpvar vi) const override;
void set_variable_name(lpvar vi, std::string);
void set_variable_name(lpvar vi, const std::string&);
unsigned number_of_vars() const;
inline bool is_base(unsigned j) const { return get_core_solver().m_r_heading[j] >= 0; }
inline const impq& column_lower_bound(unsigned j) const {

2
src/math/lp/lp_settings.h
View file

@ -90,7 +90,7 @@ inline std::ostream& operator<<(std::ostream& out, lp_status status) {
return out << lp_status_to_string(status);
}
lp_status lp_status_from_string(std::string status);
lp_status lp_status_from_string(const std::string& status);
class lp_resource_limit {

2
src/math/lp/lp_settings_def.h
View file

@ -55,7 +55,7 @@ const char* lp_status_to_string(lp_status status) {
return "UNKNOWN"; // it is unreachable
}
lp_status lp_status_from_string(std::string status) {
lp_status lp_status_from_string(const std::string& status) {
if (status == "UNKNOWN") return lp_status::UNKNOWN;
if (status == "INFEASIBLE") return lp_status::INFEASIBLE;
if (status == "UNBOUNDED") return lp_status::UNBOUNDED;

6
src/math/lp/var_register.h
View file

@ -31,11 +31,11 @@ public:
ext_var_info() = default;
ext_var_info(unsigned j): ext_var_info(j, true) {}
ext_var_info(unsigned j , bool is_int) : m_external_j(j), m_is_integer(is_int) {}
ext_var_info(unsigned j , bool is_int, std::string name) : m_external_j(j), m_is_integer(is_int), m_name(name) {}
ext_var_info(unsigned j , bool is_int, const std::string& name) : m_external_j(j), m_is_integer(is_int), m_name(name) {}
unsigned external_j() const { return m_external_j;}
bool is_integer() const {return m_is_integer;}
void set_name(std::string name) { m_name = name; }
void set_name(const std::string& name) { m_name = name; }
std::string get_name() const { return m_name; }
};
@ -44,7 +44,7 @@ class var_register {
std::unordered_map<unsigned, unsigned> m_external_to_local;
public:
void set_name(unsigned j, std::string name) {
void set_name(unsigned j, const std::string& name) {
m_local_to_external[j].set_name(name);
}

4
src/nlsat/nlsat_solver.cpp
View file

@ -1193,11 +1193,11 @@ namespace nlsat {
m_ism.set_seed(saved_ism_seed);
}
void log_lemma(std::ostream& out, clause const& cls, std::string annotation) {
void log_lemma(std::ostream& out, clause const& cls, const std::string& annotation) {
log_lemma(out, cls.size(), cls.data(), true, annotation);
}
void log_lemma(std::ostream& out, unsigned n, literal const* cls, bool is_valid, std::string annotation) {
void log_lemma(std::ostream& out, unsigned n, literal const* cls, bool is_valid, const std::string& annotation) {
bool_vector used_vars(num_vars(), false);
bool_vector used_bools(usize(m_atoms), false);
var_vector vars;

14
src/sat/sat_bcd.cpp
View file

@ -46,9 +46,9 @@ namespace sat {
IF_VERBOSE(1, verbose_stream() << "Decomposed set " << f.m_L.size() << " rest: " << f.m_R.size() << "\n";);
TRACE(sat,
tout << "Decomposed set " << f.m_L.size() << "\n";
for (bclause b : f.m_L) tout << b.lit << ": " << *b.cls << "\n";
for (const bclause& b : f.m_L) tout << b.lit << ": " << *b.cls << "\n";
tout << "Remainder " << f.m_R.size() << "\n";
for (bclause b : f.m_R) tout << b.lit << ": " << *b.cls << "\n";);
for (const bclause& b : f.m_R) tout << b.lit << ": " << *b.cls << "\n";);
}
};
@ -66,7 +66,7 @@ namespace sat {
report _report(*this);
pure_decompose();
post_decompose();
for (bclause bc : m_L) {
for (const bclause& bc : m_L) {
if (bc.cls->size() == 2)
bins.push_back(bin_clause((*bc.cls)[0], (*bc.cls)[1]));
else
@ -83,7 +83,7 @@ namespace sat {
}
bin_clauses bc;
s.collect_bin_clauses(bc, false, false); // exclude roots.
for (auto b : bc) {
for (const auto& b : bc) {
literal lits[2] = { b.first, b.second };
clause* cls = s.cls_allocator().mk_clause(2, lits, false);
ul.insert(*cls);
@ -148,7 +148,7 @@ namespace sat {
m_marked.resize(2*s.num_vars(), false);
use_list ul;
ul.init(s.num_vars());
for (bclause bc : m_L) {
for (const bclause& bc : m_L) {
ul.insert(*bc.cls);
}
@ -201,7 +201,7 @@ namespace sat {
m_new_L.push_back(bclause(cls0[0], &cls0));
bool removed = false;
reset_removed();
for (bclause bc : m_L) {
for (const bclause& bc : m_L) {
literal lit = find_blocked(ul, *bc.cls);
if (lit == null_literal) {
live_clauses.push_back(bc);
@ -215,7 +215,7 @@ namespace sat {
while (removed) {
removed = false;
unsigned j = 0;
for (bclause bc : live_clauses) {
for (const bclause& bc : live_clauses) {
literal lit = find_blocked(ul, *bc.cls);
if (lit == null_literal) {
live_clauses[j++] = bc;

20
src/test/lp/argument_parser.h
View file

@ -42,19 +42,19 @@ public:
}
}
void add_option(std::string s) {
void add_option(const std::string& s) {
add_option_with_help_string(s, "");
}
void add_option_with_help_string(std::string s, std::string help_string) {
void add_option_with_help_string(const std::string& s, const std::string& help_string) {
m_options[s]=help_string;
}
void add_option_with_after_string(std::string s) {
void add_option_with_after_string(const std::string& s) {
add_option_with_after_string_with_help(s, "");
}
void add_option_with_after_string_with_help(std::string s, std::string help_string) {
void add_option_with_after_string_with_help(const std::string& s, const std::string& help_string) {
m_options_with_after_string[s]=help_string;
}
@ -82,19 +82,19 @@ public:
return status_is_ok;
}
bool contains(std::unordered_map<std::string, std::string> & m, std::string s) {
bool contains(std::unordered_map<std::string, std::string> & m, const std::string& s) {
return m.find(s) != m.end();
}
bool contains(std::set<std::string> & m, std::string s) {
bool contains(std::set<std::string> & m, const std::string& s) {
return m.find(s) != m.end();
}
bool option_is_used(std::string option) {
bool option_is_used(const std::string& option) {
return contains(m_used_options, option) || contains(m_used_options_with_after_string, option);
}
std::string get_option_value(std::string option) {
std::string get_option_value(const std::string& option) {
auto t = m_used_options_with_after_string.find(option);
if (t != m_used_options_with_after_string.end()){
return t->second;
@ -102,11 +102,11 @@ public:
return std::string();
}
bool starts_with(std::string s, char const * prefix) {
bool starts_with(const std::string& s, char const * prefix) {
return starts_with(s, std::string(prefix));
}
bool starts_with(std::string s, std::string prefix) {
bool starts_with(const std::string& s, const std::string& prefix) {
return s.substr(0, prefix.size()) == prefix;
}

8
src/test/lp/lp.cpp
View file

@ -684,11 +684,11 @@ std::string create_output_file_name(bool minimize, std::string file_name,
}
std::string create_output_file_name_for_glpsol(bool minimize,
std::string file_name) {
const std::string& file_name) {
return file_name + (minimize ? "_min" : "_max") + "_glpk_out";
}
int run_glpk(std::string file_name, std::string glpk_out_file_name,
int run_glpk(const std::string& file_name, const std::string& glpk_out_file_name,
bool minimize, unsigned time_limit) {
std::string minmax(minimize ? "--min" : "--max");
std::string tmlim = time_limit > 0 ? std::string(" --tmlim ") +
@ -700,7 +700,7 @@ int run_glpk(std::string file_name, std::string glpk_out_file_name,
return system(command_line.c_str());
}
std::string get_status(std::string file_name) {
std::string get_status(const std::string& file_name) {
std::ifstream f(file_name);
if (!f.is_open()) {
std::cout << "cannot open " << file_name << std::endl;
@ -728,7 +728,7 @@ struct sort_pred {
}
};
vector<std::string> get_file_names_from_file_list(std::string filelist) {
vector<std::string> get_file_names_from_file_list(const std::string& filelist) {
std::ifstream file(filelist);
if (!file.is_open()) {
std::cout << "cannot open " << filelist << std::endl;

6
src/test/lp/smt_reader.h
View file

@ -66,7 +66,7 @@ namespace lp {
lconstraint_kind m_kind;
std::vector<std::pair<mpq, std::string>> m_coeffs;
mpq m_right_side;
void add_pair(mpq c, std::string name) {
void add_pair(mpq c, const std::string& name) {
m_coeffs.push_back(make_pair(c, name));
}
formula_constraint() : m_right_side(numeric_traits<mpq>::zero()) {}
@ -81,7 +81,7 @@ namespace lp {
std::string m_file_name;
std::ifstream m_file_stream;
std::string m_line;
smt_reader(std::string file_name):
smt_reader(const std::string& file_name):
m_is_OK(true),
m_line_number(0),
m_file_name(file_name),
@ -372,7 +372,7 @@ namespace lp {
}
*/
unsigned register_name(std::string s) {
unsigned register_name(const std::string& s) {
auto it = m_name_to_var_index.find(s);
if (it!= m_name_to_var_index.end())
return it->second;

2
src/test/lp/test_file_reader.h
View file

@ -59,7 +59,7 @@ class test_file_reader {
std::ifstream m_file_stream;
public:
// constructor
test_file_reader(std::string file_name) : m_file_stream(file_name) {
test_file_reader(const std::string& file_name) : m_file_stream(file_name) {
if (!m_file_stream.is_open()) {
std::cout << "cannot open file " << "\'" << file_name << "\'" << std::endl;
}