Merge pull request #544 from sosy-lab/503-update-mathsat-5-6-12

kfriedberger · web-flow · commit c4ee2b277ab2 · 2025-11-02T12:31:11.000+01:00
#503: update MathSAT5 to version 5.6.12
diff --git a/build/build-publish-solvers/solver-mathsat.xml b/build/build-publish-solvers/solver-mathsat.xml
@@ -5,7 +5,7 @@ This file is part of JavaSMT,
 an API wrapper for a collection of SMT solvers:
 https://github.com/sosy-lab/java-smt
 
-SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
@@ -73,7 +73,7 @@ SPDX-License-Identifier: Apache-2.0
         <copy file="lib/native/source/libmathsat5j/libmathsat5j-arm64.so" tofile="${mathsat.dist.dir}/arm64/libmathsat5j-${mathsat.version}.so"/>
         <copy file="lib/native/source/libmathsat5j/mathsat5j.dll" tofile="${mathsat.dist.dir}/x64/mathsat5j-${mathsat.version}.dll"/>
         <copy file="${mathsat-windows-x64.path}/lib/mathsat.dll" tofile="${mathsat.dist.dir}/x64/mathsat-${mathsat.version}.dll"/>
-        <copy file="${mathsat-windows-x64.path}/bin/mpir.dll" tofile="${mathsat.dist.dir}/x64/mpir-${mathsat.version}.dll"/>
+        <copy file="${mathsat-windows-x64.path}/bin/gmp.dll" tofile="${mathsat.dist.dir}/x64/gmp-${mathsat.version}.dll"/>
         <copy file="${gmp-windows-x64.path}/.libs/libgmp-10.dll" tofile="${mathsat.dist.dir}/x64/gmp-${mathsat.version}.dll"/>
 
         <ivy:resolve conf="solver-mathsat" file="solvers_ivy_conf/ivy_mathsat.xml"/>
diff --git a/doc/Developers-How-to-Release-into-Ivy.md b/doc/Developers-How-to-Release-into-Ivy.md
@@ -271,8 +271,9 @@ but in the normal system environment, where some testing can be applied by the d
 We publish MathSAT for Linux (x64 and arm64) and Windows (x64) systems at once.
 The build process can fully be done on a Linux system, 
 and requires several dependencies, such as gcc, x86_64-w64-mingw32-gcc, and aarch64-linux-gnu-gcc.
-We prefer to use the Docker container based on Ubuntu 22.04 (better use Ubuntu 18.04 for older GLIBC!)
+We prefer to use the Docker container based on Ubuntu 24.04
 for compiling the dependencies and assembling the libraries.
+Since MathSAT5 5.6.12, using Ubuntu 18.04 or 22.04 with older GLIBC no longer works!
 
 First, [download the (reentrant!) Linux and Windows64 binary release](http://mathsat.fbk.eu/download.html) in the same version, unpack them.
 Then provide the necessary dependencies (GMP/JDK for Linux (x64 and arm64) and GMP/JDK for Windows (x64))
@@ -295,15 +296,15 @@ ant publish-mathsat \
 Example:
 ```
 ant publish-mathsat \
-     -Dmathsat-linux-x64.path=/workspace/solvers/mathsat/mathsat-5.6.11-linux-x86_64-reentrant \
+     -Dmathsat-linux-x64.path=/workspace/solvers/mathsat/mathsat-5.6.12-linux-x86_64 \
      -Dgmp-linux-x64.path=/workspace/solvers/gmp/gmp-6.3.0-linux-x64 \
-     -Dmathsat-windows-x64.path=/workspace/solvers/mathsat/mathsat-5.6.11-win64-msvc \
+     -Dmathsat-windows-x64.path=/workspace/solvers/mathsat/mathsat-5.6.12-win64 \
      -Djdk-windows-x64.path=/workspace/solvers/jdk/openjdk-17.0.2_windows-x64_bin/jdk-17.0.2 \
      -Dgmp-windows-x64.path=/workspace/solvers/gmp/gmp-6.3.0-win-x64 \
-     -Dmathsat-linux-arm64.path=/workspace/solvers/mathsat/mathsat-5.6.11-linux-aarch64-reentrant \
+     -Dmathsat-linux-arm64.path=/workspace/solvers/mathsat/mathsat-5.6.12-linux-aarch64 \
      -Dgmp-linux-arm64.path=/workspace/solvers/gmp/gmp-6.3.0-linux-arm64 \
      -Djdk-linux-arm64.path=/workspace/solvers/jdk/openjdk-17.0.2_linux-aarch64_bin/jdk-17.0.2 \
-     -Dmathsat.version=5.6.11
+     -Dmathsat.version=5.6.12
 ```
 Finally, follow the instructions shown in the message at the end.
 
diff --git a/docker/buildUbuntu2404.sh b/docker/buildUbuntu2404.sh
@@ -0,0 +1,21 @@
+#!/bin/bash
+
+# This file is part of JavaSMT,
+# an API wrapper for a collection of SMT solvers:
+# https://github.com/sosy-lab/java-smt
+#
+# SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
+#
+# SPDX-License-Identifier: Apache-2.0
+
+podman build \
+    --build-arg BUILD_DATE=$(date -u +"%Y-%m-%dT%H:%M:%SZ") \
+    -t registry.gitlab.com/sosy-lab/software/java-smt/develop:ubuntu2404 - < ubuntu2404.Dockerfile
+
+# For pushing to Gitlab registry, please create your personal access token:
+#   https://gitlab.com/-/user_settings/personal_access_tokens
+# with read and write rights to the Gitlab registry (full API access is not required)
+#
+# Please use the following commands to push the build image to Gitlab:
+#   podman login registry.gitlab.com
+#   podman push registry.gitlab.com/sosy-lab/software/java-smt/develop:ubuntu2404
diff --git a/docker/runUbuntu2404.sh b/docker/runUbuntu2404.sh
@@ -0,0 +1,19 @@
+#!/bin/bash
+
+# This file is part of JavaSMT,
+# an API wrapper for a collection of SMT solvers:
+# https://github.com/sosy-lab/java-smt
+#
+# SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
+#
+# SPDX-License-Identifier: Apache-2.0
+
+# JavaSMT and all solver files are located in the directory WORKSPACE.
+# Derive WORKSPACE from the script's location (two directories up from current)
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+WORKSPACE="$(realpath "${SCRIPT_DIR}/../..")"
+
+podman run -it \
+    --mount type=bind,source=${WORKSPACE},target=/workspace \
+    --workdir /workspace/java-smt \
+    registry.gitlab.com/sosy-lab/software/java-smt/develop:ubuntu2404
diff --git a/docker/ubuntu2404.Dockerfile b/docker/ubuntu2404.Dockerfile
@@ -0,0 +1,107 @@
+# This file is part of JavaSMT,
+# an API wrapper for a collection of SMT solvers:
+# https://github.com/sosy-lab/java-smt
+#
+# SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
+#
+# SPDX-License-Identifier: Apache-2.0
+
+FROM ubuntu:24.04
+
+# set default locale
+RUN apt-get update \
+ && DEBIAN_FRONTEND=noninteractive TZ=Etc/UTC apt-get install -y \
+        tzdata locales locales-all \
+ && apt-get clean
+ENV LC_ALL=en_US.UTF-8
+ENV LANG=en_US.UTF-8
+ENV LANGUAGE=en_US.UTF-8
+
+# Install basic packages for building several solvers
+RUN apt-get update \
+ && apt-get install -y \
+        wget curl git build-essential cmake patchelf unzip \
+        openjdk-11-jdk ant maven \
+        gcc-mingw-w64-x86-64-posix g++-mingw-w64-x86-64-posix \
+        gcc-aarch64-linux-gnu g++-aarch64-linux-gnu \
+        binutils-aarch64-linux-gnu libc6-dev-arm64-cross \
+        zlib1g-dev m4 \
+ && apt-get clean
+
+# Yices2 requires some dependencies
+RUN  apt-get update \
+ && apt-get install -y \
+        autoconf gperf \
+ && apt-get clean
+
+# Bitwuzla requires Ninja and Meson (updated version from pip), and uses SWIG >4.0 from dependencies.
+# GMP >6.3.0 is automatically downloaded and build within Bitwuzla.
+RUN apt-get update \
+ && apt-get install -y \
+        ninja-build python3-pip meson \
+ && apt-get clean
+
+# OpenSMT requires swig, gmp, flex and bison
+# - swig v4.1 or newer for unique_ptr support
+# - libpcre2-dev is a dependency of swig
+# - gmp needs to be recompiled to generate PIC code (see below)
+# - lzip is required to unpack the gmp tar ball
+RUN apt-get update \
+ && apt-get install -y \
+        cmake flex bison libpcre2-dev lzip swig \
+ && apt-get clean
+
+WORKDIR /dependencies
+
+# Install GMP for linux on x64 and arm64
+# We could add another build for windows when needed
+RUN wget https://gmplib.org/download/gmp/gmp-6.2.1.tar.lz \
+ && tar xf gmp-6.2.1.tar.lz \
+ && rm gmp-6.2.1.tar.lz \
+ && cd gmp-6.2.1 \
+ && ./configure \
+      --enable-cxx \
+      --with-pic \
+      --disable-shared \
+      --enable-fat \
+      --prefix=/dependencies/gmp-6.2.1/install/x64-linux \
+ && make -j4 \
+ && make install \
+ && make clean \
+ && ./configure \
+      --enable-cxx \
+      --with-pic \
+      --disable-shared \
+      --enable-fat \
+      --host=aarch64-linux-gnu \
+      --prefix=/dependencies/gmp-6.2.1/install/arm64-linux \
+ && CC=aarch64-linux-gnu-gcc CXX=aarch64-linux-gnu-g++ LD=aarch64-linux-gnu-ld make -j4 \
+ && make install \
+ && make clean
+
+# Install the Jdk for Windows x64
+RUN wget https://download.java.net/openjdk/jdk11/ri/openjdk-11+28_windows-x64_bin.zip \
+ && unzip openjdk-11+28_windows-x64_bin.zip \
+ && mv jdk-11 jdk11-windows-x64 \
+ && rm openjdk-11+28_windows-x64_bin.zip
+
+# Install the Jdk for Linux arm64
+RUN wget https://download.java.net/java/GA/jdk17.0.2/dfd4a8d0985749f896bed50d7138ee7f/8/GPL/openjdk-17.0.2_linux-aarch64_bin.tar.gz \
+ && tar -xzf openjdk-17.0.2_linux-aarch64_bin.tar.gz \
+ && mv jdk-17.0.2 jdk17-linux-aarch64 \
+ && rm openjdk-17.0.2_linux-aarch64_bin.tar.gz
+
+# JNI is not found when compiling Boolector in the image, so we need to set JAVA_HOME
+ENV JAVA_HOME=/usr/lib/jvm/java-11-openjdk-amd64/
+
+# set labels for the image
+ARG BUILD_DATE
+LABEL org.opencontainers.image.created="${BUILD_DATE}"
+LABEL org.opencontainers.image.title="JavaSMT solver development"
+LABEL org.opencontainers.image.description="Ubuntu 24.04-based image for JavaSMT solver development"
+LABEL org.opencontainers.image.source="https://github.com/sosy-lab/java-smt"
+LABEL org.opencontainers.image.licenses="Apache-2.0"
+
+# Podman-Specific Label for Auto-Update
+LABEL io.containers.autoupdate=registry
+
diff --git a/lib/ivy.xml b/lib/ivy.xml
@@ -188,7 +188,7 @@ SPDX-License-Identifier: Apache-2.0
         <dependency org="edu.tum.cs" name="java-cup" rev="11b-20160615" conf="runtime-princess->runtime"/>
 
         <!-- Solver Binaries -->
-        <dependency org="org.sosy_lab" name="javasmt-solver-mathsat" rev="5.6.11-sosy1" conf="runtime-mathsat-x64->solver-mathsat-x64; runtime-mathsat-arm64->solver-mathsat-arm64" />
+        <dependency org="org.sosy_lab" name="javasmt-solver-mathsat" rev="5.6.12" conf="runtime-mathsat-x64->solver-mathsat-x64; runtime-mathsat-arm64->solver-mathsat-arm64" />
         <dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.15.2" conf="runtime-z3-x64->solver-z3-x64; runtime-z3-arm64->solver-z3-arm64; contrib->sources,javadoc" />
         <dependency org="org.sosy_lab" name="javasmt-solver-opensmt" rev="2.9.0-gef441e1c" conf="runtime-opensmt-x64->solver-opensmt-x64; runtime-opensmt-arm64->solver-opensmt-arm64; contrib->sources,javadoc"/>
         <dependency org="org.sosy_lab" name="javasmt-solver-optimathsat" rev="1.7.3-sosy1" conf="runtime-optimathsat->solver-optimathsat" />
diff --git a/lib/native/source/libmathsat5j/compileForWindows.sh b/lib/native/source/libmathsat5j/compileForWindows.sh
@@ -4,7 +4,7 @@
 # an API wrapper for a collection of SMT solvers:
 # https://github.com/sosy-lab/java-smt
 #
-# SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
+# SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
 #
 # SPDX-License-Identifier: Apache-2.0
 
@@ -20,8 +20,9 @@
 # There are the following dependencies:
 # - MinGW (install Ubuntu package: `mingw-w64`)
 # - The MathSAT5 library for Windows64 as can be downloaded from http://mathsat.fbk.eu/download.html
-# - MathSAT5 is linked against MPIR which aims to be compatible to GMP.
-#   Since 2017, MPIR is no longer developed. We use the precompiled `mpir.dll` from the MathSAT5 archive.
+# - MathSAT5 is linked against GMP. We use the precompiled `gmp.dll` from the MathSAT5 archive.
+#   Previously, MathSAT5 used MPIR which aimed to be compatible to GMP.
+#   Since 2017, MPIR was no longer developed, and since 2022, MPIR officially dead.
 #   When compiling our bindings, we use the header files from GMP.
 #   We do not actually need to compile it. However, this is a nice test, whether our build system works as expected.
 #   To build GMP, download GMP 6.3.0 from http://gmplib.org/ and run
@@ -87,7 +88,7 @@ $CC -g -std=gnu99 -Wall -Wextra -Wpedantic -Wno-return-type -Wno-unused-paramete
     -o $OUT_FILE -shared -Wl,-soname,$OUT_FILE \
     -D_JNI_IMPLEMENTATION_ -Wl,--kill-at \
     $JNI_HEADERS -I$MSAT_SRC_DIR -I$GMP_DIR -L$MSAT_LIB_DIR $SRC_FILES \
-    -lmathsat $MSAT_BIN_DIR/mpir.dll -lstdc++ -lpsapi
+    -lmathsat $MSAT_BIN_DIR/gmp.dll -lstdc++ -lpsapi
 
 echo "Compilation Done"
 echo "Reducing file size by dropping unused symbols..."
diff --git a/lib/native/x86_64-windows/README.md b/lib/native/x86_64-windows/README.md
@@ -3,7 +3,7 @@ This file is part of JavaSMT,
 an API wrapper for a collection of SMT solvers:
 https://github.com/sosy-lab/java-smt
 
-SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
@@ -32,7 +32,7 @@ For Z3:
 - `mklink libz3java.dll ..\..\java\runtime-z3\x64\libz3java.dll`
 
 For MathSAT5:
-- `mklink mpir.dll ..\..\java\runtime-mathsat\x64\mpir.dll`
+- `mklink gmp.dll ..\..\java\runtime-mathsat\x64\gmp.dll`
 - `mklink mathsat.dll ..\..\java\runtime-mathsat\x64\mathsat.dll`
 - `mklink mathsat5j.dll ..\..\java\runtime-mathsat\x64\mathsat5j.dll`
 
@@ -54,7 +54,7 @@ For Z3:
 - `copy ..\..\java\runtime-z3\x64\libz3java.dll libz3java.dll`
 
 For MathSAT5:
-- `copy ..\..\java\runtime-mathsat\x64\mpir.dll mpir.dll`
+- `copy ..\..\java\runtime-mathsat\x64\gmp.dll gmp.dll`
 - `copy ..\..\java\runtime-mathsat\x64\mathsat.dll mathsat.dll`
 - `copy ..\..\java\runtime-mathsat\x64\mathsat5j.dll mathsat5j.dll`
 
diff --git a/solvers_ivy_conf/ivy_mathsat.xml b/solvers_ivy_conf/ivy_mathsat.xml
@@ -5,7 +5,7 @@ This file is part of JavaSMT,
 an API wrapper for a collection of SMT solvers:
 https://github.com/sosy-lab/java-smt
 
-SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
@@ -45,7 +45,7 @@ SPDX-License-Identifier: Apache-2.0
         <!-- Windows x64 files -->
         <artifact name="mathsat5j" conf="solver-mathsat-windows-x64" e:arch="x64" type="dll" ext="dll"/>
         <artifact name="mathsat"   conf="solver-mathsat-windows-x64" e:arch="x64" type="dll" ext="dll"/>
-        <artifact name="mpir"      conf="solver-mathsat-windows-x64" e:arch="x64" type="dll" ext="dll"/>
+        <artifact name="gmp"       conf="solver-mathsat-windows-x64" e:arch="x64" type="dll" ext="dll"/>
     </publications>
     <dependencies></dependencies>
 
diff --git a/solvers_maven_conf/maven_mathsat_pom_template.xml b/solvers_maven_conf/maven_mathsat_pom_template.xml
@@ -6,7 +6,7 @@ This file is part of JavaSMT,
 an API wrapper for a collection of SMT solvers:
 https://github.com/sosy-lab/java-smt
 
-SPDX-FileCopyrightText: 2021 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
@@ -41,7 +41,7 @@ SPDX-License-Identifier: Apache-2.0
           <url>http://mathsat.fbk.eu/download.html</url>
       </license>
       <license>
-          <name>MPIR is licensed LGPL v3+</name>
+          <name>GMP is licensed both GNU LGPL v3 and GNU GPL v2</name>
           <url>https://www.gnu.org/licenses/lgpl-3.0.en.html</url>
       </license>
   </licenses>
diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java
@@ -2,7 +2,7 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -236,7 +236,7 @@ public static Mathsat5SolverContext create(
   @VisibleForTesting
   static void loadLibrary(Consumer<String> pLoader) {
     loadLibrariesWithFallback(
-        pLoader, ImmutableList.of("mathsat5j"), ImmutableList.of("mpir", "mathsat", "mathsat5j"));
+        pLoader, ImmutableList.of("mathsat5j"), ImmutableList.of("gmp", "mathsat", "mathsat5j"));
   }
 
   long createEnvironment(long cfg) {
diff --git a/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java b/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java
@@ -162,7 +162,7 @@ private String[] getRequiredLibcxx(String library) {
       case "opensmtj":
         return new String[] {"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"};
       case "mathsat5j":
-        return new String[] {"GLIBC_2.33"};
+        return new String[] {"GLIBC_2.33", "GLIBC_2.38"};
       case "cvc5jni":
         return new String[] {"GLIBC_2.32"};
       default:
