Skip to content

Commit cd07c79

Browse files
Introduce lazy class
This generalizes a pattern for which we have several potential usage.
1 parent 78fc2b7 commit cd07c79

File tree

1 file changed

+46
-0
lines changed

1 file changed

+46
-0
lines changed

src/util/lazy.h

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
/*******************************************************************\
2+
3+
Module: Util
4+
5+
Author: Romain Brenguier, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_UTIL_LAZY_H
10+
#define CPROVER_UTIL_LAZY_H
11+
12+
#include <functional>
13+
#include <util/optional.h>
14+
15+
template <typename valuet>
16+
class lazyt
17+
{
18+
public:
19+
/// Delay the computation of \p fun to the next time the \c force method
20+
/// is called.
21+
static lazyt from_fun(std::function<valuet()> fun)
22+
{
23+
return lazyt{std::move(fun)};
24+
}
25+
26+
/// Force the computation of the value. If it was already computed,
27+
/// return the same result.
28+
valuet force()
29+
{
30+
if(value)
31+
return *value;
32+
value = evaluation_function();
33+
return *value;
34+
}
35+
36+
private:
37+
optionalt<valuet> value;
38+
std::function<valuet()> evaluation_function;
39+
40+
explicit lazyt(std::function<valuet()> fun)
41+
: evaluation_function(std::move(fun))
42+
{
43+
}
44+
};
45+
46+
#endif // CPROVER_UTIL_LAZY_H

0 commit comments

Comments
 (0)