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 direclty on top of Z3.

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:

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