Skip to content

Commit fccff52

Browse files
author
Daniel Kroening
committed
introduce to_dstring
As std::to_string, to_dstring produces a string from a number. A key feature is that dstrings for values <=64 are pre-computed; generating strings for such numbers is 50x faster than going via std::to_string. int main() { for(unsigned i=0; i<20000000; i++) { dstringt d; int j=20; d=dstringt(std::to_string(j)); } } This is 2.5s as above, and 0.05s with to_dstring.
1 parent c8f6829 commit fccff52

File tree

3 files changed

+30
-1
lines changed

3 files changed

+30
-1
lines changed

src/util/dstring.cpp

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,3 +17,15 @@ std::ostream &dstringt::operator<<(std::ostream &out) const
1717
{
1818
return out << as_string();
1919
}
20+
21+
dstringt get_dstring_number(std::size_t value)
22+
{
23+
static const dstringt *const dstring_numbers = [] {
24+
dstringt *array = new dstringt[DSTRING_NUMBERS_MAX + 1];
25+
for(std::size_t i = 0; i <= DSTRING_NUMBERS_MAX; i++)
26+
array[i] = dstringt(std::to_string(i));
27+
return array;
28+
}();
29+
30+
return dstring_numbers[value];
31+
}

src/util/dstring.h

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -209,4 +209,21 @@ struct diagnostics_helpert<dstringt>
209209
}
210210
};
211211

212+
#define DSTRING_NUMBERS_MAX 64
213+
214+
dstringt get_dstring_number(std::size_t);
215+
216+
/// equivalent to dstringt(std::to_string(value)), i.e., produces a string
217+
/// from a number
218+
template <typename T>
219+
static inline
220+
typename std::enable_if<std::is_integral<T>::value, dstringt>::type
221+
to_dstring(T value)
222+
{
223+
if(value >= 0 && value <= DSTRING_NUMBERS_MAX)
224+
return get_dstring_number(value);
225+
else
226+
return std::to_string(value);
227+
}
228+
212229
#endif // CPROVER_UTIL_DSTRING_H

src/util/irep.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -263,7 +263,7 @@ long long irept::get_long_long(const irep_namet &name) const
263263

264264
void irept::set(const irep_namet &name, const long long value)
265265
{
266-
add(name).id(std::to_string(value));
266+
add(name).id(to_dstring(value));
267267
}
268268

269269
void irept::remove(const irep_namet &name)

0 commit comments

Comments
 (0)