Adiar 2.1.0
An External Memory Decision Diagram Library
Loading...
Searching...
No Matches
zdd.h
1#ifndef ADIAR_ZDD_H
2#define ADIAR_ZDD_H
3
14
15#include <iostream>
16#include <string>
17
18#include <adiar/bdd/bdd.h>
19#include <adiar/bool_op.h>
20#include <adiar/exec_policy.h>
21#include <adiar/functional.h>
22#include <adiar/zdd/zdd.h>
23
24namespace adiar
25{
33
42 zdd
43 zdd_terminal(bool value);
44
48 zdd
49 zdd_empty();
50
54 zdd
55 zdd_null();
56
75 zdd
76 zdd_ithvar(zdd::label_type var, const generator<zdd::label_type>& dom);
77
96 template <typename ForwardIt>
97 zdd
102
111 zdd
112 zdd_ithvar(zdd::label_type var);
113
132 zdd
133 zdd_nithvar(zdd::label_type var, const generator<zdd::label_type>& dom);
134
153 template <typename ForwardIt>
154 zdd
159
168 zdd
169 zdd_nithvar(zdd::label_type var);
170
184 zdd
185 zdd_vars(const generator<zdd::label_type>& vars);
186
200 template <typename ForwardIt>
201 zdd
206
219 zdd
220 zdd_point(const generator<zdd::label_type>& vars);
221
235 template <typename ForwardIt>
236 zdd
241
254 zdd
255 zdd_singleton(zdd::label_type var);
256
270 zdd
271 zdd_singletons(const generator<zdd::label_type>& vars);
272
286 template <typename ForwardIt>
287 zdd
292
305 zdd
306 zdd_powerset(const generator<zdd::label_type>& vars);
307
321 template <typename ForwardIt>
322 zdd
327
337 zdd
338 zdd_bot(const generator<zdd::label_type>& dom);
339
352 template <typename ForwardIt>
353 inline zdd
358
364 zdd
365 zdd_bot();
366
376 zdd
377 zdd_top(const generator<zdd::label_type>& dom);
378
391 template <typename ForwardIt>
392 inline zdd
397
406 zdd
407 zdd_top();
408
411
416
433 __zdd
434 zdd_binop(const zdd& A, const zdd& B, const predicate<bool, bool>& op);
435
439 __zdd
440 zdd_binop(const exec_policy& ep, const zdd& A, const zdd& B, const predicate<bool, bool>& op);
441
447 __zdd
448 zdd_union(const zdd& A, const zdd& B);
449
453 __zdd
454 zdd_union(const exec_policy& ep, const zdd& A, const zdd& B);
455
459 __zdd
460 operator|(const zdd& lhs, const zdd& rhs);
461
463 __zdd
464 operator|(__zdd&&, __zdd&&);
465 __zdd
466 operator|(const zdd&, __zdd&&);
467 __zdd
468 operator|(__zdd&&, const zdd&);
470
474 zdd
475 operator+(const zdd& A);
476
478 __zdd
479 operator+(__zdd&& A);
481
482 __zdd
483 operator+(const zdd& lhs, const zdd& rhs);
484
486 __zdd
487 operator+(__zdd&&, __zdd&&);
488 __zdd
489 operator+(const zdd&, __zdd&&);
490 __zdd
491 operator+(__zdd&&, const zdd&);
493
499 __zdd
500 zdd_intsec(const zdd& A, const zdd& B);
501
505 __zdd
506 zdd_intsec(const exec_policy& ep, const zdd& A, const zdd& B);
507
511 __zdd
512 operator&(const zdd& lhs, const zdd& rhs);
513
515 __zdd
516 operator&(__zdd&&, __zdd&&);
517 __zdd
518 operator&(const zdd&, __zdd&&);
519 __zdd
520 operator&(__zdd&&, const zdd&);
522
526 __zdd
527 operator*(const zdd& lhs, const zdd& rhs);
528
530 __zdd
531 operator*(__zdd&&, __zdd&&);
532 __zdd
533 operator*(const zdd&, __zdd&&);
534 __zdd
535 operator*(__zdd&&, const zdd&);
537
543 __zdd
544 zdd_diff(const zdd& A, const zdd& B);
545
549 __zdd
550 zdd_diff(const exec_policy& ep, const zdd& A, const zdd& B);
551
558 __zdd
559 operator-(const zdd& A);
560
562 __zdd
563 operator-(__zdd&& A);
565
569 __zdd
570 operator-(const zdd& lhs, const zdd& rhs);
571
573 __zdd
574 operator-(__zdd&&, __zdd&&);
575 __zdd
576 operator-(const zdd&, __zdd&&);
577 __zdd
578 operator-(__zdd&&, const zdd&);
580
593 __zdd
594 zdd_change(const zdd& A, const generator<zdd::label_type>& vars);
595
599 __zdd
600 zdd_change(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& vars);
601
617 template <typename ForwardIt>
618 __zdd
623
627 template <typename ForwardIt>
628 __zdd
629 zdd_change(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
630 {
631 return zdd_change(ep, A, make_generator(begin, end));
632 }
633
645 __zdd
646 zdd_complement(const zdd& A, const generator<zdd::label_type>& dom);
647
651 __zdd
652 zdd_complement(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& dom);
653
669 template <typename ForwardIt>
670 __zdd
675
679 template <typename ForwardIt>
680 __zdd
685
699 __zdd
700 zdd_complement(const zdd& A);
701
705 __zdd
706 zdd_complement(const exec_policy& ep, const zdd& A);
707
711 __zdd
712 operator~(const zdd& A);
713
715 __zdd
716 operator~(__zdd&& A);
718
734 __zdd
735 zdd_expand(const zdd& A, const generator<zdd::label_type>& vars);
736
740 __zdd
741 zdd_expand(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& vars);
742
762 template <typename ForwardIt>
763 __zdd
768
772 template <typename ForwardIt>
773 __zdd
774 zdd_expand(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
775 {
776 return zdd_expand(ep, A, make_generator(begin, end));
777 }
778
790 __zdd
791 zdd_offset(const zdd& A, zdd::label_type var);
792
796 __zdd
797 zdd_offset(const exec_policy& ep, const zdd& A, zdd::label_type var);
798
811 __zdd
812 zdd_offset(const zdd& A);
813
817 __zdd
818 zdd_offset(const exec_policy& ep, const zdd& A);
819
832 __zdd
833 zdd_offset(const zdd& A, const generator<zdd::label_type>& vars);
834
838 __zdd
839 zdd_offset(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& vars);
840
856 template <typename ForwardIt>
857 __zdd
862
866 template <typename ForwardIt>
867 __zdd
868 zdd_offset(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
869 {
870 return zdd_offset(ep, A, make_generator(begin, end));
871 }
872
884 __zdd
885 zdd_onset(const zdd& A, zdd::label_type var);
886
890 __zdd
891 zdd_onset(const exec_policy& ep, const zdd& A, zdd::label_type var);
892
905 __zdd
906 zdd_onset(const zdd& A);
907
911 __zdd
912 zdd_onset(const exec_policy& ep, const zdd& A);
913
926 __zdd
927 zdd_onset(const zdd& A, const generator<zdd::label_type>& vars);
928
932 __zdd
933 zdd_onset(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& vars);
934
950 template <typename ForwardIt>
951 __zdd
952 zdd_onset(const zdd& A, ForwardIt begin, ForwardIt end)
953 {
954 return zdd_onset(A, make_generator(begin, end));
955 }
956
960 template <typename ForwardIt>
961 __zdd
962 zdd_onset(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
963 {
964 return zdd_onset(ep, A, make_generator(begin, end));
965 }
966
981 __zdd
982 zdd_project(const zdd& A, const predicate<zdd::label_type>& dom);
983
985
994 __zdd
995 zdd_project(zdd&& A, const predicate<zdd::label_type>& dom);
996
1004 __zdd
1005 zdd_project(__zdd&& A, const predicate<zdd::label_type>& dom);
1006
1008
1013 __zdd
1014 zdd_project(const exec_policy& ep, const zdd& A, const predicate<zdd::label_type>& dom);
1015
1017
1026 __zdd
1027 zdd_project(const exec_policy& ep, zdd&& A, const predicate<zdd::label_type>& dom);
1028
1036 __zdd
1037 zdd_project(const exec_policy& ep, __zdd&& A, const predicate<zdd::label_type>& dom);
1038
1040
1056 __zdd
1057 zdd_project(const zdd& A, const generator<zdd::label_type>& dom);
1058
1060
1069 __zdd
1070 zdd_project(zdd&& A, const generator<zdd::label_type>& dom);
1071
1079 __zdd
1080 zdd_project(__zdd&& A, const generator<zdd::label_type>& dom);
1081
1083
1088 __zdd
1089 zdd_project(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& dom);
1090
1092
1101 __zdd
1102 zdd_project(const exec_policy& ep, zdd&& A, const generator<zdd::label_type>& dom);
1103
1111 __zdd
1112 zdd_project(const exec_policy& ep, __zdd&& A, const generator<zdd::label_type>& dom);
1113
1115
1134 template <typename ForwardIt>
1135 __zdd
1136 zdd_project(const zdd& A, ForwardIt begin, ForwardIt end)
1137 {
1138 return zdd_project(A, make_generator(begin, end));
1139 }
1140
1142
1151 template <typename ForwardIt>
1152 __zdd
1153 zdd_project(zdd&& A, ForwardIt begin, ForwardIt end)
1154 {
1155 return zdd_project(std::move(A), make_generator(begin, end));
1156 }
1157
1165 template <typename ForwardIt>
1166 __zdd
1167 zdd_project(__zdd&& A, ForwardIt begin, ForwardIt end)
1168 {
1169 return zdd_project(std::move(A), make_generator(begin, end));
1170 }
1171
1173
1178 template <typename ForwardIt>
1179 __zdd
1180 zdd_project(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
1181 {
1182 return zdd_project(ep, A, make_generator(begin, end));
1183 }
1184
1186
1195 template <typename ForwardIt>
1196 __zdd
1197 zdd_project(const exec_policy& ep, zdd&& A, ForwardIt begin, ForwardIt end)
1198 {
1199 return zdd_project(ep, std::move(A), make_generator(begin, end));
1200 }
1201
1209 template <typename ForwardIt>
1210 __zdd
1211 zdd_project(const exec_policy& ep, __zdd&& A, ForwardIt begin, ForwardIt end)
1212 {
1213 return zdd_project(ep, std::move(A), make_generator(begin, end));
1214 }
1215
1217
1220
1225
1231 bool
1232 zdd_iscanonical(const zdd& A);
1233
1237 bool
1238 zdd_isterminal(const zdd& A);
1239
1243 bool
1244 zdd_isfalse(const zdd& A);
1245
1249 bool
1250 zdd_isempty(const zdd& A);
1251
1255 bool
1256 zdd_istrue(const zdd& A);
1257
1261 bool
1262 zdd_isnull(const zdd& A);
1263
1267 bool
1268 zdd_ispoint(const zdd& A);
1269
1273 bool
1274 zdd_equal(const zdd& A, const zdd& B);
1275
1279 bool
1280 zdd_equal(const exec_policy& ep, const zdd& A, const zdd& B);
1281
1285 bool
1286 operator==(const zdd& lhs, const zdd& rhs);
1287
1289 bool
1290 operator==(__zdd&&, __zdd&&);
1291 bool
1292 operator==(const zdd&, __zdd&&);
1293 bool
1294 operator==(__zdd&&, const zdd&);
1296
1300 bool
1301 zdd_unequal(const zdd& A, const zdd& B);
1302
1306 bool
1307 zdd_unequal(const exec_policy& ep, const zdd& A, const zdd& B);
1308
1312 bool
1313 operator!=(const zdd& lhs, const zdd& rhs);
1314
1316 bool
1317 operator!=(__zdd&&, __zdd&&);
1318 bool
1319 operator!=(const zdd&, __zdd&&);
1320 bool
1321 operator!=(__zdd&&, const zdd&);
1323
1327 bool
1328 zdd_subseteq(const zdd& A, const zdd& B);
1329
1333 bool
1334 zdd_subseteq(const exec_policy& ep, const zdd& A, const zdd& B);
1335
1339 bool
1340 operator<=(const zdd& lhs, const zdd& rhs);
1341
1343 bool
1344 operator<=(__zdd&&, __zdd&&);
1345 bool
1346 operator<=(const zdd&, __zdd&&);
1347 bool
1348 operator<=(__zdd&&, const zdd&);
1350
1354 bool
1355 operator>=(const zdd& lhs, const zdd& rhs);
1356
1358 bool
1359 operator>=(__zdd&&, __zdd&&);
1360 bool
1361 operator>=(const zdd&, __zdd&&);
1362 bool
1363 operator>=(__zdd&&, const zdd&);
1365
1369 bool
1370 zdd_subset(const zdd& A, const zdd& B);
1371
1375 bool
1376 zdd_subset(const exec_policy& ep, const zdd& A, const zdd& B);
1377
1381 bool
1382 operator<(const zdd& lhs, const zdd& rhs);
1383
1385 bool
1386 operator<(__zdd&&, __zdd&&);
1387 bool
1388 operator<(const zdd&, __zdd&&);
1389 bool
1390 operator<(__zdd&&, const zdd&);
1392
1396 bool
1397 operator>(const zdd& lhs, const zdd& rhs);
1398
1400 bool
1401 operator>(__zdd&&, __zdd&&);
1402 bool
1403 operator>(const zdd&, __zdd&&);
1404 bool
1405 operator>(__zdd&&, const zdd&);
1407
1411 bool
1412 zdd_disjoint(const zdd& A, const zdd& B);
1413
1417 bool
1418 zdd_disjoint(const exec_policy& ep, const zdd& A, const zdd& B);
1419
1422
1427
1431 size_t
1432 zdd_nodecount(const zdd& A);
1433
1438 zdd::label_type
1439 zdd_varcount(const zdd& A);
1440
1444 uint64_t
1445 zdd_size(const zdd& A);
1446
1450 uint64_t
1451 zdd_size(const exec_policy& ep, const zdd& A);
1452
1455
1460
1470 void
1471 zdd_support(const zdd& A, const consumer<zdd::label_type>& cb);
1472
1485 template <typename OutputIt,
1486 typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>
1487 OutputIt
1488 zdd_support(const zdd& A, OutputIt iter)
1489 {
1490 zdd_support(A, make_consumer<zdd::label_type>(iter));
1491 return iter;
1492 }
1493
1499 zdd::label_type
1500 zdd_topvar(const zdd& f);
1501
1507 zdd::label_type
1508 zdd_minvar(const zdd& A);
1509
1515 zdd::label_type
1516 zdd_maxvar(const zdd& A);
1517
1530 bool
1531 zdd_contains(const zdd& A, const generator<zdd::label_type>& a);
1532
1548 template <typename ForwardIt>
1549 bool
1554
1565 zdd
1566 zdd_minelem(const zdd& A);
1567
1580 void
1581 zdd_minelem(const zdd& A, const consumer<zdd::label_type>& cb);
1582
1594 template <typename OutputIt,
1595 typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>
1596 OutputIt
1597 zdd_minelem(const zdd& A, OutputIt iter)
1598 {
1599 zdd_minelem(A, make_consumer<zdd::label_type>(iter));
1600 return iter;
1601 }
1602
1613 zdd
1614 zdd_maxelem(const zdd& A);
1615
1628 void
1629 zdd_maxelem(const zdd& A, const consumer<zdd::label_type>& cb);
1630
1642 template <typename OutputIt,
1643 typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>
1644 OutputIt
1645 zdd_maxelem(const zdd& A, OutputIt iter)
1646 {
1647 zdd_maxelem(A, make_consumer<zdd::label_type>(iter));
1648 return iter;
1649 }
1650
1653
1658
1672 __zdd
1673 zdd_from(const bdd& f, const generator<zdd::label_type>& dom);
1674
1679 __zdd
1680 zdd_from(const exec_policy& ep, const bdd& f, const generator<zdd::label_type>& dom);
1681
1698 template <typename ForwardIt>
1699 __zdd
1700 zdd_from(const bdd& f, ForwardIt begin, ForwardIt end)
1701 {
1702 return zdd_from(f, make_generator(begin, end));
1703 }
1704
1709 template <typename ForwardIt>
1710 __zdd
1711 zdd_from(const exec_policy& ep, const bdd& f, ForwardIt begin, ForwardIt end)
1712 {
1713 return zdd_from(ep, f, make_generator(begin, end));
1714 }
1715
1728 __zdd
1729 zdd_from(const bdd& f);
1730
1735 __zdd
1736 zdd_from(const exec_policy& ep, const bdd& f);
1737
1740
1745
1749 void
1750 zdd_printdot(const zdd& A, std::ostream& out = std::cout, bool include_id = false);
1751
1755 void
1756 zdd_printdot(const zdd& A, const std::string& file_name, bool include_id = false);
1757
1760}
1761
1762#endif // ADIAR_ZDD_H
adiar::__zdd
A (possibly unreduced) Zero-suppressed Decision Diagram.
Definition zdd.h:24
adiar::bdd
A reduced Binary Decision Diagram.
Definition bdd.h:53
adiar::exec_policy
Settings to dictate the execution of Adiar's algorithms.
Definition exec_policy.h:35
adiar::internal::dd::label_type
node_type::label_type label_type
Type of this node's variable label.
Definition dd.h:292
adiar::zdd
Reduced Ordered Zero-suppressed Decision Diagram.
Definition zdd.h:62
adiar::operator|
__bdd operator|(const bdd &lhs, const bdd &rhs)
adiar::operator+
bdd operator+(const bdd &f)
adiar::operator&
__bdd operator&(const bdd &lhs, const bdd &rhs)
adiar::operator*
__bdd operator*(const bdd &lhs, const bdd &rhs)
adiar::operator!=
bool operator!=(const bdd &f, const bdd &g)
adiar::operator~
bdd operator~(const bdd &f)
adiar::operator==
bool operator==(const bdd &f, const bdd &g)
adiar::operator-
bdd operator-(const bdd &f)
adiar::generator
function< optional< RetType >()> generator
Generator function that produces a new value of RetType for each call.
Definition functional.h:170
adiar::consumer
function< void(Arg)> consumer
Consumer function of value of type Arg.
Definition functional.h:64
adiar::make_generator
generator< typename std::remove_reference_t< ForwardIt >::value_type > make_generator(ForwardIt &&begin, ForwardIt &&end)
Wrap a begin and end iterator pair into a generator function.
Definition functional.h:177
adiar::predicate
function< bool(Args...)> predicate
Predicate function given value(s) of type(s) Args.
Definition functional.h:51
adiar::make_consumer
consumer< ValueType > make_consumer(OutputIt &&iter)
Wrap an iterator into a consumer function.
Definition functional.h:71
adiar::zdd_change
__zdd zdd_change(const zdd &A, const generator< zdd::label_type > &vars)
The symmetric difference between each set in the family and the given set of variables.
adiar::zdd_null
zdd zdd_null()
The family only with the empty set, i.e. { Ø } .
adiar::zdd_top
zdd zdd_top()
Top of the powerset lattice.
adiar::zdd_minvar
zdd::label_type zdd_minvar(const zdd &A)
Get the minimal occurring variable in the family.
adiar::zdd_topvar
zdd::label_type zdd_topvar(const zdd &f)
Get the root's variable label.
adiar::zdd_ithvar
zdd zdd_ithvar(zdd::label_type var, const generator< zdd::label_type > &dom)
The set of bitvectors over a given domain where var is set to true.
adiar::zdd_point
zdd zdd_point(const generator< zdd::label_type > &vars)
The family { { 1, 2, ..., k } } with a single bit-vector.
adiar::zdd_disjoint
bool zdd_disjoint(const zdd &A, const zdd &B)
Whether the two families are disjoint.
adiar::zdd_binop
__zdd zdd_binop(const zdd &A, const zdd &B, const predicate< bool, bool > &op)
Apply a binary operator between the sets of two families.
adiar::zdd_printdot
void zdd_printdot(const zdd &A, std::ostream &out=std::cout, bool include_id=false)
Output a DOT drawing of a ZDD to the given output stream.
adiar::zdd_powerset
zdd zdd_powerset(const generator< zdd::label_type > &vars)
The powerset of all given variables.
adiar::zdd_onset
__zdd zdd_onset(const zdd &A, zdd::label_type var)
Subset that do include the given element.
adiar::zdd_maxvar
zdd::label_type zdd_maxvar(const zdd &A)
Get the maximal occurring variable in the family.
adiar::zdd_expand
__zdd zdd_expand(const zdd &A, const generator< zdd::label_type > &vars)
Expands the domain of the given ZDD to also include the given set of labels.
adiar::zdd_isempty
bool zdd_isempty(const zdd &A)
Whether it is the empty family, i.e. Ø .
adiar::zdd_subseteq
bool zdd_subseteq(const zdd &A, const zdd &B)
Whether one family is a subset or equal to the other.
adiar::zdd_nithvar
zdd zdd_nithvar(zdd::label_type var, const generator< zdd::label_type > &dom)
The set of bitvectors over a given domain where var is set to false.
adiar::zdd_vars
zdd zdd_vars(const generator< zdd::label_type > &vars)
The family { { 1, 2, ..., k } }.
adiar::zdd_isfalse
bool zdd_isfalse(const zdd &A)
Whether this ZDD represents false terminal.
adiar::zdd_size
uint64_t zdd_size(const zdd &A)
The number of sets in the family of sets.
adiar::zdd_equal
bool zdd_equal(const zdd &A, const zdd &B)
Whether they represent the same family.
adiar::operator>
bool operator>(const zdd &lhs, const zdd &rhs)
adiar::zdd_singletons
zdd zdd_singletons(const generator< zdd::label_type > &vars)
The family { {1}, {2}, ..., {k} }.
adiar::zdd_offset
__zdd zdd_offset(const zdd &A, zdd::label_type var)
Subset that do not include the given element.
adiar::zdd_nodecount
size_t zdd_nodecount(const zdd &A)
The number of (internal) nodes used to represent the family of sets.
adiar::zdd_contains
bool zdd_contains(const zdd &A, const generator< zdd::label_type > &a)
Whether the family includes the given set of labels.
adiar::zdd_isnull
bool zdd_isnull(const zdd &A)
Whether it is the null family, i.e. { Ø } .
adiar::zdd_minelem
zdd zdd_minelem(const zdd &A)
Retrieves the lexicographically smallest set a in A.
adiar::operator<=
bool operator<=(const zdd &lhs, const zdd &rhs)
adiar::zdd_istrue
bool zdd_istrue(const zdd &A)
Whether this BDD represents true terminal.
adiar::operator>=
bool operator>=(const zdd &lhs, const zdd &rhs)
adiar::zdd_union
__zdd zdd_union(const zdd &A, const zdd &B)
The union of two families of sets.
adiar::zdd_complement
__zdd zdd_complement(const zdd &A, const generator< zdd::label_type > &dom)
Complement of A within the given domain.
adiar::zdd_subset
bool zdd_subset(const zdd &A, const zdd &B)
Whether one family is a strict subset of the other.
adiar::zdd_isterminal
bool zdd_isterminal(const zdd &A)
Whether this ZDD represents a terminal.
adiar::zdd_bot
zdd zdd_bot()
Bottom of the powerset lattice.
adiar::zdd_maxelem
zdd zdd_maxelem(const zdd &A)
Retrieves the lexicographically largest set a in A.
adiar::operator<
bool operator<(const zdd &lhs, const zdd &rhs)
adiar::zdd_singleton
zdd zdd_singleton(zdd::label_type var)
The family { {i} } .
adiar::zdd_ispoint
bool zdd_ispoint(const zdd &A)
Whether it contains a single bit-vector a, i.e. A = { a }.
adiar::zdd_project
__zdd zdd_project(const zdd &A, const predicate< zdd::label_type > &dom)
Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.
adiar::zdd_empty
zdd zdd_empty()
The empty family, i.e. Ø .
adiar::zdd_intsec
__zdd zdd_intsec(const zdd &A, const zdd &B)
The intersection of two families of sets.
adiar::zdd_unequal
bool zdd_unequal(const zdd &A, const zdd &B)
Whether they represent two different families.
adiar::zdd_terminal
zdd zdd_terminal(bool value)
The ZDD of only a single terminal.
adiar::zdd_from
__zdd zdd_from(const bdd &f, const generator< zdd::label_type > &dom)
Obtains the ZDD that represents the same function/set as the given BDD within the given domain.
adiar::zdd_iscanonical
bool zdd_iscanonical(const zdd &A)
Check whether a given ZDD is canonical.
adiar::zdd_support
void zdd_support(const zdd &A, const consumer< zdd::label_type > &cb)
Get (in ascending order) all of the variable labels that occur in the family.
adiar::zdd_varcount
zdd::label_type zdd_varcount(const zdd &A)
The number of variables that exist in the family of sets, i.e. the number of levels present in the ZD...
adiar::zdd_diff
__zdd zdd_diff(const zdd &A, const zdd &B)
The set difference of two families of sets.
adiar
Core types.
Definition adiar.h:40