Support for portfolio solving

[0xkarmacoma]

Problem

We currently only ever invoke Z3 to solve both path queries and assertion queries. This works well in general, but there is evidence in the literature that different heuristics can perform better on specific queries, so we can expect that some other solvers (e.g. yices, cvc, boolector, bitwuzla...) could potentially give results much sooner than Z3.

Solution

When we have a query, we should:

1. dump it to smtlib2 format on disk
2. invoke z3 and the other available solvers on it concurrently
3. as soon as we get a result from a solver (sat/unsat -- ignore unknown) we can cancel the other ones, they lost the race

Finer points

• I operate on the assumption that most path queries are fast, and assertion queries can get expensive, therefore this would only apply to assertion queries. But maybe that's wrong? Might be interesting to see if there's any benefit to applying this to potentially expensive path queries too, who knows

• We may also not want to cancel the other ones right away for research purposes, might be interesting to get some insight if some solvers are better on specific kinds/sizes or queries, or maybe there's one that consistently outperforms the others

• packaging and distributing solvers sounds tricky, we may want to rely on automatically discovering what solvers are available locally? We would be looking in the PATH for available well-known binaries and invoke them, which outsources installing/building them to developers, as least initially.