Skip to content
Go to file

Latest commit


Git stats


Failed to load latest commit information.
Latest commit message
Commit time


NSolv By Dan Liew.


NSolv is a simple tool for POSIX compliant operating systems that allows several
SMTLIBv2 [1] solvers to be invoked in parallel (each solver is in its own
process). The tool can operate in one of two modes

* Performance Mode
The first solver to respond (sat|unsat) is considered to be the first
solver to return useful output and the other solvers are killed. After this the
output of this "first solver" is outputted to standard output.

* Logging Mode
The first solver to respond (sat|unsat) is considered to be the first
solver to return useful output. The other solvers are allowed to finish unless
they timeout. The results and runtime of all solvers are recorded to a log file.

NSolv is so named because it allows you to launch "N Solv(ers)".

Its original purpose was to act as front-end to several SMTLIBv2 solvers for a
modified version ([2]) of KLEE [3]. These changes made to KLEE will most likely
never be merged as work is currently being done to integrate SMT-LIBv2 solvers
via a library rather than executing an external application as is needed for 

NSolv uses CMake as its build system. Here are a few commands you can run to get
started. Nsolv has very few depencies but make sure have the following

* Boost libraries and development header files
* librt (Real time library)
* PThreads library
* Standard development tools (C++ Compiler, development header files, etc...)

1. This stage is optional but it is advised you do an out of source build. Pick
any directory you like to build NSolv in.

$ mkdir /path/to/nsolv/build/directory

2. Now we'll launch your favourite CMake front-end.
$ cd /path/to/nsolv/build/directory
$ cmake-gui /path/to/nsolv/source-code/directory

Now press configure. CMake should hopefully find all the dependencies. It will
report an error if there is a problem.

At this point you set the build type by setting CMAKE_BUILD_TYPE. You probably
either want "Release" or "Debug". If you set this variable press configure

Alternatively you could use ccmake or if you're brave just plain cmake.

3. Now generate your build system. Usually you just want to generate plain UNIX
makefiles. You can do this by pressing the "Generate" button in cmake-gui

4. You can now start the build process by running the following command in the
NSolv build directory.

$ make

5. If you wish to install (prefix is CMAKE_INSTALL_PREFIX)  run

$ make install

6. CMake doesn't provide an "uninstall" makefile target. When you run install
the list of installed files are put in a file called "install_manifest.txt" in
the root of your binary build folder.

To uninstall run

$ xargs rm < install_manifest.txt


See the help message
$ nsolv --help

NSolv supports using a configuration file which is the recommended way to use
it. An example configuration file can be found in "config/example.cfg".


:set textwidth=80


Nsolv - A front-end that allows multiple SMTLIBv2 compliant solvers to executed in parallel.




No packages published
You can’t perform that action at this time.