Add 'Basic' and 'Advanced' minimal examples to documentation

docs/Doxyfile.in

@@ -867,6 +867,8 @@ WARN_LOGFILE           =
 INPUT                  = @CMAKE_SOURCE_DIR@/docs/index.md \
                          @CMAKE_SOURCE_DIR@/docs/getting_started.md \
                          @CMAKE_SOURCE_DIR@/docs/examples/ \
+                         @CMAKE_SOURCE_DIR@/docs/examples/basic.md \
+                         @CMAKE_SOURCE_DIR@/docs/examples/advanced.md \
                          @CMAKE_SOURCE_DIR@/docs/examples/builder.md \
                          @CMAKE_SOURCE_DIR@/docs/examples.md \
                          @CMAKE_SOURCE_DIR@/docs/papers/ \

docs/examples.md

@@ -1,11 +1,24 @@
 \page page__examples Examples
 
 The following examples provide an introduction to using all aspects of Adiar.
+These examples only cover \ref module__bdd (`adiar::bdd`) but the ideas presented
+here also apply to \ref module__zdd (`adiar::zdd`).
 
-- See \ref page__getting_started for how to compile, initialize and deinitialize
-  Adiar.
+- \ref page__getting_started
 
-- \subpage page__builder "Manual Construction"
+  How to compile, initialize and deinitialize the Adiar library.
+
+- \subpage page__basic
+
+  Basic operations for creating and manipulating decision diagrams.
+
+- \subpage page__advanced
+
+  Advanced variants of operations for creating and manipulating decision
+  diagrams.
+
+- \subpage page__builder
+
+  Use of `adiar::builder` to manually construct a decision diagram,  node for
+  node.
 
-  Use of `adiar::builder` to manually construct a `adiar::bdd` and `adiar::zdd`
-  node for node.

docs/examples/advanced.md

@@ -0,0 +1,90 @@
+\page page__advanced Advanced Usage
+
+\ref page__basic contained examples of the basic version of most BDD operations.
+For more advanced usage, one needs to use \ref module__functional as a bridge
+between your code and Adiar.
+
+Predicates
+===============================
+
+An `adiar::predicate<T>` is a function that given a value of some type `T`
+returns a `bool`. For example, the following *lambda* is a predicate for whether
+a BDD variable is odd.
+
+```cpp
+const auto is_odd = [](int x) -> bool { return x % 2; };
+```
+
+In \ref page__basic, we showed how to use it to quantify a single variable. You
+can parse the above predicate to `adiar::bdd_exists` to quantify all odd variables
+at once.
+
+```cpp
+adiar::bdd res = adiar::bdd_exists(f, is_odd);
+```
+
+The function `adiar::bdd_eval` can also take a predicate as its argument.
+
+Generators
+===============================
+
+As part of your program, you most likely store the to-be quantified variables
+somewhere. The *idiomatic* way in C++ to interact with data structures is to use
+*iterators*. A data structure can be parsed directly to Adiar's operations, if
+it can provide its data in the same order as they need to be consumed by the BDD
+operation. In the case of `adiar::bdd_exists`, the iterator's data has to be in
+*descending* order.
+
+```cpp
+std::vector<int> xs = { 6, 4, 2, 0 };
+
+adiar::bdd res = adiar::bdd_exists(f, xs.begin(), xs.end());
+```
+
+Under the hood, Adiar wraps the iterator-pair into an `adiar::generator<int>` -
+a stateful function that when called provides an `adiar::optional<int>` of the
+next value. Hence, we can also do the same as above with the following *lambda*
+function.
+
+```cpp
+int x = 8;
+
+const auto gen = [&x]() -> int {
+  if (x == 0) { return adiar::make_optional<int>(); }
+  return x -= 2;
+};
+
+adiar::bdd res = adiar::bdd_exists(f, gen);
+```
+
+Similarly, one can parse an (*ascending*) iterator or generator
+`adiar::bdd_restrict` to restrict multiple variables. Doing so is going to be
+significantly faster.
+
+Consumers
+===============================
+
+Reversely, one can also parse information from Adiar's algorithms back into
+one's own data structures in the idiomatic C++ way, i.e. with a pair of
+*iterators*. For example, below we use `adiar::bdd_support` to copy the
+variables in a BDD into a vector (in *ascending* order).
+
+```cpp
+std::vector<int> xs(adiar::bdd_varcount(f));
+
+adiar::bdd_support(f, xs.begin(), xs.end());
+```
+
+Under the hood, Adiar wraps the iterator-pair into an `adiar::consumer<int>` - a
+*callback* function that consumes the result. For example, we can print the
+entire result to the console with the following *lambda* function.
+
+```cpp
+const auto con = [](int x) -> void {
+ std::cout << x << "\n";
+};
+adiar::bdd_support(f, con);
+```
+
+Similarly, one can obtain the satisfying assignment of `adiar::bdd_satmin` and
+`adiar::bdd_satmax` with iterators and/or consumer functions.