adiar
adiar copied to clipboard
SSoelvsten
An I/O-efficient implementation of (Binary) Decision Diagrams
In most BDD packages, the quantification algorithm takes the domain also as a symbolic representation, i.e. as another BDD/ZDD. This is quite simple, since we already have the *generators* in...
Assuming the work to solve https://github.com/SSoelvsten/adiar/issues/462 indeed turns out to be of huge benefit, then we also want to extend this approach to the predicate algorithm. **Note:** This depends on...
TPIE handles possible errors by throwing [exceptions](https://github.com/thomasmoelhave/tpie/blob/776217b9e04682cf104d666b5f529dbdd86731f7/tpie/exception.h), In the case of running out of space on the disk, it throws an we internally catch the [tpie::out_of_space_exception](https://github.com/thomasmoelhave/tpie/blob/776217b9e04682cf104d666b5f529dbdd86731f7/tpie/exception.h#L54) . In this case,...
In [Coudert90] was proposed three functions, that are of interest for the field of verification. Based on BuDDy the three functions should be named and implemented as shown below: ###...
Whlie looking through the diff for #610 , I found the following missing coverage. These should be tested to be working as expected, similar to the other functions. **Tasks** -...
Currently we provide *generator* and *iterator* overloads for many algorithms. Yet, if possible we should also provide some *container*/*range* based input. For example, one would hope to write something like...
With #500 we have an asymptotically efficient (and hopefully in practice also great) way to compute the result of a different variable reordering. This we can use as the backbone...
The *ExactlyOne*, *AtMostOne*, and *AtLeastOne* are common formulas to build. As a follow-up on #82 , we should create simple *aliases*. - [ ] `bdd_exactly_one(vars)`: `bdd_counter(vars, 1)` - [ ]...
To help developers, we should allow the documentation to be compiled with internal stuff too. - [ ] Add `ADIAR_DOCS_INTERNAL` as a CMake option - [ ] Add *docs/internal* for...
## File Format Tom van Dijk has suggested the following format for a BDD: > Options are (optional) key-value pairs; each written on a single line as follows > ```...
Metadata
Owner
Metadata
An I/O-efficient implementation of (Binary) Decision Diagrams