Portfolio solving with multiple solvers

[karmacoma-eth]

Is your feature request related to a problem? Please describe.

We currently use only z3 to solve both path conditions and assertions. Some solvers like cvc5, bitwuzla or boolector, etc. may give better results on some kinds of tests.

Describe the solution you'd like

Ideally we could validate the concept (do some solvers outperform z3 sometimes? consistently?) without fully productizing it.

We can currently invoke an external solver explicitly with --solver-subprocess --solver-subprocess-command COMMAND, so we could manually test with a few solvers on a few types of problems.

If it looks like that approach may be beneficial, then we can try to make it more automated, for instance like this:

• every time we need to solve an assertion, we dump the smt query to disk
• there is a daemon that watches the filesystem for new smt queries
• for every new query, it kicks off the available solvers in parallel
• it then watches for a solver giving a positive result (i.e. not just crashing, timing out or running out of memory), the positive result could be SAT (counterexample) or UNSAT (no counterexample)
• as soon as one solver wins the race with a positive results, it kills the other ones and returns the result to halmos

[karmacoma-eth]

started work on this