[SMT-LIB] NSolv a tool for working with multiple SMT-LIBv2 solvers

[Delcypher]

Hi,

I'd like to announce a tool I've just released that I developed during
my project work this summer which some may find useful.

The tool is called NSolv and is essentially a simple program that can
invoke multiple SMT-LIBv2 solvers in parallel (each as a separate
process) on a single query. It can be used as a drop-in replacement
for a single SMT-LIBv2 solver.

It works in two modes...

* Performance mode. In this mode the response from the first solver to
return "sat" or "unsat" is used. All other solvers are stopped
(killed). This mode is useful for hacking together a portfolio of
solvers together that acts as a drop-in replacement for a single
solver.

* Logging mode. In this mode all solvers are allowed to finish and
their execution time is recorded. This is useful for benchmarking a
set of solvers.

NSolv only works on POSIX compliant operating systems. I've tested it
on Linux and seems to work fine. It is released under GNU GPLv3 and is
available at https://github.com/delcypher/nsolv

The current v1.0 release is available as a zip file at
https://github.com/delcypher/nsolv/archive/v1.0.zip

The solvers I have tested it with are CVC3, CVC4, MathSat5, SONOLAR,
STP and Z3 using the QF_AUFBV logic. NSolv doesn't do any input query
parsing so it should work with any query that the underlying solvers
support.

I'd like to request that the tool is added to the "Utilities" section
of the SMT-LIB website.

If anyone has any issues with the software then please contact me (I
might be able to fix it). Please do read the README file first though!

Thanks,
Dan Liew.