1.0.0

Initial release of Adiar!

BDD functions

• bdd class to hide away management of files and running the reduce algorithm. This takes care of reference counting and optimal garbage collection.

Constructors

• bdd_sink(bool v)
  or use the alternatives: bdd_true() and bdd_false()
• bdd_ithvar(label_t i)
• bdd_nithvar(label_t i)
• bdd_and(label_file ls)
  to construct an and chain.
• bdd_or(label_file ls)
  to construct an or chain.
• bdd_counter(label_t min_label, label_t max_label, label_t threshold)
  to construct whether exactly threshold many variables in the given interval are true.

Furthermore, the node_writer class is also provided as a means to construct a BDD manually bottom-up.

Basic Manipulation

• bdd_apply(bdd f, bdd g, bool_op op)
  to combine two BDDs with a binary operator (also includes aliases for every possible op)
• bdd_ite(bdd f, bdd g, bdd h)
  to compute the if-then-else
• bdd_not(bdd f)
  to negate a bdd
• bdd_restrict(bdd f, assignment_file as)
  to fix the value of one or more variables
• bdd_exists(bdd f, label_t i)
bdd_forall(bdd f, label_t i)
  to existentially or forall quantify a single variable. Overloading also allows quantifying multiple labels. But, these are still quantified one by one!

Counting Operations

• bdd_nodecount(bdd f)
  to obtain the number of (non-leaf) nodes.
• bdd_varcount(bdd f)
  the number of levels present (i.e. variables).
• bdd_pathcount(bdd f)
  the number of unique paths to the true sink.
• bdd_satcount(bdd f, size_t varcount)
  the number of satisfying assignments.

Other Functions

• bdd_eval(bdd f, assignment_file x)
  to compute f(x).
• bdd_satmin(bdd f), resp. bdd_satmax(bdd f)
  to find the lexicographical smallest, resp. largest, satisfying assignment.
• output_dot(bdd f, std::string filename)
  to output a visualizable .dot file.

Contributors

• Steffan Sølvsten( @SSoelvsten )
• Jaco van de Pol ( @jacopol )
• Anna Blume Jakobsen ( @AnnaBlume99 )
• Mathias Weller Berg Thomasen ( @MathiasWeller42 )

Thanks to the following people for helping with bugfixes and guidance on I/O algorithms, TPIE and C++.

• Asger Hautop Drewsen ( @tyilo )
• Lars Arge
• Mathias Rav ( @Mortal )

License

Adiar uses the TPIE library which is licensed under LGPL v3, and so by extension any binary file of Adiar is covered by the very same license.