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
588 __bdd
589 bdd_xnor(const exec_policy& ep, const bdd& f, const bdd& g);
591
599 __bdd
600 bdd_imp(const bdd& f, const bdd& g);
601
606 __bdd
607 bdd_imp(const exec_policy& ep, const bdd& f, const bdd& g);
609
617 __bdd
618 bdd_invimp(const bdd& f, const bdd& g);
619
624 __bdd
625 bdd_invimp(const exec_policy& ep, const bdd& f, const bdd& g);
627
635 __bdd
636 bdd_equiv(const bdd& f, const bdd& g);
637
642 __bdd
643 bdd_equiv(const exec_policy& ep, const bdd& f, const bdd& g);
645
653 __bdd
654 bdd_diff(const bdd& f, const bdd& g);
655
660 __bdd
661 bdd_diff(const exec_policy& ep, const bdd& f, const bdd& g);
663
669 bdd
670 operator-(const bdd& f);
671
673 __bdd
674 operator-(__bdd&& f);
676
680 __bdd
681 operator-(const bdd& lhs, const bdd& rhs);
682
684 __bdd
685 operator-(const bdd&, __bdd&&);
686 __bdd
687 operator-(__bdd&&, const bdd&);
688 __bdd
689 operator-(__bdd&&, __bdd&&);
691
699 __bdd
700 bdd_less(const bdd& f, const bdd& g);
701
706 __bdd
707 bdd_less(const exec_policy& ep, const bdd& f, const bdd& g);
709
733 __bdd
734 bdd_ite(const bdd& f, const bdd& g, const bdd& h);
735
740 __bdd
741 bdd_ite(const exec_policy& ep, const bdd& f, const bdd& g, const bdd& h);
743
760 __bdd
761 bdd_restrict(const bdd& f, bdd::label_type var, bool val);
762
767 __bdd
768 bdd_restrict(const exec_policy& ep, const bdd& f, bdd::label_type var, bool val);
770
786 __bdd
787 bdd_restrict(const bdd& f, const generator<pair<bdd::label_type, bool>>& xs);
788
793 __bdd
794 bdd_restrict(const exec_policy& ep,
795 const bdd& f,
796 const generator<pair<bdd::label_type, bool>>& xs);
797
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 }
835
837
849 __bdd
850 bdd_low(const bdd& f);
851
856 __bdd
857 bdd_low(const exec_policy& ep, const bdd& f);
859
871 __bdd
872 bdd_high(const bdd& f);
873
878 __bdd
879 bdd_high(const exec_policy& ep, const bdd& f);
881
896 __bdd
897 bdd_exists(const bdd& f, bdd::label_type var);
898
900
904 inline __bdd
905 bdd_exists(bdd&& f, bdd::label_type var)
906 {
907 return bdd_exists(f, var);
908 }
909
913 __bdd
914 bdd_exists(const exec_policy& ep, const bdd& f, bdd::label_type var);
915
919 inline __bdd
920 bdd_exists(const exec_policy& ep, bdd&& f, bdd::label_type var)
921 {
922 return bdd_exists(ep, f, var);
923 }
924
926
940 __bdd
941 bdd_exists(const bdd& f, const predicate<bdd::label_type>& vars);
942
944
952 __bdd
953 bdd_exists(bdd&& f, const predicate<bdd::label_type>& vars);
954
961 __bdd
962 bdd_exists(__bdd&& f, const predicate<bdd::label_type>& vars);
963
967 __bdd
968 bdd_exists(const exec_policy& ep, const bdd& f, const predicate<bdd::label_type>& vars);
969
977 __bdd
978 bdd_exists(const exec_policy& ep, bdd&& f, const predicate<bdd::label_type>& vars);
979
986 __bdd
987 bdd_exists(const exec_policy& ep, __bdd&& f, const predicate<bdd::label_type>& vars);
988
990
1003 __bdd
1004 bdd_exists(const bdd& f, const generator<bdd::label_type>& vars);
1005
1007
1015 __bdd
1016 bdd_exists(bdd&& f, const generator<bdd::label_type>& vars);
1017
1024 __bdd
1025 bdd_exists(__bdd&& f, const generator<bdd::label_type>& vars);
1026
1030 __bdd
1031 bdd_exists(const exec_policy& ep, const bdd& f, const generator<bdd::label_type>& vars);
1032
1040 __bdd
1041 bdd_exists(const exec_policy& ep, bdd&& f, const generator<bdd::label_type>& vars);
1042
1049 __bdd
1050 bdd_exists(const exec_policy& ep, __bdd&& f, const generator<bdd::label_type>& vars);
1051
1053
1069 template <typename ForwardIt>
1070 __bdd
1071 bdd_exists(const bdd& f, ForwardIt begin, ForwardIt end)
1072 {
1073 return bdd_exists(f, make_generator(begin, end));
1074 }
1075
1077
1085 template <typename ForwardIt>
1086 __bdd
1087 bdd_exists(bdd&& f, ForwardIt begin, ForwardIt end)
1088 {
1089 return bdd_exists(std::move(f), make_generator(begin, end));
1090 }
1091
1098 template <typename ForwardIt>
1099 __bdd
1100 bdd_exists(__bdd&& f, ForwardIt begin, ForwardIt end)
1101 {
1102 return bdd_exists(std::move(f), make_generator(begin, end));
1103 }
1104
1108 template <typename ForwardIt>
1109 __bdd
1110 bdd_exists(const exec_policy& ep, const bdd& f, ForwardIt begin, ForwardIt end)
1111 {
1112 return bdd_exists(ep, f, make_generator(begin, end));
1113 }
1114
1122 template <typename ForwardIt>
1123 __bdd
1124 bdd_exists(const exec_policy& ep, bdd&& f, ForwardIt begin, ForwardIt end)
1125 {
1126 return bdd_exists(ep, std::move(f), make_generator(begin, end));
1127 }
1128
1135 template <typename ForwardIt>
1136 __bdd
1137 bdd_exists(const exec_policy& ep, __bdd&& f, ForwardIt begin, ForwardIt end)
1138 {
1139 return bdd_exists(ep, std::move(f), make_generator(begin, end));
1140 }
1141
1143
1158 __bdd
1159 bdd_forall(const bdd& f, bdd::label_type var);
1160
1162
1166 inline __bdd
1167 bdd_forall(bdd&& f, bdd::label_type var)
1168 {
1169 return bdd_forall(f, var);
1170 }
1171
1175 __bdd
1176 bdd_forall(const exec_policy& ep, const bdd& f, bdd::label_type var);
1177
1181 inline __bdd
1182 bdd_forall(const exec_policy& ep, bdd&& f, bdd::label_type var)
1183 {
1184 return bdd_forall(ep, f, var);
1185 }
1186
1188
1202 __bdd
1203 bdd_forall(const bdd& f, const predicate<bdd::label_type>& vars);
1204
1206
1214 __bdd
1215 bdd_forall(bdd&& f, const predicate<bdd::label_type>& vars);
1216
1223 __bdd
1224 bdd_forall(__bdd&& f, const predicate<bdd::label_type>& vars);
1225
1229 __bdd
1230 bdd_forall(const exec_policy& ep, const bdd& f, const predicate<bdd::label_type>& vars);
1231
1239 __bdd
1240 bdd_forall(const exec_policy& ep, bdd&& f, const predicate<bdd::label_type>& vars);
1241
1248 __bdd
1249 bdd_forall(const exec_policy& ep, __bdd&& f, const predicate<bdd::label_type>& vars);
1250
1252
1265 __bdd
1266 bdd_forall(const bdd& f, const generator<bdd::label_type>& vars);
1267
1269
1277 __bdd
1278 bdd_forall(bdd&& f, const generator<bdd::label_type>& vars);
1279
1286 __bdd
1287 bdd_forall(bdd&& f, const generator<bdd::label_type>& vars);
1288
1292 __bdd
1293 bdd_forall(const exec_policy& ep, const bdd& f, const generator<bdd::label_type>& vars);
1294
1302 __bdd
1303 bdd_forall(const exec_policy& ep, bdd&& f, const generator<bdd::label_type>& vars);
1304
1311 __bdd
1312 bdd_forall(const exec_policy& ep, __bdd&& f, const generator<bdd::label_type>& vars);
1313
1315
1331 template <typename ForwardIt>
1332 __bdd
1333 bdd_forall(const bdd& f, ForwardIt begin, ForwardIt end)
1334 {
1335 return bdd_forall(f, make_generator(begin, end));
1336 }
1337
1339
1347 template <typename ForwardIt>
1348 __bdd
1349 bdd_forall(bdd&& f, ForwardIt begin, ForwardIt end)
1350 {
1351 return bdd_forall(std::move(f), make_generator(begin, end));
1352 }
1353
1360 template <typename ForwardIt>
1361 __bdd
1362 bdd_forall(__bdd&& f, ForwardIt begin, ForwardIt end)
1363 {
1364 return bdd_forall(std::move(f), make_generator(begin, end));
1365 }
1366
1370 template <typename ForwardIt>
1371 __bdd
1372 bdd_forall(const exec_policy& ep, const bdd& f, ForwardIt begin, ForwardIt end)
1373 {
1374 return bdd_forall(ep, f, make_generator(begin, end));
1375 }
1376
1384 template <typename ForwardIt>
1385 __bdd
1386 bdd_forall(const exec_policy& ep, bdd&& f, ForwardIt begin, ForwardIt end)
1387 {
1388 return bdd_forall(ep, std::move(f), make_generator(begin, end));
1389 }
1390
1397 template <typename ForwardIt>
1398 __bdd
1399 bdd_forall(const exec_policy& ep, __bdd&& f, ForwardIt begin, ForwardIt end)
1400 {
1401 return bdd_forall(ep, std::move(f), make_generator(begin, end));
1402 }
1403
1405
1409
1423
1439 __bdd
1440 bdd_replace(const bdd& f,
1441 const function<bdd::label_type(bdd::label_type)>& m,
1442 replace_type m_type = replace_type::Auto);
1443
1445
1449 __bdd
1450 bdd_replace(const exec_policy& ep,
1451 const bdd& f,
1452 const function<bdd::label_type(bdd::label_type)>& m,
1453 replace_type m_type = replace_type::Auto);
1454
1471 __bdd
1472 bdd_replace(__bdd&& f,
1473 const function<bdd::label_type(bdd::label_type)>& m,
1474 replace_type m_type = replace_type::Auto);
1475
1479 __bdd
1480 bdd_replace(const exec_policy& ep,
1481 __bdd&& f,
1482 const function<bdd::label_type(bdd::label_type)>& m,
1483 replace_type m_type = replace_type::Auto);
1484
1486
1490
1502
1517 bdd
1518 bdd_relprod(const bdd& states, const bdd& relation, const predicate<bdd::label_type>& pred);
1519
1524 bdd
1525 bdd_relprod(const exec_policy& ep,
1526 const bdd& states,
1527 const bdd& relation,
1528 const predicate<bdd::label_type>& pred);
1530
1554 bdd
1555 bdd_relnext(const bdd& states,
1556 const bdd& relation,
1557 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1558 replace_type m_type = replace_type::Auto);
1559
1564 bdd
1565 bdd_relnext(const exec_policy& ep,
1566 const bdd& states,
1567 const bdd& relation,
1568 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1569 replace_type m_type = replace_type::Auto);
1571
1591 bdd
1592 bdd_relnext(const bdd& states, const bdd& relation, const bdd::label_type varcount);
1593
1599 bdd
1600 bdd_relnext(const exec_policy& ep,
1601 const bdd& states,
1602 const bdd& relation,
1603 const bdd::label_type varcount);
1605
1621 bdd
1622 bdd_relnext(const bdd& states, const bdd& relation);
1623
1629 bdd
1630 bdd_relnext(const exec_policy& ep, const bdd& states, const bdd& relation);
1632
1657 bdd
1658 bdd_relprev(const bdd& states,
1659 const bdd& relation,
1660 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1661 replace_type m_type = replace_type::Auto);
1662
1667 bdd
1668 bdd_relprev(const exec_policy& ep,
1669 const bdd& states,
1670 const bdd& relation,
1671 const function<optional<bdd::label_type>(bdd::label_type)>& m,
1672 replace_type m_type = replace_type::Auto);
1674
1694 bdd
1695 bdd_relprev(const bdd& states, const bdd& relation, const bdd::label_type varcount);
1696
1702 bdd
1703 bdd_relprev(const exec_policy& ep,
1704 const bdd& states,
1705 const bdd& relation,
1706 const bdd::label_type varcount);
1708
1723 bdd
1724 bdd_relprev(const bdd& states, const bdd& relation);
1725
1731 bdd
1732 bdd_relprev(const exec_policy& ep, const bdd& states, const bdd& relation);
1734
1738
1750
1756 bool
1757 bdd_iscanonical(const bdd& f);
1758
1764 bool
1765 bdd_isconst(const bdd& f);
1766
1772 bool
1773 bdd_isterminal(const bdd& f);
1774
1784 bool
1785 bdd_isfalse(const bdd& f);
1786
1790 bool
1791 bdd_istrue(const bdd& f);
1792
1800 bool
1801 bdd_isvar(const bdd& f);
1802
1810 bool
1811 bdd_isithvar(const bdd& f);
1812
1820 bool
1821 bdd_isnithvar(const bdd& f);
1822
1828 bool
1829 bdd_iscube(const bdd& f);
1830
1838 bool
1839 bdd_equal(const bdd& f, const bdd& g);
1840
1845 bool
1846 bdd_equal(const exec_policy&, const bdd& f, const bdd& g);
1848
1852 bool
1853 operator==(const bdd& f, const bdd& g);
1854
1856 bool
1857 operator==(__bdd&& f, const bdd& g);
1858 bool
1859 operator==(const bdd& f, __bdd&& g);
1860 bool
1861 operator==(__bdd&& f, __bdd&& g);
1863
1873 bool
1874 bdd_unequal(const bdd& f, const bdd& g);
1875
1880 bool
1881 bdd_unequal(const exec_policy& ep, const bdd& f, const bdd& g);
1883
1887 bool
1888 operator!=(const bdd& f, const bdd& g);
1889
1891 bool
1892 operator!=(const bdd& f, __bdd&& g);
1893 bool
1894 operator!=(__bdd&& f, const bdd& g);
1895 bool
1896 operator!=(__bdd&& f, __bdd&& g);
1898
1902
1914
1918 size_t
1919 bdd_nodecount(const bdd& f);
1920
1925 bdd::label_type
1926 bdd_varcount(const bdd& f);
1927
1933 uint64_t
1934 bdd_pathcount(const bdd& f);
1935
1940 uint64_t
1941 bdd_pathcount(const exec_policy& ep, const bdd& f);
1943
1958 uint64_t
1959 bdd_satcount(const bdd& f, bdd::label_type varcount);
1960
1965 uint64_t
1966 bdd_satcount(const exec_policy& ep, const bdd& f, bdd::label_type varcount);
1968
1977 uint64_t
1978 bdd_satcount(const bdd& f);
1979
1984 uint64_t
1985 bdd_satcount(const exec_policy& ep, const bdd& f);
1987
1991
2003
2014 void
2015 bdd_support(const bdd& f, const consumer<bdd::label_type>& cb);
2016
2029 template <typename OutputIt,
2030 typename = enable_if<!is_convertible<OutputIt, consumer<bdd::label_type>>>>
2031 OutputIt
2032 bdd_support(const bdd& f, OutputIt iter)
2033 {
2034 bdd_support(f, make_consumer<bdd::label_type>(iter));
2035 return iter;
2036 }
2037
2043 bdd::label_type
2044 bdd_topvar(const bdd& f);
2045
2051 bdd::label_type
2052 bdd_minvar(const bdd& f);
2053
2059 bdd::label_type
2060 bdd_maxvar(const bdd& f);
2061
2071 bdd
2072 bdd_satmin(const bdd& f);
2073
2089 bdd
2090 bdd_satmin(const bdd& f,
2091 const generator<bdd::label_type>& d,
2092 const size_t d_size = bdd::max_label + 1);
2093
2109 template <typename ForwardIt, typename = enable_if<is_const<typename ForwardIt::reference>>>
2110 bdd
2111 bdd_satmin(const bdd& f, ForwardIt cbegin, ForwardIt cend)
2112 {
2113 return bdd_satmin(f, make_generator(cbegin, cend), std::distance(cbegin, cend));
2114 }
2115
2130 bdd
2131 bdd_satmin(const bdd& f, const bdd& d);
2132
2143 void
2144 bdd_satmin(const bdd& f, const consumer<pair<bdd::label_type, bool>>& c);
2145
2157 template <typename OutputIt,
2158 typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>>
2159 && !is_convertible<OutputIt, bdd>>>
2160 OutputIt
2166
2179 bdd
2180 bdd_satmax(const bdd& f);
2181
2196 bdd
2197 bdd_satmax(const bdd& f,
2198 const generator<bdd::label_type>& d,
2199 const size_t d_size = bdd::max_label + 1);
2200
2216 template <typename ForwardIt, typename = enable_if<is_const<typename ForwardIt::reference>>>
2217 bdd
2218 bdd_satmax(const bdd& f, ForwardIt cbegin, ForwardIt cend)
2219 {
2220 return bdd_satmax(f, make_generator(cbegin, cend), std::distance(cbegin, cend));
2221 }
2222
2237 bdd
2238 bdd_satmax(const bdd& f, const bdd& d);
2239
2250 void
2251 bdd_satmax(const bdd& f, const consumer<pair<bdd::label_type, bool>>& c);
2252
2264 template <typename OutputIt,
2265 typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>>
2266 && !is_convertible<OutputIt, bdd>>>
2267 OutputIt
2273
2287 pair<bdd, double>
2288 bdd_optmin(const bdd& f, const cost<bdd::label_type>& c);
2289
2295 pair<bdd, double>
2296 bdd_optmin(const exec_policy& ep, const bdd& f, const cost<bdd::label_type>& c);
2298
2316 double
2317 bdd_optmin(const bdd& f,
2318 const cost<bdd::label_type>& c,
2319 const consumer<pair<bdd::label_type, bool>>& cb);
2320
2326 double
2327 bdd_optmin(const exec_policy& ep,
2328 const bdd& f,
2329 const cost<bdd::label_type>& c,
2330 const consumer<pair<bdd::label_type, bool>>& cb);
2332
2345 bool
2346 bdd_eval(const bdd& f, const predicate<bdd::label_type>& xs);
2347
2363 bool
2364 bdd_eval(const bdd& f, const generator<pair<bdd::label_type, bool>>& xs);
2365
2384 template <typename ForwardIt>
2385 bool
2386 bdd_eval(const bdd& f, ForwardIt begin, ForwardIt end)
2387 {
2388 return bdd_eval(f, make_generator(begin, end));
2389 }
2390
2394
2406
2420 __bdd
2421 bdd_from(const zdd& A, const generator<bdd::label_type>& dom);
2422
2428 __bdd
2429 bdd_from(const exec_policy& ep, const zdd& A, const generator<bdd::label_type>& dom);
2430
2432
2449 template <typename ForwardIt>
2450 __bdd
2451 bdd_from(const zdd& A, ForwardIt begin, ForwardIt end)
2452 {
2453 return bdd_from(A, make_generator(begin, end));
2454 }
2455
2461 template <typename ForwardIt>
2462 __bdd
2463 bdd_from(const exec_policy& ep, const zdd& A, ForwardIt begin, ForwardIt end)
2464 {
2465 return bdd_from(ep, A, make_generator(begin, end));
2466 }
2467
2469
2484 __bdd
2485 bdd_from(const zdd& A);
2486
2492 __bdd
2493 bdd_from(const exec_policy& ep, const zdd& A);
2495
2499
2511
2515 void
2516 bdd_printdot(const bdd& f, std::ostream& out = std::cout, bool include_id = false);
2517
2521 void
2522 bdd_printdot(const bdd& f, const std::string& file_name, bool include_id = false);
2523
2527}
2528
2529#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:59
adiar::exec_policy
Settings to dictate the execution of Adiar's algorithms.
Definition exec_policy.h:35
adiar::internal::dd::label_type
level_type label_type
Type of variable labels.
Definition dd.h:312
adiar::internal::dd::max_label
static constexpr label_type max_label
The maximal possible value for a unique identifier's label.
Definition dd.h:322
adiar::zdd
Reduced Ordered Zero-suppressed Decision Diagram.
Definition zdd.h:68
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