diff --git a/src/util/lazy.h b/src/util/lazy.h new file mode 100644 index 00000000000..dc1d35db937 --- /dev/null +++ b/src/util/lazy.h @@ -0,0 +1,46 @@ +/*******************************************************************\ + +Module: Util + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_LAZY_H +#define CPROVER_UTIL_LAZY_H + +#include +#include + +template +class lazyt +{ +public: + /// Delay the computation of \p fun to the next time the \c force method + /// is called. + static lazyt from_fun(std::function fun) + { + return lazyt{std::move(fun)}; + } + + /// Force the computation of the value. If it was already computed, + /// return the same result. + valuet force() + { + if(value) + return *value; + value = evaluation_function(); + return *value; + } + +private: + optionalt value; + std::function evaluation_function; + + explicit lazyt(std::function fun) + : evaluation_function(std::move(fun)) + { + } +}; + +#endif // CPROVER_UTIL_LAZY_H diff --git a/unit/Makefile b/unit/Makefile index 760972db0c9..6d28521199e 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -74,6 +74,7 @@ SRC += analyses/ai/ai.cpp \ util/irep_sharing.cpp \ util/json_array.cpp \ util/json_object.cpp \ + util/lazy.cpp \ util/memory_info.cpp \ util/message.cpp \ util/optional.cpp \ diff --git a/unit/util/lazy.cpp b/unit/util/lazy.cpp new file mode 100644 index 00000000000..757a02aedd2 --- /dev/null +++ b/unit/util/lazy.cpp @@ -0,0 +1,29 @@ +/*******************************************************************\ + +Module: Unit tests for lazy + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +#include +#include + +SCENARIO("lazy test", "[core][util][lazy]") +{ + std::size_t call_counter = 0; + auto length_with_counter = [&call_counter](const std::string &s) { + ++call_counter; + return s.length(); + }; + auto lazy_length = + lazyt::from_fun([&]() { return length_with_counter("foo"); }); + + REQUIRE(call_counter == 0); + auto result = lazy_length.force(); + REQUIRE(call_counter == 1); + REQUIRE(result == 3); + result = lazy_length.force(); + REQUIRE(call_counter == 1); + REQUIRE(result == 3); +}