CVC4-TurnKey (Permissive)

A self-unpacking, standalone CVC4 distribution that ships all required native support code and automatically unpacks it at runtime. Permissive-licensed version.

License	The 3-Clause BSD License GNU Lesser General Public License, Version 3 The PostgreSQL Licence The MIT License ISC License
Categories	KeY Data Data Formats Formal Verification
GroupId	io.github.tudo-aqua
ArtifactId	cvc4-turnkey-permissive
Last Version	1.8
Release Date	Oct 22, 2020
Type	pom.sha512
Description	CVC4-TurnKey (Permissive) A self-unpacking, standalone CVC4 distribution that ships all required native support code and automatically unpacks it at runtime. Permissive-licensed version.
Project URL	https://github.com/tudo-aqua/cvc4-turnkey
Source Code Management	https://github.com/tudo-aqua/cvc4-turnkey/tree/master

Download cvc4-turnkey-permissive

Filename	Size
cvc4-turnkey-permissive-1.8.pom
cvc4-turnkey-permissive-1.8-sources.jar	26 MB
cvc4-turnkey-permissive-1.8-javadoc.jar	1 MB

Dependencies

There are no dependencies for this project. It is a standalone project that does not depend on any other jars.

Project Modules

There are no modules declared in this project.

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.

AQUA - Automated Quality Assurance

Versions

Version
1.8 Oct 22, 2020
1.7 Mar 5, 2020