adiar
adiar copied to clipboard
SSoelvsten
An I/O-efficient implementation of (Binary) Decision Diagrams
The `-` and `-=` operator `adiar::bdd` should be added as an overload for the `adiar::bdd_diff` function. Remember to add a test or two to ensure it works as intended.
Taking a look at [`std::copy`](https://en.cppreference.com/w/cpp/algorithm/copy), it is quite odd that we use a *first* and *last* iterator. In fact, we don't allow one to use `std::back_inserter(to_vector)` as is desired. -...
On the Grendel cluster, we have created a head-ache for the sysadmins by creating 175.000 concurrent files in the temporary folder (presumably model checking a system of about 20.000+ transitions)....
As a follow-up on #502 and the overloads in #682 , we should consider to make the creation of transitions even easier. **Add Frame-Rules to Relations** - [ ] Given...
The algorithms in this project are quite complex and their complexities are not at all similar to other BDD packages. Hence, we ought to make the time complexity much clearer...
Similar to #199 , we may want to investigate whether a *radix* sort on the keys can out-compete **Radix Sorting** - [ ] Solve parts of #445 such that there...
Smaller version of #199 , where we want to replace all usage of the `tpie` library with the C++ standard library, `std`. Here, we will accept the fact, that the...
Similar to #199 , we may want to investigate whether a *two-level* priority queue, i.e. one that is optimized both for the cache and the RAM, can squeeze out a...
With one of the optimisations in #502 , we end up adding some source-code copy by creating the `relnext_quantify_policy` which is a copy-paste of the regular BDD quantify policy (...
Metadata
Owner
Metadata
An I/O-efficient implementation of (Binary) Decision Diagrams