Inox is a solver for higher-order functional programs which provides first-class support for features such as:
- Recursive and first-class functions
- ADTs, integers, bitvectors, strings, set-multiset-map abstractions
- Quantifiers
- ADT invariants
Interfacing with the solver can take place through the Scala API by constructing the AST corresponding to the query of interest and then feeding it to one of the solvers. See the tutorial and API for more information.
Alternatively, one can use Inox through command-line by using the TIP format to describe the relevant query.
Inox is probably easiest to build on Linux-like platforms, but read on regarding other platforms.
Due to its nature, this documentation section may not always be up to date; we welcome pull requests with carefully written and tested improvements to the information below.
Requirements:
- Java SE Development Kit 8 or Java SE Development Kit 7 for your platform
- SBT 0.13.x (Available from https://www.scala-sbt.org/)
- Git and svn executables
Get the sources of Inox by cloning the official Inox repository:
$ git clone https://github.com/epfl-lara/inox.git
Cloning into 'inox'...
// ...
$ cd inox
$ sbt clean compile
// takes about 1 minutes
Inox compilation generates an inox bash script that runs Inox with all
the appropriate settings. This script expects argument files in the
TIP input format and will report SAT or UNSAT
to the specified properties.
See ./inox --help for more information about script usage.
Not yet tested!
Get the sources of Inox by cloning the official Inox repository. You will need a Git shell for windows, e.g. Git for Windows.
$ git clone https://github.com/epfl-lara/inox.git
Cloning into 'inox'...
// ...
$ cd inox
$ sbt clean compile
// takes about 1 minutes
You will now need to either port the bash inox script to Windows, or run it
under Cygwin.
Known issues
The default solver underlying Inox (nativez3) ships with a wrapped native library.
See the ScalaZ3 repository for tips on getting
the solver running on Windows. Alternatively, one can use the
Princess solver
(command-line option --solvers=princess) to get a full JVM stack experience that
should work out of the box.
You may be able to obtain additional tips on getting Inox to work on Windows from Mikael Mayer or on his dedicated web page,
Inox typically relies on external (SMT) solvers to solve the constraints it generates.
We currently support two major SMT solvers:
Solver binaries that you install should match your operating
system and your architecture. We recommend that you install
these solvers as a binary and have their binaries available
in the $PATH. Once they are installed, you can instruct
Inox to use a given sequence of solvers. The more solvers
you have installed, the more successful Inox might get,
because solver capabilities are incomparable.
In addition to these external binaries, a native Z3 API for Linux is bundled with Inox and should work out of the box (although having an external Z3 binary is a good idea in any case). For other platforms you will have to recompile the native Z3 communication layer yourself; see the section below. Inox also bundles a JVM SMT solver Princess which should work out of the box on any system.
As of now the default solver is the native Z3 API, you will
have to explicitly specify another solver if this native
layer is not available to you, e.g., by giving the option
--solvers=smt-cvc4 to use CVC4. Check the --solvers
line in Inox' help.
The main reason for using the Z3 API is that it is currently faster when there are many calls to the solver. See the ScalaZ3 repository for information about how to build and package the project. You will then need to copy the resulting jar into the "unmanaged" directory.
Inox comes with a test suite. Consider running the following commands to invoke different test suites:
$ sbt test
$ sbt it:test