MathSAT5: replace MPIR with GMP.

MPIR was no longer developed since 2017, as there was GMP anyway.
Now MPIR is officially dead and is removed from MathSAT and also from JavaSMT.

Author: kfriedberger

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"/>

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..."

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`
 

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>
 

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>

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) {