From 615585971e5c4501aead62d7c8793ddf3dd19ae5 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 29 Jul 2020 17:05:54 +0200 Subject: [PATCH 01/34] Z3: publish additional Windows binaries into our Ivy repository. As Z3 already provides DLLs for Windows, it is quite simple to support it. The AppVeyor tests will fail because of to the missing symlinks. Related issue: #129. --- .gitignore | 1 + build.xml | 2 +- build/build-publish-solvers.xml | 10 +++++++++- lib/native/x84_64-windows/README.md | 19 +++++++++++++++++++ solvers_ivy_conf/ivy_z3.xml | 5 +++++ 5 files changed, 35 insertions(+), 2 deletions(-) create mode 100644 lib/native/x84_64-windows/README.md diff --git a/.gitignore b/.gitignore index f0c94abb46..4c10446e8c 100644 --- a/.gitignore +++ b/.gitignore @@ -42,6 +42,7 @@ lib/native/source/*/*.o .idea/uiDesigner.xml /*.so +/*.dll /*.jar build.properties diff --git a/build.xml b/build.xml index c50039c329..eab92890c8 100644 --- a/build.xml +++ b/build.xml @@ -78,7 +78,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/build/build-publish-solvers.xml b/build/build-publish-solvers.xml index c3ccd9b2eb..3587c62856 100644 --- a/build/build-publish-solvers.xml +++ b/build/build-publish-solvers.xml @@ -19,7 +19,10 @@ SPDX-License-Identifier: Apache-2.0 --> + This package provides the JNI for direct usage. + Please copy both Linux64 and Windows64 release into the same root directory. + The only overlap between those releases is the JAR file, which should be equal anyway. + "> Please specify the path to Z3 with the flag -Dz3.path=/path/to/z3. The path has to point to the root Z3 folder. @@ -36,8 +39,13 @@ SPDX-License-Identifier: Apache-2.0 libz3.so has missing SONAME property. Please run 'patchelf --set-soname libz3.so ${z3.path}/libz3.so'. + + + + + diff --git a/lib/native/x84_64-windows/README.md b/lib/native/x84_64-windows/README.md new file mode 100644 index 0000000000..b5f89b5b81 --- /dev/null +++ b/lib/native/x84_64-windows/README.md @@ -0,0 +1,19 @@ +# How to install Z3 for Windows64 for developers of JavaSMT + +## Note: + +These steps are not required for using JavaSMT as a library, +but only for developing JavaSMT with Z3 support on a Windows machine. + +## Instruction: + +Windows does not allow user-space symlinks, +but requires administrator rights to create them. +Thus, we cannot check them into the repository. +Please execute the following as administrator: + +- mklink libz3.dll ..\..\java\runtime-z3\libz3.dll +- mklink libz3java.dll ..\..\java\runtime-z3\libz3java.dll + +An alternative simple solution is to copy over those files +from the `lib\java\runtime-*\` directory into the current directory. diff --git a/solvers_ivy_conf/ivy_z3.xml b/solvers_ivy_conf/ivy_z3.xml index 6f6015fcd9..04a7013bcc 100644 --- a/solvers_ivy_conf/ivy_z3.xml +++ b/solvers_ivy_conf/ivy_z3.xml @@ -27,8 +27,13 @@ SPDX-License-Identifier: Apache-2.0 + + + + + From bc93df3f0feae2970f6d41ec1046336cb0ea5a72 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 29 Jul 2020 17:09:57 +0200 Subject: [PATCH 02/34] update version of Z3 to latest version in the Ivy repository. --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 4d2ecccb50..71e7653a78 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -155,7 +155,7 @@ SPDX-License-Identifier: Apache-2.0 - + From 10e5a28465ad5d44fe6faf5bae1cb9c0a1513011 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 29 Jul 2020 17:13:28 +0200 Subject: [PATCH 03/34] simplify AppVeyor script. --- .appveyor.yml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/.appveyor.yml b/.appveyor.yml index 100964d576..ad23ed6b65 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -22,12 +22,12 @@ install: ) [System.IO.Compression.ZipFile]::ExtractToDirectory("C:\ant-bin.zip", "C:\ant") } - - cmd: SET JAVA_HOME=C:\Program Files\Java\jdk14 - - cmd: SET PATH=C:\ant\apache-ant-1.10.8\bin;%JAVA_HOME%\bin;%PATH% - - cmd: SET IVY_CACHE_DIR=C:\ivy - - cmd: echo %USERPROFILE% - - cmd: echo %PATH% - - cmd: java -version + - SET JAVA_HOME=C:\Program Files\Java\jdk14 + - SET PATH=C:\ant\apache-ant-1.10.8\bin;%JAVA_HOME%\bin;%PATH% + - SET IVY_CACHE_DIR=C:\ivy + - echo %USERPROFILE% + - echo %PATH% + - java -version build_script: - ant build From eb21711ee10f718079fb2497403b6000e1443c35 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 29 Jul 2020 17:26:32 +0200 Subject: [PATCH 04/34] fix AppVeyor CI to execute Z3. (This is a blind test, not sure if working.) --- .appveyor.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.appveyor.yml b/.appveyor.yml index ad23ed6b65..246229195c 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -31,6 +31,9 @@ install: build_script: - ant build + # Windows does not allow symlinks, thus we need to copy Z3 to make it available for JUnit tests. + # See lib\native\x86_64-windows\README.md for details. + - copy lib\java\runtime-z3\*dll lib\native\x86_64-windows\ test_script: - ant unit-tests From ca568931eed6e26323c7b1ee2caf8cb04711e096 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 29 Jul 2020 18:36:55 +0200 Subject: [PATCH 05/34] fix directory name. --- lib/native/{x84_64-windows => x86_64-windows}/README.md | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename lib/native/{x84_64-windows => x86_64-windows}/README.md (100%) diff --git a/lib/native/x84_64-windows/README.md b/lib/native/x86_64-windows/README.md similarity index 100% rename from lib/native/x84_64-windows/README.md rename to lib/native/x86_64-windows/README.md From e113d8a25eedff7344efb99f2b919a18a4765622 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Thu, 30 Jul 2020 14:44:53 +0200 Subject: [PATCH 06/34] update Z3 documentation in publish script.. --- build/build-publish-solvers.xml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/build/build-publish-solvers.xml b/build/build-publish-solvers.xml index 3587c62856..600afd8694 100644 --- a/build/build-publish-solvers.xml +++ b/build/build-publish-solvers.xml @@ -19,13 +19,10 @@ SPDX-License-Identifier: Apache-2.0 --> + This package provides the JNI for direct usage."> Please specify the path to Z3 with the flag -Dz3.path=/path/to/z3. - The path has to point to the root Z3 folder. + The path has to point to the root Z3 folder and can be relative or absolute. Note that shell substitutions do not work. @@ -52,8 +49,11 @@ SPDX-License-Identifier: Apache-2.0 Please specify the path to Z3 with the flag -Dz3.path=/path/to/z3. - The path has to point to the root Z3 folder. + The path has to point to the root Z3 folder and can be relative or absolute. Note that shell substitutions do not work. + Please provide both Linux64 and Windows64 release in the same root directory, + e.g., copy the releases together into one directory. + The only overlap between those releases is the JAR file, which should be equal anyway. From 26d8d827586ede69411051f73cb5b47fccfb4e01 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 4 Aug 2020 22:21:12 +0200 Subject: [PATCH 07/34] refactoring and simplifying the build script for the MathSAT5 library. --- lib/native/source/libmathsat5j/compile.sh | 71 ++++++++++++++--------- 1 file changed, 43 insertions(+), 28 deletions(-) diff --git a/lib/native/source/libmathsat5j/compile.sh b/lib/native/source/libmathsat5j/compile.sh index 3876f7021d..0ca596950b 100755 --- a/lib/native/source/libmathsat5j/compile.sh +++ b/lib/native/source/libmathsat5j/compile.sh @@ -8,17 +8,24 @@ # # SPDX-License-Identifier: Apache-2.0 +# ######################################### +# +# INFO: +# This script is automatically called from ant when publishing MathSAT5 or OptiMathSAT. +# There is no need to call this scripts manually, except for developing and debugging. +# +# ######################################### + # This script builds either libmathsat5j.so (bindings to mathsat5), or # liboptimathsat5j.so (bindings to optimathsat5). -# In future, mathsat5 and optimathsat should merge, making the switching -# obsolete. +# In future, mathsat5 and optimathsat should merge, making the switching obsolete. # For building libmathsat5j.so, there are two dependencies: # - The static Mathsat5 library as can be downloaded from http://mathsat.fbk.eu/download.html # - The static GMP library compiled with the "-fPIC" option. # To create this, download GMP from http://gmplib.org/ and run -# ./configure --enable-cxx --with-pic --disable-shared --enable-fat -# make +# ./configure --enable-cxx --with-pic --disable-shared --enable-fat --host=x86_64-w64-mingw32 +# make # For building liboptimathsat5.so, OptiMathSat5 can be downloaded from # http://optimathsat.disi.unitn.it/. @@ -58,23 +65,25 @@ cd ${DIR} JNI_HEADERS="$(../get_jni_headers.sh)" -if [ ! -f "$1/lib/libmathsat.a" ]; then - echo "You need to specify the directory with the downloaded Mathsat on the command line!" - exit 1 -fi MSAT_SRC_DIR="$1"/include MSAT_LIB_DIR="$1"/lib GMP_LIB_DIR="$2"/.libs GMP_HEADER_DIR="$2" -if [ ! -f "$GMP_LIB_DIR/libgmp.a" ]; then - echo "You need to specify the GMP directory on the command line!" - exit 1 -fi - SRC_FILES="org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c versions.c" OBJ_FILES="org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.o" +# check requirements +if [ ! -f "$MSAT_LIB_DIR/libmathsat.a" ]; then + echo "You need to specify the directory with the downloaded Mathsat on the command line!" + exit 1 +fi +if [ ! -f "$GMP_LIB_DIR/libgmp.a" ]; then + echo "You need to specify the GMP directory on the command line!" + exit 1 +fi + +# switch between MathSAT5 and OptiMathSAT if [ "$3" = "-optimathsat" ]; then echo "Compiling bindings to OptiMathSAT" SRC_FILES="$SRC_FILES optimization.c" @@ -86,37 +95,43 @@ else ADDITIONAL_FLAGS="" fi -echo "Compiling the C wrapper code and creating the \"$OUT_FILE\" library" +echo "Compiling the C wrapper code and creating the \"$OUT_FILE\" library..." # This will compile the JNI wrapper part, given the JNI and the Mathsat header files gcc -g -std=gnu99 -Wall -Wextra -Wpedantic -Wno-return-type -Wno-unused-parameter $JNI_HEADERS -I$MSAT_SRC_DIR -I$GMP_HEADER_DIR $SRC_FILES -fPIC -c $ADDITIONAL_FLAGS + echo "Compilation Done" +echo "Linking libraries together into one file..." # This will link together the file produced above, the Mathsat library, the GMP library and the standard libraries. # Everything except the standard libraries is included statically. -# The result is a shared library. +# The result is a single shared library containing all necessary components. if [ `uname -m` = "x86_64" ]; then - gcc -Wall -g -o $OUT_FILE -shared -Wl,-soname,libmathsat5j.so -L. -L$MSAT_LIB_DIR -L$GMP_LIB_DIR -I$GMP_HEADER_DIR versions.o $OBJ_FILES -Wl,-Bstatic -lmathsat -lgmpxx -lgmp -static-libstdc++ -lstdc++ -Wl,-Bdynamic -lc -lm -Wl,--wrap=memcpy -Wl,--version-script=libmathsat5j.version + gcc -Wall -g -o ${OUT_FILE} -shared -Wl,-soname,libmathsat5j.so -L. -L${MSAT_LIB_DIR} -L${GMP_LIB_DIR} -I${GMP_HEADER_DIR} versions.o ${OBJ_FILES} -Wl,-Bstatic -lmathsat -lgmpxx -lgmp -static-libstdc++ -lstdc++ -Wl,-Bdynamic -lc -lm -Wl,--wrap=memcpy -Wl,--version-script=libmathsat5j.version else - gcc -Wall -g -o ${OUT_FILE} -shared -Wl,-soname,libmathsat5j.so -L${MSAT_LIB_DIR} -L${GMP_LIB_DIR} -I${GMP_HEADER_DIR} ${OBJ_FILES} -Wl,-Bstatic -lmathsat -lgmpxx -lgmp -Wl,-Bdynamic -lc -lm -lstdc++ + # TODO compiling for/on a 32bit system was not done for quite a long time. We should drop it. + gcc -Wall -g -o ${OUT_FILE} -shared -Wl,-soname,libmathsat5j.so -L${MSAT_LIB_DIR} -L${GMP_LIB_DIR} -I${GMP_HEADER_DIR} ${OBJ_FILES} -Wl,-Bstatic -lmathsat -lgmpxx -lgmp -Wl,-Bdynamic -lc -lm -lstdc++ fi - -if [ $? -eq 0 ]; then - strip ${OUT_FILE} -else - echo "There was a problem during compilation of - \"org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c\"" - exit 1 +if [ $? -ne 0 ]; then + echo "There was a problem during compilation of \"org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c\"" + exit 1 fi +echo "Linking Done" +echo "Reducing file size by dropping unused symbols..." + +strip ${OUT_FILE} + +echo "Reduction Done" + MISSING_SYMBOLS="$(readelf -Ws ${OUT_FILE} | grep NOTYPE | grep GLOBAL | grep UND)" if [ ! -z "$MISSING_SYMBOLS" ]; then - echo "Warning: There are the following unresolved dependencies in libmathsat5j.so:" - readelf -Ws ${OUT_FILE} | grep NOTYPE | grep GLOBAL | grep UND - exit 1 + echo "Warning: There are the following unresolved dependencies in libmathsat5j.so:" + readelf -Ws ${OUT_FILE} | grep NOTYPE | grep GLOBAL | grep UND + exit 1 fi echo "All Done" echo "Please check in the following output that the library does not depend on any GLIBC version >= 2.11, otherwise it will not work on Ubuntu 10.04:" -LANG=C objdump -p ${OUT_FILE} |grep -A50 "required from" +LANG=C objdump -p ${OUT_FILE} | grep -A50 "required from" From 252b05e985727e767365dbb419736e0d13b74b1b Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 4 Aug 2020 23:23:13 +0200 Subject: [PATCH 08/34] fix compilation warnings for Windows. --- lib/native/source/libmathsat5j/includes/defines.h | 4 +++- ...g_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c | 4 ++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/lib/native/source/libmathsat5j/includes/defines.h b/lib/native/source/libmathsat5j/includes/defines.h index da77225051..1b0bbcc7b7 100644 --- a/lib/native/source/libmathsat5j/includes/defines.h +++ b/lib/native/source/libmathsat5j/includes/defines.h @@ -131,6 +131,7 @@ typedef void jvoid; // for symmetry to jint, jlong etc. mtype s_arg##num; \ mtype * m_arg##num = &s_arg##num; +// jint is int32 on Linux and Windows, thus the cast from jint* to int* is safe. #define INT_ARRAY_ARG(num) \ int * m_arg##num = (int *)((*jenv)->GetIntArrayElements(jenv, arg##num, NULL)); \ if (m_arg##num == NULL) { \ @@ -165,8 +166,9 @@ typedef void jvoid; // for symmetry to jint, jlong etc. free(m_arg##num); \ out##num##a: +// jint is int32 on Linux and Windows, thus the cast from int* to jint* is safe. #define FREE_INT_ARRAY_ARG(num) \ - (*jenv)->ReleaseIntArrayElements(jenv, arg##num, m_arg##num, 0); \ + (*jenv)->ReleaseIntArrayElements(jenv, arg##num, (jint *)m_arg##num, 0); \ out##num: #define PUT_STRUCT_POINTER_ARG(num) \ diff --git a/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c b/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c index 888359bb0e..478e5c99cb 100644 --- a/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c +++ b/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c @@ -1191,14 +1191,14 @@ DEFINE_FUNC(long, 1set_1termination_1callback) WITH_TWO_ARGS(jenv, object) return 0; } // Ugly: return the struct's address so that it can be free'd later on. - return (long)helper; + return (size_t)helper; } // This method is not defined by Mathsat, // we need it to prevent a memory leak. // This may be called only after the environment with this termination test has been destroyed. DEFINE_FUNC(void, 1free_1termination_1callback) WITH_ONE_ARG(long) - struct msat_callback_info *helper = (struct msat_callback_info *)(long)arg1; + struct msat_callback_info *helper = (struct msat_callback_info *)(size_t)arg1; if (helper == NULL) { throwException(jenv, "java/lang/NullPointerException", "TerminationCallback may not be null"); return; From 8fcd75d50b7419291542a22171cfa42c4d7070f1 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 4 Aug 2020 23:24:12 +0200 Subject: [PATCH 09/34] add script for cross-compiling MathSAT5 on Linux for Windows. --- .../source/libmathsat5j/compileForWindows.sh | 105 ++++++++++++++++++ 1 file changed, 105 insertions(+) create mode 100755 lib/native/source/libmathsat5j/compileForWindows.sh diff --git a/lib/native/source/libmathsat5j/compileForWindows.sh b/lib/native/source/libmathsat5j/compileForWindows.sh new file mode 100755 index 0000000000..85e17d7cee --- /dev/null +++ b/lib/native/source/libmathsat5j/compileForWindows.sh @@ -0,0 +1,105 @@ +#!/usr/bin/env 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: 2020 Dirk Beyer +# +# SPDX-License-Identifier: Apache-2.0 + +# ######################################### +# +# INFO: +# This script is automatically called from ant when publishing MathSAT5 or OptiMathSAT. +# There is no need to call this scripts manually, except for developing and debugging. +# +# ######################################### + +# This script builds either libmathsat5j.so (bindings to mathsat5), or +# liboptimathsat5j.so (bindings to optimathsat5). +# In future, mathsat5 and optimathsat should merge, making the switching obsolete. + +# For building libmathsat5j.dll on Linux for Windows, there are the following dependencies: +# - The Mathsat5 library for Windows64 as can be downloaded from http://mathsat.fbk.eu/download.html +# - The static GMP library compiled with the "-fPIC" option. +# To create this, download GMP from http://gmplib.org/ and run +# ./configure --enable-cxx --with-pic --disable-shared --enable-fat --host=x86_64-w64-mingw32 +# make +# TODO: MathSAT5 is linked against MPIR which aims to be compatible to GMP. +# Perhaps, we should also use MPIR. +# - The Windows JNI headers in a reasonable LTS version: +# Download the zip archive from https://jdk.java.net/ and unpack it +# (e.g., https://download.java.net/openjdk/jdk11/ri/openjdk-11+28_windows-x64_bin.zip). + +# To build mathsat bindings: ./compileForWindows.sh $MATHSAT_DIR $GMP_DIR $JNI_DIR + +SOURCE="${BASH_SOURCE[0]}" +while [ -h "$SOURCE" ]; do # resolve $SOURCE until the file is no longer a symlink + DIR="$( cd -P "$( dirname "$SOURCE" )" && pwd )" + SOURCE="$(readlink "$SOURCE")" + [[ ${SOURCE} != /* ]] && SOURCE="$DIR/$SOURCE" # if $SOURCE was a relative symlink, we need to resolve it relative to the path where the symlink file was located +done +DIR="$( cd -P "$( dirname "$SOURCE" )" && pwd )" + +cd ${DIR} + +JNI_DIR="$3"/include +JNI_HEADERS="-I${JNI_DIR}/ -I${JNI_DIR}/win32/" + +MSAT_SRC_DIR="$1"/include +MSAT_LIB_DIR="$1"/lib +GMP_LIB_DIR="$2"/.libs +GMP_HEADER_DIR="$2" + +SRC_FILES="org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c versions.c" +OBJ_FILES="org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.o" + +# check requirements +if [ ! -f "$MSAT_LIB_DIR/mathsat.dll" ]; then + echo "You need to specify the directory with the downloaded Mathsat on the command line!" + echo "Can not find $MSAT_LIB_DIR/mathsat.dll" + exit 1 +fi +if [ ! -f "$JNI_DIR/jni.h" ]; then + echo "You need to specify the directory with the downloaded JNI headers on the command line!" + echo "Can not find $JNI_DIR/jni.h" + exit 1 +fi + +OUT_FILE="mathsat5j.dll" +BASIC_OPTIONS="-m64 -g -std=gnu99 -Wall -Wextra -Wpedantic -Wno-return-type -Wno-unused-parameter" + +echo "Compiling the C wrapper code and creating the \"$OUT_FILE\" library..." + +# This will compile the JNI wrapper part, given the JNI and the Mathsat header files + +x86_64-w64-mingw32-gcc ${BASIC_OPTIONS} -D_JNI_IMPLEMENTATION_ $JNI_HEADERS \ + -I$MSAT_SRC_DIR -lmathsat -I$GMP_HEADER_DIR \ + org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c -fPIC -c + +echo "Compilation Done" +echo "Linking libraries together..." + +# This will link the file produced above against the Mathsat library, the GMP library, and the standard libraries. +# The result is a shared library with dependencoes towards MathSAT5. +x86_64-w64-mingw32-gcc ${BASIC_OPTIONS} -o $OUT_FILE -shared -L. \ + -L$MSAT_LIB_DIR -L$GMP_LIB_DIR -I$GMP_HEADER_DIR $OBJ_FILES \ + -Wl,-Bstatic -lmathsat -lgmpxx -lgmp -static-libstdc++ -lstdc++ -lm + +if [ $? -ne 0 ]; then + echo "There was a problem during compilation of \"org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c\"" + exit 1 +fi + +echo "Linking Done" +echo "Reducing file size by dropping unused symbols..." + +strip ${OUT_FILE} + +echo "Reduction Done" +echo "All Done" + +echo "Please check the following dependencies that will be required at runtime by $OUT_FILE:" +echo "(DLLs like 'kernel32' and 'msvcrt' are provided by Windows)" +objdump -p $OUT_FILE | grep "DLL Name" From 05772126393ae7dcc8f217418aaeef2012e94424 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 5 Aug 2020 01:07:10 +0200 Subject: [PATCH 10/34] adding publication-steps into ant-build-script. --- build/build-publish-solvers.xml | 40 +++++++++++++++++++++++++++----- solvers_ivy_conf/ivy_mathsat.xml | 6 ++++- 2 files changed, 39 insertions(+), 7 deletions(-) diff --git a/build/build-publish-solvers.xml b/build/build-publish-solvers.xml index 600afd8694..03fc1fb6bf 100644 --- a/build/build-publish-solvers.xml +++ b/build/build-publish-solvers.xml @@ -278,6 +278,26 @@ SPDX-License-Identifier: Apache-2.0 + + Please specify the path to the Mathsat5 source folder (Windows version) with the flag -Dmathsat-windows.path=/path/to/mathsat. + The path has to point to the root Mathsat5 folder. + Note that shell substitutions do not work and a full absolute path has to be specified. + + + Please specify the path to the GMP source folder (Windows version) with the flag -Dgmp-windows.path=/path/to/gmp. + The path has to point to the root GMP folder. + Note that shell substitutions do not work and a full absolute path has to be specified. + + + Please specify the path to the JDK source folder (Windows version) with the flag -Djdk-windows.path=/path/to/jdk. + The path has to point to the root JDK folder. + Note that shell substitutions do not work and a full absolute path has to be specified. + + + + + + - + description="Publish MathSAT binaries to Ivy repo."> + + Please specify the @{flag} version with the flag -Dmathsat.version=... . + + + + - @@ -303,8 +327,12 @@ SPDX-License-Identifier: Apache-2.0 Please specify the path to the Mathsat5 source folder with the flag -Dmathsat.path=/path/to/mathsat. The path has to point to the root Mathsat5 folder. - Note that shell substitutions do not work and a full absolute - path has to be specified. + Note that shell substitutions do not work and a full absolute path has to be specified. + + + Please specify the path to the GMP source folder with the flag -Dgmp.path=/path/to/gmp. + The path has to point to the root Mathsat5 folder. + Note that shell substitutions do not work and a full absolute path has to be specified. @@ -312,7 +340,6 @@ SPDX-License-Identifier: Apache-2.0 - @@ -345,6 +372,7 @@ SPDX-License-Identifier: Apache-2.0 + diff --git a/solvers_ivy_conf/ivy_mathsat.xml b/solvers_ivy_conf/ivy_mathsat.xml index 871a8af887..d27f845552 100644 --- a/solvers_ivy_conf/ivy_mathsat.xml +++ b/solvers_ivy_conf/ivy_mathsat.xml @@ -26,8 +26,12 @@ SPDX-License-Identifier: Apache-2.0 - + + + + + From 0d775b64e9285b4b9d7257c115986ed5b08ab46a Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 5 Aug 2020 08:49:56 +0200 Subject: [PATCH 11/34] MathSAT5 context supports loading the Windows library. --- .../mathsat5/Mathsat5NativeApiTest.java | 3 +- .../mathsat5/Mathsat5SolverContext.java | 35 ++++++++++++++++++- 2 files changed, 35 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java index 631c8d09cd..7c5da70d93 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java @@ -45,7 +45,6 @@ import org.junit.BeforeClass; import org.junit.Ignore; import org.junit.Test; -import org.sosy_lab.common.NativeLibraries; import org.sosy_lab.java_smt.api.SolverException; public class Mathsat5NativeApiTest extends Mathsat5AbstractNativeApiTest { @@ -57,7 +56,7 @@ public class Mathsat5NativeApiTest extends Mathsat5AbstractNativeApiTest { @BeforeClass public static void loadMathsat() { try { - NativeLibraries.loadLibrary("mathsat5j"); + Mathsat5SolverContext.loadLibrary(); } catch (UnsatisfiedLinkError e) { throw new AssumptionViolatedException("MathSAT5 is not available", e); } diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java index 6d0611de79..bbc3e9d635 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java @@ -19,13 +19,16 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_option_checked; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_termination_callback; +import com.google.common.annotations.VisibleForTesting; import com.google.common.base.Preconditions; import com.google.common.base.Splitter; import com.google.common.base.Splitter.MapSplitter; +import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; import com.google.common.io.MoreFiles; import java.io.IOException; import java.nio.file.Path; +import java.util.List; import java.util.Map; import java.util.Set; import java.util.logging.Level; @@ -151,7 +154,7 @@ public static Mathsat5SolverContext create( if (settings.loadOptimathsat5) { NativeLibraries.loadLibrary("optimathsat5j"); } else { - NativeLibraries.loadLibrary("mathsat5j"); + loadLibrary(); } long msatConf = msat_create_config(); @@ -200,6 +203,36 @@ public static Mathsat5SolverContext create( logger, msatConf, settings, randomSeed, pShutdownNotifier, manager, creator); } + @VisibleForTesting + static void loadLibrary() { + loadLibrary(ImmutableList.of("mathsat5j"), ImmutableList.of("mpir", "mathsat", "mathsat5j")); + } + + /** + * This method loads the given library, depending on the operating system. + * + *

Each list is applied in the given ordering. + */ + private static final void loadLibrary(List linuxLibrary, List windowsLibrary) { + // we try Linux first, and then Windows. + // TODO we could simply switch over the OS-name. + // TODO move this method upwards? more solvers could use it. + try { + for (String libraryName : linuxLibrary) { + NativeLibraries.loadLibrary(libraryName); + } + } catch (UnsatisfiedLinkError e1) { + try { + for (String libraryName : windowsLibrary) { + NativeLibraries.loadLibrary(libraryName); + } + } catch (UnsatisfiedLinkError e2) { + e1.addSuppressed(e2); + throw e1; + } + } + } + long createEnvironment(long cfg) { if (USE_GHOST_FILTER) { msat_set_option_checked(cfg, "dpll.ghost_filtering", "true"); From 61cf1b1b5b837b633cce2024dac9dd820e5f6d3d Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 5 Aug 2020 09:12:27 +0200 Subject: [PATCH 12/34] remove invalid part of documentation. --- lib/native/source/libmathsat5j/compileForWindows.sh | 4 ---- 1 file changed, 4 deletions(-) diff --git a/lib/native/source/libmathsat5j/compileForWindows.sh b/lib/native/source/libmathsat5j/compileForWindows.sh index 85e17d7cee..55b6b0ea1c 100755 --- a/lib/native/source/libmathsat5j/compileForWindows.sh +++ b/lib/native/source/libmathsat5j/compileForWindows.sh @@ -16,10 +16,6 @@ # # ######################################### -# This script builds either libmathsat5j.so (bindings to mathsat5), or -# liboptimathsat5j.so (bindings to optimathsat5). -# In future, mathsat5 and optimathsat should merge, making the switching obsolete. - # For building libmathsat5j.dll on Linux for Windows, there are the following dependencies: # - The Mathsat5 library for Windows64 as can be downloaded from http://mathsat.fbk.eu/download.html # - The static GMP library compiled with the "-fPIC" option. From 535616ec4a121adb86002bd92da70ebdc991b364 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 5 Aug 2020 09:16:57 +0200 Subject: [PATCH 13/34] fix invalid error message in ant-build-script. The `flag` is not available here. --- build/build-publish-solvers.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build/build-publish-solvers.xml b/build/build-publish-solvers.xml index 03fc1fb6bf..6dd5bbd39d 100644 --- a/build/build-publish-solvers.xml +++ b/build/build-publish-solvers.xml @@ -308,7 +308,7 @@ SPDX-License-Identifier: Apache-2.0 - Please specify the @{flag} version with the flag -Dmathsat.version=... . + Please specify the MathSAT5 version with the flag -Dmathsat.version=... . From 8c0436f0945d1adf7b22ba8ab396367a4f2e0411 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 5 Aug 2020 09:32:51 +0200 Subject: [PATCH 14/34] update documentation. --- lib/native/x86_64-windows/README.md | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) diff --git a/lib/native/x86_64-windows/README.md b/lib/native/x86_64-windows/README.md index b5f89b5b81..90a8d9ac77 100644 --- a/lib/native/x86_64-windows/README.md +++ b/lib/native/x86_64-windows/README.md @@ -3,7 +3,7 @@ ## Note: These steps are not required for using JavaSMT as a library, -but only for developing JavaSMT with Z3 support on a Windows machine. +but only for developing JavaSMT with native solver support on a Windows machine. ## Instruction: @@ -12,8 +12,24 @@ but requires administrator rights to create them. Thus, we cannot check them into the repository. Please execute the following as administrator: +For Z3: - mklink libz3.dll ..\..\java\runtime-z3\libz3.dll - mklink libz3java.dll ..\..\java\runtime-z3\libz3java.dll -An alternative simple solution is to copy over those files -from the `lib\java\runtime-*\` directory into the current directory. +For MathSAT5: +- mklink mpir.dll ..\..\java\runtime-mathsat\mpir.dll +- mklink mathsat.dll ..\..\java\runtime-mathsat\mathsat.dll +- mklink mathsat5j.dll ..\..\java\runtime-mathsat\mathsat5j.dll + +An alternative simple solution (without the need of administrator) is to copy over +those files from the `lib\java\runtime-*\` directory into the current directory. +Please note that this needs to be repeated after each update of Ant/Ivy dependencies. + +For Z3: +- copy ..\..\java\runtime-z3\libz3.dll libz3.dll +- copy ..\..\java\runtime-z3\libz3java.dll libz3java.dll + +For MathSAT5: +- copy ..\..\java\runtime-mathsat\mpir.dll mpir.dll +- copy ..\..\java\runtime-mathsat\mathsat.dll mathsat.dll +- copy ..\..\java\runtime-mathsat\mathsat5j.dll mathsat5j.dll From abda1cc6b774628fe1ccc28ea58013fa24542f94 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 5 Aug 2020 09:35:43 +0200 Subject: [PATCH 15/34] fix CheckStyle. --- .../java_smt/solvers/mathsat5/Mathsat5SolverContext.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java index bbc3e9d635..97dd3fb6d7 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java @@ -213,7 +213,7 @@ static void loadLibrary() { * *

Each list is applied in the given ordering. */ - private static final void loadLibrary(List linuxLibrary, List windowsLibrary) { + private static void loadLibrary(List linuxLibrary, List windowsLibrary) { // we try Linux first, and then Windows. // TODO we could simply switch over the OS-name. // TODO move this method upwards? more solvers could use it. From 2875b7201a05453d159c77cbb6de0092c86cb216 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 5 Aug 2020 09:37:14 +0200 Subject: [PATCH 16/34] add licencing information to satisfy Reuse. --- lib/native/x86_64-windows/README.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/lib/native/x86_64-windows/README.md b/lib/native/x86_64-windows/README.md index 90a8d9ac77..7d2f5f9e68 100644 --- a/lib/native/x86_64-windows/README.md +++ b/lib/native/x86_64-windows/README.md @@ -1,3 +1,13 @@ + + # How to install Z3 for Windows64 for developers of JavaSMT ## Note: From 10f8a6e675f44c561cdf05a64f22aa0b59faccf6 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 5 Aug 2020 09:41:11 +0200 Subject: [PATCH 17/34] update MathSAT5 to (internal) latest version. This version includes initial support for Windows. For testing only! Feedback welcome. There are some bugs, which need to be resolved: - FP theory broken on Windows. - Concurrency support missing/broken on Windows. - Some random SegFaults on Windows. --- .appveyor.yml | 4 +++- lib/ivy.xml | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/.appveyor.yml b/.appveyor.yml index 246229195c..0ee9283dbe 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -31,9 +31,11 @@ install: build_script: - ant build - # Windows does not allow symlinks, thus we need to copy Z3 to make it available for JUnit tests. + # Windows does not allow symlinks, thus we need to copy native solver binaries + # to make it available for JUnit tests. # See lib\native\x86_64-windows\README.md for details. - copy lib\java\runtime-z3\*dll lib\native\x86_64-windows\ + - copy lib\java\runtime-mathsat\*dll lib\native\x86_64-windows\ test_script: - ant unit-tests diff --git a/lib/ivy.xml b/lib/ivy.xml index 71e7653a78..f3cfef3f04 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -154,7 +154,7 @@ SPDX-License-Identifier: Apache-2.0 - + From 9db229cb590f595c542272a803d9f77c6274c9ff Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Fri, 14 Aug 2020 08:51:32 +0200 Subject: [PATCH 18/34] Z3: also include MacOS library. This is completely untestet, but it looks so straight-forward, that it should be working. --- build/build-publish-solvers.xml | 7 +++++-- solvers_ivy_conf/ivy_z3.xml | 3 +++ src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java | 3 ++- 3 files changed, 10 insertions(+), 3 deletions(-) diff --git a/build/build-publish-solvers.xml b/build/build-publish-solvers.xml index 6dd5bbd39d..62f660c413 100644 --- a/build/build-publish-solvers.xml +++ b/build/build-publish-solvers.xml @@ -42,6 +42,9 @@ SPDX-License-Identifier: Apache-2.0 + + + @@ -51,8 +54,8 @@ SPDX-License-Identifier: Apache-2.0 Please specify the path to Z3 with the flag -Dz3.path=/path/to/z3. The path has to point to the root Z3 folder and can be relative or absolute. Note that shell substitutions do not work. - Please provide both Linux64 and Windows64 release in the same root directory, - e.g., copy the releases together into one directory. + Please provide all releases (Linux64, MacOS, and Windows64) together in the same root directory, + e.g., copy the releases (especially the content of their `bin` directories) together into one directory. The only overlap between those releases is the JAR file, which should be equal anyway. diff --git a/solvers_ivy_conf/ivy_z3.xml b/solvers_ivy_conf/ivy_z3.xml index 04a7013bcc..e7a0e51fc1 100644 --- a/solvers_ivy_conf/ivy_z3.xml +++ b/solvers_ivy_conf/ivy_z3.xml @@ -33,6 +33,9 @@ SPDX-License-Identifier: Apache-2.0 + + + diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java index 73edd47257..82652034c0 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java @@ -113,11 +113,12 @@ public static synchronized Z3SolverContext create( // but it will fail to find the former if not loaded previously. // We load both libraries here to have all the loading in one place. try { + // On Linux and MacOS, the plain name of the library works. System.loadLibrary("z3"); System.loadLibrary("z3java"); } catch (UnsatisfiedLinkError e1) { - // On Windows, the library name is different, so we try again. try { + // On Windows, the library name is different, so we try again. System.loadLibrary("libz3"); System.loadLibrary("libz3java"); } catch (UnsatisfiedLinkError e2) { From eb2a49f15566be5347439610e099794f3cadab18 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Fri, 14 Aug 2020 08:55:12 +0200 Subject: [PATCH 19/34] update Z3. --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index f3cfef3f04..1321d08892 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -155,7 +155,7 @@ SPDX-License-Identifier: Apache-2.0 - + From 065bdb5fe3cfc3a5fe962375c30723e9b6539e8d Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Thu, 17 Sep 2020 13:23:17 +0200 Subject: [PATCH 20/34] cleanup library files from macosx, too. --- build.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.xml b/build.xml index eab92890c8..c9ae0b036e 100644 --- a/build.xml +++ b/build.xml @@ -78,7 +78,7 @@ SPDX-License-Identifier: Apache-2.0 - + From e3ae7ace580e644f5acbbd29a646c28fbd648759 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Thu, 17 Sep 2020 14:10:40 +0200 Subject: [PATCH 21/34] disable concurrency tests for MathSAT5 on Windows. Those tests cause segfaults. --- src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java index edfa225124..558d8548b1 100644 --- a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java @@ -108,6 +108,13 @@ protected Solvers solverToUse() { @Before public void checkThatSolverIsAvailable() throws InvalidConfigurationException { initSolver().close(); + + if (System.getProperty("os.name").toLowerCase().startsWith("win")) { + assume() + .withMessage("MathSAT5 is not reentant on Windows") + .that(solver) + .isNotEqualTo(Solvers.MATHSAT5); + } } private void requireConcurrentMultipleStackSupport() { From 4b0504e99ac3a87913a86cd08e44551d1e61ad10 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Thu, 17 Sep 2020 16:08:42 +0200 Subject: [PATCH 22/34] revert documentation change. --- lib/native/source/libmathsat5j/compile.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/native/source/libmathsat5j/compile.sh b/lib/native/source/libmathsat5j/compile.sh index 0ca596950b..56a6823c16 100755 --- a/lib/native/source/libmathsat5j/compile.sh +++ b/lib/native/source/libmathsat5j/compile.sh @@ -24,7 +24,7 @@ # - The static Mathsat5 library as can be downloaded from http://mathsat.fbk.eu/download.html # - The static GMP library compiled with the "-fPIC" option. # To create this, download GMP from http://gmplib.org/ and run -# ./configure --enable-cxx --with-pic --disable-shared --enable-fat --host=x86_64-w64-mingw32 +# ./configure --enable-cxx --with-pic --disable-shared --enable-fat # make # For building liboptimathsat5.so, OptiMathSat5 can be downloaded from From aab094fb2ee7459a7652a4ad9f3d0eea04365ca2 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 19 Sep 2020 14:25:29 +0200 Subject: [PATCH 23/34] cleanup tmp build files. --- build.xml | 1 + 1 file changed, 1 insertion(+) diff --git a/build.xml b/build.xml index c9ae0b036e..7ea15289bc 100644 --- a/build.xml +++ b/build.xml @@ -79,6 +79,7 @@ SPDX-License-Identifier: Apache-2.0 + From c8295c6b5c694eabb6662c646aa782db4d3b3c84 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 13 Oct 2020 19:57:20 +0200 Subject: [PATCH 24/34] improve compilation script for MathSAT. --- build/build-publish-solvers.xml | 8 ++--- .../source/libmathsat5j/compileForWindows.sh | 30 +++++++------------ 2 files changed, 14 insertions(+), 24 deletions(-) diff --git a/build/build-publish-solvers.xml b/build/build-publish-solvers.xml index 62f660c413..63450bd4df 100644 --- a/build/build-publish-solvers.xml +++ b/build/build-publish-solvers.xml @@ -286,9 +286,9 @@ SPDX-License-Identifier: Apache-2.0 The path has to point to the root Mathsat5 folder. Note that shell substitutions do not work and a full absolute path has to be specified. - - Please specify the path to the GMP source folder (Windows version) with the flag -Dgmp-windows.path=/path/to/gmp. - The path has to point to the root GMP folder. + + Please specify the path to the MPIR source folder (Windows version) with the flag -Dmpir-windows.path=/path/to/mpir. + The path has to point to the root MPIR folder. Note that shell substitutions do not work and a full absolute path has to be specified. @@ -298,7 +298,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/lib/native/source/libmathsat5j/compileForWindows.sh b/lib/native/source/libmathsat5j/compileForWindows.sh index 55b6b0ea1c..602f58cfab 100755 --- a/lib/native/source/libmathsat5j/compileForWindows.sh +++ b/lib/native/source/libmathsat5j/compileForWindows.sh @@ -45,8 +45,11 @@ JNI_HEADERS="-I${JNI_DIR}/ -I${JNI_DIR}/win32/" MSAT_SRC_DIR="$1"/include MSAT_LIB_DIR="$1"/lib -GMP_LIB_DIR="$2"/.libs -GMP_HEADER_DIR="$2" +MSAT_BIN_DIR="$1"/bin + +MPIR_HEADER_DIR="$2" +MPIR_LIB_DIR="$2"/.libs +MPIR_INCLUDE_DIR="$2" SRC_FILES="org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c versions.c" OBJ_FILES="org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.o" @@ -69,26 +72,13 @@ BASIC_OPTIONS="-m64 -g -std=gnu99 -Wall -Wextra -Wpedantic -Wno-return-type -Wno echo "Compiling the C wrapper code and creating the \"$OUT_FILE\" library..." # This will compile the JNI wrapper part, given the JNI and the Mathsat header files - -x86_64-w64-mingw32-gcc ${BASIC_OPTIONS} -D_JNI_IMPLEMENTATION_ $JNI_HEADERS \ - -I$MSAT_SRC_DIR -lmathsat -I$GMP_HEADER_DIR \ - org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c -fPIC -c +x86_64-w64-mingw32-gcc -g -o $OUT_FILE -shared -Wl,-soname,$OUT_FILE \ + -D_JNI_IMPLEMENTATION_ -Wl,--kill-at $JNI_HEADERS \ + -I$MSAT_SRC_DIR -I$MPIR_INCLUDE_DIR -L$MSAT_LIB_DIR \ + org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c \ + -lmathsat $MSAT_BIN_DIR/mpir.dll -lstdc++ -lpsapi 2>&1 echo "Compilation Done" -echo "Linking libraries together..." - -# This will link the file produced above against the Mathsat library, the GMP library, and the standard libraries. -# The result is a shared library with dependencoes towards MathSAT5. -x86_64-w64-mingw32-gcc ${BASIC_OPTIONS} -o $OUT_FILE -shared -L. \ - -L$MSAT_LIB_DIR -L$GMP_LIB_DIR -I$GMP_HEADER_DIR $OBJ_FILES \ - -Wl,-Bstatic -lmathsat -lgmpxx -lgmp -static-libstdc++ -lstdc++ -lm - -if [ $? -ne 0 ]; then - echo "There was a problem during compilation of \"org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c\"" - exit 1 -fi - -echo "Linking Done" echo "Reducing file size by dropping unused symbols..." strip ${OUT_FILE} From eba94940b9b8d6fde5675c12020e032229e8c9e4 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 13 Oct 2020 19:58:30 +0200 Subject: [PATCH 25/34] update to the latest MathSAT version 5.6.4 (including windows binary) --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 1321d08892..ec447741e8 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -154,7 +154,7 @@ SPDX-License-Identifier: Apache-2.0 - + From 4dacb53d303550460b48fffbc9d2510f6bda4ee7 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 13 Oct 2020 21:54:55 +0200 Subject: [PATCH 26/34] update Z3 to version 4.8.9 (including windows binary) --- build/build-publish-solvers.xml | 2 +- lib/ivy.xml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/build/build-publish-solvers.xml b/build/build-publish-solvers.xml index 63450bd4df..6874b76d28 100644 --- a/build/build-publish-solvers.xml +++ b/build/build-publish-solvers.xml @@ -51,7 +51,7 @@ SPDX-License-Identifier: Apache-2.0 - Please specify the path to Z3 with the flag -Dz3.path=/path/to/z3. + Please specify the path to Z3 with the flag -Dz3.path=/path/to/z3 (e.g. `bin` directory). The path has to point to the root Z3 folder and can be relative or absolute. Note that shell substitutions do not work. Please provide all releases (Linux64, MacOS, and Windows64) together in the same root directory, diff --git a/lib/ivy.xml b/lib/ivy.xml index ec447741e8..9068207ab2 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -155,7 +155,7 @@ SPDX-License-Identifier: Apache-2.0 - + From d40a443aeb73ac958f0df1c0a195b2620cd56672 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 13 Oct 2020 22:46:07 +0200 Subject: [PATCH 27/34] cleanup and update documentation for building MathSAT5 on Linux for Windows. --- .../source/libmathsat5j/compileForWindows.sh | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/lib/native/source/libmathsat5j/compileForWindows.sh b/lib/native/source/libmathsat5j/compileForWindows.sh index 602f58cfab..c4f1ea7f0f 100755 --- a/lib/native/source/libmathsat5j/compileForWindows.sh +++ b/lib/native/source/libmathsat5j/compileForWindows.sh @@ -16,19 +16,21 @@ # # ######################################### -# For building libmathsat5j.dll on Linux for Windows, there are the following dependencies: -# - The Mathsat5 library for Windows64 as can be downloaded from http://mathsat.fbk.eu/download.html -# - The static GMP library compiled with the "-fPIC" option. -# To create this, download GMP from http://gmplib.org/ and run -# ./configure --enable-cxx --with-pic --disable-shared --enable-fat --host=x86_64-w64-mingw32 +# This script cross-compiles the MathSAT5 library `mathsat5j.dll` on a Linux host for a Windows64 target. +# 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. +# We actually only need the headers, but we do a full build, and then use `mpir.dll` from the MathSAT5 archive. +# To build MPIR, download MPIR 2.7.2 from http://mpir.org/downloads.html and run +# ./configure --enable-cxx --with-pic --enable-shared --disable-static --enable-fat --host=x86_64-w64-mingw32 --enable-gmpcompat # make -# TODO: MathSAT5 is linked against MPIR which aims to be compatible to GMP. -# Perhaps, we should also use MPIR. # - The Windows JNI headers in a reasonable LTS version: # Download the zip archive from https://jdk.java.net/ and unpack it # (e.g., https://download.java.net/openjdk/jdk11/ri/openjdk-11+28_windows-x64_bin.zip). +# +# To build mathsat bindings: ./compileForWindows.sh $MATHSAT_DIR $MPIR_DIR $JNI_DIR -# To build mathsat bindings: ./compileForWindows.sh $MATHSAT_DIR $GMP_DIR $JNI_DIR SOURCE="${BASH_SOURCE[0]}" while [ -h "$SOURCE" ]; do # resolve $SOURCE until the file is no longer a symlink From b4252d146dd9c9f21874251c96397641644865d8 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 13 Oct 2020 23:18:02 +0200 Subject: [PATCH 28/34] update some documentation about publishing solvers. --- doc/Developers.md | 42 ++++++++++++++++++++++++++---------------- 1 file changed, 26 insertions(+), 16 deletions(-) diff --git a/doc/Developers.md b/doc/Developers.md index 8c911ca29d..1a6a288faa 100644 --- a/doc/Developers.md +++ b/doc/Developers.md @@ -121,8 +121,9 @@ This is one of the most critical steps in JavaSMT development. We prefer to use the official Z3 binaries, please build from source only if necessary (e.g., in case of an important bugfix). -To publish Z3, download the **Ubuntu 14.04** binary for the [latest release](https://github.com/Z3Prover/z3/releases) -and unzip it. +To publish Z3, download the **Ubuntu 16.04**, **Windows**, and **OSX** binary for the +[latest release](https://github.com/Z3Prover/z3/releases) and unzip them. +For simpler handling, we copy the files from their `bin` directories together into one directory. Then execute the following command in the JavaSMT directory, where `$Z3_DIR` is the absolute path of the unpacked Z3 directory and `$Z3_VERSION` is the version number: @@ -131,19 +132,13 @@ ant publish-z3 -Dz3.path=$Z3_DIR/bin -Dz3.version=$Z3_VERSION ``` Finally follow the instructions shown in the message at the end. -As long as [PR #1650](https://github.com/Z3Prover/z3/pull/1650) is not merged, -you need to run the following command before running ant: -``` -patchelf --set-soname libz3.so libz3.so -``` - To publish Z3 from source, [download it](https://github.com/Z3Prover/z3) and build -it with the following command in its directory on a 64bit Ubuntu 14.04 system -(building on Ubuntu 16.04 introduces unwanted dependencies to new libstdc++ and libgomp versions): - +it with the following command in its directory on a 64bit Ubuntu 16.04 system: ``` ./configure --staticlib --java --git-describe && cd build && make -j 2 ``` +(Note that additional binaries for other operating systems need to be provided, too. +This step is currently not fully tested from our side.) Then execute the following command in the JavaSMT directory, where `$Z3_DIR` is the absolute path of the Z3 directory: ``` ant publish-z3 -Dz3.path=$Z3_DIR/build @@ -190,15 +185,30 @@ Finally follow the instructions shown in the message at the end. ### Publishing (Opti)-MathSAT5 For publishing MathSAT5, you need to use a machine with at least GCC 4.9. -First, [download the (reentrant!) binary release](http://mathsat.fbk.eu/download.html), unpack it, -and then execute the following command in the JavaSMT directory, -where `$MATHSAT_PATH` is the path to the MathSAT directory, +First, [download the (reentrant!) Linux and Windows64 binary release](http://mathsat.fbk.eu/download.html), unpack them, +then provide the necessary dependencies (GMP and MPIR) as described in the compilation scripts +(see `lib/native/source/libmathsat5j/`), and then execute the following command in the JavaSMT directory, +where `$MATHSAT_LINUX_PATH` and `$MATHSAT_WINDOWS_PATH` are the paths to the MathSAT directories, and `$MATHSAT_VERSION` is the version number of MathSAT: ``` -ant publish-mathsat -Dmathsat.path=$MATHSAT_PATH -Dgmp.path=$GMP_PATH -Dmathsat.version=$MATHSAT_VERSION +ant publish-mathsat -Dmathsat.path=$MATHSAT_LINUX_PATH \ + -Dgmp.path=$GMP_PATH \ + -Dmathsat-windows.path=$MATHSAT_WINDOWS_PATH \ + -Dmpir-windows.path=$MPIR_PATH \ + -Djdk-windows.path=JDK_11_PATH \ + -Dmathsat.version=$MATHSAT_VERSION +``` +Concrete example: +``` +ant publish-mathsat -Dmathsat.path=$TMP/mathsat-5.6.4-linux-x86_64-reentrant/ \ + -Dgmp.path=$TMP/gmp-6.1.2 \ + -Dmathsat-windows.path=$TMP/mathsat-5.6.4-win64-msvc \ + -Dmpir-windows.path=$TMP/mpir-2.7.2-win \ + -Djdk-windows.path=$TMP/jdk-11 \ + -Dmathsat.version=5.6.4 ``` Finally follow the instructions shown in the message at the end. -The same procedure applies to [OptiMathSAT](http://optimathsat.disi.unitn.it/) solver, +A similar procedure applies to [OptiMathSAT](http://optimathsat.disi.unitn.it/) solver, except the publishing command is: ``` From 1d96126198757c49d59e74a8dc52f2bf0370663f Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Thu, 22 Oct 2020 23:55:45 +0200 Subject: [PATCH 29/34] extract path-option error-handling into a common macro. --- build/build-publish-solvers.xml | 60 ++++++++++++--------------------- 1 file changed, 22 insertions(+), 38 deletions(-) diff --git a/build/build-publish-solvers.xml b/build/build-publish-solvers.xml index 6874b76d28..109b768491 100644 --- a/build/build-publish-solvers.xml +++ b/build/build-publish-solvers.xml @@ -281,21 +281,9 @@ SPDX-License-Identifier: Apache-2.0 - - Please specify the path to the Mathsat5 source folder (Windows version) with the flag -Dmathsat-windows.path=/path/to/mathsat. - The path has to point to the root Mathsat5 folder. - Note that shell substitutions do not work and a full absolute path has to be specified. - - - Please specify the path to the MPIR source folder (Windows version) with the flag -Dmpir-windows.path=/path/to/mpir. - The path has to point to the root MPIR folder. - Note that shell substitutions do not work and a full absolute path has to be specified. - - - Please specify the path to the JDK source folder (Windows version) with the flag -Djdk-windows.path=/path/to/jdk. - The path has to point to the root JDK folder. - Note that shell substitutions do not work and a full absolute path has to be specified. - + + + @@ -327,17 +315,8 @@ SPDX-License-Identifier: Apache-2.0 - - Please specify the path to the Mathsat5 source folder with the flag -Dmathsat.path=/path/to/mathsat. - The path has to point to the root Mathsat5 folder. - Note that shell substitutions do not work and a full absolute path has to be specified. - - - Please specify the path to the GMP source folder with the flag -Dgmp.path=/path/to/gmp. - The path has to point to the root Mathsat5 folder. - Note that shell substitutions do not work and a full absolute path has to be specified. - - + + @@ -382,18 +361,9 @@ SPDX-License-Identifier: Apache-2.0 - - Please specify the path to the Yices2 source folder with the flag -Dyices2.path=/path/to/yices2. - The path has to point to the root Yices2 folder. - - - Please specify the path to the GMP source folder with the flag -Dgmp.path=/path/to/gmp. - The path has to point to the root GMP folder. - - - Please specify the path to the GPERF source folder with the flag -Dgperf.path=/path/to/gperf. - The path has to point to the root GPERF folder. - + + + @@ -457,4 +427,18 @@ SPDX-License-Identifier: Apache-2.0 + + + + + + + - + Please specify the path to the @{targetName} with the following flag: + -D@{pathOption}=@{defaultPath} + The path has to point to the root of the @{targetName}. + Note that shell substitutions do not work and a full absolute path is preferred. + + + From b3640df14b82763247b3f9c1cac2b36fc26ce483 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Fri, 23 Oct 2020 00:11:36 +0200 Subject: [PATCH 30/34] split ivy package for MathSAT into Linux and Windows configuration. And update documentation for publishing MathSAT. --- build/build-publish-solvers.xml | 134 ++++++++++++++++++------------- doc/Developers.md | 52 ++++++------ solvers_ivy_conf/ivy_mathsat.xml | 13 +-- 3 files changed, 115 insertions(+), 84 deletions(-) diff --git a/build/build-publish-solvers.xml b/build/build-publish-solvers.xml index 109b768491..179aed4c02 100644 --- a/build/build-publish-solvers.xml +++ b/build/build-publish-solvers.xml @@ -278,46 +278,27 @@ SPDX-License-Identifier: Apache-2.0 - - - - - - - - - - + + - - + + - - - Please specify the MathSAT5 version with the flag -Dmathsat.version=... . - - - - - - - - - + + - - + + - + @@ -325,34 +306,77 @@ SPDX-License-Identifier: Apache-2.0 - - - + + - - Please specify the @{flag} version with the flag -Dmathsat.version=... . - + + + + + + + + + + - + + + Please specify the MathSAT5 version with the flag -Dmathsat.version=... . + + + Please specify the mathsat version with the flag -Dmathsat.version=... . + - - - + + + + - - - You now want to run - svn add repository/${ivy.organisation}/${ivy.module}/*-${mathsat.version}* - svn ci repository/${ivy.organisation}/${ivy.module} -m"publish version ${mathsat.version} of @{flag} Solver" - to make the new version publicly available. - - + + + + + + + You now want to run + svn add repository/${ivy.organisation}/${ivy.module}/*-${mathsat.version}* + svn ci repository/${ivy.organisation}/${ivy.module} -m"publish version ${mathsat.version} of mathsat Solver" + to make the new version publicly available. + + + + + Please specify the @{flag} version with the flag -Dmathsat.version=... . + + + + + + + + + + + You now want to run + svn add repository/${ivy.organisation}/${ivy.module}/*-${mathsat.version}* + svn ci repository/${ivy.organisation}/${ivy.module} -m"publish version ${mathsat.version} of optimathsat Solver" + to make the new version publicly available. + - + - - - + + + - From ed6f9593527d7e56b6d19512e20037b9970af131 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Thu, 22 Oct 2020 23:56:20 +0200 Subject: [PATCH 31/34] unify error messages for publishing Z3. --- build/build-publish-solvers.xml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/build/build-publish-solvers.xml b/build/build-publish-solvers.xml index 179aed4c02..4bffef4679 100644 --- a/build/build-publish-solvers.xml +++ b/build/build-publish-solvers.xml @@ -21,9 +21,12 @@ SPDX-License-Identifier: Apache-2.0 description="Copy Z3 binaries to the root folder along with the version postfix. This package provides the JNI for direct usage."> - Please specify the path to Z3 with the flag -Dz3.path=/path/to/z3. + Please specify the path to Z3 with the flag -Dz3.path=/path/to/z3 (e.g. `bin` directory). The path has to point to the root Z3 folder and can be relative or absolute. Note that shell substitutions do not work. + Please provide all releases (Linux64, MacOS, and Windows64) together in the same root directory, + e.g., copy the releases (especially the content of their `bin` directories) together into one directory. + The only overlap between those releases is the JAR file, which should be equal anyway. From dd2efb1db78e390f9c6b52621ce344025b9da0f8 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 31 Oct 2020 15:12:31 +0100 Subject: [PATCH 32/34] split ivy package for Z3 into Linux, Windows, OS configuration. --- solvers_ivy_conf/ivy_z3.xml | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/solvers_ivy_conf/ivy_z3.xml b/solvers_ivy_conf/ivy_z3.xml index e7a0e51fc1..cc9cb523f8 100644 --- a/solvers_ivy_conf/ivy_z3.xml +++ b/solvers_ivy_conf/ivy_z3.xml @@ -23,21 +23,25 @@ SPDX-License-Identifier: Apache-2.0 - + + + + + - - + + - - + + - - + + - + From 5035293b39c13804dabf4ab06da221a3459296e8 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 31 Oct 2020 15:31:36 +0100 Subject: [PATCH 33/34] getting z3.version can crash easily. Lets add a hint how to set the version number. --- build/build-publish-solvers.xml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/build/build-publish-solvers.xml b/build/build-publish-solvers.xml index 4bffef4679..a9383d0849 100644 --- a/build/build-publish-solvers.xml +++ b/build/build-publish-solvers.xml @@ -61,7 +61,8 @@ SPDX-License-Identifier: Apache-2.0 e.g., copy the releases (especially the content of their `bin` directories) together into one directory. The only overlap between those releases is the JAR file, which should be equal anyway. - + Option -Dz3.version=... not specified. Trying to determine z3.version from git repository. This will crash if git repository is not available. + From 0f0460074cd0803e2af6b60b51a12d79839b1d5f Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 9 Nov 2020 13:25:32 +0100 Subject: [PATCH 34/34] update MathSAT5 to version 5.6.5. This version contains a fix for model generation in LIA+Array theory. --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 63e4725819..0605a25eba 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -157,7 +157,7 @@ SPDX-License-Identifier: Apache-2.0 - +