Make new BDD library that supports parallelism, larger node tables and other types of decision diagrams

From #911 (comment 2749009) (point 8):

[...] Make a new implementation of (B)DD library. There are other libraries (like Sylvan) that allow larger node arrays, can perform parallel computations using more CPU cores, and have new types of decision diagrams that are much more efficient in terms of space (tagged-DDs that combine the best of BDDs and ZDDs, but also other decision diagrams that all have different reduction rules, ones that store the predicate and it's negation in the same node, and so on). This could still give a huge boost in performance. However, it would be a huge effort. Using Sylvan itself is tricky, as it is written in C. There is PJBDD, which is also inspired by Sylvan, written in Java, and has parallelism. It however lacks a lot of basics, like resizing the node array. Still, we could also consider contributing to PJBDD, rather than making something of our own. In any regard, this would be a huge implementation effort.

This could greatly improve the ability of data-based synthesis and controller properties checker to handle larger models.