initial version

tudo-aqua · Sep 21, 2024 · ecf3b7b · ecf3b7b
commit ecf3b7b
Show file tree

Hide file tree

Showing 24 changed files with 1,779 additions and 0 deletions.
diff --git a/.github/dependabot.yml b/.github/dependabot.yml
@@ -0,0 +1,26 @@
+#  SPDX-License-Identifier: Apache-2.0
+#
+#  Copyright 2019-2024 The TurnKey Authors
+#
+#  Licensed under the Apache License, Version 2.0 (the "License");
+#  you may not use this file except in compliance with the License.
+#  You may obtain a copy of the License at
+#
+#      http://www.apache.org/licenses/LICENSE-2.0
+#
+#  Unless required by applicable law or agreed to in writing, software
+#  distributed under the License is distributed on an "AS IS" BASIS,
+#  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#  See the License for the specific language governing permissions and
+#  limitations under the License.
+
+version: 2
+updates:
+  - package-ecosystem: gradle
+    directory: /
+    schedule:
+      interval: daily
+  - package-ecosystem: github-actions
+    directory: /
+    schedule:
+      interval: daily
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -0,0 +1,112 @@
+#  SPDX-License-Identifier: Apache-2.0
+#
+#  Copyright 2019-2024 The TurnKey Authors
+#
+#  Licensed under the Apache License, Version 2.0 (the "License");
+#  you may not use this file except in compliance with the License.
+#  You may obtain a copy of the License at
+#
+#      http://www.apache.org/licenses/LICENSE-2.0
+#
+#  Unless required by applicable law or agreed to in writing, software
+#  distributed under the License is distributed on an "AS IS" BASIS,
+#  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#  See the License for the specific language governing permissions and
+#  limitations under the License.
+
+name: CI/CD
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+  workflow_dispatch:
+
+permissions:
+  contents: write
+
+jobs:
+  build-local:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-java@v4
+        with:
+          distribution: temurin
+          java-version: 17
+      - uses: gradle/actions/setup-gradle@v4
+      - run: |
+          ./gradlew build testRunner versionFile
+          cp build/cvc5.version build/libs/cvc5-turnkey-*-test-runner.jar .
+      - uses: actions/upload-artifact@v4
+        with:
+          name: test-runner
+          path: |
+            cvc5-turnkey-*-test-runner.jar
+            cvc5.version
+
+  test:
+    strategy:
+      matrix:
+        os: [macos-latest, ubuntu-latest, windows-latest]
+        java-package: [liberica, microsoft, temurin, zulu]
+        java-version: [8, 11, 17, 21]
+        architecture: [x64]
+        exclude:
+          - java-package: microsoft
+            java-version: 8
+      fail-fast: false # Ensure we get all failures on all affected platforms
+
+    name: JUnit Test on ${{ matrix.os }} and ${{ matrix.java-package }} version ${{ matrix.java-version }} for ${{ matrix.architecture }}
+    needs: build-local
+    runs-on: ${{ matrix.os }}
+    steps:
+      - uses: actions/download-artifact@v4
+        with:
+          name: test-runner
+
+      - uses: actions/setup-java@v4
+        with:
+          distribution: ${{ matrix.java-package }}
+          java-version: ${{ matrix.java-version }}
+          architecture: ${{ matrix.architecture }}
+
+      - shell: bash
+        run: |
+          cvc5version="$(cat cvc5.version)"
+          prefix=""
+          if ! command -v arch &> /dev/null; then
+            case "${{ matrix.architecture }}" in
+              "aarch64") prefix="arch -arm64";;
+              "x64") prefix="arch -x86_64";;
+              *) echo "unknown architecture ${{ matrix.architecture }}"; exit 1;;
+            esac
+          fi
+          module_options=""
+          if [ "${{ matrix.java-version }}" -gt 8 ]; then
+            module_options="--add-opens java.base/java.io=ALL-UNNAMED"
+          fi
+          ${prefix} java ${module_options} \
+                         -DexpectedCVC5Version="${cvc5version}" \
+                         -jar cvc5-turnkey-*-test-runner.jar \
+                         execute --fail-if-no-tests \
+                                 --select-package tools.aqua.turnkey.cvc5 \
+                                 --reports-dir test-results
+      - uses: mikepenz/action-junit-report@v4
+        if: always()
+        with:
+          require_tests: true
+          report_paths: "test-results/*.xml"
+
+  dependency-submission:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-java@v4
+        with:
+          distribution: temurin
+          java-version: 17
+      - uses: gradle/actions/dependency-submission@v4
diff --git a/.gitignore b/.gitignore
@@ -0,0 +1,3 @@
+.gradle
+.idea
+build
diff --git a/AUTHORS.md b/AUTHORS.md
@@ -0,0 +1,20 @@
+<!--
+   SPDX-License-Identifier: CC-BY-4.0
+
+   Copyright 2019-2024 The TurnKey Authors
+
+   This work is licensed under the Creative Commons Attribution 4.0
+   International License.
+
+   You should have received a copy of the license along with this
+   work. If not, see <https://creativecommons.org/licenses/by/4.0/>.
+-->
+
+# The TurnKey Authors
+
+The project is maintained by [AQUA Group](https://aqua.engineering/) at TU Dortmund University.
+
+## Active Contributors
+
+- [Simon Dierl](mailto:simon.dierl@tu-dortmund.de)
+- [Malte Mues](mailto:mail.mues@gmail.com)
diff --git a/README.md b/README.md
@@ -0,0 +1,72 @@
+<!--
+   SPDX-License-Identifier: CC-BY-4.0
+
+   Copyright 2019-2024 The TurnKey Authors
+
+   This work is licensed under the Creative Commons Attribution 4.0
+   International License.
+
+   You should have received a copy of the license along with this
+   work. If not, see <https://creativecommons.org/licenses/by/4.0/>.
+-->
+
+[![GitHub Workflow Status](https://img.shields.io/github/actions/workflow/status/tudo-aqua/cvc5-turnkey/ci.yml?logo=githubactions&logoColor=white)](https://github.com/tudo-aqua/cvc5-turnkey/actions)
+[![JavaDoc](https://javadoc.io/badge2/tools.aqua/cvc5-turnkey/javadoc.svg)](https://javadoc.io/doc/tools.aqua/cvc5-turnkey)
+[![Maven Central](https://img.shields.io/maven-central/v/tools.aqua/cvc5-turnkey?logo=apache-maven)](https://search.maven.org/artifact/tools.aqua/cvc5-turnkey)
+
+# The cvc5-TurnKey Distribution
+
+[cvc5](https://github.com/cvc5/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](https://github.com/tudo-aqua/turnkey-support). 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          |     |   ✓   |         |
+
+## Usage
+
+The library can be included as a regular Maven dependency from the Maven Central repository. See the
+page for your version of choice [there](https://search.maven.org/artifact/tools.aqua/cvc5-turnkey)
+for configuration snippets for most build tools.
+
+## Building
+
+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](https://github.com/tudo-aqua/turnkey-gradle-plugin).
+- Additionally, Python 3 is required for a code generation step and localized by the
+  [gradle-use-python-plugin](https://github.com/xvik/gradle-use-python-plugin).
+
+## Java and JPMS Support
+
+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.
+
+## License
+
+cvc5 itself is licensed under the
+[3-Clause BSD License](https://opensource.org/licenses/BSD-3-Clause) and also incorporates
+components licensed under the [MIT License](https://opensource.org/licenses/MIT) and the
+[GNU Lesser General Public License v3.0 or later](https://www.gnu.org/licenses/lgpl-3.0.en.html).
+Two dependencies are introduced: the TurnKey support library is licensed under the
+[ISC License](https://opensource.org/licenses/ISC) and the JSpecify annotation library used by it is
+licensed under the [Apache License, Version 2.0](https://www.apache.org/licenses/LICENSE-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](https://www.apache.org/licenses/LICENSE-2.0). Standalone documentation
+is licensed under the
+[Creative Commons Attribution 4.0 International License](https://creativecommons.org/licenses/by/4.0/).
-Original file line number
+Diff line change
@@ -0,0 +1,3 @@
+    .gradle
+    .idea
+    build