Skip to content

Commit 3a47be9

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 3a47be9

File tree

3 files changed

+70
-1
lines changed

3 files changed

+70
-1
lines changed

src/util/dstring.cpp

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,3 +17,65 @@ std::ostream &dstringt::operator<<(std::ostream &out) const
1717
{
1818
return out << as_string();
1919
}
20+
21+
#define NUMBERS_MAX 64
22+
23+
dstringt get_dstring_number(std::size_t value)
24+
{
25+
static const dstringt *dstring_numbers = [] {
26+
dstringt *array = new dstringt[NUMBERS_MAX + 1];
27+
for(std::size_t i = 0; i <= NUMBERS_MAX; i++)
28+
array[i] = dstringt(std::to_string(i));
29+
return array;
30+
}();
31+
32+
return dstring_numbers[value];
33+
}
34+
35+
dstringt to_dstring(int value)
36+
{
37+
if(value >= 0 && value <= NUMBERS_MAX)
38+
return get_dstring_number(value);
39+
else
40+
return std::to_string(value);
41+
}
42+
43+
dstringt to_dstring(long value)
44+
{
45+
if(value >= 0 && value <= NUMBERS_MAX)
46+
return get_dstring_number(value);
47+
else
48+
return std::to_string(value);
49+
}
50+
51+
dstringt to_dstring(long long value)
52+
{
53+
if(value >= 0 && value <= NUMBERS_MAX)
54+
return get_dstring_number(value);
55+
else
56+
return std::to_string(value);
57+
}
58+
59+
dstringt to_dstring(unsigned value)
60+
{
61+
if(value <= NUMBERS_MAX)
62+
return get_dstring_number(value);
63+
else
64+
return std::to_string(value);
65+
}
66+
67+
dstringt to_dstring(unsigned long value)
68+
{
69+
if(value <= NUMBERS_MAX)
70+
return get_dstring_number(value);
71+
else
72+
return std::to_string(value);
73+
}
74+
75+
dstringt to_dstring(unsigned long long value)
76+
{
77+
if(value <= NUMBERS_MAX)
78+
return get_dstring_number(value);
79+
else
80+
return std::to_string(value);
81+
}

src/util/dstring.h

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

212+
dstringt to_dstring(int value);
213+
dstringt to_dstring(long value);
214+
dstringt to_dstring(long long value);
215+
dstringt to_dstring(unsigned value);
216+
dstringt to_dstring(unsigned long);
217+
dstringt to_dstring(unsigned long long);
218+
212219
#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)