README

December 7, 2012 ยท View on GitHub

NSolv By Dan Liew.

ABOUT

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.

BUILDING 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 installed.

  • 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

  1. Now we'll launch your favourite CMake front-end. cd/path/to/nsolv/build/directorycd /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 again.

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

  1. 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

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

$ make

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

$ make install

  1. 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

USAGE

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".

REFERENCES [1] http://www.smt-lib.org [2] https://github.com/delcypher/klee/tree/smtlib [3] http://klee.llvm.org/

:set textwidth=80