From 2349bae553fa04837c512d79f23bb3c29ada79e1 Mon Sep 17 00:00:00 2001
From: Karlheinz Friedberger <kfriedberger@gmail.com>
Date: Tue, 17 Sep 2024 22:07:48 +0200
Subject: [PATCH] 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
     <!-- Main targets -->
 
     <target name="clean" description="Clean">
-        <property name="bitwuzla.path" value="${user.dir}/lib/native/source/libbitwuzla"/>
+        <property name="libraryFiles" value="${class.dir}/** ${ivy.module}-*.jar ivy-*.xml *.so *.dll *.dylib *.jar"/>
         <delete includeEmptyDirs="true">
-            <fileset dir="." includes="${class.dir}/** ${ivy.module}-*.jar ivy-*.xml *.so *.dll *.dylib *.jar"/>
+            <fileset dir="." includes="${libraryFiles"/>
+            <fileset dir="x64" includes="${libraryFiles"/>
+            <fileset dir="arm64" includes="${libraryFiles"/>
             <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>
 
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
     <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">
@@ -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">
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
 
 <!-- vim: set tabstop=8 shiftwidth=4 expandtab sts=4 filetype=ant fdm=marker: -->
 <project name="macros" basedir="."
-         xmlns:ivy="antlib:org.apache.ivy.ant">
+         xmlns:ivy="antlib:org.apache.ivy.ant"
+         xmlns:e="http://ant.apache.org/ivy/extra">
 
     <macrodef name="checkPathOption">
         <attribute name="pathOption"/>
@@ -38,12 +39,12 @@ SPDX-License-Identifier: Apache-2.0
             <ivy:publish
                     pubrevision="@{solverVersion}"
                     resolver="Sosy-Lab-Publish"
-                    artifactspattern="[artifact]-[revision](-[classifier]).[ext]"
+                    artifactspattern="([arch]/)[artifact]-[revision](-[classifier]).[ext]"
                     status="release"
             />
             <echo>
                 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.</echo>
         </sequential>
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.
         </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).
+            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'.
         </fail>
-        <!-- Linux64 files -->
-        <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-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"/>
+
+        <mkdir dir="x64"/>
+        <mkdir dir="arm64"/>
+        <!-- Linux files -->
+        <copy file="${z3.path}/libz3.so" tofile="x64/libz3-${z3.version}.so"/>
+        <copy file="${z3.path}/libz3java.so" tofile="x64/libz3java-${z3.version}.so"/>
+        <copy file="${z3.pathArm64}/libz3.so" tofile="arm64/libz3-${z3.version}.so"/>
+        <copy file="${z3.pathArm64}/libz3java.so" tofile="arm64/libz3java-${z3.version}.so"/>
+        <!-- Windows files -->
+        <copy file="${z3.path}/libz3.dll" tofile="x64/libz3-${z3.version}.dll"/>
+        <copy file="${z3.path}/libz3java.dll" tofile="x64/libz3java-${z3.version}.dll"/>
+        <copy file="${z3.pathArm64}/libz3.dll" tofile="arm64/libz3-${z3.version}.dll"/>
+        <copy file="${z3.pathArm64}/java/z3java.dll" tofile="arm64/libz3java-${z3.version}.dll"/>
         <!-- MacOS files -->
-        <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"/>
+        <copy file="${z3.path}/libz3.dylib" tofile="x64/libz3-${z3.version}.dylib"/>
+        <copy file="${z3.path}/libz3java.dylib" tofile="x64/libz3java-${z3.version}.dylib"/>
+        <copy file="${z3.pathArm64}/libz3.dylib" tofile="arm64/libz3-${z3.version}.dylib"/>
+        <copy file="${z3.pathArm64}/libz3java.dylib" tofile="arm64/libz3java-${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>
@@ -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
 
     <target name="publish-z3" depends="package-z3, load-ivy"
         description="Publish Z3 binaries to Ivy repo.">
-        <ivy:resolve conf="solver-z3" file="solvers_ivy_conf/ivy_z3.xml" />
+        <ivy:resolve conf="solver-z3,solver-z3-x64,solver-z3-arm64,sources,javadoc" file="solvers_ivy_conf/ivy_z3.xml"/>
         <publishToRepository solverName="Z3" solverVersion="${z3.version}"/>
     </target>
 
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
         <!-- Resolver for downloading dependencies -->
         <url name="Sosy-Lab" descriptor="required">
             <ivy pattern="${ivy.repo.url}/[organisation]/[module]/ivy-[revision].xml" />
-            <artifact pattern="${ivy.repo.url}/[organisation]/[module]/[artifact]-[revision](-[classifier]).[ext]" />
+            <artifact
+                    pattern="${ivy.repo.url}/[organisation]/[module]/([arch]/)[artifact]-[revision](-[classifier]).[ext]" />
         </url>
 
         <!-- Resolver for publishing this project -->
         <filesystem name="Sosy-Lab-Publish">
             <ivy pattern="${repo.dir}/[organisation]/[module]/ivy-[revision].xml" />
-            <artifact pattern="${repo.dir}/[organisation]/[module]/[artifact]-[revision](-[classifier]).[ext]" />
+            <artifact
+                    pattern="${repo.dir}/[organisation]/[module]/([arch]/)[artifact]-[revision](-[classifier]).[ext]" />
         </filesystem>
     </resolvers>
-    <caches defaultCacheDir="${ivy.cache.dir}"/>
+    <caches defaultCacheDir="${ivy.cache.dir}"
+            artifactPattern="[organisation]/[module]/[revision]/[type]s/([arch]/)[artifact](-[classifier]).[ext]"/>
 </ivysettings>
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
     </info>
 
     <configurations>
-        <conf name="solver-z3" extends="solver-z3-linux,solver-z3-windows,solver-z3-os"/>
-        <conf name="solver-z3-linux" extends="solver-z3-common"/>
-        <conf name="solver-z3-windows" extends="solver-z3-common"/>
-        <conf name="solver-z3-os" extends="solver-z3-common"/>
-        <conf name="solver-z3-common" visibility="private"/>
+        <!-- default config, provides only x64 for backwards-compatibility -->
+        <conf name="solver-z3" extends="solver-z3-x64"/>
+
+        <!-- public main configurations -->
+        <conf name="solver-z3-x64" extends="solver-z3-linux-x64,solver-z3-windows-x64,solver-z3-os-x64"/>
+        <conf name="solver-z3-arm64" extends="solver-z3-linux-arm64,solver-z3-windows-arm64,solver-z3-os-arm64"/>
         <conf name="sources"/>
         <conf name="javadoc"/>
+
+        <!-- private basic configurations -->
+        <conf name="solver-z3-linux-x64" extends="solver-z3-common" visibility="private"/>
+        <conf name="solver-z3-linux-arm64" extends="solver-z3-common" visibility="private"/>
+        <conf name="solver-z3-windows-x64" extends="solver-z3-common" visibility="private"/>
+        <conf name="solver-z3-windows-arm64" extends="solver-z3-common" visibility="private"/>
+        <conf name="solver-z3-os-x64" extends="solver-z3-common" visibility="private"/>
+        <conf name="solver-z3-os-arm64" extends="solver-z3-common" visibility="private"/>
+        <conf name="solver-z3-common" visibility="private"/>
     </configurations>
 
     <publications defaultconf="solver-z3">
         <!-- Linux64 files -->
-        <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"/>
+        <artifact name="libz3" conf="solver-z3-linux-x64" e:arch="x64" type="shared-object" ext="so"/>
+        <artifact name="libz3java" conf="solver-z3-linux-x64" e:arch="x64" type="shared-object" ext="so"/>
+        <artifact name="libz3" conf="solver-z3-linux-arm64" e:arch="arm64" type="shared-object" ext="so"/>
+        <artifact name="libz3java" conf="solver-z3-linux-arm64" e:arch="arm64" type="shared-object" ext="so"/>
+
         <!-- Windows64 files -->
-        <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"/>
+        <artifact name="libz3" conf="solver-z3-windows-x64" e:arch="x64" type="dll" ext="dll"/>
+        <artifact name="libz3java" conf="solver-z3-windows-x64" e:arch="x64" type="dll" ext="dll"/>
+        <artifact name="libz3" conf="solver-z3-windows-arm64" e:arch="arm64" type="dll" ext="dll"/>
+        <artifact name="libz3java" conf="solver-z3-windows-arm64" e:arch="arm64" type="dll" ext="dll"/>
+
         <!-- MacOS files -->
-        <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"/>
+        <artifact name="libz3" conf="solver-z3-os-x64" e:arch="x64" type="dylib" ext="dylib"/>
+        <artifact name="libz3java" conf="solver-z3-os-x64" e:arch="x64" type="dylib" ext="dylib"/>
+        <artifact name="libz3" conf="solver-z3-os-arm64" e:arch="arm64" type="dylib" ext="dylib"/>
+        <artifact name="libz3java" conf="solver-z3-os-arm64" e:arch="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"/>