Opening this issue for if anyone has some comment on this.
Currently Sylvan writes and reads BDDs in a somewhat awkward binary file format. While this is nice for parsing, it's unreadable and tricky to figure out what exactly is going on. Essentially, what Sylvan does is it simply collects all BDDs to write, then renumbers them to consecutive IDs.
Maybe we should just abandon binary formats? A BDD is not THAT complicated anyhow, typically we could just represent an internal node as <id> <variable> <then-id> <then-complemented> <else-id> <else-complemented> and a leaf as <id> <type> <value> where the predefined types are 0 (integer), 1 (double), 2 (fraction) or something along those lines.
Opening this issue for if anyone has some comment on this.
Currently Sylvan writes and reads BDDs in a somewhat awkward binary file format. While this is nice for parsing, it's unreadable and tricky to figure out what exactly is going on. Essentially, what Sylvan does is it simply collects all BDDs to write, then renumbers them to consecutive IDs.
Maybe we should just abandon binary formats? A BDD is not THAT complicated anyhow, typically we could just represent an internal node as
<id> <variable> <then-id> <then-complemented> <else-id> <else-complemented>and a leaf as<id> <type> <value>where the predefined types are 0 (integer), 1 (double), 2 (fraction) or something along those lines.