• Alexandre Duret-Lutz's avatar
    Store membership to acceptance sets using bitsets, not BDDs. · 2c764fb3
    Alexandre Duret-Lutz authored
    This is a huge patch, that took over a month to complete.  The bit sets
    are currently restricted to what 'unsigned can store', but it should be
    easy to extend it to 'uint64_t' should we need it.
    
    * NEWS: Update.
    * src/tgba/acc.hh: New file.
    * src/tgbatest/acc.cc, src/tgbatest/acc.test: Test it.
    * src/tgba/tgbakvcomplement.cc, src/tgba/tgbakvcomplement.hh,
    src/tgba/tgbasgba.cc, src/tgba/tgbasgba.hh: Delete.  The KV
    complementation is too slow to be used in practice, and I somehow broke
    it during the conversion to bitsets.  The tgba->sgba conversion was only
    used for the KV complementation, and should be better redone on
    tgba_digraph_ptr should it be needed again.
    * src/bin/ltlcross.cc, src/dstarparse/dra2ba.cc,
    src/dstarparse/nsa2tgba.cc, src/graphtest/tgbagraph.cc,
    src/graphtest/tgbagraph.test, src/kripke/fairkripke.cc,
    src/kripke/fairkripke.hh, src/kripke/kripke.cc, src/kripke/kripke.hh,
    src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.h...
    2c764fb3
tgbagraph.hh 9.33 KB