1 TdZdd User Guide {#mainpage}
2 ===========================================================================
4 * [Overview](#overview)
5 * [DD specification](#dd-specification)
6 * [Operations on DD specifications](#operations-on-dd-specifications)
7 * [DD structure](#dd-structure)
10 ===========================================================================
11 <a name="overview"></a>
13 ===========================================================================
15 A DD has one root node and two terminal nodes (⊤ and ⊥).
16 Every non-terminal node of an *N*-ary DD has *N* outgoing edges.
18 
20 The above picture shows an example of binary DD structure,
21 where the ⊥ terminal node and all edges to it are omitted for visibility;
22 dashed and solid lines are 0- and 1-edges respectively.
23 The DD represents a set of all 3-combinations out of 5 items.
24 Note that levels of DD nodes are defined in descending order;
25 the root node has the highest level and the terminal nodes have the lowest.
27 The following code from [apps/test/example1.cpp](../apps/test/example1.cpp)
28 is a *DD specification* of a binary DD structure representing a set of all
29 *k*-combinations out of *n* items.
31 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
32 class Combination: public tdzdd::DdSpec<Combination,int,2> {
37 Combination(int n, int k)
41 int getRoot(int& state) const {
46 int getChild(int& state, int level, int value) const {
48 if (--level == 0) return (state == k) ? -1 : 0;
49 if (state > k) return 0;
50 if (state + level < k) return 0;
54 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
56 Class `Combination` inherits from `tdzdd::DdSpec<Combination,int,2>`,
57 of which the first template parameter is the derived class itself,
58 the second one is the type of its *state*,
59 and the third one declares the out-degree of non-terminal DD nodes (*N*).
60 The class contains public member functions `int getRoot(int& state)`
61 and `int getChild(int& state, int level, int value)`.
63 `getRoot` initializes the `state` argument by the state of the root node
64 and returns its level.
65 `getChild` receives `state` and `level` of a non-terminal node and integer
66 `value` in the range [0, *N*-1] selecting one of the *N* branches.
67 It computes the state and the level of the child node.
68 If the child node is not a terminal, it updates `state` and returns the level.
69 If the child node is ⊥ or ⊤, it returns 0 or -1 respectively;
70 `state` is not used in those cases.
72 A DD represented by a DD specification can be dumped in "dot" format
73 for [Graphviz](http://www.graphviz.org/) visualization tools.
75 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
76 Combination spec(5, 2);
77 spec.dumpDot(std::cout);
78 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
80 `tdzdd::DdStructure<2>` is a class of explicit binary DD structures.
81 Its object can be constructed from a DD specification object.
83 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
84 tdzdd::DdStructure<2> dd(spec);
85 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
87 A DD structrue can be reduced as a BDD or ZDD using its `void bddReduce()` or
88 `void zddReduce()` member function, and also can be dumped in "dot" format.
90 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
92 dd.dumpDot(std::cout);
93 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
95 A DD structure can be evaluated from the bottom to the top.
96 The following code from
97 [apps/test/testSizeConstraint.cpp](../apps/test/testSizeConstraint.cpp) is a
98 *DD evaluator* to find the size of the largest itemset represented by a ZDD.
100 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
101 class MaxNumItems: public tdzdd::DdEval<MaxNumItems,int> {
103 void evalTerminal(int& n, bool one) const {
104 n = one ? 0 : INT_MIN;
107 void evalNode(int& n, int, DdValues<int,2> const& values) const {
108 n = std::max(values.get(0), values.get(1) + 1);
111 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
113 It is used as follows.
115 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
116 int max = dd.evaluate(MaxNumItems());
117 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
119 The construction and evaluation functions can also be used easily to implement
120 import and export functions of DD structures from/to other DD libraries.
123 ===========================================================================
124 <a name="dd-specification"></a>
126 ===========================================================================
128 A DD specification is defined by deriving it from an appropriate one of the
129 base classes defined in <tdzdd/DdSpec.hpp>.
131 Every DD specification must have `getRoot` and `getChild` member functions.
132 `getRoot` defines the root node configuration. `getChild` defines a mapping
133 from parent node configurations to child node configurations.
134 If the node is not a terminal, the functions update state information and
135 return a positive integer representing the node level.
136 If the node is ⊥ or ⊤, they simply return 0 or -1 respectively
137 for convenience, even though both nodes are level 0.
138 We refer to such a return value as a *level code*.
141 ---------------------------------------------------------------------------
143 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
144 #include <tdzdd/DdSpec.hpp>
145 class S: public tdzdd::DdSpec<S,T,N> { ... };
146 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
147 is an *N*-ary DD specification using type `T` to store state information.
148 Class `S` must implement the following member functions:
150 * `int getRoot(T& state)` stores state information of the root node into
151 `state` and returns a level code.
153 * `int getChild(T& state, int level, int value)` receives state information
154 of a non-terminal node via `state`, the level of it via `level`, and a
155 branch label in the range [0, *N*-1] via `value`;
156 updates `state` by state information of the child node and returns a level
159 In addition, `S` may have to override the following member functions:
161 * `bool equalTo(T const& state1, T const& state2)` returns if `state1` and
162 `state2` are equivalent.
163 The default implementation is `state1 == state2`.
165 * `size_t hashCode(T const& state)` computes a hash value for `state`.
166 The default implementation is `static_cast<size_t>(state)`.
168 Hash values for any two states must be the same whenever they are equivalent.
169 As shown in [Overview](#overview), we can use the default implementations and
170 do not need to override them when `T` is a fundamental data type such as `int`.
174 ---------------------------------------------------------------------------
176 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
177 #include <tdzdd/DdSpec.hpp>
178 class S: public tdzdd::PodArrayDdSpec<S,T,N> { ... };
179 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
180 is an *N*-ary DD specification using an array of type `T` to store state
182 The size of the array must be fixed to some positive integer *m* by calling
183 predefined function `setArraySize(m)` in the constructor of `S`.
184 The library handles the state information just as (`sizeof(T)` × *m*)-byte
185 raw data for efficiency;
186 therefore, `T` must be a data structure without object-oriented features
187 (user-defined constructor, destructor, copy-assignment, etc.).
188 Class `S` must implement the following member functions:
190 * `int getRoot(T* array)` stores state information of the root node into
191 `array[0]`..`array[m-1]` and returns a level code.
193 * `int getChild(T* array, int level, int value)` receives state information
194 of a non-terminal node via `array[0]`..`array[m-1]`, the level of it via
195 `level`, and a branch label in the range [0, *N*-1] via `value`;
196 updates `array[0]`..`array[m-1]` by state information of the child node
197 and returns a level code.
199 You can find an example in [apps/test/example2.cpp](../apps/test/example2.cpp).
203 ---------------------------------------------------------------------------
205 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
206 #include <tdzdd/DdSpec.hpp>
207 class S: public tdzdd::HybridDdSpec<S,TS,TA,N> { ... };
208 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
209 is an *N*-ary DD specification using a combination of type `TS` and an array
210 of type `TA` to store state information.
211 The size of the array must be fixed to some positive integer *m* by calling
212 predefined function `setArraySize(m)` in the constructor of `S`.
213 The library handles the state information of the array just as
214 (`sizeof(TA)` × *m*)-byte raw data for efficiency;
215 therefore, `TA` must be a data structure without object-oriented
216 features (user-defined constructor, destructor, copy-assignment, etc.).
217 Class `S` must implement the following member functions:
219 * `int getRoot(TS& scalar, TA* array)` stores state information of the root
220 node into `scalar` as well as `array[0]`..`array[m-1]` and returns a level
223 * `int getChild(TS& scalar, TA* array, int level, int value)` receives
224 state information of a non-terminal node via `scalar` and
225 `array[0]`..`array[m-1]`, the level of it via `level`, and a branch label
226 in the range [0, *N*-1] via `value`;
227 updates `scalar` and `array[0]`..`array[m-1]` by state information of the
228 child node and returns a level code.
232 ---------------------------------------------------------------------------
234 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
235 #include <tdzdd/DdSpec.hpp>
236 class S: public tdzdd::StatelessDdSpec<S,N> { ... };
237 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
238 is an *N*-ary DD specification using no state information, which means that
239 the DD does not have more than one node at any non-terminal level.
240 Class `S` must implement the following member functions:
242 * `int getRoot()` returns a level code of the root node.
244 * `int getChild(int level, int value)` receives level of a non-terminal
245 node via `level` and a branch label in the range [0, *N*-1] via `value`;
246 returns a level code of the child node.
248 The next example is a specification of a ZDD for a family of all
249 singletons out of *n* items.
251 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
252 #include <tdzdd/DdSpec.hpp>
254 class SingletonZdd: public tdzdd::StatelessDdSpec<SingletonZdd,2> {
262 int getRoot() const {
266 int getChild(int level, int value) const {
267 if (value) return -1;
271 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
275 ---------------------------------------------------------------------------
277 Every DD specification inherits from `tdzdd::DdSpecBase<S,N>`,
278 which defines common member functions including the one to generate a "dot"
279 file for [Graphviz](http://www.graphviz.org/).
281 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
282 void tdzdd::DdSpecBase<S,N>::dumpDot(std::ostream& os = std::cout, std::string title = tdzdd::typenameof<S>()) const;
283 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
285 Each DD specification may have to define its own `printState` member
286 function that prints text on each DD nodes.
288 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
289 void tdzdd::DdSpecBase<S,N>::printState(std::ostream& os, T const& state) const; // for DdSpec
290 void tdzdd::DdSpecBase<S,N>::printState(std::ostream& os, T const* array) const; // for PodArrayDdSpec
291 void tdzdd::DdSpecBase<S,N>::printState(std::ostream& os, TS const& scalar, TA const* array) const; // for HybridDdSpec
292 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
294 Text of each level can also be customized by overriding `printLevel`
297 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
298 void tdzdd::DdSpecBase<S,N>::printLevel(std::ostream& os, int level) const;
299 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
301 The default implementation prints the `level` itself.
304 ===========================================================================
305 <a name="operations-on-dd-specifications"></a>
306 Operations on DD specifications
307 ===========================================================================
309 Operations on DD specifications are defined as global functions in
310 <tdzdd/DdSpecOp.hpp>.
311 Note that they are also applicable to DD structures.
313 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
314 template<typename S1, typename S2>
315 tdzdd::BddAnd<S1,S2> tdzdd::bddAnd(S1 const& spec1, S2 const& spec2);
316 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
317 returns a BDD specification for logical AND of two BDD specifications.
319 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
320 template<typename... SS>
321 tdzdd::BddAnd<SS...> tdzdd::bddAnd(SS const&... specs);
322 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
323 returns a BDD specification for logical AND of two or more BDD specifications.
326 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
327 template<typename S1, typename S2>
328 tdzdd::BddOr<S1,S2> tdzdd::bddOr(S1 const& spec1, S2 const& spec2);
329 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
330 returns a BDD specification for logical OR of two BDD specifications.
332 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
333 template<typename... SS>
334 tdzdd::BddOr<SS...> tdzdd::bddOr(S const&... specs);
335 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
336 returns a BDD specification for logical OR of two or more BDD specifications.
339 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
340 template<typename S1, typename S2>
341 tdzdd::ZddIntersection<S1,S2> tdzdd::zddIntersection(S1 const& spec1, S2 const& spec2);
342 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
343 returns a ZDD specification for set intersection of two ZDD specifications.
345 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
346 template<typename... SS>
347 tdzdd::ZddIntersection<SS...> tdzdd::zddIntersection(SS const&... specs);
348 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
349 returns a ZDD specification for set intersection of two or more ZDD specifications.
352 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
353 template<typename S1, typename S2>
354 tdzdd::ZddUnion<S1,S2> tdzdd::zddUnion(S1 const& spec1, S2 const& spec2);
355 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
356 returns a ZDD specification for set union of two ZDD specifications.
358 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
359 template<typename... SS>
360 tdzdd::ZddUnion<SS...> tdzdd::zddUnion(SS const&... specs);
361 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
362 returns a ZDD specification for set union of two or more ZDD specifications.
365 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
367 tdzdd::BddLookahead<S> tdzdd::bddLookahead(S const& spec);
368 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
369 optimizes a BDD specification in terms of the BDD node deletion rule.
371 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
373 tdzdd::ZddLookahead<S> tdzdd::zddLookahead(S const& spec);
374 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
375 optimizes a ZDD specification in terms of the ZDD node deletion rule.
377 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
379 tdzdd::BddUnreduction<S> tdzdd::bddUnreduction(S const& spec, int numVars);
380 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
381 creates a QDD specification from a BDD specification by complementing
382 skipped nodes in terms of the BDD node deletion rule.
384 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
386 tdzdd::ZddUnreduction<S> tdzdd::zddUnreduction(S const& spec, int numVars);
387 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
388 creates a QDD specification from a ZDD specification by complementing
389 skipped nodes in terms of the ZDD node deletion rule.
392 ===========================================================================
393 <a name="dd-structure"></a>
395 ===========================================================================
397 The template class of DD structures is defined in <tdzdd/DdStructure.hpp>.
399 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
401 class tdzdd::DdStructure;
402 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
404 Note that `DdStructure<N>` works also as the DD specification that represent
409 ---------------------------------------------------------------------------
411 A DD structure can be constructed from a DD specification using the following
412 templated constructor.
414 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
416 tdzdd::DdStructure<N>::DdStructure(tdzdd::DdSpecBase<S,N> const& spec, bool useMP = false);
417 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
419 The optional argument `useMP` sets the attribute value of the object that
420 enables OpenMP parallel processing.
421 Note that the parallel algorithms are tuned for fairly large DDs and may
422 not be very effective on small DDs.
424 The default constructor of `tdzdd::DdStructure<N>` creates a new DD
426 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
427 tdzdd::DdStructure<N>::DdStructure();
428 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
430 The next one constructs a new DD with *n* non-terminal nodes at levels
431 *n* to 1, of which each one has *N* edges pointing to the same node at the
433 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
434 tdzdd::DdStructure<N>::DdStructure(int n, bool useMP = false);
435 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
436 When *N* = 2, it is a ZDD for the power set of a set of *n* items.
440 ---------------------------------------------------------------------------
442 TdZdd provides an efficient method, called *ZDD subsetting*, to refine an
443 existing ZDD by adding a constraint given as a DD specification.
445 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
447 void tdzdd::DdStructure<N>::zddSubset(tdzdd::DdSpecBase<S,N> const& spec);
448 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
449 This templated member function of `tdzdd::DdStructure<N>` updates the current
450 DD by a new DD for ZDD intersection of itself and the given DD specification.
451 The original DD should be reduced as a ZDD in advance for this function to
456 ---------------------------------------------------------------------------
458 The following member functions of `tdzdd::DdStructure<N>` apply reduction
459 rules to the current DD structure.
461 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
462 void tdzdd::DdStructure<N>::qddReduce();
463 void tdzdd::DdStructure<N>::bddReduce();
464 void tdzdd::DdStructure<N>::zddReduce();
465 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
467 `qddReduce()` applies the node sharing rule only.
468 `bddReduce()` applies the node sharing rule and the BDD node deletion rule,
469 which deletes a node when all its outgoing edges point to the same child.
470 `zddReduce()` applies the node sharing rule and the ZDD node deletion rule,
471 which deletes a node when all of its non-zero-labeled outgoing edges point
476 ---------------------------------------------------------------------------
478 A DD evaluator can be defined by deriving it from `tdzdd::DdEval<E,T>`
479 defined in <[tdzdd/DdSpec.hpp](../include/tdzdd/DdSpec.hpp)>.
481 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
482 #include <tdzdd/DdEval.hpp>
483 class E: public tdzdd::DdEval<E,T> { ... };
484 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
485 defines the DD evaluator *E* that computes a value of type *T*.
487 A `tdzdd::DDStructure<N>` object can be evaluated by *E* as follows.
488 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
489 tdzdd::DdStructure<N> dd = ... ;
490 T value = dd.evaluate(E());
491 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
493 Every DD evaluator must define the following functions:
495 * `void evalTerminal(T& v, int id)` receives a terminal node identifier
496 (0 or 1) via `id` and writes the value for it into `v`.
498 * `void evalNode(T& v, int level, tdzdd::DdValues<T,N> const& values)` receives
499 the `level` of the node to be evaluated and evaluation results for its
500 child nodes via `values`;
501 writes the result value into `v`.
503 In `evalNode`, the value and level of the *b*-th child node (*b* = 0..*N*-1)
504 can be obtained through `values.get(b)` and `values.getLevel(b)` respectively.
508 ---------------------------------------------------------------------------
510 The following member functions of `tdzdd::DdStructure<N>` might be also useful.
512 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
513 int tdzdd::DdStructure<N>::topLevel() const;
514 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
515 gets the level of the root node.
517 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
518 size_t tdzdd::DdStructure<N>::size() const;
519 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
520 gets the number of nonterminal nodes.
522 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
523 bool tdzdd::DdStructure<N>::operator==(tdzdd::DdStructure<N> const& o) const;
524 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
525 checks structural equivalence with another DD.
526 Compare after reduction if you want to check logical equivalence.
528 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
529 bool tdzdd::DdStructure<N>::operator!=(tdzdd::DdStructure<N> const& o) const;
530 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
531 checks structural inequivalence with another DD.
532 Compare after reduction if you want to check logical inequivalence.
534 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
535 tdzdd::DdStructure<N> tdzdd::DdStructure<N>::bdd2zdd(int numVars) const;
536 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
537 transforms a BDD into a ZDD.
539 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
540 tdzdd::DdStructure<N> tdzdd::DdStructure<N>::zdd2bdd(int numVars) const;
541 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
542 transforms a ZDD into a BDD.
544 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
545 std::string tdzdd::DdStructure<N>::bddCardinality(int numVars) const;
546 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
547 counts the number of minterms of the function represented by this BDD.
549 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
550 std::string tdzdd::DdStructure<N>::zddCardinality() const;
551 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
552 counts the number of itemsets in the family of itemsets represented
555 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
556 tdzdd::DdStructure<N>::const_iterator tdzdd::DdStructure<N>::begin() const;
557 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
558 returns an iterator to the first element of the family of itemsets
559 represented by this ZDD.
560 Each itemset is represented by `std::set<int>` of levels of selected items.
562 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~{.cpp}
563 tdzdd::DdStructure<N>::const_iterator tdzdd::DdStructure<N>::end() const;
564 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
565 returns an iterator to the element following the last element of
566 the family of itemsets represented by this ZDD.