mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity

minor simplifications to symbol class

Browse source
This commit is contained in:
Nuno Lopes 2018-07-02 11:43:00 +01:00
parent 0d4b4b30b1
commit fc8193828d
2 changed files with 7 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/util/symbol.cpp
View file

@ -21,6 +21,7 @@ Revision History:
#include "util/region.h" #include "util/region.h"
#include "util/string_buffer.h" #include "util/string_buffer.h"
#include "util/z3_omp.h" #include "util/z3_omp.h"
#include <cstring>
symbol symbol::m_dummy(TAG(void*, nullptr, 2)); symbol symbol::m_dummy(TAG(void*, nullptr, 2));
const symbol symbol::null; 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() { void initialize_symbols() {
if (!g_symbol_table) { if (!g_symbol_table) {
@ -140,27 +141,7 @@ bool lt(symbol const & s1, symbol const & s2) {
return false; return false;
} }
SASSERT(!s1.is_numerical() && !s2.is_numerical()); SASSERT(!s1.is_numerical() && !s2.is_numerical());
char const * str1 = s1.bare_str(); auto cmp = strcmp(s1.bare_str(), s2.bare_str());
char const * str2 = s2.bare_str(); SASSERT(cmp != 0);
while (true) { return cmp < 0;
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;
}
}
} }

5
src/util/symbol.h
View file

@ -83,8 +83,7 @@ public:
// It is the inverse of c_ptr(). // It is the inverse of c_ptr().
// It was made public to simplify the implementation of the C API. // It was made public to simplify the implementation of the C API.
static symbol mk_symbol_from_c_ptr(void const * ptr) { static symbol mk_symbol_from_c_ptr(void const * ptr) {
symbol s(ptr); return symbol(ptr);
return s;
} }
unsigned hash() const { unsigned hash() const {
if (m_data == nullptr) return 0x9e3779d9; if (m_data == nullptr) return 0x9e3779d9;
@ -93,7 +92,7 @@ public:
} }
bool contains(char c) const; bool contains(char c) const;
unsigned size() 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) { friend std::ostream & operator<<(std::ostream & target, symbol s) {
SASSERT(!s.is_marked()); SASSERT(!s.is_marked());
if (GET_TAG(s.m_data) == 0) { if (GET_TAG(s.m_data) == 0) {