better AIGER format support for model checking
This could be the subject of an internship.
We should improve our support of the AIGER format by:
- supporting the binary version of the format for input or output
- either making class
aig
a subclass oftwa
with support for on-the-fly iteration, or providing aas_otf_automaton()
method. (Currentlyas_automaton()
builds an explicit automaton, but that might be very large.)
This way we can use large aig instances as models for model checking benchmars.