Upgrade cvc to 1.3.4

.github/workflows/build-and-run-tests.yml

@@ -14,6 +14,9 @@ jobs:
   run_tests:
     name: Run tests
     strategy:
+      # Without this a failure on one platform cancels the others, and the
+      # cancellation is what gets reported, hiding the actual failure.
+      fail-fast: false
       matrix:
         os: [ ubuntu-22.04, windows-latest, macos-latest ]
 

README.md

@@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features:
 * Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings
 
 [![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml)
-[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.6.5)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.6.6)
 [![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core)
 
 ## Get started
@@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/):
 
 ```kotlin
 // core 
-implementation("io.ksmt:ksmt-core:0.6.5")
+implementation("io.ksmt:ksmt-core:0.6.6")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.6.5")
+implementation("io.ksmt:ksmt-z3:0.6.6")
 ```
 
 Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the 

buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts

@@ -11,7 +11,7 @@ plugins {
 }
 
 group = "io.ksmt"
-version = "0.6.5"
+version = "0.6.6"
 
 repositories {
     mavenCentral()

docs/getting-started.md

@@ -34,7 +34,7 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("io.ksmt:ksmt-core:0.6.5")    
+    implementation("io.ksmt:ksmt-core:0.6.6")    
 }
 ```
 
@@ -43,9 +43,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("io.ksmt:ksmt-z3:0.6.5")
+    implementation("io.ksmt:ksmt-z3:0.6.6")
     // bitwuzla
-    implementation("io.ksmt:ksmt-bitwuzla:0.6.5")
+    implementation("io.ksmt:ksmt-bitwuzla:0.6.6")
 }
 ```
 

examples/build.gradle.kts

@@ -9,11 +9,11 @@ repositories {
 
 dependencies {
     // core
-    implementation("io.ksmt:ksmt-core:0.6.5")
+    implementation("io.ksmt:ksmt-core:0.6.6")
     // z3 solver
-    implementation("io.ksmt:ksmt-z3:0.6.5")
+    implementation("io.ksmt:ksmt-z3:0.6.6")
     // Runner and portfolio solver
-    implementation("io.ksmt:ksmt-runner:0.6.5")
+    implementation("io.ksmt:ksmt-runner:0.6.6")
 }
 
 java {

ksmt-cvc5/dist/build.md

@@ -1,68 +1,165 @@
-### Build details
+# cvc5 distribution for ksmt
 
-Build is based on the cvc5 fork: https://github.com/Saloed/cvc5/tree/ksmt
-This fork provides fixed Java API and buildscripts (`build_(linux|windows|mac).sh`)
+`ksmt-cvc5-core` compiles against `cvc5-<version>.jar` and `ksmt-cvc5-native` ships one
+`cvc5-native-<platform>-<version>.zip` per platform, consumed as a `flatDir` dependency.
+The libraries in each zip are loaded, in order, by the matching
+`KCvc5NativeLibraryLoader*` in `ksmt-cvc5-native`.
+
+| Artifact | Contents | Origin |
+| --- | --- | --- |
+| `cvc5-<version>.jar` | `io.github.cvc5.*` classes, no natives | built from the fork (see below) |
+| `cvc5-native-linux-x86-64-<version>.zip` | `libcvc5.so.1`, `libcvc5parser.so.1`, `libcvc5jni.so` | built from the fork |
+| `cvc5-native-win-x86-64-<version>.zip` | `libcvc5jni.dll` | official cvc5 release |
+| `cvc5-native-osx-arm64-<version>.zip` | `libcvc5jni.dylib` | official cvc5 release |
+
+The jar must always come from the same cvc5 patch release as the native libraries:
+`Kind` constants are generated from the C++ headers and new kinds are inserted mid-list,
+so `Kind` ordinals shift between releases.
+
+## The fork
+
+Build is based on the cvc5 fork <https://github.com/Saloed/cvc5>, branch `ksmt-<version>`
+(`ksmt` for the 1.3.0-era builds). It is a two-commit patch series on top of the upstream
+release tag, and is refreshed by rebasing those two commits onto the new tag:
 
-We build cvc5 with the following configuration:
 ```shell
-./configure.sh production --auto-download --ipo --no-static --no-cln --no-glpk --no-editline --cryptominisat --java-bindings
+git rebase --onto cvc5-<new version> cvc5-<old version> <branch>
 ```
-To make our distribution portable we statically link cvc5 against `libgmp`.
 
-#### Building on Windows
-To produce Windows builds we use the same approach as in [`ksmt-bitwuzla`](../../ksmt-bitwuzla/dist/build.md).
-Also, we use addition configuration flag:
+**`disable library load`** — patches the Java API:
+
+* `AbstractPointer` and `IPointer` are made `public`. `KCvc5TermManager` uses
+  `AbstractPointer` as a generic bound and calls `getPointer()`/`deletePointer()` on it.
+* `Context`'s global pointer registry is disabled (`TRACK_POINTERS = false`). Upstream
+  registers *every* `Term`/`Sort`/`Op` in a static map that is only drained by
+  `Context.deletePointers()`. ksmt manages cvc5 objects per solver via `KCvc5TermManager`
+  and never calls that JVM-global method, so the registry would retain every term ksmt
+  ever creates.
+* cvc5 does not load its native libraries from its own static initializers. ksmt ships
+  the libraries in its own resource layout and loads them explicitly
+  (`KCvc5NativeLibraryLoader`). This is belt-and-braces: `KCvc5Solver` also sets
+  `-Dcvc5.skipLibraryLoad=true`, which upstream honours.
+
+**`Fix build`** — adds `build_(linux|windows|mac).sh` and cmake fixes: libpoly is linked
+statically even for a shared cvc5 build, `CMAKE_AR` is honoured when cross-compiling, and
+the macOS deployment target is pinned.
+
+## Building linux-x86-64
+
+Built in an AlmaLinux 8 container, which provides a glibc (2.28) older than any supported
+distribution together with a C++17 toolchain. Do **not** use the official Linux release
+artifacts: they require glibc 2.33 and export ~1350 `std::` symbols, which interpose on
+the C++ runtime of the other native solvers in the same JVM.
+
 ```shell
-./configure.sh ... --win64-native
+docker run --rm -v "$PWD:/work" -e "HOST_UID=$(id -u)" -e "HOST_GID=$(id -g)" \
+    -w /work almalinux:8 bash /work/cvc5/build_linux.sh
+
+cd linux-dist/dist
+zip -X -9 "cvc5-native-linux-x86-64-<version>.zip" libcvc5jni.so libcvc5parser.so.1 libcvc5.so.1
 ```
 
-### Expected dynamic dependencies
-To ensure that our distribution is portable, we verify that the produced binaries have no dependencies that might not be present on the user's machine.
+with the fork checked out in `./cvc5`. See `build_linux.sh` in the fork for the full
+recipe; the parts that matter are:
+
+* `./configure.sh production --auto-download --ipo --no-static --no-cln --no-glpk
+  --no-editline --java-bindings`
+* `LDFLAGS="-static-libgcc -static-libstdc++ -Wl,--exclude-libs=ALL"`. The static linking
+  keeps the libraries independent of the host C++ runtime; `--exclude-libs=ALL` is
+  **required** to keep those statically linked symbols out of the dynamic symbol table,
+  otherwise they interpose on the libstdc++ used by the Bitwuzla / Z3 / Yices libraries
+  loaded into the same JVM and crash it with a SIGSEGV.
+* GMP is built statically and separately, because for a shared cvc5 build cvc5 would
+  otherwise produce a shared GMP that we would have to ship as a fourth library.
+* The jar is built with JDK 8 — ksmt targets Java 8.
+* Since 1.3.4 `libcvc5.so.1` and `libcvc5parser.so.1` are symlinks to the fully versioned
+  files, so packaging must dereference them (`cp -L`).
+
+## Windows x64 and macOS arm64
+
+Taken from the official [cvc5 release](https://github.com/cvc5/cvc5/releases). Since
+cvc5 1.3.2 the `cvc5-<platform>-java-api.jar` release assets contain a single,
+self-contained JNI library under `cvc5-libs/<os>/<arch>/` with libcvc5, libcvc5parser,
+GMP and the C++ runtime all linked in, so no post-processing is needed:
 
-#### Linux x64
 ```shell
-$ ldd libcvc5.so libcvc5jni.so 
-libcvc5.so:
-        linux-vdso.so.1 (0x00007ffe22381000)
-        libm.so.6 => /usr/lib/libm.so.6 (0x00007ff4c8bf4000)
-        libc.so.6 => /usr/lib/libc.so.6 (0x00007ff4c7619000)
-        /usr/lib64/ld-linux-x86-64.so.2 (0x00007ff4c8d0a000)
-libcvc5jni.so:
-        linux-vdso.so.1 (0x00007ffccbbb5000)
-        libcvc5.so => not found
-        libc.so.6 => /usr/lib/libc.so.6 (0x00007fa594c19000)
-        libm.so.6 => /usr/lib/libm.so.6 (0x00007fa5961f3000)
-        /usr/lib64/ld-linux-x86-64.so.2 (0x00007fa596389000)
+unzip -j "cvc5-Win64-x86_64-java-api.jar"  "cvc5-libs/windows/x86_64/cvc5jni.dll"
+zip -X -9 "cvc5-native-win-x86-64-<version>.zip" libcvc5jni.dll   # note: renamed
+
+unzip -j "cvc5-macOS-arm64-java-api.jar" "cvc5-libs/osx/aarch_64/libcvc5jni.dylib"
+zip -X -9 "cvc5-native-osx-arm64-<version>.zip" libcvc5jni.dylib
 ```
-#### Windows x64
+
+Do **not** use the `-shared.zip` assets: their libraries reference each other through
+`@rpath`/relative names, and on macOS they are ad-hoc code signed, so the install-name
+rewriting the old fork-based build did would invalidate the signature.
+
+Note that the Windows library links the UCRT, so it requires Windows 10 or newer.
+
+## Verifying the result
+
+Run these before committing new archives.
+
 ```shell
-$ ldd libcvc5.dll libcvc5jni.dll
-libcvc5.dll:
-        ntdll.dll => /c/Windows/SYSTEM32/ntdll.dll (0x7ffb7a190000)
-        KERNEL32.DLL => /c/Windows/System32/KERNEL32.DLL (0x7ffb78240000)
-        KERNELBASE.dll => /c/Windows/System32/KERNELBASE.dll (0x7ffb77a70000)
-        msvcrt.dll => /c/Windows/System32/msvcrt.dll (0x7ffb79410000)
-        CRYPTBASE.DLL => /c/Windows/SYSTEM32/CRYPTBASE.DLL (0x7ffb77190000)
-        bcryptPrimitives.dll => /c/Windows/System32/bcryptPrimitives.dll (0x7ffb77de0000)
-libcvc5jni.dll:
-        ntdll.dll => /c/Windows/SYSTEM32/ntdll.dll (0x7ffb7a190000)
-        KERNEL32.DLL => /c/Windows/System32/KERNEL32.DLL (0x7ffb78240000)
-        KERNELBASE.dll => /c/Windows/System32/KERNELBASE.dll (0x7ffb77a70000)
-        msvcrt.dll => /c/Windows/System32/msvcrt.dll (0x7ffb79410000)
-        libcvc5.dll => not found
-        CRYPTBASE.DLL => /c/Windows/SYSTEM32/CRYPTBASE.DLL (0x7ffb77190000)
-        bcryptPrimitives.dll => /c/Windows/System32/bcryptPrimitives.dll (0x7ffb77de0000)
+# The version is the one we intended to ship
+strings -a libcvc5.so.1 | grep -m1 -E '^1\.[0-9]+\.[0-9]+$'
+
+# No dependency on the system C++ runtime (expect 0)
+objdump -T libcvc5.so.1 libcvc5parser.so.1 libcvc5jni.so | grep -c GLIBCXX
+
+# Old glibc is enough
+objdump -T libcvc5.so.1 libcvc5parser.so.1 libcvc5jni.so | grep -o 'GLIBC_[0-9.]*' | sort -uV | tail -1
+
+# The static C++ runtime is not exported (expect a few hundred, not thousands)
+nm -D --defined-only -C libcvc5.so.1 | grep -c 'std::'
+
+# The jar is Java 8 and carries no natives
+unzip -l cvc5-<version>.jar | grep -c cvc5-libs
 ```
-#### MacOS aarch64
+
+For cvc5 1.3.4 this gives version `1.3.4`, `0` GLIBCXX references, max `GLIBC_2.25`,
+`402`/`251`/`10` exported `std::` symbols, and `0` native entries in the jar.
+
+Finally run the tests, including `:ksmt-test:test`, which loads several solvers into a
+single JVM and is what catches the symbol interposition problem described above.
+
+## Expected dynamic dependencies
+
+To ensure the distribution is portable, verify the produced binaries have no dependencies
+that might not be present on the user's machine.
+
+### Linux x64
+
 ```shell
-$ otool -L libcvc5.dylib libcvc5jni.dylib 
-libcvc5.dylib:
-        @rpath/libcvc5.dylib (compatibility version 0.0.0, current version 0.0.0)
-        /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 1300.36.0)
-        /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1319.0.0)
+$ objdump -p libcvc5.so.1 libcvc5parser.so.1 libcvc5jni.so | grep -E 'SONAME|NEEDED'
+libcvc5.so.1:        NEEDED libm.so.6, libc.so.6, ld-linux-x86-64.so.2
+                     SONAME libcvc5.so.1
+libcvc5parser.so.1:  NEEDED libcvc5.so.1, libm.so.6, libc.so.6, ld-linux-x86-64.so.2
+                     SONAME libcvc5parser.so.1
+libcvc5jni.so:       NEEDED libcvc5parser.so.1, libcvc5.so.1, libm.so.6, libc.so.6, ld-linux-x86-64.so.2
+                     SONAME libcvc5jni.so
+```
+
+### Windows x64
+
+```shell
+$ objdump -p libcvc5jni.dll | grep 'DLL Name'
+        DLL Name: api-ms-win-crt-{convert,environment,filesystem,heap,locale,math,
+                                  multibyte,private,runtime,stdio,string,time,utility}-l1-1-0.dll
+        DLL Name: KERNEL32.dll
+```
+
+No `libstdc++-6.dll`, `libgcc_s_seh-1.dll`, `libwinpthread-1.dll` and no sibling cvc5 DLL.
+
+### MacOS aarch64
+
+```shell
+$ otool -L libcvc5jni.dylib
 libcvc5jni.dylib:
         @rpath/libcvc5jni.dylib (compatibility version 0.0.0, current version 0.0.0)
-        @rpath/libcvc5.dylib (compatibility version 0.0.0, current version 0.0.0)
-        /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 1300.36.0)
-        /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1319.0.0)
+        /usr/lib/libc++.1.dylib
+        /usr/lib/libSystem.B.dylib
 ```
+
+Both dependencies are absolute system paths and there is no `LC_RPATH`, so the `@rpath`
+install name is never resolved — ksmt loads the library by absolute path.

ksmt-cvc5/ksmt-cvc5-core/build.gradle.kts

@@ -11,7 +11,7 @@ repositories {
     mavenCentral()
 }
 
-val cvc5Version = "1.3.0"
+val cvc5Version = "1.3.4"
 val cvc5Jar = distDir.resolve("cvc5-$cvc5Version.jar")
 
 dependencies {

ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprConverter.kt

@@ -148,6 +148,7 @@ open class KCvc5ExprConverter(
             Kind.SQRT -> throw KSolverUnsupportedFeatureException("No direct mapping of sqrt on real in ksmt")
             Kind.POW -> convertNativePowExpr(expr)
             Kind.POW2 -> convertNativePowExpr(expr)
+            Kind.LOG2 -> throw KSolverUnsupportedFeatureException("No direct mapping of log2 on int in ksmt")
             Kind.INTS_MODULUS -> expr.convert(::mkIntMod)
             Kind.INTS_DIVISION -> expr.convert(::mkArithDiv)
             Kind.DIVISION -> expr.convert(::mkArithDiv)
@@ -178,7 +179,8 @@ open class KCvc5ExprConverter(
             Kind.DIVISIBLE -> expr.convert { arExpr: KExpr<KIntSort> ->
                 mkIntMod(arExpr, expr.intDivisibleArg.expr) eq 0.expr
             }
-            Kind.IAND -> throw KSolverUnsupportedFeatureException(
+            Kind.IAND,
+            Kind.PIAND -> throw KSolverUnsupportedFeatureException(
                 "No direct mapping in ksmt. btw int to bv is not supported in ksmt"
             )
 

ksmt-cvc5/ksmt-cvc5-native/build.gradle.kts

@@ -29,7 +29,7 @@ val cvc5Binaries = mapOf(
 
 cvc5Binaries.keys.forEach { it.compileClasspath = compileConfig }
 
-val cvc5Version = "1.3.0"
+val cvc5Version = "1.3.4"
 
 dependencies {
     compileConfig(project(":ksmt-cvc5:ksmt-cvc5-core"))

ksmt-cvc5/ksmt-cvc5-native/src/mac-arm/kotlin/io/ksmt/solver/cvc5/KCvc5NativeLibraryLoaderMacArm.kt

@@ -14,9 +14,9 @@ class KCvc5NativeLibraryLoaderMacArm :
     }
 
     companion object {
+        // A single self-contained library: the cvc5 release build for this platform
+        // links libcvc5 and libcvc5parser into libcvc5jni.
         private val libraries = listOf(
-            "libcvc5.1",
-            "libcvc5parser.1",
             "libcvc5jni",
         )
     }

ksmt-cvc5/ksmt-cvc5-native/src/windows-x64/kotlin/io/ksmt/solver/cvc5/KCvc5NativeLibraryLoaderWindowsX64.kt

@@ -14,9 +14,9 @@ class KCvc5NativeLibraryLoaderWindowsX64 :
     }
 
     companion object {
+        // A single self-contained library: the cvc5 release build for this platform
+        // links libcvc5 and libcvc5parser into libcvc5jni.
         private val libraries = listOf(
-            "libcvc5",
-            "libcvc5parser",
             "libcvc5jni"
         )
     }