Provide a way to pool SymCC solver workers

[luxas]

Category

User level API features/changes

Describe the feature you'd like to request

When using LocalSolver, it would be nice to have a higher-level interface that keeps a set of worker threads of cvc5 running (possibly scaling the set of workers up and down dynamically as needed) in order to not have to spawn a new process every time SymCC needs to evaluate something. For example, to not have to spawn a process (expensive) on every new HTTP request (like I do here in this PoC)

Describe alternatives you've considered

None yet.

Additional context

No response

Is this something that you'd be interested in working on?

• 👋 I may be able to implement this feature request
• ⚠️ This feature might incur a breaking change

[shaobo-he-aws]

Good idea! I think a workaround we can do now is to collect the SMT scripts by using a buffer (e.g., the implementation of Vec<u8> of the Solver trait. An example is here). Then we can send the script to the pool of solvers using a queue.