Algorithms for fixed-points, feedback vertex sets and more

This PR is rather large, but it was created to avoid making an even larger PR later down the line... so, it's a win?

Highlights

There is now a "solver context" (similar to "symbolic context") that can be used to rewrite certain problems as Z3 queries.
There are new, more efficient algorithms for computing fixed points and "projected" fixed points using both symbolic and solver methods.
There is a new suite of algorithms for analysing the structure of cycles in the RegulatoryGraph. This includes feedback vertex sets, independent cycles (with variants restricted to induced subgraphs and desired cycle parity), but also cycle and SCC detection in general.

Detailed changelog:

CI changes:
- We use a single fixed version of Rust for testing to avoid breaking the workflows randomly with new clippy issues.
- We don't run the workflow on dev-* branches (but we still run it on pull requests). Please don't merge dev-* branches into master without a PR.
Project level changes:
- We now have a "flexible" dependency on lib-bdd (>=0.4.2, <1.0.0). If you make changes that depend on newer versions, you can increase the minimum 0.4.2 version, but overall this should ensure that newer versions of lib-bdd can be used without re-releasing lib-parm-bn.
- We now depend on z3. For now, this is a dynamic dependency (i.e. the binaries will look for z3.ddl or libz3.so or whatever is required on your system). However, if you build products using lib-parm-bn, consider linking to a static version of z3 to avoid runtime errors due to version incompatibility.
Additions to existing API:
- BooleanNetwork::try_from_file: Read a Boolean model from a file. Automatically detects the model format based on file extension (.sbml/.bnet/.aeon).
- BooleanNetwork::parameter_appears_in: Compute the set of variables whose update function (syntactically) depends on the given parameter.
- BooleanNetwork::inline_inputs: Transforms variables into parameters when it's safe to do. This is still a "best effort" implementation in that some information is lost (e.g. observability/monotonicity is very hard to interpret after the transformation). However, the SymbolicAsyncGraph if the simplified network should not miss any dynamics of the original network.
- FnUpdate::contains_parameter and FnUpdate::contains_variable: Check if a VariableId or ParameterId appears in this function (syntactically).
- FnUpdate::to_and_or_normal_form: Eliminate all Boolean operators except for conjunction, disjuction and negation (however, negation can still appear anywhere in the formula).
- FnUpdate::distribute_negation: Ensures negation is only applied to the literals of the formula (variables or function invocations).
- ParameterId and VariableId now have proper usize coversion methods (to_index and from_index). Keep in mind that with great power comes great responsibility (avoid them unless you really have to).
- RegulatoryGraph::components is now deprecated in favour of RegulatoryGraph::strongly_connected_components (which is a completely new algorithm).
- New or reimplemented methods for analysis of a RegulatoryGraph (see SdGraph below for details):
  - RegulatoryGraph::strongly_connected_components
  - RegulatoryGraph::restricted_strongly_connected_components
  - RegulatoryGraph::transitive_regulators
  - RegulatoryGraph::transitive_targets
  - RegulatoryGraph::shortest_cycle
  - RegulatoryGraph::shortest_parity_cycle
  - RegulatoryGraph::feedback_vertex_set
  - RegulatoryGraph::parity_feedback_vertex_set
  - RegulatoryGraph::independent_cycles
  - RegulatoryGraph::independent_parity_cycles
- FunctionTable::symbolic_variables for when you need all variables that are used to represent a single uninterpreted function.
- GraphColoredVertices::is_subspace, GraphColoredVertices::is_singleton, plus the same thing for GraphColors and GraphVertices: Check if the set is a singleton (one value) or a subspace (can be described by a single conjunction). *GraphColoredVertices::fix_network_variable, GraphColoredVertices::restrict_network_variable, the same for GraphVertices: Restrict/transform the set of values without requiring interaction with the SymbolicAsyncGraph.
- SymbolicAsyncGraph::fix_vertices_with_network_variable: The same as fix_network_variable, but the result is GraphVertices, not GraphColoredVertices, which can be faster if you don't care about colors.
- SymbolicAsyncGraph::wrap_in_subspace: Compute the smallest subspace that contains a set of graph vertices (for now, this does not work with colors).
- SymbolicasyncGraph::wrap_in_symbolic_subspace: Compute the smallest symbolic set that is a vertex hypercube but still contains all results. As this is a fully symbolic operations, it can also work with colors, but note that colors are not affected: i.e. the result is a subspace only in the state variables, not parameter variables.
- SymbolicAsyncGraph::is_trap_set: Test if the given symbolic set is a trap set.
- SymbolicAsyncGraph::restrict_variable_in_graph: Create a new SymbolicAsyncGraph that fixes the value of a certian varaible, but the erases it from the update functions. So the dynamics of the new graph are still valid in the subspace where the given variable is fixed (and possibly easier to analyse), but in general not all transitions are preserved outside of this subspace.
Completely new API:
- ExtendedBoolean is essentially the 1/0/* enum used to express the variable's value in a subspace:
  - The type implements an "overapproximated" Boolean algebra (negate/and/or/implies/...), such that you can evaluate Boolean expressions using ExtendedBoolean and get a valid result.
- Space represents a hypercube of states:
  - You can index Space using VariableId to retrieve/save values.
  - Spaces implement a partial order based on inclusion.
  - You can use the ExtendedBoolean algebra with FnUpdate::eval_in_space to use Space as an input to a Boolean function and get a valid result. This is then used in Space::is_trap_space to check if a space is a trap.
- SdGraph is a "cleaner" implementation of a "signed directed graph" on which we implement things like cycle detection (you can create it from a RegulatoryGraph and some new methods on RegulatoryGraph use it internally). Everything in here uses standard explicit graph algorithms, but should be fast enough on graphs with less than 1M nodes:
  - Find shortest cycles in the interaction graph: SdGraph::shortest_cycle_length and SdGraph::shortest_cycle.
  - Find shortest parity cycles (positive/negative): SdGraph::shortest_parity_cycle_length and SdGraph::shortest_parity_cycle.
  - Greedily find "small" feedback vertex set and parity feedback vertex set (optionally restricted to an induced subgraph): SdGraph::restricted_feedback_vertex_set and SdGraph::restricted_parity_feedback_vertex_set.
  - Greedily find "large" set of independent cycles and independent parity cycles (again, with an optional restriction): SdGraph::restricted_independent_cycles and SdGraph::restricted_independent_parity_cycles.
  - Compute forward/backward reachable vertices (with an optional restriction): SdGraph::forward_reachable, SdGraph::backward_reachable, SdGraph::restricted_forward_reachable, SdGraph::restricted_backward_reachable.
  - Compute strongly connected components: SdGraph::strongly_connected_components, SdGraph::restricted_strongly_connected_components.
  - Compute weakly connected components: SdGraph::weakly_connected_components, SdGraph::restricted_weakly_connected_components.
- There is the BnSolverContext object, which implements an encoding of a Boolean network into a format that Z3 solver will understand. This is modelled largely to act similar to the SymbolicContext object:
  - BnSolverContext::declare_state_variables: Declare a fresh batch of variables based on the variables of the underlying Boolean network.
  - BnSolverContext::get_variable_constructor, BnSolverContext::get_explicit_parameter_constructor, BnSolverContext::get_implicit_parameter_constructor: Obtain the internal Z3 objects which represent symbol constructors for the corresponding Boolean network constructs.
  - BnSolverContext::mk_empty_solver and BnSolverContext::mk_network_solver: Create a new solver with no constraints (just the constructors/declarations) and create a new solver which also contains all static network constraints (monotonicity, essentiality, etc.).
  - BnSolverContext::mk_var, BnSolverContext::mk_explicit_parameter, BnSolverContext::mk_explicit_const_parameter, BnSolverContext::mk_implicit_parameter, BnSolverContext::mk_implicit_const_parameter, BnSolverContext::mk_update_function, BnSolverContext::mk_space: Create Z3 formula literals that are satisfied by the corresponding Boolean network objects (you can then combine these using logical connectives).
  - BnSolverContext::translate_space and BnSolverContext::translate_update_function: The same as above, but you supply your own variable constructors (e.g. after obtaining them from declare_state_variables). This means the resulting literal corresponds to your solver variables, and not the implicit ones.
- BnSolver and BnSolverModel describe the collection of constraints to be solver and one particular satisfying result. For all Z3 objects, you can get the underlying "raw" z3 struct if you need more advanced features:
  - BnSolver::check and BnSolver::get_model: Basic things that a solver should do.
  - BnSolver::push and BnSolver::pop: Save/restore context.
  - BnSolver::assert_within_space, BnSolver::assert_not_within_space, BnSolver::assert_regulation_observability, BnSolver::assert_regulation_monotonicity, BnSolver::assert_function_observability, BnSolver::assert_function_monotonicity: A pre-defined way of stating that all results should be in some space, avoid some space, or satisfy static constraints on relationships between variables and/or function inputs.
  - If you wan't to add your own assertions, you can access the "raw" underlying solver.
  - BnSolverModel::get_symbolic_state, BnSolverModel::get_symbolic_colors, BnSolverModel::get_symbolic_model: Return a singleton symbolic set representing the underlying result.
  - BnSolverModel::get_state, BnSolverModel::get_bool, BnSolverModel::get_raw_state, BnSolverModel::get_space: A few other extra methods to retrieve more "low level" objects from the result. Note that depending on your assertions, not all may be valid or relevant.
- RawBnModelIterator is an iterator over all satisfying results of a particular solver. You can specify individual "enumeration terms" which will be used to distinguish unique outputs. By supplying your own enumeration terms, you can implement various projections and "views" of the result.
- The FixedPoints "god object" that unites several algorithms for computing network fixed-points under various circumstances.
  - FixedPoints::naive: A "baseline" symbolic algorithm (used mainly for correctness comparisons).
  - FixedPoints::symbolic, FixedPoints::symbolic_vertices and FixedPoints::symbolic_colors: Compute either all fixed-points (vertex-color pair), just vertices, or just colors. Uses a better symbolic algorithm than the "baseline" algorithm.
  - FixedPoints::symbolic_iterator: Uses the same symbolic algorithm as above, but you can specify a "max" BDD size, after which the algorithm will attempt to "fork" the computation into multiple results which will be returned separately. This way, the enumeration can take more time, but can often happen with a fraction of memory required by the full algorithm.
  - FixedPoints::solver_iterator, FixedPoints::solver_vertex_iterator, and FixedPoints::solver_color_iterator: The same as the symbolic variants, but uses Z3 to search for fixed-points. I.e. the first results are usually very fast, but can take a long time to enumerate everything. There are specific types for each iterator which internally rely on RawBnModelIterator (you can look at how they are implemented to build things like custom projections and views).
- We now have a bunch of binaries that work as "integration tests" (e.g. check_fixed_points) and "benchmarks" (e.g. bench_fixed_points_solver; see REAMDE.md for more details). But you can also use them as a template to quickly find the FVS, independent cycles or fixed-points of a simple network.

sybila / biodivine-lib-param-bn

Algorithms for fixed-points, feedback vertex sets and more #36

Highlights

Detailed changelog:

Codecov Report