CVC4-TurnKey (GPL)

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

License

License

Categories

Categories

KeY Data Data Formats Formal Verification
GroupId

GroupId

io.github.tudo-aqua
ArtifactId

ArtifactId

cvc4-turnkey-gpl
Last Version

Last Version

1.8
Release Date

Release Date

Type

Type

pom.sha512
Description

Description

CVC4-TurnKey (GPL)
A self-unpacking, standalone CVC4 distribution that ships all required native support code and automatically unpacks it at runtime. GPL-licensed version.
Project URL

Project URL

https://github.com/tudo-aqua/cvc4-turnkey
Source Code Management

Source Code Management

https://github.com/tudo-aqua/cvc4-turnkey/tree/master

Download cvc4-turnkey-gpl

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.

Azure DevOps builds Maven Central Maven Central

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:

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

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

io.github.tudo-aqua

AQUA - Automated Quality Assurance

Versions

Version
1.8
1.7