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

src/math/lp/lar_solver.cpp

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

src/math/lp/lar_solver.h

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

src/math/lp/lp_settings.h

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

src/math/lp/lp_settings_def.h

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

src/math/lp/var_register.h

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

src/nlsat/nlsat_solver.cpp

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

src/sat/sat_bcd.cpp

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

src/test/lp/argument_parser.h

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

src/test/lp/lp.cpp

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

src/test/lp/smt_reader.h

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

src/test/lp/test_file_reader.h

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