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
21
22#include <iostream>
23#include <string>
24
25#include <adiar/bdd/bdd.h>
26#include <adiar/bool_op.h>
27#include <adiar/exec_policy.h>
28#include <adiar/functional.h>
29#include <adiar/zdd/zdd.h>
30
31namespace adiar
32{
47
56 zdd
57 zdd_terminal(bool value);
58
62 zdd
63 zdd_empty();
64
68 zdd
69 zdd_null();
70
89 zdd
90 zdd_ithvar(zdd::label_type var, const generator<zdd::label_type>& dom);
91
110 template <typename ForwardIt>
111 zdd
116
125 zdd
126 zdd_ithvar(zdd::label_type var);
127
146 zdd
147 zdd_nithvar(zdd::label_type var, const generator<zdd::label_type>& dom);
148
167 template <typename ForwardIt>
168 zdd
173
182 zdd
183 zdd_nithvar(zdd::label_type var);
184
198 zdd
199 zdd_vars(const generator<zdd::label_type>& vars);
200
214 template <typename ForwardIt>
215 zdd
220
233 zdd
234 zdd_point(const generator<zdd::label_type>& vars);
235
249 template <typename ForwardIt>
250 zdd
255
268 zdd
269 zdd_singleton(zdd::label_type var);
270
284 zdd
285 zdd_singletons(const generator<zdd::label_type>& vars);
286
300 template <typename ForwardIt>
301 zdd
306
319 zdd
320 zdd_powerset(const generator<zdd::label_type>& vars);
321
335 template <typename ForwardIt>
336 zdd
341
351 zdd
352 zdd_bot(const generator<zdd::label_type>& dom);
353
366 template <typename ForwardIt>
367 inline zdd
372
378 zdd
379 zdd_bot();
380
390 zdd
391 zdd_top(const generator<zdd::label_type>& dom);
392
405 template <typename ForwardIt>
406 inline zdd
411
420 zdd
421 zdd_top();
422
426
438
455 __zdd
456 zdd_binop(const zdd& A, const zdd& B, const predicate<bool, bool>& op);
457
462 __zdd
463 zdd_binop(const exec_policy& ep, const zdd& A, const zdd& B, const predicate<bool, bool>& op);
465
471 __zdd
472 zdd_union(const zdd& A, const zdd& B);
473
478 __zdd
479 zdd_union(const exec_policy& ep, const zdd& A, const zdd& B);
481
485 __zdd
486 operator|(const zdd& lhs, const zdd& rhs);
487
489 __zdd
490 operator|(__zdd&&, __zdd&&);
491 __zdd
492 operator|(const zdd&, __zdd&&);
493 __zdd
494 operator|(__zdd&&, const zdd&);
496
500 zdd
501 operator+(const zdd& A);
502
504 __zdd
505 operator+(__zdd&& A);
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
528 __zdd
529 zdd_intsec(const zdd& A, const zdd& B);
530
535 __zdd
536 zdd_intsec(const exec_policy& ep, const zdd& A, const zdd& B);
538
542 __zdd
543 operator&(const zdd& lhs, const zdd& rhs);
544
546 __zdd
547 operator&(__zdd&&, __zdd&&);
548 __zdd
549 operator&(const zdd&, __zdd&&);
550 __zdd
551 operator&(__zdd&&, const zdd&);
553
557 __zdd
558 operator*(const zdd& lhs, const zdd& rhs);
559
561 __zdd
562 operator*(__zdd&&, __zdd&&);
563 __zdd
564 operator*(const zdd&, __zdd&&);
565 __zdd
566 operator*(__zdd&&, const zdd&);
568
574 __zdd
575 zdd_diff(const zdd& A, const zdd& B);
576
581 __zdd
582 zdd_diff(const exec_policy& ep, const zdd& A, const zdd& B);
584
591 __zdd
592 operator-(const zdd& A);
593
595 __zdd
596 operator-(__zdd&& A);
598
602 __zdd
603 operator-(const zdd& lhs, const zdd& rhs);
604
606 __zdd
607 operator-(__zdd&&, __zdd&&);
608 __zdd
609 operator-(const zdd&, __zdd&&);
610 __zdd
611 operator-(__zdd&&, const zdd&);
613
626 __zdd
627 zdd_change(const zdd& A, const generator<zdd::label_type>& vars);
628
633 __zdd
634 zdd_change(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& vars);
636
652 template <typename ForwardIt>
653 __zdd
658
663 template <typename ForwardIt>
664 __zdd
665 zdd_change(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
666 {
667 return zdd_change(ep, A, make_generator(begin, end));
668 }
670
682 __zdd
683 zdd_complement(const zdd& A, const generator<zdd::label_type>& dom);
684
689 __zdd
690 zdd_complement(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& dom);
692
708 template <typename ForwardIt>
709 __zdd
714
719 template <typename ForwardIt>
720 __zdd
721 zdd_complement(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
722 {
723 return zdd_complement(ep, A, make_generator(begin, end));
724 }
726
740 __zdd
741 zdd_complement(const zdd& A);
742
743
748 __zdd
749 zdd_complement(const exec_policy& ep, const zdd& A);
751
755 __zdd
756 operator~(const zdd& A);
757
759 __zdd
760 operator~(__zdd&& A);
762
778 __zdd
779 zdd_expand(const zdd& A, const generator<zdd::label_type>& vars);
780
785 __zdd
786 zdd_expand(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& vars);
788
809 template <typename ForwardIt>
810 __zdd
815
820 template <typename ForwardIt>
821 __zdd
822 zdd_expand(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
823 {
824 return zdd_expand(ep, A, make_generator(begin, end));
825 }
827
839 __zdd
840 zdd_offset(const zdd& A, zdd::label_type var);
841
846 __zdd
847 zdd_offset(const exec_policy& ep, const zdd& A, zdd::label_type var);
849
862 __zdd
863 zdd_offset(const zdd& A);
864
869 __zdd
870 zdd_offset(const exec_policy& ep, const zdd& A);
872
885 __zdd
886 zdd_offset(const zdd& A, const generator<zdd::label_type>& vars);
887
892 __zdd
893 zdd_offset(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& vars);
895
911 template <typename ForwardIt>
912 __zdd
917
922 template <typename ForwardIt>
923 __zdd
924 zdd_offset(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
925 {
926 return zdd_offset(ep, A, make_generator(begin, end));
927 }
929
941 __zdd
942 zdd_onset(const zdd& A, zdd::label_type var);
943
948 __zdd
949 zdd_onset(const exec_policy& ep, const zdd& A, zdd::label_type var);
951
964 __zdd
965 zdd_onset(const zdd& A);
966
971 __zdd
972 zdd_onset(const exec_policy& ep, const zdd& A);
974
987 __zdd
988 zdd_onset(const zdd& A, const generator<zdd::label_type>& vars);
989
994 __zdd
995 zdd_onset(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& vars);
997
1013 template <typename ForwardIt>
1014 __zdd
1015 zdd_onset(const zdd& A, ForwardIt begin, ForwardIt end)
1016 {
1017 return zdd_onset(A, make_generator(begin, end));
1018 }
1019
1024 template <typename ForwardIt>
1025 __zdd
1026 zdd_onset(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
1027 {
1028 return zdd_onset(ep, A, make_generator(begin, end));
1029 }
1031
1046 __zdd
1047 zdd_project(const zdd& A, const predicate<zdd::label_type>& dom);
1048
1050
1059 __zdd
1060 zdd_project(zdd&& A, const predicate<zdd::label_type>& dom);
1061
1069 __zdd
1070 zdd_project(__zdd&& A, const predicate<zdd::label_type>& dom);
1071
1076 __zdd
1077 zdd_project(const exec_policy& ep, const zdd& A, const predicate<zdd::label_type>& dom);
1078
1087 __zdd
1088 zdd_project(const exec_policy& ep, zdd&& A, const predicate<zdd::label_type>& dom);
1089
1097 __zdd
1098 zdd_project(const exec_policy& ep, __zdd&& A, const predicate<zdd::label_type>& dom);
1099
1101
1117 __zdd
1118 zdd_project(const zdd& A, const generator<zdd::label_type>& dom);
1119
1121
1130 __zdd
1131 zdd_project(zdd&& A, const generator<zdd::label_type>& dom);
1132
1140 __zdd
1141 zdd_project(__zdd&& A, const generator<zdd::label_type>& dom);
1142
1147 __zdd
1148 zdd_project(const exec_policy& ep, const zdd& A, const generator<zdd::label_type>& dom);
1149
1158 __zdd
1159 zdd_project(const exec_policy& ep, zdd&& A, const generator<zdd::label_type>& dom);
1160
1168 __zdd
1169 zdd_project(const exec_policy& ep, __zdd&& A, const generator<zdd::label_type>& dom);
1170
1172
1191 template <typename ForwardIt>
1192 __zdd
1193 zdd_project(const zdd& A, ForwardIt begin, ForwardIt end)
1194 {
1195 return zdd_project(A, make_generator(begin, end));
1196 }
1197
1199
1208 template <typename ForwardIt>
1209 __zdd
1210 zdd_project(zdd&& A, ForwardIt begin, ForwardIt end)
1211 {
1212 return zdd_project(std::move(A), make_generator(begin, end));
1213 }
1214
1222 template <typename ForwardIt>
1223 __zdd
1224 zdd_project(__zdd&& A, ForwardIt begin, ForwardIt end)
1225 {
1226 return zdd_project(std::move(A), make_generator(begin, end));
1227 }
1228
1233 template <typename ForwardIt>
1234 __zdd
1235 zdd_project(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
1236 {
1237 return zdd_project(ep, A, make_generator(begin, end));
1238 }
1239
1248 template <typename ForwardIt>
1249 __zdd
1250 zdd_project(const exec_policy& ep, zdd&& A, ForwardIt begin, ForwardIt end)
1251 {
1252 return zdd_project(ep, std::move(A), make_generator(begin, end));
1253 }
1254
1262 template <typename ForwardIt>
1263 __zdd
1264 zdd_project(const exec_policy& ep, __zdd&& A, ForwardIt begin, ForwardIt end)
1265 {
1266 return zdd_project(ep, std::move(A), make_generator(begin, end));
1267 }
1268
1270
1274
1286
1292 bool
1293 zdd_iscanonical(const zdd& A);
1294
1298 bool
1299 zdd_isterminal(const zdd& A);
1300
1310 bool
1311 zdd_isfalse(const zdd& A);
1312
1322 bool
1323 zdd_isempty(const zdd& A);
1324
1328 bool
1329 zdd_istrue(const zdd& A);
1330
1334 bool
1335 zdd_isnull(const zdd& A);
1336
1340 bool
1341 zdd_ispoint(const zdd& A);
1342
1346 bool
1347 zdd_equal(const zdd& A, const zdd& B);
1348
1353 bool
1354 zdd_equal(const exec_policy& ep, const zdd& A, const zdd& B);
1356
1360 bool
1361 operator==(const zdd& lhs, const zdd& rhs);
1362
1364 bool
1365 operator==(__zdd&&, __zdd&&);
1366 bool
1367 operator==(const zdd&, __zdd&&);
1368 bool
1369 operator==(__zdd&&, const zdd&);
1371
1375 bool
1376 zdd_unequal(const zdd& A, const zdd& B);
1377
1382 bool
1383 zdd_unequal(const exec_policy& ep, const zdd& A, const zdd& B);
1385
1389 bool
1390 operator!=(const zdd& lhs, const zdd& rhs);
1391
1393 bool
1394 operator!=(__zdd&&, __zdd&&);
1395 bool
1396 operator!=(const zdd&, __zdd&&);
1397 bool
1398 operator!=(__zdd&&, const zdd&);
1400
1404 bool
1405 zdd_subseteq(const zdd& A, const zdd& B);
1406
1411 bool
1412 zdd_subseteq(const exec_policy& ep, const zdd& A, const zdd& B);
1414
1418 bool
1419 operator<=(const zdd& lhs, const zdd& rhs);
1420
1422 bool
1423 operator<=(__zdd&&, __zdd&&);
1424 bool
1425 operator<=(const zdd&, __zdd&&);
1426 bool
1427 operator<=(__zdd&&, const zdd&);
1429
1433 bool
1434 operator>=(const zdd& lhs, const zdd& rhs);
1435
1437 bool
1438 operator>=(__zdd&&, __zdd&&);
1439 bool
1440 operator>=(const zdd&, __zdd&&);
1441 bool
1442 operator>=(__zdd&&, const zdd&);
1444
1448 bool
1449 zdd_subset(const zdd& A, const zdd& B);
1450
1455 bool
1456 zdd_subset(const exec_policy& ep, const zdd& A, const zdd& B);
1458
1462 bool
1463 operator<(const zdd& lhs, const zdd& rhs);
1464
1466 bool
1467 operator<(__zdd&&, __zdd&&);
1468 bool
1469 operator<(const zdd&, __zdd&&);
1470 bool
1471 operator<(__zdd&&, const zdd&);
1473
1477 bool
1478 operator>(const zdd& lhs, const zdd& rhs);
1479
1481 bool
1482 operator>(__zdd&&, __zdd&&);
1483 bool
1484 operator>(const zdd&, __zdd&&);
1485 bool
1486 operator>(__zdd&&, const zdd&);
1488
1492 bool
1493 zdd_disjoint(const zdd& A, const zdd& B);
1494
1499 bool
1500 zdd_disjoint(const exec_policy& ep, const zdd& A, const zdd& B);
1502
1506
1518
1522 size_t
1523 zdd_nodecount(const zdd& A);
1524
1529 zdd::label_type
1530 zdd_varcount(const zdd& A);
1531
1535 uint64_t
1536 zdd_size(const zdd& A);
1537
1542 uint64_t
1543 zdd_size(const exec_policy& ep, const zdd& A);
1545
1549
1561
1571 void
1572 zdd_support(const zdd& A, const consumer<zdd::label_type>& cb);
1573
1586 template <typename OutputIt,
1587 typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>
1588 OutputIt
1589 zdd_support(const zdd& A, OutputIt iter)
1590 {
1591 zdd_support(A, make_consumer<zdd::label_type>(iter));
1592 return iter;
1593 }
1594
1600 zdd::label_type
1601 zdd_topvar(const zdd& f);
1602
1608 zdd::label_type
1609 zdd_minvar(const zdd& A);
1610
1616 zdd::label_type
1617 zdd_maxvar(const zdd& A);
1618
1631 bool
1632 zdd_contains(const zdd& A, const generator<zdd::label_type>& a);
1633
1649 template <typename ForwardIt>
1650 bool
1655
1666 zdd
1667 zdd_minelem(const zdd& A);
1668
1681 void
1682 zdd_minelem(const zdd& A, const consumer<zdd::label_type>& cb);
1683
1695 template <typename OutputIt,
1696 typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>
1697 OutputIt
1698 zdd_minelem(const zdd& A, OutputIt iter)
1699 {
1700 zdd_minelem(A, make_consumer<zdd::label_type>(iter));
1701 return iter;
1702 }
1703
1714 zdd
1715 zdd_maxelem(const zdd& A);
1716
1729 void
1730 zdd_maxelem(const zdd& A, const consumer<zdd::label_type>& cb);
1731
1743 template <typename OutputIt,
1744 typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>
1745 OutputIt
1746 zdd_maxelem(const zdd& A, OutputIt iter)
1747 {
1748 zdd_maxelem(A, make_consumer<zdd::label_type>(iter));
1749 return iter;
1750 }
1751
1755
1767
1781 __zdd
1782 zdd_from(const bdd& f, const generator<zdd::label_type>& dom);
1783
1789 __zdd
1790 zdd_from(const exec_policy& ep, const bdd& f, const generator<zdd::label_type>& dom);
1792
1809 template <typename ForwardIt>
1810 __zdd
1811 zdd_from(const bdd& f, ForwardIt begin, ForwardIt end)
1812 {
1813 return zdd_from(f, make_generator(begin, end));
1814 }
1815
1821 template <typename ForwardIt>
1822 __zdd
1823 zdd_from(const exec_policy& ep, const bdd& f, ForwardIt begin, ForwardIt end)
1824 {
1825 return zdd_from(ep, f, make_generator(begin, end));
1826 }
1828
1841 __zdd
1842 zdd_from(const bdd& f);
1843
1849 __zdd
1850 zdd_from(const exec_policy& ep, const bdd& f);
1852
1856
1868
1872 void
1873 zdd_printdot(const zdd& A, std::ostream& out = std::cout, bool include_id = false);
1874
1878 void
1879 zdd_printdot(const zdd& A, const std::string& file_name, bool include_id = false);
1880
1884}
1885
1886#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:58
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:67
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~
bdd operator~(const bdd &f)
adiar::operator-
bdd operator-(const bdd &f)
adiar::operator!=
bool operator!=(const bdd &f, const bdd &g)
adiar::operator==
bool operator==(const bdd &f, const bdd &g)
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_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_onset
__zdd zdd_onset(const zdd &A, zdd::label_type var)
Subset that do include the given element.
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_offset
__zdd zdd_offset(const zdd &A, zdd::label_type var)
Subset that do not include the given element.
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_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_intsec
__zdd zdd_intsec(const zdd &A, const zdd &B)
The intersection of two families of sets.
adiar::zdd_diff
__zdd zdd_diff(const zdd &A, const zdd &B)
The set difference of two families of sets.
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_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_powerset
zdd zdd_powerset(const generator< zdd::label_type > &vars)
The powerset of all given variables.
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_singletons
zdd zdd_singletons(const generator< zdd::label_type > &vars)
The family { {1}, {2}, ..., {k} }.
adiar::zdd_bot
zdd zdd_bot()
Bottom of the powerset lattice.
adiar::zdd_singleton
zdd zdd_singleton(zdd::label_type var)
The family { {i} } .
adiar::zdd_empty
zdd zdd_empty()
The empty family, i.e. Ø .
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_size
uint64_t zdd_size(const zdd &A)
The number of sets in the family of sets.
adiar::zdd_nodecount
size_t zdd_nodecount(const zdd &A)
The number of (internal) nodes used to represent the family of sets.
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_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_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_maxvar
zdd::label_type zdd_maxvar(const zdd &A)
Get the maximal occurring variable in the family.
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_minelem
zdd zdd_minelem(const zdd &A)
Retrieves the lexicographically smallest set a in A.
adiar::zdd_maxelem
zdd zdd_maxelem(const zdd &A)
Retrieves the lexicographically largest set a in A.
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_disjoint
bool zdd_disjoint(const zdd &A, const zdd &B)
Whether the two families are disjoint.
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_isfalse
bool zdd_isfalse(const zdd &A)
Whether this ZDD is the false terminal.
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_isnull
bool zdd_isnull(const zdd &A)
Whether it is the null family, i.e. { Ø } .
adiar::operator<=
bool operator<=(const zdd &lhs, const zdd &rhs)
adiar::zdd_istrue
bool zdd_istrue(const zdd &A)
Whether this ZDD is the true terminal.
adiar::operator>=
bool operator>=(const zdd &lhs, const zdd &rhs)
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::operator<
bool operator<(const zdd &lhs, const zdd &rhs)
adiar::zdd_ispoint
bool zdd_ispoint(const zdd &A)
Whether it contains a single bit-vector a, i.e. A = { a }.
adiar::zdd_unequal
bool zdd_unequal(const zdd &A, const zdd &B)
Whether they represent two different families.
adiar::zdd_iscanonical
bool zdd_iscanonical(const zdd &A)
Check whether a given ZDD is canonical.
adiar
Core types.
Definition adiar.h:40