diff --git a/.github/workflows/example-project-ci.yml b/.github/workflows/example-project-ci.yml new file mode 100644 index 0000000000..d850eeaf0d --- /dev/null +++ b/.github/workflows/example-project-ci.yml @@ -0,0 +1,298 @@ +# This file is part of JavaSMT, +# an API wrapper for a collection of SMT solvers: +# https://github.com/sosy-lab/java-smt +# +# SPDX-FileCopyrightText: 2026 Dirk Beyer +# +# SPDX-License-Identifier: Apache-2.0 + +name: example-project-ci + +on: + push + +jobs: + ivy: + name: Ivy Example Project + strategy: + fail-fast: false + matrix: + java-version: [ 21 ] + os: [ubuntu-latest, ubuntu-24.04-arm, windows-latest, windows-11-arm, macos-26-intel, macos-latest] + runs-on: ${{ matrix.os }} + steps: + - uses: actions/checkout@v6 + + - name: Set up JDK ${{ matrix.java-version }} + uses: actions/setup-java@v5 + with: + java-version: ${{ matrix.java-version }} + distribution: 'temurin' + + - name: Shared Ivy Cache + uses: actions/cache@v5 + with: + path: .ivy2 + # We use a unique key for each run to ensure the cache is updated if needed, + # while restoring from the most recent "ivy-shared-" cache. + key: ivy-shared-${{ github.run_id }} + restore-keys: | + ivy-shared- + enableCrossOsArchive: true + + - name: Build Ivy project + run: | + cd doc/Example-Ivy-Project + ant compile + + - name: Show solver table + run: | + cd doc/Example-Ivy-Project + ant run + env: + LD_PRELOAD: /usr/lib/${{ matrix.os == 'ubuntu-24.04-arm' && 'aarch64-linux-gnu' || 'x86_64-linux-gnu' }}/libstdc++.so.6 + + - name: Run tests + run: | + cd doc/Example-Ivy-Project + ant test + env: + LD_PRELOAD: /usr/lib/${{ matrix.os == 'ubuntu-24.04-arm' && 'aarch64-linux-gnu' || 'x86_64-linux-gnu' }}/libstdc++.so.6 + + - name: Upload test report + uses: actions/upload-artifact@v7 + if: always() + with: + path: doc/Example-Ivy-Project/build/test-report/html/junit-noframes.html + archive: false + + maven: + name: Maven Example Project + strategy: + fail-fast: false + matrix: + java-version: [ 21 ] + os: [ubuntu-24.04, ubuntu-24.04-arm, windows-2025, windows-11-arm, macos-26-intel, macos-26] + runs-on: ${{ matrix.os }} + steps: + - uses: actions/checkout@v6 + + - name: Set up JDK ${{ matrix.java-version }} + uses: actions/setup-java@v5 + with: + java-version: ${{ matrix.java-version }} + distribution: 'temurin' + + - name: Shared Maven Cache + uses: actions/cache@v5 + with: + path: .m2/repository + # We use a unique key for each run to ensure the cache is updated if needed, + # while restoring from the most recent "maven-shared-" cache. + key: maven-shared-${{ github.run_id }} + restore-keys: | + maven-shared- + enableCrossOsArchive: true + + - name: Build Maven example project + run: | + cd doc/Example-Maven-Project + mvn -DskipTests compile + + - name: Show solver table + run: | + cd doc/Example-Maven-Project + mvn exec:exec + env: + LD_PRELOAD: /usr/lib/${{ matrix.os == 'ubuntu-24.04-arm' && 'aarch64-linux-gnu' || 'x86_64-linux-gnu' }}/libstdc++.so.6 + + - name: Run tests + run: | + cd doc/Example-Maven-Project + mvn test + env: + LD_PRELOAD: /usr/lib/${{ matrix.os == 'ubuntu-24.04-arm' && 'aarch64-linux-gnu' || 'x86_64-linux-gnu' }}/libstdc++.so.6 + + - name: Generate test report + run : | + cd doc/Example-Maven-Project + mvn surefire-report:report-only + + - name: Upload test report + uses: actions/upload-artifact@v7 + if: always() + with: + path: doc/Example-Maven-Project/target/reports/surefire.html + archive: false + + web: + name: Maven Web Example Project + strategy: + fail-fast: false + matrix: + java-version: [ 21 ] + os: [ubuntu-24.04] + runs-on: ${{ matrix.os }} + steps: + - uses: actions/checkout@v6 + + - name: Set up JDK ${{ matrix.java-version }} + uses: actions/setup-java@v5 + with: + java-version: ${{ matrix.java-version }} + distribution: 'temurin' + + - name: Shared Maven Cache + uses: actions/cache@v5 + with: + path: .m2/repository + # We use a unique key for each run to ensure the cache is updated if needed, + # while restoring from the most recent "maven-shared-" cache. + key: maven-shared-${{ github.run_id }} + restore-keys: | + maven-shared- + enableCrossOsArchive: true + + - name: Build Maven Web example project + run: | + cd doc/Example-Maven-Web-Project + mvn -DskipTests package + + - name: Run tests + run: | + cd doc/Example-Maven-Web-Project + mvn test + env: + LD_PRELOAD: /usr/lib/${{ matrix.os == 'ubuntu-24.04-arm' && 'aarch64-linux-gnu' || 'x86_64-linux-gnu' }}/libstdc++.so.6 + + - name: Generate test report + run : | + cd doc/Example-Maven-Web-Project + mvn surefire-report:report-only + + - name: Upload test report + uses: actions/upload-artifact@v7 + if: always() + with: + path: doc/Example-Maven-Web-Project/target/reports/surefire.html + archive: false + + gradle: + name: Gradle Example Project + strategy: + fail-fast: false + matrix: + java-version: [ 21 ] + os: [ ubuntu-24.04, ubuntu-24.04-arm, windows-2025, windows-11-arm, macos-26-intel, macos-26 ] + runs-on: ${{ matrix.os }} + steps: + - uses: actions/checkout@v6 + + - name: Set up JDK ${{ matrix.java-version }} + uses: actions/setup-java@v5 + with: + java-version: ${{ matrix.java-version }} + distribution: 'temurin' + architecture: ${{ matrix.arch }} + + - name: Shared Maven Cache + uses: actions/cache@v5 + with: + path: .m2/repository + # We use a unique key for each run to ensure the cache is updated if needed, + # while restoring from the most recent "maven-shared-" cache. + key: maven-shared-${{ github.run_id }} + restore-keys: | + maven-shared- + enableCrossOsArchive: true + + - name: Install Gradle + uses: gradle/actions/setup-gradle@v6 + with: + gradle-version: '9.5.1' + + - name: Build Gradle example project + run: | + cd doc/Example-Gradle-Project + gradle build -x test + + - name: Show solver table + run: | + cd doc/Example-Gradle-Project + gradle run + env: + LD_PRELOAD: /usr/lib/${{ matrix.os == 'ubuntu-24.04-arm' && 'aarch64-linux-gnu' || 'x86_64-linux-gnu' }}/libstdc++.so.6 + + - name: Run tests + run: | + cd doc/Example-Gradle-Project + gradle test + env: + LD_PRELOAD: /usr/lib/${{ matrix.os == 'ubuntu-24.04-arm' && 'aarch64-linux-gnu' || 'x86_64-linux-gnu' }}/libstdc++.so.6 + + - name: Upload test report + uses: actions/upload-artifact@v7 + if: always() + with: + path: doc/Example-Gradle-Project/build/reports/tests/test/index.html + archive: false + + kotlin: + name: Kotlin Gradle Example Project + strategy: + fail-fast: false + matrix: + java-version: [ 21 ] + os: [ ubuntu-24.04, ubuntu-24.04-arm, windows-2025, windows-11-arm, macos-26-intel, macos-26 ] + runs-on: ${{ matrix.os }} + steps: + - uses: actions/checkout@v6 + + - name: Set up JDK ${{ matrix.java-version }} + uses: actions/setup-java@v5 + with: + java-version: ${{ matrix.java-version }} + distribution: 'temurin' + architecture: ${{ matrix.arch }} + + - name: Shared Maven Cache + uses: actions/cache@v5 + with: + path: .m2/repository + # We use a unique key for each run to ensure the cache is updated if needed, + # while restoring from the most recent "maven-shared-" cache. + key: maven-shared-${{ github.run_id }} + restore-keys: | + maven-shared- + enableCrossOsArchive: true + + - name: Install Gradle + uses: gradle/actions/setup-gradle@v6 + with: + gradle-version: '9.5.1' + + - name: Build Kotlin example project + run: | + cd doc/Example-Gradle-Project-Kotlin + gradle build -x test + + - name: Show solver table + run: | + cd doc/Example-Gradle-Project-Kotlin + gradle run + env: + LD_PRELOAD: /usr/lib/${{ matrix.os == 'ubuntu-24.04-arm' && 'aarch64-linux-gnu' || 'x86_64-linux-gnu' }}/libstdc++.so.6 + + - name: Run tests + run: | + cd doc/Example-Gradle-Project-Kotlin + gradle test + env: + LD_PRELOAD: /usr/lib/${{ matrix.os == 'ubuntu-24.04-arm' && 'aarch64-linux-gnu' || 'x86_64-linux-gnu' }}/libstdc++.so.6 + + - name: Upload test report + uses: actions/upload-artifact@v7 + if: always() + with: + path: doc/Example-Gradle-Project-Kotlin/build/reports/tests/test/index.html + archive: false diff --git a/doc/Example-Gradle-Project-Kotlin/build.gradle.kts b/doc/Example-Gradle-Project-Kotlin/build.gradle.kts index f61c077498..5e4357b51b 100644 --- a/doc/Example-Gradle-Project-Kotlin/build.gradle.kts +++ b/doc/Example-Gradle-Project-Kotlin/build.gradle.kts @@ -8,31 +8,35 @@ // This is an example for Gradle usage in Kotlin with Kotlin in Gradle -import org.jetbrains.kotlin.gradle.tasks.KotlinCompile +import org.gradle.nativeplatform.platform.internal.DefaultNativePlatform +import org.jetbrains.kotlin.gradle.dsl.JvmTarget plugins { // Apply the kotlin.jvm plugin to add support for Kotlin. - kotlin("jvm") version "1.6.21" + kotlin("jvm") version "2.3.21" // Apply the application plugin to add support for building a CLI application in Java. application } -// Set the used Java version -java.sourceCompatibility = JavaVersion.VERSION_11 - // Globally define versions used for our dependencies -val javasmtVersion = "3.12.0" -val javasmtYices2Version = "3.12.0" -val junit4Version = "4.13" -val z3Version = "4.8.17" -val smtInterpolVersion = "2.5-916-ga5843d8b" +val javasmtVersion = "6.0.0-148-gba08f432a" +val javasmtYices2Version = "6.0.0-141-g04134287c" + +val bitwuzlaVersion = "0.9.0-gd13ef925" val boolectorVersion = "3.2.2-g1a89c229" val cvc4Version = "1.8-prerelease-2020-06-24-g7825d8f28" -val mathsat5Version = "5.6.6-sosy1" -val optiMathsat5Version = "1.7.1-sosy0" -val yices2Version = "2.6.2-396-g194350c1" -val princessVersion = "2021-11-15" +val cvc5Version = "2026-02-26-d22638a" +val mathsat5Version = "5.6.15" +val opensmtVersion = "2.9.2-ge4c80308" +val smtInterpolVersion = "2.5-1242-g5c50fb6d" +val princessVersion = "2025-11-17" +val ostrichVersion = "2.0" +val yices2Version = "2.7.0-gdc5687ca" +val z3Version = "4.15.0" +val z3LegacyVersion = "4.5.0-gd57a2a6dc" + +val junit6Version = "6.1.0" repositories { // Use MavenCentral as a source, but try using POMs first and if that fails just use the artifact @@ -59,58 +63,163 @@ repositories { } } +val os = DefaultNativePlatform.getCurrentOperatingSystem() +val arch = DefaultNativePlatform.getCurrentArchitecture() + dependencies { // Align versions of all Kotlin components - //implementation(platform("org.jetbrains.kotlin:kotlin-bom")) + implementation(platform("org.jetbrains.kotlin:kotlin-bom")) - // Use the Kotlin JDK 11 standard library. - //implementation("org.jetbrains.kotlin:kotlin-stdlib-jdk11") - - // JUnit 4 - testImplementation("junit:junit:$junit4Version") + // JUnit + testImplementation("org.junit.jupiter:junit-jupiter-api:$junit6Version") + testImplementation("org.junit.jupiter:junit-jupiter-params:$junit6Version") + testImplementation("org.junit.jupiter:junit-jupiter-engine:$junit6Version") // JavaSMT dependencies implementation("org.sosy-lab:java-smt:$javasmtVersion") - // JavaSMT solver dependencies + // Princess/Ostrich + runtimeOnly("io.github.uuverifiers:princess_2.13:$princessVersion") + runtimeOnly("io.github.uuverifiers:ostrich_2.13:$ostrichVersion") + + // SMTInterpol + runtimeOnly("de.uni-freiburg.informatik.ultimate:smtinterpol:$smtInterpolVersion") + // Z3 - runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:com.microsoft.z3@jar") - runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3@so") - runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3java@so") - - runtimeOnly("org.sosy-lab:javasmt-solver-mathsat5:$mathsat5Version:libmathsat5j@so") + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version@jar") - // Retrieve OptiMathSAT via Ivy (as it is currently not available in Maven) - runtimeOnly("org.sosy_lab:javasmt-solver-optimathsat:$optiMathsat5Version:liboptimathsat5j@so") + // Z3 4.5 + runtimeOnly("org.sosy-lab:javasmt-solver-z3-legacy:$z3LegacyVersion:com.microsoft.z3legacy@jar") - // Retrieve CVC4 via Maven + // Bitwuzla + runtimeOnly("org.sosy-lab:javasmt-solver-bitwuzla:$bitwuzlaVersion@jar") + + // CVC4 runtimeOnly("org.sosy-lab:javasmt-solver-cvc4:$cvc4Version:CVC4@jar") - runtimeOnly("org.sosy-lab:javasmt-solver-cvc4:$cvc4Version:libcvc4@so") - runtimeOnly("org.sosy-lab:javasmt-solver-cvc4:$cvc4Version:libcvc4jni@so") - runtimeOnly("org.sosy-lab:javasmt-solver-cvc4:$cvc4Version:libcvc4parser@so") - - // Retrieve Boolector via Maven - runtimeOnly("org.sosy-lab:javasmt-solver-boolector:$boolectorVersion:libboolector@so") - runtimeOnly("org.sosy-lab:javasmt-solver-boolector:$boolectorVersion:libminisat@so") - runtimeOnly("org.sosy-lab:javasmt-solver-boolector:$boolectorVersion:libpicosat@so") - - // Retrieve Princess - runtimeOnly("io.github.uuverifiers:princess_2.13:$princessVersion@jar") - - // Retrieve SMTInterpol - runtimeOnly("de.uni-freiburg.informatik.ultimate:smtinterpol:$smtInterpolVersion@jar") - - // Example as to how to use Yices2 - // First get JavaSMT for Yices2 from Maven (if you want to use only Yices2 use this dependency in the "implementation" part above instead of regual JavaSMT) + + // CVC5 + runtimeOnly("org.sosy-lab:javasmt-solver-cvc5:$cvc5Version@jar") + + // Yices2 runtimeOnly("org.sosy-lab:javasmt-yices2:$javasmtYices2Version@jar") - // And the Yices2 solver from Maven - runtimeOnly("org.sosy-lab:javasmt-solver-yices2:$yices2Version:libyices2j@so") - + runtimeOnly("org.sosy-lab:javasmt-solver-yices2:$yices2Version@jar") + + // OpenSMT + runtimeOnly("org.sosy-lab:javasmt-solver-opensmt:$opensmtVersion@jar") + + when { + os.isLinux() && arch.isAmd64() -> { + // Mathsat5 + runtimeOnly("org.sosy-lab:javasmt-solver-mathsat:$mathsat5Version:libmathsat5j-x64@so") + + // Z3 + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3-x64@so") + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3java-x64@so") + + // Z3 4.5 + runtimeOnly("org.sosy-lab:javasmt-solver-z3-legacy:$z3LegacyVersion:libz3legacy-x64@so") + runtimeOnly("org.sosy-lab:javasmt-solver-z3-legacy:$z3LegacyVersion:libz3javalegacy-x64@so") + + // Bitwuzla + runtimeOnly("org.sosy-lab:javasmt-solver-bitwuzla:$bitwuzlaVersion:libbitwuzlaj-x64@so") + + // CVC4 + runtimeOnly("org.sosy-lab:javasmt-solver-cvc4:$cvc4Version:libcvc4@so") + runtimeOnly("org.sosy-lab:javasmt-solver-cvc4:$cvc4Version:libcvc4jni@so") + runtimeOnly("org.sosy-lab:javasmt-solver-cvc4:$cvc4Version:libcvc4parser@so") + + // CVC5 + runtimeOnly("org.sosy-lab:javasmt-solver-cvc5:$cvc5Version:libcvc5jni-x64@so") + + // Boolector + runtimeOnly("org.sosy-lab:javasmt-solver-boolector:$boolectorVersion:libboolector@so") + runtimeOnly("org.sosy-lab:javasmt-solver-boolector:$boolectorVersion:libminisat@so") + runtimeOnly("org.sosy-lab:javasmt-solver-boolector:$boolectorVersion:libpicosat@so") + + // Yices2 + runtimeOnly("org.sosy-lab:javasmt-solver-yices2:$yices2Version:libyices2java-x64@so") + + // OpenSMT + runtimeOnly("org.sosy-lab:javasmt-solver-opensmt:$opensmtVersion:libopensmtj-x64@so") + } + + os.isLinux() && arch.isArm64() -> { + // Mathsat5 + runtimeOnly("org.sosy-lab:javasmt-solver-mathsat:$mathsat5Version:libmathsat5j-arm64@so") + + // Z3 + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3-arm64@so") + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3java-arm64@so") + + // Z3 4.5 + runtimeOnly("org.sosy-lab:javasmt-solver-z3-legacy:$z3LegacyVersion:libz3legacy-arm64@so") + runtimeOnly("org.sosy-lab:javasmt-solver-z3-legacy:$z3LegacyVersion:libz3javalegacy-arm64@so") + + // Bitwuzla + runtimeOnly("org.sosy-lab:javasmt-solver-bitwuzla:$bitwuzlaVersion:libbitwuzlaj-arm64@so") + + // CVC5 + runtimeOnly("org.sosy-lab:javasmt-solver-cvc5:$cvc5Version:libcvc5jni-arm64@so") + // OpenSMT + runtimeOnly("org.sosy-lab:javasmt-solver-opensmt:$opensmtVersion:libopensmtj-arm64@so") + } + + os.isWindows() && arch.isAmd64() -> { + // Mathsat5 + runtimeOnly("org.sosy-lab:javasmt-solver-mathsat:$mathsat5Version:mathsat5j-x64@dll") + runtimeOnly("org.sosy-lab:javasmt-solver-mathsat:$mathsat5Version:mathsat-x64@dll") + runtimeOnly("org.sosy-lab:javasmt-solver-mathsat:$mathsat5Version:gmp-x64@dll") + + // Z3 + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3-x64@dll") + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3java-x64@dll") + + // Bitwuzla + runtimeOnly("org.sosy-lab:javasmt-solver-bitwuzla:$bitwuzlaVersion:libbitwuzlaj-x64@dll") + + // CVC5 + runtimeOnly("org.sosy-lab:javasmt-solver-cvc5:$cvc5Version:libcvc5jni-x64@dll") + + // Yices2 + runtimeOnly("org.sosy-lab:javasmt-solver-yices2:$yices2Version:yices2java-x64@dll") + } + + os.isWindows() && arch.isArm64() -> { + // Z3 + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3-arm64@dll") + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3java-arm64@dll") + + // CVC5 + runtimeOnly("org.sosy-lab:javasmt-solver-cvc5:$cvc5Version:libcvc5jni-arm64@dll") + } + + os.isMacOsX() && arch.isAmd64() -> { + // Z3 + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3-x64@dylib") + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3java-x64@dylib") + + // CVC5 + runtimeOnly("org.sosy-lab:javasmt-solver-cvc5:$cvc5Version:libcvc5jni-x64@dylib") + } + + os.isMacOsX() && arch.isArm64() -> { + // Z3 + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3-arm64@dylib") + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3java-arm64@dylib") + + // CVC5 + runtimeOnly("org.sosy-lab:javasmt-solver-cvc5:$cvc5Version:libcvc5jni-arm64@dylib") + } + + else -> error("Unsupported OS or architecture") + } + + // Tell implementation config to use the JavaSMT + dependencies from our dependencies folder implementation(fileTree("dir" to "build/dependencies", "include" to "*.jar")) } -// Not really used in the current example, just here for completeness sake +// Configure tests testing { suites { // Configure the built-in test suite @@ -126,10 +235,14 @@ application { mainClass.set("org.sosy_lab.java_smt_example.JavaSMTKotlinExampleKt") } -// compile bytecode to java 11 -tasks.withType { - kotlinOptions.jvmTarget = "11" +// Compile to Java 17 +// JavaSMT requires at least Java 17, but a newer version could be used here +kotlin { + compilerOptions { + jvmTarget.set(JvmTarget.JVM_17) + } } +java.sourceCompatibility = JavaVersion.VERSION_17 // Use a config to identify JavaSMT components configurations { @@ -139,6 +252,26 @@ configurations { } } +fun shorten(full: String) : String { + val regex = """(.*)(?:-x64|-arm64)\.(so|dll|dylib)$""".toRegex() + val matchResult = regex.find(full) + var clipped = "" + if (matchResult != null) { + val (prefix, suffix) = matchResult.destructured + clipped = "$prefix.$suffix" + } else { + clipped = full + } + val regex2 = """.*-(.*).(so|dll|dylib)$""".toRegex() + val matchResult2 = regex2.find(clipped) + if (matchResult2 != null) { + val (libname, suffix) = matchResult2.destructured + return "$libname.$suffix" + } else { + return clipped + } +} + // JavaSMT needs the solver dependencies in a particular folder structure; in the same folder as JavaSMT is the easiest. // Also we need to rename some solver dependencies. // Clean, then copy all JavaSMT components into the build/dependencies folder, rename and use it from there @@ -146,7 +279,7 @@ tasks.register("copyDependencies") { dependsOn("cleanDownloadedDependencies") from(configurations["javaSMTConfig"]) into("build/dependencies") - rename(".*(lib[^-]*)-?.*.so", "\$1.so") + rename(::shorten) } // Cleanup task for the JavaSMT components/dependencies @@ -169,6 +302,6 @@ tasks.withType { duplicatesStrategy = DuplicatesStrategy.EXCLUDE } -tasks.withType{ +tasks.withType { duplicatesStrategy = DuplicatesStrategy.EXCLUDE -} \ No newline at end of file +} diff --git a/doc/Example-Gradle-Project-Kotlin/src/main/kotlin/org/sosy_lab/java_smt_example/JavaSMTKotlinExample.kt b/doc/Example-Gradle-Project-Kotlin/src/main/kotlin/org/sosy_lab/java_smt_example/JavaSMTKotlinExample.kt index cbd98625a2..afe72b70e9 100644 --- a/doc/Example-Gradle-Project-Kotlin/src/main/kotlin/org/sosy_lab/java_smt_example/JavaSMTKotlinExample.kt +++ b/doc/Example-Gradle-Project-Kotlin/src/main/kotlin/org/sosy_lab/java_smt_example/JavaSMTKotlinExample.kt @@ -20,10 +20,7 @@ import org.sosy_lab.java_smt.example.SolverOverviewTable.SolverInfo fun main() { val infos: MutableList = mutableListOf() for (s in Solvers.values()) { - val info: SolverInfo? = SolverOverviewTable().getSolverInformation(s) - if (info != null) { - infos.add(info) - } + infos.add(SolverOverviewTable().getSolverInformation(s)!!) } infos.sortBy { it.getName() } // alphabetical ordering diff --git a/doc/Example-Gradle-Project-Kotlin/src/test/kotlin/org/sosy_lab/java_smt_example/AppTest.kt b/doc/Example-Gradle-Project-Kotlin/src/test/kotlin/org/sosy_lab/java_smt_example/AppTest.kt index 0b3563eb98..cce142b2ef 100644 --- a/doc/Example-Gradle-Project-Kotlin/src/test/kotlin/org/sosy_lab/java_smt_example/AppTest.kt +++ b/doc/Example-Gradle-Project-Kotlin/src/test/kotlin/org/sosy_lab/java_smt_example/AppTest.kt @@ -2,48 +2,164 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2021 Dirk Beyer +// SPDX-FileCopyrightText: 2026 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 package org.sosy_lab.java_smt_example; +import com.google.common.base.Joiner +import com.google.common.base.Splitter +import com.google.common.base.StandardSystemProperty +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.Assertions.assertNotNull +import org.junit.jupiter.api.Assumptions.assumeTrue +import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.params.Parameter +import org.junit.jupiter.params.ParameterizedClass +import org.junit.jupiter.params.provider.MethodSource +import org.sosy_lab.common.NativeLibraries +import org.sosy_lab.common.ShutdownNotifier +import org.sosy_lab.common.configuration.Configuration +import org.sosy_lab.common.log.BasicLogManager +import org.sosy_lab.common.log.LogManager +import org.sosy_lab.java_smt.SolverContextFactory +import org.sosy_lab.java_smt.SolverContextFactory.Solvers +import org.sosy_lab.java_smt.api.SolverContext +import org.sosy_lab.java_smt.example.Sudoku +import java.util.* +import java.util.logging.Level +import kotlin.test.AfterTest +import kotlin.test.BeforeTest import kotlin.test.Test +/** + * This test parses a String-given Sudoku and solves it with an SMT solver. + * + * + * This program is just an example and clearly SMT is not the best solution for solving Sudoku. + * There might be other algorithms out there that are better suited for solving Sudoku. + * + * + * The more numbers are available in a Sudoku, the easier it can be solved. A completely empty + * Sudoku will cause the longest runtime in the solver, because it will guess a lot of values. + * + * + * The Sudoku is read from a String and should be formatted as the following example: + * + * ``` + * 2..9.6..1 + * ..6.4...9 + * ...52.4.. + * 3.2..7.5. + * ...2..1.. + * .9.3..7.. + * .87.5.31. + * 6.3.1.8.. + * 4....9... + * ``` + * + * The solution will then be printed on StdOut and checked by an assertion, just like the + * following solution: + * + * ``` + * 248976531 + * 536148279 + * 179523468 + * 312487956 + * 764295183 + * 895361742 + * 987652314 + * 623714895 + * 451839627 + * ``` + */ + +@ParameterizedClass +@MethodSource("getAllSolvers") class AppTest { + @Parameter(0) + lateinit var solver: Solvers + + val config = Configuration.defaultConfiguration() + val logger = BasicLogManager.create(config) + val notifier = ShutdownNotifier.createDummy() + + @BeforeEach + fun init() { + assumeTrue(Platform.isSupported(solver)) + } + + @Test + fun checkSudoku() { + logger.log(Level.INFO, "Executing " + solver + "...") + + SolverContextFactory.createSolverContext(config, logger, notifier, solver).use { + val grid = readGridFromString(input) + val sudoku = Sudoku.BooleanBasedSudokuSolver(it) + val solution = sudoku.solve(grid) + + assertNotNull(solution) + assertEquals(sudokuSolution, solutionToString(solution)) + } + } + + private fun solutionToString(solution: Array?>): String { + val sb = StringBuilder() + for (s1 in solution) { + sb.append(Joiner.on("").join(s1!!)).append('\n') + } + return sb.toString().trim() + } + + /** + * A simple parser for a half-filled Sudoku. + * + * + * Use digits 0-9 as values, other values will be set to 'unknown'. + */ + private fun readGridFromString(puzzle: String): Array?> { + val lines = Splitter.on('\n').splitToList(puzzle) + val size = lines.size + val grid = Array?>(size) { arrayOfNulls(size) } + + for (row in lines.indices) { + for (col in 0.. +// +// SPDX-License-Identifier: Apache-2.0 +package org.sosy_lab.java_smt_example + +import com.google.common.base.StandardSystemProperty +import org.sosy_lab.common.NativeLibraries +import org.sosy_lab.java_smt.SolverContextFactory +import java.util.* + +internal object Platform { + private val OS: String = StandardSystemProperty.OS_NAME.value()!!.lowercase(Locale.getDefault()).replace(" ", "") + private val ARCH: String = StandardSystemProperty.OS_ARCH.value()!!.lowercase(Locale.getDefault()).replace(" ", "") + + private val IS_WINDOWS: Boolean = OS.startsWith("windows") + private val IS_MAC: Boolean = OS.startsWith("macos") + private val IS_LINUX: Boolean = OS.startsWith("linux") + + private val IS_ARCH_ARM64: Boolean = ARCH.equals("aarch64") + + private fun isSufficientVersionOfLibcxx(library: String): Boolean { + try { + NativeLibraries.loadLibrary(library) + } catch (e: UnsatisfiedLinkError) { + for (dependency in getRequiredLibcxx(library)) { + if (e.message!!.contains("version `" + dependency + "' not found")) { + return false + } + } + } + return true + } + + private fun getRequiredLibcxx(library: String): Array { + return when (library) { + "z3" -> arrayOf("GLIBC_2.34", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29") + "bitwuzlaj" -> arrayOf("GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29") + "opensmtj" -> arrayOf("GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29") + "mathsat5j" -> arrayOf("GLIBC_2.33", "GLIBC_2.38") + "cvc5jni" -> arrayOf("GLIBC_2.32") + "yices2java" -> arrayOf("GLIBC_2.34") + else -> arrayOf() + } + } + + /** + * `True` if the solver is supported on the current operating system and CPU + * architecture + */ + fun isSupported(solver: SolverContextFactory.Solvers): Boolean { + return when (solver) { + SolverContextFactory.Solvers.SMTINTERPOL, SolverContextFactory.Solvers.PRINCESS -> + // Any operating system and any architecture is allowed, Java is sufficient + true + + SolverContextFactory.Solvers.BOOLECTOR, SolverContextFactory.Solvers.CVC4 -> + IS_LINUX && !IS_ARCH_ARM64 + + SolverContextFactory.Solvers.YICES2 -> + (IS_LINUX && !IS_ARCH_ARM64 && isSufficientVersionOfLibcxx("yices2java")) || (IS_WINDOWS && !IS_ARCH_ARM64) + + SolverContextFactory.Solvers.CVC5 -> + (IS_LINUX && isSufficientVersionOfLibcxx("cvc5jni")) || IS_WINDOWS || IS_MAC + + SolverContextFactory.Solvers.OPENSMT -> + IS_LINUX && isSufficientVersionOfLibcxx("opensmtj") + + SolverContextFactory.Solvers.BITWUZLA -> + (IS_LINUX && isSufficientVersionOfLibcxx("bitwuzlaj")) || (IS_WINDOWS && !IS_ARCH_ARM64) + + SolverContextFactory.Solvers.MATHSAT5 -> + (IS_LINUX && isSufficientVersionOfLibcxx("mathsat5j")) || (IS_WINDOWS && !IS_ARCH_ARM64) + + SolverContextFactory.Solvers.Z3 -> + (IS_LINUX && isSufficientVersionOfLibcxx("z3")) || IS_WINDOWS || IS_MAC + + SolverContextFactory.Solvers.Z3_WITH_INTERPOLATION -> + IS_LINUX && !IS_ARCH_ARM64 + } + } +} \ No newline at end of file diff --git a/doc/Example-Gradle-Project/build.gradle b/doc/Example-Gradle-Project/build.gradle index 33ada17510..7a7c5c9742 100644 --- a/doc/Example-Gradle-Project/build.gradle +++ b/doc/Example-Gradle-Project/build.gradle @@ -6,118 +6,247 @@ // // SPDX-License-Identifier: Apache-2.0 -apply plugin: 'java' -apply plugin: 'application' +import org.gradle.nativeplatform.platform.internal.DefaultNativePlatform -mainClassName = 'org.sosy_lab.java_smt_example.SolverOverviewTable' +plugins { + id 'java' + id 'application' +} // Globally define versions used for our dependencies def version = [ - 'javasmt': '3.12.0', - 'javasmtYices2': '3.12.0', - 'junit4': '4.13', - 'smtInterpol': '2.5-916-ga5843d8b', + 'javasmt': '6.0.0-148-gba08f432a', + 'javasmtYices2': '6.0.0-141-g04134287c', + + 'bitwuzla': '0.9.0-gd13ef925', 'boolector': '3.2.2-g1a89c229', - 'z3': '4.8.17', 'cvc4': '1.8-prerelease-2020-06-24-g7825d8f28', - 'mathsat5': '5.6.6-sosy1', - 'optiMathsat5': '1.7.1-sosy0', - 'yices2': '2.6.2-396-g194350c1', - 'princess': '2021-11-15' + 'cvc5': '2026-02-26-d22638a', + 'mathsat5': '5.6.15', + 'opensmt': '2.9.2-ge4c80308', + 'smtInterpol': '2.5-1242-g5c50fb6d', + 'princess': '2025-11-17', + 'ostrich': '2.0', + 'yices2': '2.7.0-gdc5687ca', + 'z3': '4.15.0', + 'z3legacy': '4.5.0-gd57a2a6dc', + + 'junit6': '6.1.0' ]; +def os = DefaultNativePlatform.getCurrentOperatingSystem() +def arch = DefaultNativePlatform.getCurrentArchitecture() + repositories { // try to resolve by pom first mavenCentral { metadataSources { - mavenPom() + mavenPom() } } // try to get artifacts if no useful pom is found mavenCentral { metadataSources { - artifact() + artifact() } } // Ivy can be used as well ivy { - url "https://www.sosy-lab.org/ivy" + url = "https://www.sosy-lab.org/ivy" patternLayout { - artifact "/[organisation]/[module]/[classifier]-[revision].[ext]" - // ivy "/[organisation]/[module]/ivy-[revision].xml" + artifact "/[organisation]/[module]/[classifier]-[revision].[ext]" + // ivy "/[organisation]/[module]/ivy-[revision].xml" } metadataSources { - artifact() + artifact() } } } configurations { // Use a custom config that inherits all dependencies from runtimeOnly and implementation. - // If you want to seperate your dependencies from the JavaSMT ones + // If you want to separate your dependencies from the JavaSMT ones // simply use it when pulling the dependencies. javaSMTConfig.extendsFrom(runtimeOnly, implementation) } // You can manage the JavaSMT dependencies via a config if you need to split them from your regular dependencies dependencies { - // JUnit 4 - testImplementation "junit:junit:${version.junit4}" - - // Retrieve JavaSMT with Maven and transitive dependencies via a pom.xml - implementation "org.sosy-lab:java-smt:${version.javasmt}" - - // Retrieve Z3 with Maven but without a pom.xml, just the artifacts - //runtimeOnly group: 'org.sosy-lab', name: 'javasmt-solver-z3', version: version.z3, classifier: 'com.microsoft.z3', ext: 'jar' - //runtimeOnly group: 'org.sosy-lab', name: 'javasmt-solver-z3', version: version.z3, classifier: 'libz3', ext: 'so' - //runtimeOnly group: 'org.sosy-lab', name: 'javasmt-solver-z3', version: version.z3, classifier: 'libz3java', ext: 'so' - - // Kotlin version as an alternative. Both should be equal - runtimeOnly("org/sosy-lab:javasmt-solver-z3:${version.z3}:com.microsoft.z3@jar") - runtimeOnly("org/sosy-lab:javasmt-solver-z3:${version.z3}:libz3@so") - runtimeOnly("org/sosy-lab:javasmt-solver-z3:${version.z3}:libz3java@so") - - // Mathsat5 via Maven - runtimeOnly group: 'org.sosy-lab', name: 'javasmt-solver-mathsat5', version: version.mathsat5, classifier: 'libmathsat5j', ext: 'so' - - // Retrieve OptiMathSAT via Ivy (as it is currently not available in Maven) - runtimeOnly "org.sosy_lab:javasmt-solver-optimathsat:${version.optiMathsat5}:liboptimathsat5j@so" - - // Retrieve CVC4 via Maven - runtimeOnly group: 'org.sosy-lab', name: 'javasmt-solver-cvc4', version: version.cvc4, classifier: 'CVC4', ext: 'jar' - runtimeOnly group: 'org.sosy-lab', name: 'javasmt-solver-cvc4', version: version.cvc4, classifier: 'libcvc4', ext: 'so' - runtimeOnly group: 'org.sosy-lab', name: 'javasmt-solver-cvc4', version: version.cvc4, classifier: 'libcvc4jni', ext: 'so' - runtimeOnly group: 'org.sosy-lab', name: 'javasmt-solver-cvc4', version: version.cvc4, classifier: 'libcvc4parser', ext: 'so' - - // Retrieve Boolector via Maven - runtimeOnly group: 'org.sosy-lab', name: 'javasmt-solver-boolector', version: version.boolector, classifier: 'libboolector', ext: 'so' - runtimeOnly group: 'org.sosy-lab', name: 'javasmt-solver-boolector', version: version.boolector, classifier: 'libminisat', ext: 'so' - runtimeOnly group: 'org.sosy-lab', name: 'javasmt-solver-boolector', version: version.boolector, classifier: 'libpicosat', ext: 'so' - - // Retrieve Princess - runtimeOnly group: 'io.github.uuverifiers', name: 'princess_2.13', version: version.princess, ext: 'jar' - - // Retrieve SMTInterpol - runtimeOnly group: 'de.uni-freiburg.informatik.ultimate', name: 'smtinterpol', version: version.smtInterpol, ext: 'jar' - - // Example as to how to use Yices2 - // First get JavaSMT for Yices2 from Maven (if you want to use only Yices2 use this dependency in the "implementation" part above instead of regual JavaSMT) - runtimeOnly group: 'org.sosy-lab', name: 'javasmt-yices2', version: version.javasmtYices2, ext: 'jar' - // And the Yices2 solver from Maven - runtimeOnly group: 'org.sosy-lab', name: 'javasmt-solver-yices2', version: version.yices2, classifier: 'libyices2j', ext: 'so' + // JUnit + testImplementation("org.junit.jupiter:junit-jupiter-api:$version.junit6") + testImplementation("org.junit.jupiter:junit-jupiter-params:$version.junit6") + testImplementation("org.junit.jupiter:junit-jupiter-engine:$version.junit6") + testRuntimeOnly("org.junit.platform:junit-platform-launcher:$version.junit6") + + // JavaSMT dependencies + implementation("org.sosy-lab:java-smt:$version.javasmt") + + // Princess/Ostrich + runtimeOnly("io.github.uuverifiers:princess_2.13:$version.princess") + runtimeOnly("io.github.uuverifiers:ostrich_2.13:$version.ostrich") + + // SMTInterpol + runtimeOnly("de.uni-freiburg.informatik.ultimate:smtinterpol:$version.smtInterpol") + + // Z3 + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$version.z3@jar") + + // Z3 4.5 + runtimeOnly("org.sosy-lab:javasmt-solver-z3-legacy:$version.z3legacy:com.microsoft.z3legacy@jar") + + // Bitwuzla + runtimeOnly("org.sosy-lab:javasmt-solver-bitwuzla:$version.bitwuzla@jar") + + // CVC4 + runtimeOnly("org.sosy-lab:javasmt-solver-cvc4:$version.cvc4:CVC4@jar") + + // CVC5 + runtimeOnly("org.sosy-lab:javasmt-solver-cvc5:$version.cvc5@jar") + + // Yices2 + runtimeOnly("org.sosy-lab:javasmt-yices2:$version.javasmtYices2@jar") + runtimeOnly("org.sosy-lab:javasmt-solver-yices2:$version.yices2@jar") + + // OpenSMT + runtimeOnly("org.sosy-lab:javasmt-solver-opensmt:$version.opensmt@jar") + + if(os.isLinux() && arch.isAmd64()) { + // Mathsat5 + runtimeOnly("org.sosy-lab:javasmt-solver-mathsat:$version.mathsat5:libmathsat5j-x64@so") + + // Z3 + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$version.z3:libz3-x64@so") + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$version.z3:libz3java-x64@so") + + // Z3 4.5 + runtimeOnly("org.sosy-lab:javasmt-solver-z3-legacy:$version.z3legacy:libz3legacy-x64@so") + runtimeOnly("org.sosy-lab:javasmt-solver-z3-legacy:$version.z3legacy:libz3javalegacy-x64@so") + + // Bitwuzla + runtimeOnly("org.sosy-lab:javasmt-solver-bitwuzla:$version.bitwuzla:libbitwuzlaj-x64@so") + + // CVC4 + runtimeOnly("org.sosy-lab:javasmt-solver-cvc4:$version.cvc4:libcvc4@so") + runtimeOnly("org.sosy-lab:javasmt-solver-cvc4:$version.cvc4:libcvc4jni@so") + runtimeOnly("org.sosy-lab:javasmt-solver-cvc4:$version.cvc4:libcvc4parser@so") + + // CVC5 + runtimeOnly("org.sosy-lab:javasmt-solver-cvc5:$version.cvc5:libcvc5jni-x64@so") + + // Boolector + runtimeOnly("org.sosy-lab:javasmt-solver-boolector:$version.boolector:libboolector@so") + runtimeOnly("org.sosy-lab:javasmt-solver-boolector:$version.boolector:libminisat@so") + runtimeOnly("org.sosy-lab:javasmt-solver-boolector:$version.boolector:libpicosat@so") + + // Yices2 + runtimeOnly("org.sosy-lab:javasmt-solver-yices2:$version.yices2:libyices2java-x64@so") + + // OpenSMT + runtimeOnly("org.sosy-lab:javasmt-solver-opensmt:$version.opensmt:libopensmtj-x64@so") + + } else if (os.isLinux() && arch.isArm64()) { + // Mathsat5 + runtimeOnly("org.sosy-lab:javasmt-solver-mathsat:$version.mathsat5:libmathsat5j-arm64@so") + + // Z3 + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$version.z3:libz3-arm64@so") + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$version.z3:libz3java-arm64@so") + + // Z3 4.5 + runtimeOnly("org.sosy-lab:javasmt-solver-z3-legacy:$version.z3Legacy:libz3legacy-arm64@so") + runtimeOnly("org.sosy-lab:javasmt-solver-z3-legacy:$version.z3Legacy:libz3javalegacy-arm64@so") + + // Bitwuzla + runtimeOnly("org.sosy-lab:javasmt-solver-bitwuzla:$version.bitwuzla:libbitwuzlaj-arm64@so") + + // CVC5 + runtimeOnly("org.sosy-lab:javasmt-solver-cvc5:$version.cvc5:libcvc5jni-arm64@so") + + // OpenSMT + runtimeOnly("org.sosy-lab:javasmt-solver-opensmt:$version.opensmt:libopensmtj-arm64@so") + + } else if(os.isWindows() && arch.isAmd64()) { + // Mathsat5 + runtimeOnly("org.sosy-lab:javasmt-solver-mathsat:$version.mathsat5:mathsat5j-x64@dll") + runtimeOnly("org.sosy-lab:javasmt-solver-mathsat:$version.mathsat5:mathsat-x64@dll") + runtimeOnly("org.sosy-lab:javasmt-solver-mathsat:$version.mathsat5:gmp-x64@dll") + + // Z3 + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$version.z3:libz3-x64@dll") + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$version.z3:libz3java-x64@dll") + + // Bitwuzla + runtimeOnly("org.sosy-lab:javasmt-solver-bitwuzla:$version.bitwuzla:libbitwuzlaj-x64@dll") + + // CVC5 + runtimeOnly("org.sosy-lab:javasmt-solver-cvc5:$version.cvc5:libcvc5jni-x64@dll") + + // Yices2 + runtimeOnly("org.sosy-lab:javasmt-solver-yices2:$version.yices2:yices2java-x64@dll") + + } else if (os.isWindows() && arch.isArm64()){ + // Z3 + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$version.z3:libz3-arm64@dll") + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$version.z3:libz3java-arm64@dll") + + // CVC5 + runtimeOnly("org.sosy-lab:javasmt-solver-cvc5:$version.cvc5:libcvc5jni-arm64@dll") + + } else if(os.isMacOsX() && arch.isAmd64()) { + // Z3 + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$version.z3:libz3-x64@dylib") + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$version.z3:libz3java-x64@dylib") + + // CVC5 + runtimeOnly("org.sosy-lab:javasmt-solver-cvc5:$version.cvc5:libcvc5jni-x64@dylib") + + } else if(os.isMacOsX() && arch.isArm64()) { + // Z3 + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$version.z3:libz3-arm64@dylib") + runtimeOnly("org.sosy-lab:javasmt-solver-z3:$version.z3:libz3java-arm64@dylib") + + // CVC5 + runtimeOnly("org.sosy-lab:javasmt-solver-cvc5:$version.cvc5:libcvc5jni-arm64@dylib") + + } else { + throw new GradleException('Unsupported OS or architecture') + } // Tell implementation config to use the JavaSMT + dependencies from our dependencies folder implementation fileTree(dir: 'build/dependencies', include: '*.jar') } -// Test with JUnit4 (see dependencies) and 1gig heap +// Test with JUnit (see dependencies) and 1gig heap test { - useJUnit() + useJUnitPlatform() maxHeapSize = '1G' } +// Define the main class for the application. +application { + mainClass = 'org.sosy_lab.java_smt_example.SolverOverviewTable' +} + +// Compile to Java 17 +// JavaSMT requires at least Java 17, but a newer version could be used here +java.sourceCompatibility = JavaVersion.VERSION_17 + +def shorten(full) { + def match = full =~ /(.*)(?:-x64|-arm64)\.(so|dll|dylib)$/ + def clipped = full + if (match) { + clipped = match[0][1] + "." + match[0][2] + } + def match2 = clipped =~ /.*-(.*).(so|dll|dylib)$/ + if (match2) { + return match2[0][1] + "." + match2[0][2] + } else { + return clipped + } +} + // Copy and rename all JavaSMT dependencies -// This is necassary as Gradle renames the JavaSMT dependencies, but we need them to have certain names, +// This is necessary as Gradle renames the JavaSMT dependencies, but we need them to have certain names, // and they need to be in a specific location for JavaSMT to be found (the easiest ist the same folder) // For more information about this look up the sosy-commons loading process task copyDependencies(type: Copy) { @@ -126,7 +255,7 @@ task copyDependencies(type: Copy) { from configurations.javaSMTConfig into 'build/dependencies' // Renames the dependencies - rename '.*(lib[^-]*)-?.*.so', '$1.so' + rename(this.&shorten) } // Cleans the dependencies folder @@ -134,7 +263,7 @@ task cleanDownloadedDependencies(type: Delete) { delete fileTree('build/dependencies') } -// Copy the JavaSMT depdendencies before using them, to do this we declare a dependency on the copy task of ours here +// Copy the JavaSMT dependencies before using them, to do this we declare a dependency on the copy task of ours here compileJava.dependsOn copyDependencies // When clean is called we want to delete our copied JavaSMT files @@ -151,4 +280,4 @@ jar { attributes 'Main-Class': 'org.sosy_lab.java_smt_example.SolverOverviewTable' attributes 'Class-Path': configurations.javaSMTConfig.files.collect { it.getName() }.join(' ') } -} \ No newline at end of file +} diff --git a/doc/Example-Gradle-Project/src/test/java/org/sosy_lab/java_smt_example/Platform.java b/doc/Example-Gradle-Project/src/test/java/org/sosy_lab/java_smt_example/Platform.java new file mode 100644 index 0000000000..3949708466 --- /dev/null +++ b/doc/Example-Gradle-Project/src/test/java/org/sosy_lab/java_smt_example/Platform.java @@ -0,0 +1,76 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2026 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt_example; + +import com.google.common.base.StandardSystemProperty; +import java.util.Locale; +import org.sosy_lab.common.NativeLibraries; +import org.sosy_lab.java_smt.SolverContextFactory; + +class Platform { + private static final String OS = + StandardSystemProperty.OS_NAME.value().toLowerCase(Locale.getDefault()).replace(" ", ""); + private static final String ARCH = + StandardSystemProperty.OS_ARCH.value().toLowerCase(Locale.getDefault()).replace(" ", ""); + + private static final boolean IS_WINDOWS = OS.startsWith("windows"); + private static final boolean IS_MAC = OS.startsWith("macos"); + private static final boolean IS_LINUX = OS.startsWith("linux"); + + private static final boolean IS_ARCH_ARM64 = ARCH.equals("aarch64"); + + private static boolean isSufficientVersionOfLibcxx(String library) { + try { + NativeLibraries.loadLibrary(library); + } catch (UnsatisfiedLinkError e) { + for (String dependency : getRequiredLibcxx(library)) { + if (e.getMessage().contains("version `" + dependency + "' not found")) { + return false; + } + } + } + return true; + } + + private static String[] getRequiredLibcxx(String library) { + return switch (library) { + case "z3" -> new String[] {"GLIBC_2.34", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "bitwuzlaj" -> new String[] {"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "opensmtj" -> new String[] {"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "mathsat5j" -> new String[] {"GLIBC_2.33", "GLIBC_2.38"}; + case "cvc5jni" -> new String[] {"GLIBC_2.32"}; + case "yices2java" -> new String[] {"GLIBC_2.34"}; + default -> new String[] {}; + }; + } + + /** + * True if the solver is supported on the current operating system and CPU + * architecture + */ + static boolean isSupported(SolverContextFactory.Solvers solver) { + return switch (solver) { + case SMTINTERPOL, PRINCESS -> + // Any operating system and any architecture is allowed, Java is sufficient + true; + case BOOLECTOR, CVC4 -> IS_LINUX && !IS_ARCH_ARM64; + case YICES2 -> + (IS_LINUX && !IS_ARCH_ARM64 && isSufficientVersionOfLibcxx("yices2java")) + || (IS_WINDOWS && !IS_ARCH_ARM64); + case CVC5 -> (IS_LINUX && isSufficientVersionOfLibcxx("cvc5jni")) || IS_WINDOWS || IS_MAC; + case OPENSMT -> IS_LINUX && isSufficientVersionOfLibcxx("opensmtj"); + case BITWUZLA -> + (IS_LINUX && isSufficientVersionOfLibcxx("bitwuzlaj")) || (IS_WINDOWS && !IS_ARCH_ARM64); + case MATHSAT5 -> + (IS_LINUX && isSufficientVersionOfLibcxx("mathsat5j")) || (IS_WINDOWS && !IS_ARCH_ARM64); + case Z3 -> (IS_LINUX && isSufficientVersionOfLibcxx("z3")) || IS_WINDOWS || IS_MAC; + case Z3_WITH_INTERPOLATION -> IS_LINUX && !IS_ARCH_ARM64; + }; + } +} diff --git a/doc/Example-Gradle-Project/src/test/java/org/sosy_lab/java_smt_example/SudokuTest.java b/doc/Example-Gradle-Project/src/test/java/org/sosy_lab/java_smt_example/SudokuTest.java index 943a395f8d..8481060769 100644 --- a/doc/Example-Gradle-Project/src/test/java/org/sosy_lab/java_smt_example/SudokuTest.java +++ b/doc/Example-Gradle-Project/src/test/java/org/sosy_lab/java_smt_example/SudokuTest.java @@ -2,22 +2,20 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2021 Dirk Beyer +// SPDX-FileCopyrightText: 2026 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 package org.sosy_lab.java_smt_example; -import static org.junit.Assert.assertEquals; -import static org.junit.Assert.assertNotNull; -import static org.sosy_lab.java_smt.example.Sudoku.SIZE; - import com.google.common.base.Joiner; import com.google.common.base.Splitter; -import java.util.List; -import org.junit.After; -import org.junit.Before; -import org.junit.Test; +import org.junit.jupiter.api.AfterEach; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; +import org.junit.jupiter.params.Parameter; +import org.junit.jupiter.params.ParameterizedClass; +import org.junit.jupiter.params.provider.MethodSource; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; @@ -27,10 +25,18 @@ import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverException; -import org.sosy_lab.java_smt.example.Sudoku.IntegerBasedSudokuSolver; -import org.sosy_lab.java_smt.example.Sudoku.BooleanBasedSudokuSolver; +import org.sosy_lab.java_smt.example.Sudoku; import org.sosy_lab.java_smt.example.Sudoku.SudokuSolver; +import java.util.Arrays; +import java.util.List; +import java.util.logging.Level; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertNotNull; +import static org.junit.jupiter.api.Assumptions.assumeTrue; + + /** * This program parses a String-given Sudoku and solves it with an SMT solver. * @@ -69,38 +75,51 @@ * 451839627 * */ +@ParameterizedClass +@MethodSource("getAllSolvers") public class SudokuTest { + public static List getAllSolvers() { + return Arrays.asList(Solvers.values()); + } + + @Parameter(0) + public Solvers solver; + private Configuration config; private LogManager logger; private ShutdownNotifier notifier; private SolverContext context; - private static final String input = - "2..9.6..1\n" - + "..6.4...9\n" - + "...52.4..\n" - + "3.2..7.5.\n" - + "...2..1..\n" - + ".9.3..7..\n" - + ".87.5.31.\n" - + "6.3.1.8..\n" - + "4....9..."; - - private static final String sudokuSolution = - "248976531\n" - + "536148279\n" - + "179523468\n" - + "312487956\n" - + "764295183\n" - + "895361742\n" - + "987652314\n" - + "623714895\n" - + "451839627\n"; - - @Before + private static final String input = """ + 2..9.6..1 + ..6.4...9 + ...52.4.. + 3.2..7.5. + ...2..1.. + .9.3..7.. + .87.5.31. + 6.3.1.8.. + 4....9... + """; + + private static final String sudokuSolution = """ + 248976531 + 536148279 + 179523468 + 312487956 + 764295183 + 895361742 + 987652314 + 623714895 + 451839627 + """; + + @BeforeEach public void init() throws InvalidConfigurationException { + assumeTrue(Platform.isSupported(solver)); + config = Configuration.defaultConfiguration(); logger = BasicLogManager.create(config); notifier = ShutdownNotifier.createDummy(); @@ -109,7 +128,7 @@ public void init() throws InvalidConfigurationException { /* * We close our context after we are done with a solver to not waste memory. */ - @After + @AfterEach public final void closeSolver() { if (context != null) { context.close(); @@ -117,69 +136,14 @@ public final void closeSolver() { } @Test - public void princessSudokuTest() - throws InvalidConfigurationException, InterruptedException, SolverException { - checkSudoku(Solvers.PRINCESS); - } - - @Test - public void smtInterpolSudokuTest() - throws InvalidConfigurationException, InterruptedException, SolverException { - checkSudoku(Solvers.SMTINTERPOL); - } - - @Test - public void cvc4SudokuTest() - throws InvalidConfigurationException, InterruptedException, SolverException { - checkSudoku(Solvers.CVC4); - } - - @Test - public void z3SudokuTest() - throws InvalidConfigurationException, InterruptedException, SolverException { - checkSudoku(Solvers.Z3); - } - - @Test - public void mathsatSudokuTest() - throws InvalidConfigurationException, InterruptedException, SolverException { - checkSudoku(Solvers.MATHSAT5); - } - - @Test - public void boolectorSudokuTest() - throws InvalidConfigurationException, InterruptedException, SolverException { - // Boolector does not support Integers - checkSudokuWithBooleans(Solvers.BOOLECTOR); - } - - @Test - public void yicesSudokuTest() - throws InvalidConfigurationException, InterruptedException, SolverException { - checkSudoku(Solvers.YICES2); - } - - private void checkSudoku(Solvers solver) - throws InvalidConfigurationException, InterruptedException, SolverException { - - context = SolverContextFactory.createSolverContext(config, logger, notifier, solver); - Integer[][] grid = readGridFromString(input); - - SudokuSolver sudoku = new IntegerBasedSudokuSolver(context); - Integer[][] solution = sudoku.solve(grid); - - assertNotNull(solution); - assertEquals(sudokuSolution, solutionToString(solution)); - } - - // Same as checkSudoku but with Booleans instead of Integers - private void checkSudokuWithBooleans(Solvers solver) + public void checkSudoku() throws InvalidConfigurationException, InterruptedException, SolverException { + logger.log(Level.INFO, "Executing " + solver + "..."); context = SolverContextFactory.createSolverContext(config, logger, notifier, solver); Integer[][] grid = readGridFromString(input); - SudokuSolver sudoku = new BooleanBasedSudokuSolver(context); + SudokuSolver sudoku = new Sudoku.BooleanBasedSudokuSolver(context); Integer[][] solution = sudoku.solve(grid); assertNotNull(solution); @@ -200,8 +164,8 @@ private String solutionToString(Integer[][] solution) { *

Use digits 0-9 as values, other values will be set to 'unknown'. */ private Integer[][] readGridFromString(String puzzle) { - Integer[][] grid = new Integer[SIZE][SIZE]; List lines = Splitter.on('\n').splitToList(puzzle); + Integer[][] grid = new Integer[lines.size()][lines.size()]; for (int row = 0; row < lines.size(); row++) { for (int col = 0; col < lines.get(row).length(); col++) { diff --git a/doc/Example-Ivy-Project/README.md b/doc/Example-Ivy-Project/README.md new file mode 100644 index 0000000000..7e95a4d431 --- /dev/null +++ b/doc/Example-Ivy-Project/README.md @@ -0,0 +1,24 @@ + + +This is an example application for using JavaSMT with Ant/Ivy. +The example application prints a table of the available SMT solvers, along with their version +number and supported features. + +The project supports the following build targets: + +- `resolve` retrieve dependencies with Ivy +- `compile` compile the project +- `test` run the tests +- `package` build a .jar +- `run` run the program +- `clean` clean the project + +Calling `ant` with no target will build and then execute the project. diff --git a/doc/Example-Ivy-Project/build.xml b/doc/Example-Ivy-Project/build.xml new file mode 100644 index 0000000000..12125a0b4c --- /dev/null +++ b/doc/Example-Ivy-Project/build.xml @@ -0,0 +1,147 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/doc/Example-Ivy-Project/ivy.xml b/doc/Example-Ivy-Project/ivy.xml new file mode 100644 index 0000000000..bc4647e61b --- /dev/null +++ b/doc/Example-Ivy-Project/ivy.xml @@ -0,0 +1,29 @@ + + + + + + + + + + + + + + + + + + + + + diff --git a/doc/Example-Ivy-Project/lib/ivy-settings.xml b/doc/Example-Ivy-Project/lib/ivy-settings.xml new file mode 100644 index 0000000000..0f8c6e63e7 --- /dev/null +++ b/doc/Example-Ivy-Project/lib/ivy-settings.xml @@ -0,0 +1,30 @@ + + + + + + + + + + + + + + + + + + + + + diff --git a/doc/Example-Ivy-Project/src/main/org/sosy_lab/java_smt_example/SolverOverviewTable.java b/doc/Example-Ivy-Project/src/main/org/sosy_lab/java_smt_example/SolverOverviewTable.java new file mode 100644 index 0000000000..29ee5ab3b5 --- /dev/null +++ b/doc/Example-Ivy-Project/src/main/org/sosy_lab/java_smt_example/SolverOverviewTable.java @@ -0,0 +1,46 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2026 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt_example; + +import java.util.ArrayList; +import java.util.Comparator; +import java.util.List; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; +import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.example.SolverOverviewTable.RowBuilder; +import org.sosy_lab.java_smt.example.SolverOverviewTable.SolverInfo; + +/** + * This program takes all installed solvers and checks them for version, theories and features and + * prints them to StdOut in a nice table. + * + *

This is just a copy of org.sosy_lab.java_smt.example.SolverOverviewTable + */ +public class SolverOverviewTable { + + public static void main(String[] args) throws SolverException, InterruptedException { + + final org.sosy_lab.java_smt.example.SolverOverviewTable infoProvider = + new org.sosy_lab.java_smt.example.SolverOverviewTable(); + final List infos = new ArrayList<>(); + for (Solvers s : Solvers.values()) { + infos.add(infoProvider.getSolverInformation(s)); + } + + infos.sort(Comparator.comparing(SolverInfo::getName)); // alphabetical ordering + + RowBuilder rowBuilder = new RowBuilder(); + for (SolverInfo info : infos) { + rowBuilder.addSolver(info); + } + System.out.println(rowBuilder); + } + + private SolverOverviewTable() {} +} diff --git a/doc/Example-Ivy-Project/src/test/org/sosy_lab/java_smt_example/Platform.java b/doc/Example-Ivy-Project/src/test/org/sosy_lab/java_smt_example/Platform.java new file mode 100644 index 0000000000..2d11f8c731 --- /dev/null +++ b/doc/Example-Ivy-Project/src/test/org/sosy_lab/java_smt_example/Platform.java @@ -0,0 +1,76 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2026 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt_example; + +import com.google.common.base.StandardSystemProperty; +import java.util.Locale; +import org.sosy_lab.common.NativeLibraries; +import org.sosy_lab.java_smt.SolverContextFactory; + +class Platform { + private static final String OS = + StandardSystemProperty.OS_NAME.value().toLowerCase(Locale.getDefault()).replace(" ", ""); + private static final String ARCH = + StandardSystemProperty.OS_ARCH.value().toLowerCase(Locale.getDefault()).replace(" ", ""); + + private static final boolean IS_WINDOWS = OS.startsWith("windows"); + private static final boolean IS_MAC = OS.startsWith("macos"); + private static final boolean IS_LINUX = OS.startsWith("linux"); + + private static final boolean IS_ARCH_ARM64 = ARCH.equals("aarch64"); + + private static boolean isSufficientVersionOfLibcxx(String library) { + try { + NativeLibraries.loadLibrary(library); + } catch (UnsatisfiedLinkError e) { + for (String dependency : getRequiredLibcxx(library)) { + if (e.getMessage().contains("version `" + dependency + "' not found")) { + return false; + } + } + } + return true; + } + + private static String[] getRequiredLibcxx(String library) { + return switch (library) { + case "z3" -> new String[] {"GLIBC_2.34", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "bitwuzlaj" -> new String[] {"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "opensmtj" -> new String[] {"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "mathsat5j" -> new String[] {"GLIBC_2.33", "GLIBC_2.38"}; + case "cvc5jni" -> new String[] {"GLIBC_2.32"}; + case "yices2java" -> new String[] {"GLIBC_2.34"}; + default -> new String[] {}; + }; + } + + /** + * True if the solver is supported on the current operating system and CPU + * architecture + */ + static boolean isSupported(SolverContextFactory.Solvers solver) { + return switch (solver) { + case SMTINTERPOL, PRINCESS -> + // Any operating system and any architecture is allowed, Java is sufficient + true; + case BOOLECTOR, CVC4 -> IS_LINUX && !IS_ARCH_ARM64; + case YICES2 -> + (IS_LINUX && !IS_ARCH_ARM64 && isSufficientVersionOfLibcxx("yices2java")) + || (IS_WINDOWS && !IS_ARCH_ARM64); + case CVC5 -> (IS_LINUX && isSufficientVersionOfLibcxx("cvc5jni")) || IS_WINDOWS || IS_MAC; + case OPENSMT -> IS_LINUX && isSufficientVersionOfLibcxx("opensmtj"); + case BITWUZLA -> + (IS_LINUX && isSufficientVersionOfLibcxx("bitwuzlaj")) || (IS_WINDOWS && !IS_ARCH_ARM64); + case MATHSAT5 -> + (IS_LINUX && isSufficientVersionOfLibcxx("mathsat5j")) || (IS_WINDOWS && !IS_ARCH_ARM64); + case Z3 -> (IS_LINUX && isSufficientVersionOfLibcxx("z3")) || IS_WINDOWS || IS_MAC; + case Z3_WITH_INTERPOLATION -> IS_LINUX && !IS_ARCH_ARM64; + }; + } +} diff --git a/doc/Example-Gradle-Project-Kotlin/src/test/java/org/sosy_lab/java_smt_example/SudokuTest.java b/doc/Example-Ivy-Project/src/test/org/sosy_lab/java_smt_example/SudokuTest.java similarity index 51% rename from doc/Example-Gradle-Project-Kotlin/src/test/java/org/sosy_lab/java_smt_example/SudokuTest.java rename to doc/Example-Ivy-Project/src/test/org/sosy_lab/java_smt_example/SudokuTest.java index 7ee43a3133..5312791fe9 100644 --- a/doc/Example-Gradle-Project-Kotlin/src/test/java/org/sosy_lab/java_smt_example/SudokuTest.java +++ b/doc/Example-Ivy-Project/src/test/org/sosy_lab/java_smt_example/SudokuTest.java @@ -2,22 +2,20 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2021 Dirk Beyer +// SPDX-FileCopyrightText: 2026 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 package org.sosy_lab.java_smt_example; -import static org.junit.Assert.assertEquals; -import static org.junit.Assert.assertNotNull; -import static org.sosy_lab.java_smt.example.Sudoku.SIZE; - import com.google.common.base.Joiner; import com.google.common.base.Splitter; -import java.util.List; -import org.junit.After; -import org.junit.Before; -import org.junit.Test; +import org.junit.jupiter.api.AfterEach; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; +import org.junit.jupiter.params.Parameter; +import org.junit.jupiter.params.ParameterizedClass; +import org.junit.jupiter.params.provider.MethodSource; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; @@ -27,10 +25,18 @@ import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverException; -import org.sosy_lab.java_smt.example.Sudoku.IntegerBasedSudokuSolver; -import org.sosy_lab.java_smt.example.Sudoku.BooleanBasedSudokuSolver; +import org.sosy_lab.java_smt.example.Sudoku; import org.sosy_lab.java_smt.example.Sudoku.SudokuSolver; +import java.util.Arrays; +import java.util.List; +import java.util.logging.Level; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertNotNull; +import static org.junit.jupiter.api.Assumptions.assumeTrue; + + /** * This program parses a String-given Sudoku and solves it with an SMT solver. * @@ -69,41 +75,50 @@ * 451839627 * */ +@ParameterizedClass +@MethodSource("getAllSolvers") public class SudokuTest { + public static List getAllSolvers() { + return Arrays.asList(Solvers.values()); + } + + @Parameter(0) + public Solvers solver; + private Configuration config; private LogManager logger; private ShutdownNotifier notifier; private SolverContext context; - private static final String input = - "2..9.6..1\n" - + "..6.4...9\n" - + "...52.4..\n" - + "3.2..7.5.\n" - + "...2..1..\n" - + ".9.3..7..\n" - + ".87.5.31.\n" - + "6.3.1.8..\n" - + "4....9..."; - - private static final String sudokuSolution = - "248976531\n" - + "536148279\n" - + "179523468\n" - + "312487956\n" - + "764295183\n" - + "895361742\n" - + "987652314\n" - + "623714895\n" - + "451839627\n"; - - public SudokuTest() { - - } - - private void init() throws InvalidConfigurationException { + private static final String input = """ + 2..9.6..1 + ..6.4...9 + ...52.4.. + 3.2..7.5. + ...2..1.. + .9.3..7.. + .87.5.31. + 6.3.1.8.. + 4....9... + """; + + private static final String sudokuSolution = """ + 248976531 + 536148279 + 179523468 + 312487956 + 764295183 + 895361742 + 987652314 + 623714895 + 451839627 + """; + + @BeforeEach + public void init() throws InvalidConfigurationException { + assumeTrue(Platform.isSupported(solver)); config = Configuration.defaultConfiguration(); logger = BasicLogManager.create(config); notifier = ShutdownNotifier.createDummy(); @@ -112,83 +127,22 @@ private void init() throws InvalidConfigurationException { /* * We close our context after we are done with a solver to not waste memory. */ - private final void closeSolver() { + @AfterEach + public final void closeSolver() { if (context != null) { context.close(); } } - public void princessSudokuTest() - throws InvalidConfigurationException, InterruptedException, SolverException { - init(); - checkSudoku(Solvers.PRINCESS); - closeSolver(); - } - - public void smtInterpolSudokuTest() - throws InvalidConfigurationException, InterruptedException, SolverException { - init(); - checkSudoku(Solvers.SMTINTERPOL); - closeSolver(); - } - - public void cvc4SudokuTest() - throws InvalidConfigurationException, InterruptedException, SolverException { - init(); - checkSudoku(Solvers.CVC4); - closeSolver(); - } - - public void z3SudokuTest() - throws InvalidConfigurationException, InterruptedException, SolverException { - init(); - checkSudoku(Solvers.Z3); - closeSolver(); - } - - public void mathsatSudokuTest() - throws InvalidConfigurationException, InterruptedException, SolverException { - init(); - checkSudoku(Solvers.MATHSAT5); - closeSolver(); - } - - public void boolectorSudokuTest() - throws InvalidConfigurationException, InterruptedException, SolverException { - init(); - // Boolector does not support Integers - checkSudokuWithBooleans(Solvers.BOOLECTOR); - closeSolver(); - } - - public void yicesSudokuTest() - throws InvalidConfigurationException, InterruptedException, SolverException { - init(); - checkSudoku(Solvers.YICES2); - closeSolver(); - } - - private void checkSudoku(Solvers solver) - throws InvalidConfigurationException, InterruptedException, SolverException { - - context = SolverContextFactory.createSolverContext(config, logger, notifier, solver); - Integer[][] grid = readGridFromString(input); - - SudokuSolver sudoku = new IntegerBasedSudokuSolver(context); - Integer[][] solution = sudoku.solve(grid); - - assertNotNull(solution); - assertEquals(sudokuSolution, solutionToString(solution)); - } - - // Same as checkSudoku but with Booleans instead of Integers - private void checkSudokuWithBooleans(Solvers solver) - throws InvalidConfigurationException, InterruptedException, SolverException { + @Test + public void checkSudoku() + throws InvalidConfigurationException, InterruptedException, SolverException { + logger.log(Level.INFO, "Executing " + solver + "..."); context = SolverContextFactory.createSolverContext(config, logger, notifier, solver); Integer[][] grid = readGridFromString(input); - SudokuSolver sudoku = new BooleanBasedSudokuSolver(context); + SudokuSolver sudoku = new Sudoku.BooleanBasedSudokuSolver(context); Integer[][] solution = sudoku.solve(grid); assertNotNull(solution); @@ -209,8 +163,8 @@ private String solutionToString(Integer[][] solution) { *

Use digits 0-9 as values, other values will be set to 'unknown'. */ private Integer[][] readGridFromString(String puzzle) { - Integer[][] grid = new Integer[SIZE][SIZE]; List lines = Splitter.on('\n').splitToList(puzzle); + Integer[][] grid = new Integer[lines.size()][lines.size()]; for (int row = 0; row < lines.size(); row++) { for (int col = 0; col < lines.get(row).length(); col++) { diff --git a/doc/Example-Maven-Project/pom.xml b/doc/Example-Maven-Project/pom.xml index 1f550263f4..165bbacdbf 100644 --- a/doc/Example-Maven-Project/pom.xml +++ b/doc/Example-Maven-Project/pom.xml @@ -10,8 +10,9 @@ SPDX-FileCopyrightText: 2025 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> - + 4.0.0 org.sosy_lab.java_smt_example @@ -69,23 +70,29 @@ SPDX-License-Identifier: Apache-2.0 dependency ${project.build.directory}/${project.dependency.relativepath} - - x64 + + + 6.0.0-148-gba08f432a + 6.0.0-141-g04134287c - - 6.0.0 - 0.8.2-339-g550ed911 + + + 0.9.0-gd13ef925 3.2.2-g1a89c229 1.8-prerelease-2020-06-24-g7825d8f28 2026-02-26-d22638a 5.6.15 - 2.9.0-gef441e1c + 2.9.2-ge4c80308 2.5-1242-g5c50fb6d 2025-11-17 2.0 - 5.0.1-1258-gdad634a69 - 2.6.4-264-g553897f5 - 4.15.4 + 2.7.0-gdc5687ca + 4.15.0 4.5.0-gd57a2a6dc @@ -97,12 +104,14 @@ SPDX-License-Identifier: Apache-2.0 ${javasmt.version} - + de.uni-freiburg.informatik.ultimate smtinterpol ${smtinterpol.version} + + io.github.uuverifiers princess_2.13 @@ -114,143 +123,48 @@ SPDX-License-Identifier: Apache-2.0 ${ostrich.version} - - - org.sosy-lab - javasmt-solver-mathsat - ${mathsat.version} - libmathsat5j-${system.arch} - so - - - + org.sosy-lab javasmt-solver-z3 ${z3.version} - - org.sosy-lab - javasmt-solver-z3 - ${z3.version} - so - libz3-${system.arch} - - - org.sosy-lab - javasmt-solver-z3 - ${z3.version} - so - libz3java-${system.arch} - - + org.sosy-lab javasmt-solver-z3-legacy ${z3-legacy.version} com.microsoft.z3legacy - - org.sosy-lab - javasmt-solver-z3-legacy - ${z3-legacy.version} - so - libz3legacy-${system.arch} - - - org.sosy-lab - javasmt-solver-z3-legacy - ${z3-legacy.version} - so - libz3javalegacy-${system.arch} - - + org.sosy-lab javasmt-solver-bitwuzla ${bitwuzla.version} - - org.sosy-lab - javasmt-solver-bitwuzla - ${bitwuzla.version} - so - libbitwuzlaj-${system.arch} - - - - - org.sosy-lab - javasmt-solver-boolector - ${boolector.version} - so - libboolector - - - org.sosy-lab - javasmt-solver-boolector - ${boolector.version} - so - libminisat - - - org.sosy-lab - javasmt-solver-boolector - ${boolector.version} - so - libpicosat - - + org.sosy-lab javasmt-solver-cvc4 ${cvc4.version} CVC4 - - org.sosy-lab - javasmt-solver-cvc4 - ${cvc4.version} - so - libcvc4 - - - org.sosy-lab - javasmt-solver-cvc4 - ${cvc4.version} - so - libcvc4jni - - - org.sosy-lab - javasmt-solver-cvc4 - ${cvc4.version} - so - libcvc4parser - - - - org.sosy-lab - javasmt-solver-cvc5 - ${cvc5.version} - + org.sosy-lab javasmt-solver-cvc5 ${cvc5.version} - so - libcvc5jni-${system.arch} - + org.sosy-lab javasmt-yices2 - ${javasmt-yices.version} + ${javasmt-yices.version} org.sosy-lab @@ -261,34 +175,416 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-yices2 - ${yices.version} - so - libyices2j + ${yices.version} - - - org.sosy-lab - javasmt-solver-opensmt - ${opensmt.version} - + org.sosy-lab javasmt-solver-opensmt ${opensmt.version} - so - libopensmtj-${system.arch} - junit - junit - 4.13.2 + org.junit.jupiter + junit-jupiter-api + 6.1.0 + test + + + org.junit.jupiter + junit-jupiter-params + 6.1.0 + test + + + org.junit.jupiter + junit-jupiter-engine + 6.1.0 test + + + x64-linux + + + linux + amd64 + + + + + + org.sosy-lab + javasmt-solver-mathsat + ${mathsat.version} + libmathsat5j-x64 + so + + + + + org.sosy-lab + javasmt-solver-z3 + ${z3.version} + so + libz3-x64 + + + org.sosy-lab + javasmt-solver-z3 + ${z3.version} + so + libz3java-x64 + + + + + org.sosy-lab + javasmt-solver-z3-legacy + ${z3-legacy.version} + so + libz3legacy-x64 + + + org.sosy-lab + javasmt-solver-z3-legacy + ${z3-legacy.version} + so + libz3javalegacy-x64 + + + + + org.sosy-lab + javasmt-solver-bitwuzla + ${bitwuzla.version} + so + libbitwuzlaj-x64 + + + + + org.sosy-lab + javasmt-solver-boolector + ${boolector.version} + so + libboolector + + + org.sosy-lab + javasmt-solver-boolector + ${boolector.version} + so + libminisat + + + org.sosy-lab + javasmt-solver-boolector + ${boolector.version} + so + libpicosat + + + + + org.sosy-lab + javasmt-solver-cvc4 + ${cvc4.version} + so + libcvc4 + + + org.sosy-lab + javasmt-solver-cvc4 + ${cvc4.version} + so + libcvc4jni + + + org.sosy-lab + javasmt-solver-cvc4 + ${cvc4.version} + so + libcvc4parser + + + + + org.sosy-lab + javasmt-solver-cvc5 + ${cvc5.version} + so + libcvc5jni-x64 + + + + + org.sosy-lab + javasmt-solver-yices2 + ${yices.version} + so + libyices2java-x64 + + + + + org.sosy-lab + javasmt-solver-opensmt + ${opensmt.version} + so + libopensmtj-x64 + + + + + arm64-linux + + + linux + aarch64 + + + + + + org.sosy-lab + javasmt-solver-mathsat + ${mathsat.version} + libmathsat5j-arm64 + so + + + + + org.sosy-lab + javasmt-solver-z3 + ${z3.version} + so + libz3-arm64 + + + org.sosy-lab + javasmt-solver-z3 + ${z3.version} + so + libz3java-arm64 + + + + + org.sosy-lab + javasmt-solver-bitwuzla + ${bitwuzla.version} + so + libbitwuzlaj-arm64 + + + + + org.sosy-lab + javasmt-solver-cvc5 + ${cvc5.version} + so + libcvc5jni-arm64 + + + + + org.sosy-lab + javasmt-solver-opensmt + ${opensmt.version} + so + libopensmtj-arm64 + + + + + x64-windows + + + windows + amd64 + + + + + + org.sosy-lab + javasmt-solver-mathsat + ${mathsat.version} + mathsat5j-x64 + dll + + + org.sosy-lab + javasmt-solver-mathsat + ${mathsat.version} + mathsat-x64 + dll + + + org.sosy-lab + javasmt-solver-mathsat + ${mathsat.version} + gmp-x64 + dll + + + + + org.sosy-lab + javasmt-solver-z3 + ${z3.version} + dll + libz3-x64 + + + org.sosy-lab + javasmt-solver-z3 + ${z3.version} + dll + libz3java-x64 + + + + + org.sosy-lab + javasmt-solver-bitwuzla + ${bitwuzla.version} + dll + libbitwuzlaj-x64 + + + + + org.sosy-lab + javasmt-solver-cvc5 + ${cvc5.version} + dll + libcvc5jni-x64 + + + + + org.sosy-lab + javasmt-solver-yices2 + ${yices.version} + dll + yices2java-x64 + + + + + arm64-windows + + + windows + aarch64 + + + + + + org.sosy-lab + javasmt-solver-z3 + ${z3.version} + dll + libz3-arm64 + + + org.sosy-lab + javasmt-solver-z3 + ${z3.version} + dll + libz3java-arm64 + + + + + org.sosy-lab + javasmt-solver-cvc5 + ${cvc5.version} + dll + libcvc5jni-arm64 + + + + + x64-macosx + + + mac + x86_64 + + + + + + org.sosy-lab + javasmt-solver-z3 + ${z3.version} + dylib + libz3-x64 + + + org.sosy-lab + javasmt-solver-z3 + ${z3.version} + dylib + libz3java-x64 + + + + + org.sosy-lab + javasmt-solver-cvc5 + ${cvc5.version} + dylib + libcvc5jni-x64 + + + + + arm64-macosx + + + mac + aarch64 + + + + + + org.sosy-lab + javasmt-solver-z3 + ${z3.version} + dylib + libz3-arm64 + + + org.sosy-lab + javasmt-solver-z3 + ${z3.version} + dylib + libz3java-arm64 + + + + + org.sosy-lab + javasmt-solver-cvc5 + ${cvc5.version} + dylib + libcvc5jni-arm64 + + + + + @@ -387,7 +683,9 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/doc/Example-Maven-Project/src/test/java/org/sosy_lab/java_smt_example/Platform.java b/doc/Example-Maven-Project/src/test/java/org/sosy_lab/java_smt_example/Platform.java new file mode 100644 index 0000000000..2d11f8c731 --- /dev/null +++ b/doc/Example-Maven-Project/src/test/java/org/sosy_lab/java_smt_example/Platform.java @@ -0,0 +1,76 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2026 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt_example; + +import com.google.common.base.StandardSystemProperty; +import java.util.Locale; +import org.sosy_lab.common.NativeLibraries; +import org.sosy_lab.java_smt.SolverContextFactory; + +class Platform { + private static final String OS = + StandardSystemProperty.OS_NAME.value().toLowerCase(Locale.getDefault()).replace(" ", ""); + private static final String ARCH = + StandardSystemProperty.OS_ARCH.value().toLowerCase(Locale.getDefault()).replace(" ", ""); + + private static final boolean IS_WINDOWS = OS.startsWith("windows"); + private static final boolean IS_MAC = OS.startsWith("macos"); + private static final boolean IS_LINUX = OS.startsWith("linux"); + + private static final boolean IS_ARCH_ARM64 = ARCH.equals("aarch64"); + + private static boolean isSufficientVersionOfLibcxx(String library) { + try { + NativeLibraries.loadLibrary(library); + } catch (UnsatisfiedLinkError e) { + for (String dependency : getRequiredLibcxx(library)) { + if (e.getMessage().contains("version `" + dependency + "' not found")) { + return false; + } + } + } + return true; + } + + private static String[] getRequiredLibcxx(String library) { + return switch (library) { + case "z3" -> new String[] {"GLIBC_2.34", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "bitwuzlaj" -> new String[] {"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "opensmtj" -> new String[] {"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "mathsat5j" -> new String[] {"GLIBC_2.33", "GLIBC_2.38"}; + case "cvc5jni" -> new String[] {"GLIBC_2.32"}; + case "yices2java" -> new String[] {"GLIBC_2.34"}; + default -> new String[] {}; + }; + } + + /** + * True if the solver is supported on the current operating system and CPU + * architecture + */ + static boolean isSupported(SolverContextFactory.Solvers solver) { + return switch (solver) { + case SMTINTERPOL, PRINCESS -> + // Any operating system and any architecture is allowed, Java is sufficient + true; + case BOOLECTOR, CVC4 -> IS_LINUX && !IS_ARCH_ARM64; + case YICES2 -> + (IS_LINUX && !IS_ARCH_ARM64 && isSufficientVersionOfLibcxx("yices2java")) + || (IS_WINDOWS && !IS_ARCH_ARM64); + case CVC5 -> (IS_LINUX && isSufficientVersionOfLibcxx("cvc5jni")) || IS_WINDOWS || IS_MAC; + case OPENSMT -> IS_LINUX && isSufficientVersionOfLibcxx("opensmtj"); + case BITWUZLA -> + (IS_LINUX && isSufficientVersionOfLibcxx("bitwuzlaj")) || (IS_WINDOWS && !IS_ARCH_ARM64); + case MATHSAT5 -> + (IS_LINUX && isSufficientVersionOfLibcxx("mathsat5j")) || (IS_WINDOWS && !IS_ARCH_ARM64); + case Z3 -> (IS_LINUX && isSufficientVersionOfLibcxx("z3")) || IS_WINDOWS || IS_MAC; + case Z3_WITH_INTERPOLATION -> IS_LINUX && !IS_ARCH_ARM64; + }; + } +} diff --git a/doc/Example-Maven-Project/src/test/java/org/sosy_lab/java_smt_example/SudokuTest.java b/doc/Example-Maven-Project/src/test/java/org/sosy_lab/java_smt_example/SudokuTest.java index 83c900d860..8481060769 100644 --- a/doc/Example-Maven-Project/src/test/java/org/sosy_lab/java_smt_example/SudokuTest.java +++ b/doc/Example-Maven-Project/src/test/java/org/sosy_lab/java_smt_example/SudokuTest.java @@ -8,21 +8,14 @@ package org.sosy_lab.java_smt_example; -import static org.junit.Assert.assertEquals; -import static org.junit.Assert.assertNotNull; -import static org.junit.Assume.assumeTrue; -import static org.sosy_lab.java_smt.example.Sudoku.SIZE; - import com.google.common.base.Joiner; import com.google.common.base.Splitter; -import java.util.Arrays; -import java.util.List; -import java.util.logging.Level; -import org.junit.After; -import org.junit.Before; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; +import org.junit.jupiter.api.AfterEach; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; +import org.junit.jupiter.params.Parameter; +import org.junit.jupiter.params.ParameterizedClass; +import org.junit.jupiter.params.provider.MethodSource; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; @@ -35,6 +28,15 @@ import org.sosy_lab.java_smt.example.Sudoku; import org.sosy_lab.java_smt.example.Sudoku.SudokuSolver; +import java.util.Arrays; +import java.util.List; +import java.util.logging.Level; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertNotNull; +import static org.junit.jupiter.api.Assumptions.assumeTrue; + + /** * This program parses a String-given Sudoku and solves it with an SMT solver. * @@ -73,59 +75,51 @@ * 451839627 * */ -@RunWith(Parameterized.class) +@ParameterizedClass +@MethodSource("getAllSolvers") public class SudokuTest { - @Parameterized.Parameters(name = "{0}") - public static List getSolvers() { + public static List getAllSolvers() { return Arrays.asList(Solvers.values()); } - @Parameterized.Parameter(0) + @Parameter(0) public Solvers solver; - private static final String OS = System.getProperty("os.name").toLowerCase().replace(" ", ""); - private static final boolean IS_LINUX = OS.startsWith("linux"); - private static final boolean IS_X64 = System.getProperty("os.arch").contains("64"); - - /** Disable some checks on certain combinations of operating systems and solvers, because of missing dependencies. */ - private static boolean isOperatingSystemSupported(Solvers solver) { - return switch (solver) { - case SMTINTERPOL, PRINCESS -> true; // Java-based solvers should work on all platforms - default -> IS_LINUX && IS_X64; // this example only includes Linux x64 binaries for native solvers - }; - } - private Configuration config; private LogManager logger; private ShutdownNotifier notifier; private SolverContext context; - private static final String input = - "2..9.6..1\n" - + "..6.4...9\n" - + "...52.4..\n" - + "3.2..7.5.\n" - + "...2..1..\n" - + ".9.3..7..\n" - + ".87.5.31.\n" - + "6.3.1.8..\n" - + "4....9..."; - - private static final String sudokuSolution = - "248976531\n" - + "536148279\n" - + "179523468\n" - + "312487956\n" - + "764295183\n" - + "895361742\n" - + "987652314\n" - + "623714895\n" - + "451839627\n"; - - @Before + private static final String input = """ + 2..9.6..1 + ..6.4...9 + ...52.4.. + 3.2..7.5. + ...2..1.. + .9.3..7.. + .87.5.31. + 6.3.1.8.. + 4....9... + """; + + private static final String sudokuSolution = """ + 248976531 + 536148279 + 179523468 + 312487956 + 764295183 + 895361742 + 987652314 + 623714895 + 451839627 + """; + + @BeforeEach public void init() throws InvalidConfigurationException { + assumeTrue(Platform.isSupported(solver)); + config = Configuration.defaultConfiguration(); logger = BasicLogManager.create(config); notifier = ShutdownNotifier.createDummy(); @@ -134,7 +128,7 @@ public void init() throws InvalidConfigurationException { /* * We close our context after we are done with a solver to not waste memory. */ - @After + @AfterEach public final void closeSolver() { if (context != null) { context.close(); @@ -144,8 +138,6 @@ public final void closeSolver() { @Test public void checkSudoku() throws InvalidConfigurationException, InterruptedException, SolverException { - assumeTrue(isOperatingSystemSupported(solver)); - logger.log(Level.INFO, "Executing " + solver + "..."); context = SolverContextFactory.createSolverContext(config, logger, notifier, solver); @@ -172,8 +164,8 @@ private String solutionToString(Integer[][] solution) { *

Use digits 0-9 as values, other values will be set to 'unknown'. */ private Integer[][] readGridFromString(String puzzle) { - Integer[][] grid = new Integer[SIZE][SIZE]; List lines = Splitter.on('\n').splitToList(puzzle); + Integer[][] grid = new Integer[lines.size()][lines.size()]; for (int row = 0; row < lines.size(); row++) { for (int col = 0; col < lines.get(row).length(); col++) { diff --git a/doc/Example-Maven-Web-Project/Dockerfile b/doc/Example-Maven-Web-Project/Dockerfile index 01a3683671..40695f80bb 100644 --- a/doc/Example-Maven-Web-Project/Dockerfile +++ b/doc/Example-Maven-Web-Project/Dockerfile @@ -15,6 +15,7 @@ ENV DEBIAN_FRONTEND=noninteractive RUN apt-get update && apt-get install -y \ openjdk-17-jdk \ tomcat10 \ + libgomp1 \ && rm -rf /var/lib/apt/lists/* # 2. Set the environment so Tomcat knows where everything is diff --git a/doc/Example-Maven-Web-Project/pom.xml b/doc/Example-Maven-Web-Project/pom.xml index c95f4ce0a2..20ce6df69d 100644 --- a/doc/Example-Maven-Web-Project/pom.xml +++ b/doc/Example-Maven-Web-Project/pom.xml @@ -73,20 +73,29 @@ SPDX-License-Identifier: Apache-2.0 x64 - - 6.0.0 - 0.8.2-339-g550ed911 + + + 6.0.0-148-gba08f432a + 6.0.0-141-g04134287c + + + + 0.9.0-gd13ef925 3.2.2-g1a89c229 1.8-prerelease-2020-06-24-g7825d8f28 2026-02-26-d22638a 5.6.15 - 2.9.0-gef441e1c + 2.9.2-ge4c80308 2.5-1242-g5c50fb6d 2025-11-17 2.0 - 5.0.1-1258-gdad634a69 - 2.6.4-264-g553897f5 - 4.15.4 + 2.7.0-gdc5687ca + 4.16.0 4.5.0-gd57a2a6dc @@ -247,11 +256,11 @@ SPDX-License-Identifier: Apache-2.0 libcvc5jni-${system.arch} - + org.sosy-lab javasmt-yices2 - ${javasmt-yices.version} + ${javasmt-yices.version} org.sosy-lab @@ -262,9 +271,14 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-yices2 - ${yices.version} + ${yices.version} + + + org.sosy-lab + javasmt-solver-yices2 + ${yices.version} so - libyices2j + libyices2java-${system.arch} @@ -283,9 +297,21 @@ SPDX-License-Identifier: Apache-2.0 - junit - junit - 4.13.2 + org.junit.jupiter + junit-jupiter-api + 6.1.0 + test + + + org.junit.jupiter + junit-jupiter-params + 6.1.0 + test + + + org.junit.jupiter + junit-jupiter-engine + 6.1.0 test diff --git a/doc/Example-Maven-Web-Project/src/test/java/org/sosy_lab/java_smt_web_example/Platform.java b/doc/Example-Maven-Web-Project/src/test/java/org/sosy_lab/java_smt_web_example/Platform.java new file mode 100644 index 0000000000..ff0f514d18 --- /dev/null +++ b/doc/Example-Maven-Web-Project/src/test/java/org/sosy_lab/java_smt_web_example/Platform.java @@ -0,0 +1,76 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2026 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt_web_example; + +import com.google.common.base.StandardSystemProperty; +import java.util.Locale; +import org.sosy_lab.common.NativeLibraries; +import org.sosy_lab.java_smt.SolverContextFactory; + +class Platform { + private static final String OS = + StandardSystemProperty.OS_NAME.value().toLowerCase(Locale.getDefault()).replace(" ", ""); + private static final String ARCH = + StandardSystemProperty.OS_ARCH.value().toLowerCase(Locale.getDefault()).replace(" ", ""); + + private static final boolean IS_WINDOWS = OS.startsWith("windows"); + private static final boolean IS_MAC = OS.startsWith("macos"); + private static final boolean IS_LINUX = OS.startsWith("linux"); + + private static final boolean IS_ARCH_ARM64 = ARCH.equals("aarch64"); + + private static boolean isSufficientVersionOfLibcxx(String library) { + try { + NativeLibraries.loadLibrary(library); + } catch (UnsatisfiedLinkError e) { + for (String dependency : getRequiredLibcxx(library)) { + if (e.getMessage().contains("version `" + dependency + "' not found")) { + return false; + } + } + } + return true; + } + + private static String[] getRequiredLibcxx(String library) { + return switch (library) { + case "z3" -> new String[] {"GLIBC_2.34", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "bitwuzlaj" -> new String[] {"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "opensmtj" -> new String[] {"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "mathsat5j" -> new String[] {"GLIBC_2.33", "GLIBC_2.38"}; + case "cvc5jni" -> new String[] {"GLIBC_2.32"}; + case "yices2java" -> new String[] {"GLIBC_2.34"}; + default -> new String[] {}; + }; + } + + /** + * True if the solver is supported on the current operating system and CPU + * architecture + */ + static boolean isSupported(SolverContextFactory.Solvers solver) { + return switch (solver) { + case SMTINTERPOL, PRINCESS -> + // Any operating system and any architecture is allowed, Java is sufficient + true; + case BOOLECTOR, CVC4 -> IS_LINUX && !IS_ARCH_ARM64; + case YICES2 -> + (IS_LINUX && !IS_ARCH_ARM64 && isSufficientVersionOfLibcxx("yices2java")) + || (IS_WINDOWS && !IS_ARCH_ARM64); + case CVC5 -> (IS_LINUX && isSufficientVersionOfLibcxx("cvc5jni")) || IS_WINDOWS || IS_MAC; + case OPENSMT -> IS_LINUX && isSufficientVersionOfLibcxx("opensmtj"); + case BITWUZLA -> + (IS_LINUX && isSufficientVersionOfLibcxx("bitwuzlaj")) || (IS_WINDOWS && !IS_ARCH_ARM64); + case MATHSAT5 -> + (IS_LINUX && isSufficientVersionOfLibcxx("mathsat5j")) || (IS_WINDOWS && !IS_ARCH_ARM64); + case Z3 -> (IS_LINUX && isSufficientVersionOfLibcxx("z3")) || IS_WINDOWS || IS_MAC; + case Z3_WITH_INTERPOLATION -> IS_LINUX && !IS_ARCH_ARM64; + }; + } +} diff --git a/doc/Example-Maven-Web-Project/src/test/java/org/sosy_lab/java_smt_web_example/SudokuTest.java b/doc/Example-Maven-Web-Project/src/test/java/org/sosy_lab/java_smt_web_example/SudokuTest.java index d59de501fd..2be5e73bec 100644 --- a/doc/Example-Maven-Web-Project/src/test/java/org/sosy_lab/java_smt_web_example/SudokuTest.java +++ b/doc/Example-Maven-Web-Project/src/test/java/org/sosy_lab/java_smt_web_example/SudokuTest.java @@ -8,21 +8,16 @@ package org.sosy_lab.java_smt_web_example; -import static org.junit.Assert.assertEquals; -import static org.junit.Assert.assertNotNull; -import static org.junit.Assume.assumeTrue; -import static org.sosy_lab.java_smt.example.Sudoku.SIZE; - import com.google.common.base.Joiner; import com.google.common.base.Splitter; -import java.util.Arrays; -import java.util.List; -import java.util.logging.Level; -import org.junit.After; -import org.junit.Before; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; +import com.google.common.base.StandardSystemProperty; +import org.junit.jupiter.api.AfterEach; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; +import org.junit.jupiter.params.Parameter; +import org.junit.jupiter.params.ParameterizedClass; +import org.junit.jupiter.params.provider.MethodSource; +import org.sosy_lab.common.NativeLibraries; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; @@ -35,6 +30,16 @@ import org.sosy_lab.java_smt.example.Sudoku; import org.sosy_lab.java_smt.example.Sudoku.SudokuSolver; +import java.util.Arrays; +import java.util.List; +import java.util.Locale; +import java.util.logging.Level; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertNotNull; +import static org.junit.jupiter.api.Assumptions.assumeTrue; + + /** * This program parses a String-given Sudoku and solves it with an SMT solver. * @@ -73,59 +78,51 @@ * 451839627 * */ -@RunWith(Parameterized.class) +@ParameterizedClass +@MethodSource("getAllSolvers") public class SudokuTest { - @Parameterized.Parameters(name = "{0}") - public static List getSolvers() { + public static List getAllSolvers() { return Arrays.asList(Solvers.values()); } - @Parameterized.Parameter(0) + @Parameter(0) public Solvers solver; - private static final String OS = System.getProperty("os.name").toLowerCase().replace(" ", ""); - private static final boolean IS_LINUX = OS.startsWith("linux"); - private static final boolean IS_X64 = System.getProperty("os.arch").contains("64"); - - /** Disable some checks on certain combinations of operating systems and solvers, because of missing dependencies. */ - private static boolean isOperatingSystemSupported(Solvers solver) { - return switch (solver) { - case SMTINTERPOL, PRINCESS -> true; // Java-based solvers should work on all platforms - default -> IS_LINUX && IS_X64; // this example only includes Linux x64 binaries for native solvers - }; - } - private Configuration config; private LogManager logger; private ShutdownNotifier notifier; private SolverContext context; - private static final String input = - "2..9.6..1\n" - + "..6.4...9\n" - + "...52.4..\n" - + "3.2..7.5.\n" - + "...2..1..\n" - + ".9.3..7..\n" - + ".87.5.31.\n" - + "6.3.1.8..\n" - + "4....9..."; - - private static final String sudokuSolution = - "248976531\n" - + "536148279\n" - + "179523468\n" - + "312487956\n" - + "764295183\n" - + "895361742\n" - + "987652314\n" - + "623714895\n" - + "451839627\n"; - - @Before + private static final String input = """ + 2..9.6..1 + ..6.4...9 + ...52.4.. + 3.2..7.5. + ...2..1.. + .9.3..7.. + .87.5.31. + 6.3.1.8.. + 4....9... + """; + + private static final String sudokuSolution = """ + 248976531 + 536148279 + 179523468 + 312487956 + 764295183 + 895361742 + 987652314 + 623714895 + 451839627 + """; + + @BeforeEach public void init() throws InvalidConfigurationException { + assumeTrue(Platform.isSupported(solver)); + config = Configuration.defaultConfiguration(); logger = BasicLogManager.create(config); notifier = ShutdownNotifier.createDummy(); @@ -134,7 +131,7 @@ public void init() throws InvalidConfigurationException { /* * We close our context after we are done with a solver to not waste memory. */ - @After + @AfterEach public final void closeSolver() { if (context != null) { context.close(); @@ -144,8 +141,6 @@ public final void closeSolver() { @Test public void checkSudoku() throws InvalidConfigurationException, InterruptedException, SolverException { - assumeTrue(isOperatingSystemSupported(solver)); - logger.log(Level.INFO, "Executing " + solver + "..."); context = SolverContextFactory.createSolverContext(config, logger, notifier, solver); @@ -172,8 +167,8 @@ private String solutionToString(Integer[][] solution) { *

Use digits 0-9 as values, other values will be set to 'unknown'. */ private Integer[][] readGridFromString(String puzzle) { - Integer[][] grid = new Integer[SIZE][SIZE]; List lines = Splitter.on('\n').splitToList(puzzle); + Integer[][] grid = new Integer[lines.size()][lines.size()]; for (int row = 0; row < lines.size(); row++) { for (int col = 0; col < lines.get(row).length(); col++) { diff --git a/doc/Getting-started.md b/doc/Getting-started.md index 0e5bcde1bd..9cf29954be 100644 --- a/doc/Getting-started.md +++ b/doc/Getting-started.md @@ -28,6 +28,28 @@ After the repository URL is configured, you only need to add the following depen ``` +Solvers that are not needed can be excluded from the download: +```xml + + + + +``` + +By removing the dependency and then adding it back in, it is also possible to manually override the solver version: +```xml + + + + + + +``` +However, note that this should be done with caution as it may often lead to compatibility issues + #### Architecture specification and Operating System The support for operating systems depends on the solver, @@ -127,6 +149,11 @@ The XML snippets for other solvers available via Maven, such as `Boolector`, `CVC4`, `CVC5`, `OpenSMT`, `Princess`, and `Yices2`, can be found in the [`POM file`](Example-Maven-Project/pom.xml) of our [`Example-Maven-Project`](Example-Maven-Project). +The latest supported solver versions can be found in the Maven example project under +[`Example-Maven-Project/pom.xml`](Example-Maven-Project/pom.xml). It may sometimes be possible to use a newer version of a solver, or downgrade to +an older release. However, this should be done with caution as JavaSMT releases are generally tied to specific solver +version, and any change may lead to compatibility issues. + If you are not using Linux, but Windows or macOS, or if you want to use a different architecture, such as `arm64`, you might need to set the dependencies accordingly, e.g., change the type from `so` to `dll` (for Windows) or `dylib` (for macOS),