Enable fully symbolic network reduction

[daemontus]

This PR should finally enable fully symbolic network reduction at the level of SymbolicAsyncGraph.

Specifically:

• FnUpdate::to_string can now skip parenthesis around nested and/or functions, meaning the output is more readable, especially in witness networks (e.g. a & b & (a | c | d) instead of ((a & b) & ((a | c) | d)).
• Added FnUpdate::mk_conjunction and FnUpdate::mk_disjunction that can be used to create update functions using n-ary operators. This also simplifies FnUpdate::build_from_bdd.
• Added Space::new_raw which takes the number of variables instead of the whole network.
• [breaking] SymbolicAsyncGraph::new and other variants now only need a reference to a Boolean network, since the network is no longer a required part of the structure (although in most cases, it is simply copied).
• [breaking] SymbolicAsyncGraph::empty_vertices and SymbolicAsyncGraph::mk_empty_vertices renamed to empty_colored_vertices. This was a typo and we should have done this a long time ago.
• Added proper SymbolicAsyncGraph::unit_vertices and SymbolicAsyncGraph::empty_vertices methods.
• [breaking] SymbolicAsyncGraph::as_network now returns Option<BooleanNetwork>. The code that was using the underlying network was rewritten to use one of the new utility methods instead. With that said...
• Added a bunch of utility methods to SymbolicAsyncGraph and SymbolicContext for managing VariableId objects without the underlying BooleanNetwork (namely SymbolicContext::find_network_variable, SymbolicContext::get_network_variable_name, SymbolicContext::network_variables, SymbolicContext::find_state_variable, SymbolicAsyncGraph::get_symbolic_fn_update, SymbolicAsyncGraph::get_variable_name, SymbolicAsyncGraph::num_vars, and SymbolicAsyncGraph::variables).
• Added SymbolicContext::eliminate_variable which is used by the reduction.
• Added SymbolicContext::mk_instantiated_fn_update which is a utility function used by witness generation and projected iteration.
• Added SymbolicAsyncGraph::new_raw which can be used to create a graph from BDDs, without the underlying Boolean network.
• Added SymbolicAsyncGraph::inline_symbolic, which implements the actual variable inlining.

[codecov[bot]]

Codecov Report

Attention: 45 lines in your changes are missing coverage. Please review.

Comparison is base (1070fc3) 80.26% compared to head (e72e4b1) 80.04%.

Files	Patch %	Lines
...symbolic_async_graph/_impl_symbolic_async_graph.rs	81.06%	25 Missing :warning:
...sync_graph/_impl_symbolic_async_graph_operators.rs	66.66%	16 Missing :warning:
src/_impl_fn_update.rs	96.07%	2 Missing :warning:
src/symbolic_async_graph/_impl_symbolic_context.rs	90.90%	2 Missing :warning:

Additional details and impacted files

```diff @@ Coverage Diff @@ ## master #53 +/- ## ========================================== - Coverage 80.26% 80.04% -0.23% ========================================== Files 71 71 Lines 4744 4800 +56 ========================================== + Hits 3808 3842 +34 - Misses 936 958 +22 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.