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

[karmacoma-eth]

✅ Preliminary work confirmed the intuition, there are indeed solvers like yices and bitwuzla that consistently outperform z3.

✅ We have a Docker image (https://github.com/a16z/halmos/tree/main/packages/solvers) that ships with multiple competitive solvers, ready to be invoked.

Now we need the infrastructure to spawn solver processes, monitor them, kill them and return results to halmos. This way, halmos can remain "single solver", and just invoke the metasolver.

[karmacoma-eth]

❌ https://github.com/agra-uni-bremen/metaSMT is a project that sounds similar to what we need, but seems to take a strange approach by actually building the solvers?

For what we need, we can stay in the Python ecosystem

[karmacoma-eth]

Spec'ing out what we need:

• [x] discover at runtime the solvers available on the PATH
• [x] accept an smt2 file as a command line argument
• [x] spawn each supported solver in a subprocess
• [x] redirect the stdout and stderr of the subprocesses
• [x] monitor the subprocesses for termination
• [x] as soon as one returns sat/unsat (not error or unknown), kill the remaining solvers (maybe terminate() first, wait some grace period, then kill())
• [x] ☝️ implies a translation layer, we need to understand the output and termination codes of the various solvers
• [x] return the output of the winning solver in a way halmos understands (sat/unsat, counterexample, unsat core)
• [x] danger: we don't want orphan processes that can survive the tool (listening to signals and interrupting children? daemon processes? process groups? may need to restrict to POSIX or even linux only solution)
• [x] configuration options: we may want to support running multiple solver versions (e.g. yices-2.6.4 and yices-2.6.5) as if they were separate solvers, and we may also want to support running the same solver but with different options (e.g. bitwuzla and bitwuzla --abstraction or default cvc5 and cvc5 with int blasting)

[karmacoma-eth]

more motivation: https://karmacoma.notion.site/halmos-multicore-processing-6b485bf455c9496c93d4c96872950154