From fc8193828d58600b03ecb0109a1446c0524ef99d Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Mon, 2 Jul 2018 11:43:00 +0100
Subject: [PATCH] minor simplifications to symbol class

---
 src/util/symbol.cpp | 29 +++++------------------------
 src/util/symbol.h   |  5 ++---
 2 files changed, 7 insertions(+), 27 deletions(-)

diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp
index 220711003..90b245e6c 100644
--- a/src/util/symbol.cpp
+++ b/src/util/symbol.cpp
@@ -21,6 +21,7 @@ Revision History:
 #include "util/region.h"
 #include "util/string_buffer.h"
 #include "util/z3_omp.h"
+#include <cstring>
 
 symbol symbol::m_dummy(TAG(void*, nullptr, 2));
 const symbol symbol::null;
@@ -60,7 +61,7 @@ public:
     }
 };
 
-internal_symbol_table* g_symbol_table = nullptr;
+static internal_symbol_table* g_symbol_table = nullptr;
 
 void initialize_symbols() {
     if (!g_symbol_table) {
@@ -140,27 +141,7 @@ bool lt(symbol const & s1, symbol const & s2) {
         return false;
     }
     SASSERT(!s1.is_numerical() && !s2.is_numerical());
-    char const * str1 = s1.bare_str();
-    char const * str2 = s2.bare_str();
-    while (true) {
-        if (*str1 < *str2) {
-            return true;
-        }
-        else if (*str1 == *str2) {
-            str1++;
-            str2++;
-            if (!*str1) {
-                SASSERT(*str2); // the strings can't be equal.
-                return true;
-            }
-            if (!*str2) {
-                SASSERT(*str1); // the strings can't be equal.
-                return false;
-            }
-        }
-        else {
-            SASSERT(*str1 > *str2);
-            return false;
-        }
-    }
+    auto cmp = strcmp(s1.bare_str(), s2.bare_str());
+    SASSERT(cmp != 0);
+    return cmp < 0;
 }
diff --git a/src/util/symbol.h b/src/util/symbol.h
index 6a6e93747..88e825551 100644
--- a/src/util/symbol.h
+++ b/src/util/symbol.h
@@ -83,8 +83,7 @@ public:
     // It is the inverse of c_ptr().
     // It was made public to simplify the implementation of the C API.
     static symbol mk_symbol_from_c_ptr(void const * ptr) { 
-        symbol s(ptr); 
-        return s;
+        return symbol(ptr);
     }
     unsigned hash() const { 
         if (m_data == nullptr) return 0x9e3779d9;
@@ -93,7 +92,7 @@ public:
     }
     bool contains(char c) const;
     unsigned size() const;
-    char const * bare_str() const { SASSERT(!is_numerical()); return is_numerical() ? "" : m_data; }
+    char const * bare_str() const { SASSERT(!is_numerical()); return m_data; }
     friend std::ostream & operator<<(std::ostream & target, symbol s) {
         SASSERT(!s.is_marked());
         if (GET_TAG(s.m_data) == 0) {