Support storing and reading ASCII format for BDDs

[SSoelvsten]

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

.<option> <value>

Possible options are:	option	name	count	order
type	string	uint	"pre", "post"

This is then followed by a set of nodes, starting with

.nodes

• Terminals are given with the t key and are of the form.

  t "type" "value"

• Nodes are of the form

  b <label> '-'?<then> '-'?<else>

  where then is also known as high and else is also known as low. The optional '-' character marks an edge to be complemented, which depends on the attributed edge feature. Every node is identified by referencing its linenumber or the name of another bdd in the same file.

Finally, the list is ended with

.end

Parsing a file

This feature might be blocked until we support attributed edges.

The simplest way to implement this would be to do the following:

1. Read the entire bdd from a file and push it as edges { source_line, target_line } to a tpie::merge_sorter.
2. Run a bottom-up version of Reduce that merely puts it into the normal node based form.

By use of a b-tree we could also store the id of all prior nodes and then that way skip the merge sorter. Most likely this will not run as fast as using the sorter. Furthermore, it also takes up much more space

The "reference another bdd" also makes things much more complicated. At that point one probably has to first check whether some reference like this exists to then "inline" the other BDD inside of this one and then run the actual Reduce algorithm.

Comments

Notice, while this is quite close to #126 , it also is quite disjoint (both in terms of how to do these and the usecase they are solving. The purpose of this is to have a common file format that can be used between different BDD packages, while the other is supposed to be used for Adiar alone by using the least amount of space.

[SSoelvsten]

I wonder whether the "every node is identified by referencing its linenumber" is not extremely tedious, since adding a node in the middle will result in having to shift all other numbers? Yet, otherwise it is pretty much just a condensed version of the blif format.

[SSoelvsten]

The corresponding issue on Tom's Sylvan repo is here: https://github.com/trolando/sylvan/issues/20

[SSoelvsten]

Alternatively, one can also investigate the lib-bdd format. A parser is implemented in https://github.com/SSoelvsten/bdd-benchmark/blob/main/src/apply.cpp. By making it use signed values, one can make it future-proof for complement edges.