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
68 bdd
69 bdd_false();
70
78 inline bdd
79 bdd_bot()
80 {
81 return bdd_false();
82 }
83
89 bdd
90 bdd_true();
91
99 inline bdd
100 bdd_top()
101 {
102 return bdd_true();
103 }
104
116 bdd
117 bdd_ithvar(bdd::label_type var);
118
130 bdd
131 bdd_nithvar(bdd::label_type var);
132
148 bdd
149 bdd_and(const generator<int>& vars);
150
163 bdd
164 bdd_and(const generator<pair<bdd::label_type, bool>>& vars);
165
184 template <typename ForwardIt, typename = enable_if<!is_convertible<ForwardIt, bdd>>>
185 bdd
186 bdd_and(ForwardIt begin, ForwardIt end)
187 {
188 return bdd_and(make_generator(begin, end));
189 }
190
206 bdd
207 bdd_or(const generator<int>& vars);
208
221 bdd
222 bdd_or(const generator<pair<bdd::label_type, bool>>& vars);
223
242 template <typename ForwardIt, typename = enable_if<!is_convertible<ForwardIt, bdd>>>
243 bdd
244 bdd_or(ForwardIt begin, ForwardIt end)
245 {
246 return bdd_or(make_generator(begin, end));
247 }
248
265 bdd
266 bdd_cube(const generator<int>& vars);
267
281 bdd
282 bdd_cube(const generator<pair<bdd::label_type, bool>>& vars);
283
303 template <typename ForwardIt>
304 bdd
305 bdd_cube(ForwardIt begin, ForwardIt end)
306 {
307 return bdd_cube(make_generator(begin, end));
308 }
309
312
317
327 bdd
328 bdd_not(const bdd& f);
329
331 bdd
332 bdd_not(bdd&& f);
334
338 bdd
339 operator~(const bdd& f);
340
342 bdd
343 operator~(bdd&& f);
344 bdd
345 operator~(__bdd&& f);
347
364 __bdd
365 bdd_apply(const bdd& f, const bdd& g, const predicate<bool, bool>& op);
366
370 __bdd
371 bdd_apply(const exec_policy& ep, const bdd& f, const bdd& g, const predicate<bool, bool>& op);
372
380 __bdd
381 bdd_and(const bdd& f, const bdd& g);
382
386 __bdd
387 bdd_and(const exec_policy& ep, const bdd& f, const bdd& g);
388
392 __bdd
393 operator&(const bdd& lhs, const bdd& rhs);
394
396 __bdd
397 operator&(const bdd&, __bdd&&);
398 __bdd
399 operator&(__bdd&&, const bdd&);
400 __bdd
401 operator&(__bdd&&, __bdd&&);
403
407 __bdd
408 operator*(const bdd& lhs, const bdd& rhs);
409
411 __bdd
412 operator*(const bdd&, __bdd&&);
413 __bdd
414 operator*(__bdd&&, const bdd&);
415 __bdd
416 operator*(__bdd&&, __bdd&&);
418
426 __bdd
427 bdd_nand(const bdd& f, const bdd& g);
428
432 __bdd
433 bdd_nand(const exec_policy& ep, const bdd& f, const bdd& g);
434
442 __bdd
443 bdd_or(const bdd& f, const bdd& g);
444
448 __bdd
449 bdd_or(const exec_policy& ep, const bdd& f, const bdd& g);
450
454 __bdd
455 operator|(const bdd& lhs, const bdd& rhs);
456
458 __bdd
459 operator|(const bdd&, __bdd&&);
460 __bdd
461 operator|(__bdd&&, const bdd&);
462 __bdd
463 operator|(__bdd&&, __bdd&&);
465
469 bdd
470 operator+(const bdd& f);
471
476 __bdd
477 operator+(__bdd&& f);
479
483 __bdd
484 operator+(const bdd& lhs, const bdd& rhs);
485
487 __bdd
488 operator+(const bdd&, __bdd&&);
489 __bdd
490 operator+(__bdd&&, const bdd&);
491 __bdd
492 operator+(__bdd&&, __bdd&&);
494
502 __bdd
503 bdd_nor(const bdd& f, const bdd& g);
504
508 __bdd
509 bdd_nor(const exec_policy& ep, const bdd& f, const bdd& g);
510
518 __bdd
519 bdd_xor(const bdd& f, const bdd& g);
520
524 __bdd
525 bdd_xor(const exec_policy& ep, const bdd& f, const bdd& g);
526
530 __bdd
531 operator^(const bdd& lhs, const bdd& rhs);
532
534 __bdd
535 operator^(const bdd&, __bdd&&);
536 __bdd
537 operator^(__bdd&&, const bdd&);
538 __bdd
539 operator^(__bdd&&, __bdd&&);
541
549 __bdd
550 bdd_xnor(const bdd& f, const bdd& g);
551
555 __bdd
556 bdd_xnor(const exec_policy& ep, const bdd& f, const bdd& g);
557
565 __bdd
566 bdd_imp(const bdd& f, const bdd& g);
567
571 __bdd
572 bdd_imp(const exec_policy& ep, const bdd& f, const bdd& g);
573
581 __bdd
582 bdd_invimp(const bdd& f, const bdd& g);
583
587 __bdd
588 bdd_invimp(const exec_policy& ep, const bdd& f, const bdd& g);
589
597 __bdd
598 bdd_equiv(const bdd& f, const bdd& g);
599
603 __bdd
604 bdd_equiv(const exec_policy& ep, const bdd& f, const bdd& g);
605
613 __bdd
614 bdd_diff(const bdd& f, const bdd& g);
615
619 __bdd
620 bdd_diff(const exec_policy& ep, const bdd& f, const bdd& g);
621
625 bdd
626 operator-(const bdd& f);
627
629 __bdd
630 operator-(__bdd&& f);
632
636 __bdd
637 operator-(const bdd& lhs, const bdd& rhs);
638
640 __bdd
641 operator-(const bdd&, __bdd&&);
642 __bdd
643 operator-(__bdd&&, const bdd&);
644 __bdd
645 operator-(__bdd&&, __bdd&&);
647
655 __bdd
656 bdd_less(const bdd& f, const bdd& g);
657
661 __bdd
662 bdd_less(const exec_policy& ep, const bdd& f, const bdd& g);
663
687 __bdd
688 bdd_ite(const bdd& f, const bdd& g, const bdd& h);
689
693 __bdd
694 bdd_ite(const exec_policy& ep, const bdd& f, const bdd& g, const bdd& h);
695
712 __bdd
713 bdd_restrict(const bdd& f, bdd::label_type var, bool val);
714
718 __bdd
719 bdd_restrict(const exec_policy& ep, const bdd& f, bdd::label_type var, bool val);
720
736 __bdd
737 bdd_restrict(const bdd& f, const generator<pair<bdd::label_type, bool>>& xs);
738
742 __bdd
743 bdd_restrict(const exec_policy& ep,
744 const bdd& f,
745 const generator<pair<bdd::label_type, bool>>& xs);
746
765 template <typename ForwardIt>
766 __bdd
767 bdd_restrict(const bdd& f, ForwardIt begin, ForwardIt end)
768 {
769 return bdd_restrict(f, make_generator(begin, end));
770 }
771
775 template <typename ForwardIt>
776 __bdd
777 bdd_restrict(const exec_policy& ep, const bdd& f, ForwardIt begin, ForwardIt end)
778 {
779 return bdd_restrict(ep, f, make_generator(begin, end));
780 }
781
792 __bdd
793 bdd_low(const bdd& f);
794
798 __bdd
799 bdd_low(const exec_policy& ep, const bdd& f);
800
811 __bdd
812 bdd_high(const bdd& f);
813
817 __bdd
818 bdd_high(const exec_policy& ep, const bdd& f);
819
834 __bdd
835 bdd_exists(const bdd& f, bdd::label_type var);
836
838
842 inline __bdd
843 bdd_exists(bdd&& f, bdd::label_type var)
844 {
845 return bdd_exists(f, var);
846 }
847
849
853 __bdd
854 bdd_exists(const exec_policy& ep, const bdd& f, bdd::label_type var);
855
857
861 inline __bdd
862 bdd_exists(const exec_policy& ep, bdd&& f, bdd::label_type var)
863 {
864 return bdd_exists(ep, f, var);
865 }
866
868
882 __bdd
883 bdd_exists(const bdd& f, const predicate<bdd::label_type>& vars);
884
886
894 __bdd
895 bdd_exists(bdd&& f, const predicate<bdd::label_type>& vars);
896
903 __bdd
904 bdd_exists(__bdd&& f, const predicate<bdd::label_type>& vars);
905
907
911 __bdd
912 bdd_exists(const exec_policy& ep, const bdd& f, const predicate<bdd::label_type>& vars);
913
915
923 __bdd
924 bdd_exists(const exec_policy& ep, bdd&& f, const predicate<bdd::label_type>& vars);
925
932 __bdd
933 bdd_exists(const exec_policy& ep, __bdd&& f, const predicate<bdd::label_type>& vars);
934
936
949 __bdd
950 bdd_exists(const bdd& f, const generator<bdd::label_type>& vars);
951
953
961 __bdd
962 bdd_exists(bdd&& f, const generator<bdd::label_type>& vars);
963
970 __bdd
971 bdd_exists(__bdd&& f, const generator<bdd::label_type>& vars);
972
974
978 __bdd
979 bdd_exists(const exec_policy& ep, const bdd& f, const generator<bdd::label_type>& vars);
980
982
990 __bdd
991 bdd_exists(const exec_policy& ep, bdd&& f, const generator<bdd::label_type>& vars);
992
999 __bdd
1000 bdd_exists(const exec_policy& ep, __bdd&& f, const generator<bdd::label_type>& vars);
1001
1003
1019 template <typename ForwardIt>
1020 __bdd
1021 bdd_exists(const bdd& f, ForwardIt begin, ForwardIt end)
1022 {
1023 return bdd_exists(f, make_generator(begin, end));
1024 }
1025
1027
1035 template <typename ForwardIt>
1036 __bdd
1037 bdd_exists(bdd&& f, ForwardIt begin, ForwardIt end)
1038 {
1039 return bdd_exists(std::move(f), make_generator(begin, end));
1040 }
1041
1048 template <typename ForwardIt>
1049 __bdd
1050 bdd_exists(__bdd&& f, ForwardIt begin, ForwardIt end)
1051 {
1052 return bdd_exists(std::move(f), make_generator(begin, end));
1053 }
1054
1056
1060 template <typename ForwardIt>
1061 __bdd
1062 bdd_exists(const exec_policy& ep, const bdd& f, ForwardIt begin, ForwardIt end)
1063 {
1064 return bdd_exists(ep, f, make_generator(begin, end));
1065 }
1066
1068
1076 template <typename ForwardIt>
1077 __bdd
1078 bdd_exists(const exec_policy& ep, bdd&& f, ForwardIt begin, ForwardIt end)
1079 {
1080 return bdd_exists(ep, std::move(f), make_generator(begin, end));
1081 }
1082
1089 template <typename ForwardIt>
1090 __bdd
1091 bdd_exists(const exec_policy& ep, __bdd&& f, ForwardIt begin, ForwardIt end)
1092 {
1093 return bdd_exists(ep, std::move(f), make_generator(begin, end));
1094 }
1095
1097
1112 __bdd
1113 bdd_forall(const bdd& f, bdd::label_type var);
1114
1116
1120 inline __bdd
1121 bdd_forall(bdd&& f, bdd::label_type var)
1122 {
1123 return bdd_forall(f, var);
1124 }
1125
1127
1131 __bdd
1132 bdd_forall(const exec_policy& ep, const bdd& f, bdd::label_type var);
1133
1135
1139 inline __bdd
1140 bdd_forall(const exec_policy& ep, bdd&& f, bdd::label_type var)
1141 {
1142 return bdd_forall(ep, f, var);
1143 }
1144
1146
1160 __bdd
1161 bdd_forall(const bdd& f, const predicate<bdd::label_type>& vars);
1162
1164
1172 __bdd
1173 bdd_forall(bdd&& f, const predicate<bdd::label_type>& vars);
1174
1181 __bdd
1182 bdd_forall(__bdd&& f, const predicate<bdd::label_type>& vars);
1183
1185
1189 __bdd
1190 bdd_forall(const exec_policy& ep, const bdd& f, const predicate<bdd::label_type>& vars);
1191
1193
1201 __bdd
1202 bdd_forall(const exec_policy& ep, bdd&& f, const predicate<bdd::label_type>& vars);
1203
1210 __bdd
1211 bdd_forall(const exec_policy& ep, __bdd&& f, const predicate<bdd::label_type>& vars);
1212
1214
1227 __bdd
1228 bdd_forall(const bdd& f, const generator<bdd::label_type>& vars);
1229
1231
1239 __bdd
1240 bdd_forall(bdd&& f, const generator<bdd::label_type>& vars);
1241
1248 __bdd
1249 bdd_forall(bdd&& f, const generator<bdd::label_type>& vars);
1250
1252
1256 __bdd
1257 bdd_forall(const exec_policy& ep, const bdd& f, const generator<bdd::label_type>& vars);
1258
1260
1268 __bdd
1269 bdd_forall(const exec_policy& ep, bdd&& f, const generator<bdd::label_type>& vars);
1270
1277 __bdd
1278 bdd_forall(const exec_policy& ep, __bdd&& f, const generator<bdd::label_type>& vars);
1279
1281
1297 template <typename ForwardIt>
1298 __bdd
1299 bdd_forall(const bdd& f, ForwardIt begin, ForwardIt end)
1300 {
1301 return bdd_forall(f, make_generator(begin, end));
1302 }
1303
1305
1313 template <typename ForwardIt>
1314 __bdd
1315 bdd_forall(bdd&& f, ForwardIt begin, ForwardIt end)
1316 {
1317 return bdd_forall(std::move(f), make_generator(begin, end));
1318 }
1319
1326 template <typename ForwardIt>
1327 __bdd
1328 bdd_forall(__bdd&& f, ForwardIt begin, ForwardIt end)
1329 {
1330 return bdd_forall(std::move(f), make_generator(begin, end));
1331 }
1332
1334
1338 template <typename ForwardIt>
1339 __bdd
1340 bdd_forall(const exec_policy& ep, const bdd& f, ForwardIt begin, ForwardIt end)
1341 {
1342 return bdd_forall(ep, f, make_generator(begin, end));
1343 }
1344
1346
1354 template <typename ForwardIt>
1355 __bdd
1356 bdd_forall(const exec_policy& ep, bdd&& f, ForwardIt begin, ForwardIt end)
1357 {
1358 return bdd_forall(ep, std::move(f), make_generator(begin, end));
1359 }
1360
1367 template <typename ForwardIt>
1368 __bdd
1369 bdd_forall(const exec_policy& ep, __bdd&& f, ForwardIt begin, ForwardIt end)
1370 {
1371 return bdd_forall(ep, std::move(f), make_generator(begin, end));
1372 }
1373
1375
1388 bdd
1389 bdd_relprod(const bdd& states, const bdd& relation, const predicate<bdd::label_type>& pred);
1390
1394 bdd
1395 bdd_relprod(const exec_policy& ep,
1396 const bdd& states,
1397 const bdd& relation,
1398 const predicate<bdd::label_type>& pred);
1399
1413 bdd
1414 bdd_relnext(const bdd& states,
1415 const bdd& relation,
1416 const function<optional<bdd::label_type>(bdd::label_type)>& m);
1417
1421 bdd
1422 bdd_relnext(const exec_policy& ep,
1423 const bdd& states,
1424 const bdd& relation,
1425 const function<optional<bdd::label_type>(bdd::label_type)>& m);
1426
1443 bdd
1444 bdd_relnext(const bdd& states,
1445 const bdd& relation,
1446 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1447 replace_type m_type);
1448
1452 bdd
1453 bdd_relnext(const exec_policy& ep,
1454 const bdd& states,
1455 const bdd& relation,
1456 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1457 replace_type m_type);
1458
1471 bdd
1472 bdd_relnext(const bdd& states, const bdd& relation, const bdd::label_type varcount);
1473
1478 bdd
1479 bdd_relnext(const exec_policy& ep,
1480 const bdd& states,
1481 const bdd& relation,
1482 const bdd::label_type varcount);
1483
1495 bdd
1496 bdd_relnext(const bdd& states, const bdd& relation);
1497
1502 bdd
1503 bdd_relnext(const exec_policy& ep, const bdd& states, const bdd& relation);
1504
1519 bdd
1520 bdd_relprev(const bdd& states,
1521 const bdd& relation,
1522 const function<optional<bdd::label_type>(bdd::label_type)>& m);
1523
1527 bdd
1528 bdd_relprev(const exec_policy& ep,
1529 const bdd& states,
1530 const bdd& relation,
1531 const function<optional<bdd::label_type>(bdd::label_type)>& m);
1532
1550 bdd
1551 bdd_relprev(const bdd& states,
1552 const bdd& relation,
1553 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1554 replace_type m_type);
1555
1559 bdd
1560 bdd_relprev(const exec_policy& ep,
1561 const bdd& states,
1562 const bdd& relation,
1563 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1564 replace_type m_type);
1565
1578 bdd
1579 bdd_relprev(const bdd& states, const bdd& relation, const bdd::label_type varcount);
1580
1585 bdd
1586 bdd_relprev(const exec_policy& ep,
1587 const bdd& states,
1588 const bdd& relation,
1589 const bdd::label_type varcount);
1590
1602 bdd
1603 bdd_relprev(const bdd& states, const bdd& relation);
1604
1609 bdd
1610 bdd_relprev(const exec_policy& ep, const bdd& states, const bdd& relation);
1611
1614
1619
1625 bool
1626 bdd_iscanonical(const bdd& f);
1627
1633 bool
1634 bdd_isconst(const bdd& f);
1635
1641 bool
1642 bdd_isterminal(const bdd& f);
1643
1647 bool
1648 bdd_isfalse(const bdd& f);
1649
1653 bool
1654 bdd_istrue(const bdd& f);
1655
1661 bool
1662 bdd_isvar(const bdd& f);
1663
1669 bool
1670 bdd_isithvar(const bdd& f);
1671
1677 bool
1678 bdd_isnithvar(const bdd& f);
1679
1685 bool
1686 bdd_iscube(const bdd& f);
1687
1691 bool
1692 bdd_equal(const bdd& f, const bdd& g);
1693
1697 bool
1698 bdd_equal(const exec_policy&, const bdd& f, const bdd& g);
1699
1703 bool
1704 operator==(const bdd& f, const bdd& g);
1705
1707 bool
1708 operator==(__bdd&& f, const bdd& g);
1709 bool
1710 operator==(const bdd& f, __bdd&& g);
1711 bool
1712 operator==(__bdd&& f, __bdd&& g);
1714
1720 bool
1721 bdd_unequal(const bdd& f, const bdd& g);
1722
1726 bool
1727 bdd_unequal(const exec_policy& ep, const bdd& f, const bdd& g);
1728
1732 bool
1733 operator!=(const bdd& f, const bdd& g);
1734
1736 bool
1737 operator!=(const bdd& f, __bdd&& g);
1738 bool
1739 operator!=(__bdd&& f, const bdd& g);
1740 bool
1741 operator!=(__bdd&& f, __bdd&& g);
1743
1746
1751
1755 size_t
1756 bdd_nodecount(const bdd& f);
1757
1762 bdd::label_type
1763 bdd_varcount(const bdd& f);
1764
1770 uint64_t
1771 bdd_pathcount(const bdd& f);
1772
1776 uint64_t
1777 bdd_pathcount(const exec_policy& ep, const bdd& f);
1778
1793 uint64_t
1794 bdd_satcount(const bdd& f, bdd::label_type varcount);
1795
1799 uint64_t
1800 bdd_satcount(const exec_policy& ep, const bdd& f, bdd::label_type varcount);
1801
1810 uint64_t
1811 bdd_satcount(const bdd& f);
1812
1816 uint64_t
1817 bdd_satcount(const exec_policy& ep, const bdd& f);
1818
1821
1826
1838 bdd
1839 bdd_replace(const bdd& f, const function<bdd::label_type(bdd::label_type)>& m);
1840
1844 bdd
1845 bdd_replace(const exec_policy& ep,
1846 const bdd& f,
1847 const function<bdd::label_type(bdd::label_type)>& m);
1848
1863 bdd
1864 bdd_replace(const bdd& f,
1865 const function<bdd::label_type(bdd::label_type)>& m,
1866 replace_type m_type);
1867
1871 bdd
1872 bdd_replace(const exec_policy& ep,
1873 const bdd& f,
1874 const function<bdd::label_type(bdd::label_type)>& m,
1875 replace_type m_type);
1876
1878
1893 bdd
1894 bdd_replace(__bdd&& f, const function<bdd::label_type(bdd::label_type)>& m);
1895
1899 bdd
1900 bdd_replace(const exec_policy& ep,
1901 __bdd&& f,
1902 const function<bdd::label_type(bdd::label_type)>& m);
1903
1919 bdd
1920 bdd_replace(__bdd&& f, const function<bdd::label_type(bdd::label_type)>& m, replace_type m_type);
1921
1925 bdd
1926 bdd_replace(const exec_policy& ep,
1927 __bdd&& f,
1928 const function<bdd::label_type(bdd::label_type)>& m,
1929 replace_type m_type);
1930
1932
1943 void
1944 bdd_support(const bdd& f, const consumer<bdd::label_type>& cb);
1945
1958 template <typename OutputIt,
1959 typename = enable_if<!is_convertible<OutputIt, consumer<bdd::label_type>>>>
1960 OutputIt
1961 bdd_support(const bdd& f, OutputIt iter)
1962 {
1963 bdd_support(f, make_consumer<bdd::label_type>(iter));
1964 return iter;
1965 }
1966
1972 bdd::label_type
1973 bdd_topvar(const bdd& f);
1974
1980 bdd::label_type
1981 bdd_minvar(const bdd& f);
1982
1988 bdd::label_type
1989 bdd_maxvar(const bdd& f);
1990
2000 bdd
2001 bdd_satmin(const bdd& f);
2002
2014 bdd
2015 bdd_satmin(const bdd& f,
2016 const generator<bdd::label_type>& d,
2017 const size_t d_size = bdd::max_label + 1);
2018
2034 template <typename ForwardIt, typename = enable_if<is_const<typename ForwardIt::reference>>>
2035 bdd
2036 bdd_satmin(const bdd& f, ForwardIt cbegin, ForwardIt cend)
2037 {
2038 return bdd_satmin(f, make_generator(cbegin, cend), std::distance(cbegin, cend));
2039 }
2040
2055 bdd
2056 bdd_satmin(const bdd& f, const bdd& d);
2057
2065 void
2066 bdd_satmin(const bdd& f, const consumer<pair<bdd::label_type, bool>>& c);
2067
2079 template <typename OutputIt,
2080 typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>>
2081 && !is_convertible<OutputIt, bdd>>>
2082 OutputIt
2088
2098 bdd
2099 bdd_satmax(const bdd& f);
2100
2112 bdd
2113 bdd_satmax(const bdd& f,
2114 const generator<bdd::label_type>& d,
2115 const size_t d_size = bdd::max_label + 1);
2116
2132 template <typename ForwardIt, typename = enable_if<is_const<typename ForwardIt::reference>>>
2133 bdd
2134 bdd_satmax(const bdd& f, ForwardIt cbegin, ForwardIt cend)
2135 {
2136 return bdd_satmax(f, make_generator(cbegin, cend), std::distance(cbegin, cend));
2137 }
2138
2153 bdd
2154 bdd_satmax(const bdd& f, const bdd& d);
2155
2163 void
2164 bdd_satmax(const bdd& f, const consumer<pair<bdd::label_type, bool>>& c);
2165
2177 template <typename OutputIt,
2178 typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>>
2179 && !is_convertible<OutputIt, bdd>>>
2180 OutputIt
2186
2200 pair<bdd, double>
2201 bdd_optmin(const bdd& f, const cost<bdd::label_type>& c);
2202
2207 pair<bdd, double>
2208 bdd_optmin(const exec_policy& ep, const bdd& f, const cost<bdd::label_type>& c);
2209
2227 double
2228 bdd_optmin(const bdd& f,
2229 const cost<bdd::label_type>& c,
2230 const consumer<pair<bdd::label_type, bool>>& cb);
2231
2236 double
2237 bdd_optmin(const exec_policy& ep,
2238 const bdd& f,
2239 const cost<bdd::label_type>& c,
2240 const consumer<pair<bdd::label_type, bool>>& cb);
2241
2254 bool
2255 bdd_eval(const bdd& f, const predicate<bdd::label_type>& xs);
2256
2272 bool
2273 bdd_eval(const bdd& f, const generator<pair<bdd::label_type, bool>>& xs);
2274
2293 template <typename ForwardIt>
2294 bool
2295 bdd_eval(const bdd& f, ForwardIt begin, ForwardIt end)
2296 {
2297 return bdd_eval(f, make_generator(begin, end));
2298 }
2299
2302
2307
2321 __bdd
2322 bdd_from(const zdd& A, const generator<bdd::label_type>& dom);
2323
2328 __bdd
2329 bdd_from(const exec_policy& ep, const zdd& A, const generator<bdd::label_type>& dom);
2330
2347 template <typename ForwardIt>
2348 __bdd
2349 bdd_from(const zdd& A, ForwardIt begin, ForwardIt end)
2350 {
2351 return bdd_from(A, make_generator(begin, end));
2352 }
2353
2358 template <typename ForwardIt>
2359 __bdd
2360 bdd_from(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
2361 {
2362 return bdd_from(ep, A, make_generator(begin, end));
2363 }
2364
2379 __bdd
2380 bdd_from(const zdd& A);
2381
2386 __bdd
2387 bdd_from(const exec_policy& ep, const zdd& A);
2388
2391
2396
2400 void
2401 bdd_printdot(const bdd& f, std::ostream& out = std::cout, bool include_id = false);
2402
2406 void
2407 bdd_printdot(const bdd& f, const std::string& file_name, bool include_id = false);
2408
2411
2414}
2415
2416#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:100
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.
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 f, i.e. the number of levels in the BDD.
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:79
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:169
adiar::cost
function< double(VarType)> cost
Cost function that assigns a cost to each variable.
Definition functional.h:155
adiar::consumer
function< void(Arg)> consumer
Consumer function of value(s) of type(s) Args.
Definition functional.h:60
adiar::make_generator
generator< typename ForwardIt::value_type > make_generator(ForwardIt &begin, ForwardIt &end)
Wrap a begin and end iterator pair into a generator function.
Definition functional.h:176
adiar::function
std::function< TypeSignature > function
General-purpose polymorphic function wrapper.
Definition functional.h:38
adiar::predicate
function< bool(Args...)> predicate
Predicate function given value(s) of type(s) Args.
Definition functional.h:48
adiar::make_consumer
consumer< ValueType > make_consumer(OutputIt &iter)
Wrap an iterator into a consumer function.
Definition functional.h:67
adiar
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