# ksmt

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

## Usage

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.

## Linearisations

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.

## How to build from source

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.

## Benchmarks

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{⇀}{x}{}_{1},\dots ,\stackrel{⇀}{x}{}_{n}\in {ℝ}^{d}:\underset{1\le i\le n}{\bigwedge }‖\stackrel{⇀}{x}{}_{i}{‖}_{\infty }\le 1\wedge \underset{1\le i2$

• nonlinear-ball*-in-ball64 are instances of this form: $\exists \stackrel{⇀}{x},\stackrel{⇀}{y}\in {ℝ}^{3}:‖\stackrel{⇀}{x}{‖}_{2}\le r\wedge ‖\stackrel{⇀}{y}{‖}_{2}\ge \sqrt{64}\wedge ‖\stackrel{⇀}{x}-\stackrel{⇀}{y}{‖}_{\infty }\le \genfrac{}{}{0.1ex}{}{1}{100}$