diff --git a/src/solvers/smt2/letify.h b/src/solvers/smt2/letify.h index 71085432b2d..6a5239a2e9d 100644 --- a/src/solvers/smt2/letify.h +++ b/src/solvers/smt2/letify.h @@ -33,7 +33,7 @@ class letifyt symbol_exprt let_symbol; }; -#ifdef HASH_CODE +#if HASH_CODE using seen_expressionst = std::unordered_map; #else using seen_expressionst = irep_hash_mapt; diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index b66883496bc..47c17f395fe 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -16,8 +16,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#ifndef HASH_CODE -#include +#if !HASH_CODE +# include #endif #include diff --git a/src/util/irep.cpp b/src/util/irep.cpp index 543c7b662ff..8f4074e89bf 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -519,7 +519,7 @@ std::size_t irept::number_of_non_comments(const named_subt &named_sub) std::size_t irept::hash() const { - #ifdef HASH_CODE +#if HASH_CODE if(read().hash_code!=0) return read().hash_code; #endif @@ -543,7 +543,7 @@ std::size_t irept::hash() const result = hash_finalize(result, sub.size() + number_of_named_ireps); -#ifdef HASH_CODE +#if HASH_CODE read().hash_code=result; #endif #ifdef IREP_HASH_STATS diff --git a/src/util/irep.h b/src/util/irep.h index 3cb27175392..ee955d1048b 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -17,7 +17,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "irep_ids.h" #define SHARING -// #define HASH_CODE +#ifndef HASH_CODE +# define HASH_CODE 1 +#endif // #define NAMED_SUB_IS_FORWARD_LIST #ifdef NAMED_SUB_IS_FORWARD_LIST @@ -138,7 +140,7 @@ class tree_nodet : public ref_count_ift named_subt named_sub; subt sub; -#ifdef HASH_CODE +#if HASH_CODE mutable std::size_t hash_code = 0; #endif @@ -147,7 +149,7 @@ class tree_nodet : public ref_count_ift data.clear(); sub.clear(); named_sub.clear(); -#ifdef HASH_CODE +#if HASH_CODE hash_code = 0; #endif } @@ -157,7 +159,7 @@ class tree_nodet : public ref_count_ift d.data.swap(data); d.sub.swap(sub); d.named_sub.swap(named_sub); -#ifdef HASH_CODE +#if HASH_CODE std::swap(d.hash_code, hash_code); #endif } @@ -278,7 +280,7 @@ class sharing_treet dt &write() { detach(); -#ifdef HASH_CODE +#if HASH_CODE data->hash_code = 0; #endif return *data; @@ -319,7 +321,7 @@ class non_sharing_treet dt &write() { -#ifdef HASH_CODE +#if HASH_CODE data.hash_code = 0; #endif return data; diff --git a/unit/util/irep.cpp b/unit/util/irep.cpp index f0d45369432..d9da47bb18b 100644 --- a/unit/util/irep.cpp +++ b/unit/util/irep.cpp @@ -53,7 +53,7 @@ SCENARIO("irept_memory", "[core][utils][irept]") # endif #endif -#ifdef HASH_CODE +#if HASH_CODE const std::size_t hash_code_size = sizeof(std::size_t); #else const std::size_t hash_code_size = 0;