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{
30
38
47 zdd
48 zdd_terminal(bool value);
49
53 zdd
54 zdd_empty();
55
59 zdd
60 zdd_null();
61
80 zdd
81 zdd_ithvar(zdd::label_type var, const generator<zdd::label_type>& dom);
82
101 template <typename ForwardIt>
102 zdd
107
116 zdd
117 zdd_ithvar(zdd::label_type var);
118
137 zdd
138 zdd_nithvar(zdd::label_type var, const generator<zdd::label_type>& dom);
139
158 template <typename ForwardIt>
159 zdd
164
173 zdd
174 zdd_nithvar(zdd::label_type var);
175
189 zdd
190 zdd_vars(const generator<zdd::label_type>& vars);
191
205 template <typename ForwardIt>
206 zdd
211
224 zdd
225 zdd_point(const generator<zdd::label_type>& vars);
226
240 template <typename ForwardIt>
241 zdd
246
259 zdd
260 zdd_singleton(zdd::label_type var);
261
275 zdd
276 zdd_singletons(const generator<zdd::label_type>& vars);
277
291 template <typename ForwardIt>
292 zdd
297
310 zdd
311 zdd_powerset(const generator<zdd::label_type>& vars);
312
326 template <typename ForwardIt>
327 zdd
332
342 zdd
343 zdd_bot(const generator<zdd::label_type>& dom);
344
357 template <typename ForwardIt>
358 inline zdd
363
369 zdd
370 zdd_bot();
371
381 zdd
382 zdd_top(const generator<zdd::label_type>& dom);
383
396 template <typename ForwardIt>
397 inline zdd
402
411 zdd
412 zdd_top();
413
416
421
438 __zdd
439 zdd_binop(const zdd& A, const zdd& B, const predicate<bool, bool>& op);
440
444 __zdd
445 zdd_binop(const exec_policy& ep, const zdd& A, const zdd& B, const predicate<bool, bool>& op);
446
452 __zdd
453 zdd_union(const zdd& A, const zdd& B);
454
458 __zdd
459 zdd_union(const exec_policy& ep, const zdd& A, const zdd& B);
460
464 __zdd
465 operator|(const zdd& lhs, const zdd& rhs);
466
468 __zdd
469 operator|(__zdd&&, __zdd&&);
470 __zdd
471 operator|(const zdd&, __zdd&&);
472 __zdd
473 operator|(__zdd&&, const zdd&);
475
479 zdd
480 operator+(const zdd& A);
481
483 __zdd
484 operator+(__zdd&& A);
486
487 __zdd
488 operator+(const zdd& lhs, const zdd& rhs);
489
491 __zdd
492 operator+(__zdd&&, __zdd&&);
493 __zdd
494 operator+(const zdd&, __zdd&&);
495 __zdd
496 operator+(__zdd&&, const zdd&);
498
504 __zdd
505 zdd_intsec(const zdd& A, const zdd& B);
506
510 __zdd
511 zdd_intsec(const exec_policy& ep, const zdd& A, const zdd& B);
512
516 __zdd
517 operator&(const zdd& lhs, const zdd& rhs);
518
520 __zdd
521 operator&(__zdd&&, __zdd&&);
522 __zdd
523 operator&(const zdd&, __zdd&&);
524 __zdd
525 operator&(__zdd&&, const zdd&);
527
531 __zdd
532 operator*(const zdd& lhs, const zdd& rhs);
533
535 __zdd
536 operator*(__zdd&&, __zdd&&);
537 __zdd
538 operator*(const zdd&, __zdd&&);
539 __zdd
540 operator*(__zdd&&, const zdd&);
542
548 __zdd
549 zdd_diff(const zdd& A, const zdd& B);
550
554 __zdd
555 zdd_diff(const exec_policy& ep, const zdd& A, const zdd& B);
556
560 __zdd
561 operator-(const zdd& A);
562
564 __zdd
565 operator-(__zdd&& A);
567
571 __zdd
572 operator-(const zdd& lhs, const zdd& rhs);
573
575 __zdd
576 operator-(__zdd&&, __zdd&&);
577 __zdd
578 operator-(const zdd&, __zdd&&);
579 __zdd
580 operator-(__zdd&&, const zdd&);
582
595 __zdd
596 zdd_change(const zdd& A, const generator<zdd::label_type>& vars);
597
601 __zdd
602 zdd_change(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& vars);
603
619 template <typename ForwardIt>
620 __zdd
625
629 template <typename ForwardIt>
630 __zdd
631 zdd_change(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
632 {
633 return zdd_change(ep, A, make_generator(begin, end));
634 }
635
647 __zdd
648 zdd_complement(const zdd& A, const generator<zdd::label_type>& dom);
649
653 __zdd
654 zdd_complement(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& dom);
655
671 template <typename ForwardIt>
672 __zdd
677
681 template <typename ForwardIt>
682 __zdd
687
701 __zdd
702 zdd_complement(const zdd& A);
703
707 __zdd
708 zdd_complement(const exec_policy& ep, const zdd& A);
709
713 __zdd
714 operator~(const zdd& A);
715
717 __zdd
718 operator~(__zdd&& A);
720
736 __zdd
737 zdd_expand(const zdd& A, const generator<zdd::label_type>& vars);
738
742 __zdd
743 zdd_expand(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& vars);
744
764 template <typename ForwardIt>
765 __zdd
770
774 template <typename ForwardIt>
775 __zdd
776 zdd_expand(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
777 {
778 return zdd_expand(ep, A, make_generator(begin, end));
779 }
780
792 __zdd
793 zdd_offset(const zdd& A, zdd::label_type var);
794
798 __zdd
799 zdd_offset(const exec_policy& ep, const zdd& A, zdd::label_type var);
800
813 __zdd
814 zdd_offset(const zdd& A);
815
819 __zdd
820 zdd_offset(const exec_policy& ep, const zdd& A);
821
834 __zdd
835 zdd_offset(const zdd& A, const generator<zdd::label_type>& vars);
836
840 __zdd
841 zdd_offset(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& vars);
842
858 template <typename ForwardIt>
859 __zdd
864
868 template <typename ForwardIt>
869 __zdd
870 zdd_offset(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
871 {
872 return zdd_offset(ep, A, make_generator(begin, end));
873 }
874
886 __zdd
887 zdd_onset(const zdd& A, zdd::label_type var);
888
892 __zdd
893 zdd_onset(const exec_policy& ep, const zdd& A, zdd::label_type var);
894
907 __zdd
908 zdd_onset(const zdd& A);
909
913 __zdd
914 zdd_onset(const exec_policy& ep, const zdd& A);
915
928 __zdd
929 zdd_onset(const zdd& A, const generator<zdd::label_type>& vars);
930
934 __zdd
935 zdd_onset(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& vars);
936
952 template <typename ForwardIt>
953 __zdd
954 zdd_onset(const zdd& A, ForwardIt begin, ForwardIt end)
955 {
956 return zdd_onset(A, make_generator(begin, end));
957 }
958
962 template <typename ForwardIt>
963 __zdd
964 zdd_onset(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
965 {
966 return zdd_onset(ep, A, make_generator(begin, end));
967 }
968
983 __zdd
984 zdd_project(const zdd& A, const predicate<zdd::label_type>& dom);
985
987
996 __zdd
997 zdd_project(zdd&& A, const predicate<zdd::label_type>& dom);
998
1006 __zdd
1007 zdd_project(__zdd&& A, const predicate<zdd::label_type>& dom);
1008
1010
1015 __zdd
1016 zdd_project(const exec_policy& ep, const zdd& A, const predicate<zdd::label_type>& dom);
1017
1019
1028 __zdd
1029 zdd_project(const exec_policy& ep, zdd&& A, const predicate<zdd::label_type>& dom);
1030
1038 __zdd
1039 zdd_project(const exec_policy& ep, __zdd&& A, const predicate<zdd::label_type>& dom);
1040
1042
1058 __zdd
1059 zdd_project(const zdd& A, const generator<zdd::label_type>& dom);
1060
1062
1071 __zdd
1072 zdd_project(zdd&& A, const generator<zdd::label_type>& dom);
1073
1081 __zdd
1082 zdd_project(__zdd&& A, const generator<zdd::label_type>& dom);
1083
1085
1090 __zdd
1091 zdd_project(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& dom);
1092
1094
1103 __zdd
1104 zdd_project(const exec_policy& ep, zdd&& A, const generator<zdd::label_type>& dom);
1105
1113 __zdd
1114 zdd_project(const exec_policy& ep, __zdd&& A, const generator<zdd::label_type>& dom);
1115
1117
1136 template <typename ForwardIt>
1137 __zdd
1138 zdd_project(const zdd& A, ForwardIt begin, ForwardIt end)
1139 {
1140 return zdd_project(A, make_generator(begin, end));
1141 }
1142
1144
1153 template <typename ForwardIt>
1154 __zdd
1155 zdd_project(zdd&& A, ForwardIt begin, ForwardIt end)
1156 {
1157 return zdd_project(std::move(A), make_generator(begin, end));
1158 }
1159
1167 template <typename ForwardIt>
1168 __zdd
1169 zdd_project(__zdd&& A, ForwardIt begin, ForwardIt end)
1170 {
1171 return zdd_project(std::move(A), make_generator(begin, end));
1172 }
1173
1175
1180 template <typename ForwardIt>
1181 __zdd
1182 zdd_project(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
1183 {
1184 return zdd_project(ep, A, make_generator(begin, end));
1185 }
1186
1188
1197 template <typename ForwardIt>
1198 __zdd
1199 zdd_project(const exec_policy& ep, zdd&& A, ForwardIt begin, ForwardIt end)
1200 {
1201 return zdd_project(ep, std::move(A), make_generator(begin, end));
1202 }
1203
1211 template <typename ForwardIt>
1212 __zdd
1213 zdd_project(const exec_policy& ep, __zdd&& A, ForwardIt begin, ForwardIt end)
1214 {
1215 return zdd_project(ep, std::move(A), make_generator(begin, end));
1216 }
1217
1219
1222
1227
1233 bool
1234 zdd_iscanonical(const zdd& A);
1235
1239 bool
1240 zdd_isterminal(const zdd& A);
1241
1245 bool
1246 zdd_isfalse(const zdd& A);
1247
1251 bool
1252 zdd_isempty(const zdd& A);
1253
1257 bool
1258 zdd_istrue(const zdd& A);
1259
1263 bool
1264 zdd_isnull(const zdd& A);
1265
1269 bool
1270 zdd_ispoint(const zdd& A);
1271
1275 bool
1276 zdd_equal(const zdd& A, const zdd& B);
1277
1281 bool
1282 zdd_equal(const exec_policy& ep, const zdd& A, const zdd& B);
1283
1287 bool
1288 operator==(const zdd& lhs, const zdd& rhs);
1289
1291 bool
1292 operator==(__zdd&&, __zdd&&);
1293 bool
1294 operator==(const zdd&, __zdd&&);
1295 bool
1296 operator==(__zdd&&, const zdd&);
1298
1302 bool
1303 zdd_unequal(const zdd& A, const zdd& B);
1304
1308 bool
1309 zdd_unequal(const exec_policy& ep, const zdd& A, const zdd& B);
1310
1314 bool
1315 operator!=(const zdd& lhs, const zdd& rhs);
1316
1318 bool
1319 operator!=(__zdd&&, __zdd&&);
1320 bool
1321 operator!=(const zdd&, __zdd&&);
1322 bool
1323 operator!=(__zdd&&, const zdd&);
1325
1329 bool
1330 zdd_subseteq(const zdd& A, const zdd& B);
1331
1335 bool
1336 zdd_subseteq(const exec_policy& ep, const zdd& A, const zdd& B);
1337
1341 bool
1342 operator<=(const zdd& lhs, const zdd& rhs);
1343
1345 bool
1346 operator<=(__zdd&&, __zdd&&);
1347 bool
1348 operator<=(const zdd&, __zdd&&);
1349 bool
1350 operator<=(__zdd&&, const zdd&);
1352
1356 bool
1357 operator>=(const zdd& lhs, const zdd& rhs);
1358
1360 bool
1361 operator>=(__zdd&&, __zdd&&);
1362 bool
1363 operator>=(const zdd&, __zdd&&);
1364 bool
1365 operator>=(__zdd&&, const zdd&);
1367
1371 bool
1372 zdd_subset(const zdd& A, const zdd& B);
1373
1377 bool
1378 zdd_subset(const exec_policy& ep, const zdd& A, const zdd& B);
1379
1383 bool
1384 operator<(const zdd& lhs, const zdd& rhs);
1385
1387 bool
1388 operator<(__zdd&&, __zdd&&);
1389 bool
1390 operator<(const zdd&, __zdd&&);
1391 bool
1392 operator<(__zdd&&, const zdd&);
1394
1398 bool
1399 operator>(const zdd& lhs, const zdd& rhs);
1400
1402 bool
1403 operator>(__zdd&&, __zdd&&);
1404 bool
1405 operator>(const zdd&, __zdd&&);
1406 bool
1407 operator>(__zdd&&, const zdd&);
1409
1413 bool
1414 zdd_disjoint(const zdd& A, const zdd& B);
1415
1419 bool
1420 zdd_disjoint(const exec_policy& ep, const zdd& A, const zdd& B);
1421
1424
1429
1433 size_t
1434 zdd_nodecount(const zdd& A);
1435
1440 zdd::label_type
1441 zdd_varcount(const zdd& A);
1442
1446 uint64_t
1447 zdd_size(const zdd& A);
1448
1452 uint64_t
1453 zdd_size(const exec_policy& ep, const zdd& A);
1454
1457
1462
1472 void
1473 zdd_support(const zdd& A, const consumer<zdd::label_type>& cb);
1474
1487 template <typename OutputIt,
1488 typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>
1489 OutputIt
1490 zdd_support(const zdd& A, OutputIt iter)
1491 {
1492 zdd_support(A, make_consumer<zdd::label_type>(iter));
1493 return iter;
1494 }
1495
1501 zdd::label_type
1502 zdd_topvar(const zdd& f);
1503
1509 zdd::label_type
1510 zdd_minvar(const zdd& A);
1511
1517 zdd::label_type
1518 zdd_maxvar(const zdd& A);
1519
1532 bool
1533 zdd_contains(const zdd& A, const generator<zdd::label_type>& a);
1534
1550 template <typename ForwardIt>
1551 bool
1556
1567 zdd
1568 zdd_minelem(const zdd& A);
1569
1582 void
1583 zdd_minelem(const zdd& A, const consumer<zdd::label_type>& cb);
1584
1596 template <typename OutputIt,
1597 typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>
1598 OutputIt
1599 zdd_minelem(const zdd& A, OutputIt iter)
1600 {
1601 zdd_minelem(A, make_consumer<zdd::label_type>(iter));
1602 return iter;
1603 }
1604
1615 zdd
1616 zdd_maxelem(const zdd& A);
1617
1630 void
1631 zdd_maxelem(const zdd& A, const consumer<zdd::label_type>& cb);
1632
1644 template <typename OutputIt,
1645 typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>
1646 OutputIt
1647 zdd_maxelem(const zdd& A, OutputIt iter)
1648 {
1649 zdd_maxelem(A, make_consumer<zdd::label_type>(iter));
1650 return iter;
1651 }
1652
1655
1660
1674 __zdd
1675 zdd_from(const bdd& f, const generator<zdd::label_type>& dom);
1676
1681 __zdd
1682 zdd_from(const exec_policy& ep, const bdd& f, const generator<zdd::label_type>& dom);
1683
1700 template <typename ForwardIt>
1701 __zdd
1702 zdd_from(const bdd& f, ForwardIt begin, ForwardIt end)
1703 {
1704 return zdd_from(f, make_generator(begin, end));
1705 }
1706
1711 template <typename ForwardIt>
1712 __zdd
1713 zdd_from(const exec_policy& ep, const bdd& f, ForwardIt begin, ForwardIt end)
1714 {
1715 return bdd_from(ep, f, make_generator(begin, end));
1716 }
1717
1730 __zdd
1731 zdd_from(const bdd& f);
1732
1737 __zdd
1738 zdd_from(const exec_policy& ep, const bdd& f);
1739
1742
1747
1751 void
1752 zdd_printdot(const zdd& A, std::ostream& out = std::cout, bool include_id = false);
1753
1757 void
1758 zdd_printdot(const zdd& A, const std::string& file_name, bool include_id = false);
1759
1762
1765}
1766
1767#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:282
adiar::zdd
Reduced Ordered Zero-suppressed Decision Diagram.
Definition zdd.h:62
adiar::operator|
__bdd operator|(const bdd &lhs, const bdd &rhs)
adiar::bdd_from
__bdd bdd_from(const zdd &A, const generator< bdd::label_type > &dom)
Obtains the BDD that represents the same function/set as the given ZDD within the given domain.
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:169
adiar::consumer
function< void(Arg)> consumer
Consumer function of value(s) of type(s) Args.
Definition functional.h:60
adiar::make_generator
generator< typename ForwardIt::value_type > make_generator(ForwardIt &begin, ForwardIt &end)
Wrap a begin and end iterator pair into a generator function.
Definition functional.h:176
adiar::predicate
function< bool(Args...)> predicate
Predicate function given value(s) of type(s) Args.
Definition functional.h:48
adiar::make_consumer
consumer< ValueType > make_consumer(OutputIt &iter)
Wrap an iterator into a consumer function.
Definition functional.h:67
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 in the ZDD.
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