adiar
adiar copied to clipboard
SSoelvsten
An I/O-efficient implementation of (Binary) Decision Diagrams
There are some spicy invariants when using the `ptr_uint64` class; namely the *out_idx*, *flag*, and the need to use *essential(...)*. If we somehow can make a `source` type and `target`...
Where an MTBDDs ( #438 ) generalize BDDs for functions from binary inputs to a non-binary output, a *Multi-valued Decision Diagram* (MDD) [Kam98] generalizes it to functions from non-binary input...
Right now, Adiar only supports diagrams, where the terminals (leaves) have boolean values. Of course, one can already use this to express non-boolean values by having *b* BDDs to represent...
In all algorithms we have something akin to the following from *internal/quantify.h* ```cpp while (v.uid < t_seek) { v = in_nodes.pull(); } ``` We may as well just add a...
A problem in SAT solving is trusting the solver when it claims a formula to be *unsatisfiable*. To this end, the solver can create an *LRAT* (or just a *DRAT*)...
Currently, to get the *i-level* cut computations to work, we count the number of arcs to the *true* and the *false* terminal. Yet, if the arc is tainted, we know...
**Context** With #128 the sink arcs in an `arc_file` was split in two: the ones given in-order and the ones given out-of-order. This reduces the number of elements involved in...
We ought to move the *taint* flag from the `e.target().is_flagged()` into a separate `e.flags[REDUCE_FLAG::CUT_TAINT]`. This provides the basis for us to add many of the extensions. - For #433, we...
Some user's would like to build Adiar once and then install it. This way, you do not need to include it as a submodule to each of your projects (and...
Follow-up on #147 , #419 , and #225 : The *Restrict* and *Eval* function currently takes a `shared_file` as an input which is quite clunky. :warning: These will break when...
Metadata
Owner
Metadata
An I/O-efficient implementation of (Binary) Decision Diagrams