Consistently disable simplify_exprt::local_replace_map

This avoids unnecessarily computing the hash of an exprt for an unused map. The
common preprocessor macro now also links together all related bits of code.

Author: tautschnig

src/util/simplify_expr.cpp

@@ -1067,7 +1067,7 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr)
       result=false;
     }
 
-    #if 0
+#ifdef USE_LOCAL_REPLACE_MAP
     replace_mapt map_before(local_replace_map);
 
     // a ? b : c  --> a ? b[a/true] : c
@@ -1109,10 +1109,10 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr)
     result=simplify_rec(falsevalue) && result;
 
     local_replace_map.swap(map_before);
-    #else
+#else
     result=simplify_rec(truevalue) && result;
     result=simplify_rec(falsevalue) && result;
-    #endif
+#endif
   }
   else
   {
@@ -2382,6 +2382,7 @@ bool simplify_exprt::simplify_rec(exprt &expr)
   if(!simplify_node(tmp))
     result=false;
 
+#ifdef USE_LOCAL_REPLACE_MAP
   #if 1
   replace_mapt::const_iterator it=local_replace_map.find(tmp);
   if(it!=local_replace_map.end())
@@ -2397,6 +2398,7 @@ bool simplify_exprt::simplify_rec(exprt &expr)
     result=false;
   }
   #endif
+#endif
 
   if(!result)
   {

src/util/simplify_expr_class.h

@@ -19,7 +19,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "type.h"
 #include "mp_arith.h"
+// #define USE_LOCAL_REPLACE_MAP
+#ifdef USE_LOCAL_REPLACE_MAP
 #include "replace_expr.h"
+#endif
 
 class bswap_exprt;
 class byte_extract_exprt;
@@ -154,7 +157,9 @@ class simplify_exprt
 #ifdef DEBUG_ON_DEMAND
   bool debug_on;
 #endif
+#ifdef USE_LOCAL_REPLACE_MAP
   replace_mapt local_replace_map;
+#endif
 };
 
 #endif // CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H