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

- 2019-10-27: v0.1.7: source, statically linked x86_64 binary for Linux, README
- 2019-05-07: v0.1.6: source, statically linked x86_64 binary for Linux, README
- 2019-04-13: v0.1.5: source, statically linked x86_64 binary for Linux, README
- 2019-04-10: v0.1.4: source, statically linked x86_64 binary for Linux, README
- 2019-01-25: v0.1.3:
source,
statically linked x86_64 binary for Linux
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:

`kepler.sh`is a script creating instances of this form: $\exists \stackrel{\rightharpoonup}{x}{}_{1},\dots ,\stackrel{\rightharpoonup}{x}{}_{n}\in {\mathbb{R}}^{d}:\underset{1\le i\le n}{\bigwedge}\Vert \stackrel{\rightharpoonup}{x}{}_{i}{\Vert}_{\infty}\le 1\wedge \underset{1\le i<j\le n}{\bigwedge}\Vert \stackrel{\rightharpoonup}{x}{}_{i}-\stackrel{\rightharpoonup}{x}{}_{j}{\Vert}_{2}>2$`nonlinear-ball*-in-ball64`are instances of this form: $\exists \stackrel{\rightharpoonup}{x},\stackrel{\rightharpoonup}{y}\in {\mathbb{R}}^{3}:\Vert \stackrel{\rightharpoonup}{x}{\Vert}_{2}\le r\wedge \Vert \stackrel{\rightharpoonup}{y}{\Vert}_{2}\ge \sqrt{64}\wedge \Vert \stackrel{\rightharpoonup}{x}-\stackrel{\rightharpoonup}{y}{\Vert}_{\infty}\le {\textstyle \genfrac{}{}{0.1ex}{}{1}{100}}$