better alias support
Currently we can use Alias:
definitions in the HOA format, but those will be inlined on parsing, and they then completely disappear.
It would be nice if the parser could return the set of aliases used on input, and if print_hoa()
could use such a list to simplify its output. Even print_dot
could be taught to use aliases. A use case could be to encode an arbitrary alphabet Σ in binary over log(|Σ|) atomic propositions.
I suspect that we could have the parser export a vector<pair<bdd,string>>
, maybe by attaching it to the automaton, and that print_hoa()
and print_dot()
could use that to reintroduce aliases on export.
One question is how to output a bdd
that does not appear in that list of aliases, especially in presence of multiple overlapping aliases.
I would suggest that the aliases are stored in the reverse order of the order in which they were parsed, so that the more complex aliases (that may depend upon previous aliases) appear first, and that this order is used to decompose a BDD as a sum of aliases in a greedy way.