Migrate codebase to std::string_view (except z3++.h) (#8266)

* Initial plan

* Update z3 codebase to use std::string_view (except z3++.h)

- Updated params.cpp/h to use string_view internally for parameter descriptions
- Updated trace.h/cpp to accept string_view for trace tag functions
- Updated hash.h/cpp to use string_view for string_hash function
- Updated all callers of string_hash to use string_view
- Properly handled nullptr to empty string_view conversions
- All tests passing

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add missing string_view includes to headers

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/ast/rewriter/cached_var_subst.h

@@ -29,7 +29,7 @@ class cached_var_subst {
     };
     struct key_hash_proc {
         unsigned operator()(key * k) const {
-            return string_hash(reinterpret_cast<char const *>(k->m_bindings), sizeof(expr *) * k->m_num_bindings, k->m_qa->get_id());
+            return string_hash(std::string_view(reinterpret_cast<char const *>(k->m_bindings), sizeof(expr *) * k->m_num_bindings), k->m_qa->get_id());
         }
     };
     struct key_eq_proc {

src/ast/sls/sls_seq_plugin.cpp

@@ -103,7 +103,7 @@ namespace sls {
     struct zstring_hash_proc {
         unsigned operator()(zstring const & s) const {
             auto str = s.encode();
-            return string_hash(str.c_str(), static_cast<unsigned>(s.length()), 17);
+            return string_hash(std::string_view(str), 17);
         }
     };
     

src/math/lp/emonics.h

@@ -60,7 +60,7 @@ class emonics {
             
         unsigned operator()(lpvar v) const {
             auto const& vec = v != UINT_MAX? em.m_monics[em.m_var2index[v]].rvars() : em.m_find_key;
-            return string_hash(reinterpret_cast<char const*>(vec.data()), sizeof(lpvar)*vec.size(), 10);
+            return string_hash(std::string_view(reinterpret_cast<char const*>(vec.data()), sizeof(lpvar)*vec.size()), 10);
         }
     };
         

src/math/polynomial/polynomial.cpp

@@ -168,7 +168,7 @@ namespace polynomial {
         }
     public:
         static unsigned hash_core(unsigned sz, power const * pws) {
-            return string_hash(reinterpret_cast<char*>(const_cast<power*>(pws)), sz*sizeof(power), 11);
+            return string_hash(std::string_view(reinterpret_cast<char*>(const_cast<power*>(pws)), sz*sizeof(power)), 11);
         }
 
         struct hash_proc {

src/muz/base/dl_util.h

@@ -63,7 +63,7 @@ namespace datalog {
 
     struct std_string_hash_proc { 
         unsigned operator()(const std::string & s) const 
-        { return string_hash(s.c_str(), static_cast<unsigned>(s.length()), 17); } 
+        { return string_hash(std::string_view(s), 17); } 
     };
 
     // typedef int_hashtable<int_hash, default_eq<int> > idx_set;

src/muz/rel/dl_sparse_table.h

@@ -121,7 +121,7 @@ namespace datalog {
             offset_hash_proc(storage & s, unsigned unique_entry_sz) 
                 : m_storage(s), m_unique_entry_size(unique_entry_sz) {}
             unsigned operator()(store_offset ofs) const {
-                return string_hash(m_storage.data()+ofs, m_unique_entry_size, 0);
+                return string_hash(std::string_view(m_storage.data()+ofs, m_unique_entry_size), 0);
             } 
         };
 

src/sat/sat_proof_trim.h

@@ -40,7 +40,7 @@ namespace sat {
         
         struct hash {
             unsigned operator()(literal_vector const& v) const {
-                return string_hash((char const*)v.begin(), v.size()*sizeof(literal), 3);
+                return string_hash(std::string_view((char const*)v.begin(), v.size()*sizeof(literal)), 3);
             }
         };
         struct eq {

src/sat/smt/bv_solver.cpp

@@ -711,7 +711,7 @@ namespace bv {
             hash(solver& s) :s(s) {}
             bool operator()(theory_var v) const {
                 literal_vector const& a = s.m_bits[v];
-                return string_hash(reinterpret_cast<char*>(a.data()), a.size() * sizeof(sat::literal), 3);
+                return string_hash(std::string_view(reinterpret_cast<char*>(a.data()), a.size() * sizeof(sat::literal)), 3);
             }
         };
         eq eq_proc(*this);

src/tactic/arith/bv2real_rewriter.h

@@ -48,7 +48,7 @@ class bv2real_util {
     struct bvr_hash {
         unsigned operator()(bvr_sig const& x) const {
             unsigned a[3] = { x.m_msz, x.m_nsz, x.m_d.hash() };            
-            return string_hash((char const*)a, 12, x.m_r.hash());
+            return string_hash(std::string_view((char const*)a, 12), x.m_r.hash());
         }
     };
 

src/util/bit_vector.cpp

@@ -223,7 +223,7 @@ bool bit_vector::contains(bit_vector const& other) const {
 }
 
 unsigned bit_vector::get_hash() const {
-    return string_hash(reinterpret_cast<char const* const>(m_data), size()/8,  0);
+    return string_hash(std::string_view(reinterpret_cast<char const* const>(m_data), size()/8),  0);
 }
 
 bit_vector& bit_vector::neg() {

src/util/fixed_bit_vector.cpp

@@ -137,7 +137,7 @@ bool fixed_bit_vector_manager::equals(fixed_bit_vector const& a, fixed_bit_vecto
     return last_word(a) == last_word(b);
 }
 unsigned fixed_bit_vector_manager::hash(fixed_bit_vector const& src) const {
-    return string_hash(reinterpret_cast<char const* const>(src.m_data), num_bits()/8, num_bits());
+    return string_hash(std::string_view(reinterpret_cast<char const* const>(src.m_data), num_bits()/8), num_bits());
 }
 
 bool fixed_bit_vector_manager::contains(fixed_bit_vector const& a, fixed_bit_vector const& b) const {

src/util/hash.cpp

@@ -29,8 +29,10 @@ static unsigned read_unsigned(const char *s) {
 
 // I'm using Bob Jenkin's hash function.
 // http://burtleburtle.net/bob/hash/doobs.html
-unsigned string_hash(const char * str, unsigned length, unsigned init_value) {
+unsigned string_hash(std::string_view str, unsigned init_value) {
     unsigned a, b, c, len;
+    const char * data = str.data();
+    unsigned length = static_cast<unsigned>(str.length());
 
     /* Set up the internal state */
     len = length;
@@ -40,49 +42,49 @@ unsigned string_hash(const char * str, unsigned length, unsigned init_value) {
     /*---------------------------------------- handle most of the key */
     SASSERT(sizeof(unsigned) == 4);
     while (len >= 12) {
-        a += read_unsigned(str);
+        a += read_unsigned(data);
-        b += read_unsigned(str+4);
+        b += read_unsigned(data+4);
-        c += read_unsigned(str+8);
+        c += read_unsigned(data+8);
         mix(a,b,c);
-        str += 12; len -= 12;
+        data += 12; len -= 12;
     }
 
     /*------------------------------------- handle the last 11 bytes */
     c += length;
     switch(len) {        /* all the case statements fall through */
     case 11: 
-        c+=((unsigned)str[10]<<24);
+        c+=((unsigned)data[10]<<24);
         Z3_fallthrough;
     case 10: 
-        c+=((unsigned)str[9]<<16);
+        c+=((unsigned)data[9]<<16);
         Z3_fallthrough;
     case 9 : 
-        c+=((unsigned)str[8]<<8);
+        c+=((unsigned)data[8]<<8);
         Z3_fallthrough;
         /* the first byte of c is reserved for the length */
     case 8 : 
-        b+=((unsigned)str[7]<<24);
+        b+=((unsigned)data[7]<<24);
         Z3_fallthrough;
     case 7 : 
-        b+=((unsigned)str[6]<<16);
+        b+=((unsigned)data[6]<<16);
         Z3_fallthrough;
     case 6 : 
-        b+=((unsigned)str[5]<<8);
+        b+=((unsigned)data[5]<<8);
         Z3_fallthrough;
     case 5 : 
-        b+=str[4];
+        b+=data[4];
         Z3_fallthrough;
     case 4 : 
-        a+=((unsigned)str[3]<<24);
+        a+=((unsigned)data[3]<<24);
         Z3_fallthrough;
     case 3 : 
-        a+=((unsigned)str[2]<<16);
+        a+=((unsigned)data[2]<<16);
         Z3_fallthrough;
     case 2 : 
-        a+=((unsigned)str[1]<<8);
+        a+=((unsigned)data[1]<<8);
         Z3_fallthrough;
     case 1 : 
-        a+=str[0];
+        a+=data[0];
         /* case 0: nothing left to add */
         break;
     }

src/util/hash.h

@@ -19,6 +19,7 @@ Revision History:
 #pragma once
 
 #include<algorithm>
+#include<string_view>
 #include "util/util.h"
 
 #define mix(a,b,c)              \
@@ -65,10 +66,10 @@ inline unsigned hash_u_u(unsigned a, unsigned b) {
     return combine_hash(hash_u(a), hash_u(b));
 }
 
-unsigned string_hash(const char * str, unsigned len, unsigned init_value);
+unsigned string_hash(std::string_view str, unsigned init_value);
 
 inline unsigned unsigned_ptr_hash(unsigned const* vec, unsigned len, unsigned init_value) {
-    return string_hash((char const*)(vec), len*4, init_value);
+    return string_hash(std::string_view((char const*)(vec), len*4), init_value);
 }
 
 template<typename Composite, typename GetKindHashProc, typename GetChildHashProc>

src/util/id_gen.h

@@ -57,7 +57,7 @@ public:
     }
     
     unsigned show_hash(){
-      unsigned h = string_hash((char *)&m_free_ids[0],m_free_ids.size()*sizeof(unsigned),17);
+      unsigned h = string_hash(std::string_view((char *)&m_free_ids[0],m_free_ids.size()*sizeof(unsigned)),17);
       return hash_u_u(h,m_next_id);
     }
 

src/util/mpz.cpp

@@ -1862,7 +1862,7 @@ unsigned mpz_manager<SYNCH>::hash(mpz const & a) {
     unsigned sz = size(a);
     if (sz == 1)
         return static_cast<unsigned>(digits(a)[0]);
-    return string_hash(reinterpret_cast<char*>(digits(a)), sz * sizeof(digit_t), 17);
+    return string_hash(std::string_view(reinterpret_cast<char*>(digits(a)), sz * sizeof(digit_t)), 17);
 #else
     return mpz_get_si(*a.m_ptr);
 #endif

src/util/params.cpp

@@ -50,12 +50,12 @@ std::string norm_param_name(symbol const & n) {
 
 struct param_descrs::imp {
     struct info {
-        param_kind   m_kind;
+        param_kind         m_kind;
-        char const * m_descr;
+        std::string_view   m_descr;
-        char const * m_default;
+        std::string_view   m_default;
-        char const * m_module;
+        std::string_view   m_module;
 
-        info(param_kind k, char const * descr, char const * def, char const* module):
+        info(param_kind k, std::string_view descr, std::string_view def, std::string_view module):
             m_kind(k),
             m_descr(descr),
             m_default(def),
@@ -64,16 +64,16 @@ struct param_descrs::imp {
 
         info():
             m_kind(CPK_INVALID), 
-            m_descr(nullptr),
+            m_descr(),
-            m_default(nullptr),
+            m_default(),
-            m_module(nullptr) {
+            m_module() {
         }
     };
 
     dictionary<info> m_info;
     svector<symbol> m_names;
 
-    void insert(symbol const & name, param_kind k, char const * descr, char const * def, char const* module) {
+    void insert(symbol const & name, param_kind k, std::string_view descr, std::string_view def, std::string_view module) {
         SASSERT(!name.is_numerical());
         info i;
         if (m_info.find(name, i)) {
@@ -83,6 +83,13 @@ struct param_descrs::imp {
         m_info.insert(name, info(k, descr, def, module));
         m_names.push_back(name);
     }
+    
+    void insert(symbol const & name, param_kind k, char const * descr, char const * def, char const* module) {
+        insert(name, k, 
+               descr ? std::string_view(descr) : std::string_view(),
+               def ? std::string_view(def) : std::string_view(),
+               module ? std::string_view(module) : std::string_view());
+    }
 
     void erase(symbol const & name) {
         m_info.erase(name);
@@ -127,25 +134,25 @@ struct param_descrs::imp {
         return k;
     }
 
-    char const* get_module(symbol const& name) const {
+    std::string_view get_module(symbol const& name) const {
         info i;
         if (m_info.find(name, i)) 
             return i.m_module;
-        return nullptr;
+        return {};
     }
 
-    char const * get_descr(symbol const & name) const {
+    std::string_view get_descr(symbol const & name) const {
         info i;
         if (m_info.find(name, i))
             return i.m_descr;
-        return nullptr;
+        return {};
     }
 
-    char const * get_default(symbol const & name) const {
+    std::string_view get_default(symbol const & name) const {
         info i;
         if (m_info.find(name, i))
             return i.m_default;
-        return nullptr;
+        return {};
     }
 
     unsigned size() const {
@@ -190,14 +197,14 @@ struct param_descrs::imp {
             }
             info d;
             m_info.find(name, d);
-            SASSERT(d.m_descr);
+            SASSERT(!d.m_descr.empty());
             if (markdown) 
                 out << " | " << d.m_kind << " ";
             else
                 out << " (" << d.m_kind << ")";
             if (markdown) {
                 out << " |  ";
-                for (auto ch : std::string_view(d.m_descr)) {
+                for (auto ch : d.m_descr) {
                     switch (ch) {
                     case '<': out << "&lt;"; break;
                     case '>': out << "&gt;"; break;
@@ -209,10 +216,10 @@ struct param_descrs::imp {
                 out << " " << d.m_descr;
             if (markdown) {
                 out << " | ";
-                if (d.m_default)
+                if (!d.m_default.empty())
                     out << d.m_default;
             }
-            else if (d.m_default != nullptr)
+            else if (!d.m_default.empty())
                 out << " (default: " << d.m_default << ")";
             out << "\n";
         }
@@ -259,7 +266,8 @@ char const * param_descrs::get_descr(char const * name) const {
 }
 
 char const * param_descrs::get_descr(symbol const & name) const {
-    return m_imp->get_descr(name);
+    auto sv = m_imp->get_descr(name);
+    return sv.empty() ? nullptr : sv.data();
 }
 
 char const * param_descrs::get_default(char const * name) const {
@@ -267,7 +275,8 @@ char const * param_descrs::get_default(char const * name) const {
 }
 
 char const * param_descrs::get_default(symbol const & name) const {
-    return m_imp->get_default(name);
+    auto sv = m_imp->get_default(name);
+    return sv.empty() ? nullptr : sv.data();
 }
 
 void param_descrs::erase(symbol const & name) {
@@ -299,7 +308,8 @@ symbol param_descrs::get_param_name(unsigned i) const {
 }
 
 char const* param_descrs::get_module(symbol const& name) const {
-    return m_imp->get_module(name);
+    auto sv = m_imp->get_module(name);
+    return sv.empty() ? nullptr : sv.data();
 }
 
 void param_descrs::display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const {

src/util/str_hashtable.h

@@ -24,7 +24,7 @@ Revision History:
 #include "util/hash.h"
 
 struct str_hash_proc { 
-    unsigned operator()(char const * s) const { return string_hash(s, static_cast<unsigned>(strlen(s)), 17); } 
+    unsigned operator()(char const * s) const { return string_hash(std::string_view(s), 17); } 
 };
 struct str_eq_proc { bool operator()(char const * s1, char const * s2) const { return strcmp(s1, s2) == 0; } }; 
 typedef ptr_hashtable<const char, str_hash_proc, str_eq_proc> str_hashtable;

src/util/symbol.cpp

@@ -109,7 +109,7 @@ struct internal_symbol_tables {
     }
 
     char const * get_str(char const * d) {
-        auto* table = tables[string_hash(d, static_cast<unsigned>(strlen(d)), 251) % sz];
+        auto* table = tables[string_hash(std::string_view(d), 251) % sz];
         return table->get_str(d);
     }
 };

src/util/trace.cpp

@@ -105,9 +105,9 @@ static const tag_info* get_tag_infos() {
 }
 
 
-static size_t levenshtein_distance(const char* s, const char* t) {
+static size_t levenshtein_distance(std::string_view s, std::string_view t) {
-    size_t len_s = strlen(s);
+    size_t len_s = s.length();
-    size_t len_t = strlen(t);
+    size_t len_t = t.length();
     std::vector<size_t> prev(len_t + 1), curr(len_t + 1);
 
     for (size_t j = 0; j <= len_t; ++j)
@@ -124,19 +124,19 @@ static size_t levenshtein_distance(const char* s, const char* t) {
     return prev[len_t];
 }
 
-static bool has_overlap(char const* s, char const* t, size_t k) {
+static bool has_overlap(std::string_view s, std::string_view t, size_t k) {
     // Consider overlap if Levenshtein distance is <= k
     return levenshtein_distance(s, t) <= k;
 }
 
-void enable_trace(const char * tag_str) {
+void enable_trace(std::string_view tag_str) {
-    TraceTag tag = find_trace_tag_by_string(tag_str);
+    std::string tag_string(tag_str); // Convert to std::string for null-termination
-    size_t k = strlen(tag_str);
+    TraceTag tag = find_trace_tag_by_string(tag_string.c_str());
-
+    size_t k = tag_str.length();
 
   
     if (tag == TraceTag::Count) {
-        warning_msg("trace tag '%s' does not exist", tag_str);
+        warning_msg("trace tag '%s' does not exist", tag_string.c_str());
 #define X(tag_class, tag, desc) k = std::min(levenshtein_distance(#tag, tag_str), k);
 #include "util/trace_tags.def"
 #undef X
@@ -163,8 +163,9 @@ void enable_all_trace(bool flag) {
     g_enable_all_trace_tags = flag;
 }
 
-void disable_trace(const char * tag) {
+void disable_trace(std::string_view tag) {
-    TraceTag tag_str = find_trace_tag_by_string(tag);
+    std::string tag_string(tag); // Convert to std::string for null-termination
+    TraceTag tag_str = find_trace_tag_by_string(tag_string.c_str());
     disable_tag(tag_str);
 }
 

src/util/trace.h

@@ -20,6 +20,7 @@ Revision History:
 #pragma once
 
 #include<fstream>
+#include<string_view>
 #include "trace_tags.h"
 
 #ifdef SINGLE_THREAD
@@ -53,9 +54,9 @@ void verbose_unlock();
 extern std::ofstream tout; 
 #define TRACE_CODE(CODE) { CODE } ((void) 0 )
 
-void enable_trace(const char * tag);
+void enable_trace(std::string_view tag);
 void enable_all_trace(bool flag);
-void disable_trace(const char * tag);
+void disable_trace(std::string_view tag);
 bool is_trace_enabled(TraceTag tag);
 void close_trace();
 void open_trace();
@@ -63,9 +64,9 @@ void open_trace();
 #else
 #define TRACE_CODE(CODE) ((void) 0)
 
-static inline void enable_trace(const char * tag) {}
+static inline void enable_trace(std::string_view tag) {}
 static inline void enable_all_trace(bool flag) {}
-static inline void disable_trace(const char * tag) {}
+static inline void disable_trace(std::string_view tag) {}
 static inline bool is_trace_enabled(TraceTag tag) { return false; }
 static inline void close_trace() {}
 static inline void open_trace() {}