mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

Merge pull request #2066 from waywardmonkeys/const-str-hashtable

Browse source 
Let str_hashtable store `const char*`.
This commit is contained in:
Nikolaj Bjorner 2019-01-06 18:55:32 -08:00 committed by GitHub
parent ea48d0a95a a06bc49710
commit 8ad2f70aaa
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
4 changed files with 11 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/util/debug.cpp
View file

@ -56,17 +56,17 @@ void finalize_debug() {
void enable_debug(const char * tag) { void enable_debug(const char * tag) {
init_debug_table(); init_debug_table();
g_enabled_debug_tags->insert(const_cast<char *>(tag)); g_enabled_debug_tags->insert(tag);
} }
void disable_debug(const char * tag) { void disable_debug(const char * tag) {
init_debug_table(); init_debug_table();
g_enabled_debug_tags->erase(const_cast<char *>(tag)); g_enabled_debug_tags->erase(tag);
} }
bool is_debug_enabled(const char * tag) { bool is_debug_enabled(const char * tag) {
init_debug_table(); init_debug_table();
return g_enabled_debug_tags->contains(const_cast<char *>(tag)); return g_enabled_debug_tags->contains(tag);
} }
#if !defined(_WINDOWS) && !defined(NO_Z3_DEBUGGER) #if !defined(_WINDOWS) && !defined(NO_Z3_DEBUGGER)

2
src/util/str_hashtable.h
View file

@ -28,7 +28,7 @@ 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(s, static_cast<unsigned>(strlen(s)), 17); }
}; };
struct str_eq_proc { bool operator()(char const * s1, char const * s2) const { return strcmp(s1, s2) == 0; } }; struct str_eq_proc { bool operator()(char const * s1, char const * s2) const { return strcmp(s1, s2) == 0; } };
typedef ptr_hashtable<char, str_hash_proc, str_eq_proc> str_hashtable; typedef ptr_hashtable<const char, str_hash_proc, str_eq_proc> str_hashtable;
#endif /* STR_HASHTABLE_H_ */ #endif /* STR_HASHTABLE_H_ */

9
src/util/symbol.cpp
View file

@ -35,20 +35,19 @@ class internal_symbol_table {
public: public:
char const * get_str(char const * d) { char const * get_str(char const * d) {
char * result; const char * result;
#pragma omp critical (cr_symbol) #pragma omp critical (cr_symbol)
{ {
char * r_d = const_cast<char *>(d);
str_hashtable::entry * e; str_hashtable::entry * e;
if (m_table.insert_if_not_there_core(r_d, e)) { if (m_table.insert_if_not_there_core(d, e)) {
// new entry // new entry
size_t l = strlen(d); size_t l = strlen(d);
// store the hash-code before the string // store the hash-code before the string
size_t * mem = static_cast<size_t*>(m_region.allocate(l + 1 + sizeof(size_t))); size_t * mem = static_cast<size_t*>(m_region.allocate(l + 1 + sizeof(size_t)));
*mem = e->get_hash(); *mem = e->get_hash();
mem++; mem++;
result = reinterpret_cast<char*>(mem); result = reinterpret_cast<const char*>(mem);
memcpy(result, d, l+1); memcpy(mem, d, l+1);
// update the entry with the new ptr. // update the entry with the new ptr.
e->set_data(result); e->set_data(result);
} }

6
src/util/trace.cpp
View file

@ -38,7 +38,7 @@ void finalize_trace() {
} }
void enable_trace(const char * tag) { void enable_trace(const char * tag) {
get_enabled_trace_tags().insert(const_cast<char *>(tag)); get_enabled_trace_tags().insert(tag);
} }
void enable_all_trace(bool flag) { void enable_all_trace(bool flag) {
@ -46,12 +46,12 @@ void enable_all_trace(bool flag) {
} }
void disable_trace(const char * tag) { void disable_trace(const char * tag) {
get_enabled_trace_tags().erase(const_cast<char *>(tag)); get_enabled_trace_tags().erase(tag);
} }
bool is_trace_enabled(const char * tag) { bool is_trace_enabled(const char * tag) {
return g_enable_all_trace_tags || return g_enable_all_trace_tags ||
(g_enabled_trace_tags && get_enabled_trace_tags().contains(const_cast<char *>(tag))); (g_enabled_trace_tags && get_enabled_trace_tags().contains(tag));
} }
void close_trace() { void close_trace() {