ksmt is an SMT solver for quantifier-free non-linear real arithmetic. The description of the calculus underlying the algorithm and of the class of functions supported by it can be found here (while arXiv processes the update after reviews of: https://arxiv.org/abs/1905.09227). (Best Paper at FroCoS 2019)
Authors: Franz Brauße (alias [AT] informatik.uni-trier.de where alias=brausse), Norbert Müller, Hubert Glesener
It is licensed under LGPL-3.
ksmt expects input (path via command-line parameter or alternatively on stdin) in the SMT-LIB v2.5 format.
$ ksmt [-OPTS] [INSTANCE.smt2]
Non-QF_NRA non-linear function symbols support is disabled by any (set-logic) command. This behaviour can be turned off by passing option -i set-logic.
ksmt makes use of Tangent Space Linearisations, a method to linearise a wide variety of non-linear functions with good approximation conditions based on Taylor models.
To build from source, recent versions of at least the library GMP (including its C++-wrapper gmpxx.h) including its respective header files is assumed to be present, as well as a recent C++ compiler and GNU make. Features of newer releases rely on the presence of the libraries MPFR and iRRAM as well. Optionally, ksmt can make use of flint for faster rational arithmetic. See the respective README file for details.
On such a system it is enough to type
make
Support for transcendental functions requires a development version of iRRAM, an efficient implementation of the concepts from Computable Analysis in C++. It is to be found at https://github.com/fbrausse/iRRAM. To enable transcendental functions, compile using
make USE=iRRAM
If present, the minisat SAT-solver can be enabled by adding minisat to the string the USE variable is set to when building and by calling ksmt with the parameter -ssat=minisat. Flint is enabled in the build by including flint in the USE string.
To build from source, recent versions of the libraries GMP (including its C++-wrapper gmpxx.h), Flint, MPFR, Boost and iRRAM including their respective header files are assumed to be present, as well as a recent C++ compiler and GNU make. See the README file for details. Proceed with these commands:
$ git clone https://github.com/fbrausse/smtlib2parser.git
$ git clone https://github.com/fbrausse/ksat.git sat
$ git clone https://github.com/fbrausse/minisat.git
$ make ksmt
ksmt includes example instances for the following problems in the examples/nonlinear subdirectory of the source tree.
Benchmarks on some of these instances is provided in the tables below. Versions of the solvers compared against are: ksmt-0.1.3+flint-2.5.2+gmp, cvc4-1.6+gmp, z3-4.7.1+gmp, mathsat-5.5.2, yices-2.6+lpoly-1.7, dreal-3.16.08.01, rasat-0.3.
The first column for each solver refers to the respective output:
