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

[Tinelli, Cesare]

Dear Dan,

On 23 Nov 2012, at 19:48, Delcypher <delcypher at gmail.com> wrote:

> 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.
> 
Many thanks for making NSolv available to the community!

We have added it to the Utilities section of the SMT-LIB website.

Best,


Cesare


PS: Could you please use the official URL 

http://www.smt-lib.org/

for the SMT-LIB site in NSolv's documentation. 



> 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.
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib