mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

Avoid unnecessary copies in for-range loops.

Browse source
This commit is contained in:
Bruce Mitchener 2018-10-02 10:38:41 +07:00
parent b0dac346dc
commit 7bc283b84e
4 changed files with 14 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/pb2bv_rewriter.cpp
View file

@ -458,7 +458,7 @@ struct pb2bv_rewriter::imp {
result = m.mk_true();
expr_ref_vector carry(m), new_carry(m);
m_base.push_back(bound + rational::one());
for (rational b_i : m_base) {
for (const rational& b_i : m_base) {
unsigned B = b_i.get_unsigned();
unsigned d_i = (bound % b_i).get_unsigned();
bound = div(bound, b_i);

4
src/smt/theory_seq.cpp
View file

@ -1375,8 +1375,8 @@ bool theory_seq::branch_variable_mb() {
continue;
}
rational l1, l2;
for (auto elem : len1) l1 += elem;
for (auto elem : len2) l2 += elem;
for (const auto& elem : len1) l1 += elem;
for (const auto& elem : len2) l2 += elem;
if (l1 != l2) {
TRACE("seq", tout << "lengths are not compatible\n";);
expr_ref l = mk_concat(e.ls());

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

@ -112,7 +112,7 @@ public:
std::string usage_string() {
std::string ret = "";
std::vector<std::string> unknown_options;
for (auto t : m_free_args) {
for (const auto & t : m_free_args) {
if (starts_with(t, "-") || starts_with(t, "\\")) {
unknown_options.push_back(t);
}
@ -120,7 +120,7 @@ public:
if (unknown_options.size()) {
ret = "Unknown options:";
}
for (auto unknownOption : unknown_options) {
for (const auto & unknownOption : unknown_options) {
ret += unknownOption;
ret += ",";
}
@ -140,7 +140,7 @@ public:
return;
}
std::cout << "options are: " << std::endl;
for (std::string s : m_used_options) {
for (const std::string & s : m_used_options) {
std::cout << s << std::endl;
}
for (auto & t : m_used_options_with_after_string) {

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

@ -1161,14 +1161,14 @@ void setup_solver(unsigned max_iterations, unsigned time_limit, bool look_for_mi
bool values_are_one_percent_close(double a, double b);
void print_x(mps_reader<double, double> & reader, lp_solver<double, double> * solver) {
for (auto name : reader.column_names()) {
for (const auto & name : reader.column_names()) {
std::cout << name << "=" << solver->get_column_value_by_name(name) << ' ';
}
std::cout << std::endl;
}
void compare_solutions(mps_reader<double, double> & reader, lp_solver<double, double> * solver, lp_solver<double, double> * solver0) {
for (auto name : reader.column_names()) {
for (const auto & name : reader.column_names()) {
double a = solver->get_column_value_by_name(name);
double b = solver0->get_column_value_by_name(name);
if (!values_are_one_percent_close(a, b)) {
@ -1299,7 +1299,7 @@ void solve_mps_in_rational(std::string file_name, bool dual, argument_parser & /
std::cout << "status is " << lp_status_to_string(solver->get_status()) << std::endl;
if (solver->get_status() == lp_status::OPTIMAL) {
if (reader.column_names().size() < 20) {
for (auto name : reader.column_names()) {
for (const auto & name : reader.column_names()) {
std::cout << name << "=" << solver->get_column_value_by_name(name).get_double() << ' ';
}
}
@ -1414,7 +1414,7 @@ void solve_mps_with_known_solution(std::string file_name, std::unordered_map<std
}
}
if (reader.column_names().size() < 20) {
for (auto name : reader.column_names()) {
for (const auto & name : reader.column_names()) {
std::cout << name << "=" << solver->get_column_value_by_name(name) << ' ';
}
std::cout << std::endl;
@ -1775,7 +1775,7 @@ void solve_rational() {
expected_sol["x8"] = lp::mpq(0);
solver.find_maximal_solution();
lp_assert(solver.get_status() == lp_status::OPTIMAL);
for (auto it : expected_sol) {
for (const auto & it : expected_sol) {
lp_assert(it.second == solver.get_column_value_by_name(it.first));
}
}
@ -2369,7 +2369,7 @@ void test_files_from_directory(std::string test_file_dir, argument_parser & args
std::unordered_map<std::string, lp::mpq> get_solution_map(lp_solver<lp::mpq, lp::mpq> * lps, mps_reader<lp::mpq, lp::mpq> & reader) {
std::unordered_map<std::string, lp::mpq> ret;
for (auto it : reader.column_names()) {
for (const auto & it : reader.column_names()) {
ret[it] = lps->get_column_value_by_name(it);
}
return ret;
@ -2487,7 +2487,7 @@ void test_lar_solver(argument_parser & args_parser) {
std::string file_list = args_parser.get_option_value("--filelist");
if (file_list.size() > 0) {
for (std::string fn : get_file_names_from_file_list(file_list))
for (const std::string & fn : get_file_names_from_file_list(file_list))
test_lar_on_file(fn, args_parser);
return;
}
@ -3624,7 +3624,7 @@ void test_lp_local(int argn, char**argv) {
}
std::string file_list = args_parser.get_option_value("--filelist");
if (file_list.size() > 0) {
for (std::string fn : get_file_names_from_file_list(file_list))
for (const std::string & fn : get_file_names_from_file_list(file_list))
solve_mps(fn, args_parser);
return finalize(0);
}