From f23b053fb9002a136de6198922091266eb27babb Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Sun, 3 Aug 2025 10:41:38 +0100
Subject: [PATCH] remove a bunch of string copies

---
 src/solver/smt_logics.cpp | 88 +++++++++++++++++++++++----------------
 src/util/gparams.cpp      |  2 +-
 2 files changed, 53 insertions(+), 37 deletions(-)

diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp
index 1afea69dc..0942ed3fe 100644
--- a/src/solver/smt_logics.cpp
+++ b/src/solver/smt_logics.cpp
@@ -29,52 +29,56 @@ bool smt_logics::supported_logic(symbol const & s) {
 }
 
 bool smt_logics::logic_has_reals_only(symbol const& s) {
+    auto str = s.str();
     return
-        s.str().find("LRA") != std::string::npos ||
-        s.str().find("LRA") != std::string::npos ||
-        s.str().find("NRA") != std::string::npos ||
-        s.str().find("RDL") != std::string::npos;
+        str.find("LRA") != std::string::npos ||
+        str.find("LRA") != std::string::npos ||
+        str.find("NRA") != std::string::npos ||
+        str.find("RDL") != std::string::npos;
 }
 
 bool smt_logics::logic_has_arith(symbol const & s) {
+    auto str = s.str();
     return
-        s.str().find("LRA") != std::string::npos ||
-        s.str().find("LIRA") != std::string::npos ||
-        s.str().find("LIA") != std::string::npos ||
-        s.str().find("LRA") != std::string::npos ||
-        s.str().find("NRA") != std::string::npos ||
-        s.str().find("NIRA") != std::string::npos ||
-        s.str().find("NIA") != std::string::npos ||
-        s.str().find("IDL") != std::string::npos ||
-        s.str().find("RDL") != std::string::npos ||
-        s == "QF_BVRE" ||
-        s == "QF_FP" ||
-        s == "FP" ||
-        s == "QF_FPBV" ||
-        s == "QF_BVFP" ||
-        s == "QF_S" ||
+        str.find("LRA") != std::string::npos ||
+        str.find("LIRA") != std::string::npos ||
+        str.find("LIA") != std::string::npos ||
+        str.find("LRA") != std::string::npos ||
+        str.find("NRA") != std::string::npos ||
+        str.find("NIRA") != std::string::npos ||
+        str.find("NIA") != std::string::npos ||
+        str.find("IDL") != std::string::npos ||
+        str.find("RDL") != std::string::npos ||
+        str == "QF_BVRE" ||
+        str == "QF_FP" ||
+        str == "FP" ||
+        str == "QF_FPBV" ||
+        str == "QF_BVFP" ||
+        str == "QF_S" ||
         logic_is_all(s) ||
-        s == "QF_FD" ||
-        s == "HORN";
+        str == "QF_FD" ||
+        str == "HORN";
 }
 
 bool smt_logics::logic_has_bv(symbol const & s) {
+    auto str = s.str();
     return
-        s.str().find("BV") != std::string::npos ||
-        s == "FP" ||
+        str.find("BV") != std::string::npos ||
+        str == "FP" ||
         logic_is_all(s) ||
-        s == "QF_FD" ||
-        s == "SMTFD" ||
-        s == "HORN";
+        str == "QF_FD" ||
+        str == "SMTFD" ||
+        str == "HORN";
 }
 
 bool smt_logics::logic_has_array(symbol const & s) {
+    auto str = s.str();
     return
-        s.str().starts_with("QF_A") ||   
-        s.str().starts_with("A") ||   
+        str.starts_with("QF_A") ||
+        str.starts_with("A") ||
         logic_is_all(s) ||
-        s == "SMTFD" ||
-        s == "HORN";
+        str == "SMTFD" ||
+        str == "HORN";
 }
 
 bool smt_logics::logic_has_seq(symbol const & s) {
@@ -82,17 +86,28 @@ bool smt_logics::logic_has_seq(symbol const & s) {
 }
 
 bool smt_logics::logic_has_str(symbol const & s) {
-    return s == "QF_S" || s == "QF_SLIA" || s == "QF_SNIA" || logic_is_all(s);
+    auto str = s.str();
+    return str == "QF_S" ||
+           str == "QF_SLIA" ||
+           str == "QF_SNIA" ||
+           logic_is_all(s);
 }
 
 bool smt_logics::logic_has_fpa(symbol const & s) {
-    return s == "FP" || s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "QF_FPLRA"  || logic_is_all(s);
+    auto str = s.str();
+    return str == "FP" ||
+           str == "QF_FP" ||
+           str == "QF_FPBV" ||
+           str == "QF_BVFP" ||
+           str == "QF_FPLRA"  ||
+           logic_is_all(s);
 }
 
 bool smt_logics::logic_has_uf(symbol const & s) {
+    auto str = s.str();
     return 
-        s.str().find("UF") != std::string::npos ||
-        s == "SMTFD";
+        str.find("UF") != std::string::npos ||
+        str == "SMTFD";
 }
 
 bool smt_logics::logic_has_horn(symbol const& s) {
@@ -104,9 +119,10 @@ bool smt_logics::logic_has_pb(symbol const& s) {
 }
 
 bool smt_logics::logic_has_datatype(symbol const& s) {
+    auto str = s.str();
     return 
-        s.str().find("DT") != std::string::npos ||
-        s == "QF_FD" ||
+        str.find("DT") != std::string::npos ||
+        str == "QF_FD" ||
         logic_is_all(s) ||
         logic_has_horn(s);
 }
diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp
index d2adc9f9f..7a81e000c 100644
--- a/src/util/gparams.cpp
+++ b/src/util/gparams.cpp
@@ -416,7 +416,7 @@ public:
         symbol sp(p.c_str());
         std::ostringstream buffer;
         ps.display(buffer, sp);
-        return buffer.str();
+        return std::move(buffer).str();
     }
 
     std::string get_default(param_descrs const & d, std::string const & p, std::string const & m) {