Use multiple solvers in qalpha

[edenfrenkel]

This defines a BasicSolver trait in solver/src/basics.rs, which allows making very basic check-sat queries which return a sat result together with a trace, an unsat result together with an unsat-core, or unknown. By abstracting this basic functionality it is possible to implement this trait for a single SolverConf, as well as for a vector of SolverConf's in two different ways, once as FallbackSolvers tried sequentially and second as ParallelSolvers tried in parallel. This is utilized in qalpha, which now uses ParallelSolvers for its inductiveness and safety checks by default, and is configurable to use FallbackSolvers instead via --fallback. The simulation queries in qalpha still use a single SolverConf, now abstracted behind the BasicSolver trait as well.

Solver cancellation has also been moved out of the inference code and made more generic, using the new BasicSolverCanceler trait and SolverCancelers struct, which aggregates multiple BasicSolverCanceler's and itself implements BasicSolverCanceler. This is used recursively to create hierarchical tree-like cancellation, where the cancellation of a node cancels all of its descendants. The idea is that functions should only cancel queries which they (perhaps recursively) launched and not assume anything about the behavior of their callers. When the result is bubbled up to those callers, they should cancel their queries according to their own desired behavior. This allows more general applicablity which is independent of the specific goals of any single use-case, (in this case qalpha, which cancels all solvers on the first sat result.)

Another change is that now transition queries parallelize over disjunctive transitions, with proper cancellation if a sat response is encountered.

[tchajed]

I left a bunch of comments, but it's mostly just code-style advice.

This PR would be a great candidate for benchmarking, so you might want to add some benchmarking on top of #142. If you already have some data on the performance impact of this change from your own benchmarking script please include that data in the PR description.

[edenfrenkel]

@tchajed When trying to factor out try_conf I realized I should probably just implement multi-solvers more generally using a solver trait, like you said. This turned out to be more tricky than expected, unless I reduced solver behavior to something very basic, which is now implemented in the BasicSolver trait in solver/src/basics.rs. This trait allows making very simple check_sat queries which return sat+trace, unsat+unsat-core, or unknown. I implemented this trait for a single SolverConf, as well as for a vector of SolverConf's twice, first as fallback solvers and second as parallel solvers. Solver cancellation has also been moved out of the inference code and made more generic.

Let me know what you think. I'll rebase and update the pull request description soon.

[tchajed]

I like the trait solution, that nicely abstracts over what we need in this case!

Can you update the PR description? Other than that (and the usual rebase onto main) this is ready to merge.

[edenfrenkel]

@tchajed updated and rebased