initial steps to provide multiple binaries of Z3.

Not tested, not finished, just a draft.

build/build-publish-solvers/solver-z3.xml

@@ -25,14 +25,22 @@ 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.
             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.
         </fail>
+        <fail unless="z3.pathArm64">
+            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.
+        </fail>
         <exec executable="readelf" dir="${z3.path}" outputproperty="z3.elf_details" logError="true" failonerror="true">
             <arg value="-d"/>
             <arg value="libz3.so"/>
@@ -45,14 +53,20 @@ SPDX-License-Identifier: Apache-2.0
             Please run 'patchelf --set-soname libz3.so ${z3.path}/libz3.so'.
         </fail>
         <!-- Linux64 files -->
-        <copy file="${z3.path}/libz3.so" tofile="libz3-${z3.version}.so"/>
-        <copy file="${z3.path}/libz3java.so" tofile="libz3java-${z3.version}.so"/>
+        <copy file="${z3.path}/libz3.so" tofile="libz3-x64-${z3.version}.so"/>
+        <copy file="${z3.path}/libz3java.so" tofile="libz3java-x64-${z3.version}.so"/>
+        <copy file="${z3.pathArm64}/libz3.so" tofile="libz3-arm64-${z3.version}.so"/>
+        <copy file="${z3.pathArm64}/libz3java.so" tofile="libz3java-arm64-${z3.version}.so"/>
         <!-- Windows64 files -->
-        <copy file="${z3.path}/libz3.dll" tofile="libz3-${z3.version}.dll"/>
-        <copy file="${z3.path}/libz3java.dll" tofile="libz3java-${z3.version}.dll"/>
+        <copy file="${z3.path}/libz3.dll" tofile="libz3-x64-${z3.version}.dll"/>
+        <copy file="${z3.path}/libz3java.dll" tofile="libz3java-x64-${z3.version}.dll"/>
+        <copy file="${z3.pathArm64}/libz3.dll" tofile="libz3-arm64-${z3.version}.dll"/>
+        <copy file="${z3.pathArm64}/libz3java.dll" tofile="libz3java-arm64-${z3.version}.dll"/>
         <!-- MacOS files -->
-        <copy file="${z3.path}/libz3.dylib" tofile="libz3-${z3.version}.dylib"/>
-        <copy file="${z3.path}/libz3java.dylib" tofile="libz3java-${z3.version}.dylib"/>
+        <copy file="${z3.path}/libz3.dylib" tofile="libz3-x64-${z3.version}.dylib"/>
+        <copy file="${z3.path}/libz3java.dylib" tofile="libz3java-x64-${z3.version}.dylib"/>
+        <copy file="${z3.pathArm64}/libz3.dylib" tofile="libz3-arm64-${z3.version}.dylib"/>
+        <copy file="${z3.pathArm64}/libz3java.dylib" tofile="libz3java-arm64-${z3.version}.dylib"/>
         <!-- common Java file, Java is platform independent -->
         <copy file="${z3.path}/com.microsoft.z3.jar" tofile="com.microsoft.z3-${z3.version}.jar"/>
     </target>

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:

solvers_ivy_conf/ivy_z3.xml

@@ -34,14 +34,20 @@ SPDX-License-Identifier: Apache-2.0
 
     <publications defaultconf="solver-z3">
         <!-- Linux64 files -->
-        <artifact name="libz3" conf="solver-z3-linux" type="shared-object" ext="so" />
+        <artifact name="libz3" conf="solver-z3-linux" type="shared-object" ext="so"/>
         <artifact name="libz3java" conf="solver-z3-linux" type="shared-object" ext="so"/>
+        <artifact name="libz3" conf="solver-z3-linux" e:classifier="arm64" type="shared-object" ext="so"/>
+        <artifact name="libz3java" conf="solver-z3-linux" e:classifier="arm64" type="shared-object" ext="so"/>
         <!-- Windows64 files -->
-        <artifact name="libz3" conf="solver-z3-windows" type="dll" ext="dll" />
+        <artifact name="libz3" conf="solver-z3-windows" type="dll" ext="dll"/>
         <artifact name="libz3java" conf="solver-z3-windows" type="dll" ext="dll"/>
+        <artifact name="libz3" conf="solver-z3-windows" e:classifier="arm64" type="dll" ext="dll"/>
+        <artifact name="libz3java" conf="solver-z3-windows" e:classifier="arm64" type="dll" ext="dll"/>
         <!-- MacOS files -->
-        <artifact name="libz3" conf="solver-z3-os" type="dylib" ext="dylib" />
+        <artifact name="libz3" conf="solver-z3-os" type="dylib" ext="dylib"/>
         <artifact name="libz3java" conf="solver-z3-os" type="dylib" ext="dylib"/>
+        <artifact name="libz3" conf="solver-z3-os" e:classifier="arm64" type="dylib" ext="dylib"/>
+        <artifact name="libz3java" conf="solver-z3-os" e:classifier="arm64" type="dylib" ext="dylib"/>
         <!-- common Java file, Java is platform independent -->
         <artifact name="com.microsoft.z3" conf="solver-z3-common" ext="jar"/>
         <artifact name="com.microsoft.z3" conf="sources" e:classifier="sources" type="source" ext="jar"/>