The CVC4-TurnKey distribution

The CVC4 Theorem Prover is a widely used SMT solver that is written in C and C++, wrapping a large number of open source sub-solvers and libraries. The authors provide a Java API, however, it is not trivial to set up in a Java project. This project aims to solve this issue.

Why?

Similar to Z3-TurnKey, usage of CVC4 would be simplified by distributing a Java artifact that

1. ships its own native libraries,
2. can use them without administrative privileges, and
3. can be obtained using Maven.

How?

This project consists of two parts:

1. a Java loader, CVC4Loader, that handles runtime unpacking and linking of the native support libraries, and
2. a build system that creates a JAR from our unofficial CVC4 distributions that
   1. contains all native support libraries built by us (at the moment, Linux and Mac OS),
   2. introduced a call to CVC4Loader by rewriting the generated source code, and
   3. bundles all of the required files. Also, JavaDoc and source JARs are generated for ease of use.

Building

The project is built using Gradle. In addition to Java 11 or higher, building a GPG signature key.

The project can be built and tested on the current platform using:

./gradlew assemble integrationTest

Signing

Normally, Gradle will enforce a GPG signature on the artifacts. By setting the project parameter skip-signing, enforcement is disabled:

./gradlew -Pskip-signing assemble

License

CVC4 combines multiple software projects under different licenses:

• CVC4, its ANTLR support code and CmakeCoverage.cmage are available under the BSD 3-Clause License.
• MiniSat and BVMiniSat (parts of the CVC4 source tree) are available under the MIT License.
• ABC is available under the PostgreSQL License and is statically linked.
• CaDiCal is available under the MIT License and is statically linked.
• CryptoMiniSat 5 is available under the MIT License and is statically linked.
• drat2er is available under the MIT License and is statically linked.
• GMP is available under the GNU Lesser General Public License, Version 3 and is statically linked. Make sure to comply with the license terms when using the resulting binary.
• LFSC is available under the BSD 3-Clause License.
• SymFPU's CVC4 branch is available under the BSD 3-Clause License.

The GPL build also incorporates the following libraries, which require the binary and its consumers to adopt the GPL license on publication:

• CLN is available under the GNU General Public License (without version constraints) and is statically linked.
• glpk-cut-log is available under the GNU General Public License, Version 3 and is statically linked.

The support files in this project are licensed under the ISC License.