SwInE

SwInE (SMT with Integer Exponentiation) is an SMT solver with support for integer exponentation. To handle integer exponentation, it uses counterexample-guided abstraction refinement. More precisely, it abstracts integer exponentiation with an uninterpreted function, inspects the models that are found by an underlying SMT solver with support for non-linear integer arithmetic and uninterpreted functions, and computes lemmas to eliminate those models if they violate the semantics of exponentiation.

There are two implementations of SwInE: The original implementation is built on top of SMT-Switch and uses the SMT solvers Z3 and CVC5 as backends. The more efficient re-implementation, called SwInE-Z3, is built directly on top of Z3.

News

This fork of SwInE features an implementation of a complete algorithm for a decidable fragment of integer arithmetic with exponentiation. It is based on the paper The complexity of Presburger arithmetic with power or powers by M. Benedikt, D. Chistikov, and A. Mansutti. We hope to merge it into the main development branch soon!
SwInE will be presented at the upcomming SMT workshop!

Downloading SwInE

Here you can find the latest releases of SwInE-Z3, including nightly releases. Here you can find the latest releases of the original implementation.

Input Format

SwInE supports an extension of the SMT-LIB format with an additional binary function symbol exp, whose arguments have to be of sort Int. Here you can find an example. Please use (set-logic ALL) to enable support for integer exponentiation.

The semantics of exp(s,t) is s^|t|.

Using SwInE

Please execute swine-z3 --help or swine --help, respectively, for detailed information on using SwInE.

Build

For SwInE-Z3, see here.

For the original implementation, proceed as follows:

think about using one of our releases instead
install Docker
go to the subdirectory scripts
execute ./build-container.sh to initialize the Docker container that is used for building SwInE
execute ./build.sh to build a statically linked binary (build/swine)
if you want to contribute to SwInE, execute ./qtcreator.sh to start a pre-configured IDE, which runs in a Docker container as well
if you experience any problems, contact florian.frohn [at] cs.rwth-aachen.de