Adiar 2.1.0
An External Memory Decision Diagram Library
Loading...
Searching...
No Matches
bdd.h
1#ifndef ADIAR_BDD_H
2#define ADIAR_BDD_H
3
14
15#include <iostream>
16#include <string>
17#include <type_traits>
18
19#include <adiar/bdd/bdd.h>
20#include <adiar/bool_op.h>
21#include <adiar/exec_policy.h>
22#include <adiar/functional.h>
23#include <adiar/types.h>
24#include <adiar/zdd/zdd.h>
25
26namespace adiar
27{
32
40
49 bdd
50 bdd_const(bool value);
51
60 bdd
61 bdd_terminal(bool value);
62
70 bdd
71 bdd_false();
72
80 inline bdd
81 bdd_bot()
82 {
83 return bdd_false();
84 }
85
91 bdd
92 bdd_true();
93
101 inline bdd
102 bdd_top()
103 {
104 return bdd_true();
105 }
106
118 bdd
119 bdd_ithvar(bdd::label_type var);
120
132 bdd
133 bdd_nithvar(bdd::label_type var);
134
150 bdd
151 bdd_and(const generator<int>& vars);
152
165 bdd
166 bdd_and(const generator<pair<bdd::label_type, bool>>& vars);
167
186 template <typename ForwardIt, typename = enable_if<!is_convertible<ForwardIt, bdd>>>
187 bdd
188 bdd_and(ForwardIt begin, ForwardIt end)
189 {
190 return bdd_and(make_generator(begin, end));
191 }
192
208 bdd
209 bdd_or(const generator<int>& vars);
210
223 bdd
224 bdd_or(const generator<pair<bdd::label_type, bool>>& vars);
225
244 template <typename ForwardIt, typename = enable_if<!is_convertible<ForwardIt, bdd>>>
245 bdd
246 bdd_or(ForwardIt begin, ForwardIt end)
247 {
248 return bdd_or(make_generator(begin, end));
249 }
250
267 bdd
268 bdd_cube(const generator<int>& vars);
269
283 bdd
284 bdd_cube(const generator<pair<bdd::label_type, bool>>& vars);
285
305 template <typename ForwardIt>
306 bdd
307 bdd_cube(ForwardIt begin, ForwardIt end)
308 {
309 return bdd_cube(make_generator(begin, end));
310 }
311
314
319
329 bdd
330 bdd_not(const bdd& f);
331
333 bdd
334 bdd_not(bdd&& f);
336
340 bdd
341 operator~(const bdd& f);
342
344 bdd
345 operator~(bdd&& f);
346 bdd
347 operator~(__bdd&& f);
349
366 __bdd
367 bdd_apply(const bdd& f, const bdd& g, const predicate<bool, bool>& op);
368
372 __bdd
373 bdd_apply(const exec_policy& ep, const bdd& f, const bdd& g, const predicate<bool, bool>& op);
374
382 __bdd
383 bdd_and(const bdd& f, const bdd& g);
384
388 __bdd
389 bdd_and(const exec_policy& ep, const bdd& f, const bdd& g);
390
394 __bdd
395 operator&(const bdd& lhs, const bdd& rhs);
396
398 __bdd
399 operator&(const bdd&, __bdd&&);
400 __bdd
401 operator&(__bdd&&, const bdd&);
402 __bdd
403 operator&(__bdd&&, __bdd&&);
405
409 __bdd
410 operator*(const bdd& lhs, const bdd& rhs);
411
413 __bdd
414 operator*(const bdd&, __bdd&&);
415 __bdd
416 operator*(__bdd&&, const bdd&);
417 __bdd
418 operator*(__bdd&&, __bdd&&);
420
428 __bdd
429 bdd_nand(const bdd& f, const bdd& g);
430
434 __bdd
435 bdd_nand(const exec_policy& ep, const bdd& f, const bdd& g);
436
444 __bdd
445 bdd_or(const bdd& f, const bdd& g);
446
450 __bdd
451 bdd_or(const exec_policy& ep, const bdd& f, const bdd& g);
452
456 __bdd
457 operator|(const bdd& lhs, const bdd& rhs);
458
460 __bdd
461 operator|(const bdd&, __bdd&&);
462 __bdd
463 operator|(__bdd&&, const bdd&);
464 __bdd
465 operator|(__bdd&&, __bdd&&);
467
471 bdd
472 operator+(const bdd& f);
473
478 __bdd
479 operator+(__bdd&& f);
481
485 __bdd
486 operator+(const bdd& lhs, const bdd& rhs);
487
489 __bdd
490 operator+(const bdd&, __bdd&&);
491 __bdd
492 operator+(__bdd&&, const bdd&);
493 __bdd
494 operator+(__bdd&&, __bdd&&);
496
504 __bdd
505 bdd_nor(const bdd& f, const bdd& g);
506
510 __bdd
511 bdd_nor(const exec_policy& ep, const bdd& f, const bdd& g);
512
520 __bdd
521 bdd_xor(const bdd& f, const bdd& g);
522
526 __bdd
527 bdd_xor(const exec_policy& ep, const bdd& f, const bdd& g);
528
532 __bdd
533 operator^(const bdd& lhs, const bdd& rhs);
534
536 __bdd
537 operator^(const bdd&, __bdd&&);
538 __bdd
539 operator^(__bdd&&, const bdd&);
540 __bdd
541 operator^(__bdd&&, __bdd&&);
543
551 __bdd
552 bdd_xnor(const bdd& f, const bdd& g);
553
557 __bdd
558 bdd_xnor(const exec_policy& ep, const bdd& f, const bdd& g);
559
567 __bdd
568 bdd_imp(const bdd& f, const bdd& g);
569
573 __bdd
574 bdd_imp(const exec_policy& ep, const bdd& f, const bdd& g);
575
583 __bdd
584 bdd_invimp(const bdd& f, const bdd& g);
585
589 __bdd
590 bdd_invimp(const exec_policy& ep, const bdd& f, const bdd& g);
591
599 __bdd
600 bdd_equiv(const bdd& f, const bdd& g);
601
605 __bdd
606 bdd_equiv(const exec_policy& ep, const bdd& f, const bdd& g);
607
615 __bdd
616 bdd_diff(const bdd& f, const bdd& g);
617
621 __bdd
622 bdd_diff(const exec_policy& ep, const bdd& f, const bdd& g);
623
629 bdd
630 operator-(const bdd& f);
631
633 __bdd
634 operator-(__bdd&& f);
636
640 __bdd
641 operator-(const bdd& lhs, const bdd& rhs);
642
644 __bdd
645 operator-(const bdd&, __bdd&&);
646 __bdd
647 operator-(__bdd&&, const bdd&);
648 __bdd
649 operator-(__bdd&&, __bdd&&);
651
659 __bdd
660 bdd_less(const bdd& f, const bdd& g);
661
665 __bdd
666 bdd_less(const exec_policy& ep, const bdd& f, const bdd& g);
667
691 __bdd
692 bdd_ite(const bdd& f, const bdd& g, const bdd& h);
693
697 __bdd
698 bdd_ite(const exec_policy& ep, const bdd& f, const bdd& g, const bdd& h);
699
716 __bdd
717 bdd_restrict(const bdd& f, bdd::label_type var, bool val);
718
722 __bdd
723 bdd_restrict(const exec_policy& ep, const bdd& f, bdd::label_type var, bool val);
724
740 __bdd
741 bdd_restrict(const bdd& f, const generator<pair<bdd::label_type, bool>>& xs);
742
746 __bdd
747 bdd_restrict(const exec_policy& ep,
748 const bdd& f,
749 const generator<pair<bdd::label_type, bool>>& xs);
750
769 template <typename ForwardIt>
770 __bdd
771 bdd_restrict(const bdd& f, ForwardIt begin, ForwardIt end)
772 {
773 return bdd_restrict(f, make_generator(begin, end));
774 }
775
779 template <typename ForwardIt>
780 __bdd
781 bdd_restrict(const exec_policy& ep, const bdd& f, ForwardIt begin, ForwardIt end)
782 {
783 return bdd_restrict(ep, f, make_generator(begin, end));
784 }
785
797 __bdd
798 bdd_low(const bdd& f);
799
803 __bdd
804 bdd_low(const exec_policy& ep, const bdd& f);
805
817 __bdd
818 bdd_high(const bdd& f);
819
823 __bdd
824 bdd_high(const exec_policy& ep, const bdd& f);
825
840 __bdd
841 bdd_exists(const bdd& f, bdd::label_type var);
842
844
848 inline __bdd
849 bdd_exists(bdd&& f, bdd::label_type var)
850 {
851 return bdd_exists(f, var);
852 }
853
855
859 __bdd
860 bdd_exists(const exec_policy& ep, const bdd& f, bdd::label_type var);
861
863
867 inline __bdd
868 bdd_exists(const exec_policy& ep, bdd&& f, bdd::label_type var)
869 {
870 return bdd_exists(ep, f, var);
871 }
872
874
888 __bdd
889 bdd_exists(const bdd& f, const predicate<bdd::label_type>& vars);
890
892
900 __bdd
901 bdd_exists(bdd&& f, const predicate<bdd::label_type>& vars);
902
909 __bdd
910 bdd_exists(__bdd&& f, const predicate<bdd::label_type>& vars);
911
913
917 __bdd
918 bdd_exists(const exec_policy& ep, const bdd& f, const predicate<bdd::label_type>& vars);
919
921
929 __bdd
930 bdd_exists(const exec_policy& ep, bdd&& f, const predicate<bdd::label_type>& vars);
931
938 __bdd
939 bdd_exists(const exec_policy& ep, __bdd&& f, const predicate<bdd::label_type>& vars);
940
942
955 __bdd
956 bdd_exists(const bdd& f, const generator<bdd::label_type>& vars);
957
959
967 __bdd
968 bdd_exists(bdd&& f, const generator<bdd::label_type>& vars);
969
976 __bdd
977 bdd_exists(__bdd&& f, const generator<bdd::label_type>& vars);
978
980
984 __bdd
985 bdd_exists(const exec_policy& ep, const bdd& f, const generator<bdd::label_type>& vars);
986
988
996 __bdd
997 bdd_exists(const exec_policy& ep, bdd&& f, const generator<bdd::label_type>& vars);
998
1005 __bdd
1006 bdd_exists(const exec_policy& ep, __bdd&& f, const generator<bdd::label_type>& vars);
1007
1009
1025 template <typename ForwardIt>
1026 __bdd
1027 bdd_exists(const bdd& f, ForwardIt begin, ForwardIt end)
1028 {
1029 return bdd_exists(f, make_generator(begin, end));
1030 }
1031
1033
1041 template <typename ForwardIt>
1042 __bdd
1043 bdd_exists(bdd&& f, ForwardIt begin, ForwardIt end)
1044 {
1045 return bdd_exists(std::move(f), make_generator(begin, end));
1046 }
1047
1054 template <typename ForwardIt>
1055 __bdd
1056 bdd_exists(__bdd&& f, ForwardIt begin, ForwardIt end)
1057 {
1058 return bdd_exists(std::move(f), make_generator(begin, end));
1059 }
1060
1062
1066 template <typename ForwardIt>
1067 __bdd
1068 bdd_exists(const exec_policy& ep, const bdd& f, ForwardIt begin, ForwardIt end)
1069 {
1070 return bdd_exists(ep, f, make_generator(begin, end));
1071 }
1072
1074
1082 template <typename ForwardIt>
1083 __bdd
1084 bdd_exists(const exec_policy& ep, bdd&& f, ForwardIt begin, ForwardIt end)
1085 {
1086 return bdd_exists(ep, std::move(f), make_generator(begin, end));
1087 }
1088
1095 template <typename ForwardIt>
1096 __bdd
1097 bdd_exists(const exec_policy& ep, __bdd&& f, ForwardIt begin, ForwardIt end)
1098 {
1099 return bdd_exists(ep, std::move(f), make_generator(begin, end));
1100 }
1101
1103
1118 __bdd
1119 bdd_forall(const bdd& f, bdd::label_type var);
1120
1122
1126 inline __bdd
1127 bdd_forall(bdd&& f, bdd::label_type var)
1128 {
1129 return bdd_forall(f, var);
1130 }
1131
1133
1137 __bdd
1138 bdd_forall(const exec_policy& ep, const bdd& f, bdd::label_type var);
1139
1141
1145 inline __bdd
1146 bdd_forall(const exec_policy& ep, bdd&& f, bdd::label_type var)
1147 {
1148 return bdd_forall(ep, f, var);
1149 }
1150
1152
1166 __bdd
1167 bdd_forall(const bdd& f, const predicate<bdd::label_type>& vars);
1168
1170
1178 __bdd
1179 bdd_forall(bdd&& f, const predicate<bdd::label_type>& vars);
1180
1187 __bdd
1188 bdd_forall(__bdd&& f, const predicate<bdd::label_type>& vars);
1189
1191
1195 __bdd
1196 bdd_forall(const exec_policy& ep, const bdd& f, const predicate<bdd::label_type>& vars);
1197
1199
1207 __bdd
1208 bdd_forall(const exec_policy& ep, bdd&& f, const predicate<bdd::label_type>& vars);
1209
1216 __bdd
1217 bdd_forall(const exec_policy& ep, __bdd&& f, const predicate<bdd::label_type>& vars);
1218
1220
1233 __bdd
1234 bdd_forall(const bdd& f, const generator<bdd::label_type>& vars);
1235
1237
1245 __bdd
1246 bdd_forall(bdd&& f, const generator<bdd::label_type>& vars);
1247
1254 __bdd
1255 bdd_forall(bdd&& f, const generator<bdd::label_type>& vars);
1256
1258
1262 __bdd
1263 bdd_forall(const exec_policy& ep, const bdd& f, const generator<bdd::label_type>& vars);
1264
1266
1274 __bdd
1275 bdd_forall(const exec_policy& ep, bdd&& f, const generator<bdd::label_type>& vars);
1276
1283 __bdd
1284 bdd_forall(const exec_policy& ep, __bdd&& f, const generator<bdd::label_type>& vars);
1285
1287
1303 template <typename ForwardIt>
1304 __bdd
1305 bdd_forall(const bdd& f, ForwardIt begin, ForwardIt end)
1306 {
1307 return bdd_forall(f, make_generator(begin, end));
1308 }
1309
1311
1319 template <typename ForwardIt>
1320 __bdd
1321 bdd_forall(bdd&& f, ForwardIt begin, ForwardIt end)
1322 {
1323 return bdd_forall(std::move(f), make_generator(begin, end));
1324 }
1325
1332 template <typename ForwardIt>
1333 __bdd
1334 bdd_forall(__bdd&& f, ForwardIt begin, ForwardIt end)
1335 {
1336 return bdd_forall(std::move(f), make_generator(begin, end));
1337 }
1338
1340
1344 template <typename ForwardIt>
1345 __bdd
1346 bdd_forall(const exec_policy& ep, const bdd& f, ForwardIt begin, ForwardIt end)
1347 {
1348 return bdd_forall(ep, f, make_generator(begin, end));
1349 }
1350
1352
1360 template <typename ForwardIt>
1361 __bdd
1362 bdd_forall(const exec_policy& ep, bdd&& f, ForwardIt begin, ForwardIt end)
1363 {
1364 return bdd_forall(ep, std::move(f), make_generator(begin, end));
1365 }
1366
1373 template <typename ForwardIt>
1374 __bdd
1375 bdd_forall(const exec_policy& ep, __bdd&& f, ForwardIt begin, ForwardIt end)
1376 {
1377 return bdd_forall(ep, std::move(f), make_generator(begin, end));
1378 }
1379
1381
1384
1389
1401 bdd
1402 bdd_replace(const bdd& f, const function<bdd::label_type(bdd::label_type)>& m);
1403
1407 bdd
1408 bdd_replace(const exec_policy& ep,
1409 const bdd& f,
1410 const function<bdd::label_type(bdd::label_type)>& m);
1411
1426 bdd
1427 bdd_replace(const bdd& f,
1428 const function<bdd::label_type(bdd::label_type)>& m,
1429 replace_type m_type);
1430
1434 bdd
1435 bdd_replace(const exec_policy& ep,
1436 const bdd& f,
1437 const function<bdd::label_type(bdd::label_type)>& m,
1438 replace_type m_type);
1439
1441
1456 bdd
1457 bdd_replace(__bdd&& f, const function<bdd::label_type(bdd::label_type)>& m);
1458
1462 bdd
1463 bdd_replace(const exec_policy& ep,
1464 __bdd&& f,
1465 const function<bdd::label_type(bdd::label_type)>& m);
1466
1482 bdd
1483 bdd_replace(__bdd&& f, const function<bdd::label_type(bdd::label_type)>& m, replace_type m_type);
1484
1488 bdd
1489 bdd_replace(const exec_policy& ep,
1490 __bdd&& f,
1491 const function<bdd::label_type(bdd::label_type)>& m,
1492 replace_type m_type);
1493
1495
1498
1503
1518 bdd
1519 bdd_relprod(const bdd& states, const bdd& relation, const predicate<bdd::label_type>& pred);
1520
1524 bdd
1525 bdd_relprod(const exec_policy& ep,
1526 const bdd& states,
1527 const bdd& relation,
1528 const predicate<bdd::label_type>& pred);
1529
1549 bdd
1550 bdd_relnext(const bdd& states,
1551 const bdd& relation,
1552 const function<optional<bdd::label_type>(bdd::label_type)>& m);
1553
1557 bdd
1558 bdd_relnext(const exec_policy& ep,
1559 const bdd& states,
1560 const bdd& relation,
1561 const function<optional<bdd::label_type>(bdd::label_type)>& m);
1562
1585 bdd
1586 bdd_relnext(const bdd& states,
1587 const bdd& relation,
1588 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1589 replace_type m_type);
1590
1594 bdd
1595 bdd_relnext(const exec_policy& ep,
1596 const bdd& states,
1597 const bdd& relation,
1598 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1599 replace_type m_type);
1600
1617 bdd
1618 bdd_relnext(const bdd& states, const bdd& relation, const bdd::label_type varcount);
1619
1624 bdd
1625 bdd_relnext(const exec_policy& ep,
1626 const bdd& states,
1627 const bdd& relation,
1628 const bdd::label_type varcount);
1629
1645 bdd
1646 bdd_relnext(const bdd& states, const bdd& relation);
1647
1652 bdd
1653 bdd_relnext(const exec_policy& ep, const bdd& states, const bdd& relation);
1654
1675 bdd
1676 bdd_relprev(const bdd& states,
1677 const bdd& relation,
1678 const function<optional<bdd::label_type>(bdd::label_type)>& m);
1679
1683 bdd
1684 bdd_relprev(const exec_policy& ep,
1685 const bdd& states,
1686 const bdd& relation,
1687 const function<optional<bdd::label_type>(bdd::label_type)>& m);
1688
1712 bdd
1713 bdd_relprev(const bdd& states,
1714 const bdd& relation,
1715 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1716 replace_type m_type);
1717
1721 bdd
1722 bdd_relprev(const exec_policy& ep,
1723 const bdd& states,
1724 const bdd& relation,
1725 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1726 replace_type m_type);
1727
1744 bdd
1745 bdd_relprev(const bdd& states, const bdd& relation, const bdd::label_type varcount);
1746
1751 bdd
1752 bdd_relprev(const exec_policy& ep,
1753 const bdd& states,
1754 const bdd& relation,
1755 const bdd::label_type varcount);
1756
1771 bdd
1772 bdd_relprev(const bdd& states, const bdd& relation);
1773
1778 bdd
1779 bdd_relprev(const exec_policy& ep, const bdd& states, const bdd& relation);
1780
1783
1788
1794 bool
1795 bdd_iscanonical(const bdd& f);
1796
1802 bool
1803 bdd_isconst(const bdd& f);
1804
1810 bool
1811 bdd_isterminal(const bdd& f);
1812
1816 bool
1817 bdd_isfalse(const bdd& f);
1818
1822 bool
1823 bdd_istrue(const bdd& f);
1824
1832 bool
1833 bdd_isvar(const bdd& f);
1834
1842 bool
1843 bdd_isithvar(const bdd& f);
1844
1852 bool
1853 bdd_isnithvar(const bdd& f);
1854
1860 bool
1861 bdd_iscube(const bdd& f);
1862
1870 bool
1871 bdd_equal(const bdd& f, const bdd& g);
1872
1876 bool
1877 bdd_equal(const exec_policy&, const bdd& f, const bdd& g);
1878
1882 bool
1883 operator==(const bdd& f, const bdd& g);
1884
1886 bool
1887 operator==(__bdd&& f, const bdd& g);
1888 bool
1889 operator==(const bdd& f, __bdd&& g);
1890 bool
1891 operator==(__bdd&& f, __bdd&& g);
1893
1903 bool
1904 bdd_unequal(const bdd& f, const bdd& g);
1905
1909 bool
1910 bdd_unequal(const exec_policy& ep, const bdd& f, const bdd& g);
1911
1915 bool
1916 operator!=(const bdd& f, const bdd& g);
1917
1919 bool
1920 operator!=(const bdd& f, __bdd&& g);
1921 bool
1922 operator!=(__bdd&& f, const bdd& g);
1923 bool
1924 operator!=(__bdd&& f, __bdd&& g);
1926
1929
1934
1938 size_t
1939 bdd_nodecount(const bdd& f);
1940
1945 bdd::label_type
1946 bdd_varcount(const bdd& f);
1947
1953 uint64_t
1954 bdd_pathcount(const bdd& f);
1955
1959 uint64_t
1960 bdd_pathcount(const exec_policy& ep, const bdd& f);
1961
1976 uint64_t
1977 bdd_satcount(const bdd& f, bdd::label_type varcount);
1978
1982 uint64_t
1983 bdd_satcount(const exec_policy& ep, const bdd& f, bdd::label_type varcount);
1984
1993 uint64_t
1994 bdd_satcount(const bdd& f);
1995
1999 uint64_t
2000 bdd_satcount(const exec_policy& ep, const bdd& f);
2001
2004
2009
2020 void
2021 bdd_support(const bdd& f, const consumer<bdd::label_type>& cb);
2022
2035 template <typename OutputIt,
2036 typename = enable_if<!is_convertible<OutputIt, consumer<bdd::label_type>>>>
2037 OutputIt
2038 bdd_support(const bdd& f, OutputIt iter)
2039 {
2040 bdd_support(f, make_consumer<bdd::label_type>(iter));
2041 return iter;
2042 }
2043
2049 bdd::label_type
2050 bdd_topvar(const bdd& f);
2051
2057 bdd::label_type
2058 bdd_minvar(const bdd& f);
2059
2065 bdd::label_type
2066 bdd_maxvar(const bdd& f);
2067
2077 bdd
2078 bdd_satmin(const bdd& f);
2079
2092 bdd
2093 bdd_satmin(const bdd& f,
2094 const generator<bdd::label_type>& d,
2095 const size_t d_size = bdd::max_label + 1);
2096
2112 template <typename ForwardIt, typename = enable_if<is_const<typename ForwardIt::reference>>>
2113 bdd
2114 bdd_satmin(const bdd& f, ForwardIt cbegin, ForwardIt cend)
2115 {
2116 return bdd_satmin(f, make_generator(cbegin, cend), std::distance(cbegin, cend));
2117 }
2118
2133 bdd
2134 bdd_satmin(const bdd& f, const bdd& d);
2135
2143 void
2144 bdd_satmin(const bdd& f, const consumer<pair<bdd::label_type, bool>>& c);
2145
2157 template <typename OutputIt,
2158 typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>>
2159 && !is_convertible<OutputIt, bdd>>>
2160 OutputIt
2166
2176 bdd
2177 bdd_satmax(const bdd& f);
2178
2190 bdd
2191 bdd_satmax(const bdd& f,
2192 const generator<bdd::label_type>& d,
2193 const size_t d_size = bdd::max_label + 1);
2194
2210 template <typename ForwardIt, typename = enable_if<is_const<typename ForwardIt::reference>>>
2211 bdd
2212 bdd_satmax(const bdd& f, ForwardIt cbegin, ForwardIt cend)
2213 {
2214 return bdd_satmax(f, make_generator(cbegin, cend), std::distance(cbegin, cend));
2215 }
2216
2231 bdd
2232 bdd_satmax(const bdd& f, const bdd& d);
2233
2241 void
2242 bdd_satmax(const bdd& f, const consumer<pair<bdd::label_type, bool>>& c);
2243
2255 template <typename OutputIt,
2256 typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>>
2257 && !is_convertible<OutputIt, bdd>>>
2258 OutputIt
2264
2278 pair<bdd, double>
2279 bdd_optmin(const bdd& f, const cost<bdd::label_type>& c);
2280
2285 pair<bdd, double>
2286 bdd_optmin(const exec_policy& ep, const bdd& f, const cost<bdd::label_type>& c);
2287
2305 double
2306 bdd_optmin(const bdd& f,
2307 const cost<bdd::label_type>& c,
2308 const consumer<pair<bdd::label_type, bool>>& cb);
2309
2314 double
2315 bdd_optmin(const exec_policy& ep,
2316 const bdd& f,
2317 const cost<bdd::label_type>& c,
2318 const consumer<pair<bdd::label_type, bool>>& cb);
2319
2332 bool
2333 bdd_eval(const bdd& f, const predicate<bdd::label_type>& xs);
2334
2350 bool
2351 bdd_eval(const bdd& f, const generator<pair<bdd::label_type, bool>>& xs);
2352
2371 template <typename ForwardIt>
2372 bool
2373 bdd_eval(const bdd& f, ForwardIt begin, ForwardIt end)
2374 {
2375 return bdd_eval(f, make_generator(begin, end));
2376 }
2377
2380
2385
2399 __bdd
2400 bdd_from(const zdd& A, const generator<bdd::label_type>& dom);
2401
2406 __bdd
2407 bdd_from(const exec_policy& ep, const zdd& A, const generator<bdd::label_type>& dom);
2408
2425 template <typename ForwardIt>
2426 __bdd
2427 bdd_from(const zdd& A, ForwardIt begin, ForwardIt end)
2428 {
2429 return bdd_from(A, make_generator(begin, end));
2430 }
2431
2436 template <typename ForwardIt>
2437 __bdd
2438 bdd_from(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
2439 {
2440 return bdd_from(ep, A, make_generator(begin, end));
2441 }
2442
2457 __bdd
2458 bdd_from(const zdd& A);
2459
2464 __bdd
2465 bdd_from(const exec_policy& ep, const zdd& A);
2466
2469
2474
2478 void
2479 bdd_printdot(const bdd& f, std::ostream& out = std::cout, bool include_id = false);
2480
2484 void
2485 bdd_printdot(const bdd& f, const std::string& file_name, bool include_id = false);
2486
2489
2492}
2493
2494#endif // ADIAR_BDD_H
adiar::__bdd
A (possibly) unreduced Binary Decision Diagram.
Definition bdd.h:22
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::max_label
static constexpr label_type max_label
The maximal possible value for a unique identifier's label.
Definition dd.h:292
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_diff
__bdd bdd_diff(const bdd &f, const bdd &g)
Logical 'difference' operator.
adiar::bdd_nodecount
size_t bdd_nodecount(const bdd &f)
The number of (internal) nodes used to represent the function.
adiar::bdd_nor
__bdd bdd_nor(const bdd &f, const bdd &g)
Logical 'nor' operator.
adiar::bdd_nithvar
bdd bdd_nithvar(bdd::label_type var)
The BDD representing the negation of the i'th variable.
adiar::bdd_terminal
bdd bdd_terminal(bool value)
The BDD representing the given constant value.
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::bdd_const
bdd bdd_const(bool value)
The BDD representing the given constant value.
adiar::bdd_satcount
uint64_t bdd_satcount(const bdd &f, bdd::label_type varcount)
Count the number of assignments x that make f(x) true.
adiar::bdd_relprod
bdd bdd_relprod(const bdd &states, const bdd &relation, const predicate< bdd::label_type > &pred)
Relational Product of states and a relation.
adiar::bdd_iscanonical
bool bdd_iscanonical(const bdd &f)
Check whether a BDD is canonical.
adiar::operator+
bdd operator+(const bdd &f)
adiar::bdd_optmin
pair< bdd, double > bdd_optmin(const bdd &f, const cost< bdd::label_type > &c)
Obtain the satisfying assignment that is minimal for the given linear cost function over the global d...
adiar::operator&
__bdd operator&(const bdd &lhs, const bdd &rhs)
adiar::bdd_invimp
__bdd bdd_invimp(const bdd &f, const bdd &g)
Logical 'inverse implication' operator.
adiar::bdd_unequal
bool bdd_unequal(const bdd &f, const bdd &g)
Whether the two BDDs represent different functions.
adiar::bdd_ithvar
bdd bdd_ithvar(bdd::label_type var)
The BDD representing the i'th variable.
adiar::bdd_relnext
bdd bdd_relnext(const bdd &states, const bdd &relation, const function< optional< bdd::label_type >(bdd::label_type)> &m)
Forwards step with the Relational Product, including relabelling.
adiar::bdd_true
bdd bdd_true()
The BDD representing the constant true.
adiar::bdd_cube
bdd bdd_cube(const generator< int > &vars)
The BDD representing the cube of all the given variables.
adiar::bdd_apply
__bdd bdd_apply(const bdd &f, const bdd &g, const predicate< bool, bool > &op)
Apply a binary operator between two BDDs.
adiar::bdd_xor
__bdd bdd_xor(const bdd &f, const bdd &g)
Logical 'xor' operator.
adiar::bdd_isithvar
bool bdd_isithvar(const bdd &f)
Whether a BDD is the function of a single positive variable.
adiar::operator*
__bdd operator*(const bdd &lhs, const bdd &rhs)
adiar::bdd_low
__bdd bdd_low(const bdd &f)
Restrict the root to false, i.e. follow its low edge.
adiar::bdd_ite
__bdd bdd_ite(const bdd &f, const bdd &g, const bdd &h)
If-Then-Else operator.
adiar::bdd_top
bdd bdd_top()
The top of the powerset lattice.
Definition bdd.h:102
adiar::bdd_printdot
void bdd_printdot(const bdd &f, std::ostream &out=std::cout, bool include_id=false)
Output a DOT drawing of a BDD to the given output stream.
adiar::bdd_not
bdd bdd_not(const bdd &f)
Negation of a BDD.
adiar::bdd_istrue
bool bdd_istrue(const bdd &f)
Whether a BDD is the constant true.
adiar::bdd_imp
__bdd bdd_imp(const bdd &f, const bdd &g)
Logical 'implication' operator.
adiar::bdd_satmin
bdd bdd_satmin(const bdd &f)
The lexicographically smallest cube x such that f(x) is true.
adiar::bdd_isvar
bool bdd_isvar(const bdd &f)
Whether a BDD is a function dependent on a single variable, i.e. is a literal.
adiar::bdd_relprev
bdd bdd_relprev(const bdd &states, const bdd &relation, const function< optional< bdd::label_type >(bdd::label_type)> &m)
Backwards step with the Relational Product, including relabelling.
adiar::bdd_isfalse
bool bdd_isfalse(const bdd &f)
Whether a BDD is the constant false.
adiar::bdd_high
__bdd bdd_high(const bdd &f)
Restrict the root to true, i.e. follow its high edge.
adiar::bdd_satmax
bdd bdd_satmax(const bdd &f)
The lexicographically largest cube x such that f(x) is true.
adiar::bdd_varcount
bdd::label_type bdd_varcount(const bdd &f)
The number of variables that influence the outcome of the Boolean function, i.e. the number of levels...
adiar::bdd_xnor
__bdd bdd_xnor(const bdd &f, const bdd &g)
Logical 'xnor' operator.
adiar::operator!=
bool operator!=(const bdd &f, const bdd &g)
adiar::bdd_equiv
__bdd bdd_equiv(const bdd &f, const bdd &g)
Logical 'equivalence' operator.
adiar::bdd_bot
bdd bdd_bot()
The bottom of the powerset lattice.
Definition bdd.h:81
adiar::bdd_iscube
bool bdd_iscube(const bdd &f)
Whether a BDD represents a cube.
adiar::bdd_maxvar
bdd::label_type bdd_maxvar(const bdd &f)
Get the maximal occurring variable in the function's support.
adiar::operator~
bdd operator~(const bdd &f)
adiar::bdd_isconst
bool bdd_isconst(const bdd &f)
Whether a BDD is a constant.
adiar::bdd_support
void bdd_support(const bdd &f, const consumer< bdd::label_type > &cb)
Get (in ascending order) all of the variable labels that occur in the BDD.
adiar::bdd_or
bdd bdd_or(const generator< int > &vars)
The BDD representing the logical 'or' of all the given variables, i.e. a clause of variables.
adiar::bdd_exists
__bdd bdd_exists(const bdd &f, bdd::label_type var)
Existential quantification of a single variable.
adiar::operator==
bool operator==(const bdd &f, const bdd &g)
adiar::operator^
__bdd operator^(const bdd &lhs, const bdd &rhs)
adiar::bdd_eval
bool bdd_eval(const bdd &f, const predicate< bdd::label_type > &xs)
Evaluate a BDD according to an assignment to its variables.
adiar::bdd_equal
bool bdd_equal(const bdd &f, const bdd &g)
Whether the two BDDs represent the same function.
adiar::bdd_less
__bdd bdd_less(const bdd &f, const bdd &g)
Logical 'less than' operator.
adiar::bdd_pathcount
uint64_t bdd_pathcount(const bdd &f)
Count all unique (but not necessarily disjoint) paths to the true terminal.
adiar::bdd_replace
bdd bdd_replace(const bdd &f, const function< bdd::label_type(bdd::label_type)> &m)
Replace variables in f according to the mapping in m.
adiar::bdd_nand
__bdd bdd_nand(const bdd &f, const bdd &g)
Logical 'nand' operator.
adiar::bdd_isterminal
bool bdd_isterminal(const bdd &f)
Whether a BDD is a constant (terminal).
adiar::bdd_isnithvar
bool bdd_isnithvar(const bdd &f)
Whether a BDD is the function of a single negative variable.
adiar::bdd_and
bdd bdd_and(const generator< int > &vars)
The BDD representing the logical 'and' of all the given variables, i.e. a term of variables.
adiar::bdd_false
bdd bdd_false()
The BDD representing the constant false.
adiar::operator-
bdd operator-(const bdd &f)
adiar::bdd_forall
__bdd bdd_forall(const bdd &f, bdd::label_type var)
Forall quantification of a single variable.
adiar::bdd_restrict
__bdd bdd_restrict(const bdd &f, bdd::label_type var, bool val)
Restrict a single variable to a constant value.
adiar::bdd_minvar
bdd::label_type bdd_minvar(const bdd &f)
Get the minimal occurring variable in the function's support.
adiar::bdd_topvar
bdd::label_type bdd_topvar(const bdd &f)
Get the root's variable label.
adiar::generator
function< optional< RetType >()> generator
Generator function that produces a new value of RetType for each call.
Definition functional.h:170
adiar::cost
function< double(VarType)> cost
Cost function that assigns a cost to each variable.
Definition functional.h:156
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::function
std::function< TypeSignature > function
General-purpose polymorphic function wrapper.
Definition functional.h:41
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
Core types.
Definition adiar.h:40
adiar::pair
std::pair< T1, T2 > pair
A pair of values.
Definition types.h:53
adiar::replace_type
replace_type
Possible guarantees of a variable permutation/remapping m of type int -> int.
Definition types.h:32
adiar::optional
std::optional< T > optional
An optional value, i.e. a possibly existent value.
Definition types.h:81