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
1400 bdd
1401 bdd_replace(const bdd& f,
1402 const function<bdd::label_type(bdd::label_type)>& m,
1403 replace_type m_type = replace_type::Auto);
1404
1408 bdd
1409 bdd_replace(const exec_policy& ep,
1410 const bdd& f,
1411 const function<bdd::label_type(bdd::label_type)>& m,
1412 replace_type m_type = replace_type::Auto);
1413
1415
1432 bdd
1433 bdd_replace(__bdd&& f,
1434 const function<bdd::label_type(bdd::label_type)>& m,
1435 replace_type m_type = replace_type::Auto);
1436
1440 bdd
1441 bdd_replace(const exec_policy& ep,
1442 __bdd&& f,
1443 const function<bdd::label_type(bdd::label_type)>& m,
1444 replace_type m_type = replace_type::Auto);
1445
1447
1450
1455
1470 bdd
1471 bdd_relprod(const bdd& states, const bdd& relation, const predicate<bdd::label_type>& pred);
1472
1476 bdd
1477 bdd_relprod(const exec_policy& ep,
1478 const bdd& states,
1479 const bdd& relation,
1480 const predicate<bdd::label_type>& pred);
1481
1505 bdd
1506 bdd_relnext(const bdd& states,
1507 const bdd& relation,
1508 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1509 replace_type m_type = replace_type::Auto);
1510
1514 bdd
1515 bdd_relnext(const exec_policy& ep,
1516 const bdd& states,
1517 const bdd& relation,
1518 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1519 replace_type m_type = replace_type::Auto);
1520
1537 bdd
1538 bdd_relnext(const bdd& states, const bdd& relation, const bdd::label_type varcount);
1539
1544 bdd
1545 bdd_relnext(const exec_policy& ep,
1546 const bdd& states,
1547 const bdd& relation,
1548 const bdd::label_type varcount);
1549
1565 bdd
1566 bdd_relnext(const bdd& states, const bdd& relation);
1567
1572 bdd
1573 bdd_relnext(const exec_policy& ep, const bdd& states, const bdd& relation);
1574
1599 bdd
1600 bdd_relprev(const bdd& states,
1601 const bdd& relation,
1602 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1603 replace_type m_type = replace_type::Auto);
1604
1608 bdd
1609 bdd_relprev(const exec_policy& ep,
1610 const bdd& states,
1611 const bdd& relation,
1612 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1613 replace_type m_type = replace_type::Auto);
1614
1631 bdd
1632 bdd_relprev(const bdd& states, const bdd& relation, const bdd::label_type varcount);
1633
1638 bdd
1639 bdd_relprev(const exec_policy& ep,
1640 const bdd& states,
1641 const bdd& relation,
1642 const bdd::label_type varcount);
1643
1658 bdd
1659 bdd_relprev(const bdd& states, const bdd& relation);
1660
1665 bdd
1666 bdd_relprev(const exec_policy& ep, const bdd& states, const bdd& relation);
1667
1670
1675
1681 bool
1682 bdd_iscanonical(const bdd& f);
1683
1689 bool
1690 bdd_isconst(const bdd& f);
1691
1697 bool
1698 bdd_isterminal(const bdd& f);
1699
1703 bool
1704 bdd_isfalse(const bdd& f);
1705
1709 bool
1710 bdd_istrue(const bdd& f);
1711
1719 bool
1720 bdd_isvar(const bdd& f);
1721
1729 bool
1730 bdd_isithvar(const bdd& f);
1731
1739 bool
1740 bdd_isnithvar(const bdd& f);
1741
1747 bool
1748 bdd_iscube(const bdd& f);
1749
1757 bool
1758 bdd_equal(const bdd& f, const bdd& g);
1759
1763 bool
1764 bdd_equal(const exec_policy&, const bdd& f, const bdd& g);
1765
1769 bool
1770 operator==(const bdd& f, const bdd& g);
1771
1773 bool
1774 operator==(__bdd&& f, const bdd& g);
1775 bool
1776 operator==(const bdd& f, __bdd&& g);
1777 bool
1778 operator==(__bdd&& f, __bdd&& g);
1780
1790 bool
1791 bdd_unequal(const bdd& f, const bdd& g);
1792
1796 bool
1797 bdd_unequal(const exec_policy& ep, const bdd& f, const bdd& g);
1798
1802 bool
1803 operator!=(const bdd& f, const bdd& g);
1804
1806 bool
1807 operator!=(const bdd& f, __bdd&& g);
1808 bool
1809 operator!=(__bdd&& f, const bdd& g);
1810 bool
1811 operator!=(__bdd&& f, __bdd&& g);
1813
1816
1821
1825 size_t
1826 bdd_nodecount(const bdd& f);
1827
1832 bdd::label_type
1833 bdd_varcount(const bdd& f);
1834
1840 uint64_t
1841 bdd_pathcount(const bdd& f);
1842
1846 uint64_t
1847 bdd_pathcount(const exec_policy& ep, const bdd& f);
1848
1863 uint64_t
1864 bdd_satcount(const bdd& f, bdd::label_type varcount);
1865
1869 uint64_t
1870 bdd_satcount(const exec_policy& ep, const bdd& f, bdd::label_type varcount);
1871
1880 uint64_t
1881 bdd_satcount(const bdd& f);
1882
1886 uint64_t
1887 bdd_satcount(const exec_policy& ep, const bdd& f);
1888
1891
1896
1907 void
1908 bdd_support(const bdd& f, const consumer<bdd::label_type>& cb);
1909
1922 template <typename OutputIt,
1923 typename = enable_if<!is_convertible<OutputIt, consumer<bdd::label_type>>>>
1924 OutputIt
1925 bdd_support(const bdd& f, OutputIt iter)
1926 {
1927 bdd_support(f, make_consumer<bdd::label_type>(iter));
1928 return iter;
1929 }
1930
1936 bdd::label_type
1937 bdd_topvar(const bdd& f);
1938
1944 bdd::label_type
1945 bdd_minvar(const bdd& f);
1946
1952 bdd::label_type
1953 bdd_maxvar(const bdd& f);
1954
1964 bdd
1965 bdd_satmin(const bdd& f);
1966
1979 bdd
1980 bdd_satmin(const bdd& f,
1981 const generator<bdd::label_type>& d,
1982 const size_t d_size = bdd::max_label + 1);
1983
1999 template <typename ForwardIt, typename = enable_if<is_const<typename ForwardIt::reference>>>
2000 bdd
2001 bdd_satmin(const bdd& f, ForwardIt cbegin, ForwardIt cend)
2002 {
2003 return bdd_satmin(f, make_generator(cbegin, cend), std::distance(cbegin, cend));
2004 }
2005
2020 bdd
2021 bdd_satmin(const bdd& f, const bdd& d);
2022
2030 void
2031 bdd_satmin(const bdd& f, const consumer<pair<bdd::label_type, bool>>& c);
2032
2044 template <typename OutputIt,
2045 typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>>
2046 && !is_convertible<OutputIt, bdd>>>
2047 OutputIt
2053
2063 bdd
2064 bdd_satmax(const bdd& f);
2065
2077 bdd
2078 bdd_satmax(const bdd& f,
2079 const generator<bdd::label_type>& d,
2080 const size_t d_size = bdd::max_label + 1);
2081
2097 template <typename ForwardIt, typename = enable_if<is_const<typename ForwardIt::reference>>>
2098 bdd
2099 bdd_satmax(const bdd& f, ForwardIt cbegin, ForwardIt cend)
2100 {
2101 return bdd_satmax(f, make_generator(cbegin, cend), std::distance(cbegin, cend));
2102 }
2103
2118 bdd
2119 bdd_satmax(const bdd& f, const bdd& d);
2120
2128 void
2129 bdd_satmax(const bdd& f, const consumer<pair<bdd::label_type, bool>>& c);
2130
2142 template <typename OutputIt,
2143 typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>>
2144 && !is_convertible<OutputIt, bdd>>>
2145 OutputIt
2151
2165 pair<bdd, double>
2166 bdd_optmin(const bdd& f, const cost<bdd::label_type>& c);
2167
2172 pair<bdd, double>
2173 bdd_optmin(const exec_policy& ep, const bdd& f, const cost<bdd::label_type>& c);
2174
2192 double
2193 bdd_optmin(const bdd& f,
2194 const cost<bdd::label_type>& c,
2195 const consumer<pair<bdd::label_type, bool>>& cb);
2196
2201 double
2202 bdd_optmin(const exec_policy& ep,
2203 const bdd& f,
2204 const cost<bdd::label_type>& c,
2205 const consumer<pair<bdd::label_type, bool>>& cb);
2206
2219 bool
2220 bdd_eval(const bdd& f, const predicate<bdd::label_type>& xs);
2221
2237 bool
2238 bdd_eval(const bdd& f, const generator<pair<bdd::label_type, bool>>& xs);
2239
2258 template <typename ForwardIt>
2259 bool
2260 bdd_eval(const bdd& f, ForwardIt begin, ForwardIt end)
2261 {
2262 return bdd_eval(f, make_generator(begin, end));
2263 }
2264
2267
2272
2286 __bdd
2287 bdd_from(const zdd& A, const generator<bdd::label_type>& dom);
2288
2293 __bdd
2294 bdd_from(const exec_policy& ep, const zdd& A, const generator<bdd::label_type>& dom);
2295
2312 template <typename ForwardIt>
2313 __bdd
2314 bdd_from(const zdd& A, ForwardIt begin, ForwardIt end)
2315 {
2316 return bdd_from(A, make_generator(begin, end));
2317 }
2318
2323 template <typename ForwardIt>
2324 __bdd
2325 bdd_from(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
2326 {
2327 return bdd_from(ep, A, make_generator(begin, end));
2328 }
2329
2344 __bdd
2345 bdd_from(const zdd& A);
2346
2351 __bdd
2352 bdd_from(const exec_policy& ep, const zdd& A);
2353
2356
2361
2365 void
2366 bdd_printdot(const bdd& f, std::ostream& out = std::cout, bool include_id = false);
2367
2371 void
2372 bdd_printdot(const bdd& f, const std::string& file_name, bool include_id = false);
2373
2376}
2377
2378#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_relnext
bdd bdd_relnext(const bdd &states, const bdd &relation, const function< optional< bdd::label_type >(bdd::label_type)> &m, replace_type m_type=replace_type::Auto)
Forwards step with the Relational Product, including relabelling.
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_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_isfalse
bool bdd_isfalse(const bdd &f)
Whether a BDD is the constant false.
adiar::bdd_replace
bdd bdd_replace(const bdd &f, const function< bdd::label_type(bdd::label_type)> &m, replace_type m_type=replace_type::Auto)
Replace variables in f according to the mapping in m.
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_relprev
bdd bdd_relprev(const bdd &states, const bdd &relation, const function< optional< bdd::label_type >(bdd::label_type)> &m, replace_type m_type=replace_type::Auto)
Backwards step with the Relational Product, including relabelling.
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_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:75
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:103