Extended symbolic domain

[daemontus]

This PR should mostly generalise the work completed as part of dev-hctl by @ondrej33, such that the resulting SymbolicContext can be also used for other applications that assume multiple BDD variables associated to every network variable.

Overall, there shouldn't be any breaking changes, however, there is a minor adjustment to how symbolic set operations are implemented which I wanted to do for quite some time.

• There is a new constructor SymbolicContext::with_extra_state_variables, which you can use to create a symbolic context with an arbitrary number of extra BDD variables.
• To access these extra variables, you can use SymbolicContext::all_extra_state_variables, SymbolicContext::extra_state_variables, SymbolicContext::extra_state_variables_by_offset, SymbolicContext::get_extra_state_variable, and SymbolicContext::mk_extra_state_variable_is_true.
• Just in case you need it, there is now also SymbolicContext::num_state_variables, SymbolicContext::num_parameter_variables, and SymbolicContext::num_extra_state_variables.
• Similarly, there is a new constructor SymbolicAsyncGraph::with_custom_context that you can use to create a graph with a specific context and "unit" symbolic universe. There are several caveats as to how the SymbolicAsyncGraph can break if you mix the extra symbolic variables into the existing data structures, but as long as you use them outside of the SymbolicAsyncGraph API, you should be fine.
• There is SymbolicAsyncGraph::existential_extra_variable_projection and SymbolicAsyncGraph::universal_extra_variable_projection which project a symbolic set that uses extra state variables onto a normal set that is guaranteed to be compatible with this symbolic graph.
• Computation of approx_cardinality and exact_cardinality has been adjusted to account for extra symbolic variables.
• Finally, there is a new trait called BddSet which now provides default implementations for most common symbolic operations (including the whole Set trait). This removes a lot of redundant code, but some of the old methods are still included to avoid breaking compatibility. Later, we should deprecate them and remove them from the library.

[daemontus]

@ondrej33: Can you please review this PR to check that it is indeed sufficient for your implementation of the HCTL model checker? (Also, feel free to merge it after the review, so that you are the one who commits it to master and thus appears in the list of contributors ;))

[codecov[bot]]

Codecov Report

Base: 76.64% // Head: 76.90% // Increases project coverage by +0.25% :tada:

Coverage data is based on head (1687a62) compared to base (d23032d). Patch coverage: 74.10% of modified lines in pull request are covered.

Additional details and impacted files

```diff @@ Coverage Diff @@ ## master #39 +/- ## ========================================== + Coverage 76.64% 76.90% +0.25% ========================================== Files 71 72 +1 Lines 4059 4113 +54 ========================================== + Hits 3111 3163 +52 - Misses 948 950 +2 ``` | [Impacted Files](https://codecov.io/gh/sybila/biodivine-lib-param-bn/pull/39?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=sybila) | Coverage Δ | | |---|---|---| | [src/symbolic\_async\_graph/bdd\_set.rs](https://codecov.io/gh/sybila/biodivine-lib-param-bn/pull/39/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=sybila#diff-c3JjL3N5bWJvbGljX2FzeW5jX2dyYXBoL2JkZF9zZXQucnM=) | `45.83% <45.83%> (ø)` | | | [src/symbolic\_async\_graph/\_impl\_symbolic\_context.rs](https://codecov.io/gh/sybila/biodivine-lib-param-bn/pull/39/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=sybila#diff-c3JjL3N5bWJvbGljX2FzeW5jX2dyYXBoL19pbXBsX3N5bWJvbGljX2NvbnRleHQucnM=) | `85.71% <77.50%> (-2.86%)` | :arrow_down: | | [src/symbolic\_async\_graph/\_impl\_graph\_colors.rs](https://codecov.io/gh/sybila/biodivine-lib-param-bn/pull/39/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=sybila#diff-c3JjL3N5bWJvbGljX2FzeW5jX2dyYXBoL19pbXBsX2dyYXBoX2NvbG9ycy5ycw==) | `56.41% <77.77%> (+6.41%)` | :arrow_up: | | [src/symbolic\_async\_graph/\_impl\_graph\_vertices.rs](https://codecov.io/gh/sybila/biodivine-lib-param-bn/pull/39/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=sybila#diff-c3JjL3N5bWJvbGljX2FzeW5jX2dyYXBoL19pbXBsX2dyYXBoX3ZlcnRpY2VzLnJz) | `53.22% <77.77%> (+6.74%)` | :arrow_up: | | [...mbolic\_async\_graph/\_impl\_graph\_colored\_vertices.rs](https://codecov.io/gh/sybila/biodivine-lib-param-bn/pull/39/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=sybila#diff-c3JjL3N5bWJvbGljX2FzeW5jX2dyYXBoL19pbXBsX2dyYXBoX2NvbG9yZWRfdmVydGljZXMucnM=) | `57.89% <80.00%> (-1.79%)` | :arrow_down: | | [...symbolic\_async\_graph/\_impl\_symbolic\_async\_graph.rs](https://codecov.io/gh/sybila/biodivine-lib-param-bn/pull/39/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=sybila#diff-c3JjL3N5bWJvbGljX2FzeW5jX2dyYXBoL19pbXBsX3N5bWJvbGljX2FzeW5jX2dyYXBoLnJz) | `81.69% <95.00%> (+3.05%)` | :arrow_up: | Help us with your feedback. Take ten seconds to tell us [how you rate us](https://about.codecov.io/nps?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=sybila). Have a feature suggestion? [Share it here.](https://app.codecov.io/gh/feedback/?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=sybila)

:umbrella: View full report at Codecov.
:loudspeaker: Do you have feedback about the report comment? Let us know in this issue.