introduce to_dstring

src/util/dstring.cpp

@@ -17,3 +17,15 @@ std::ostream &dstringt::operator<<(std::ostream &out) const
 {
   return out << as_string();
 }
+
+dstringt get_dstring_number(std::size_t value)
+{
+  static const dstringt *const dstring_numbers = [] {
+    dstringt *array = new dstringt[DSTRING_NUMBERS_MAX + 1];
+    for(std::size_t i = 0; i <= DSTRING_NUMBERS_MAX; i++)
+      array[i] = dstringt(std::to_string(i));
+    return array;
+  }();
+
+  return dstring_numbers[value];
+}

src/util/dstring.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <string>
 
 #include "invariant.h"
+#include "magic.h"
 #include "string_container.h"
 
 /// \ref dstringt has one field, an unsigned integer \ref no which is an index
@@ -220,4 +221,19 @@ struct diagnostics_helpert<dstringt>
   }
 };
 
+dstringt get_dstring_number(std::size_t);
+
+/// equivalent to dstringt(std::to_string(value)), i.e., produces a string
+/// from a number
+template <typename T>
+static inline
+  typename std::enable_if<std::is_integral<T>::value, dstringt>::type
+  to_dstring(T value)
+{
+  if(value >= 0 && value <= static_cast<T>(DSTRING_NUMBERS_MAX))
+    return get_dstring_number(value);
+  else
+    return std::to_string(value);
+}
+
 #endif // CPROVER_UTIL_DSTRING_H

src/util/irep.cpp

@@ -126,7 +126,11 @@ long long irept::get_long_long(const irep_namet &name) const
 
 void irept::set(const irep_namet &name, const long long value)
 {
+#ifdef USE_DSTRING
+  add(name).id(to_dstring(value));
+#else
   add(name).id(std::to_string(value));
+#endif
 }
 
 void irept::remove(const irep_namet &name)

src/util/magic.h

@@ -13,4 +13,7 @@ const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH = 16;
 // Limit the size of strings in traces to 64M chars to avoid memout
 const std::size_t MAX_CONCRETE_STRING_SIZE = 1 << 26;
 
+// The top end of the range of integers for which dstrings are precomputed
+constexpr std::size_t DSTRING_NUMBERS_MAX = 64;
+
 #endif