Merge pull request #1859 from waywardmonkeys/for-range-copy

Avoid unnecessary copies in for-range loops.

src/ast/rewriter/pb2bv_rewriter.cpp

@@ -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);                

src/smt/theory_seq.cpp

@@ -1375,8 +1375,8 @@ bool theory_seq::branch_variable_mb() {
             continue;
         }
         rational l1, l2;
-        for (auto elem : len1) l1 += elem;
+        for (const auto& elem : len1) l1 += elem;
-        for (auto elem : len2) l2 += 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());

src/test/lp/argument_parser.h

@@ -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) {

src/test/lp/lp.cpp

@@ -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);
     }