Merge pull request #1992 from tautschnig/irep-speedup

Enable HASH_CODE by default to avoid repeated hash computation [blocks: #3486]

Author: tautschnig

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<exprt, let_count_idt, irep_hash>;
 #else
   using seen_expressionst = irep_hash_mapt<exprt, let_count_idt>;

src/solvers/smt2/smt2_conv.h

@@ -16,8 +16,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/byte_operators.h>
 
-#ifndef HASH_CODE
-#include <util/irep_hash_container.h>
+#if !HASH_CODE
+#  include <util/irep_hash_container.h>
 #endif
 
 #include <solvers/prop/prop_conv.h>

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

src/util/irep.h

@@ -17,7 +17,9 @@ Author: Daniel Kroening, [email protected]
 #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<sharing>
   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<sharing>
     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<sharing>
     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;

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;