From 80bc2684448ede38d898d95c9cb2d596da4c9e1c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Sun, 5 Apr 2026 13:25:13 +0200 Subject: [PATCH 1/7] Hide overloads with 'exec_policy' for BDDs --- src/adiar/bdd.h | 123 ++++++++++++++++++++++++++++++++---------------- 1 file changed, 83 insertions(+), 40 deletions(-) diff --git a/src/adiar/bdd.h b/src/adiar/bdd.h index d658d0a66..70416b788 100644 --- a/src/adiar/bdd.h +++ b/src/adiar/bdd.h @@ -10,6 +10,13 @@ /// The \ref bdd class takes care of reference counting and optimal garbage collection of the /// underlying files. To ensure the most disk-space is available, try to release your \ref bdd /// objects as quickly as possible and/or minimise the number of lvalues of said type. +/// +/// To construct a more complex but well-structured \ref bdd by hand, please +/// use the \ref bdd_builder (see \ref builder) instead. +/// +/// An \ref exec_policy can be provided as an optional *first* argument for (most) of the functions +/// that follow. This provides you with the ability to change settings on the algorithm execution, +/// e.g. the type of priority queue and algorithm used. //////////////////////////////////////////////////////////////////////////////////////////////////// #include @@ -28,9 +35,6 @@ namespace adiar ////////////////////////////////////////////////////////////////////////////////////////////////// /// \addtogroup module__bdd Basic Constructors /// - /// To construct a more complex but well-structured \ref bdd by hand, please - /// use the \ref bdd_builder (see \ref builder) instead. - /// /// \{ ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -361,11 +365,13 @@ namespace adiar __bdd bdd_apply(const bdd& f, const bdd& g, const predicate& op); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Apply a binary operator between two BDDs. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_apply(const exec_policy& ep, const bdd& f, const bdd& g, const predicate& op); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'and' operator. @@ -377,11 +383,13 @@ namespace adiar __bdd bdd_and(const bdd& f, const bdd& g); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'and' operator. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_and(const exec_policy& ep, const bdd& f, const bdd& g); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \see bdd_and @@ -423,11 +431,13 @@ namespace adiar __bdd bdd_nand(const bdd& f, const bdd& g); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'nand' operator. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_nand(const exec_policy& ep, const bdd& f, const bdd& g); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'or' operator. @@ -439,11 +449,13 @@ namespace adiar __bdd bdd_or(const bdd& f, const bdd& g); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'or' operator. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_or(const exec_policy& ep, const bdd& f, const bdd& g); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \see bdd_or @@ -499,11 +511,13 @@ namespace adiar __bdd bdd_nor(const bdd& f, const bdd& g); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'nor' operator. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_nor(const exec_policy& ep, const bdd& f, const bdd& g); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'xor' operator. @@ -515,11 +529,13 @@ namespace adiar __bdd bdd_xor(const bdd& f, const bdd& g); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'xor' operator. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_xor(const exec_policy& ep, const bdd& f, const bdd& g); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \see bdd_xor @@ -546,11 +562,14 @@ namespace adiar __bdd bdd_xnor(const bdd& f, const bdd& g); + + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Logical 'xnor' operator. + /// \brief Logical 'xnor' operator. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_xnor(const exec_policy& ep, const bdd& f, const bdd& g); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'implication' operator. @@ -562,11 +581,13 @@ namespace adiar __bdd bdd_imp(const bdd& f, const bdd& g); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'implication' operator. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_imp(const exec_policy& ep, const bdd& f, const bdd& g); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'inverse implication' operator. @@ -578,11 +599,13 @@ namespace adiar __bdd bdd_invimp(const bdd& f, const bdd& g); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'inverse implication' operator. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_invimp(const exec_policy& ep, const bdd& f, const bdd& g); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'equivalence' operator. @@ -594,11 +617,13 @@ namespace adiar __bdd bdd_equiv(const bdd& f, const bdd& g); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'equivalence' operator. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_equiv(const exec_policy& ep, const bdd& f, const bdd& g); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'difference' operator. @@ -610,11 +635,13 @@ namespace adiar __bdd bdd_diff(const bdd& f, const bdd& g); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'difference' operator. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_diff(const exec_policy& ep, const bdd& f, const bdd& g); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \remark Unary difference subtracts from \f$ \top \f$ value, making its equivalent to negation. @@ -654,11 +681,13 @@ namespace adiar __bdd bdd_less(const bdd& f, const bdd& g); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'less than' operator. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_less(const exec_policy& ep, const bdd& f, const bdd& g); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief If-Then-Else operator. @@ -686,11 +715,13 @@ namespace adiar __bdd bdd_ite(const bdd& f, const bdd& g, const bdd& h); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief If-Then-Else operator. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_ite(const exec_policy& ep, const bdd& f, const bdd& g, const bdd& h); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Restrict a single variable to a constant value. @@ -711,11 +742,13 @@ namespace adiar __bdd bdd_restrict(const bdd& f, bdd::label_type var, bool val); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Restrict a single variable to a constant value. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_restrict(const exec_policy& ep, const bdd& f, bdd::label_type var, bool val); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Restrict a subset of variables to constant values. @@ -735,6 +768,7 @@ namespace adiar __bdd bdd_restrict(const bdd& f, const generator>& xs); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Restrict a subset of variables to constant values. ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -742,6 +776,7 @@ namespace adiar bdd_restrict(const exec_policy& ep, const bdd& f, const generator>& xs); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Restrict a subset of variables to constant values. @@ -768,6 +803,7 @@ namespace adiar return bdd_restrict(f, make_generator(begin, end)); } + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Restrict a subset of variables to constant values. ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -777,6 +813,7 @@ namespace adiar { return bdd_restrict(ep, f, make_generator(begin, end)); } + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Restrict the root to `false`, i.e. follow its low edge. @@ -792,11 +829,13 @@ namespace adiar __bdd bdd_low(const bdd& f); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Restrict the root to `false`, i.e. follow its low edge. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_low(const exec_policy& ep, const bdd& f); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Restrict the root to `true`, i.e. follow its high edge. @@ -812,11 +851,13 @@ namespace adiar __bdd bdd_high(const bdd& f); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Restrict the root to `true`, i.e. follow its high edge. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_high(const exec_policy& ep, const bdd& f); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Existential quantification of a single variable. @@ -846,16 +887,12 @@ namespace adiar return bdd_exists(f, var); } - /// \endcond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Existential quantification of a single variable. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_exists(const exec_policy& ep, const bdd& f, bdd::label_type var); - /// \cond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Existential quantification of a single variable. ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -904,16 +941,12 @@ namespace adiar __bdd bdd_exists(__bdd&& f, const predicate& vars); - /// \endcond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Existential quantification of multiple variables. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_exists(const exec_policy& ep, const bdd& f, const predicate& vars); - /// \cond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Existential quantification of multiple variables. /// @@ -971,16 +1004,12 @@ namespace adiar __bdd bdd_exists(__bdd&& f, const generator& vars); - /// \endcond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Existential quantification of multiple variables. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_exists(const exec_policy& ep, const bdd& f, const generator& vars); - /// \cond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Existential quantification of multiple variables. /// @@ -1053,8 +1082,6 @@ namespace adiar return bdd_exists(std::move(f), make_generator(begin, end)); } - /// \endcond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Existential quantification of multiple variables. ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -1065,8 +1092,6 @@ namespace adiar return bdd_exists(ep, f, make_generator(begin, end)); } - /// \cond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Existential quantification of multiple variables. /// @@ -1124,16 +1149,12 @@ namespace adiar return bdd_forall(f, var); } - /// \endcond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Forall quantification of a single variable. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_forall(const exec_policy& ep, const bdd& f, bdd::label_type var); - /// \cond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Forall quantification of a single variable. ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -1182,16 +1203,12 @@ namespace adiar __bdd bdd_forall(__bdd&& f, const predicate& vars); - /// \endcond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Forall quantification of multiple variables. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_forall(const exec_policy& ep, const bdd& f, const predicate& vars); - /// \cond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Forall quantification of multiple variables. /// @@ -1249,16 +1266,12 @@ namespace adiar __bdd bdd_forall(bdd&& f, const generator& vars); - /// \endcond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Forall quantification of multiple variables. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_forall(const exec_policy& ep, const bdd& f, const generator& vars); - /// \cond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Forall quantification of multiple variables. /// @@ -1331,8 +1344,6 @@ namespace adiar return bdd_forall(std::move(f), make_generator(begin, end)); } - /// \endcond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Forall quantification of multiple variables. ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -1343,8 +1354,6 @@ namespace adiar return bdd_forall(ep, f, make_generator(begin, end)); } - /// \cond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Forall quantification of multiple variables. /// @@ -1402,6 +1411,8 @@ namespace adiar const function& m, replace_type m_type = replace_type::Auto); + /// \cond + ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Replace variables in *f* according to the mapping in *m*. ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -1411,8 +1422,6 @@ namespace adiar const function& m, replace_type m_type = replace_type::Auto); - /// \cond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Replace variables in *f* according to the mapping in *m*. /// @@ -1470,6 +1479,7 @@ namespace adiar bdd bdd_relprod(const bdd& states, const bdd& relation, const predicate& pred); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Relational Product of *states* and a *relation*. ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -1478,6 +1488,7 @@ namespace adiar const bdd& states, const bdd& relation, const predicate& pred); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Forwards step with the Relational Product, including relabelling. @@ -1508,6 +1519,7 @@ namespace adiar const function(bdd::label_type)>& m, replace_type m_type = replace_type::Auto); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Forwards step with the Relational Product, including relabelling. ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -1517,6 +1529,7 @@ namespace adiar const bdd& relation, const function(bdd::label_type)>& m, replace_type m_type = replace_type::Auto); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Forwards step with the Relational Product for *disjoint* variable orderings, @@ -1537,6 +1550,7 @@ namespace adiar bdd bdd_relnext(const bdd& states, const bdd& relation, const bdd::label_type varcount); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Forwards step with the Relational Product for *disjoint* variable orderings, /// including relabelling. @@ -1546,6 +1560,7 @@ namespace adiar const bdd& states, const bdd& relation, const bdd::label_type varcount); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Forwards step with the Relational Product for *interleaved* variable orderings, @@ -1565,12 +1580,14 @@ namespace adiar bdd bdd_relnext(const bdd& states, const bdd& relation); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Forwards step with the Relational Product for *interleaved* variable orderings, /// including relabelling. ////////////////////////////////////////////////////////////////////////////////////////////////// bdd bdd_relnext(const exec_policy& ep, const bdd& states, const bdd& relation); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Backwards step with the Relational Product, including relabelling. @@ -1602,6 +1619,7 @@ namespace adiar const function(bdd::label_type)>& m, replace_type m_type = replace_type::Auto); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Backwards step with the Relational Product, including relabelling. ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -1611,6 +1629,7 @@ namespace adiar const bdd& relation, const function(bdd::label_type)>& m, replace_type m_type = replace_type::Auto); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Backwards step with the Relational Product for *disjoint* variable orderings, @@ -1631,6 +1650,7 @@ namespace adiar bdd bdd_relprev(const bdd& states, const bdd& relation, const bdd::label_type varcount); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Backwards step with the Relational Product for *disjoint* variable orderings, /// including relabelling. @@ -1640,6 +1660,7 @@ namespace adiar const bdd& states, const bdd& relation, const bdd::label_type varcount); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Backwards step with the Relational Product for *interleaved* variable orderings, @@ -1658,12 +1679,14 @@ namespace adiar bdd bdd_relprev(const bdd& states, const bdd& relation); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Backwards step with the Relational Product for *interleaved* variable orderings, /// including relabelling. ////////////////////////////////////////////////////////////////////////////////////////////////// bdd bdd_relprev(const exec_policy& ep, const bdd& states, const bdd& relation); + /// \endcond /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -1763,11 +1786,13 @@ namespace adiar bool bdd_equal(const bdd& f, const bdd& g); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Whether the two BDDs represent the same function. ////////////////////////////////////////////////////////////////////////////////////////////////// bool bdd_equal(const exec_policy&, const bdd& f, const bdd& g); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \see bdd_equal @@ -1796,11 +1821,13 @@ namespace adiar bool bdd_unequal(const bdd& f, const bdd& g); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Whether the two BDDs represent different functions. ////////////////////////////////////////////////////////////////////////////////////////////////// bool bdd_unequal(const exec_policy& ep, const bdd& f, const bdd& g); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \see bdd_equal bdd_unequal @@ -1846,11 +1873,13 @@ namespace adiar uint64_t bdd_pathcount(const bdd& f); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Count all unique (but not necessarily disjoint) paths to the true terminal. ////////////////////////////////////////////////////////////////////////////////////////////////// uint64_t bdd_pathcount(const exec_policy& ep, const bdd& f); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Count the number of assignments x that make f(x) true. @@ -1869,11 +1898,13 @@ namespace adiar uint64_t bdd_satcount(const bdd& f, bdd::label_type varcount); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Count the number of assignments x that make f(x) true. ////////////////////////////////////////////////////////////////////////////////////////////////// uint64_t bdd_satcount(const exec_policy& ep, const bdd& f, bdd::label_type varcount); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Count the number of assignments x that make f(x) true. @@ -1886,11 +1917,13 @@ namespace adiar uint64_t bdd_satcount(const bdd& f); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Count the number of assignments *x that make f(x) true. + /// \brief Count the number of assignments *x that make f(x) true. ////////////////////////////////////////////////////////////////////////////////////////////////// uint64_t bdd_satcount(const exec_policy& ep, const bdd& f); + /// \endcond /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -2171,12 +2204,14 @@ namespace adiar pair bdd_optmin(const bdd& f, const cost& c); + /// \cond //////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief obtain the satisfying assignment that is minimal for the given linear cost function + /// \brief Obtain the satisfying assignment that is minimal for the given linear cost function /// over the global domain. //////////////////////////////////////////////////////////////////////////////////////////////////// pair bdd_optmin(const exec_policy& ep, const bdd& f, const cost& c); + /// \endcond //////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Obtain the satisfying assignment that is minimal for the given linear cost function @@ -2200,6 +2235,7 @@ namespace adiar const cost& c, const consumer>& cb); + /// \cond //////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Obtain the satisfying assignment that is minimal for the given linear cost function /// over the global domain. @@ -2209,6 +2245,7 @@ namespace adiar const bdd& f, const cost& c, const consumer>& cb); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Evaluate a BDD according to an assignment to its variables. @@ -2292,12 +2329,14 @@ namespace adiar __bdd bdd_from(const zdd& A, const generator& dom); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Obtains the BDD that represents the same function/set as the given ZDD within the given /// domain. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_from(const exec_policy& ep, const zdd& A, const generator& dom); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Obtains the BDD that represents the same function/set as the given ZDD within the given @@ -2322,6 +2361,7 @@ namespace adiar return bdd_from(A, make_generator(begin, end)); } + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Obtains the BDD that represents the same function/set as the given ZDD within the given /// domain. @@ -2332,6 +2372,7 @@ namespace adiar { return bdd_from(ep, A, make_generator(begin, end)); } + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Obtains the BDD that represents the same function/set as the given ZDD within the @@ -2350,12 +2391,14 @@ namespace adiar __bdd bdd_from(const zdd& A); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Obtains the BDD that represents the same function/set as the given ZDD within the /// global domain. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_from(const exec_policy& ep, const zdd& A); + /// \endcond /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// From 10788c24e6f2f6749b04ecddf65d52a80fff495d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Sun, 5 Apr 2026 13:29:54 +0200 Subject: [PATCH 2/7] Hide overloads with 'exec_policy' for ZDDs --- src/adiar/zdd.h | 79 +++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 64 insertions(+), 15 deletions(-) diff --git a/src/adiar/zdd.h b/src/adiar/zdd.h index 1a4bbb93c..8b83e9de1 100644 --- a/src/adiar/zdd.h +++ b/src/adiar/zdd.h @@ -10,6 +10,13 @@ /// The \ref zdd class takes care of reference counting and optimal garbage collection of the /// underlying files. To ensure the most disk-space is available, try to garbage collect the \ref /// zdd objects as quickly as possible and/or minimise the number of lvalues of said type. +/// +/// To construct a more complex but well-structured \ref zdd by hand, please use the \ref +/// zdd_builder (see \ref builder) instead. +/// +/// An \ref exec_policy can be provided as an optional *first* argument for (most) of the functions +/// that follow. This provides you with the ability to change settings on the algorithm execution, +/// e.g. the type of priority queue and algorithm used. //////////////////////////////////////////////////////////////////////////////////////////////////// #include @@ -26,9 +33,6 @@ namespace adiar ////////////////////////////////////////////////////////////////////////////////////////////////// /// \addtogroup module__zdd Basic Constructors /// - /// To construct a more complex but well-structured \ref zdd by hand, please use the \ref - /// zdd_builder (see \ref builder) instead. - /// /// \{ ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -433,11 +437,13 @@ namespace adiar __zdd zdd_binop(const zdd& A, const zdd& B, const predicate& op); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Apply a binary operator between the sets of two families. ////////////////////////////////////////////////////////////////////////////////////////////////// __zdd zdd_binop(const exec_policy& ep, const zdd& A, const zdd& B, const predicate& op); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief The union of two families of sets. @@ -447,11 +453,13 @@ namespace adiar __zdd zdd_union(const zdd& A, const zdd& B); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief The union of two families of sets. ////////////////////////////////////////////////////////////////////////////////////////////////// __zdd zdd_union(const exec_policy& ep, const zdd& A, const zdd& B); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \see zdd_union @@ -499,11 +507,13 @@ namespace adiar __zdd zdd_intsec(const zdd& A, const zdd& B); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief The intersection of two families of sets. ////////////////////////////////////////////////////////////////////////////////////////////////// __zdd zdd_intsec(const exec_policy& ep, const zdd& A, const zdd& B); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \see zdd_intsec @@ -543,11 +553,13 @@ namespace adiar __zdd zdd_diff(const zdd& A, const zdd& B); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief The set difference of two families of sets. ////////////////////////////////////////////////////////////////////////////////////////////////// __zdd zdd_diff(const exec_policy& ep, const zdd& A, const zdd& B); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \remark Unary difference subtracts from universe over all variables in th global \ref @@ -593,11 +605,13 @@ namespace adiar __zdd zdd_change(const zdd& A, const generator& vars); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief The symmetric difference between each set in the family and the given set of variables. ////////////////////////////////////////////////////////////////////////////////////////////////// __zdd zdd_change(const exec_policy& ep, const zdd& A, const generator& vars); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief The symmetric difference between each set in the family and the given set of variables. @@ -621,6 +635,7 @@ namespace adiar return zdd_change(A, make_generator(begin, end)); } + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief The symmetric difference between each set in the family and the given set of variables. ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -630,6 +645,7 @@ namespace adiar { return zdd_change(ep, A, make_generator(begin, end)); } + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Complement of A within the given domain. @@ -645,11 +661,13 @@ namespace adiar __zdd zdd_complement(const zdd& A, const generator& dom); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Complement of A within the given domain. ////////////////////////////////////////////////////////////////////////////////////////////////// __zdd zdd_complement(const exec_policy& ep, const zdd& A, const generator& dom); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Complement of A within the given domain. @@ -673,6 +691,7 @@ namespace adiar return zdd_complement(A, make_generator(begin, end)); } + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Complement of A within the given domain. ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -682,6 +701,7 @@ namespace adiar { return zdd_complement(ep, A, make_generator(begin, end)); } + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Complement of A within the global \ref module__domain @@ -699,11 +719,14 @@ namespace adiar __zdd zdd_complement(const zdd& A); + + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Complement of A within the global \ref module__domain ////////////////////////////////////////////////////////////////////////////////////////////////// __zdd zdd_complement(const exec_policy& ep, const zdd& A); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \see zdd_complement @@ -734,11 +757,13 @@ namespace adiar __zdd zdd_expand(const zdd& A, const generator& vars); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Expands the domain of the given ZDD to also include the given set of labels. ////////////////////////////////////////////////////////////////////////////////////////////////// __zdd zdd_expand(const exec_policy& ep, const zdd& A, const generator& vars); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Expands the domain of the given ZDD to also include the given set of labels. @@ -766,6 +791,7 @@ namespace adiar return zdd_expand(A, make_generator(begin, end)); } + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Expands the domain of the given ZDD to also include the given set of labels. ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -775,6 +801,7 @@ namespace adiar { return zdd_expand(ep, A, make_generator(begin, end)); } + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Subset that do \em not include the given element. @@ -790,11 +817,13 @@ namespace adiar __zdd zdd_offset(const zdd& A, zdd::label_type var); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Subset that do \em not include the given element. ////////////////////////////////////////////////////////////////////////////////////////////////// __zdd zdd_offset(const exec_policy& ep, const zdd& A, zdd::label_type var); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Subset that do \em not include the top variable. @@ -811,11 +840,13 @@ namespace adiar __zdd zdd_offset(const zdd& A); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Subset that do \em not include the top variable. ////////////////////////////////////////////////////////////////////////////////////////////////// __zdd zdd_offset(const exec_policy& ep, const zdd& A); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Subset that do \em not include the given set of variables. @@ -832,11 +863,13 @@ namespace adiar __zdd zdd_offset(const zdd& A, const generator& vars); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Subset that do \em not include the given set of variables. ////////////////////////////////////////////////////////////////////////////////////////////////// __zdd zdd_offset(const exec_policy& ep, const zdd& A, const generator& vars); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Subset that do \em not include the given set of variables. @@ -860,6 +893,7 @@ namespace adiar return zdd_offset(A, make_generator(begin, end)); } + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Subset that do \em not include the given set of variables. ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -869,6 +903,7 @@ namespace adiar { return zdd_offset(ep, A, make_generator(begin, end)); } + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Subset that \em do include the given element. @@ -884,11 +919,13 @@ namespace adiar __zdd zdd_onset(const zdd& A, zdd::label_type var); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Subset that \em do include the given element. ////////////////////////////////////////////////////////////////////////////////////////////////// __zdd zdd_onset(const exec_policy& ep, const zdd& A, zdd::label_type var); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Subset that \em do include the top variable. @@ -905,11 +942,13 @@ namespace adiar __zdd zdd_onset(const zdd& A); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Subset that \em do include the top variable. ////////////////////////////////////////////////////////////////////////////////////////////////// __zdd zdd_onset(const exec_policy& ep, const zdd& A); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Subset that \em do include the given set of variables. @@ -926,11 +965,13 @@ namespace adiar __zdd zdd_onset(const zdd& A, const generator& vars); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Subset that \em do include the given set of variables. ////////////////////////////////////////////////////////////////////////////////////////////////// __zdd zdd_onset(const exec_policy& ep, const zdd& A, const generator& vars); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Subset that \em do include the given set of variables. @@ -954,6 +995,7 @@ namespace adiar return zdd_onset(A, make_generator(begin, end)); } + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Subset that \em do include the given set of variables. ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -963,6 +1005,7 @@ namespace adiar { return zdd_onset(ep, A, make_generator(begin, end)); } + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Project family of sets onto a domain, i.e. remove from every set all variables not @@ -1004,8 +1047,6 @@ namespace adiar __zdd zdd_project(__zdd&& A, const predicate& dom); - /// \endcond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Project family of sets onto a domain, i.e. remove from every set all variables not /// within the domain. @@ -1013,8 +1054,6 @@ namespace adiar __zdd zdd_project(const exec_policy& ep, const zdd& A, const predicate& dom); - /// \cond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Project family of sets onto a domain, i.e. remove from every set all variables not /// within the domain. @@ -1079,8 +1118,6 @@ namespace adiar __zdd zdd_project(__zdd&& A, const generator& dom); - /// \endcond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Project family of sets onto a domain, i.e. remove from every set all variables not /// within the domain. @@ -1088,8 +1125,6 @@ namespace adiar __zdd zdd_project(const exec_policy& ep, const zdd& A, const generator& dom); - /// \cond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Project family of sets onto a domain, i.e. remove from every set all variables not /// within the domain. @@ -1169,8 +1204,6 @@ namespace adiar return zdd_project(std::move(A), make_generator(begin, end)); } - /// \endcond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Project family of sets onto a domain, i.e. remove from every set all variables not /// within the domain. @@ -1182,8 +1215,6 @@ namespace adiar return zdd_project(ep, A, make_generator(begin, end)); } - /// \cond - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Project family of sets onto a domain, i.e. remove from every set all variables not /// within the domain. @@ -1285,11 +1316,13 @@ namespace adiar bool zdd_equal(const zdd& A, const zdd& B); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Whether they represent the same family. ////////////////////////////////////////////////////////////////////////////////////////////////// bool zdd_equal(const exec_policy& ep, const zdd& A, const zdd& B); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \see zdd_equal @@ -1312,11 +1345,13 @@ namespace adiar bool zdd_unequal(const zdd& A, const zdd& B); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Whether they represent two different families. ////////////////////////////////////////////////////////////////////////////////////////////////// bool zdd_unequal(const exec_policy& ep, const zdd& A, const zdd& B); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \see zdd_unequal @@ -1339,11 +1374,13 @@ namespace adiar bool zdd_subseteq(const zdd& A, const zdd& B); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Whether one family is a subset or equal to the other. ////////////////////////////////////////////////////////////////////////////////////////////////// bool zdd_subseteq(const exec_policy& ep, const zdd& A, const zdd& B); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \see zdd_subseteq @@ -1381,11 +1418,13 @@ namespace adiar bool zdd_subset(const zdd& A, const zdd& B); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Whether one family is a strict subset of the other. ////////////////////////////////////////////////////////////////////////////////////////////////// bool zdd_subset(const exec_policy& ep, const zdd& A, const zdd& B); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \see zdd_subset @@ -1423,11 +1462,13 @@ namespace adiar bool zdd_disjoint(const zdd& A, const zdd& B); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Whether the two families are disjoint. ////////////////////////////////////////////////////////////////////////////////////////////////// bool zdd_disjoint(const exec_policy& ep, const zdd& A, const zdd& B); + /// \endcond /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -1456,11 +1497,13 @@ namespace adiar uint64_t zdd_size(const zdd& A); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief The number of sets in the family of sets. ////////////////////////////////////////////////////////////////////////////////////////////////// uint64_t zdd_size(const exec_policy& ep, const zdd& A); + /// \endcond /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -1684,12 +1727,14 @@ namespace adiar __zdd zdd_from(const bdd& f, const generator& dom); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Obtains the ZDD that represents the same function/set as the given /// BDD within the given domain. ////////////////////////////////////////////////////////////////////////////////////////////////// __zdd zdd_from(const exec_policy& ep, const bdd& f, const generator& dom); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Obtains the ZDD that represents the same function/set as the given BDD within the given @@ -1714,6 +1759,7 @@ namespace adiar return zdd_from(f, make_generator(begin, end)); } + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Obtains the ZDD that represents the same function/set as the given BDD within the given /// domain. @@ -1724,6 +1770,7 @@ namespace adiar { return zdd_from(ep, f, make_generator(begin, end)); } + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Obtains the ZDD that represents the same function/set as the given BDD within the @@ -1740,12 +1787,14 @@ namespace adiar __zdd zdd_from(const bdd& f); + /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Obtains the BDD that represents the same function/set as the given /// ZDD within the global domain. ////////////////////////////////////////////////////////////////////////////////////////////////// __zdd zdd_from(const exec_policy& ep, const bdd& f); + /// \endcond /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// From a55a7654537b9cc57aca324dedb8df6a3ffec77f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Sun, 5 Apr 2026 13:39:11 +0200 Subject: [PATCH 3/7] Reformat BDD documentation --- src/adiar/bdd.h | 102 ++++++++++++++++++++++++------------------------ 1 file changed, 51 insertions(+), 51 deletions(-) diff --git a/src/adiar/bdd.h b/src/adiar/bdd.h index 70416b788..7ed946607 100644 --- a/src/adiar/bdd.h +++ b/src/adiar/bdd.h @@ -49,7 +49,7 @@ namespace adiar bdd_const(bool value); ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The BDD representing the given constant value. + /// \brief The BDD representing the given constant value. /// /// \param value /// The constant boolean (terminal) value @@ -132,8 +132,8 @@ namespace adiar bdd_nithvar(bdd::label_type var); ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The BDD representing the logical 'and' of all the given variables, i.e. a *term* of - /// variables. + /// \brief The BDD representing the logical 'and' of all the given variables, i.e. a *term* of + /// variables. /// /// \details Any negative labels provided by the generator are interpreted as the negation of /// said variable. @@ -165,8 +165,8 @@ namespace adiar bdd_and(const generator>& vars); ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The BDD representing the logical 'and' of all the given variables, i.e. a *term* of - /// variables. + /// \brief The BDD representing the logical 'and' of all the given variables, i.e. a *term* of + /// variables. /// /// \details Any negative labels provided by the generator are interpreted as the negation of said /// variable. @@ -190,8 +190,8 @@ namespace adiar } ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The BDD representing the logical 'or' of all the given variables, i.e. a *clause* of - /// variables. + /// \brief The BDD representing the logical 'or' of all the given variables, i.e. a *clause* of + /// variables. /// /// \details Any negative labels provided by the generator are interpreted as the negation of said /// variable. @@ -208,8 +208,8 @@ namespace adiar bdd_or(const generator& vars); ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The BDD representing the logical 'or' of all the given variables, i.e. a *clause* - /// of variables. + /// \brief The BDD representing the logical 'or' of all the given variables, i.e. a *clause* of + /// variables. /// /// \param vars /// Generator of pairs (label, negated) in \em descending order. These values can at most be @@ -223,8 +223,8 @@ namespace adiar bdd_or(const generator>& vars); ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The BDD representing the logical 'or' of all the given variables, i.e. a *clause* of - /// variables. + /// \brief The BDD representing the logical 'or' of all the given variables, i.e. a *clause* of + /// variables. /// /// \details Any negative labels provided by the generator are interpreted as the negation of said /// variable. @@ -248,10 +248,10 @@ namespace adiar } ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The BDD representing the cube of all the given variables. + /// \brief The BDD representing the cube of all the given variables. /// - /// \details Any negative labels provided by the generator are interpreted as the negation of - /// said variable. + /// \details Any negative labels provided by the generator are interpreted as the negation of said + /// variable. /// /// \param vars /// Generator of labels of variables in \em descending order. These values can at most be @@ -283,7 +283,7 @@ namespace adiar bdd_cube(const generator>& vars); ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The BDD representing the cube of all the given variables. + /// \brief The BDD representing the cube of all the given variables. /// /// \details Any negative labels provided by the generator are interpreted as the negation of said /// variable. @@ -317,7 +317,7 @@ namespace adiar /// \{ ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Negation of a BDD. + /// \brief Negation of a BDD. /// /// \details Flips the negation flag such that reading nodes with a `node_stream` within Adiar's /// algorithms will on-the-fly change the `false` terminals into the `true` terminals and @@ -513,7 +513,7 @@ namespace adiar /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Logical 'nor' operator. + /// \brief Logical 'nor' operator. ////////////////////////////////////////////////////////////////////////////////////////////////// __bdd bdd_nor(const exec_policy& ep, const bdd& f, const bdd& g); @@ -690,7 +690,7 @@ namespace adiar /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief If-Then-Else operator. + /// \brief If-Then-Else operator. /// /// \details Computes the BDD expressing \f$ f ? g : h \f$ more efficient than computing \f$ (f /// \land g) \lor (\neg f \land h) \f$ with `bdd_apply`. @@ -724,7 +724,7 @@ namespace adiar /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Restrict a single variable to a constant value. + /// \brief Restrict a single variable to a constant value. /// /// \details The variable `i` is restricted to the value `v`. /// @@ -751,7 +751,7 @@ namespace adiar /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Restrict a subset of variables to constant values. + /// \brief Restrict a subset of variables to constant values. /// /// \details For each tuple (i,v) in the assignment `xs`, the variable with label i is set to the /// constant value v. This binds the scope of the variables in `xs`, i.e. any later @@ -779,7 +779,7 @@ namespace adiar /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Restrict a subset of variables to constant values. + /// \brief Restrict a subset of variables to constant values. /// /// \details For each tuple (i,v) provided by the iterator, the variable with label i is set to /// the constant value v. @@ -816,7 +816,7 @@ namespace adiar /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Restrict the root to `false`, i.e. follow its low edge. + /// \brief Restrict the root to `false`, i.e. follow its low edge. /// /// \remark In other BDD packages, this function is good for traversing a BDD. But, here this is /// not a constant-time operation but constructs an entire new BDD of up-to linear size @@ -838,7 +838,7 @@ namespace adiar /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Restrict the root to `true`, i.e. follow its high edge. + /// \brief Restrict the root to `true`, i.e. follow its high edge. /// /// \remark In other BDD packages, this function is good for traversing a BDD. But, here this is /// not a constant-time operation but constructs an entire new BDD of up-to linear size @@ -860,7 +860,7 @@ namespace adiar /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Existential quantification of a single variable. + /// \brief Existential quantification of a single variable. /// /// \details Computes the BDD for \f$ \exists x_{i} : f \f$ faster than computing /// \f$ f|_{x_i = \bot} \lor f|_{x_i = \top} \f$ using `bdd_apply` and `bdd_restrict`. @@ -969,7 +969,7 @@ namespace adiar /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Existential quantification of multiple variables. + /// \brief Existential quantification of multiple variables. /// /// \param f /// BDD to be quantified. @@ -986,7 +986,7 @@ namespace adiar /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Existential quantification of multiple variables. + /// \brief Existential quantification of multiple variables. /// /// \remark Unlike `bdd_exists(const bdd& f, const generator<...>& vars)`, this function moves the /// ownership of `f` into the quantification algorithm. This allows it to garbage collect @@ -996,7 +996,7 @@ namespace adiar bdd_exists(bdd&& f, const generator& vars); ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Existential quantification of multiple variables. + /// \brief Existential quantification of multiple variables. /// /// \remark Unlike `bdd_exists(const bdd& f, const generator<...>& vars)`, this function skips the /// initial transposition of `f` if possible. @@ -1070,7 +1070,7 @@ namespace adiar } ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Existential quantification of multiple variables. + /// \brief Existential quantification of multiple variables. /// /// \remark Unlike `bdd_exists(const bdd& f, ForwardIt, ForwardIt)`, this function skips the /// initial transposition of `f` if possible. @@ -1107,7 +1107,7 @@ namespace adiar } ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Existential quantification of multiple variables. + /// \brief Existential quantification of multiple variables. /// /// \remark Unlike `bdd_exists(const bdd& f, ForwardIt, ForwardIt)`, this function skips the /// initial transposition of `f` if possible. @@ -1122,7 +1122,7 @@ namespace adiar /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Forall quantification of a single variable. + /// \brief Forall quantification of a single variable. /// /// \details Computes the BDD for \f$ \forall x_{i} : f \f$ faster than computing /// \f$ f|_{x_i = \bot} \land f|_{x_i = \top} \f$ using `bdd_apply` and `bdd_restrict`. @@ -1231,7 +1231,7 @@ namespace adiar /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Forall quantification of multiple variables. + /// \brief Forall quantification of multiple variables. /// /// \param f /// BDD to be quantified. @@ -1294,7 +1294,7 @@ namespace adiar /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Forall quantification of multiple variables. + /// \brief Forall quantification of multiple variables. /// /// \param f /// BDD to be quantified. @@ -1306,7 +1306,7 @@ namespace adiar /// \param end /// Marks the end for `begin`. /// - /// \returns \f$ \forall x_i \in \texttt{begin} ... \texttt{end} : f \f$ + /// \returns \f$ \forall x_i \in \texttt{begin} ... \texttt{end} : f \f$ ////////////////////////////////////////////////////////////////////////////////////////////////// template __bdd @@ -1882,7 +1882,7 @@ namespace adiar /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Count the number of assignments x that make f(x) true. + /// \brief Count the number of assignments x that make f(x) true. /// /// \param f /// BDD to count within. @@ -1891,7 +1891,7 @@ namespace adiar /// The number of variables in the domain of the function. This number should be larger than or /// equal to the number of levels in the BDD (\see bdd_varcount()) /// - /// \returns The number of unique assignments. + /// \returns The number of unique assignments. /// /// \throws invalid_argument If varcount is not larger than the number of levels in the BDD. ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -1900,14 +1900,14 @@ namespace adiar /// \cond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Count the number of assignments x that make f(x) true. + /// \brief Count the number of assignments x that make f(x) true. ////////////////////////////////////////////////////////////////////////////////////////////////// uint64_t bdd_satcount(const exec_policy& ep, const bdd& f, bdd::label_type varcount); /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Count the number of assignments x that make f(x) true. + /// \brief Count the number of assignments x that make f(x) true. /// /// \details Same as `bdd_satcount(f, varcount)`, with varcount set to be the size of the global /// domain or the number of variables within the given BDD. @@ -1992,7 +1992,7 @@ namespace adiar bdd_maxvar(const bdd& f); ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The lexicographically smallest cube x such that f(x) is true. + /// \brief The lexicographically smallest cube x such that f(x) is true. /// /// \details Outputs the trace of the low-most path to the true terminal. The resulting assignment /// is lexicographically smallest, where every variable is treated as a digit and @@ -2091,7 +2091,7 @@ namespace adiar } ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The lexicographically largest cube x such that f(x) is true. + /// \brief The lexicographically largest cube x such that f(x) is true. /// /// \details Outputs the trace of the high-most path to the true terminal. The resulting /// assignment is lexicographically largest, where every variable is treated as a digit @@ -2158,7 +2158,7 @@ namespace adiar bdd_satmax(const bdd& f, const bdd& d); ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The lexicographically largest x such that f(x) is true. + /// \brief The lexicographically largest x such that f(x) is true. /// /// \param c /// Consumer that is called in ascending order of the bdd's levels with the (var, value) pairs @@ -2177,7 +2177,7 @@ namespace adiar /// Single-pass output iterator for where to place the output. /// /// \returns The output iterator at its final state. - ////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// template >> && !is_convertible>> @@ -2188,7 +2188,7 @@ namespace adiar return iter; } - //////////////////////////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Obtain the satisfying assignment that is minimal for the given linear cost function /// over the global domain. /// @@ -2200,22 +2200,22 @@ namespace adiar /// /// \returns A pair of a BDD cube with the best satisfying assignment and its cost. If no solution /// was found, returns the false constant and NaN - //////////////////////////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// pair bdd_optmin(const bdd& f, const cost& c); /// \cond - //////////////////////////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Obtain the satisfying assignment that is minimal for the given linear cost function /// over the global domain. - //////////////////////////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// pair bdd_optmin(const exec_policy& ep, const bdd& f, const cost& c); /// \endcond - //////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Obtain the satisfying assignment that is minimal for the given linear cost function - /// over the global domain. + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Obtain the satisfying assignment that is minimal for the given linear cost function + /// over the global domain. /// /// \param f /// The BDD of feasible solutions @@ -2229,17 +2229,17 @@ namespace adiar /// \returns The cost of the satisfying solution if any, otherwise NaN. /// /// \remark If `f` is a terminal, `cb` will never be called - //////////////////////////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// double bdd_optmin(const bdd& f, const cost& c, const consumer>& cb); /// \cond - //////////////////////////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Obtain the satisfying assignment that is minimal for the given linear cost function /// over the global domain. - //////////////////////////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// double bdd_optmin(const exec_policy& ep, const bdd& f, From 5d2e6844a0a6619751f0f6d48550e7f5142cfc3a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Sun, 5 Apr 2026 13:39:18 +0200 Subject: [PATCH 4/7] Reformat ZDD documentation --- src/adiar/zdd.h | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/src/adiar/zdd.h b/src/adiar/zdd.h index 8b83e9de1..14bd36d65 100644 --- a/src/adiar/zdd.h +++ b/src/adiar/zdd.h @@ -36,7 +36,7 @@ namespace adiar /// \{ ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The ZDD of only a single terminal. + /// \brief The ZDD of only a single terminal. /// /// \param value /// The constant terminal value. @@ -59,7 +59,7 @@ namespace adiar zdd_null(); ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The set of bitvectors over a given domain where *var* is set to true. + /// \brief The set of bitvectors over a given domain where *var* is set to true. /// /// \details This function is (given the same domain of variables) semantically equivalent to /// `bdd_ithvar` even though the ZDD DAG does not at all look like the BDD DAG. @@ -116,7 +116,7 @@ namespace adiar zdd_ithvar(zdd::label_type var); ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The set of bitvectors over a given domain where *var* is set to false. + /// \brief The set of bitvectors over a given domain where *var* is set to false. /// /// \details Creates a ZDD with a don't care chain of nodes to the true child except for the node /// for `var`; this one instead is forced to be true. @@ -173,7 +173,7 @@ namespace adiar zdd_nithvar(zdd::label_type var); ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The family { { 1, 2, ..., k } }. + /// \brief The family { { 1, 2, ..., k } }. /// /// \details Creates a ZDD with a chain of nodes on the 'high' arc to the true child, and false /// otherwise. @@ -295,7 +295,7 @@ namespace adiar } ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The powerset of all given variables. + /// \brief The powerset of all given variables. /// /// \details Creates a ZDD with a don't care chain of nodes to the true child. /// @@ -500,7 +500,7 @@ namespace adiar /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The intersection of two families of sets. + /// \brief The intersection of two families of sets. /// /// \returns \f$ A \cap B \f$ ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -546,7 +546,7 @@ namespace adiar /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The set difference of two families of sets. + /// \brief The set difference of two families of sets. /// /// \returns \f$ A \setminus B \f$ ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -704,7 +704,7 @@ namespace adiar /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Complement of A within the global \ref module__domain + /// \brief Complement of A within the global \ref module__domain /// /// \param A /// family of sets to complement @@ -740,7 +740,7 @@ namespace adiar /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Expands the domain of the given ZDD to also include the given set of labels. + /// \brief Expands the domain of the given ZDD to also include the given set of labels. /// /// \details Adds don't care nodes on each levels in `vars`. That is, this essentially is the /// inverse of the `zdd_project` and lifts the set of sets unprojects to a larger domain. @@ -849,7 +849,7 @@ namespace adiar /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Subset that do \em not include the given set of variables. + /// \brief Subset that do \em not include the given set of variables. /// /// \param A /// Family of set @@ -1586,7 +1586,7 @@ namespace adiar zdd_contains(const zdd& A, const generator& a); ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Whether the family includes the given set of labels. + /// \brief Whether the family includes the given set of labels. /// /// \param A /// Set of interest @@ -1621,7 +1621,7 @@ namespace adiar zdd_minelem(const zdd& A); ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Retrieves the lexicographically smallest set a in A. + /// \brief Retrieves the lexicographically smallest set a in A. /// /// \param A /// Set of sets of interest. From d96abd1159b259762f6d67840f484a258780a445 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Sun, 5 Apr 2026 13:55:45 +0200 Subject: [PATCH 5/7] Fix(ish) link to internal 'shared_file' --- src/adiar/adiar.h | 2 +- src/adiar/domain.h | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/adiar/adiar.h b/src/adiar/adiar.h index 5d2065ca2..09f6946c1 100644 --- a/src/adiar/adiar.h +++ b/src/adiar/adiar.h @@ -87,7 +87,7 @@ namespace adiar /// /// \warning All of Adiar's file objects must be destructed **before** this functions i called. /// That is, any \ref bdd \ref bdd_builder, \ref zdd \ref zdd_builder or any \ref - /// shared_file objects you may be using. + /// adiar::internal::shared_file objects you may be using. /// /// \throws runtime_error /// If compiled with *debug* and one of Adiar's objects have *not* been destructed. diff --git a/src/adiar/domain.h b/src/adiar/domain.h index 20d15c31e..019801b6d 100644 --- a/src/adiar/domain.h +++ b/src/adiar/domain.h @@ -77,7 +77,8 @@ namespace adiar /// to the prior value without recreating the entire file. /// /// \param dom - /// A \ref shared_file containing all labels of the problem domain in ascending order. + /// A \ref adiar::internal::shared_file containing all labels of the problem domain in + /// ascending order. /// /// \see domain_get() ////////////////////////////////////////////////////////////////////////////////////////////////// From c01c4f2f7c0a0786b330542610b28fa15af6d637 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Sun, 5 Apr 2026 16:15:44 +0200 Subject: [PATCH 6/7] Fix Doxygen warnings for BDD and ZDD operations --- src/adiar/bdd.h | 39 ++++++++++++++++++++++++++++++--------- src/adiar/zdd.h | 12 ++++++++---- 2 files changed, 38 insertions(+), 13 deletions(-) diff --git a/src/adiar/bdd.h b/src/adiar/bdd.h index 7ed946607..390601e67 100644 --- a/src/adiar/bdd.h +++ b/src/adiar/bdd.h @@ -1236,7 +1236,7 @@ namespace adiar /// \param f /// BDD to be quantified. /// - /// \param gen + /// \param vars /// Generator function, that produces variables to be quantified in \em descending order. These /// values have to be smaller than or equals to `bdd::max_label`. /// @@ -1471,7 +1471,7 @@ namespace adiar /// \param relation /// A relation between *current* and *next* states. /// - /// \param m + /// \param pred /// Predicate whether a variable should be existentially quantified. /// /// \returns \f$ \exists x \in \mathit{pred}(x) : (\mathit{states} \land \mathit{relation}) \f$ @@ -1543,6 +1543,9 @@ namespace adiar /// A relation between *current* and *next* state variables. The *next* state is encoded with /// variables `varcount`, `varcount+1`, ... `2*varcount - 1`. /// + /// \param varcount + /// Number of variables used for the *current* set of states. + /// /// \returns \f$ (\exists x \in \{ x \mid x < \mathit{varcount} \} /// : (\mathit{states} \land \mathit{relation})) /// [x' \mapsto x' - \mathit{varcount}] \f$ @@ -1643,6 +1646,9 @@ namespace adiar /// A relation between *current* and *next* state variables. The *next* state is encoded with /// variables `varcount`, `varcount+1`, ... `2*varcount - 1`. /// + /// \param varcount + /// Number of variables used for the *current* set of states. + /// /// \returns \f$ (\exists x' \in \{ x' \mid \geq \mathit{varcount} \} /// : (\mathit{states}[x \mapsto x + \mathit{varcount}] /// \land \mathit{relation})) \f$ @@ -2006,6 +2012,9 @@ namespace adiar ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief The lexicographically smallest x such that f(x) is true within the given domain. /// + /// \param f + /// BDD of interest. + /// /// \param d /// Generator of domain in ascending order. /// @@ -2026,10 +2035,10 @@ namespace adiar /// \param f /// BDD of interest. /// - /// \param begin + /// \param cbegin /// Single-pass forward iterator of *immutable* variables in *ascending* ordering. /// - /// \param end + /// \param cend /// Marks the end for `begin`. /// /// \returns A bdd whos only path to the `true` terminal reflects the minimal assignment and @@ -2062,6 +2071,9 @@ namespace adiar ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief The lexicographically smallest x such that f(x) is true. /// + /// \param f + /// BDD of interest. + /// /// \param c /// Consumer that is called in ascending order of the bdd's levels with the (var, value) /// pairs of the assignment. @@ -2075,7 +2087,7 @@ namespace adiar /// \param f /// BDD of interest. /// - /// \param begin + /// \param iter /// Single-pass output iterator for where to place the output. /// /// \returns The output iterator at its final state. @@ -2093,6 +2105,9 @@ namespace adiar ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief The lexicographically largest cube x such that f(x) is true. /// + /// \param f + /// BDD of interest. + /// /// \details Outputs the trace of the high-most path to the true terminal. The resulting /// assignment is lexicographically largest, where every variable is treated as a digit /// and \f$ x_0 > x_1 > \dots \f$. @@ -2105,6 +2120,9 @@ namespace adiar ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief The lexicographically largest x such that f(x) is true within the given domain. /// + /// \param f + /// BDD of interest. + /// /// \param d /// Generator of domain in ascending order. /// @@ -2124,11 +2142,11 @@ namespace adiar /// \param f /// BDD of interest. /// - /// \param begin + /// \param cbegin /// Single-pass forward iterator of *immutable* variables in *ascending* ordering. /// - /// \param end - /// Marks the end for `begin`. + /// \param cend + /// Marks the end for `cbegin`. /// /// \returns A bdd whos only path to the `true` terminal reflects the maximal assignment and /// (at least) includes the variables in *[begin, end)*. @@ -2160,6 +2178,9 @@ namespace adiar ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief The lexicographically largest x such that f(x) is true. /// + /// \param f + /// BDD of interest. + /// /// \param c /// Consumer that is called in ascending order of the bdd's levels with the (var, value) pairs /// of the assignment. @@ -2173,7 +2194,7 @@ namespace adiar /// \param f /// BDD of interest. /// - /// \param begin + /// \param iter /// Single-pass output iterator for where to place the output. /// /// \returns The output iterator at its final state. diff --git a/src/adiar/zdd.h b/src/adiar/zdd.h index 14bd36d65..fa5f1657b 100644 --- a/src/adiar/zdd.h +++ b/src/adiar/zdd.h @@ -487,6 +487,9 @@ namespace adiar operator+(__zdd&& A); /// \endcond + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \see zdd_union + ////////////////////////////////////////////////////////////////////////////////////////////////// __zdd operator+(const zdd& lhs, const zdd& rhs); @@ -768,7 +771,8 @@ namespace adiar ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Expands the domain of the given ZDD to also include the given set of labels. /// - /// \copydetails + /// \details Adds don't care nodes on each levels in `vars`. That is, this essentially is the + /// inverse of the `zdd_project` and lifts the set of sets unprojects to a larger domain. /// /// \param A /// Family of set to expand. @@ -1532,7 +1536,7 @@ namespace adiar /// \param A /// ZDD of interest. /// - /// \param begin + /// \param iter /// Single-pass output iterator for where to place the output. /// /// \returns The output iterator at its final state. @@ -1641,7 +1645,7 @@ namespace adiar /// \param A /// Set of sets of interest. /// - /// \param begin + /// \param iter /// Single-pass forward iterator for where to place the output. /// /// \returns The output iterator at its final state. @@ -1689,7 +1693,7 @@ namespace adiar /// \param A /// Set of sets of interest. /// - /// \param begin + /// \param iter /// Single-pass output iterator for where to place the output. /// /// \returns The output iterator at its final state. From 7b4427bd627d00d5fd9f6b281bcef5aff4c29909 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Sun, 5 Apr 2026 17:33:08 +0200 Subject: [PATCH 7/7] Fix \addtogroup does not create subsections (\name) or subgroups (nested \defgroup) --- src/adiar/bdd.h | 112 ++++++++++++++++++++++++++++++++++++++++-------- src/adiar/zdd.h | 89 +++++++++++++++++++++++++++++++------- 2 files changed, 169 insertions(+), 32 deletions(-) diff --git a/src/adiar/bdd.h b/src/adiar/bdd.h index 390601e67..bd6719366 100644 --- a/src/adiar/bdd.h +++ b/src/adiar/bdd.h @@ -7,16 +7,16 @@ /// \brief A Binary Decision Diagram (BDD) represents a boolean function \f$ \{ 0, 1 \}^n /// \rightarrow \{ 0, 1 \} \f$ over a finite domain of \f$ n \f$ boolean input variables. /// -/// The \ref bdd class takes care of reference counting and optimal garbage collection of the -/// underlying files. To ensure the most disk-space is available, try to release your \ref bdd -/// objects as quickly as possible and/or minimise the number of lvalues of said type. +/// \details The \ref bdd class takes care of reference counting and optimal garbage collection of +/// the underlying files. To ensure the most disk-space is available, try to release your +/// \ref bdd objects as quickly as possible and/or minimise the number of lvalues of said +/// type. /// -/// To construct a more complex but well-structured \ref bdd by hand, please -/// use the \ref bdd_builder (see \ref builder) instead. +/// \details An \ref exec_policy can be provided as an optional *first* argument for (most) of the +/// BDD functions. This provides you with the ability to change settings on the algorithm +/// execution, e.g. the type of priority queue and algorithm used. /// -/// An \ref exec_policy can be provided as an optional *first* argument for (most) of the functions -/// that follow. This provides you with the ability to change settings on the algorithm execution, -/// e.g. the type of priority queue and algorithm used. +/// \hidegroupgraph //////////////////////////////////////////////////////////////////////////////////////////////////// #include @@ -33,7 +33,18 @@ namespace adiar { ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \addtogroup module__bdd Basic Constructors + /// \addtogroup module__bdd + /// \{ + /// + /// \defgroup module__bdd__constructors Basic Constructors + /// + /// \brief Construction of constants, variables, and cubes. + /// + /// \remark To construct a more complex but well-structured \ref bdd by hand, please use the \ref + /// bdd_builder (see \ref builder) instead. + /// + /// + /// \hidegroupgraph /// /// \{ @@ -308,11 +319,19 @@ namespace adiar return bdd_cube(make_generator(begin, end)); } + /// \} /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \addtogroup module__bdd Basic Operations + /// \addtogroup module__bdd + /// \{ + /// + /// \defgroup module__bdd__basic_operations Basic Operations + /// + /// \brief Basic Boolean operations. + /// + /// \hidegroupgraph /// /// \{ @@ -1383,11 +1402,21 @@ namespace adiar /// \endcond + /// \} /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \addtogroup module__bdd Variable Reordering / Substitution + /// \addtogroup module__bdd + /// \{ + /// + /// \defgroup module__bdd__replace Variable Substitution + /// + /// \brief Variable substitution and reordering. + /// + /// \remark Variable substitution can be used as a poor man's explicit reordering operation. + /// + /// \hidegroupgraph /// /// \{ @@ -1454,11 +1483,19 @@ namespace adiar /// \endcond + /// \} /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \addtogroup module__bdd Transition System Operations + /// \addtogroup module__bdd + /// \{ + /// + /// \defgroup module__bdd__relprod Transition System Operations + /// + /// \brief Relational operations on BDDs. + /// + /// \hidegroupgraph /// /// \{ @@ -1694,11 +1731,19 @@ namespace adiar bdd_relprev(const exec_policy& ep, const bdd& states, const bdd& relation); /// \endcond + /// \} /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \addtogroup module__bdd Predicates + /// \addtogroup module__bdd + /// \{ + /// + /// \defgroup module__bdd__predicates Predicates + /// + /// \brief Predicative information on BDDs + /// + /// \hidegroupgraph /// /// \{ @@ -1850,11 +1895,19 @@ namespace adiar operator!=(__bdd&& f, __bdd&& g); /// \endcond + /// \} /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \addtogroup module__bdd Counting Operations + /// \addtogroup module__bdd + /// \{ + /// + /// \defgroup module__bdd__counting Counting Operations + /// + /// \brief Numerical information on BDDs. + /// + /// \hidegroupgraph /// /// \{ @@ -1931,11 +1984,19 @@ namespace adiar bdd_satcount(const exec_policy& ep, const bdd& f); /// \endcond + /// \} /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \addtogroup module__bdd Input Variables + /// \addtogroup module__bdd + /// \{ + /// + /// \defgroup module__bdd__inputs Input Variables + /// + /// \brief Information on variables in BDDs. + /// + /// \hidegroupgraph /// /// \{ @@ -2326,11 +2387,19 @@ namespace adiar return bdd_eval(f, make_generator(begin, end)); } + /// \} /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \addtogroup module__bdd Conversion from other Decision Diagrams + /// \addtogroup module__bdd + /// \{ + /// + /// \defgroup module__bdd__conversion Conversion to BDDs + /// + /// \brief Conversion from \ref module__zdd . + /// + /// \hidegroupgraph /// /// \{ @@ -2421,11 +2490,19 @@ namespace adiar bdd_from(const exec_policy& ep, const zdd& A); /// \endcond + /// \} /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \addtogroup module__bdd DOT Files + /// \addtogroup module__bdd + /// \{ + /// + /// \defgroup module__bdd__dot Visualization + /// + /// \brief Printing of `.dot` files. + /// + /// \hidegroupgraph /// /// \{ @@ -2441,6 +2518,7 @@ namespace adiar void bdd_printdot(const bdd& f, const std::string& file_name, bool include_id = false); + /// \} /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// } diff --git a/src/adiar/zdd.h b/src/adiar/zdd.h index fa5f1657b..d850413c7 100644 --- a/src/adiar/zdd.h +++ b/src/adiar/zdd.h @@ -7,16 +7,16 @@ /// \brief A Zero-suppressed Decision Diagram (ZDD) represents a family of a set of \f$ n \f$ /// numbers, i.e. an \f$ S \subseteq 2^{\{ 0, 1, \dots, n-1 \}} \f$. /// -/// The \ref zdd class takes care of reference counting and optimal garbage collection of the -/// underlying files. To ensure the most disk-space is available, try to garbage collect the \ref -/// zdd objects as quickly as possible and/or minimise the number of lvalues of said type. +/// \details The \ref zdd class takes care of reference counting and optimal garbage collection of +/// the underlying files. To ensure the most disk-space is available, try to garbage +/// collect the \ref zdd objects as quickly as possible and/or minimise the number of +/// lvalues of said type. /// -/// To construct a more complex but well-structured \ref zdd by hand, please use the \ref -/// zdd_builder (see \ref builder) instead. +/// \details An \ref exec_policy can be provided as an optional *first* argument for (most) of the +/// ZDD functions. This provides you with the ability to change settings on the algorithm +/// execution, e.g. the type of priority queue and algorithm used. /// -/// An \ref exec_policy can be provided as an optional *first* argument for (most) of the functions -/// that follow. This provides you with the ability to change settings on the algorithm execution, -/// e.g. the type of priority queue and algorithm used. +/// \hidegroupgraph //////////////////////////////////////////////////////////////////////////////////////////////////// #include @@ -31,7 +31,17 @@ namespace adiar { ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \addtogroup module__zdd Basic Constructors + /// \addtogroup module__zdd + /// \{ + /// + /// \defgroup module__zdd__constructors Basic Constructors + /// + /// \brief Construction of constants, singletons, and points. + /// + /// \remark To construct a more complex but well-structured \ref zdd by hand, please use the \ref + /// zdd_builder (see \ref builder) instead. + /// + /// \hidegroupgraph /// /// \{ @@ -410,11 +420,19 @@ namespace adiar zdd zdd_top(); + /// \} /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \addtogroup module__zdd Basic Operations + /// \addtogroup module__zdd + /// \{ + /// + /// \defgroup module__zdd__basic_operations Basic ZDD Operations + /// + /// \brief Basic set operations. + /// + /// \hidegroupgraph /// /// \{ @@ -1250,11 +1268,19 @@ namespace adiar /// \endcond + /// \} /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \addtogroup module__zdd Predicates + /// \addtogroup module__zdd + /// \{ + /// + /// \defgroup module__zdd__predicates Predicates + /// + /// \brief Predicative information on ZDDs. + /// + /// \hidegroupgraph /// /// \{ @@ -1474,11 +1500,19 @@ namespace adiar zdd_disjoint(const exec_policy& ep, const zdd& A, const zdd& B); /// \endcond + /// \} /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \addtogroup module__zdd Counting Operations + /// \addtogroup module__zdd + /// \{ + /// + /// \defgroup module__zdd__counting Counting Operations + /// + /// \brief Numerical information on ZDDs. + /// + /// \hidegroupgraph /// /// \{ @@ -1509,11 +1543,19 @@ namespace adiar zdd_size(const exec_policy& ep, const zdd& A); /// \endcond + /// \} /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \addtogroup module__zdd Set Elements + /// \addtogroup module__zdd + /// \{ + /// + /// \defgroup module__zdd__inputs Set Elements + /// + /// \brief Information on the elements in a ZDD. + /// + /// \hidegroupgraph /// /// \{ @@ -1707,11 +1749,19 @@ namespace adiar return iter; } + /// \} /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \addtogroup module__zdd Conversion from other Decision Diagrams + /// \addtogroup module__zdd + /// \{ + /// + /// \defgroup module__zdd__conversion Conversion to ZDDs + /// + /// \brief Conversion from \ref module__bdd . + /// + /// \hidegroupgraph /// /// \{ @@ -1800,11 +1850,19 @@ namespace adiar zdd_from(const exec_policy& ep, const bdd& f); /// \endcond + /// \} /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \addtogroup module__zdd Dot Files + /// \addtogroup module__zdd + /// \{ + /// + /// \defgroup module__zdd__dot ZDD Visualization + /// + /// \brief Printing of `.dot` files. + /// + /// \hidegroupgraph /// /// \{ @@ -1820,6 +1878,7 @@ namespace adiar void zdd_printdot(const zdd& A, const std::string& file_name, bool include_id = false); + /// \} /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// }