Skip to content

Commit 087946b

Browse files
Introduce lazy class
This generalizes a pattern for which we have several potential usage.
1 parent eaf8cb3 commit 087946b

File tree

1 file changed

+45
-0
lines changed

1 file changed

+45
-0
lines changed

src/util/lazy.h

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
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, typename infot>
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(infot)> fun)
22+
{
23+
return lazyt{std::move(fun)};
24+
}
25+
26+
/// Force the computation of the value. If it was already computed (even if
27+
/// \p info was different), return the same result.
28+
valuet force(infot info)
29+
{
30+
if(value)
31+
return *value;
32+
value = evaluation_function(info);
33+
return *value;
34+
}
35+
36+
private:
37+
optionalt<valuet> value;
38+
std::function<valuet(infot)> evaluation_function;
39+
40+
explicit lazyt(std::function<valuet(infot)> fun)
41+
: evaluation_function(std::move(fun))
42+
{ }
43+
};
44+
45+
#endif // CPROVER_UTIL_LAZY_H

0 commit comments

Comments
 (0)