Skip to content

Commit cdca9fa

Browse files
committed
MathSAT5: update MathSAT5 to v5.6.12., which comes with updated dependencies:
- On Windows systems, MPIR is replaced with GMP. MPIR was no longer developed since 2017, as there was GMP as alternative anyway. Now, MPIR is officially dead, and it is removed from MathSAT and also from JavaSMT. - The Linux version of MathSAT5 requires GLIBC 2.38 or newer, available at least in Ubuntu 24.04 or newer. In the last commit, we already updated our development Podman/Docker image to Ubuntu 24.04.
1 parent 5bafbdc commit cdca9fa

File tree

3 files changed

+8
-7
lines changed

3 files changed

+8
-7
lines changed

doc/Developers-How-to-Release-into-Ivy.md

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -271,8 +271,9 @@ but in the normal system environment, where some testing can be applied by the d
271271
We publish MathSAT for Linux (x64 and arm64) and Windows (x64) systems at once.
272272
The build process can fully be done on a Linux system,
273273
and requires several dependencies, such as gcc, x86_64-w64-mingw32-gcc, and aarch64-linux-gnu-gcc.
274-
We prefer to use the Docker container based on Ubuntu 22.04 (better use Ubuntu 18.04 for older GLIBC!)
274+
We prefer to use the Docker container based on Ubuntu 24.04
275275
for compiling the dependencies and assembling the libraries.
276+
Since MathSAT5 5.6.12, using Ubuntu 18.04 or 22.04 with older GLIBC no longer works!
276277

277278
First, [download the (reentrant!) Linux and Windows64 binary release](http://mathsat.fbk.eu/download.html) in the same version, unpack them.
278279
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 \
295296
Example:
296297
```
297298
ant publish-mathsat \
298-
-Dmathsat-linux-x64.path=/workspace/solvers/mathsat/mathsat-5.6.11-linux-x86_64-reentrant \
299+
-Dmathsat-linux-x64.path=/workspace/solvers/mathsat/mathsat-5.6.12-linux-x86_64 \
299300
-Dgmp-linux-x64.path=/workspace/solvers/gmp/gmp-6.3.0-linux-x64 \
300-
-Dmathsat-windows-x64.path=/workspace/solvers/mathsat/mathsat-5.6.11-win64-msvc \
301+
-Dmathsat-windows-x64.path=/workspace/solvers/mathsat/mathsat-5.6.12-win64 \
301302
-Djdk-windows-x64.path=/workspace/solvers/jdk/openjdk-17.0.2_windows-x64_bin/jdk-17.0.2 \
302303
-Dgmp-windows-x64.path=/workspace/solvers/gmp/gmp-6.3.0-win-x64 \
303-
-Dmathsat-linux-arm64.path=/workspace/solvers/mathsat/mathsat-5.6.11-linux-aarch64-reentrant \
304+
-Dmathsat-linux-arm64.path=/workspace/solvers/mathsat/mathsat-5.6.12-linux-aarch64 \
304305
-Dgmp-linux-arm64.path=/workspace/solvers/gmp/gmp-6.3.0-linux-arm64 \
305306
-Djdk-linux-arm64.path=/workspace/solvers/jdk/openjdk-17.0.2_linux-aarch64_bin/jdk-17.0.2 \
306-
-Dmathsat.version=5.6.11
307+
-Dmathsat.version=5.6.12
307308
```
308309
Finally, follow the instructions shown in the message at the end.
309310

lib/ivy.xml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -188,7 +188,7 @@ SPDX-License-Identifier: Apache-2.0
188188
<dependency org="edu.tum.cs" name="java-cup" rev="11b-20160615" conf="runtime-princess->runtime"/>
189189

190190
<!-- Solver Binaries -->
191-
<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" />
191+
<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" />
192192
<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" />
193193
<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"/>
194194
<dependency org="org.sosy_lab" name="javasmt-solver-optimathsat" rev="1.7.3-sosy1" conf="runtime-optimathsat->solver-optimathsat" />

src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -162,7 +162,7 @@ private String[] getRequiredLibcxx(String library) {
162162
case "opensmtj":
163163
return new String[] {"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"};
164164
case "mathsat5j":
165-
return new String[] {"GLIBC_2.33"};
165+
return new String[] {"GLIBC_2.33", "GLIBC_2.38"};
166166
case "cvc5jni":
167167
return new String[] {"GLIBC_2.32"};
168168
default:

0 commit comments

Comments
 (0)