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
21
22#include <iostream>
23#include <string>
24#include <type_traits>
25
26#include <adiar/bdd/bdd.h>
27#include <adiar/bool_op.h>
28#include <adiar/exec_policy.h>
29#include <adiar/functional.h>
30#include <adiar/types.h>
31#include <adiar/zdd/zdd.h>
32
33namespace adiar
34{
50
59 bdd
60 bdd_const(bool value);
61
70 bdd
71 bdd_terminal(bool value);
72
80 bdd
81 bdd_false();
82
90 inline bdd
91 bdd_bot()
92 {
93 return bdd_false();
94 }
95
101 bdd
102 bdd_true();
103
111 inline bdd
112 bdd_top()
113 {
114 return bdd_true();
115 }
116
128 bdd
129 bdd_ithvar(bdd::label_type var);
130
142 bdd
143 bdd_nithvar(bdd::label_type var);
144
160 bdd
161 bdd_and(const generator<int>& vars);
162
175 bdd
176 bdd_and(const generator<pair<bdd::label_type, bool>>& vars);
177
196 template <typename ForwardIt, typename = enable_if<!is_convertible<ForwardIt, bdd>>>
197 bdd
198 bdd_and(ForwardIt begin, ForwardIt end)
199 {
200 return bdd_and(make_generator(begin, end));
201 }
202
218 bdd
219 bdd_or(const generator<int>& vars);
220
233 bdd
234 bdd_or(const generator<pair<bdd::label_type, bool>>& vars);
235
254 template <typename ForwardIt, typename = enable_if<!is_convertible<ForwardIt, bdd>>>
255 bdd
256 bdd_or(ForwardIt begin, ForwardIt end)
257 {
258 return bdd_or(make_generator(begin, end));
259 }
260
277 bdd
278 bdd_cube(const generator<int>& vars);
279
293 bdd
294 bdd_cube(const generator<pair<bdd::label_type, bool>>& vars);
295
315 template <typename ForwardIt>
316 bdd
317 bdd_cube(ForwardIt begin, ForwardIt end)
318 {
319 return bdd_cube(make_generator(begin, end));
320 }
321
325
337
347 bdd
348 bdd_not(const bdd& f);
349
351 bdd
352 bdd_not(bdd&& f);
354
358 bdd
359 operator~(const bdd& f);
360
362 bdd
363 operator~(bdd&& f);
364 bdd
365 operator~(__bdd&& f);
367
384 __bdd
385 bdd_apply(const bdd& f, const bdd& g, const predicate<bool, bool>& op);
386
391 __bdd
392 bdd_apply(const exec_policy& ep, const bdd& f, const bdd& g, const predicate<bool, bool>& op);
394
402 __bdd
403 bdd_and(const bdd& f, const bdd& g);
404
409 __bdd
410 bdd_and(const exec_policy& ep, const bdd& f, const bdd& g);
412
416 __bdd
417 operator&(const bdd& lhs, const bdd& rhs);
418
420 __bdd
421 operator&(const bdd&, __bdd&&);
422 __bdd
423 operator&(__bdd&&, const bdd&);
424 __bdd
425 operator&(__bdd&&, __bdd&&);
427
431 __bdd
432 operator*(const bdd& lhs, const bdd& rhs);
433
435 __bdd
436 operator*(const bdd&, __bdd&&);
437 __bdd
438 operator*(__bdd&&, const bdd&);
439 __bdd
440 operator*(__bdd&&, __bdd&&);
442
450 __bdd
451 bdd_nand(const bdd& f, const bdd& g);
452
457 __bdd
458 bdd_nand(const exec_policy& ep, const bdd& f, const bdd& g);
460
468 __bdd
469 bdd_or(const bdd& f, const bdd& g);
470
475 __bdd
476 bdd_or(const exec_policy& ep, const bdd& f, const bdd& g);
478
482 __bdd
483 operator|(const bdd& lhs, const bdd& rhs);
484
486 __bdd
487 operator|(const bdd&, __bdd&&);
488 __bdd
489 operator|(__bdd&&, const bdd&);
490 __bdd
491 operator|(__bdd&&, __bdd&&);
493
497 bdd
498 operator+(const bdd& f);
499
504 __bdd
505 operator+(__bdd&& f);
507
511 __bdd
512 operator+(const bdd& lhs, const bdd& rhs);
513
515 __bdd
516 operator+(const bdd&, __bdd&&);
517 __bdd
518 operator+(__bdd&&, const bdd&);
519 __bdd
520 operator+(__bdd&&, __bdd&&);
522
530 __bdd
531 bdd_nor(const bdd& f, const bdd& g);
532
537 __bdd
538 bdd_nor(const exec_policy& ep, const bdd& f, const bdd& g);
540
548 __bdd
549 bdd_xor(const bdd& f, const bdd& g);
550
555 __bdd
556 bdd_xor(const exec_policy& ep, const bdd& f, const bdd& g);
558
562 __bdd
563 operator^(const bdd& lhs, const bdd& rhs);
564
566 __bdd
567 operator^(const bdd&, __bdd&&);
568 __bdd
569 operator^(__bdd&&, const bdd&);
570 __bdd
571 operator^(__bdd&&, __bdd&&);
573
581 __bdd
582 bdd_xnor(const bdd& f, const bdd& g);
583
584
589 __bdd
590 bdd_xnor(const exec_policy& ep, const bdd& f, const bdd& g);
592
600 __bdd
601 bdd_imp(const bdd& f, const bdd& g);
602
607 __bdd
608 bdd_imp(const exec_policy& ep, const bdd& f, const bdd& g);
610
618 __bdd
619 bdd_invimp(const bdd& f, const bdd& g);
620
625 __bdd
626 bdd_invimp(const exec_policy& ep, const bdd& f, const bdd& g);
628
636 __bdd
637 bdd_equiv(const bdd& f, const bdd& g);
638
643 __bdd
644 bdd_equiv(const exec_policy& ep, const bdd& f, const bdd& g);
646
654 __bdd
655 bdd_diff(const bdd& f, const bdd& g);
656
661 __bdd
662 bdd_diff(const exec_policy& ep, const bdd& f, const bdd& g);
664
670 bdd
671 operator-(const bdd& f);
672
674 __bdd
675 operator-(__bdd&& f);
677
681 __bdd
682 operator-(const bdd& lhs, const bdd& rhs);
683
685 __bdd
686 operator-(const bdd&, __bdd&&);
687 __bdd
688 operator-(__bdd&&, const bdd&);
689 __bdd
690 operator-(__bdd&&, __bdd&&);
692
700 __bdd
701 bdd_less(const bdd& f, const bdd& g);
702
707 __bdd
708 bdd_less(const exec_policy& ep, const bdd& f, const bdd& g);
710
734 __bdd
735 bdd_ite(const bdd& f, const bdd& g, const bdd& h);
736
741 __bdd
742 bdd_ite(const exec_policy& ep, const bdd& f, const bdd& g, const bdd& h);
744
761 __bdd
762 bdd_restrict(const bdd& f, bdd::label_type var, bool val);
763
768 __bdd
769 bdd_restrict(const exec_policy& ep, const bdd& f, bdd::label_type var, bool val);
771
787 __bdd
788 bdd_restrict(const bdd& f, const generator<pair<bdd::label_type, bool>>& xs);
789
794 __bdd
795 bdd_restrict(const exec_policy& ep,
796 const bdd& f,
797 const generator<pair<bdd::label_type, bool>>& xs);
799
818 template <typename ForwardIt>
819 __bdd
820 bdd_restrict(const bdd& f, ForwardIt begin, ForwardIt end)
821 {
822 return bdd_restrict(f, make_generator(begin, end));
823 }
824
829 template <typename ForwardIt>
830 __bdd
831 bdd_restrict(const exec_policy& ep, const bdd& f, ForwardIt begin, ForwardIt end)
832 {
833 return bdd_restrict(ep, f, make_generator(begin, end));
834 }
836
848 __bdd
849 bdd_low(const bdd& f);
850
855 __bdd
856 bdd_low(const exec_policy& ep, const bdd& f);
858
870 __bdd
871 bdd_high(const bdd& f);
872
877 __bdd
878 bdd_high(const exec_policy& ep, const bdd& f);
880
895 __bdd
896 bdd_exists(const bdd& f, bdd::label_type var);
897
899
903 inline __bdd
904 bdd_exists(bdd&& f, bdd::label_type var)
905 {
906 return bdd_exists(f, var);
907 }
908
912 __bdd
913 bdd_exists(const exec_policy& ep, const bdd& f, bdd::label_type var);
914
918 inline __bdd
919 bdd_exists(const exec_policy& ep, bdd&& f, bdd::label_type var)
920 {
921 return bdd_exists(ep, f, var);
922 }
923
925
939 __bdd
940 bdd_exists(const bdd& f, const predicate<bdd::label_type>& vars);
941
943
951 __bdd
952 bdd_exists(bdd&& f, const predicate<bdd::label_type>& vars);
953
960 __bdd
961 bdd_exists(__bdd&& f, const predicate<bdd::label_type>& vars);
962
966 __bdd
967 bdd_exists(const exec_policy& ep, const bdd& f, const predicate<bdd::label_type>& vars);
968
976 __bdd
977 bdd_exists(const exec_policy& ep, bdd&& f, const predicate<bdd::label_type>& vars);
978
985 __bdd
986 bdd_exists(const exec_policy& ep, __bdd&& f, const predicate<bdd::label_type>& vars);
987
989
1002 __bdd
1003 bdd_exists(const bdd& f, const generator<bdd::label_type>& vars);
1004
1006
1014 __bdd
1015 bdd_exists(bdd&& f, const generator<bdd::label_type>& vars);
1016
1023 __bdd
1024 bdd_exists(__bdd&& f, const generator<bdd::label_type>& vars);
1025
1029 __bdd
1030 bdd_exists(const exec_policy& ep, const bdd& f, const generator<bdd::label_type>& vars);
1031
1039 __bdd
1040 bdd_exists(const exec_policy& ep, bdd&& f, const generator<bdd::label_type>& vars);
1041
1048 __bdd
1049 bdd_exists(const exec_policy& ep, __bdd&& f, const generator<bdd::label_type>& vars);
1050
1052
1068 template <typename ForwardIt>
1069 __bdd
1070 bdd_exists(const bdd& f, ForwardIt begin, ForwardIt end)
1071 {
1072 return bdd_exists(f, make_generator(begin, end));
1073 }
1074
1076
1084 template <typename ForwardIt>
1085 __bdd
1086 bdd_exists(bdd&& f, ForwardIt begin, ForwardIt end)
1087 {
1088 return bdd_exists(std::move(f), make_generator(begin, end));
1089 }
1090
1097 template <typename ForwardIt>
1098 __bdd
1099 bdd_exists(__bdd&& f, ForwardIt begin, ForwardIt end)
1100 {
1101 return bdd_exists(std::move(f), make_generator(begin, end));
1102 }
1103
1107 template <typename ForwardIt>
1108 __bdd
1109 bdd_exists(const exec_policy& ep, const bdd& f, ForwardIt begin, ForwardIt end)
1110 {
1111 return bdd_exists(ep, f, make_generator(begin, end));
1112 }
1113
1121 template <typename ForwardIt>
1122 __bdd
1123 bdd_exists(const exec_policy& ep, bdd&& f, ForwardIt begin, ForwardIt end)
1124 {
1125 return bdd_exists(ep, std::move(f), make_generator(begin, end));
1126 }
1127
1134 template <typename ForwardIt>
1135 __bdd
1136 bdd_exists(const exec_policy& ep, __bdd&& f, ForwardIt begin, ForwardIt end)
1137 {
1138 return bdd_exists(ep, std::move(f), make_generator(begin, end));
1139 }
1140
1142
1157 __bdd
1158 bdd_forall(const bdd& f, bdd::label_type var);
1159
1161
1165 inline __bdd
1166 bdd_forall(bdd&& f, bdd::label_type var)
1167 {
1168 return bdd_forall(f, var);
1169 }
1170
1174 __bdd
1175 bdd_forall(const exec_policy& ep, const bdd& f, bdd::label_type var);
1176
1180 inline __bdd
1181 bdd_forall(const exec_policy& ep, bdd&& f, bdd::label_type var)
1182 {
1183 return bdd_forall(ep, f, var);
1184 }
1185
1187
1201 __bdd
1202 bdd_forall(const bdd& f, const predicate<bdd::label_type>& vars);
1203
1205
1213 __bdd
1214 bdd_forall(bdd&& f, const predicate<bdd::label_type>& vars);
1215
1222 __bdd
1223 bdd_forall(__bdd&& f, const predicate<bdd::label_type>& vars);
1224
1228 __bdd
1229 bdd_forall(const exec_policy& ep, const bdd& f, const predicate<bdd::label_type>& vars);
1230
1238 __bdd
1239 bdd_forall(const exec_policy& ep, bdd&& f, const predicate<bdd::label_type>& vars);
1240
1247 __bdd
1248 bdd_forall(const exec_policy& ep, __bdd&& f, const predicate<bdd::label_type>& vars);
1249
1251
1264 __bdd
1265 bdd_forall(const bdd& f, const generator<bdd::label_type>& vars);
1266
1268
1276 __bdd
1277 bdd_forall(bdd&& f, const generator<bdd::label_type>& vars);
1278
1285 __bdd
1286 bdd_forall(bdd&& f, const generator<bdd::label_type>& vars);
1287
1291 __bdd
1292 bdd_forall(const exec_policy& ep, const bdd& f, const generator<bdd::label_type>& vars);
1293
1301 __bdd
1302 bdd_forall(const exec_policy& ep, bdd&& f, const generator<bdd::label_type>& vars);
1303
1310 __bdd
1311 bdd_forall(const exec_policy& ep, __bdd&& f, const generator<bdd::label_type>& vars);
1312
1314
1330 template <typename ForwardIt>
1331 __bdd
1332 bdd_forall(const bdd& f, ForwardIt begin, ForwardIt end)
1333 {
1334 return bdd_forall(f, make_generator(begin, end));
1335 }
1336
1338
1346 template <typename ForwardIt>
1347 __bdd
1348 bdd_forall(bdd&& f, ForwardIt begin, ForwardIt end)
1349 {
1350 return bdd_forall(std::move(f), make_generator(begin, end));
1351 }
1352
1359 template <typename ForwardIt>
1360 __bdd
1361 bdd_forall(__bdd&& f, ForwardIt begin, ForwardIt end)
1362 {
1363 return bdd_forall(std::move(f), make_generator(begin, end));
1364 }
1365
1369 template <typename ForwardIt>
1370 __bdd
1371 bdd_forall(const exec_policy& ep, const bdd& f, ForwardIt begin, ForwardIt end)
1372 {
1373 return bdd_forall(ep, f, make_generator(begin, end));
1374 }
1375
1383 template <typename ForwardIt>
1384 __bdd
1385 bdd_forall(const exec_policy& ep, bdd&& f, ForwardIt begin, ForwardIt end)
1386 {
1387 return bdd_forall(ep, std::move(f), make_generator(begin, end));
1388 }
1389
1396 template <typename ForwardIt>
1397 __bdd
1398 bdd_forall(const exec_policy& ep, __bdd&& f, ForwardIt begin, ForwardIt end)
1399 {
1400 return bdd_forall(ep, std::move(f), make_generator(begin, end));
1401 }
1402
1404
1408
1422
1438 __bdd
1439 bdd_replace(const bdd& f,
1440 const function<bdd::label_type(bdd::label_type)>& m,
1441 replace_type m_type = replace_type::Auto);
1442
1444
1448 __bdd
1449 bdd_replace(const exec_policy& ep,
1450 const bdd& f,
1451 const function<bdd::label_type(bdd::label_type)>& m,
1452 replace_type m_type = replace_type::Auto);
1453
1470 __bdd
1471 bdd_replace(__bdd&& f,
1472 const function<bdd::label_type(bdd::label_type)>& m,
1473 replace_type m_type = replace_type::Auto);
1474
1478 __bdd
1479 bdd_replace(const exec_policy& ep,
1480 __bdd&& f,
1481 const function<bdd::label_type(bdd::label_type)>& m,
1482 replace_type m_type = replace_type::Auto);
1483
1485
1489
1501
1516 bdd
1517 bdd_relprod(const bdd& states, const bdd& relation, const predicate<bdd::label_type>& pred);
1518
1523 bdd
1524 bdd_relprod(const exec_policy& ep,
1525 const bdd& states,
1526 const bdd& relation,
1527 const predicate<bdd::label_type>& pred);
1529
1553 bdd
1554 bdd_relnext(const bdd& states,
1555 const bdd& relation,
1556 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1557 replace_type m_type = replace_type::Auto);
1558
1563 bdd
1564 bdd_relnext(const exec_policy& ep,
1565 const bdd& states,
1566 const bdd& relation,
1567 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1568 replace_type m_type = replace_type::Auto);
1570
1590 bdd
1591 bdd_relnext(const bdd& states, const bdd& relation, const bdd::label_type varcount);
1592
1598 bdd
1599 bdd_relnext(const exec_policy& ep,
1600 const bdd& states,
1601 const bdd& relation,
1602 const bdd::label_type varcount);
1604
1620 bdd
1621 bdd_relnext(const bdd& states, const bdd& relation);
1622
1628 bdd
1629 bdd_relnext(const exec_policy& ep, const bdd& states, const bdd& relation);
1631
1656 bdd
1657 bdd_relprev(const bdd& states,
1658 const bdd& relation,
1659 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1660 replace_type m_type = replace_type::Auto);
1661
1666 bdd
1667 bdd_relprev(const exec_policy& ep,
1668 const bdd& states,
1669 const bdd& relation,
1670 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1671 replace_type m_type = replace_type::Auto);
1673
1693 bdd
1694 bdd_relprev(const bdd& states, const bdd& relation, const bdd::label_type varcount);
1695
1701 bdd
1702 bdd_relprev(const exec_policy& ep,
1703 const bdd& states,
1704 const bdd& relation,
1705 const bdd::label_type varcount);
1707
1722 bdd
1723 bdd_relprev(const bdd& states, const bdd& relation);
1724
1730 bdd
1731 bdd_relprev(const exec_policy& ep, const bdd& states, const bdd& relation);
1733
1737
1749
1755 bool
1756 bdd_iscanonical(const bdd& f);
1757
1763 bool
1764 bdd_isconst(const bdd& f);
1765
1771 bool
1772 bdd_isterminal(const bdd& f);
1773
1783 bool
1784 bdd_isfalse(const bdd& f);
1785
1789 bool
1790 bdd_istrue(const bdd& f);
1791
1799 bool
1800 bdd_isvar(const bdd& f);
1801
1809 bool
1810 bdd_isithvar(const bdd& f);
1811
1819 bool
1820 bdd_isnithvar(const bdd& f);
1821
1827 bool
1828 bdd_iscube(const bdd& f);
1829
1837 bool
1838 bdd_equal(const bdd& f, const bdd& g);
1839
1844 bool
1845 bdd_equal(const exec_policy&, const bdd& f, const bdd& g);
1847
1851 bool
1852 operator==(const bdd& f, const bdd& g);
1853
1855 bool
1856 operator==(__bdd&& f, const bdd& g);
1857 bool
1858 operator==(const bdd& f, __bdd&& g);
1859 bool
1860 operator==(__bdd&& f, __bdd&& g);
1862
1872 bool
1873 bdd_unequal(const bdd& f, const bdd& g);
1874
1879 bool
1880 bdd_unequal(const exec_policy& ep, const bdd& f, const bdd& g);
1882
1886 bool
1887 operator!=(const bdd& f, const bdd& g);
1888
1890 bool
1891 operator!=(const bdd& f, __bdd&& g);
1892 bool
1893 operator!=(__bdd&& f, const bdd& g);
1894 bool
1895 operator!=(__bdd&& f, __bdd&& g);
1897
1901
1913
1917 size_t
1918 bdd_nodecount(const bdd& f);
1919
1924 bdd::label_type
1925 bdd_varcount(const bdd& f);
1926
1932 uint64_t
1933 bdd_pathcount(const bdd& f);
1934
1939 uint64_t
1940 bdd_pathcount(const exec_policy& ep, const bdd& f);
1942
1957 uint64_t
1958 bdd_satcount(const bdd& f, bdd::label_type varcount);
1959
1964 uint64_t
1965 bdd_satcount(const exec_policy& ep, const bdd& f, bdd::label_type varcount);
1967
1976 uint64_t
1977 bdd_satcount(const bdd& f);
1978
1983 uint64_t
1984 bdd_satcount(const exec_policy& ep, const bdd& f);
1986
1990
2002
2013 void
2014 bdd_support(const bdd& f, const consumer<bdd::label_type>& cb);
2015
2028 template <typename OutputIt,
2029 typename = enable_if<!is_convertible<OutputIt, consumer<bdd::label_type>>>>
2030 OutputIt
2031 bdd_support(const bdd& f, OutputIt iter)
2032 {
2033 bdd_support(f, make_consumer<bdd::label_type>(iter));
2034 return iter;
2035 }
2036
2042 bdd::label_type
2043 bdd_topvar(const bdd& f);
2044
2050 bdd::label_type
2051 bdd_minvar(const bdd& f);
2052
2058 bdd::label_type
2059 bdd_maxvar(const bdd& f);
2060
2070 bdd
2071 bdd_satmin(const bdd& f);
2072
2088 bdd
2089 bdd_satmin(const bdd& f,
2090 const generator<bdd::label_type>& d,
2091 const size_t d_size = bdd::max_label + 1);
2092
2108 template <typename ForwardIt, typename = enable_if<is_const<typename ForwardIt::reference>>>
2109 bdd
2110 bdd_satmin(const bdd& f, ForwardIt cbegin, ForwardIt cend)
2111 {
2112 return bdd_satmin(f, make_generator(cbegin, cend), std::distance(cbegin, cend));
2113 }
2114
2129 bdd
2130 bdd_satmin(const bdd& f, const bdd& d);
2131
2142 void
2143 bdd_satmin(const bdd& f, const consumer<pair<bdd::label_type, bool>>& c);
2144
2156 template <typename OutputIt,
2157 typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>>
2158 && !is_convertible<OutputIt, bdd>>>
2159 OutputIt
2165
2178 bdd
2179 bdd_satmax(const bdd& f);
2180
2195 bdd
2196 bdd_satmax(const bdd& f,
2197 const generator<bdd::label_type>& d,
2198 const size_t d_size = bdd::max_label + 1);
2199
2215 template <typename ForwardIt, typename = enable_if<is_const<typename ForwardIt::reference>>>
2216 bdd
2217 bdd_satmax(const bdd& f, ForwardIt cbegin, ForwardIt cend)
2218 {
2219 return bdd_satmax(f, make_generator(cbegin, cend), std::distance(cbegin, cend));
2220 }
2221
2236 bdd
2237 bdd_satmax(const bdd& f, const bdd& d);
2238
2249 void
2250 bdd_satmax(const bdd& f, const consumer<pair<bdd::label_type, bool>>& c);
2251
2263 template <typename OutputIt,
2264 typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>>
2265 && !is_convertible<OutputIt, bdd>>>
2266 OutputIt
2272
2286 pair<bdd, double>
2287 bdd_optmin(const bdd& f, const cost<bdd::label_type>& c);
2288
2294 pair<bdd, double>
2295 bdd_optmin(const exec_policy& ep, const bdd& f, const cost<bdd::label_type>& c);
2297
2315 double
2316 bdd_optmin(const bdd& f,
2317 const cost<bdd::label_type>& c,
2318 const consumer<pair<bdd::label_type, bool>>& cb);
2319
2325 double
2326 bdd_optmin(const exec_policy& ep,
2327 const bdd& f,
2328 const cost<bdd::label_type>& c,
2329 const consumer<pair<bdd::label_type, bool>>& cb);
2331
2344 bool
2345 bdd_eval(const bdd& f, const predicate<bdd::label_type>& xs);
2346
2362 bool
2363 bdd_eval(const bdd& f, const generator<pair<bdd::label_type, bool>>& xs);
2364
2383 template <typename ForwardIt>
2384 bool
2385 bdd_eval(const bdd& f, ForwardIt begin, ForwardIt end)
2386 {
2387 return bdd_eval(f, make_generator(begin, end));
2388 }
2389
2393
2405
2419 __bdd
2420 bdd_from(const zdd& A, const generator<bdd::label_type>& dom);
2421
2427 __bdd
2428 bdd_from(const exec_policy& ep, const zdd& A, const generator<bdd::label_type>& dom);
2430
2447 template <typename ForwardIt>
2448 __bdd
2449 bdd_from(const zdd& A, ForwardIt begin, ForwardIt end)
2450 {
2451 return bdd_from(A, make_generator(begin, end));
2452 }
2453
2459 template <typename ForwardIt>
2460 __bdd
2461 bdd_from(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
2462 {
2463 return bdd_from(ep, A, make_generator(begin, end));
2464 }
2466
2481 __bdd
2482 bdd_from(const zdd& A);
2483
2489 __bdd
2490 bdd_from(const exec_policy& ep, const zdd& A);
2492
2496
2508
2512 void
2513 bdd_printdot(const bdd& f, std::ostream& out = std::cout, bool include_id = false);
2514
2518 void
2519 bdd_printdot(const bdd& f, const std::string& file_name, bool include_id = false);
2520
2524}
2525
2526#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:58
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:67
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_nor
__bdd bdd_nor(const bdd &f, const bdd &g)
Logical 'nor' operator.
adiar::operator+
bdd operator+(const bdd &f)
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_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::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_not
bdd bdd_not(const bdd &f)
Negation of a BDD.
adiar::bdd_imp
__bdd bdd_imp(const bdd &f, const bdd &g)
Logical 'implication' operator.
adiar::bdd_high
__bdd bdd_high(const bdd &f)
Restrict the root to true, i.e. follow its high edge.
adiar::bdd_xnor
__bdd bdd_xnor(const bdd &f, const bdd &g)
Logical 'xnor' operator.
adiar::bdd_equiv
__bdd bdd_equiv(const bdd &f, const bdd &g)
Logical 'equivalence' operator.
adiar::operator~
bdd operator~(const bdd &f)
adiar::bdd_exists
__bdd bdd_exists(const bdd &f, bdd::label_type var)
Existential quantification of a single variable.
adiar::operator^
__bdd operator^(const bdd &lhs, const bdd &rhs)
adiar::bdd_less
__bdd bdd_less(const bdd &f, const bdd &g)
Logical 'less than' operator.
adiar::bdd_nand
__bdd bdd_nand(const bdd &f, const bdd &g)
Logical 'nand' operator.
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_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_const
bdd bdd_const(bool value)
The BDD representing the given constant value.
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_top
bdd bdd_top()
The top of the powerset lattice.
Definition bdd.h:112
adiar::bdd_bot
bdd bdd_bot()
The bottom of the powerset lattice.
Definition bdd.h:91
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_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::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_nodecount
size_t bdd_nodecount(const bdd &f)
The number of (internal) nodes used to represent the function.
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_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_pathcount
uint64_t bdd_pathcount(const bdd &f)
Count all unique (but not necessarily disjoint) paths to the true terminal.
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_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::bdd_satmin
bdd bdd_satmin(const bdd &f)
The lexicographically smallest cube x such that f(x) is true.
adiar::bdd_satmax
bdd bdd_satmax(const bdd &f)
The lexicographically largest cube x such that f(x) is true.
adiar::bdd_maxvar
bdd::label_type bdd_maxvar(const bdd &f)
Get the maximal occurring variable in the function's support.
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_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_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::bdd_iscanonical
bool bdd_iscanonical(const bdd &f)
Check whether a BDD is canonical.
adiar::bdd_unequal
bool bdd_unequal(const bdd &f, const bdd &g)
Whether the two BDDs represent different functions.
adiar::bdd_isithvar
bool bdd_isithvar(const bdd &f)
Whether a BDD is the function of a single positive variable.
adiar::bdd_istrue
bool bdd_istrue(const bdd &f)
Whether a BDD is the constant 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::operator!=
bool operator!=(const bdd &f, const bdd &g)
adiar::bdd_iscube
bool bdd_iscube(const bdd &f)
Whether a BDD represents a cube.
adiar::bdd_isconst
bool bdd_isconst(const bdd &f)
Whether a BDD is a constant.
adiar::operator==
bool operator==(const bdd &f, const bdd &g)
adiar::bdd_equal
bool bdd_equal(const bdd &f, const bdd &g)
Whether the two BDDs represent the same function.
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_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_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_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_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::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