Michaël Cadilhac <michael@cadilhac.name> writes:
I guess my question is: If you had to go from scratch today, which BDD library would you use?
I'd consider either CUDD or Sylvan. Having transitions labeled by BDDs from BuDDy is currently what prevents Spot from supporting multithreaded algorithms easily. Having the global in a class, like CUDD or what you did, would at least allow to run independent BDD computations in parallel. Also there are some algorithms in Spot that would benefit from using ZDDs instead of BDDs. Getting rid of BuDDy has been a wish for a very long time, but it's just so pervasive in Spot that it would take a lot work. Also note that the version of BuDDy distributed with Spot has also diverged a lot from the "upstream" BuDDy. I reduced the memory footprint of the BDD nodes to improve caching, derecursived several algorithms to reduce stack overflows, and introduced a few algorithms needed by Spot (e.g. the development version of Spot now has a way to iterate over all minterms of a BDD that is much faster than what we used to do before). These small improvements are easier to do than getting rid of BuDDy :-( Best,