Build without Dd support

[volkm]

Fixes #590

• Introduce CMake options STORM_USE_CUDD/ STORM_USE_SYLVAN to disable Dd libraries, and use CMake flags STORM_HAVE_CUDD / STORM_HAVE_SYLVAN.
• Build only with Sylvan
• Build only with CUDD
• Build without any Dd library
• Extend CI tests to test different configurations -> separate PR

[volkm]

I need some input on how to best handle disabling Dd libraries. I see two options:

1. Disabling support completely by removing the template instantiations using ifdef. I started doing this in this PR, see this example.
2. Only disabling the calls to the Dd library in the InternalBdd etc. classes. A similar approach is used for e.g. the GurobiSolver.

The first version has the advantage that build times are reduced if the dependency is not available. We also get compile time errors if there are issues with the missing dependency. The disadvantage is that in case of no Dd library, we have to disable all parts using Symbolic representations because we cannot link against any Dd datastructure. An example is the AbstractModelchecker which has a default dummy Dd Representation even for Sparse models. Another example are the tests, which need to be explicitly removed in case of missing dependencies, see this example.

The second version has the advantage that we need fewer changes, because we only need to locally disable the functions. Compilation against the InternalX classes can still be done and the tests can for example simply be skipped, if the Dd library is unavailable. The disadvantage is that we still need to build all instantiations even though the library is not available and we might only see issues during runtime (when the exception is thrown) and not at build time.

[sjunges]

Hmm.

I think option 1 sound unreasonable right now, although the fact that this is unreasonable shows that we have too tightly integrated some parts of the code base with eachother, i.e., an abstract model checker should not need to know about Dd-based model checkers. That may, however, be another issue that is not related to the ability to not compile against a dd library.

I am not too worried about the overhead in compile times. That should be really minimal as these objects can and will be minimal. I am mostly concerned about the disability to figure out that things will not work out properly at compile time and the fact that we are compiling 100 different versions of our code.

[volkm]

Thanks for your opinion. I am also leaning towards the second option for now, because it is easier to integrate.

Trying out the first options definitely raised some interesting issues and we now know better what the possible pitfalls are. For now, I will start with compiling against dummy internal Dd libraries.

[volkm]

Building with only CUDD, with only Sylvan and without any DD library is now supported.

I will add a separate PR to check all the different configurations. I will try to have a weekly CI job which tests more "exotic" configurations instead of checking all configurations all the time.