From 2b5e801b6eac2fee164a56b2553e3d6faee12590 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 11 Sep 2024 23:51:45 +0200 Subject: [PATCH 01/63] initial steps to provide multiple binaries of Z3. Not tested, not finished, just a draft. --- build/build-publish-solvers/solver-z3.xml | 28 +++++++++++++++++------ doc/Developers-How-to-Release-into-Ivy.md | 14 ++++++++---- solvers_ivy_conf/ivy_z3.xml | 12 +++++++--- 3 files changed, 39 insertions(+), 15 deletions(-) diff --git a/build/build-publish-solvers/solver-z3.xml b/build/build-publish-solvers/solver-z3.xml index 1b5045aa81..240043e645 100644 --- a/build/build-publish-solvers/solver-z3.xml +++ b/build/build-publish-solvers/solver-z3.xml @@ -25,7 +25,7 @@ SPDX-License-Identifier: Apache-2.0 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 (i.e., the path is ending with '/bin') 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, + Please provide all releases (Linux, MacOS, and Windows for x64 architecture) 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. Additionally, make the Java sources available in this directory. @@ -33,6 +33,14 @@ SPDX-License-Identifier: Apache-2.0 - copying the content of sources-zip into the current directory (or vice versa) - executing `python scripts/mk_make.py --java` to generate all Java related files. Executing `make` is not required. + + Please specify the path to Z3 (ARM64 version) with the flag -Dz3.pathArm64=/path/to/z3-arm64 (e.g. `bin` directory). + The path has to point to the root Z3 folder (i.e., the path is ending with '/bin') and can be relative or absolute. + Note that shell substitutions do not work. + Please provide all releases (Linux, MacOS, and Windows for ARM64 architecture) 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. + @@ -45,14 +53,20 @@ SPDX-License-Identifier: Apache-2.0 Please run 'patchelf --set-soname libz3.so ${z3.path}/libz3.so'. - - + + + + - - + + + + - - + + + + diff --git a/doc/Developers-How-to-Release-into-Ivy.md b/doc/Developers-How-to-Release-into-Ivy.md index 838de831fd..e4d25392fd 100644 --- a/doc/Developers-How-to-Release-into-Ivy.md +++ b/doc/Developers-How-to-Release-into-Ivy.md @@ -46,18 +46,22 @@ there are scripts for publishing available at the root of the [Ivy Repository](h 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**, **Windows**, and **OSX** binary +### From official binaries (for Linux, Windows, and OSX) + +To publish Z3, download the **Linux**, **Windows**, and **OSX** binary (for both, x64 and ARM64 architecture) and the sources (for JavaDoc) for the [latest release](https://github.com/Z3Prover/z3/releases) and unzip them. In the unpacked sources directory, prepare Java sources via `python scripts/mk_make.py --java`. -For simpler handling, we then copy the files from the three `bin` directories together into one directory, -and include the sources (we can keep the internal structure of each directory, just copy them above each other). +For simpler handling, we then copy the files together into two directories: +- use the source directory as `Z3_DIR`. +- from the three `*x64*/bin` directories together into directory `$Z3_DIR`, +- from the three `*arm64*/bin` directories together into another directory `Z3_DIR_ARM64`. 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: ``` -ant publish-z3 -Dz3.path=$Z3_DIR/bin -Dz3.version=$Z3_VERSION +ant publish-z3 -Dz3.path=$Z3_DIR/bin -Dz3.pathArm64=$Z3_DIR_ARM64/bin -Dz3.version=$Z3_VERSION ``` -Finally follow the instructions shown in the message at the end. +Finally, follow the instructions shown in the message at the end. #### Optional (from source for Linux target with older GLIBC) This step is for the following use case: diff --git a/solvers_ivy_conf/ivy_z3.xml b/solvers_ivy_conf/ivy_z3.xml index 30b3905663..268d0af4f5 100644 --- a/solvers_ivy_conf/ivy_z3.xml +++ b/solvers_ivy_conf/ivy_z3.xml @@ -34,14 +34,20 @@ SPDX-License-Identifier: Apache-2.0 - + + + - + + + - + + + From 2349bae553fa04837c512d79f23bb3c29ada79e1 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 17 Sep 2024 22:07:48 +0200 Subject: [PATCH 02/63] configure Ivy with a new classifier for 'arch', tested for Z3 binary. --- build.xml | 10 +++-- build/build-ivy.xml | 4 +- build/build-publish-solvers/macros.xml | 7 ++-- build/build-publish-solvers/solver-z3.xml | 37 ++++++++++-------- build/ivysettings.xml | 9 +++-- lib/native/x86_64-linux/libz3.so | 2 +- lib/native/x86_64-linux/libz3java.so | 2 +- solvers_ivy_conf/ivy_z3.xml | 47 +++++++++++++++-------- 8 files changed, 70 insertions(+), 48 deletions(-) diff --git a/build.xml b/build.xml index 9710d2cc88..7dad4a974f 100644 --- a/build.xml +++ b/build.xml @@ -79,12 +79,14 @@ SPDX-License-Identifier: Apache-2.0 - + - + + + - - + + diff --git a/build/build-ivy.xml b/build/build-ivy.xml index b5b6b733b5..e571206b34 100644 --- a/build/build-ivy.xml +++ b/build/build-ivy.xml @@ -66,7 +66,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -80,7 +80,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/build/build-publish-solvers/macros.xml b/build/build-publish-solvers/macros.xml index f7145604d8..d698480928 100644 --- a/build/build-publish-solvers/macros.xml +++ b/build/build-publish-solvers/macros.xml @@ -12,7 +12,8 @@ SPDX-License-Identifier: Apache-2.0 + xmlns:ivy="antlib:org.apache.ivy.ant" + xmlns:e="http://ant.apache.org/ivy/extra"> @@ -38,12 +39,12 @@ SPDX-License-Identifier: Apache-2.0 You now want to run - svn add repository/${ivy.organisation}/${ivy.module}/*-@{solverVersion}* + svn add repository/${ivy.organisation}/${ivy.module}/*-@{solverVersion}* repository/${ivy.organisation}/${ivy.module}/*/*-@{solverVersion}* svn ci repository/${ivy.organisation}/${ivy.module} -m"publish version @{solverVersion} of @{solverName} Solver" to make the new version publicly available. diff --git a/build/build-publish-solvers/solver-z3.xml b/build/build-publish-solvers/solver-z3.xml index 240043e645..a9153b36d8 100644 --- a/build/build-publish-solvers/solver-z3.xml +++ b/build/build-publish-solvers/solver-z3.xml @@ -34,7 +34,7 @@ SPDX-License-Identifier: Apache-2.0 - executing `python scripts/mk_make.py --java` to generate all Java related files. Executing `make` is not required. - Please specify the path to Z3 (ARM64 version) with the flag -Dz3.pathArm64=/path/to/z3-arm64 (e.g. `bin` directory). + Please specify the path to Z3 (ARM64 version) with the flag -Dz3.pathArm64=/path/to/z3 (e.g. `bin` directory). The path has to point to the root Z3 folder (i.e., the path is ending with '/bin') and can be relative or absolute. Note that shell substitutions do not work. Please provide all releases (Linux, MacOS, and Windows for ARM64 architecture) together in the same root directory, @@ -52,21 +52,24 @@ SPDX-License-Identifier: Apache-2.0 libz3.so has missing SONAME property. Please run 'patchelf --set-soname libz3.so ${z3.path}/libz3.so'. - - - - - - - - - - + + + + + + + + + + + + + - - - - + + + + @@ -76,7 +79,7 @@ SPDX-License-Identifier: Apache-2.0 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, + Please provide all releases (Linux, MacOS, and Windows) 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. Additionally, make the Java sources available in this directory. @@ -92,7 +95,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/build/ivysettings.xml b/build/ivysettings.xml index be96cf00b5..39a5864f2e 100644 --- a/build/ivysettings.xml +++ b/build/ivysettings.xml @@ -22,14 +22,17 @@ SPDX-License-Identifier: Apache-2.0 - + - + - + diff --git a/lib/native/x86_64-linux/libz3.so b/lib/native/x86_64-linux/libz3.so index fb25e3fd75..29c5b70571 120000 --- a/lib/native/x86_64-linux/libz3.so +++ b/lib/native/x86_64-linux/libz3.so @@ -1 +1 @@ -../../java/runtime-z3/libz3.so \ No newline at end of file +../../java/runtime-z3/x64/libz3.so \ No newline at end of file diff --git a/lib/native/x86_64-linux/libz3java.so b/lib/native/x86_64-linux/libz3java.so index b6422c8714..c287c055d4 120000 --- a/lib/native/x86_64-linux/libz3java.so +++ b/lib/native/x86_64-linux/libz3java.so @@ -1 +1 @@ -../../java/runtime-z3/libz3java.so \ No newline at end of file +../../java/runtime-z3/x64/libz3java.so \ No newline at end of file diff --git a/solvers_ivy_conf/ivy_z3.xml b/solvers_ivy_conf/ivy_z3.xml index 268d0af4f5..35f36b0231 100644 --- a/solvers_ivy_conf/ivy_z3.xml +++ b/solvers_ivy_conf/ivy_z3.xml @@ -23,31 +23,44 @@ SPDX-License-Identifier: Apache-2.0 - - - - - + + + + + + + + + + + + + + + - - - - + + + + + - - - - + + + + + - - - - + + + + + From 68bab2bbc9cf7b4673487df81f756eb03ab4f9c3 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 29 Sep 2024 09:28:12 +0200 Subject: [PATCH 03/63] #380: reduce manual steps for publishing Z3, create copies of library for backwards compatibility. --- build/build-publish-solvers/solver-z3.xml | 166 ++++++++++++++-------- doc/Developers-How-to-Release-into-Ivy.md | 36 +++-- solvers_ivy_conf/ivy_z3.xml | 23 +-- 3 files changed, 143 insertions(+), 82 deletions(-) diff --git a/build/build-publish-solvers/solver-z3.xml b/build/build-publish-solvers/solver-z3.xml index a9153b36d8..e55f42c550 100644 --- a/build/build-publish-solvers/solver-z3.xml +++ b/build/build-publish-solvers/solver-z3.xml @@ -18,32 +18,62 @@ SPDX-License-Identifier: Apache-2.0 - - + - 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 (i.e., the path is ending with '/bin') and can be relative or absolute. - Note that shell substitutions do not work. - Please provide all releases (Linux, MacOS, and Windows for x64 architecture) 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. - Additionally, make the Java sources available in this directory. - This can be done by: - - copying the content of sources-zip into the current directory (or vice versa) - - executing `python scripts/mk_make.py --java` to generate all Java related files. Executing `make` is not required. - - - Please specify the path to Z3 (ARM64 version) with the flag -Dz3.pathArm64=/path/to/z3 (e.g. `bin` directory). - The path has to point to the root Z3 folder (i.e., the path is ending with '/bin') and can be relative or absolute. - Note that shell substitutions do not work. - Please provide all releases (Linux, MacOS, and Windows for ARM64 architecture) 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. + INFO + Please specify the path to Z3 sources directory with the flag '-Dz3.path=/path/to/z3/z3-unpacked-sources'. + The path should contain directories like './src/' and './scripts/', and can be relative or absolute. + Please provide all unpacked releases (Linux, MacOS, and Windows for x64 and arm64 + architecture) in the same parent directory './../' above the 'z3.path'. + This script does not expect other z3-related files or directories in the parent directory. + For example, the directory structure can look like this: + + z3/ // <-- parent directory + |-- z3-4.13.2-arm64-glibc-2.34/ // <-- unpacked release artifact + |-- z3-4.13.2-arm64-osx-11.0/ + |-- z3-4.13.2-arm64-win/ + |-- z3-4.13.2-x64-glibc-2.35/ + |-- z3-4.13.2-x64-osx-12.7.6/ + |-- z3-4.13.2-x64-win/ + |-- z3-z3-4.13.2/ // <-- sources directory as 'z3.path' + + This can be achieved by: + - download all artifacts (Linux, MacOS, and Windows for x64 and arm64 architecture) + from the Z3 release webpage (https://github.com/Z3Prover/z3/releases) + - create an empty directory 'z3/' and unpack all artifact into it. + - in the sources directory execute `python scripts/mk_make.py --java` to generate all + Java related files (required for JavaDoc). Executing `make` is not required. - + + + + + + + + + + + + + + + + + + + + + + + + + + + - + @@ -53,43 +83,39 @@ SPDX-License-Identifier: Apache-2.0 Please run 'patchelf --set-soname libz3.so ${z3.path}/libz3.so'. - - - - - - + + + + - - - - + + + + - - - - + + + + - + + + + + + - - - 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 (Linux, MacOS, and Windows) 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. - Additionally, make the Java sources available in this directory. - This can be done by: - - copying the content of sources-zip into the current directory (or vice versa) - - executing `python scripts/mk_make.py --java` to generate all Java related files. Executing `make` is not required. - + Option -Dz3.version=... not specified. Trying to determine z3.version from git repository. This will fail if git repository is not available. - + @@ -97,20 +123,38 @@ SPDX-License-Identifier: Apache-2.0 description="Publish Z3 binaries to Ivy repo."> + + + + Lets copy the files for architecture x64 into main directory, for backwards compatibility. + Afterwards, please execute the SVN command from above. + + + + + + - - - - + + + + - - + + @@ -133,7 +177,7 @@ SPDX-License-Identifier: Apache-2.0 failonwarning="false" overview="doc/javadoc_overview.html" > - + @@ -147,8 +191,8 @@ SPDX-License-Identifier: Apache-2.0 - - + + diff --git a/doc/Developers-How-to-Release-into-Ivy.md b/doc/Developers-How-to-Release-into-Ivy.md index e4d25392fd..80a8b3c221 100644 --- a/doc/Developers-How-to-Release-into-Ivy.md +++ b/doc/Developers-How-to-Release-into-Ivy.md @@ -50,19 +50,32 @@ please build from source only if necessary (e.g., in case of an important bugfix To publish Z3, download the **Linux**, **Windows**, and **OSX** binary (for both, x64 and ARM64 architecture) and the sources (for JavaDoc) for the [latest release](https://github.com/Z3Prover/z3/releases) and unzip them. -In the unpacked sources directory, prepare Java sources via `python scripts/mk_make.py --java`. -For simpler handling, we then copy the files together into two directories: -- use the source directory as `Z3_DIR`. -- from the three `*x64*/bin` directories together into directory `$Z3_DIR`, -- from the three `*arm64*/bin` directories together into another directory `Z3_DIR_ARM64`. +For example, the directory structure can look like this: + +``` +z3/ // <-- parent directory + |-- z3-4.13.2-arm64-glibc-2.34/ // <-- unpacked release artifact + |-- z3-4.13.2-arm64-osx-11.0/ + |-- z3-4.13.2-arm64-win/ + |-- z3-4.13.2-x64-glibc-2.35/ + |-- z3-4.13.2-x64-osx-12.7.6/ + |-- z3-4.13.2-x64-win/ + |-- z3-z3-4.13.2/ // <-- sources directory used as 'z3.path' +``` + +In the unpacked sources directory, prepare Java sources via `python3 scripts/mk_make.py --java`. 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: +where `$Z3_DIR` is the path of the sources directory and `$Z3_VERSION` is the version number: ``` -ant publish-z3 -Dz3.path=$Z3_DIR/bin -Dz3.pathArm64=$Z3_DIR_ARM64/bin -Dz3.version=$Z3_VERSION +ant publish-z3 -Dz3.path=$Z3_DIR -Dz3.version=$Z3_VERSION +``` +Example: +``` +ant publish-z3 -Dz3.path=/workspace/solvers/z3/z3-z3-4.13.2 -Dz3.version=4.13.2 ``` Finally, follow the instructions shown in the message at the end. + #### Optional (from source for Linux target with older GLIBC) This step is for the following use case: Newer releases of Z3 depend on newer versions of GLIBC (>=v2.35), @@ -73,15 +86,16 @@ in which the following build command can be run in the unpacked source directory ``` python3 scripts/mk_make.py --java && cd build && make -j 2 ``` -Afterwards copy the native libraries for Linux (`libz3.so` and `libz3java.so`) from the directory `./build` into `./bin`. +Afterwards copy the native libraries for Linux (`libz3.so` and `libz3java.so`) from the directory +`./build` into `./bin` (if needed, adjust the directory to match the x64 or arm64 path for Linux). Then perform as written above with adding the additional pre-compiled binaries for other operating systems, and publish the directory `./bin` with an ant command like the one from above: ``` -ant publish-z3 -Dz3.path=$Z3_DIR/bin -Dz3.version=$Z3_VERSION-glibc_2.27 +ant publish-z3 -Dz3.path=$Z3_DIR -Dz3.version=$Z3_VERSION-glibc_2.27 ``` -#### Optional (outdated: from source for Linux target) +#### Optional (from source for Linux target) (Info: this step is outdated and no longer used for releases of JavaSMT) 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 16.04 system: ``` diff --git a/solvers_ivy_conf/ivy_z3.xml b/solvers_ivy_conf/ivy_z3.xml index 35f36b0231..51a999c915 100644 --- a/solvers_ivy_conf/ivy_z3.xml +++ b/solvers_ivy_conf/ivy_z3.xml @@ -27,8 +27,8 @@ SPDX-License-Identifier: Apache-2.0 - - + + @@ -37,29 +37,32 @@ SPDX-License-Identifier: Apache-2.0 - - + + - + + - + - - - - + + + + From fa64e1df1d1876f608d19c81cde10132705ff53c Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 29 Sep 2024 10:12:51 +0200 Subject: [PATCH 04/63] #380: make cache-pattern more similar to default pattern. This should keep the existing cache valid and re-usable. Otherwise, we would create a new cache structure within the existing cache, with redundant entries. With this change, we limit the redundancy to arch- or classifier-specific entries. --- build/ivysettings.xml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/build/ivysettings.xml b/build/ivysettings.xml index 39a5864f2e..627892667a 100644 --- a/build/ivysettings.xml +++ b/build/ivysettings.xml @@ -22,17 +22,17 @@ SPDX-License-Identifier: Apache-2.0 - + - + + + + artifactPattern="[organisation]/[module]/[type]s/([arch]/)[artifact]-[revision](-[classifier]).[ext]"/> From a3021abfa2c364fbae54605faa719a0261d8cba4 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 29 Sep 2024 10:45:26 +0200 Subject: [PATCH 05/63] fix typo in property usage. --- build.xml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/build.xml b/build.xml index 7dad4a974f..991d1d713c 100644 --- a/build.xml +++ b/build.xml @@ -81,9 +81,9 @@ SPDX-License-Identifier: Apache-2.0 - - - + + + From 5d70c5fa3d529a9ff4c5fd0cfb53cb7000f6e680 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 29 Sep 2024 11:11:29 +0200 Subject: [PATCH 06/63] update Z3 to v4.13.0. We could include x64 and ARM64 dependencies for Z3. However, the default stays by only x64. --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index ac4c58e555..e93ef50770 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -161,7 +161,7 @@ SPDX-License-Identifier: Apache-2.0 - + From ddc9977b0168dffec360eb11e59d039d0d835743 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 29 Sep 2024 16:12:09 +0200 Subject: [PATCH 07/63] Maven: change publication pattern, do not use classifier for plain Jars, but only all other files. This cleanup aligns better with Maven guidelines. This is a small change for all upcoming publications to Maven and the Maven users. --- build/build-maven-publish.xml | 61 ++++++++++++++++++----------------- 1 file changed, 32 insertions(+), 29 deletions(-) diff --git a/build/build-maven-publish.xml b/build/build-maven-publish.xml index e6015b556f..0f5c74a704 100644 --- a/build/build-maven-publish.xml +++ b/build/build-maven-publish.xml @@ -84,8 +84,11 @@ SPDX-License-Identifier: Apache-2.0 + - + + @@ -104,7 +107,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -114,8 +117,8 @@ SPDX-License-Identifier: Apache-2.0 - - + + @@ -130,10 +133,10 @@ SPDX-License-Identifier: Apache-2.0 - - - - + + + + - - - - - - + + + + + + - - + + @@ -179,9 +182,9 @@ SPDX-License-Identifier: Apache-2.0 - - - + + + - - - + + + - - - - - + + + + + - + - + From 14699d67410af4457638acd599ddd7700e8d23b9 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 29 Sep 2024 21:46:50 +0200 Subject: [PATCH 08/63] #380: rewrite Maven publication step to support x64 and arm64 architecture. Additionally, we upload Java sources and JavaDoc for z3 to the Maven repository. We need to test whether the uploaded files work as expected. --- build/build-maven-publish.xml | 27 +++++++++++++++++++++------ lib/ivy.xml | 2 +- 2 files changed, 22 insertions(+), 7 deletions(-) diff --git a/build/build-maven-publish.xml b/build/build-maven-publish.xml index 0f5c74a704..a0364726ff 100644 --- a/build/build-maven-publish.xml +++ b/build/build-maven-publish.xml @@ -145,16 +145,31 @@ SPDX-License-Identifier: Apache-2.0 + + + - - - - - - + + + + + + + + + + + + + + + + + - + From 78a298e03cf29385d4d451baebc73244c1d3ef17 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 29 Sep 2024 21:59:52 +0200 Subject: [PATCH 09/63] update Maven examples as expected to work. Not yet tested. --- doc/Example-Maven-Project/pom.xml | 18 ++++++++++-------- doc/Example-Maven-Web-Project/pom.xml | 18 ++++++++++-------- 2 files changed, 20 insertions(+), 16 deletions(-) diff --git a/doc/Example-Maven-Project/pom.xml b/doc/Example-Maven-Project/pom.xml index ec6770c883..952c2a63dc 100644 --- a/doc/Example-Maven-Project/pom.xml +++ b/doc/Example-Maven-Project/pom.xml @@ -16,7 +16,7 @@ SPDX-License-Identifier: Apache-2.0 org.sosy_lab.java_smt_example java-smt-maven-example - 1.10 + 1.11 java-smt-maven-example Example Maven project to show how to use JavaSMT with native solver libraries. https://github.com/sosy-lab/java-smt @@ -69,6 +69,10 @@ SPDX-License-Identifier: Apache-2.0 dependency ${project.build.directory}/${project.dependency.relativepath} + + x64 + + 5.0.0 0.4.0-g4dbf3b1f 3.2.2-g1a89c229 @@ -78,7 +82,7 @@ SPDX-License-Identifier: Apache-2.0 2.6.0-g2f72cc0e 4.1.1-734-g3732f7e08 2.6.2-396-g194350c1 - 4.12.5 + 4.13.0 @@ -102,22 +106,20 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-z3 ${z3.version} - jar - com.microsoft.z3 org.sosy-lab javasmt-solver-z3 ${z3.version} so - libz3 + libz3-${system.arch} org.sosy-lab javasmt-solver-z3 ${z3.version} so - libz3java + libz3java-${system.arch} @@ -374,14 +376,14 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-z3 so - libz3java + libz3java-${system.arch} libz3java.so org.sosy-lab javasmt-solver-z3 so - libz3 + libz3-${system.arch} libz3.so diff --git a/doc/Example-Maven-Web-Project/pom.xml b/doc/Example-Maven-Web-Project/pom.xml index 91342fa916..cf8c6a9764 100644 --- a/doc/Example-Maven-Web-Project/pom.xml +++ b/doc/Example-Maven-Web-Project/pom.xml @@ -16,7 +16,7 @@ SPDX-License-Identifier: Apache-2.0 org.sosy_lab.java_smt_web_example java-smt-web-example - 1.10 + 1.11 war java-smt-maven-web-example Example Maven project to show how to use JavaSMT with native solver libraries in a web project. @@ -70,6 +70,10 @@ SPDX-License-Identifier: Apache-2.0 dependency ${project.build.directory}/${project.dependency.relativepath} + + x64 + + 5.0.0 0.4.0-g4dbf3b1f 3.2.2-g1a89c229 @@ -79,7 +83,7 @@ SPDX-License-Identifier: Apache-2.0 2.6.0-g2f72cc0e 4.1.1-734-g3732f7e08 2.6.2-396-g194350c1 - 4.12.5 + 4.13.0 @@ -103,22 +107,20 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-z3 ${z3.version} - jar - com.microsoft.z3 org.sosy-lab javasmt-solver-z3 ${z3.version} so - libz3 + libz3-${system.arch} org.sosy-lab javasmt-solver-z3 ${z3.version} so - libz3java + libz3java-${system.arch} @@ -421,14 +423,14 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-z3 so - libz3java + libz3java-${system.arch} libz3java.so org.sosy-lab javasmt-solver-z3 so - libz3 + libz3-${system.arch} libz3.so From a55cfe7c6aabce12246c76c4a9618e0a9a7b5d20 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 29 Sep 2024 22:56:01 +0200 Subject: [PATCH 10/63] #380: update readme to show our support for ARM64. --- README.md | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 4d496e0ff8..36e92128ef 100644 --- a/README.md +++ b/README.md @@ -56,7 +56,7 @@ Only a few SMT solvers provide support for theories like Arrays, Floating Point, Currently JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started.md) for installation): -| SMT Solver | Linux64 | Windows64 | MacOS | Description | +| SMT Solver | Linux | Windows | MacOS | Description | | --- |:---:|:---:|:---:|:--- | | [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark: | :heavy_check_mark: | | a fast solver for bitvector logic | | [Boolector](https://boolector.github.io/) | :heavy_check_mark: | | | a fast solver for bitvector logic, misses formula introspection, deprecated | @@ -70,12 +70,17 @@ Currently JavaSMT supports several SMT solvers (see [Getting Started](doc/Gettin | [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: | [maybe](https://github.com/sosy-lab/java-smt/pull/215) | | | | [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | mature and well-known solver | +#### Operating System and Architecture Support We support a reasonable list of operating systems and versions. Our main target is Linux (64-bit, mainly Ubuntu 22.04 or newer, several solver libraries also work on Ubuntu 18.04, or comparable Linux distributions). -Windows 10/11 and MacOS are supported for several SMT solvers (with limited hardware for testing). -If a specific operating system is missing and required, please do not hesitate and open an issue! +Windows 10/11 and MacOS are supported for several SMT solvers. +Our main development architecture is x64 (x86-64). +We also provide some solvers for ARM64 (AArch64 for ARMv8-A), e.g., Java-based SMT solvers and Z3. +If a specific operating system or architecture is missing and required, +please do not hesitate and open an issue! +#### Solver Features The following features are supported (depending on the used SMT solver): - Satisfiability checking From 9d6830600b15ed8c2de975b1acfe93bf7e07ba09 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 12 Oct 2024 15:08:49 +0200 Subject: [PATCH 11/63] #380: make basic configurations for Z3 public. Let the user decide what to load, e.g. on a minimal system only load for one specific OS and arch. --- solvers_ivy_conf/ivy_z3.xml | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/solvers_ivy_conf/ivy_z3.xml b/solvers_ivy_conf/ivy_z3.xml index 51a999c915..0aba0d25d2 100644 --- a/solvers_ivy_conf/ivy_z3.xml +++ b/solvers_ivy_conf/ivy_z3.xml @@ -26,19 +26,20 @@ SPDX-License-Identifier: Apache-2.0 - + - - - - - - - + + + + + + + + From 321da3453fcc82de061b9cc4723fd3a92ba51c60 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 12 Oct 2024 16:04:52 +0200 Subject: [PATCH 12/63] Z3: update to v4.13.2 --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 0d01084393..a0747a13fd 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -161,7 +161,7 @@ SPDX-License-Identifier: Apache-2.0 - + From bbfb72796e734c721cb83989eba5898f11ede6aa Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 12 Oct 2024 16:04:52 +0200 Subject: [PATCH 13/63] Z3: update build-scripts for v4.13.3 --- build.xml | 2 +- build/build-publish-solvers/solver-z3.xml | 8 +++----- doc/Developers-How-to-Release-into-Ivy.md | 16 ++++++++-------- solvers_ivy_conf/ivy_z3.xml | 3 --- 4 files changed, 12 insertions(+), 17 deletions(-) diff --git a/build.xml b/build.xml index 991d1d713c..6915258559 100644 --- a/build.xml +++ b/build.xml @@ -81,7 +81,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/build/build-publish-solvers/solver-z3.xml b/build/build-publish-solvers/solver-z3.xml index e55f42c550..855f8c5813 100644 --- a/build/build-publish-solvers/solver-z3.xml +++ b/build/build-publish-solvers/solver-z3.xml @@ -48,8 +48,6 @@ SPDX-License-Identifier: Apache-2.0 - @@ -64,7 +62,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -86,8 +84,8 @@ SPDX-License-Identifier: Apache-2.0 - - + + diff --git a/doc/Developers-How-to-Release-into-Ivy.md b/doc/Developers-How-to-Release-into-Ivy.md index 80a8b3c221..3a85e192b4 100644 --- a/doc/Developers-How-to-Release-into-Ivy.md +++ b/doc/Developers-How-to-Release-into-Ivy.md @@ -54,13 +54,13 @@ For example, the directory structure can look like this: ``` z3/ // <-- parent directory - |-- z3-4.13.2-arm64-glibc-2.34/ // <-- unpacked release artifact - |-- z3-4.13.2-arm64-osx-11.0/ - |-- z3-4.13.2-arm64-win/ - |-- z3-4.13.2-x64-glibc-2.35/ - |-- z3-4.13.2-x64-osx-12.7.6/ - |-- z3-4.13.2-x64-win/ - |-- z3-z3-4.13.2/ // <-- sources directory used as 'z3.path' + |-- z3-4.13.3-arm64-glibc-2.34/ // <-- unpacked release artifact + |-- z3-4.13.3-arm64-osx-13.7/ + |-- z3-4.13.3-arm64-win/ + |-- z3-4.13.3-x64-glibc-2.35/ + |-- z3-4.13.3-x64-osx-13.7/ + |-- z3-4.13.3-x64-win/ + |-- z3-z3-4.13.3/ // <-- sources directory used as 'z3.path' ``` In the unpacked sources directory, prepare Java sources via `python3 scripts/mk_make.py --java`. @@ -71,7 +71,7 @@ ant publish-z3 -Dz3.path=$Z3_DIR -Dz3.version=$Z3_VERSION ``` Example: ``` -ant publish-z3 -Dz3.path=/workspace/solvers/z3/z3-z3-4.13.2 -Dz3.version=4.13.2 +ant publish-z3 -Dz3.path=/workspace/solvers/z3/z3-z3-4.13.3 -Dz3.version=4.13.3 ``` Finally, follow the instructions shown in the message at the end. diff --git a/solvers_ivy_conf/ivy_z3.xml b/solvers_ivy_conf/ivy_z3.xml index 0aba0d25d2..7a860d6ff5 100644 --- a/solvers_ivy_conf/ivy_z3.xml +++ b/solvers_ivy_conf/ivy_z3.xml @@ -47,11 +47,8 @@ SPDX-License-Identifier: Apache-2.0 - From d6019c6d5843534fdbca6d129aaf40e891f5e596 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 12 Oct 2024 20:51:15 +0200 Subject: [PATCH 14/63] Z3: avoid regression error. See https://github.com/Z3Prover/z3/issues/7419 for details. If required, the Z3 parser automatically converts Boolean formulas `f` to e.g. `ITE(f 1 0)`, which makes them comparable to Integer symbols and numbers 0/1. --- .../test/SolverFormulaIODeclarationsTest.java | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java index 2ea0975084..5701551726 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java @@ -201,11 +201,23 @@ public void parseDeclareConflictInQueryTest3() { } @Test - public void parseDeclareConflictBeforeQueryTest() { + public void parseDeclareConflictBeforeQueryTest_IntBool() { requireIntegers(); @SuppressWarnings("unused") IntegerFormula var = imgr.makeVariable("x"); String query = "(declare-fun x () Bool)(assert (= 0 x))"; + if (Solvers.Z3 != solverToUse()) { // The Z3 parser converts Booleans to Int if required. + assertThrows(IllegalArgumentException.class, () -> mgr.parse(query)); + } + } + + @Test + public void parseDeclareConflictBeforeQueryTest_IntBV() { + requireIntegers(); + requireBitvectors(); + @SuppressWarnings("unused") + IntegerFormula var = imgr.makeVariable("x"); + String query = "(declare-fun x () Int)(assert (= (_ bv20 8) x))"; assertThrows(IllegalArgumentException.class, () -> mgr.parse(query)); } From 8a2cddb9f95dcbf7c7748f79e5ba7d07119eff51 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 12 Oct 2024 21:00:58 +0200 Subject: [PATCH 15/63] fix paths for Windows-based CI. --- .appveyor.yml | 2 +- lib/native/x86_64-windows/README.md | 9 +++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/.appveyor.yml b/.appveyor.yml index bc2cb05461..470cf8fab1 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -34,7 +34,7 @@ build_script: # 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-z3\x64\*dll lib\native\x86_64-windows\ - copy lib\java\runtime-mathsat\*dll lib\native\x86_64-windows\ - copy lib\java\runtime-bitwuzla\*dll lib\native\x86_64-windows\ diff --git a/lib/native/x86_64-windows/README.md b/lib/native/x86_64-windows/README.md index ed625308c2..53b95450ca 100644 --- a/lib/native/x86_64-windows/README.md +++ b/lib/native/x86_64-windows/README.md @@ -28,8 +28,8 @@ Thus, we cannot check them into the repository. Please execute the following as in the current directory `lib/native/x86_64-windows`: For Z3: -- mklink libz3.dll ..\..\java\runtime-z3\libz3.dll -- mklink libz3java.dll ..\..\java\runtime-z3\libz3java.dll +- mklink libz3.dll ..\..\java\runtime-z3\x64\libz3.dll +- mklink libz3java.dll ..\..\java\runtime-z3\x64\libz3java.dll For MathSAT5: - mklink mpir.dll ..\..\java\runtime-mathsat\mpir.dll @@ -46,8 +46,8 @@ those files from the `lib\java\runtime-*\` directory into the current directory Please note that this copy process needs to be repeated after each update of a solver library via Ant/Ivy dependencies. For Z3: -- copy ..\..\java\runtime-z3\libz3.dll libz3.dll -- copy ..\..\java\runtime-z3\libz3java.dll libz3java.dll +- copy ..\..\java\runtime-z3\x64\libz3.dll libz3.dll +- copy ..\..\java\runtime-z3\x64\libz3java.dll libz3java.dll For MathSAT5: - copy ..\..\java\runtime-mathsat\mpir.dll mpir.dll @@ -59,6 +59,7 @@ For Bitwuzla: Or simply use a wildcard: - copy ..\..\java\runtime-*\*dll .\ +- copy ..\..\java\runtime-*\x64\*dll .\ ## Additional dependencies: From 32d5b71d6804f3dfffa3d909454d7f4b39ee940d Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 12 Oct 2024 21:03:42 +0200 Subject: [PATCH 16/63] Z3: update to v4.13.3 --- build/build-maven-publish.xml | 6 ++---- lib/ivy.xml | 2 +- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/build/build-maven-publish.xml b/build/build-maven-publish.xml index a0364726ff..050d92c337 100644 --- a/build/build-maven-publish.xml +++ b/build/build-maven-publish.xml @@ -162,12 +162,10 @@ SPDX-License-Identifier: Apache-2.0 - - + - + diff --git a/lib/ivy.xml b/lib/ivy.xml index a0747a13fd..6af2f9933e 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -161,7 +161,7 @@ SPDX-License-Identifier: Apache-2.0 - + From 9c6867f238ee471a6c0718420214c4b7574bc1e8 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 13 Oct 2024 09:42:31 +0200 Subject: [PATCH 17/63] exclude Z3 on some older Linux systems. --- .../test/SolverContextFactoryTest.java | 20 ++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java b/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java index 5d9523999a..0fdc1d2621 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java @@ -115,13 +115,16 @@ private void requireSupportedOperatingSystem() { } } - /** Some libraries require GLIBCXX in version 3.4.26 or newer. This excludes Ubuntu 18.04. */ + /** + * Some libraries require GLIBC in version 2.34 or GLIBCXX in version 3.4.26 or newer. This + * excludes Ubuntu 18.04 or 20.04 for some solvers. + */ private boolean isSufficientVersionOfLibcxx(String library) { try { NativeLibraries.loadLibrary(library); } catch (UnsatisfiedLinkError e) { - for (String version : new String[] {"3.4.26", "3.4.29"}) { - if (e.getMessage().contains("version `GLIBCXX_" + version + "' not found")) { + for (String dependency : getRequiredLibcxx(library)) { + if (e.getMessage().contains("version `" + dependency + "' not found")) { return false; } } @@ -129,6 +132,17 @@ private boolean isSufficientVersionOfLibcxx(String library) { return true; } + private String[] getRequiredLibcxx(String library) { + switch (library) { + case "z3": + return new String[] {"GLIBC_2.34", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "bitwuzlaj": + return new String[] {"GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + default: + return new String[] {}; + } + } + @Before public final void initSolver() throws InvalidConfigurationException { config = Configuration.builder().setOption("solver.solver", solverToUse().toString()).build(); From 316d99e339bc50e8e201383779ef263e17a0406a Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 13 Oct 2024 09:54:26 +0200 Subject: [PATCH 18/63] use platform-independent solver for simple test. --- src/org/sosy_lab/java_smt/test/example/BinoxxoTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/example/BinoxxoTest.java b/src/org/sosy_lab/java_smt/test/example/BinoxxoTest.java index 9a12b74195..a7d0714318 100644 --- a/src/org/sosy_lab/java_smt/test/example/BinoxxoTest.java +++ b/src/org/sosy_lab/java_smt/test/example/BinoxxoTest.java @@ -100,7 +100,7 @@ private void checkBinoxxo(String[] input, String[] expected) LogManager logger = BasicLogManager.create(config); ShutdownNotifier notifier = ShutdownNotifier.createDummy(); try (SolverContext context = - SolverContextFactory.createSolverContext(config, logger, notifier, Solvers.Z3)) { + SolverContextFactory.createSolverContext(config, logger, notifier, Solvers.SMTINTERPOL)) { BinoxxoSolver binoxxo = new BooleanBasedBinoxxoSolver(context); assertThat(binoxxo.solve(fromString(input))).isEqualTo(fromString(expected)); } From 4a40c32ffe5855287b9864e7bde6cdfe1401be82 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 13 Oct 2024 10:49:02 +0200 Subject: [PATCH 19/63] improve exception messages in concurrent tests, i.e. also print the stacktrace. --- .../java_smt/test/SolverConcurrencyTest.java | 25 ++++++++++++++++--- 1 file changed, 22 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java index 3f9e1da75a..f64f3024b1 100644 --- a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java @@ -12,7 +12,10 @@ import static com.google.common.truth.Truth.assertWithMessage; import static com.google.common.truth.TruthJUnit.assume; +import com.google.common.base.Joiner; import com.google.common.collect.ImmutableMap; +import java.io.PrintWriter; +import java.io.StringWriter; import java.math.BigInteger; import java.util.ArrayList; import java.util.Collections; @@ -27,6 +30,7 @@ import java.util.concurrent.LinkedBlockingQueue; import java.util.concurrent.TimeUnit; import java.util.concurrent.atomic.AtomicReferenceArray; +import java.util.stream.Collectors; import org.junit.Before; import org.junit.Test; import org.junit.runner.RunWith; @@ -728,9 +732,24 @@ private static void assertConcurrency(String testName, Run runnable) { } finally { threadPool.shutdownNow(); } - assertWithMessage("Test %s failed with exception(s): %s", testName, exceptionsList) - .that(exceptionsList.isEmpty()) - .isTrue(); + List exceptionDetails = + exceptionsList.stream() + .map( + ex -> { + StringWriter sw = new StringWriter(); + // CHECKSTYLE:OFF IllegalInstantiation + try (PrintWriter pw = new PrintWriter(sw)) { + // CHECKSTYLE:ON + ex.printStackTrace(pw); + } + return sw.toString(); + }) + .collect(Collectors.toList()); + assertWithMessage( + "Test %s failed with exception(s): %s", + testName, Joiner.on("\n").join(exceptionDetails)) + .that(exceptionsList) + .isEmpty(); } /** just a small lambda-compatible interface. */ From 95d3ab33744c76c77b9a1fd46241293b051394d2 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 13 Oct 2024 12:32:38 +0200 Subject: [PATCH 20/63] improve exception messages in concurrent tests, i.e. also print the stacktrace. --- src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java index f64f3024b1..4290a58040 100644 --- a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java @@ -737,11 +737,9 @@ private static void assertConcurrency(String testName, Run runnable) { .map( ex -> { StringWriter sw = new StringWriter(); - // CHECKSTYLE:OFF IllegalInstantiation - try (PrintWriter pw = new PrintWriter(sw)) { - // CHECKSTYLE:ON - ex.printStackTrace(pw); - } + @SuppressWarnings("checkstyle:IllegalInstantiation") + PrintWriter pw = new PrintWriter(sw); + ex.printStackTrace(pw); return sw.toString(); }) .collect(Collectors.toList()); From 07a40153a8aa5dcf4302da32959e796b9b868f8c Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 13 Oct 2024 19:23:31 +0200 Subject: [PATCH 21/63] update the image for Windows-based CI. This might fix problems with Z3 v4.13.2 and incompatible msvcp140.dll. See https://github.com/Z3Prover/z3/issues/7420 for details. This update is just a test. If it does not work, we will revert it. --- .appveyor.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.appveyor.yml b/.appveyor.yml index 470cf8fab1..78f61a22fa 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -8,7 +8,7 @@ version: build {build} {branch} -os: Visual Studio 2019 +os: Visual Studio 2022 clone_depth: 1 From 6f25eb34d37b6db230ae21cc4db8e53559171883 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 13 Oct 2024 20:23:12 +0200 Subject: [PATCH 22/63] update the image for Windows-based CI: use JDK 17. --- .appveyor.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.appveyor.yml b/.appveyor.yml index 78f61a22fa..a687189117 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -15,15 +15,15 @@ clone_depth: 1 install: - ps: | Add-Type -AssemblyName System.IO.Compression.FileSystem - if (!(Test-Path -Path "C:\ant\apache-ant-1.10.14" )) { + if (!(Test-Path -Path "C:\ant\apache-ant-1.10.15" )) { (new-object System.Net.WebClient).DownloadFile( - 'https://archive.apache.org/dist/ant/binaries/apache-ant-1.10.14-bin.zip', + 'https://archive.apache.org/dist/ant/binaries/apache-ant-1.10.15-bin.zip', 'C:\ant-bin.zip' ) [System.IO.Compression.ZipFile]::ExtractToDirectory("C:\ant-bin.zip", "C:\ant") } - - SET JAVA_HOME=C:\Program Files\Java\jdk14 - - SET PATH=C:\ant\apache-ant-1.10.14\bin;%JAVA_HOME%\bin;%PATH% + - SET JAVA_HOME=C:\Program Files\Java\jdk17 + - SET PATH=C:\ant\apache-ant-1.10.15\bin;%JAVA_HOME%\bin;%PATH% - SET IVY_CACHE_DIR=C:\ivy - echo %USERPROFILE% - echo %PATH% From 78f2adaef15ed0405e21fb14f20d6b75cfb4a8e4 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 13 Oct 2024 20:29:03 +0200 Subject: [PATCH 23/63] Revert "update the image for Windows-based CI. This might fix problems with Z3 v4.13.2 and incompatible msvcp140.dll." This reverts commit 07a40153a8aa5dcf4302da32959e796b9b868f8c. --- .appveyor.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.appveyor.yml b/.appveyor.yml index a687189117..6718320e88 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -8,7 +8,7 @@ version: build {build} {branch} -os: Visual Studio 2022 +os: Visual Studio 2019 clone_depth: 1 From a96931189df38cfe75ecf1f4660401252da997e9 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 13 Oct 2024 22:28:39 +0200 Subject: [PATCH 24/63] #380: add symlinks for Z3 for ARM64. --- lib/native/arm64-linux/libz3.so | 1 + lib/native/arm64-linux/libz3java.so | 1 + 2 files changed, 2 insertions(+) create mode 120000 lib/native/arm64-linux/libz3.so create mode 120000 lib/native/arm64-linux/libz3java.so diff --git a/lib/native/arm64-linux/libz3.so b/lib/native/arm64-linux/libz3.so new file mode 120000 index 0000000000..f02cc1bde5 --- /dev/null +++ b/lib/native/arm64-linux/libz3.so @@ -0,0 +1 @@ +../../java/runtime-z3/arm64/libz3.so \ No newline at end of file diff --git a/lib/native/arm64-linux/libz3java.so b/lib/native/arm64-linux/libz3java.so new file mode 120000 index 0000000000..f663467b7e --- /dev/null +++ b/lib/native/arm64-linux/libz3java.so @@ -0,0 +1 @@ +../../java/runtime-z3/arm64/libz3java.so \ No newline at end of file From e66261593a6aee21295bd7cd9df155ee52b69d41 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 13 Oct 2024 22:35:40 +0200 Subject: [PATCH 25/63] update sosy-lab-common to latest release 0.3000-609-g90a352c --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 6af2f9933e..e7c64e142c 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -84,7 +84,7 @@ SPDX-License-Identifier: Apache-2.0 - + From 086c4b9fe2cf8d3cbc0850753e3354a5b1f6abbb Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 13 Oct 2024 23:25:38 +0200 Subject: [PATCH 26/63] #380: extend JavaSMTs own ivy configuration to provide configurations for multiple architectures. We aim for backwards-compatibility and provide the x64-version as default for most public configurations. The solver-specific configuration "runtime-z3" does provide more than x64, and comes with arm64 included. --- build/build-maven-publish.xml | 4 ++-- lib/ivy.xml | 29 +++++++++++++++++++++-------- 2 files changed, 23 insertions(+), 10 deletions(-) diff --git a/build/build-maven-publish.xml b/build/build-maven-publish.xml index 050d92c337..d6845db5c8 100644 --- a/build/build-maven-publish.xml +++ b/build/build-maven-publish.xml @@ -145,8 +145,8 @@ SPDX-License-Identifier: Apache-2.0 - - + + diff --git a/lib/ivy.xml b/lib/ivy.xml index e7c64e142c..7f47e8dd9c 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -37,22 +37,34 @@ SPDX-License-Identifier: Apache-2.0 - + + + + + + + - + + - + + @@ -161,7 +173,8 @@ SPDX-License-Identifier: Apache-2.0 - + + From 598b0f9f8cad073540c772b5b813b3fcd38ccaa4 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 16 Oct 2024 22:17:49 +0200 Subject: [PATCH 27/63] cleanup Z3 build-script --- build/build-publish-solvers/solver-z3.xml | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/build/build-publish-solvers/solver-z3.xml b/build/build-publish-solvers/solver-z3.xml index 855f8c5813..0cf8d1644f 100644 --- a/build/build-publish-solvers/solver-z3.xml +++ b/build/build-publish-solvers/solver-z3.xml @@ -98,16 +98,6 @@ SPDX-License-Identifier: Apache-2.0 - - - - - From bd4ad9bb0e57a768b1686efbb04ef8febf0b0272 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 16 Oct 2024 22:17:49 +0200 Subject: [PATCH 28/63] update Dockerfile to compile solvers for arm64 architecture. --- docker/ubuntu2204.Dockerfile | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/docker/ubuntu2204.Dockerfile b/docker/ubuntu2204.Dockerfile index cdcf647a04..89bbc9dced 100644 --- a/docker/ubuntu2204.Dockerfile +++ b/docker/ubuntu2204.Dockerfile @@ -13,9 +13,9 @@ 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 +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 \ @@ -23,6 +23,8 @@ RUN apt-get update \ 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 From 7494d841938a9def9291e274f60e8f15f920691d Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 16 Oct 2024 22:17:49 +0200 Subject: [PATCH 29/63] MathSAT5: update/prepare build-scripts for several platforms, and update dependencies. - prepare for distinct architectures x64 and arm64 under Linux. - remove MPIR usage and replace it with GMP headers. MPIR is unmaintained since several years. - update GMP to v6.3.0 and JDK to v17 --- .../build-publish-solvers/solver-mathsat.xml | 107 ++++++++----- doc/Developers-How-to-Release-into-Ivy.md | 31 ++-- .../source/libmathsat5j/compileForLinux.sh | 148 ++++++++++++++++++ .../source/libmathsat5j/compileForWindows.sh | 69 ++++---- 4 files changed, 269 insertions(+), 86 deletions(-) create mode 100755 lib/native/source/libmathsat5j/compileForLinux.sh diff --git a/build/build-publish-solvers/solver-mathsat.xml b/build/build-publish-solvers/solver-mathsat.xml index cfabeb1b62..a507509adc 100644 --- a/build/build-publish-solvers/solver-mathsat.xml +++ b/build/build-publish-solvers/solver-mathsat.xml @@ -15,61 +15,86 @@ SPDX-License-Identifier: Apache-2.0 - - + + + + + + + + - - + + + + + + + + + + - - + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + Please specify the MathSAT5 version with the flag -Dmathsat.version=... . - - - - + + + + + + + + - + + + + + Lets copy the files for architecture x64 into main directory, for backwards compatibility. + Afterwards, please execute the SVN command from above. + + + + + + - Please specify the @{flag} version with the flag -Dmathsat.version=... . @@ -77,7 +102,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/doc/Developers-How-to-Release-into-Ivy.md b/doc/Developers-How-to-Release-into-Ivy.md index 3a85e192b4..553a5b1de1 100644 --- a/doc/Developers-How-to-Release-into-Ivy.md +++ b/doc/Developers-How-to-Release-into-Ivy.md @@ -205,33 +205,32 @@ but in the normal system environment, where some testing can be applied by the d We publish MathSAT for both Linux and Windows systems at once. The build process can fully be done on a Linux system. -We prefer to use the Docker container based on Ubuntu 18.04 for compiling the dependencies and assembling the libraries, -because GMP and MPIR might cause problems with newer versions of GCC and MinGW during compilation. +For publishing MathSAT, you need to use a Linux machine with at least GCC 7.5.0 and x86_64-w64-mingw32-gcc 7.3. +We prefer to use the Docker container based on Ubuntu 22.04 for compiling the dependencies and assembling the libraries. -For publishing MathSAT5, you need to use a Linux machine with at least GCC 7.5.0 and x86_64-w64-mingw32-gcc 7.3. 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 for Linux and MPIR/JDK for Windows) as described in the compilation scripts. +then provide the necessary dependencies (GMP for Linux and GMP/JDK for Windows) as described in the compilation scripts. (see `lib/native/source/libmathsat5j/`), and then execute the following command in the JavaSMT directory, where `$MATHSAT_PATH_LINUX` and `$MATHSAT_PATH_WINDOWS` are the paths to the MathSAT root directory, and `$MATHSAT_VERSION` is the version number of MathSAT (all-in-one, runtime: less than 5s): ``` ant publish-mathsat \ - -Dmathsat.path=$MATHSAT_PATH_LINUX \ - -Dgmp.path=$GMP_PATH \ - -Dmathsat-windows.path=$MATHSAT_PATH_WINDOWS \ - -Dmpir-windows.path=$MPIR_PATH \ - -Djdk-windows.path=$JDK_11_PATH \ + -Dmathsat-linux-x64.path=$MATHSAT_PATH_LINUX \ + -Dgmp-linux-x64.path=$GMP_PATH \ + -Dmathsat-windows-x64.path=$MATHSAT_PATH_WINDOWS \ + -Dgmp-windows-x64.path=$GMP_PATH_WINDOWS \ + -Djdk-windows-x64.path=$JDK_11_PATH \ -Dmathsat.version=$MATHSAT_VERSION ``` -Concrete example (`$WD` is a working directory where all dependencies are located): +Example: ``` ant publish-mathsat \ - -Dmathsat.path=$WD/mathsat-5.6.7-linux-x86_64-reentrant \ - -Dgmp.path=$WD/gmp-6.1.2 \ - -Dmathsat-windows.path=$WD/mathsat-5.6.7-win64-msvc \ - -Dmpir-windows.path=$WD/mpir-2.7.2-win \ - -Djdk-windows.path=$WD/jdk-11 \ - -Dmathsat.version=5.6.7 + -Dmathsat-linux-x64.path=/workspace/solvers/mathsat/mathsat-5.6.11-linux-x86_64-reentrant \ + -Dgmp-linux-x64.path=/workspace/solvers/gmp/gmp-6.3.0 \ + -Dmathsat-windows-x64.path=/workspace/solvers/mathsat/mathsat-5.6.11-win64-msvc \ + -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-windows \ + -Dmathsat.version=5.6.11 ``` Finally follow the instructions shown in the message at the end. diff --git a/lib/native/source/libmathsat5j/compileForLinux.sh b/lib/native/source/libmathsat5j/compileForLinux.sh new file mode 100755 index 0000000000..dee198d640 --- /dev/null +++ b/lib/native/source/libmathsat5j/compileForLinux.sh @@ -0,0 +1,148 @@ +#!/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: 2024 Dirk Beyer +# +# SPDX-License-Identifier: Apache-2.0 + +# ######################################### +# +# INFO: +# This script is automatically called from ant when publishing MathSAT5. +# There is no need to call this script manually, except for developing and debugging. +# +# ######################################### + +# This script builds libmathsat5j.so (bindings to mathsat5). +# 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 6.3.0 from http://gmplib.org/ and build GMP: +# For linux-x64: +# ./configure --enable-cxx --with-pic --disable-shared --enable-static --enable-fat +# make -j4 +# For linux-arm64: +# ./configure --enable-cxx --with-pic --disable-shared --enable-static --enable-fat \ +# --host=aarch64-linux-gnu \ +# CC=aarch64-linux-gnu-gcc CXX=aarch64-linux-gnu-g++ LD=aarch64-linux-gnu-ld +# make -j4 +# - For linux-arm64: Provide 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/java/GA/jdk17.0.2/dfd4a8d0985749f896bed50d7138ee7f/8/GPL/openjdk-17.0.2_linux-aarch64_bin.tar.gz). +# +# This script searches for all included libraries in the current directory first. +# You can use this to override specific libraries installed on your system. +# You can also use this to force static linking of a specific library, +# if you put only the corresponding .a file in this directory, not the .so file. +# For example, to statically link against libstdc++, +# compile this library with --with-pic, +# and put the resulting libstdc++.a file in this directory. + +# ######################################### +# Usage: ./compileForLinux.sh [] +# ARCH should be either 'linux-x64' or 'linux-arm64'. +# JNI_DIR is not required for 'linux-x64'. + +check_requirements() { + local file_path=$1 + local message=$2 + + if [ ! -f "$file_path" ]; then + echo "$message" + echo "Cannot find $file_path" + exit 1 + fi +} + +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} + +# Determine architecture and set variables accordingly +ARCH=$1 +if [ "$ARCH" == "linux-x64" ]; then + OUT_FILE="libmathsat5j-x64.so" + CC=gcc + STRIP=strip + JNI_HEADERS="$(../get_jni_headers.sh)" +elif [ "$ARCH" == "linux-arm64" ]; then + OUT_FILE="libmathsat5j-arm64.so" + CC=aarch64-linux-gnu-gcc + STRIP=aarch64-linux-gnu-strip + JNI_DIR="$4/include" + JNI_HEADERS="-I${JNI_DIR}/ -I${JNI_DIR}/linux/" +else + echo "Invalid architecture specified. Use 'linux-x64' or 'linux-arm64'." + exit 1 +fi + +MSAT_DIR="$2" +MSAT_SRC_DIR="$MSAT_DIR/include" +MSAT_LIB_DIR="$MSAT_DIR/lib" +MSAT_BIN_DIR="$MSAT_DIR/bin" + +GMP_DIR="$3" +GMP_LIB_DIR="$GMP_DIR/.libs" + +SRC_FILES="org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c" +OBJ_FILES="org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.o" + +check_requirements "$MSAT_LIB_DIR/libmathsat.a" "You need to specify the directory with the downloaded MathSAT5 on the command line!" +check_requirements "$GMP_LIB_DIR/libgmp.a" "You need to specify the directory with the downloaded and compiled GMP on the command line!" +if [ "$ARCH" == "linux-arm64" ]; then # on linux-x64, we use the installed default JDK + check_requirements "$JNI_DIR/jni.h" "You need to specify the directory with the downloaded JNI headers on the command line!" +fi + +rm "$OBJ_FILES" + +echo "Compiling the C wrapper code and creating the \"$OUT_FILE\" library..." + +# This will compile the JNI wrapper part, given the JNI and the MathSAT5 header files +$CC -g -std=gnu99 -Wall -Wextra -Wpedantic -Wno-return-type -Wno-unused-parameter \ + $JNI_HEADERS -I$MSAT_SRC_DIR -I$GMP_DIR $SRC_FILES -fPIC -c + +echo "Compilation Done" +echo "Linking libraries together into one file..." + +# This will link together the file produced above, the MathSAT5 library, the GMP library and the standard libraries. +# Everything except the standard libraries is included statically. +# The result is a single shared library containing all necessary components. +$CC -Wall -g -o ${OUT_FILE} -shared -Wl,-soname,${OUT_FILE} \ + -L. -L${MSAT_LIB_DIR} -L${GMP_LIB_DIR} -I${GMP_DIR} ${OBJ_FILES} \ + -Wl,-Bstatic -lmathsat -lgmpxx -lgmp -static-libstdc++ -lstdc++ \ + -Wl,-Bdynamic -lc -lm + +if [ $? -ne 0 ]; then + echo "There was a problem during compilation of \"$SRC_FILES\"" + 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)" +echo "Missing symbols: '$MISSING_SYMBOLS'" +if [ ! -z "$MISSING_SYMBOLS" ]; then + echo "Warning: There are the following unresolved dependencies in libmathsat5j.so:" + echo "Missing symbols: '$MISSING_SYMBOLS'" + readelf -Ws ${OUT_FILE} | grep NOTYPE | grep GLOBAL | grep UND + exit 1 +fi + +echo "All Done" + +echo "Please check the following dependencies that will be required at runtime by ${OUT_FILE}:" +LANG=C objdump -p ${OUT_FILE} | grep -A50 "required from" diff --git a/lib/native/source/libmathsat5j/compileForWindows.sh b/lib/native/source/libmathsat5j/compileForWindows.sh index 53e38525ad..d499b4317b 100755 --- a/lib/native/source/libmathsat5j/compileForWindows.sh +++ b/lib/native/source/libmathsat5j/compileForWindows.sh @@ -4,14 +4,14 @@ # an API wrapper for a collection of SMT solvers: # https://github.com/sosy-lab/java-smt # -# SPDX-FileCopyrightText: 2020 Dirk Beyer +# SPDX-FileCopyrightText: 2024 Dirk Beyer # # SPDX-License-Identifier: Apache-2.0 # ######################################### # # INFO: -# This script is automatically called from ant when publishing MathSAT5 or OptiMathSAT. +# This script is automatically called from ant when publishing MathSAT5. # There is no need to call this scripts manually, except for developing and debugging. # # ######################################### @@ -21,15 +21,28 @@ # - 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 +# Since 2017, MPIR is no longer developed. We use the precompiled `mpir.dll` from the MathSAT5 archive. +# 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 +# ./configure --enable-cxx --with-pic --enable-shared --disable-static --enable-fat --host=x86_64-w64-mingw32 +# make -j4 # - 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). +# (e.g., https://download.java.net/java/GA/jdk17.0.2/dfd4a8d0985749f896bed50d7138ee7f/8/GPL/openjdk-17.0.2_windows-x64_bin.zip). # -# To build mathsat bindings: ./compileForWindows.sh $MATHSAT_DIR $MPIR_DIR $JNI_DIR +# To build MathSAT5 bindings: ./compileForWindows-x64.sh $MATHSAT_DIR $GMP_DIR $JNI_DIR + +check_requirements() { + local file_path=$1 + local message=$2 + + if [ ! -f "$file_path" ]; then + echo "$message" + echo "Cannot find $file_path" + exit 1 + fi +} set -e @@ -43,6 +56,11 @@ DIR="$( cd -P "$( dirname "$SOURCE" )" && pwd )" cd ${DIR} +OUT_FILE="mathsat5j.dll" + +CC=x86_64-w64-mingw32-gcc +STRIP=strip + JNI_DIR="$3"/include JNI_HEADERS="-I${JNI_DIR}/ -I${JNI_DIR}/win32/" @@ -50,38 +68,31 @@ MSAT_SRC_DIR="$1"/include MSAT_LIB_DIR="$1"/lib MSAT_BIN_DIR="$1"/bin -MPIR_HEADER_DIR="$2" -MPIR_LIB_DIR="$2"/.libs -MPIR_INCLUDE_DIR="$2" +GMP_DIR="$2" +GMP_LIB_DIR="$2/.libs" SRC_FILES="org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.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 MathSAT5 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 +check_requirements "$MSAT_LIB_DIR/mathsat.dll" "You need to specify the directory with the downloaded MathSAT5 on the command line!" +check_requirements "$JNI_DIR/jni.h" "You need to specify the directory with the downloaded JNI headers on the command line!" +check_requirements "$GMP_DIR/gmp.h" "You need to specify the directory with the downloaded GMP on the command line!" -OUT_FILE="mathsat5j.dll" +rm "$OBJ_FILES" 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 -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 $SRC_FILES \ - -lmathsat $MSAT_BIN_DIR/mpir.dll -lstdc++ -lpsapi 2>&1 +# This will compile the JNI wrapper part, given the JNI and the MathSAT5 header files +$CC -g -std=gnu99 -Wall -Wextra -Wpedantic -Wno-return-type -Wno-unused-parameter \ + -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 echo "Compilation Done" echo "Reducing file size by dropping unused symbols..." -strip ${OUT_FILE} +$STRIP ${OUT_FILE} echo "Reduction Done" echo "All Done" From a27dd389f7efcedc1cf06e6b13df4901676faacc Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 16 Oct 2024 22:17:50 +0200 Subject: [PATCH 30/63] MathSAT: update build documentation --- doc/Developers-How-to-Release-into-Ivy.md | 55 +++++++++++++---------- 1 file changed, 31 insertions(+), 24 deletions(-) diff --git a/doc/Developers-How-to-Release-into-Ivy.md b/doc/Developers-How-to-Release-into-Ivy.md index 553a5b1de1..6ff1817d6c 100644 --- a/doc/Developers-How-to-Release-into-Ivy.md +++ b/doc/Developers-How-to-Release-into-Ivy.md @@ -203,36 +203,43 @@ but in the normal system environment, where some testing can be applied by the d ### Publishing (Opti)-MathSAT5 -We publish MathSAT for both Linux and Windows systems at once. -The build process can fully be done on a Linux system. -For publishing MathSAT, you need to use a Linux machine with at least GCC 7.5.0 and x86_64-w64-mingw32-gcc 7.3. +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 for compiling the dependencies and assembling the libraries. -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 for Linux and GMP/JDK for Windows) as described in the compilation scripts. -(see `lib/native/source/libmathsat5j/`), and then execute the following command in the JavaSMT directory, -where `$MATHSAT_PATH_LINUX` and `$MATHSAT_PATH_WINDOWS` are the paths to the MathSAT root directory, -and `$MATHSAT_VERSION` is the version number of MathSAT (all-in-one, runtime: less than 5s): -``` - ant publish-mathsat \ - -Dmathsat-linux-x64.path=$MATHSAT_PATH_LINUX \ - -Dgmp-linux-x64.path=$GMP_PATH \ - -Dmathsat-windows-x64.path=$MATHSAT_PATH_WINDOWS \ - -Dgmp-windows-x64.path=$GMP_PATH_WINDOWS \ - -Djdk-windows-x64.path=$JDK_11_PATH \ - -Dmathsat.version=$MATHSAT_VERSION +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)) +as described in the compilation scripts (see `lib/native/source/libmathsat5j/compileFor.sh`). +Then execute the following command in the JavaSMT directory, +where `$MATHSAT_PATH_` is the paths to the corresponding MathSAT root directory, +and `$MATHSAT_VERSION` is the version number of MathSAT (all-in-one command, runtime is about 10s): +``` +ant publish-mathsat \ + -Dmathsat-linux-x64.path=$MATHSAT_PATH_LINUX_X64 \ + -Dgmp-linux-x64.path=$GMP_PATH_LINUX_X64 \ + -Dmathsat-windows-x64.path=$MATHSAT_PATH_WINDOWS_X64 \ + -Dgmp-windows-x64.path=$GMP_PATH_WINDOWS_X64 \ + -Djdk-windows-x64.path=$JDK_PATH_WINDOWS_X64 \ + -Dmathsat-linux-arm64.path=$MATHSAT_PATH_LINUX_ARM64 \ + -Dgmp-linux-arm64.path=$GMP_PATH_LINUX_ARM64 \ + -Djdk-linux-arm64.path=$JDK_PATH_LINUX_ARM64 \ + -Dmathsat.version=$MATHSAT_VERSION ``` Example: ``` - ant publish-mathsat \ - -Dmathsat-linux-x64.path=/workspace/solvers/mathsat/mathsat-5.6.11-linux-x86_64-reentrant \ - -Dgmp-linux-x64.path=/workspace/solvers/gmp/gmp-6.3.0 \ - -Dmathsat-windows-x64.path=/workspace/solvers/mathsat/mathsat-5.6.11-win64-msvc \ - -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-windows \ - -Dmathsat.version=5.6.11 +ant publish-mathsat \ + -Dmathsat-linux-x64.path=/workspace/solvers/mathsat/mathsat-5.6.11-linux-x86_64-reentrant \ + -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 \ + -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 \ + -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 ``` -Finally follow the instructions shown in the message at the end. +Finally, follow the instructions shown in the message at the end. A similar procedure applies to [OptiMathSAT](http://optimathsat.disi.unitn.it/) solver, except that Windows is not yet supported and the publishing command is simpler: From 08143b73261cb48c3d4fa508a92501787eaba103 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 16 Oct 2024 22:17:50 +0200 Subject: [PATCH 31/63] MathSAT5: update Ivy configuration for x64 and arm64 --- build/build-maven-publish.xml | 13 ++++++++----- lib/ivy.xml | 11 +++++++---- solvers_ivy_conf/ivy_mathsat.xml | 30 +++++++++++++++++++++--------- 3 files changed, 36 insertions(+), 18 deletions(-) diff --git a/build/build-maven-publish.xml b/build/build-maven-publish.xml index d6845db5c8..07fa2f7bc0 100644 --- a/build/build-maven-publish.xml +++ b/build/build-maven-publish.xml @@ -124,19 +124,22 @@ SPDX-License-Identifier: Apache-2.0 - + + - - - - + + + + + - + + + @@ -60,10 +62,10 @@ SPDX-License-Identifier: Apache-2.0 @@ -172,7 +174,8 @@ SPDX-License-Identifier: Apache-2.0 - + + diff --git a/solvers_ivy_conf/ivy_mathsat.xml b/solvers_ivy_conf/ivy_mathsat.xml index 9040966f50..d9a8022f59 100644 --- a/solvers_ivy_conf/ivy_mathsat.xml +++ b/solvers_ivy_conf/ivy_mathsat.xml @@ -22,18 +22,30 @@ SPDX-License-Identifier: Apache-2.0 - - - + + + + + + + + + + + - - - - - - + + + + + + + + + + From 8302e03a08b7e0c351c38b859a47aef8041feb77 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 16 Oct 2024 22:17:50 +0200 Subject: [PATCH 32/63] MathSAT5: add symlinks to architecture-dependent libraries. This reverts commit 07a40153a8aa5dcf4302da32959e796b9b868f8c. --- lib/native/arm64-linux/libmathsat5j.so | 1 + lib/native/x86_64-linux/libmathsat5j.so | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) create mode 120000 lib/native/arm64-linux/libmathsat5j.so diff --git a/lib/native/arm64-linux/libmathsat5j.so b/lib/native/arm64-linux/libmathsat5j.so new file mode 120000 index 0000000000..c2e11cc1a1 --- /dev/null +++ b/lib/native/arm64-linux/libmathsat5j.so @@ -0,0 +1 @@ +../../java/runtime-mathsat/arm64/libmathsat5j.so \ No newline at end of file diff --git a/lib/native/x86_64-linux/libmathsat5j.so b/lib/native/x86_64-linux/libmathsat5j.so index 7d9bdac573..528927fe06 120000 --- a/lib/native/x86_64-linux/libmathsat5j.so +++ b/lib/native/x86_64-linux/libmathsat5j.so @@ -1 +1 @@ -../../java/runtime-mathsat/libmathsat5j.so \ No newline at end of file +../../java/runtime-mathsat/x64/libmathsat5j.so \ No newline at end of file From 2dbefcd1983ea93c7918a1fa14bd612f52b95c07 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 16 Oct 2024 22:26:28 +0200 Subject: [PATCH 33/63] fix cleanup script, if temporary build-directories are missing. --- build.xml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/build.xml b/build.xml index 6915258559..850efbc87c 100644 --- a/build.xml +++ b/build.xml @@ -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 +SPDX-FileCopyrightText: 2024 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> @@ -79,11 +79,11 @@ SPDX-License-Identifier: Apache-2.0 - + + + - - - + From 141f60670f19e8ca50e6b3e93b92f7cc62129923 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 16 Oct 2024 22:45:12 +0200 Subject: [PATCH 34/63] exclude MathSAT5 on some older Linux systems. --- src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java b/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java index 0fdc1d2621..fc20f1e30a 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java @@ -103,6 +103,9 @@ private void requireSupportedOperatingSystem() { return; case MATHSAT5: assume.that(IS_LINUX || IS_WINDOWS).isTrue(); + if (IS_LINUX) { + assume.that(isSufficientVersionOfLibcxx("mathsat5j")).isTrue(); + } return; case Z3: assume.that(IS_LINUX || IS_WINDOWS || IS_MAC).isTrue(); @@ -138,6 +141,8 @@ private String[] getRequiredLibcxx(String library) { return new String[] {"GLIBC_2.34", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; case "bitwuzlaj": return new String[] {"GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "mathsat5j": + return new String[] {"GLIBC_2.33"}; default: return new String[] {}; } From e4cbf365e34ef0c3f4080cb43275f915bcf9521e Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 19 Oct 2024 19:17:01 +0200 Subject: [PATCH 35/63] MathSAT5: simplify Ivy dependencies. --- lib/ivy.xml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 03dac1ffd9..926223b9e7 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -174,10 +174,8 @@ SPDX-License-Identifier: Apache-2.0 - - - - + + From 655d3608449ab4d64d31f8a222e8f789b54bfd12 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 19 Oct 2024 19:18:59 +0200 Subject: [PATCH 36/63] Update Readme and user guide. --- README.md | 36 +++++++++++++++---------------- doc/Getting-started.md | 49 ++++++++++++++++++++++++++++++++---------- 2 files changed, 56 insertions(+), 29 deletions(-) diff --git a/README.md b/README.md index 36e92128ef..1b1cb8d84a 100644 --- a/README.md +++ b/README.md @@ -54,21 +54,21 @@ JavaSMT can express formulas in the following theories: The concrete support for a certain theory depends on the underlying SMT solver. Only a few SMT solvers provide support for theories like Arrays, Floating Point, String or RegEx. -Currently JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started.md) for installation): - -| SMT Solver | Linux | Windows | MacOS | Description | -| --- |:---:|:---:|:---:|:--- | -| [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark: | :heavy_check_mark: | | a fast solver for bitvector logic | -| [Boolector](https://boolector.github.io/) | :heavy_check_mark: | | | a fast solver for bitvector logic, misses formula introspection, deprecated | -| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | | | | -| [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | | | | -| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: | :heavy_check_mark: | | | -| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark: | | | | -| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | | | based on MathSAT5, with support for optimization queries | -| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver | -| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver | -| [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: | [maybe](https://github.com/sosy-lab/java-smt/pull/215) | | | -| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | mature and well-known solver | +JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started.md) for installation): + +| SMT Solver | Linux x64 | Linux arm64 | Windows x64 | Windows arm64 | MacOS x64 | MacOS arm64 | Description | +| --- |:---:|:---:|:---:|:---:|:---:|:---:|:--- | +| [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark: | | :heavy_check_mark: | | | | a fast solver for bitvector logic | +| [Boolector](https://boolector.github.io/) | :heavy_check_mark: | | | | | | a fast solver for bitvector logic, misses formula introspection, deprecated | +| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | | | | | | | +| [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | | | | | | | +| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | | | | | +| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark: | | | | | | | +| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | | | | | | based on MathSAT5, with support for optimization queries | +| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver | +| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver | +| [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: | | [maybe](https://github.com/sosy-lab/java-smt/pull/215) | | | | | +| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | mature and well-known solver | #### Operating System and Architecture Support We support a reasonable list of operating systems and versions. @@ -76,7 +76,7 @@ Our main target is Linux (64-bit, mainly Ubuntu 22.04 or newer, several solver libraries also work on Ubuntu 18.04, or comparable Linux distributions). Windows 10/11 and MacOS are supported for several SMT solvers. Our main development architecture is x64 (x86-64). -We also provide some solvers for ARM64 (AArch64 for ARMv8-A), e.g., Java-based SMT solvers and Z3. +We also provide some solvers for ARM64 (AArch64 for ARMv8-A), e.g., Java-based SMT solvers, Z3, and MathSAT. If a specific operating system or architecture is missing and required, please do not hesitate and open an issue! @@ -102,9 +102,9 @@ If something specific is missing, please [look for or file an issue](https://git | [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark: | | | [Boolector](https://boolector.github.io/) | :heavy_check_mark: | | | [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | :heavy_check_mark: | -| [CVC5](https://cvc4.github.io/) | :question: | | +| [CVC5](https://cvc4.github.io/) | :question: | | | [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: | | -| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :question: | | +| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :question: | | | [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | | | [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | | | [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | | diff --git a/doc/Getting-started.md b/doc/Getting-started.md index 9ec2dce256..1d7ec954ed 100644 --- a/doc/Getting-started.md +++ b/doc/Getting-started.md @@ -22,7 +22,34 @@ which would automatically fetch `JavaSMT` and all of its dependencies. After the repository URL is configured, you only need to add the following dependency: ```xml - + +``` + +#### Architecture specification + +JavaSMT includes native binaries for several SMT solvers and only installs for x64 architecture, by default. +Starting with version 5.0.?, JavaSMT also supports additional architectures, such as x64 and arm64. +For a full list of supported solvers and architectures, refer to the [Readme](../README.md). +You can configure and download dependencies for specific architectures, or even multiple architectures in parallel. +To specify an architecture, the Ivy configuration must recognize the `arch` attribute. +An example Ivy configuration for this setup can be found in the [Ivy settings](../build/ivysettings.xml) of JavaSMT. + +Afterwards, you can use JavaSMT for other architectures with: + +```xml + +``` + +or + +```xml + +``` + +Or specify a specific architecture for a solver directly: + +```xml + ``` ### Automatic Installation from Maven Central (possibly outdated) @@ -36,7 +63,7 @@ For Maven: org.sosy-lab java-smt - 3.7.0-61-gea80187e + 5.0.0-61-gea80187e ``` @@ -123,15 +150,15 @@ In order to perform the manual installation, the following steps should be follo Latest version can be found by looking at the [Ivy index](https://www.sosy-lab.org/ivy/org.sosy_lab/java-smt/). **JavaSMT might not yet support the latest version on the solver's webpage, but only the latest version in the [Ivy index](https://www.sosy-lab.org/ivy/org.sosy_lab/java-smt/).** - - Suppose the version `3.7.0` was chosen. - Ivy description file [`ivy-3.7.0.xml`](https://www.sosy-lab.org/ivy/org.sosy_lab/java-smt/ivy-3.7.0.xml) can + - Suppose the version `5.0.0` was chosen. + Ivy description file [`ivy-5.0.0.xml`](https://www.sosy-lab.org/ivy/org.sosy_lab/java-smt/ivy-5.0.0.xml) can be consulted in order to determine all the files which should be fetched. - The artifacts tag specifies what files the release depends on. - In the example case, those are `java-smt-3.7.0.jar` and (optionally) - `java-smt-3.7.0-sources.jar`, located in the same directory. + In the example case, those are `java-smt-5.0.0.jar` and (optionally) + `java-smt-5.0.0-sources.jar`, located in the same directory. - Finally, the dependencies can be manually followed and resolved. - E.g. in the example, Z3 version `4.8.9-sosy0` is specified, - which is described by the corresponding [XML](https://www.sosy-lab.org/ivy/org.sosy_lab/javasmt-solver-z3/ivy-4.8.9-sosy0.xml) + E.g. in the example, Z3 version `4.13.3` is specified, + which is described by the corresponding [XML](https://www.sosy-lab.org/ivy/org.sosy_lab/javasmt-solver-z3/ivy-4.13.3.xml) file, specifying what binaries should be fetched from the corresponding [directory](https://www.sosy-lab.org/ivy/org.sosy_lab/javasmt-solver-z3/). @@ -140,7 +167,7 @@ In order to perform the manual installation, the following steps should be follo When using Ivy or Maven for installation on a 64-bit Linux platform, solver binaries for native solvers are downloaded automatically, if available. -Some solvers are also available for supporting Windows or MacOS. +The [Readme](../README.md) contains a list of solvers and supported platforms. Everything should work as is after installation. Without Ivy or Maven you need to download and install the binaries manually as described above under [Manual Installation](#manual-installation). @@ -148,8 +175,8 @@ You can either copy them into the directory of the JavaSMT JAR file, or in a directory `../native/-/` relative to the directory of the JAR file. See [NativeLibraries][] documentation for more details on which path is searched. -For systems other than 64-bit Linux (e.g., Windows, MacOS, or 32-bit systems) we might not always provide binaries, -so you need to download or compile them for yourself. +We might not provide binaries for some platforms, +so you need to download or compile them for yourself, if supported by the SMT solver. You can find the necessary steps for compiling and using solver binaries in [`lib/native/source/`](../lib/native/source/) and [`build`](../build). Solvers which run directly on JDK (currently Princess and SMTInterpol) do not require any configuration and work out of the box. From ec1766dd9ad9884549a40810e5b16c7bc9824c4a Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 19 Oct 2024 21:10:15 +0200 Subject: [PATCH 37/63] MathSAT5: fix publication script. --- build/build-maven-publish.xml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/build/build-maven-publish.xml b/build/build-maven-publish.xml index 07fa2f7bc0..fe1fdc3d2a 100644 --- a/build/build-maven-publish.xml +++ b/build/build-maven-publish.xml @@ -127,11 +127,11 @@ SPDX-License-Identifier: Apache-2.0 - + - - + + From 24bcd6f24265693489b1656785e9d1f5db273d4d Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 20 Oct 2024 09:21:18 +0200 Subject: [PATCH 38/63] MathSAT: avoid using MathSAT on CI when GLIBC_2.33 is not available. Instead, we use a plain Java-based solver as reference. --- src/org/sosy_lab/java_smt/test/DebugModeTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/DebugModeTest.java b/src/org/sosy_lab/java_smt/test/DebugModeTest.java index 0f88c9cab3..8d5d60af22 100644 --- a/src/org/sosy_lab/java_smt/test/DebugModeTest.java +++ b/src/org/sosy_lab/java_smt/test/DebugModeTest.java @@ -199,7 +199,7 @@ public void noSharedDeclarationsTest() throws InvalidConfigurationException { public void noSharingBetweenSolversTest() throws InvalidConfigurationException, InterruptedException, SolverException { Solvers otherSolver = - solverToUse() == Solvers.SMTINTERPOL ? Solvers.MATHSAT5 : Solvers.SMTINTERPOL; + solverToUse() == Solvers.SMTINTERPOL ? Solvers.PRINCESS : Solvers.SMTINTERPOL; try (SolverContext otherContext = debugFactory.generateContext(otherSolver)) { BooleanFormulaManager otherBmgr = otherContext.getFormulaManager().getBooleanFormulaManager(); From 30d9d6900f66e6a87fcdcf63a4153b053c37f300 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 20 Oct 2024 13:12:50 +0200 Subject: [PATCH 39/63] update the Ubuntu18.04 Docker image for cross-architecture builds. --- docker/ubuntu1804.Dockerfile | 47 ++++++++++++++++++++++++------------ 1 file changed, 31 insertions(+), 16 deletions(-) diff --git a/docker/ubuntu1804.Dockerfile b/docker/ubuntu1804.Dockerfile index d3353e33d4..588a117fbc 100644 --- a/docker/ubuntu1804.Dockerfile +++ b/docker/ubuntu1804.Dockerfile @@ -2,29 +2,42 @@ # an API wrapper for a collection of SMT solvers: # https://github.com/sosy-lab/java-smt # -# SPDX-FileCopyrightText: 2021 Dirk Beyer +# SPDX-FileCopyrightText: 2024 Dirk Beyer # # SPDX-License-Identifier: Apache-2.0 -FROM ubuntu:bionic +FROM ubuntu:18.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 \ + wget curl git build-essential cmake patchelf unzip \ openjdk-11-jdk ant maven \ - mingw-w64 zlib1g-dev m4 + gcc-aarch64-linux-gnu g++-aarch64-linux-gnu \ + binutils-aarch64-linux-gnu libc6-dev-arm64-cross \ + mingw-w64 zlib1g-dev m4 \ + && apt-get clean # Yices2 requires some dependencies -RUN apt-get update \ +RUN apt-get update \ && apt-get install -y \ - autoconf gperf + autoconf gperf \ + && apt-get clean # CVC5 requires some dependencies RUN apt-get update \ && apt-get install -y \ python3 python3-toml python3-pyparsing flex libssl-dev \ + && apt-get clean \ && wget https://github.com/Kitware/CMake/releases/download/v3.26.3/cmake-3.26.3.tar.gz \ && tar -zxvf cmake-3.26.3.tar.gz \ && cd cmake-3.26.3 \ @@ -32,13 +45,13 @@ RUN apt-get update \ && make \ && make install -# set default locale +# 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 \ - locales locales-all -ENV LC_ALL en_US.UTF-8 -ENV LANG en_US.UTF-8 -ENV LANGUAGE en_US.UTF-8 + ninja-build python3-pip \ + && apt-get clean +RUN pip3 install --upgrade meson # OpenSMT requires swig, gmp, flex and bison # - swig needs to built manually to get version 4.1 for unique_ptr support @@ -47,10 +60,9 @@ ENV LANGUAGE en_US.UTF-8 # - lzip is required to unpack the gmp tar ball RUN apt-get update \ && apt-get install -y \ - flex \ - bison \ - libpcre2-dev \ - lzip + flex bison libpcre2-dev lzip \ + && apt-get clean + WORKDIR /dependencies RUN wget http://prdownloads.sourceforge.net/swig/swig-4.1.1.tar.gz \ && tar xf swig-4.1.1.tar.gz \ @@ -58,13 +70,16 @@ RUN wget http://prdownloads.sourceforge.net/swig/swig-4.1.1.tar.gz \ && ./configure \ && make -j4 \ && make install \ + && rm -rf swig-4.1.1.tar.gz swig-4.1.1 \ && cd -- + RUN wget https://gmplib.org/download/gmp/gmp-6.2.1.tar.lz \ && tar xf gmp-6.2.1.tar.lz \ && cd gmp-6.2.1 \ && ./configure --enable-cxx --with-pic --disable-shared --enable-fat \ && make -j4 \ && make install \ + && rm -rf gmp-6.2.1.tar.lz gmp-6.2.1 \ && cd -- # Add the user "developer" with UID:1000, GID:1000, home at /developer. From 696f7b8ada2fa7de2393cb63f78066d9244bc331 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 20 Oct 2024 15:17:19 +0200 Subject: [PATCH 40/63] MathSAT5: provide a dependency that works on older Ubuntu, such as 18.04 and 20.04, using only GLIBC_2.27. --- doc/Developers-How-to-Release-into-Ivy.md | 3 ++- lib/ivy.xml | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/doc/Developers-How-to-Release-into-Ivy.md b/doc/Developers-How-to-Release-into-Ivy.md index 6ff1817d6c..8779165610 100644 --- a/doc/Developers-How-to-Release-into-Ivy.md +++ b/doc/Developers-How-to-Release-into-Ivy.md @@ -206,7 +206,8 @@ 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 for compiling the dependencies and assembling the libraries. +We prefer to use the Docker container based on Ubuntu 22.04 (better use Ubuntu 18.04 for older GLIBC!) +for compiling the dependencies and assembling the libraries. 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)) diff --git a/lib/ivy.xml b/lib/ivy.xml index 926223b9e7..75b3c74b20 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -174,7 +174,7 @@ SPDX-License-Identifier: Apache-2.0 - + From 7f19ecc10e1b90377d7f818965c15e30b9b629e2 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 27 Oct 2024 12:51:38 +0100 Subject: [PATCH 41/63] Bitwuzla: extend build-steps for Linux with x64-flag --- .../build-publish-solvers/solver-bitwuzla.xml | 42 +++++++++---------- 1 file changed, 21 insertions(+), 21 deletions(-) diff --git a/build/build-publish-solvers/solver-bitwuzla.xml b/build/build-publish-solvers/solver-bitwuzla.xml index 0ae203cb31..42e24c5603 100644 --- a/build/build-publish-solvers/solver-bitwuzla.xml +++ b/build/build-publish-solvers/solver-bitwuzla.xml @@ -13,7 +13,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -59,18 +59,18 @@ SPDX-License-Identifier: Apache-2.0 - + - + - @@ -87,7 +87,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -118,8 +118,8 @@ SPDX-License-Identifier: Apache-2.0 - + depends="compile-bitwuzla-linux-x64, compile-bitwuzla-windows"> + This ant-step uses the Linux dependencies for building the SWIG-wrapper. The Windows dependencies are identical and would also work. @@ -132,7 +132,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -155,8 +155,8 @@ SPDX-License-Identifier: Apache-2.0 - + depends="compile-bitwuzla-linux-x64, compile-bitwuzla-windows, build-wrapper"> + @@ -172,7 +172,7 @@ SPDX-License-Identifier: Apache-2.0 - @@ -180,7 +180,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -199,12 +199,12 @@ SPDX-License-Identifier: Apache-2.0 - - - - - - + + + + + + @@ -264,8 +264,8 @@ SPDX-License-Identifier: Apache-2.0 - + From e648ac15f4b466d64add12806fa7fa466be83bed Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 28 Oct 2024 15:47:34 +0100 Subject: [PATCH 42/63] Bitwuzla: prepare for arm64-build. --- build/build-maven-publish.xml | 5 +- .../build-publish-solvers/solver-bitwuzla.xml | 144 +++++++++++++++--- doc/Developers-How-to-Release-into-Ivy.md | 24 ++- solvers_ivy_conf/ivy_bitwuzla.xml | 24 ++- 4 files changed, 158 insertions(+), 39 deletions(-) diff --git a/build/build-maven-publish.xml b/build/build-maven-publish.xml index fe1fdc3d2a..e301b06e69 100644 --- a/build/build-maven-publish.xml +++ b/build/build-maven-publish.xml @@ -179,11 +179,14 @@ SPDX-License-Identifier: Apache-2.0 + + - + + diff --git a/build/build-publish-solvers/solver-bitwuzla.xml b/build/build-publish-solvers/solver-bitwuzla.xml index 42e24c5603..f69a91eac6 100644 --- a/build/build-publish-solvers/solver-bitwuzla.xml +++ b/build/build-publish-solvers/solver-bitwuzla.xml @@ -14,7 +14,8 @@ SPDX-License-Identifier: Apache-2.0 - + + @@ -34,7 +35,8 @@ SPDX-License-Identifier: Apache-2.0 - + + Please specify a custom revision with the flag -Dbitwuzla.customRev=XXX. The custom revision should be a version number of Bitwuzla. @@ -60,10 +62,12 @@ SPDX-License-Identifier: Apache-2.0 - + + + @@ -73,7 +77,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -92,7 +96,30 @@ SPDX-License-Identifier: Apache-2.0 - + + + + + + + + + + + + + + + + + + + + + + @@ -118,10 +145,11 @@ SPDX-License-Identifier: Apache-2.0 + depends="compile-bitwuzla-linux-x64"> - This ant-step uses the Linux dependencies for building the SWIG-wrapper. - The Windows dependencies are identical and would also work. + This ant-step uses the Linux x64 dependencies for building the SWIG-wrapper. + Any other dependencies, e.g., Windows or Linux for other platforms, are identical + and would also work. However, the Linux x64 path is hardcoded here. @@ -132,7 +160,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -154,8 +182,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -185,7 +212,7 @@ SPDX-License-Identifier: Apache-2.0 - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - @@ -220,11 +293,11 @@ SPDX-License-Identifier: Apache-2.0 - - + + - + - - + + + + + + + Lets copy the files for architecture x64 into main directory, for backwards compatibility. + Afterwards, please execute the SVN command from above. + + + + + + \ No newline at end of file diff --git a/doc/Developers-How-to-Release-into-Ivy.md b/doc/Developers-How-to-Release-into-Ivy.md index 8779165610..eddf27c67b 100644 --- a/doc/Developers-How-to-Release-into-Ivy.md +++ b/doc/Developers-How-to-Release-into-Ivy.md @@ -183,18 +183,26 @@ To publish Bitwuzla, checkout the [Bitwuzla repository](https://github.com/bitwu Then execute the following command in the JavaSMT directory: ``` ant publish-bitwuzla \ - -Dbitwuzla.path=$BITWUZLA_DIR -Dbitwuzla.customRev=$VERSION \ - -Dbitwuzla.rebuildWrapper=$BOOL -Djdk-windows.path=$JNI_DIR + -Dbitwuzla.path=$BITWUZLA_DIR \ + -Dbitwuzla.customRev=$VERSION \ + -Dbitwuzla.rebuildWrapper=false \ + -Djdk-windows.path=$JDK_DIR_WINDOWS \ + -Djdk-linux-arm64.path=$JDK_DIR_LINUX_ARM64 ``` Example: ``` ant publish-bitwuzla \ - -Dbitwuzla.path=../bitwuzla/ -Dbitwuzla.customRev=0.4.0 \ - -Dbitwuzla.rebuildWrapper=false -Djdk-windows.path=/dependencies/jdk-11/ -``` -The build-scripts Bitwuzla will download and build necessary dependencies like GMP automatically. -Our build script will automatically append the git-revision of Bitwuzla, if available. -The build-steps will produce a Linux and a Windows library and publish them. + -Dbitwuzla.path=/workspace/solvers/bitwuzla/bitwuzla/ \ + -Dbitwuzla.customRev=0.6.0 \ + -Dbitwuzla.rebuildWrapper=false \ + -Djdk-windows-x64.path=/workspace/solvers/jdk/openjdk-17.0.2_windows-x64_bin/jdk-17.0.2/ \ + -Djdk-linux-arm64.path=/workspace/solvers/jdk/openjdk-17.0.2_linux-aarch64_bin/jdk-17.0.2/ +``` +The build-scripts for Bitwuzla ... : +- run for about 10 minutes (we build everything from scratch, three times). +- download and build necessary dependencies like GMP automatically. +- automatically append the git-revision of Bitwuzla, if available. +- produce two Linux (x64 and arm64) and one Windows (x64) library and publish them. Finally, follow the instructions shown in the message at the end. The instructions for publication via SVN into the Ivy repository are not intended to be executed in the Docker environment, diff --git a/solvers_ivy_conf/ivy_bitwuzla.xml b/solvers_ivy_conf/ivy_bitwuzla.xml index 5f44ceed04..80f74962ce 100644 --- a/solvers_ivy_conf/ivy_bitwuzla.xml +++ b/solvers_ivy_conf/ivy_bitwuzla.xml @@ -23,18 +23,28 @@ SPDX-License-Identifier: Apache-2.0 - - - - - + + + + + + + + + + + + + + - - + + + From d689f147b95a2f0825b9e33443d55160b92fc7a5 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 28 Oct 2024 15:48:59 +0100 Subject: [PATCH 43/63] Bitwuzla: update symlinks --- lib/native/arm64-linux/libbitwuzlaj.so | 1 + lib/native/x86_64-linux/libbitwuzlaj.so | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) create mode 120000 lib/native/arm64-linux/libbitwuzlaj.so diff --git a/lib/native/arm64-linux/libbitwuzlaj.so b/lib/native/arm64-linux/libbitwuzlaj.so new file mode 120000 index 0000000000..12c0179255 --- /dev/null +++ b/lib/native/arm64-linux/libbitwuzlaj.so @@ -0,0 +1 @@ +../../java/runtime-bitwuzla/arm64/libbitwuzlaj.so \ No newline at end of file diff --git a/lib/native/x86_64-linux/libbitwuzlaj.so b/lib/native/x86_64-linux/libbitwuzlaj.so index f853af1fc2..5d9be8a6cf 120000 --- a/lib/native/x86_64-linux/libbitwuzlaj.so +++ b/lib/native/x86_64-linux/libbitwuzlaj.so @@ -1 +1 @@ -../../java/runtime-bitwuzla/libbitwuzlaj.so \ No newline at end of file +../../java/runtime-bitwuzla/x64/libbitwuzlaj.so \ No newline at end of file From 7d3b3b6dfb213951c9cb1ab013672f0d00fbc006 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 28 Oct 2024 15:50:07 +0100 Subject: [PATCH 44/63] Bitwuzla: update dependency, include libraries for x64 and arm64 on Linux --- README.md | 2 +- lib/ivy.xml | 10 ++++++---- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 1b1cb8d84a..12765cdf65 100644 --- a/README.md +++ b/README.md @@ -58,7 +58,7 @@ JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started. | SMT Solver | Linux x64 | Linux arm64 | Windows x64 | Windows arm64 | MacOS x64 | MacOS arm64 | Description | | --- |:---:|:---:|:---:|:---:|:---:|:---:|:--- | -| [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark: | | :heavy_check_mark: | | | | a fast solver for bitvector logic | +| [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | | | | a fast solver for bitvector logic | | [Boolector](https://boolector.github.io/) | :heavy_check_mark: | | | | | | a fast solver for bitvector logic, misses formula introspection, deprecated | | [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | | | | | | | | [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | | | | | | | diff --git a/lib/ivy.xml b/lib/ivy.xml index 9b7bd6a5de..a39d9842eb 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -46,7 +46,9 @@ SPDX-License-Identifier: Apache-2.0 - + + + @@ -62,10 +64,10 @@ SPDX-License-Identifier: Apache-2.0 @@ -181,7 +183,7 @@ SPDX-License-Identifier: Apache-2.0 - + From e87c068aa7acde81d0f0219ff2d34c31969ae237 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 28 Oct 2024 16:15:10 +0100 Subject: [PATCH 45/63] Bitwuzla and MathSAT: fix dependency location on Windows CI. --- .appveyor.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.appveyor.yml b/.appveyor.yml index 6718320e88..a460c98065 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -35,8 +35,8 @@ build_script: # to make it available for JUnit tests. # See lib\native\x86_64-windows\README.md for details. - copy lib\java\runtime-z3\x64\*dll lib\native\x86_64-windows\ - - copy lib\java\runtime-mathsat\*dll lib\native\x86_64-windows\ - - copy lib\java\runtime-bitwuzla\*dll lib\native\x86_64-windows\ + - copy lib\java\runtime-mathsat\x64\*dll lib\native\x86_64-windows\ + - copy lib\java\runtime-bitwuzla\x64\*dll lib\native\x86_64-windows\ test_script: - ant unit-tests From 03acd1e87552718eb04c0409075d8716be012f52 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 28 Oct 2024 20:13:41 +0100 Subject: [PATCH 46/63] Bitwuzla: fix copy7paste error in script for publishing to Maven. --- build/build-maven-publish.xml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/build/build-maven-publish.xml b/build/build-maven-publish.xml index e301b06e69..0e60a036b3 100644 --- a/build/build-maven-publish.xml +++ b/build/build-maven-publish.xml @@ -179,15 +179,15 @@ SPDX-License-Identifier: Apache-2.0 - - + + - + From 0f0fd2cea8613ea80448a034d22867196d575304 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 28 Oct 2024 20:30:03 +0100 Subject: [PATCH 47/63] Bitwuzla: fix path according to documentation. This does not change the output of the script. --- build/build-publish-solvers/solver-bitwuzla.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build/build-publish-solvers/solver-bitwuzla.xml b/build/build-publish-solvers/solver-bitwuzla.xml index f69a91eac6..c4fb5d70ed 100644 --- a/build/build-publish-solvers/solver-bitwuzla.xml +++ b/build/build-publish-solvers/solver-bitwuzla.xml @@ -160,7 +160,7 @@ SPDX-License-Identifier: Apache-2.0 - + From 03ff9f3913764f5623712a580cad42af0eb6f87b Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Thu, 2 Jan 2025 15:06:54 +0100 Subject: [PATCH 48/63] Z3: update to version 4.13.4 --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index a39d9842eb..698ebf78c9 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -177,7 +177,7 @@ SPDX-License-Identifier: Apache-2.0 - + From ed50ec0de60ec707b735376ba1805c27c36af847 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 4 Jan 2025 15:59:29 +0100 Subject: [PATCH 49/63] more documentation --- doc/Developers-How-to-Release-into-Ivy.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/doc/Developers-How-to-Release-into-Ivy.md b/doc/Developers-How-to-Release-into-Ivy.md index eddf27c67b..2e0f15ac70 100644 --- a/doc/Developers-How-to-Release-into-Ivy.md +++ b/doc/Developers-How-to-Release-into-Ivy.md @@ -63,6 +63,11 @@ z3/ // <-- parent directory |-- z3-z3-4.13.3/ // <-- sources directory used as 'z3.path' ``` +You can prepare the Z3 Java sources on an arbitrary system, as we only prepare +Java sources and JavaDoc for the bindings, but do no compile any native library. +This only depends on a Python3 environment and Java 17 or later. +For simple usage, we provide a Docker definition/environment under `/docker`, in which the following command can be run. + In the unpacked sources directory, prepare Java sources via `python3 scripts/mk_make.py --java`. Then execute the following command in the JavaSMT directory, where `$Z3_DIR` is the path of the sources directory and `$Z3_VERSION` is the version number: From cd2529a68dafccc58a69f21d26f34ec04d96d349 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 5 Jan 2025 10:41:02 +0100 Subject: [PATCH 50/63] Z3, MathSAT5, Bitwuzla: use separate directory 'dist' for publication instead of JavaSMT root directory. --- .gitignore | 1 + build.xml | 3 +- build/build-publish-solvers/macros.xml | 3 +- .../build-publish-solvers/solver-bitwuzla.xml | 15 +++---- .../build-publish-solvers/solver-mathsat.xml | 24 ++++++----- build/build-publish-solvers/solver-z3.xml | 41 ++++++++++--------- 6 files changed, 47 insertions(+), 40 deletions(-) diff --git a/.gitignore b/.gitignore index d25be26a1c..b132f42f57 100644 --- a/.gitignore +++ b/.gitignore @@ -69,5 +69,6 @@ solvers_maven_conf/*.asc build.properties /.apt-generated/ /repository +/dist pom.xml diff --git a/build.xml b/build.xml index 850efbc87c..02176f81d0 100644 --- a/build.xml +++ b/build.xml @@ -36,6 +36,7 @@ SPDX-License-Identifier: Apache-2.0 "/> + @@ -80,7 +81,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/build/build-publish-solvers/macros.xml b/build/build-publish-solvers/macros.xml index d698480928..2a3301b685 100644 --- a/build/build-publish-solvers/macros.xml +++ b/build/build-publish-solvers/macros.xml @@ -32,6 +32,7 @@ SPDX-License-Identifier: Apache-2.0 + diff --git a/build/build-publish-solvers/solver-bitwuzla.xml b/build/build-publish-solvers/solver-bitwuzla.xml index c4fb5d70ed..367d470080 100644 --- a/build/build-publish-solvers/solver-bitwuzla.xml +++ b/build/build-publish-solvers/solver-bitwuzla.xml @@ -13,6 +13,7 @@ SPDX-License-Identifier: Apache-2.0 + @@ -188,15 +189,15 @@ SPDX-License-Identifier: Apache-2.0 - + - + - + - - - + + + - + - + - + - + @@ -71,7 +72,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -82,22 +83,22 @@ SPDX-License-Identifier: Apache-2.0 - - - - + + + + - - - - + + + + - - - - + + + + - + @@ -110,7 +111,7 @@ SPDX-License-Identifier: Apache-2.0 - + From ebd70301ae3453c0dd18c901c6989da770a5386f Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Thu, 16 Jan 2025 23:28:53 +0100 Subject: [PATCH 53/63] Bitwuzla: update library version to compiled with enabled experimental FP sizes. --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 48b5a012b4..542723a198 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -190,7 +190,7 @@ SPDX-License-Identifier: Apache-2.0 - + From 9156cee36b8a2e48e9639adb03b54ee1a4364480 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 19 Jan 2025 19:13:13 +0100 Subject: [PATCH 54/63] Bitwuzla: fix typo and rename task to avoid naming conflicts. --- build/build-publish-solvers/solver-bitwuzla.xml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/build/build-publish-solvers/solver-bitwuzla.xml b/build/build-publish-solvers/solver-bitwuzla.xml index 720f82fe8b..3c0aa67ede 100644 --- a/build/build-publish-solvers/solver-bitwuzla.xml +++ b/build/build-publish-solvers/solver-bitwuzla.xml @@ -147,8 +147,8 @@ SPDX-License-Identifier: Apache-2.0 - - + This ant-step uses the Linux x64 dependencies for building the SWIG-wrapper. @@ -186,7 +186,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -346,15 +346,15 @@ SPDX-License-Identifier: Apache-2.0 + depends="compile-bitwuzla-linux-x64, build-bitwuzla-wrapper, build-bitwuzla-bindings-linux-x64"> + depends="compile-bitwuzla-linux-arm64, build-bitwuzla-wrapper, build-bitwuzla-bindings-linux-arm64"> + depends="compile-bitwuzla-windows-x64, build-bitwuzla-wrapper, build-bitwuzla-bindings-windows-x64"> Date: Sun, 19 Jan 2025 19:13:16 +0100 Subject: [PATCH 55/63] OpenSMT: refactor build-script to align with other Swig-based build-scripts, like Bitwuzla. --- .gitignore | 1 + .../build-publish-solvers/solver-opensmt.xml | 188 +++++++++--------- 2 files changed, 97 insertions(+), 92 deletions(-) diff --git a/.gitignore b/.gitignore index b132f42f57..8f12518357 100644 --- a/.gitignore +++ b/.gitignore @@ -21,6 +21,7 @@ lib/native/source/libz3j/org_sosy_lab_solver_z3_Z3NativeApi.c lib/native/source/libbitwuzla/build lib/native/source/libbitwuzla/doc lib/native/source/libbitwuzla/install* +lib/native/source/opensmt/install* lib/native/source/*/*.so lib/native/source/*/*.o lib/native/source/**/*.java diff --git a/build/build-publish-solvers/solver-opensmt.xml b/build/build-publish-solvers/solver-opensmt.xml index 633357fe2d..ef36ab4078 100644 --- a/build/build-publish-solvers/solver-opensmt.xml +++ b/build/build-publish-solvers/solver-opensmt.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 +SPDX-FileCopyrightText: 2025 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> @@ -13,16 +13,12 @@ SPDX-License-Identifier: Apache-2.0 + + - - - Please specify the path to OpenSMT with the flag -Dopensmt.path=/path/to/opensmt. - The path has to point to the root OpenSMT folder, i.e., - a checkout of the official git repository from - 'https://github.com/usi-verification-and-security/opensmt.git'. - Note that shell substitutions do not work and a full absolute path has to be specified. - + + Please specify a custom revision with the flag -Dopensmt.customRev=XXX. The custom revision has to be unique amongst the already known version @@ -38,28 +34,33 @@ SPDX-License-Identifier: Apache-2.0 - - - - + + + + + + + + + + + + - - + + + - + - - - - - - - + + + @@ -67,121 +68,124 @@ SPDX-License-Identifier: Apache-2.0 - + - - - + + + + - - - + + + + + + + + + + + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + - - + + + + - - - - - + + + + - #define VERSION "${opensmt.version}" + #define VERSION "${opensmt.version}" - - + + - - - - + + + - + + - + - + + - - - - - - - - - + + + - + + + + + + + + - + From 478ac33836fe0714b52a6ef685993fa770ca3992 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 19 Jan 2025 19:13:16 +0100 Subject: [PATCH 56/63] OpenSMT: replace GMP from Docker image with externally compiled GMP, and improve the linking process. --- .../build-publish-solvers/solver-opensmt.xml | 21 ++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/build/build-publish-solvers/solver-opensmt.xml b/build/build-publish-solvers/solver-opensmt.xml index ef36ab4078..de56885de8 100644 --- a/build/build-publish-solvers/solver-opensmt.xml +++ b/build/build-publish-solvers/solver-opensmt.xml @@ -19,6 +19,15 @@ SPDX-License-Identifier: Apache-2.0 + + + + Please specify a custom revision with the flag -Dopensmt.customRev=XXX. The custom revision has to be unique amongst the already known version @@ -159,12 +168,14 @@ SPDX-License-Identifier: Apache-2.0 + + + + + + - - - - - + From e7b03efdd0715a4bfea274b80e7a361231b41f41 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 19 Jan 2025 19:13:16 +0100 Subject: [PATCH 57/63] OpenSMT: add compilation step for Linux on ARM64. OpenSMT can be compiled for ARM in two simple steps: - provide GMP for ARM64 (we use the version that we provide for MathSAT anyway) - replace GCC with the cross-compiler for ARM64 --- README.md | 2 +- build.xml | 4 +- build/build-maven-publish.xml | 6 +- .../build-publish-solvers/solver-opensmt.xml | 123 +++++++++++++++++- doc/Developers-How-to-Release-into-Ivy.md | 46 ++++++- solvers_ivy_conf/ivy_opensmt.xml | 21 ++- 6 files changed, 182 insertions(+), 20 deletions(-) diff --git a/README.md b/README.md index 529b18feab..a11a213c91 100644 --- a/README.md +++ b/README.md @@ -63,7 +63,7 @@ JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started. | [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | | | | | | | | [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | | | | | | | | [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | | | | | -| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark: | | | | | | | +| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark: | :heavy_check_mark: | | | | | | | [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | | | | | | based on MathSAT5, with support for optimization queries | | [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver | | [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver | diff --git a/build.xml b/build.xml index 02176f81d0..dd63649c65 100644 --- a/build.xml +++ b/build.xml @@ -86,8 +86,8 @@ SPDX-License-Identifier: Apache-2.0 - - + + diff --git a/build/build-maven-publish.xml b/build/build-maven-publish.xml index 0e60a036b3..441b6a07ea 100644 --- a/build/build-maven-publish.xml +++ b/build/build-maven-publish.xml @@ -114,12 +114,14 @@ SPDX-License-Identifier: Apache-2.0 + + - - + + diff --git a/build/build-publish-solvers/solver-opensmt.xml b/build/build-publish-solvers/solver-opensmt.xml index de56885de8..cd12e69113 100644 --- a/build/build-publish-solvers/solver-opensmt.xml +++ b/build/build-publish-solvers/solver-opensmt.xml @@ -25,8 +25,15 @@ SPDX-License-Identifier: Apache-2.0 For linux-x64: ./configure -?-enable-cxx -?-with-pic -?-disable-shared -?-enable-static -?-enable-fat make -j4 + For linux-arm64: + ./configure -?-enable-cxx -?-with-pic -?-disable-shared -?-enable-static -?-enable-fat \ + -?-host=aarch64-linux-gnu \ + CC=aarch64-linux-gnu-gcc CXX=aarch64-linux-gnu-g++ LD=aarch64-linux-gnu-ld + make -j4 --> + + Please specify a custom revision with the flag -Dopensmt.customRev=XXX. @@ -48,9 +55,11 @@ SPDX-License-Identifier: Apache-2.0 + + @@ -66,7 +75,10 @@ SPDX-License-Identifier: Apache-2.0 - + + @@ -86,6 +98,40 @@ SPDX-License-Identifier: Apache-2.0 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -152,9 +198,10 @@ SPDX-License-Identifier: Apache-2.0 + - + + #define VERSION "${opensmt.version}" + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + Lets copy the files for architecture x64 into main directory, for backwards compatibility. + Afterward, please execute the SVN command from above. + + + + + + diff --git a/doc/Developers-How-to-Release-into-Ivy.md b/doc/Developers-How-to-Release-into-Ivy.md index 9ae7127397..cb6ee752a3 100644 --- a/doc/Developers-How-to-Release-into-Ivy.md +++ b/doc/Developers-How-to-Release-into-Ivy.md @@ -142,14 +142,48 @@ We prefer to build directly on Ubuntu 22.04, where CMake, SWIG, and GCC are suff For simple usage, we provide a Docker definition/environment under `/docker`, in which the following command can be run. -To publish OpenSMT, checkout the [OpenSMT repository](https://github.com/usi-verification-and-security/opensmt). -Then execute the following command in the JavaSMT directory to patch the OpenSMT2 API, -generate Java bindings with SWIG, build the library, and package it. +Please provide GMP from http://gmplib.org/ in version 6.3.0 (version 6.2.1 also works) and build GMP: +- For linux-x64 in directory $GMP_DIR_LINUX_X64: + ``` + ./configure --enable-cxx --with-pic --disable-shared --enable-static --enable-fat + make -j4 + ``` +- For linux-arm64 in directory $GMP_DIR_LINUX_ARM64: + ``` + ./configure --enable-cxx --with-pic --disable-shared --enable-static --enable-fat \ + --host=aarch64-linux-gnu \ + CC=aarch64-linux-gnu-gcc CXX=aarch64-linux-gnu-g++ LD=aarch64-linux-gnu-ld + make -j4 + ``` + +For linux-arm64, provide JNI headers in a reasonable LTS version. +Download the zip archive from https://jdk.java.net/ and unpack it into $JDK_DIR_LINUX_ARM64 +(e.g., https://download.java.net/java/GA/jdk17.0.2/dfd4a8d0985749f896bed50d7138ee7f/8/GPL/openjdk-17.0.2_linux-aarch64_bin.tar.gz). +To publish OpenSMT, checkout the [OpenSMT repository](https://github.com/usi-verification-and-security/opensmt). +Then execute the following command in the JavaSMT directory: ``` -ant publish-opensmt -Dopensmt.path=/workspace/opensmt -Dopensmt.customRev=2.8.0 +ant publish-opensmt \ + -Dopensmt.path=$OPENSMT_DIR \ + -Dopensmt.customRev=$VERSION \ + -Dgmp-linux-x64.path=$GMP_DIR_LINUX_X64 \ + -Dgmp-linux-arm64.path=$GMP_DIR_LINUX_ARM64 \ + -Djdk-linux-arm64.path=$JDK_DIR_LINUX_ARM64 ``` -Our build script will automatically append the git revision of OpenSMT. +Example: +``` +ant publish-opensmt \ + -Dopensmt.path=/workspace/solvers/opensmt/opensmt \ + -Dopensmt.customRev=2.8.0-sosy0 \ + -Dgmp-linux-x64.path=/workspace/solvers/gmp/gmp-6.3.0-linux-x64 \ + -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 +``` +The build scripts for OpenSMT ... : +- run for about 20 minutes (we build everything from scratch, two times). +- download Google-based test components (requires internet access). +- append the git revision of Bitwuzla. +- produce two Linux (x64 and arm64) libraries, and publish them. Finally, follow the instructions shown in the message at the end of the command. The instructions for publication via SVN into the Ivy repository are not intended to be executed in the Docker environment, @@ -212,7 +246,7 @@ The build scripts for Bitwuzla ... : - run for about 10 minutes (we build everything from scratch, three times). - download and build necessary dependencies like GMP automatically. - append the git revision of Bitwuzla. -- produce two Linux (x64 and arm64) and one Windows (x64) library and publish them. +- produce two Linux (x64 and arm64) libraries and one Windows (x64) library, and publish them. Finally, follow the instructions shown in the message at the end of the command. The instructions for publication via SVN into the Ivy repository are not intended to be executed in the Docker environment, diff --git a/solvers_ivy_conf/ivy_opensmt.xml b/solvers_ivy_conf/ivy_opensmt.xml index c41149c383..c27ed33dfb 100644 --- a/solvers_ivy_conf/ivy_opensmt.xml +++ b/solvers_ivy_conf/ivy_opensmt.xml @@ -21,18 +21,29 @@ SPDX-License-Identifier: Apache-2.0 OpenSMT is provided under the MIT License. - + - - - + + + + + + + + + + + + + - + + From d7a3059073c50ec231db9c44ac03e4be5e878811 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 19 Jan 2025 19:13:17 +0100 Subject: [PATCH 58/63] OpenSMT: rename library, i.e., shorten "java" to "j". --- build/build-maven-publish.xml | 4 ++-- build/build-publish-solvers/solver-opensmt.xml | 16 ++++++++-------- lib/native/arm64-linux/libopensmtj.so | 1 + lib/native/x86_64-linux/libopensmtj.so | 1 + lib/native/x86_64-linux/libopensmtjava.so | 1 - solvers_ivy_conf/ivy_opensmt.xml | 4 ++-- .../solvers/opensmt/OpenSmtNativeAPITest.java | 3 +-- .../solvers/opensmt/OpenSmtSolverContext.java | 2 +- .../java_smt/test/SolverContextFactoryTest.java | 4 ++-- 9 files changed, 18 insertions(+), 18 deletions(-) create mode 120000 lib/native/arm64-linux/libopensmtj.so create mode 120000 lib/native/x86_64-linux/libopensmtj.so delete mode 120000 lib/native/x86_64-linux/libopensmtjava.so diff --git a/build/build-maven-publish.xml b/build/build-maven-publish.xml index 441b6a07ea..73204abef6 100644 --- a/build/build-maven-publish.xml +++ b/build/build-maven-publish.xml @@ -120,8 +120,8 @@ SPDX-License-Identifier: Apache-2.0 - - + + diff --git a/build/build-publish-solvers/solver-opensmt.xml b/build/build-publish-solvers/solver-opensmt.xml index cd12e69113..bf23f9cc57 100644 --- a/build/build-publish-solvers/solver-opensmt.xml +++ b/build/build-publish-solvers/solver-opensmt.xml @@ -201,7 +201,7 @@ SPDX-License-Identifier: Apache-2.0 - + + - - + + diff --git a/lib/native/arm64-linux/libopensmtj.so b/lib/native/arm64-linux/libopensmtj.so new file mode 120000 index 0000000000..0d0d693892 --- /dev/null +++ b/lib/native/arm64-linux/libopensmtj.so @@ -0,0 +1 @@ +../../java/runtime-opensmt/arm64/libopensmtj.so \ No newline at end of file diff --git a/lib/native/x86_64-linux/libopensmtj.so b/lib/native/x86_64-linux/libopensmtj.so new file mode 120000 index 0000000000..7733eba50e --- /dev/null +++ b/lib/native/x86_64-linux/libopensmtj.so @@ -0,0 +1 @@ +../../java/runtime-opensmt/x64/libopensmtj.so \ No newline at end of file diff --git a/lib/native/x86_64-linux/libopensmtjava.so b/lib/native/x86_64-linux/libopensmtjava.so deleted file mode 120000 index 931486be49..0000000000 --- a/lib/native/x86_64-linux/libopensmtjava.so +++ /dev/null @@ -1 +0,0 @@ -../../java/runtime-opensmt/libopensmtjava.so \ No newline at end of file diff --git a/solvers_ivy_conf/ivy_opensmt.xml b/solvers_ivy_conf/ivy_opensmt.xml index c27ed33dfb..d8ce3e668e 100644 --- a/solvers_ivy_conf/ivy_opensmt.xml +++ b/solvers_ivy_conf/ivy_opensmt.xml @@ -42,8 +42,8 @@ SPDX-License-Identifier: Apache-2.0 - - + + diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtNativeAPITest.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtNativeAPITest.java index e8b26f98db..322dca0a6c 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtNativeAPITest.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtNativeAPITest.java @@ -37,8 +37,7 @@ public class OpenSmtNativeAPITest { @BeforeClass public static void load() { try { - NativeLibraries.loadLibrary("opensmt"); - NativeLibraries.loadLibrary("opensmtjava"); + NativeLibraries.loadLibrary("opensmtj"); } catch (UnsatisfiedLinkError e) { throw new AssumptionViolatedException("OpenSMT is not available", e); } diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtSolverContext.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtSolverContext.java index da602bcc54..cc525d7c5b 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtSolverContext.java @@ -86,7 +86,7 @@ public static SolverContext create( throws InvalidConfigurationException { // Make sure the native libraries are loaded - pLoader.accept("opensmtjava"); + pLoader.accept("opensmtj"); OpenSMTOptions solverOptions = new OpenSMTOptions(config, (int) pRandom); diff --git a/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java b/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java index b85bea445b..a5886c621a 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java @@ -99,7 +99,7 @@ private void requireSupportedOperatingSystem() { return; case OPENSMT: assume.that(IS_LINUX).isTrue(); - assume.that(isSufficientVersionOfLibcxx("opensmtjava")).isTrue(); + assume.that(isSufficientVersionOfLibcxx("opensmtj")).isTrue(); return; case BITWUZLA: assume.that(IS_LINUX).isTrue(); @@ -144,7 +144,7 @@ private String[] getRequiredLibcxx(String library) { case "z3": return new String[] {"GLIBC_2.34", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; case "bitwuzlaj": - case "opensmtjava": + case "opensmtj": return new String[] {"GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; case "mathsat5j": return new String[] {"GLIBC_2.33"}; From 3d81fe2619b69649cd776f778932ced8f8baafdb Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 19 Jan 2025 19:13:17 +0100 Subject: [PATCH 59/63] OpenSMT: update dependency to use x64/arm64 version of OpenSMT. --- lib/ivy.xml | 10 ++++++---- lib/native/arm64-linux/libopensmtjava.so | 1 + 2 files changed, 7 insertions(+), 4 deletions(-) create mode 120000 lib/native/arm64-linux/libopensmtjava.so diff --git a/lib/ivy.xml b/lib/ivy.xml index 542723a198..cfb32dc962 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -34,7 +34,9 @@ SPDX-License-Identifier: Apache-2.0 - + + + @@ -64,10 +66,10 @@ SPDX-License-Identifier: Apache-2.0 @@ -185,7 +187,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/lib/native/arm64-linux/libopensmtjava.so b/lib/native/arm64-linux/libopensmtjava.so new file mode 120000 index 0000000000..b91915ab43 --- /dev/null +++ b/lib/native/arm64-linux/libopensmtjava.so @@ -0,0 +1 @@ +../../java/runtime-opensmt/arm64/libopensmtjava.so \ No newline at end of file From 13b3f1267994f33139ea906353eb3e08c532799c Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 19 Jan 2025 20:35:44 +0100 Subject: [PATCH 60/63] OpenSMT: enrich test with info about GLIBC dependency. --- src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java b/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java index a5886c621a..92b19127ab 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java @@ -144,8 +144,9 @@ private String[] getRequiredLibcxx(String library) { case "z3": return new String[] {"GLIBC_2.34", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; case "bitwuzlaj": - case "opensmtj": return new String[] {"GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "opensmtj": + return new String[] {"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; case "mathsat5j": return new String[] {"GLIBC_2.33"}; default: From 657ee3c594cde19a088a675d6379ad73a9dc99d7 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 19 Jan 2025 21:22:28 +0100 Subject: [PATCH 61/63] AppVeyor: improve Windows build --- .appveyor.yml | 45 ++++++++++++++++++++++++++++----------------- 1 file changed, 28 insertions(+), 17 deletions(-) diff --git a/.appveyor.yml b/.appveyor.yml index b6af708377..52fc2f2556 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -2,7 +2,7 @@ # an API wrapper for a collection of SMT solvers: # https://github.com/sosy-lab/java-smt # -# SPDX-FileCopyrightText: 2024 Dirk Beyer +# SPDX-FileCopyrightText: 2025 Dirk Beyer # # SPDX-License-Identifier: Apache-2.0 @@ -15,17 +15,22 @@ clone_depth: 1 install: - ps: | Add-Type -AssemblyName System.IO.Compression.FileSystem - if (!(Test-Path -Path "C:\ant\apache-ant-1.10.15" )) { - (new-object System.Net.WebClient).DownloadFile( - 'https://archive.apache.org/dist/ant/binaries/apache-ant-1.10.15-bin.zip', + $antPath = "C:\ant\apache-ant-1.10.15" + if (!(Test-Path -Path $antPath)) { + echo "Downloading and extracting Apache Ant..." + (New-Object System.Net.WebClient).DownloadFile( + 'https://archive.apache.org/dist/ant/binaries/apache-ant-1.10.15-bin.zip', 'C:\ant-bin.zip' ) [System.IO.Compression.ZipFile]::ExtractToDirectory("C:\ant-bin.zip", "C:\ant") } + # Set environment variables - SET JAVA_HOME=C:\Program Files\Java\jdk17 - SET PATH=C:\ant\apache-ant-1.10.15\bin;%JAVA_HOME%\bin;%PATH% - SET IVY_CACHE_DIR=C:\ivy + # Verify environment - echo %USERPROFILE% + - echo %JAVA_HOME% - echo %PATH% - java -version @@ -34,35 +39,41 @@ build_script: # 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\x64\*dll lib\native\x86_64-windows\ - - copy lib\java\runtime-mathsat\x64\*dll lib\native\x86_64-windows\ - - copy lib\java\runtime-bitwuzla\x64\*dll lib\native\x86_64-windows\ + - ps: | + echo "Copying native solver binaries..." + Copy-Item -Path "lib\java\runtime-z3\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force + Copy-Item -Path "lib\java\runtime-mathsat\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force + Copy-Item -Path "lib\java\runtime-bitwuzla\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force test_script: - ant unit-tests on_finish: - ps: | + echo "Uploading JUnit test results..." $wc = New-Object 'System.Net.WebClient' $files = Get-ChildItem -Path ".\junit\TEST-*.xml" -Exclude "*VariableNames*" $url = "https://ci.appveyor.com/api/testresults/junit/$($env:APPVEYOR_JOB_ID)" - foreach($file in $files){ - echo $file.FullName + foreach ($file in $files) { + echo "Uploading $($file.FullName)..." $wc.UploadFile($url, $file.FullName) } - ps: | - $files = Get-ChildItem -Path ".\hs_err_pid*" - foreach($file in $files){ - echo $file.FullName - Push-AppveyorArtifact $file.FullName -DeploymentName $file.name + echo "Uploading error files as artifacts..." + $errorFiles = Get-ChildItem -Path ".\hs_err_pid*" + foreach ($file in $errorFiles) { + echo "Uploading $($file.FullName)..." + Push-AppveyorArtifact $file.FullName -DeploymentName $file.Name } - ps: | - $files = Get-ChildItem -Path ".\replay_pid*" - foreach($file in $files){ - echo $file.FullName - Push-AppveyorArtifact $file.FullName -DeploymentName $file.name + echo "Uploading replay files as artifacts..." + $replayFiles = Get-ChildItem -Path ".\replay_pid*" + foreach ($file in $replayFiles) { + echo "Uploading $($file.FullName)..." + Push-AppveyorArtifact $file.FullName -DeploymentName $file.Name } - ps: | + echo "Compressing and uploading JUnit HTML report..." 7z a JUnit.html.zip JUnit.html Push-AppveyorArtifact JUnit.html.zip -DeploymentName "JUnit Report" From 244467c7630bff847416d768b5628f22fe6ffc01 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 25 Jan 2025 14:37:25 +0100 Subject: [PATCH 62/63] update Readme. --- README.md | 67 ++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 41 insertions(+), 26 deletions(-) diff --git a/README.md b/README.md index a11a213c91..a59a31dcf6 100644 --- a/README.md +++ b/README.md @@ -24,6 +24,7 @@ wrapping layer) and type-safety (it shouldn't be possible to add boolean terms to integer ones at _compile_ time) sometimes at the cost of verbosity. #### Quick links + [Getting Started](doc/Getting-started.md) | [Documentation][JavaDoc] | [Known Issues](doc/KnownIssues.md) | @@ -41,6 +42,7 @@ to integer ones at _compile_ time) sometimes at the cost of verbosity. In Proc. VSTTE, LNCS 9971, pages 139–148, 2016. Springer. ### Feature overview + JavaSMT can express formulas in the following theories: - Integer @@ -54,33 +56,42 @@ JavaSMT can express formulas in the following theories: The concrete support for a certain theory depends on the underlying SMT solver. Only a few SMT solvers provide support for theories like Arrays, Floating Point, String or RegEx. +#### Solver support for different Operating System and Architectures + JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started.md) for installation): -| SMT Solver | Linux x64 | Linux arm64 | Windows x64 | Windows arm64 | MacOS x64 | MacOS arm64 | Description | -| --- |:---:|:---:|:---:|:---:|:---:|:---:|:--- | -| [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | | | | a fast solver for bitvector logic | -| [Boolector](https://boolector.github.io/) | :heavy_check_mark: | | | | | | a fast solver for bitvector logic, misses formula introspection, deprecated | -| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | | | | | | | -| [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | | | | | | | -| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | | | | | -| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark: | :heavy_check_mark: | | | | | | -| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | | | | | | based on MathSAT5, with support for optimization queries | -| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver | -| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver | -| [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: | | [maybe](https://github.com/sosy-lab/java-smt/pull/215) | | | | | -| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | mature and well-known solver | - -#### Operating System and Architecture Support +| SMT Solver | Linux x64 | Linux arm64 | Windows x64 | Windows arm64 | MacOS x64 | MacOS arm64 | Description | +| --- |:---------------------:|:-------------------:|:---:|:---:|:------------------------------------------------------:|:---:|:--- | +| [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark:² | :heavy_check_mark:² | :heavy_check_mark: | | | | a fast solver for bitvector logic | +| [Boolector](https://boolector.github.io/) | :heavy_check_mark: | | | | | | a fast solver for bitvector logic, misses formula introspection, deprecated | +| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | | | | | | | +| [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | | | | | | | +| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | | [maybe](https://github.com/sosy-lab/java-smt/pull/430)³ | | | +| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark:² | :heavy_check_mark:² | | | | | | +| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | | | | | | based on MathSAT5, with support for optimization queries | +| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver | +| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver | +| [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: | | [maybe](https://github.com/sosy-lab/java-smt/pull/215) | | [maybe](https://github.com/sosy-lab/java-smt/pull/400)³ | | | +| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark:² | :heavy_check_mark:² | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | mature and well-known solver | + We support a reasonable list of operating systems and versions. -Our main target is Linux (64-bit, mainly Ubuntu 22.04 or newer, -several solver libraries also work on Ubuntu 18.04, or comparable Linux distributions). -Windows 10/11 and MacOS are supported for several SMT solvers. -Our main development architecture is x64 (x86-64). -We also provide some solvers for ARM64 (AArch64 for ARMv8-A), e.g., Java-based SMT solvers, Z3, and MathSAT. -If a specific operating system or architecture is missing and required, -please do not hesitate and open an issue! +- Our main target is Linux (mainly Ubuntu or comparable Linux distributions). + Windows 10/11 and MacOS are supported for several SMT solvers. +- Our main development architecture is x64 (x86-64). + We also provide some solvers for ARM64 (AArch64 for ARMv8-A), e.g., Java-based SMT solvers, Z3, and MathSAT. + If a specific operating system or architecture is missing and required, + please do not hesitate and open an issue! + +On all operating systems and architectures, JavaSMT requires Java 11 or newer. +Unless otherwise noted, the solver requires a minimum of `GLIBC_2.28` on Linux, +available with Ubuntu 18.04 or later. + +² Solver requires at least `GLIBC_2.29`/`GLIBCXX_3.4.26` or `GLIBC_2.34`/`GLIBCXX_3.4.29`, +available with Ubuntu 22.04 or later. +³ We do not provide a signed solver library for MacOS. The user needs to compile and sign it. #### Solver Features + The following features are supported (depending on the used SMT solver): - Satisfiability checking @@ -97,7 +108,8 @@ We aim for supporting more important features, more SMT solvers, and more system If something specific is missing, please [look for or file an issue](https://github.com/sosy-lab/java-smt/issues). #### Multithreading Support -| SMT Solver | Concurrent context usage¹ | Concurrent prover usage² | + +| SMT Solver | Concurrent context usage⁴ | Concurrent prover usage⁵ | | --- |:---:|:---:| | [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark: | | | [Boolector](https://boolector.github.io/) | :heavy_check_mark: | | @@ -114,10 +126,11 @@ If something specific is missing, please [look for or file an issue](https://git Interruption using a [ShutdownNotifier][] may be used to interrupt a solver from any thread. Formulas are translatable in between contexts/provers/threads using _FormulaManager.translateFrom()_. -¹ Multiple contexts, but all operations on each context only from a single thread. -² Multiple provers on one or more contexts, with each prover using its own thread. +⁴ Multiple contexts, but all operations on each context only from a single thread. +⁵ Multiple provers on one or more contexts, with each prover using its own thread. #### Garbage Collection in Native Solvers + JavaSMT exposes an API for performing garbage collection on solvers implemented in a native language. As a native solver has no way of knowing whether the created formula object is still referenced by the client application, this API is necessary to avoid leaking memory. @@ -132,15 +145,17 @@ compared to solver-internal memory-consumption when solving a hard SMT query. whether JavaSMT will attempt to decrease references on Z3 formula objects once they are no longer referenced. - **MathSAT5**: Currently we do not support performing garbage collection for MathSAT5. -- **CVC4, CVC5, Bitwuzla**: Solvers using SWIG bindings do perform garbage collection. +- **CVC4, CVC5, Bitwuzla, OpenSMT**: Solvers using SWIG bindings do perform garbage collection. - **Other native SMT solvers**: we do not perform garbage collection. ## Getting started + Installation is possible via [Maven][Maven repository], [Ivy][Ivy repository], or [manually][Manual Installation]. Please see our [Getting Started Guide](doc/Getting-started.md). #### Usage + ``` java // Instantiate JavaSMT with SMTInterpol as backend (for dependencies cf. documentation) try (SolverContext context = SolverContextFactory.createSolverContext( From 937b9171fce06cd041059e0cd91b6244e3593df8 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 25 Jan 2025 15:59:28 +0100 Subject: [PATCH 63/63] update Maven example projects with new library versions. The compilation will fail, because JavaSMT is not yet released in a new version, and some library names have been changed. --- doc/Example-Maven-Project/pom.xml | 28 ++++++++++++------------- doc/Example-Maven-Web-Project/pom.xml | 30 +++++++++++++-------------- 2 files changed, 27 insertions(+), 31 deletions(-) diff --git a/doc/Example-Maven-Project/pom.xml b/doc/Example-Maven-Project/pom.xml index 4acff46414..f182b2cb49 100644 --- a/doc/Example-Maven-Project/pom.xml +++ b/doc/Example-Maven-Project/pom.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: 2023 Dirk Beyer +SPDX-FileCopyrightText: 2025 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> @@ -16,7 +16,7 @@ SPDX-License-Identifier: Apache-2.0 org.sosy_lab.java_smt_example java-smt-maven-example - 1.11 + 1.12 java-smt-maven-example Example Maven project to show how to use JavaSMT with native solver libraries. https://github.com/sosy-lab/java-smt @@ -74,15 +74,15 @@ SPDX-License-Identifier: Apache-2.0 5.0.0 - 0.4.0-g4dbf3b1f + 0.7.0-13.1-g595512ae 3.2.2-g1a89c229 1.8-prerelease-2020-06-24-g7825d8f28 1.0.5-g4cb2ab9eb - 5.6.10 - 2.6.0-g2f72cc0e + 5.6.11-glibc2.27 + 2.8.0-sosy0-ge831bf23 4.1.1-734-g3732f7e08 2.6.2-396-g194350c1 - 4.13.0 + 4.13.4 @@ -97,7 +97,7 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-mathsat5 ${mathsat.version} - libmathsat5j + libmathsat5j-${system.arch} so @@ -128,14 +128,13 @@ SPDX-License-Identifier: Apache-2.0 javasmt-solver-bitwuzla ${bitwuzla.version} jar - bitwuzla org.sosy-lab javasmt-solver-bitwuzla ${bitwuzla.version} so - libbitwuzlaj + libbitwuzlaj-${system.arch} @@ -256,14 +255,13 @@ SPDX-License-Identifier: Apache-2.0 javasmt-solver-opensmt ${opensmt.version} jar - opensmt org.sosy-lab javasmt-solver-opensmt ${opensmt.version} so - libopensmtjava + libopensmtj-${system.arch} @@ -360,7 +358,7 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-mathsat5 so - libmathsat5j + libmathsat5j-${system.arch} libmathsat5j.so @@ -385,7 +383,7 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-bitwuzla so - libbitwuzlaj + libbitwuzlaj-${system.arch} libbitwuzlaj.so @@ -490,8 +488,8 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-opensmt so - libopensmtjava - libopensmtjava.so + libopensmtj-${system.arch} + libopensmtj.so diff --git a/doc/Example-Maven-Web-Project/pom.xml b/doc/Example-Maven-Web-Project/pom.xml index 47d0edaafe..d32c8c1339 100644 --- a/doc/Example-Maven-Web-Project/pom.xml +++ b/doc/Example-Maven-Web-Project/pom.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: 2023 Dirk Beyer +SPDX-FileCopyrightText: 2025 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> @@ -16,7 +16,7 @@ SPDX-License-Identifier: Apache-2.0 org.sosy_lab.java_smt_web_example java-smt-web-example - 1.11 + 1.12 war java-smt-maven-web-example Example Maven project to show how to use JavaSMT with native solver libraries in a web project. @@ -75,15 +75,15 @@ SPDX-License-Identifier: Apache-2.0 5.0.0 - 0.4.0-g4dbf3b1f + 0.7.0-13.1-g595512ae 3.2.2-g1a89c229 1.8-prerelease-2020-06-24-g7825d8f28 1.0.5-g4cb2ab9eb - 5.6.10 - 2.6.0-g2f72cc0e + 5.6.11-glibc2.27 + 2.8.0-sosy0-ge831bf23 4.1.1-734-g3732f7e08 2.6.2-396-g194350c1 - 4.13.0 + 4.13.4 @@ -98,7 +98,7 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-mathsat5 ${mathsat.version} - libmathsat5j + libmathsat5j-${system.arch} so @@ -129,14 +129,13 @@ SPDX-License-Identifier: Apache-2.0 javasmt-solver-bitwuzla ${bitwuzla.version} jar - bitwuzla org.sosy-lab javasmt-solver-bitwuzla ${bitwuzla.version} so - libbitwuzlaj + libbitwuzlaj-${system.arch} @@ -257,14 +256,13 @@ SPDX-License-Identifier: Apache-2.0 javasmt-solver-opensmt ${opensmt.version} jar - opensmt org.sosy-lab javasmt-solver-opensmt ${opensmt.version} so - libopensmtjava + libopensmtj-${system.arch} @@ -329,7 +327,7 @@ SPDX-License-Identifier: Apache-2.0 libpoly.so libpolyxx.so libyices2j.so - libopensmtjava.so + libopensmtj.so WEB-INF/lib @@ -406,7 +404,7 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-mathsat5 so - libmathsat5j + libmathsat5j-${system.arch} libmathsat5j.so @@ -431,7 +429,7 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-bitwuzla so - libbitwuzlaj + libbitwuzlaj-${system.arch} libbitwuzlaj.so @@ -536,8 +534,8 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-opensmt so - libopensmtjava - libopensmtjava.so + libopensmtj-${system.arch} + libopensmtj.so