Merge pull request #5090 from romainbrenguier/feature/lazy

Add a lazyt class for delaying computations

Author: romainbrenguier

src/util/lazy.h

@@ -0,0 +1,46 @@
+/*******************************************************************\
+
+Module: Util
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_LAZY_H
+#define CPROVER_UTIL_LAZY_H
+
+#include <functional>
+#include <util/optional.h>
+
+template <typename valuet>
+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<valuet()> 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<valuet> value;
+  std::function<valuet()> evaluation_function;
+
+  explicit lazyt(std::function<valuet()> fun)
+    : evaluation_function(std::move(fun))
+  {
+  }
+};
+
+#endif // CPROVER_UTIL_LAZY_H

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 \

unit/util/lazy.cpp

@@ -0,0 +1,29 @@
+/*******************************************************************\
+
+Module: Unit tests for lazy
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+#include <testing-utils/use_catch.h>
+#include <util/lazy.h>
+
+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<int>::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);
+}