reduce memory allocs in params

Z3Prover · Dec 21, 2023 · 766f5f0 · 766f5f0
1 parent ae1d927
commit 766f5f0
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 19 deletions.
diff --git a/src/util/params.cpp b/src/util/params.cpp
@@ -99,25 +99,24 @@ struct param_descrs::imp {
         return CPK_INVALID;
     }
 
-    bool split_name(symbol const& name, symbol & prefix, symbol & suffix) const {
+    bool split_name(symbol const& name, std::string_view & prefix, symbol & suffix) const {
         if (name.is_numerical()) return false;
         char const* str = name.bare_str();
         char const* period = strchr(str,'.');
         if (!period) return false;
-        svector<char> prefix_((unsigned)(period-str), str);
-        prefix_.push_back(0);
-        prefix = symbol(prefix_.data());
+        prefix = std::string_view(str, period - str);
         suffix = symbol(period + 1);
         return true;
     }
 
     param_kind get_kind_in_module(symbol & name) const {
         param_kind k = get_kind(name);
-        symbol prefix, suffix;
+        std::string_view prefix;
+        symbol suffix;
         if (k == CPK_INVALID && split_name(name, prefix, suffix)) {   
             k = get_kind(suffix);
             if (k != CPK_INVALID) {
-                if (symbol(get_module(suffix)) == prefix) {
+                if (get_module(suffix) == prefix) {
                     name = suffix;
                 }
                 else {
@@ -170,8 +169,8 @@ struct param_descrs::imp {
         if (names.empty())
             return;
         if (markdown) {
-            out << " Parameter | Type | Description | Default\n";
-            out << " ----------|------|-------------|--------\n";            
+            out << " Parameter | Type | Description | Default\n"
+                   " ----------|------|-------------|--------\n";
         }
         for (symbol const& name : names) {
             for (unsigned i = 0; i < indent; i++) out << " ";
@@ -197,16 +196,14 @@ struct param_descrs::imp {
             else
                 out << " (" << d.m_kind << ")";
             if (markdown) {
-                out << " | ";
-                std::string desc;
-                for (auto ch : std::string(d.m_descr)) {
+                out << " |  ";
+                for (auto ch : std::string_view(d.m_descr)) {
                     switch (ch) {
-                    case '<': desc += "&lt;"; break;
-                    case '>': desc += "&gt;"; break;
-                    default: desc.push_back(ch);
+                    case '<': out << "&lt;"; break;
+                    case '>': out << "&gt;"; break;
+                    default:  out << ch; break;
                     }
                 }
-                out << " " << desc;
             }
             else if (include_descr)
                 out << " " << d.m_descr;
@@ -549,8 +546,7 @@ params_ref::~params_ref() {
         m_params->dec_ref();
 }
 
-params_ref::params_ref(params_ref const & p):
-    m_params(nullptr) {
+params_ref::params_ref(params_ref const & p) {
     set(p);
 }
 

diff --git a/src/util/params.h b/src/util/params.h
@@ -32,12 +32,12 @@ class param_descrs;
 class params_ref {
     static params_ref g_empty_params_ref;
 
-    params * m_params;
+    params * m_params = nullptr;
     void init();
     void copy_core(params const * p);
     void set(params_ref const& p);
 public:
-    params_ref():m_params(nullptr) {}
+    params_ref() = default;
     params_ref(params_ref const & p);
     ~params_ref();