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{
35
44 bdd
45 bdd_const(bool value);
46
55 bdd
56 bdd_terminal(bool value);
57
65 bdd
66 bdd_false();
67
75 inline bdd
76 bdd_bot()
77 {
78 return bdd_false();
79 }
80
86 bdd
87 bdd_true();
88
96 inline bdd
97 bdd_top()
98 {
99 return bdd_true();
100 }
101
113 bdd
114 bdd_ithvar(bdd::label_type var);
115
127 bdd
128 bdd_nithvar(bdd::label_type var);
129
145 bdd
146 bdd_and(const generator<int>& vars);
147
160 bdd
161 bdd_and(const generator<pair<bdd::label_type, bool>>& vars);
162
181 template <typename ForwardIt, typename = enable_if<!is_convertible<ForwardIt, bdd>>>
182 bdd
183 bdd_and(ForwardIt begin, ForwardIt end)
184 {
185 return bdd_and(make_generator(begin, end));
186 }
187
203 bdd
204 bdd_or(const generator<int>& vars);
205
218 bdd
219 bdd_or(const generator<pair<bdd::label_type, bool>>& vars);
220
239 template <typename ForwardIt, typename = enable_if<!is_convertible<ForwardIt, bdd>>>
240 bdd
241 bdd_or(ForwardIt begin, ForwardIt end)
242 {
243 return bdd_or(make_generator(begin, end));
244 }
245
262 bdd
263 bdd_cube(const generator<int>& vars);
264
278 bdd
279 bdd_cube(const generator<pair<bdd::label_type, bool>>& vars);
280
300 template <typename ForwardIt>
301 bdd
302 bdd_cube(ForwardIt begin, ForwardIt end)
303 {
304 return bdd_cube(make_generator(begin, end));
305 }
306
309
314
324 bdd
325 bdd_not(const bdd& f);
326
328 bdd
329 bdd_not(bdd&& f);
331
335 bdd
336 operator~(const bdd& f);
337
339 bdd
340 operator~(bdd&& f);
341 bdd
342 operator~(__bdd&& f);
344
361 __bdd
362 bdd_apply(const bdd& f, const bdd& g, const predicate<bool, bool>& op);
363
367 __bdd
368 bdd_apply(const exec_policy& ep, const bdd& f, const bdd& g, const predicate<bool, bool>& op);
369
377 __bdd
378 bdd_and(const bdd& f, const bdd& g);
379
383 __bdd
384 bdd_and(const exec_policy& ep, const bdd& f, const bdd& g);
385
389 __bdd
390 operator&(const bdd& lhs, const bdd& rhs);
391
393 __bdd
394 operator&(const bdd&, __bdd&&);
395 __bdd
396 operator&(__bdd&&, const bdd&);
397 __bdd
398 operator&(__bdd&&, __bdd&&);
400
404 __bdd
405 operator*(const bdd& lhs, const bdd& rhs);
406
408 __bdd
409 operator*(const bdd&, __bdd&&);
410 __bdd
411 operator*(__bdd&&, const bdd&);
412 __bdd
413 operator*(__bdd&&, __bdd&&);
415
423 __bdd
424 bdd_nand(const bdd& f, const bdd& g);
425
429 __bdd
430 bdd_nand(const exec_policy& ep, const bdd& f, const bdd& g);
431
439 __bdd
440 bdd_or(const bdd& f, const bdd& g);
441
445 __bdd
446 bdd_or(const exec_policy& ep, const bdd& f, const bdd& g);
447
451 __bdd
452 operator|(const bdd& lhs, const bdd& rhs);
453
455 __bdd
456 operator|(const bdd&, __bdd&&);
457 __bdd
458 operator|(__bdd&&, const bdd&);
459 __bdd
460 operator|(__bdd&&, __bdd&&);
462
466 bdd
467 operator+(const bdd& f);
468
473 __bdd
474 operator+(__bdd&& f);
476
480 __bdd
481 operator+(const bdd& lhs, const bdd& rhs);
482
484 __bdd
485 operator+(const bdd&, __bdd&&);
486 __bdd
487 operator+(__bdd&&, const bdd&);
488 __bdd
489 operator+(__bdd&&, __bdd&&);
491
499 __bdd
500 bdd_nor(const bdd& f, const bdd& g);
501
505 __bdd
506 bdd_nor(const exec_policy& ep, const bdd& f, const bdd& g);
507
515 __bdd
516 bdd_xor(const bdd& f, const bdd& g);
517
521 __bdd
522 bdd_xor(const exec_policy& ep, const bdd& f, const bdd& g);
523
527 __bdd
528 operator^(const bdd& lhs, const bdd& rhs);
529
531 __bdd
532 operator^(const bdd&, __bdd&&);
533 __bdd
534 operator^(__bdd&&, const bdd&);
535 __bdd
536 operator^(__bdd&&, __bdd&&);
538
546 __bdd
547 bdd_xnor(const bdd& f, const bdd& g);
548
552 __bdd
553 bdd_xnor(const exec_policy& ep, const bdd& f, const bdd& g);
554
562 __bdd
563 bdd_imp(const bdd& f, const bdd& g);
564
568 __bdd
569 bdd_imp(const exec_policy& ep, const bdd& f, const bdd& g);
570
578 __bdd
579 bdd_invimp(const bdd& f, const bdd& g);
580
584 __bdd
585 bdd_invimp(const exec_policy& ep, const bdd& f, const bdd& g);
586
594 __bdd
595 bdd_equiv(const bdd& f, const bdd& g);
596
600 __bdd
601 bdd_equiv(const exec_policy& ep, const bdd& f, const bdd& g);
602
610 __bdd
611 bdd_diff(const bdd& f, const bdd& g);
612
616 __bdd
617 bdd_diff(const exec_policy& ep, const bdd& f, const bdd& g);
618
624 bdd
625 operator-(const bdd& f);
626
628 __bdd
629 operator-(__bdd&& f);
631
635 __bdd
636 operator-(const bdd& lhs, const bdd& rhs);
637
639 __bdd
640 operator-(const bdd&, __bdd&&);
641 __bdd
642 operator-(__bdd&&, const bdd&);
643 __bdd
644 operator-(__bdd&&, __bdd&&);
646
654 __bdd
655 bdd_less(const bdd& f, const bdd& g);
656
660 __bdd
661 bdd_less(const exec_policy& ep, const bdd& f, const bdd& g);
662
686 __bdd
687 bdd_ite(const bdd& f, const bdd& g, const bdd& h);
688
692 __bdd
693 bdd_ite(const exec_policy& ep, const bdd& f, const bdd& g, const bdd& h);
694
711 __bdd
712 bdd_restrict(const bdd& f, bdd::label_type var, bool val);
713
717 __bdd
718 bdd_restrict(const exec_policy& ep, const bdd& f, bdd::label_type var, bool val);
719
735 __bdd
736 bdd_restrict(const bdd& f, const generator<pair<bdd::label_type, bool>>& xs);
737
741 __bdd
742 bdd_restrict(const exec_policy& ep,
743 const bdd& f,
744 const generator<pair<bdd::label_type, bool>>& xs);
745
764 template <typename ForwardIt>
765 __bdd
766 bdd_restrict(const bdd& f, ForwardIt begin, ForwardIt end)
767 {
768 return bdd_restrict(f, make_generator(begin, end));
769 }
770
774 template <typename ForwardIt>
775 __bdd
776 bdd_restrict(const exec_policy& ep, const bdd& f, ForwardIt begin, ForwardIt end)
777 {
778 return bdd_restrict(ep, f, make_generator(begin, end));
779 }
780
792 __bdd
793 bdd_low(const bdd& f);
794
798 __bdd
799 bdd_low(const exec_policy& ep, const bdd& f);
800
812 __bdd
813 bdd_high(const bdd& f);
814
818 __bdd
819 bdd_high(const exec_policy& ep, const bdd& f);
820
835 __bdd
836 bdd_exists(const bdd& f, bdd::label_type var);
837
839
843 inline __bdd
844 bdd_exists(bdd&& f, bdd::label_type var)
845 {
846 return bdd_exists(f, var);
847 }
848
850
854 __bdd
855 bdd_exists(const exec_policy& ep, const bdd& f, bdd::label_type var);
856
858
862 inline __bdd
863 bdd_exists(const exec_policy& ep, bdd&& f, bdd::label_type var)
864 {
865 return bdd_exists(ep, f, var);
866 }
867
869
883 __bdd
884 bdd_exists(const bdd& f, const predicate<bdd::label_type>& vars);
885
887
895 __bdd
896 bdd_exists(bdd&& f, const predicate<bdd::label_type>& vars);
897
904 __bdd
905 bdd_exists(__bdd&& f, const predicate<bdd::label_type>& vars);
906
908
912 __bdd
913 bdd_exists(const exec_policy& ep, const bdd& f, const predicate<bdd::label_type>& vars);
914
916
924 __bdd
925 bdd_exists(const exec_policy& ep, bdd&& f, const predicate<bdd::label_type>& vars);
926
933 __bdd
934 bdd_exists(const exec_policy& ep, __bdd&& f, const predicate<bdd::label_type>& vars);
935
937
950 __bdd
951 bdd_exists(const bdd& f, const generator<bdd::label_type>& vars);
952
954
962 __bdd
963 bdd_exists(bdd&& f, const generator<bdd::label_type>& vars);
964
971 __bdd
972 bdd_exists(__bdd&& f, const generator<bdd::label_type>& vars);
973
975
979 __bdd
980 bdd_exists(const exec_policy& ep, const bdd& f, const generator<bdd::label_type>& vars);
981
983
991 __bdd
992 bdd_exists(const exec_policy& ep, bdd&& f, const generator<bdd::label_type>& vars);
993
1000 __bdd
1001 bdd_exists(const exec_policy& ep, __bdd&& f, const generator<bdd::label_type>& vars);
1002
1004
1020 template <typename ForwardIt>
1021 __bdd
1022 bdd_exists(const bdd& f, ForwardIt begin, ForwardIt end)
1023 {
1024 return bdd_exists(f, make_generator(begin, end));
1025 }
1026
1028
1036 template <typename ForwardIt>
1037 __bdd
1038 bdd_exists(bdd&& f, ForwardIt begin, ForwardIt end)
1039 {
1040 return bdd_exists(std::move(f), make_generator(begin, end));
1041 }
1042
1049 template <typename ForwardIt>
1050 __bdd
1051 bdd_exists(__bdd&& f, ForwardIt begin, ForwardIt end)
1052 {
1053 return bdd_exists(std::move(f), make_generator(begin, end));
1054 }
1055
1057
1061 template <typename ForwardIt>
1062 __bdd
1063 bdd_exists(const exec_policy& ep, const bdd& f, ForwardIt begin, ForwardIt end)
1064 {
1065 return bdd_exists(ep, f, make_generator(begin, end));
1066 }
1067
1069
1077 template <typename ForwardIt>
1078 __bdd
1079 bdd_exists(const exec_policy& ep, bdd&& f, ForwardIt begin, ForwardIt end)
1080 {
1081 return bdd_exists(ep, std::move(f), make_generator(begin, end));
1082 }
1083
1090 template <typename ForwardIt>
1091 __bdd
1092 bdd_exists(const exec_policy& ep, __bdd&& f, ForwardIt begin, ForwardIt end)
1093 {
1094 return bdd_exists(ep, std::move(f), make_generator(begin, end));
1095 }
1096
1098
1113 __bdd
1114 bdd_forall(const bdd& f, bdd::label_type var);
1115
1117
1121 inline __bdd
1122 bdd_forall(bdd&& f, bdd::label_type var)
1123 {
1124 return bdd_forall(f, var);
1125 }
1126
1128
1132 __bdd
1133 bdd_forall(const exec_policy& ep, const bdd& f, bdd::label_type var);
1134
1136
1140 inline __bdd
1141 bdd_forall(const exec_policy& ep, bdd&& f, bdd::label_type var)
1142 {
1143 return bdd_forall(ep, f, var);
1144 }
1145
1147
1161 __bdd
1162 bdd_forall(const bdd& f, const predicate<bdd::label_type>& vars);
1163
1165
1173 __bdd
1174 bdd_forall(bdd&& f, const predicate<bdd::label_type>& vars);
1175
1182 __bdd
1183 bdd_forall(__bdd&& f, const predicate<bdd::label_type>& vars);
1184
1186
1190 __bdd
1191 bdd_forall(const exec_policy& ep, const bdd& f, const predicate<bdd::label_type>& vars);
1192
1194
1202 __bdd
1203 bdd_forall(const exec_policy& ep, bdd&& f, const predicate<bdd::label_type>& vars);
1204
1211 __bdd
1212 bdd_forall(const exec_policy& ep, __bdd&& f, const predicate<bdd::label_type>& vars);
1213
1215
1228 __bdd
1229 bdd_forall(const bdd& f, const generator<bdd::label_type>& vars);
1230
1232
1240 __bdd
1241 bdd_forall(bdd&& f, const generator<bdd::label_type>& vars);
1242
1249 __bdd
1250 bdd_forall(bdd&& f, const generator<bdd::label_type>& vars);
1251
1253
1257 __bdd
1258 bdd_forall(const exec_policy& ep, const bdd& f, const generator<bdd::label_type>& vars);
1259
1261
1269 __bdd
1270 bdd_forall(const exec_policy& ep, bdd&& f, const generator<bdd::label_type>& vars);
1271
1278 __bdd
1279 bdd_forall(const exec_policy& ep, __bdd&& f, const generator<bdd::label_type>& vars);
1280
1282
1298 template <typename ForwardIt>
1299 __bdd
1300 bdd_forall(const bdd& f, ForwardIt begin, ForwardIt end)
1301 {
1302 return bdd_forall(f, make_generator(begin, end));
1303 }
1304
1306
1314 template <typename ForwardIt>
1315 __bdd
1316 bdd_forall(bdd&& f, ForwardIt begin, ForwardIt end)
1317 {
1318 return bdd_forall(std::move(f), make_generator(begin, end));
1319 }
1320
1327 template <typename ForwardIt>
1328 __bdd
1329 bdd_forall(__bdd&& f, ForwardIt begin, ForwardIt end)
1330 {
1331 return bdd_forall(std::move(f), make_generator(begin, end));
1332 }
1333
1335
1339 template <typename ForwardIt>
1340 __bdd
1341 bdd_forall(const exec_policy& ep, const bdd& f, ForwardIt begin, ForwardIt end)
1342 {
1343 return bdd_forall(ep, f, make_generator(begin, end));
1344 }
1345
1347
1355 template <typename ForwardIt>
1356 __bdd
1357 bdd_forall(const exec_policy& ep, bdd&& f, ForwardIt begin, ForwardIt end)
1358 {
1359 return bdd_forall(ep, std::move(f), make_generator(begin, end));
1360 }
1361
1368 template <typename ForwardIt>
1369 __bdd
1370 bdd_forall(const exec_policy& ep, __bdd&& f, ForwardIt begin, ForwardIt end)
1371 {
1372 return bdd_forall(ep, std::move(f), make_generator(begin, end));
1373 }
1374
1376
1379
1384
1396 bdd
1397 bdd_replace(const bdd& f, const function<bdd::label_type(bdd::label_type)>& m);
1398
1402 bdd
1403 bdd_replace(const exec_policy& ep,
1404 const bdd& f,
1405 const function<bdd::label_type(bdd::label_type)>& m);
1406
1421 bdd
1422 bdd_replace(const bdd& f,
1423 const function<bdd::label_type(bdd::label_type)>& m,
1424 replace_type m_type);
1425
1429 bdd
1430 bdd_replace(const exec_policy& ep,
1431 const bdd& f,
1432 const function<bdd::label_type(bdd::label_type)>& m,
1433 replace_type m_type);
1434
1436
1451 bdd
1452 bdd_replace(__bdd&& f, const function<bdd::label_type(bdd::label_type)>& m);
1453
1457 bdd
1458 bdd_replace(const exec_policy& ep,
1459 __bdd&& f,
1460 const function<bdd::label_type(bdd::label_type)>& m);
1461
1477 bdd
1478 bdd_replace(__bdd&& f, const function<bdd::label_type(bdd::label_type)>& m, replace_type m_type);
1479
1483 bdd
1484 bdd_replace(const exec_policy& ep,
1485 __bdd&& f,
1486 const function<bdd::label_type(bdd::label_type)>& m,
1487 replace_type m_type);
1488
1490
1493
1498
1513 bdd
1514 bdd_relprod(const bdd& states, const bdd& relation, const predicate<bdd::label_type>& pred);
1515
1519 bdd
1520 bdd_relprod(const exec_policy& ep,
1521 const bdd& states,
1522 const bdd& relation,
1523 const predicate<bdd::label_type>& pred);
1524
1544 bdd
1545 bdd_relnext(const bdd& states,
1546 const bdd& relation,
1547 const function<optional<bdd::label_type>(bdd::label_type)>& m);
1548
1552 bdd
1553 bdd_relnext(const exec_policy& ep,
1554 const bdd& states,
1555 const bdd& relation,
1556 const function<optional<bdd::label_type>(bdd::label_type)>& m);
1557
1580 bdd
1581 bdd_relnext(const bdd& states,
1582 const bdd& relation,
1583 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1584 replace_type m_type);
1585
1589 bdd
1590 bdd_relnext(const exec_policy& ep,
1591 const bdd& states,
1592 const bdd& relation,
1593 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1594 replace_type m_type);
1595
1612 bdd
1613 bdd_relnext(const bdd& states, const bdd& relation, const bdd::label_type varcount);
1614
1619 bdd
1620 bdd_relnext(const exec_policy& ep,
1621 const bdd& states,
1622 const bdd& relation,
1623 const bdd::label_type varcount);
1624
1640 bdd
1641 bdd_relnext(const bdd& states, const bdd& relation);
1642
1647 bdd
1648 bdd_relnext(const exec_policy& ep, const bdd& states, const bdd& relation);
1649
1670 bdd
1671 bdd_relprev(const bdd& states,
1672 const bdd& relation,
1673 const function<optional<bdd::label_type>(bdd::label_type)>& m);
1674
1678 bdd
1679 bdd_relprev(const exec_policy& ep,
1680 const bdd& states,
1681 const bdd& relation,
1682 const function<optional<bdd::label_type>(bdd::label_type)>& m);
1683
1707 bdd
1708 bdd_relprev(const bdd& states,
1709 const bdd& relation,
1710 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1711 replace_type m_type);
1712
1716 bdd
1717 bdd_relprev(const exec_policy& ep,
1718 const bdd& states,
1719 const bdd& relation,
1720 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1721 replace_type m_type);
1722
1739 bdd
1740 bdd_relprev(const bdd& states, const bdd& relation, const bdd::label_type varcount);
1741
1746 bdd
1747 bdd_relprev(const exec_policy& ep,
1748 const bdd& states,
1749 const bdd& relation,
1750 const bdd::label_type varcount);
1751
1766 bdd
1767 bdd_relprev(const bdd& states, const bdd& relation);
1768
1773 bdd
1774 bdd_relprev(const exec_policy& ep, const bdd& states, const bdd& relation);
1775
1778
1783
1789 bool
1790 bdd_iscanonical(const bdd& f);
1791
1797 bool
1798 bdd_isconst(const bdd& f);
1799
1805 bool
1806 bdd_isterminal(const bdd& f);
1807
1811 bool
1812 bdd_isfalse(const bdd& f);
1813
1817 bool
1818 bdd_istrue(const bdd& f);
1819
1827 bool
1828 bdd_isvar(const bdd& f);
1829
1837 bool
1838 bdd_isithvar(const bdd& f);
1839
1847 bool
1848 bdd_isnithvar(const bdd& f);
1849
1855 bool
1856 bdd_iscube(const bdd& f);
1857
1865 bool
1866 bdd_equal(const bdd& f, const bdd& g);
1867
1871 bool
1872 bdd_equal(const exec_policy&, const bdd& f, const bdd& g);
1873
1877 bool
1878 operator==(const bdd& f, const bdd& g);
1879
1881 bool
1882 operator==(__bdd&& f, const bdd& g);
1883 bool
1884 operator==(const bdd& f, __bdd&& g);
1885 bool
1886 operator==(__bdd&& f, __bdd&& g);
1888
1898 bool
1899 bdd_unequal(const bdd& f, const bdd& g);
1900
1904 bool
1905 bdd_unequal(const exec_policy& ep, const bdd& f, const bdd& g);
1906
1910 bool
1911 operator!=(const bdd& f, const bdd& g);
1912
1914 bool
1915 operator!=(const bdd& f, __bdd&& g);
1916 bool
1917 operator!=(__bdd&& f, const bdd& g);
1918 bool
1919 operator!=(__bdd&& f, __bdd&& g);
1921
1924
1929
1933 size_t
1934 bdd_nodecount(const bdd& f);
1935
1940 bdd::label_type
1941 bdd_varcount(const bdd& f);
1942
1948 uint64_t
1949 bdd_pathcount(const bdd& f);
1950
1954 uint64_t
1955 bdd_pathcount(const exec_policy& ep, const bdd& f);
1956
1971 uint64_t
1972 bdd_satcount(const bdd& f, bdd::label_type varcount);
1973
1977 uint64_t
1978 bdd_satcount(const exec_policy& ep, const bdd& f, bdd::label_type varcount);
1979
1988 uint64_t
1989 bdd_satcount(const bdd& f);
1990
1994 uint64_t
1995 bdd_satcount(const exec_policy& ep, const bdd& f);
1996
1999
2004
2015 void
2016 bdd_support(const bdd& f, const consumer<bdd::label_type>& cb);
2017
2030 template <typename OutputIt,
2031 typename = enable_if<!is_convertible<OutputIt, consumer<bdd::label_type>>>>
2032 OutputIt
2033 bdd_support(const bdd& f, OutputIt iter)
2034 {
2035 bdd_support(f, make_consumer<bdd::label_type>(iter));
2036 return iter;
2037 }
2038
2044 bdd::label_type
2045 bdd_topvar(const bdd& f);
2046
2052 bdd::label_type
2053 bdd_minvar(const bdd& f);
2054
2060 bdd::label_type
2061 bdd_maxvar(const bdd& f);
2062
2072 bdd
2073 bdd_satmin(const bdd& f);
2074
2087 bdd
2088 bdd_satmin(const bdd& f,
2089 const generator<bdd::label_type>& d,
2090 const size_t d_size = bdd::max_label + 1);
2091
2107 template <typename ForwardIt, typename = enable_if<is_const<typename ForwardIt::reference>>>
2108 bdd
2109 bdd_satmin(const bdd& f, ForwardIt cbegin, ForwardIt cend)
2110 {
2111 return bdd_satmin(f, make_generator(cbegin, cend), std::distance(cbegin, cend));
2112 }
2113
2128 bdd
2129 bdd_satmin(const bdd& f, const bdd& d);
2130
2138 void
2139 bdd_satmin(const bdd& f, const consumer<pair<bdd::label_type, bool>>& c);
2140
2152 template <typename OutputIt,
2153 typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>>
2154 && !is_convertible<OutputIt, bdd>>>
2155 OutputIt
2161
2171 bdd
2172 bdd_satmax(const bdd& f);
2173
2185 bdd
2186 bdd_satmax(const bdd& f,
2187 const generator<bdd::label_type>& d,
2188 const size_t d_size = bdd::max_label + 1);
2189
2205 template <typename ForwardIt, typename = enable_if<is_const<typename ForwardIt::reference>>>
2206 bdd
2207 bdd_satmax(const bdd& f, ForwardIt cbegin, ForwardIt cend)
2208 {
2209 return bdd_satmax(f, make_generator(cbegin, cend), std::distance(cbegin, cend));
2210 }
2211
2226 bdd
2227 bdd_satmax(const bdd& f, const bdd& d);
2228
2236 void
2237 bdd_satmax(const bdd& f, const consumer<pair<bdd::label_type, bool>>& c);
2238
2250 template <typename OutputIt,
2251 typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>>
2252 && !is_convertible<OutputIt, bdd>>>
2253 OutputIt
2259
2273 pair<bdd, double>
2274 bdd_optmin(const bdd& f, const cost<bdd::label_type>& c);
2275
2280 pair<bdd, double>
2281 bdd_optmin(const exec_policy& ep, const bdd& f, const cost<bdd::label_type>& c);
2282
2300 double
2301 bdd_optmin(const bdd& f,
2302 const cost<bdd::label_type>& c,
2303 const consumer<pair<bdd::label_type, bool>>& cb);
2304
2309 double
2310 bdd_optmin(const exec_policy& ep,
2311 const bdd& f,
2312 const cost<bdd::label_type>& c,
2313 const consumer<pair<bdd::label_type, bool>>& cb);
2314
2327 bool
2328 bdd_eval(const bdd& f, const predicate<bdd::label_type>& xs);
2329
2345 bool
2346 bdd_eval(const bdd& f, const generator<pair<bdd::label_type, bool>>& xs);
2347
2366 template <typename ForwardIt>
2367 bool
2368 bdd_eval(const bdd& f, ForwardIt begin, ForwardIt end)
2369 {
2370 return bdd_eval(f, make_generator(begin, end));
2371 }
2372
2375
2380
2394 __bdd
2395 bdd_from(const zdd& A, const generator<bdd::label_type>& dom);
2396
2401 __bdd
2402 bdd_from(const exec_policy& ep, const zdd& A, const generator<bdd::label_type>& dom);
2403
2420 template <typename ForwardIt>
2421 __bdd
2422 bdd_from(const zdd& A, ForwardIt begin, ForwardIt end)
2423 {
2424 return bdd_from(A, make_generator(begin, end));
2425 }
2426
2431 template <typename ForwardIt>
2432 __bdd
2433 bdd_from(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
2434 {
2435 return bdd_from(ep, A, make_generator(begin, end));
2436 }
2437
2452 __bdd
2453 bdd_from(const zdd& A);
2454
2459 __bdd
2460 bdd_from(const exec_policy& ep, const zdd& A);
2461
2464
2469
2473 void
2474 bdd_printdot(const bdd& f, std::ostream& out = std::cout, bool include_id = false);
2475
2479 void
2480 bdd_printdot(const bdd& f, const std::string& file_name, bool include_id = false);
2481
2484}
2485
2486#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:302
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::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:97
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:76
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