As a user of Rosette, the biggest solver performance improvement I ever achieved came from building a portfolio solver that wraps over Rosette and runs multiple solvers in parallel. I think Rosette would be made much more powerful by building a user-friendly portfolio solver directly into the language. Here is my proposal for how this would work.

The portfolio solver would simply be another solver instance, implementing the solver interface as with the other Rosette solvers. To construct a portfolio solver, you pass a list of solvers. In general, we would implement each solver method for the portfolio solver by simply calling the equivalent method for each solver in the portfolio. So, for example, implementing solver-assert for the portfolio solver simply involves looping over all solvers in the portfolio and calling their appropriate solver-assert.

It's worth elaborating on one method specifically: solver-check. Most of the other methods that interact with the solver should be "non-blocking" to some degree, ie we don't expect to have to wait long for a response from the solver. Furthermore, for each of the other methods, we'll need the command to terminate in each solver (e.g. for solver-assert, we truly need the assert to be pushed on to each solver's stack). However, solver-check (and solver-debug) (1) may take varying lengths of time in each solver, and (2) we don't actually need each solver to terminate, just one of them. Thus, solver-check's implementation will be a bit more interesting. I suspect it will work like this:

• First, we should ensure that each solver server is running in a separate thread. I think this likely happens at server startup time, not at solver-check time.
• Call solver-check for each solver.
• Monitor each solver process.
• As soon as the first one terminates, return its result and stop the other solvers.

The one complication with the above proposed implementation of solver-check is that it potentially breaks incremental solving. For example, imagine we have a portfolio of cvc5 and bitwuzla, and the user has the following interactions:

1. User pushes assertions. Portfolio solver pushes them onto both the cvc5 and bitwuzla assertion stacks.
2. User calls solver-check. Portfolio solver runs both solvers, and cvc5 returns first. Portfolio solver stops the bitwuzla solve.
3. User pushes more assertions and again calls solver-check. At this point, we're in a weird state. If we stopped the bitwuzla solving process because cvc5 returned first, can we keep pushing assertions onto bitwuzla? I simply don't know enough about how incremental solvers work, and if they allow for termination of a solve without destroying all of the accumulated state.

All in all, I think a portfolio solver would not be difficult to build, but would be of massive utility to the average Rosette user.

cc @sorawee who I've talked about this with before. Looking for opinions on (1) whether this sounds like it'll work, (2) if there are any gotchas I should be aware of, and (3) if this is something Rosette maintainers would want in Rosette.

Subtasks:

• Documentation
• Tests
• Initial implementation