cvc5 is a widely used SMT solver that is written in C and C++. The authors provide a Java API, however, it expects the user to install native libraries for their platform. This precludes easy usage of the solver as, e.g., a Maven dependency.
This project packages the cvc5 Java API and native libraries for all supported platforms as a TurnKey bundle. At runtime, the correct library for the platform is extracted and automatically loaded. The libraries themselves are modified to support this paradigm.
At the moment, platform support is as follows:
| Operating System | x86 | AMD64 | AARCH64 |
|---|---|---|---|
| Linux | ✓ | ||
| macOS | ✓ | ✓ | |
| Windows | ✓ |
The library can be included as a regular Maven dependency from the Maven Central repository. See the page for your version of choice there for configuration snippets for most build tools.
Building the library requires multiple native tools to be installed that can not be installed using Gradle:
- For library rewriting, see the tools required by the turnkey-gradle-plugin.
- Additionally, Python 3 is required for a code generation step and localized by the gradle-use-python-plugin.
The library requires Java 8. It can be used as a Java module on Java 9+ via the multi-release JAR
mechanism as the tools.aqua.turnkey.cvc5 module.
cvc5 itself is licensed under the 3-Clause BSD License and also incorporates components licensed under the MIT License and the GNU Lesser General Public License v3.0 or later. Two dependencies are introduced: the TurnKey support library is licensed under the ISC License and the JSpecify annotation library used by it is licensed under the Apache License, Version 2.0.
This does not bundle a GPL-licensed version of cvc5.
Tests and other non-runtime code are licensed under the Apache License, Version 2.0. Standalone documentation is licensed under the Creative Commons Attribution 4.0 International License.