Theta uses Java (JDK) 11 with Gradle 6 as a build system. Currently, we use OpenJDK 11 (see instructions for Windows and Ubuntu). We are developing Theta both on Linux and Windows. Currently, floating point types are only fully supported on Linux. Windows support is experimental and can cause cryptic exceptions to occur in native code. Theta can be built from the command line, but you can also import it into IntelliJ IDEA. Unfortunately, Eclipse does not support Gradle projects with Kotlin build scripts (yet).
Theta has some external dependencies that may need to be obtained/installed depending on what parts of the framework you are working with.
Z3 SMT Solver:
The libraries for the Z3 solver (version 4.5.0) are included in the lib directory, both for Windows and Ubuntu (64 bit).
However, on Windows, libz3.dll also requires some libraries from the Microsoft Visual C++ Redistributable package that we could not include due to licensing.
Install it, or just execute Download-VCredist.ps1, which will download the required libraries.
If you have a different OS, you should download the appropriate Z3 binary for version 4.5.0.
These libraries should be available on PATH for the executable tools.
Troubleshooting:
- If Z3 gives an assertion error (unreachable code reached), your Z3 version may not be correct.
GraphViz:
Theta can export graphs in dot format and automatically convert them to images.
For this, GraphViz has to be installed and dot (or dot.exe on Windows) has to be on the PATH.
Theta can be built from the command line by simply executing gradlew.bat build (Windows) or ./gradlew build (Linux) from the root of the repository, where build is the name of the task that will compile all projects and run the tests.
On Linux make sure you do not use gradle build as it executes your globally installed Gradle tool which might not be the appropriate version.