Keep track of whether an irept has been subject to simplification

This should avoid redundant simplification.

Author: tautschnig

src/util/irep.h

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #define SHARING
 #define HASH_CODE
 #define NAMED_SUB_IS_FORWARD_LIST
+#define IS_CANONICAL_BIT
 
 #ifdef NAMED_SUB_IS_FORWARD_LIST
 #include <forward_list>
@@ -143,13 +144,20 @@ class tree_nodet : public ref_count_ift<sharing>
   mutable std::size_t hash_code = 0;
 #endif
 
+#ifdef IS_CANONICAL_BIT
+  bool is_canonical = true;
+#endif
+
   void clear()
   {
     data.clear();
     sub.clear();
     named_sub.clear();
 #ifdef HASH_CODE
     hash_code = 0;
+#endif
+#ifdef IS_CANONICAL_BIT
+    is_canonical = true;
 #endif
   }
 
@@ -160,6 +168,9 @@ class tree_nodet : public ref_count_ift<sharing>
     d.named_sub.swap(named_sub);
 #ifdef HASH_CODE
     std::swap(d.hash_code, hash_code);
+#endif
+#ifdef IS_CANONICAL_BIT
+    std::swap(d.is_canonical, is_canonical);
 #endif
   }
 
@@ -173,6 +184,10 @@ class tree_nodet : public ref_count_ift<sharing>
     : data(std::move(_data)),
       named_sub(std::move(_named_sub)),
       sub(std::move(_sub))
+#ifdef IS_CANONICAL_BIT
+      ,
+      is_canonical(false)
+#endif
   {
   }
 };
@@ -282,6 +297,9 @@ class sharing_treet
     detach();
 #ifdef HASH_CODE
     data->hash_code = 0;
+#endif
+#ifdef IS_CANONICAL_BIT
+    data->is_canonical = false;
 #endif
     return *data;
   }
@@ -323,6 +341,9 @@ class non_sharing_treet
   {
 #ifdef HASH_CODE
     data.hash_code = 0;
+#endif
+#ifdef IS_CANONICAL_BIT
+    data.is_canonical = false;
 #endif
     return data;
   }
@@ -494,6 +515,22 @@ class irept
 
   /// count the number of named_sub elements that are not comments
   static std::size_t number_of_non_comments(const named_subt &);
+
+#ifdef IS_CANONICAL_BIT
+  bool get_is_canonical() const
+  {
+    return read().is_canonical;
+  }
+
+  void set_is_canonical()
+  {
+#ifdef SHARING
+    data->is_canonical = true;
+#else
+    data.is_canonical = true;
+#endif
+  }
+#endif
 };
 
 // NOLINTNEXTLINE(readability/identifiers)

src/util/simplify_expr.cpp

@@ -2464,9 +2464,14 @@ bool simplify_exprt::simplify_node(exprt &expr)
 /// \return returns true if expression unchanged; returns false if changed
 bool simplify_exprt::simplify_rec(exprt &expr)
 {
-  // look up in cache
+#ifdef IS_CANONICAL_BIT
+  if(expr.get_is_canonical())
+    return true;
+#endif
+
+    // look up in cache
 
-  #ifdef USE_CACHE
+#ifdef USE_CACHE
   std::pair<simplify_expr_cachet::containert::iterator, bool>
     cache_result=simplify_expr_cache.container().
       insert(std::pair<exprt, exprt>(expr, exprt()));
@@ -2514,11 +2519,19 @@ bool simplify_exprt::simplify_rec(exprt &expr)
   {
     expr.swap(tmp);
 
-    #ifdef USE_CACHE
+#ifdef IS_CANONICAL_BIT
+    expr.set_is_canonical();
+#endif
+
+#ifdef USE_CACHE
     // save in cache
     cache_result.first->second=expr;
     #endif
   }
+#ifdef IS_CANONICAL_BIT
+  else
+    expr.set_is_canonical();
+#endif
 
   return result;
 }

unit/util/irep.cpp

@@ -59,9 +59,17 @@ SCENARIO("irept_memory", "[core][utils][irept]")
       const std::size_t hash_code_size = 0;
 #endif
 
+#ifdef HASH_CODE
+      const std::size_t is_canonical_size = sizeof(bool);
+#else
+      const std::size_t is_canonical_size = 0;
+#endif
+
       REQUIRE(
         sizeof(irept::dt) ==
-        ref_count_size + data_size + sub_size + named_size + hash_code_size);
+        ((ref_count_size + data_size + sub_size + named_size + hash_code_size +
+          is_canonical_size + (alignof(irept::dt) - 1)) &
+         ~(alignof(irept::dt) - 1)));
     }
 
     THEN("get_nil_irep yields ID_nil")