Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

#380 support multiple architectures for solver binaries z3 #395

Open
wants to merge 49 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
49 commits
Select commit Hold shift + click to select a range
2b5e801
initial steps to provide multiple binaries of Z3.
kfriedberger Sep 11, 2024
2349bae
configure Ivy with a new classifier for 'arch', tested for Z3 binary.
kfriedberger Sep 17, 2024
68bab2b
#380: reduce manual steps for publishing Z3, create copies of library…
kfriedberger Sep 29, 2024
fa64e1d
#380: make cache-pattern more similar to default pattern.
kfriedberger Sep 29, 2024
a3021ab
fix typo in property usage.
kfriedberger Sep 29, 2024
5d70c5f
update Z3 to v4.13.0.
kfriedberger Sep 29, 2024
ddc9977
Maven: change publication pattern, do not use classifier for plain Ja…
kfriedberger Sep 29, 2024
14699d6
#380: rewrite Maven publication step to support x64 and arm64 archite…
kfriedberger Sep 29, 2024
78a298e
update Maven examples as expected to work. Not yet tested.
kfriedberger Sep 29, 2024
a55cfe7
#380: update readme to show our support for ARM64.
kfriedberger Sep 29, 2024
9d68306
#380: make basic configurations for Z3 public.
kfriedberger Oct 12, 2024
321da34
Z3: update to v4.13.2
kfriedberger Oct 12, 2024
bbfb727
Z3: update build-scripts for v4.13.3
kfriedberger Oct 12, 2024
d6019c6
Z3: avoid regression error.
kfriedberger Oct 12, 2024
8a2cddb
fix paths for Windows-based CI.
kfriedberger Oct 12, 2024
32d5b71
Z3: update to v4.13.3
kfriedberger Oct 12, 2024
9c6867f
exclude Z3 on some older Linux systems.
kfriedberger Oct 13, 2024
316d99e
use platform-independent solver for simple test.
kfriedberger Oct 13, 2024
4a40c32
improve exception messages in concurrent tests, i.e. also print the s…
kfriedberger Oct 13, 2024
95d3ab3
improve exception messages in concurrent tests, i.e. also print the s…
kfriedberger Oct 13, 2024
07a4015
update the image for Windows-based CI. This might fix problems with Z…
kfriedberger Oct 13, 2024
6f25eb3
update the image for Windows-based CI: use JDK 17.
kfriedberger Oct 13, 2024
78f2ada
Revert "update the image for Windows-based CI. This might fix problem…
kfriedberger Oct 13, 2024
a969311
#380: add symlinks for Z3 for ARM64.
kfriedberger Oct 13, 2024
e662615
update sosy-lab-common to latest release 0.3000-609-g90a352c
kfriedberger Oct 13, 2024
086c4b9
#380: extend JavaSMTs own ivy configuration to provide configurations…
kfriedberger Oct 13, 2024
598b0f9
cleanup Z3 build-script
kfriedberger Oct 16, 2024
bd4ad9b
update Dockerfile to compile solvers for arm64 architecture.
kfriedberger Oct 16, 2024
7494d84
MathSAT5: update/prepare build-scripts for several platforms, and upd…
kfriedberger Oct 16, 2024
a27dd38
MathSAT: update build documentation
kfriedberger Oct 16, 2024
08143b7
MathSAT5: update Ivy configuration for x64 and arm64
kfriedberger Oct 16, 2024
8302e03
MathSAT5: add symlinks to architecture-dependent libraries.
kfriedberger Oct 16, 2024
2dbefcd
fix cleanup script, if temporary build-directories are missing.
kfriedberger Oct 16, 2024
141f606
exclude MathSAT5 on some older Linux systems.
kfriedberger Oct 16, 2024
e4cbf36
MathSAT5: simplify Ivy dependencies.
kfriedberger Oct 19, 2024
655d360
Update Readme and user guide.
kfriedberger Oct 19, 2024
ec1766d
MathSAT5: fix publication script.
kfriedberger Oct 19, 2024
c8a4220
Merge remote-tracking branch 'origin/master' into 380-multi-architect…
kfriedberger Oct 20, 2024
24bcd6f
MathSAT: avoid using MathSAT on CI when GLIBC_2.33 is not available. …
kfriedberger Oct 20, 2024
30d9d69
update the Ubuntu18.04 Docker image for cross-architecture builds.
kfriedberger Oct 20, 2024
696f7b8
MathSAT5: provide a dependency that works on older Ubuntu, such as 18…
kfriedberger Oct 20, 2024
2f4f2e8
Merge remote-tracking branch 'origin/master' into 380-multi-architect…
kfriedberger Oct 27, 2024
7f19ecc
Bitwuzla: extend build-steps for Linux with x64-flag
kfriedberger Oct 27, 2024
e648ac1
Bitwuzla: prepare for arm64-build.
kfriedberger Oct 28, 2024
d689f14
Bitwuzla: update symlinks
kfriedberger Oct 28, 2024
7d3b3b6
Bitwuzla: update dependency, include libraries for x64 and arm64 on L…
kfriedberger Oct 28, 2024
e87c068
Bitwuzla and MathSAT: fix dependency location on Windows CI.
kfriedberger Oct 28, 2024
03acd1e
Bitwuzla: fix copy7paste error in script for publishing to Maven.
kfriedberger Oct 28, 2024
0f0fd2c
Bitwuzla: fix path according to documentation.
kfriedberger Oct 28, 2024
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions .appveyor.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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%
Expand All @@ -34,9 +34,9 @@ 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-mathsat\*dll lib\native\x86_64-windows\
- copy lib\java\runtime-bitwuzla\*dll lib\native\x86_64-windows\
- 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\

test_script:
- ant unit-tests
Expand Down
45 changes: 25 additions & 20 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -54,28 +54,33 @@ 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 | Linux64 | Windows64 | 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: | :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.
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, Z3, and MathSAT.
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
Expand All @@ -97,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: | |
Expand Down
12 changes: 7 additions & 5 deletions build.xml
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ This file is part of JavaSMT,
an API wrapper for a collection of SMT solvers:
https://github.com/sosy-lab/java-smt

SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>

SPDX-License-Identifier: Apache-2.0
-->
Expand Down Expand Up @@ -79,12 +79,14 @@ SPDX-License-Identifier: Apache-2.0
<!-- Main targets -->

<target name="clean" description="Clean">
<property name="bitwuzla.path" value="${user.dir}/lib/native/source/libbitwuzla"/>
<property name="jarFiles" value="${class.dir}/** ${ivy.module}-*.jar ivy-*.xml *.jar"/>
<property name="libraryFiles" value="*.so *.dll *.dylib x64/*.so x64/*.dll x64/*.dylib arm64/*.so arm64/*.dll arm64/*.dylib"/>

<delete includeEmptyDirs="true">
<fileset dir="." includes="${class.dir}/** ${ivy.module}-*.jar ivy-*.xml *.so *.dll *.dylib *.jar"/>
<fileset dir="." includes="${libraryFiles} ${jarFiles} Javadoc-z3/"/>
<fileset dir="lib/native/source/libmathsat5j" includes="*.so *.dll *.o"/>
<fileset dir="${bitwuzla.path}" includes="include/"/>
<fileset dir="${bitwuzla.path}" includes="bitwuzla_wrap.o"/>
<fileset dir="lib/native/source/libbitwuzla" includes="include/"/>
<fileset dir="lib/native/source/libbitwuzla" includes="bitwuzla_wrap.o"/>
</delete>
</target>

Expand Down
4 changes: 2 additions & 2 deletions build/build-ivy.xml
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ SPDX-License-Identifier: Apache-2.0
<target name="resolve-dependencies" depends="load-ivy, update-contrib" unless="ivy.disable">
<echo message="Downloading and installing dependencies with Ivy..."/>
<ivy:resolve conf="${ivy.configurations}" log="download-only"/>
<ivy:retrieve sync="true" overwriteMode="different" pattern="${ivy.lib.dir}/[conf]/[artifact](-[classifier]).[ext]"/>
<ivy:retrieve sync="true" overwriteMode="different" pattern="${ivy.lib.dir}/[conf]/([arch]/)[artifact](-[classifier]).[ext]"/>
</target>

<target name="report-dependencies" depends="resolve-dependencies" description="Generate dependencies report">
Expand All @@ -80,7 +80,7 @@ SPDX-License-Identifier: Apache-2.0

<target name="install-contrib" depends="load-ivy" unless="ivy.disable" description="Retrieve sources and docs for external libraries">
<ivy:resolve conf="contrib" log="download-only"/>
<ivy:retrieve sync="true" pattern="${ivy.lib.dir}-contrib/[artifact](-[classifier]).[ext]"/>
<ivy:retrieve sync="true" pattern="${ivy.lib.dir}-contrib/([arch]/)[artifact](-[classifier]).[ext]"/>
</target>

<target name="update-lib" depends="load-ivy" description="Update the version of a library to the latest one">
Expand Down
Loading