CVC5: Add multi-arch support

daniel-raffler · daniel-raffler · commit 526ff577d7de · 2025-03-17T07:00:03.000+01:00
We compile for linux on x64 and arm64 and windows on x64 only. CVC5 is also available on MacOS, but there doesn't seem to be a simple way to cross compile. The same is true for windows on arm64.
diff --git a/build/build-maven-publish.xml b/build/build-maven-publish.xml
@@ -229,11 +229,15 @@ SPDX-License-Identifier: Apache-2.0
         <ivy:artifactproperty name="[artifact].revision" value="[revision]"/>
         <property name="stage.solver" value="cvc5"/>
         <property name="stage.revision" value="${cvc5.revision}"/>
+        <property name="libDir.x64" value="lib/java/runtime-cvc5/x64"/>
+        <property name="libDir.arm64" value="lib/java/runtime-cvc5/arm64"/>
         <!-- prepare the pom-file -->
         <generate-solver-pom-file/>
         <!-- then publish the files -->
         <stage-solver-file filename="cvc5" fileending="jar"/>
-        <stage-solver-file filename="libcvc5j" classifier="libcvc5j" fileending="so"/>
+        <stage-solver-file filename="libcvc5j" classifier="libcvc5j-x64" filedirectory="${libDir.x64}" fileending="so"/>
+        <stage-solver-file filename="libcvc5j" classifier="libcvc5j-arm64" filedirectory="${libDir.arm64}" fileending="so"/>
+        <stage-solver-file filename="libcvc5j" classifier="libcvc5j-x64" filedirectory="${libDir.x64}" fileending="dll"/>
     </target>
 
     <!--
diff --git a/build/build-publish-solvers/solver-cvc5.xml b/build/build-publish-solvers/solver-cvc5.xml
@@ -12,15 +12,15 @@ SPDX-License-Identifier: Apache-2.0
 
 <!-- vim: set tabstop=8 shiftwidth=4 expandtab sts=4 filetype=ant fdm=marker: -->
 <project name="publish-solvers-cvc5" basedir="." xmlns:ivy="antlib:org.apache.ivy.ant">
-
     <import file="macros.xml"/>
 
+    <property name="cvc5.distDir" value="${ivy.solver.dist.dir}/cvc5"/>
+
     <!-- Build options for CVC5, Reasoning:
           - 'production' enable optimization, disables assertions and tracing,
           - 'static' build libcvc5 and all dependencies statically,
           - 'java-bindings' build the JNI bindings,
           - 'auto-download' load all dependencies automatically,
-          - 'statistics' for the new statistics stuff,
           - 'prefix' because I don't want it to use system installed or install system-wide,
           Theoretically CVC5s performance should be improvable by using -best (uses the best
           known general performance/dependencies) but this can not be combined with auto-download.
@@ -41,6 +41,8 @@ SPDX-License-Identifier: Apache-2.0
             The custom revision has to be unique amongst the already known version
             numbers from the ivy repository. The script will append the git revision.
         </fail>
+        <checkPathOption pathOption="jdk-linux-arm64.path" defaultPath="/path/to/jdk" targetName="JDK source folder (Linux arm64 version)"/>
+        <checkPathOption pathOption="jdk-windows-x64.path" defaultPath="/path/to/jdk" targetName="JDK source folder (Windows x64 version)"/>
 
         <!-- get the short commit hash of the cvc5 version used -->
         <exec executable="git" dir="${cvc5.path}" outputproperty="cvc5.revision" failonerror="true">
@@ -51,47 +53,113 @@ SPDX-License-Identifier: Apache-2.0
         <property name="cvc5.version" value="${cvc5.customRev}-g${cvc5.revision}"/>
         <echo message="Building CVC5 in version '${cvc5.version}'"/>
 
-        <!-- build CVC5 -->
-        <echo message="Cleaning old build files"/>
-        <exec executable="rm" dir="${cvc5.path}" failonerror="true">
+        <!-- set a path to the build folder and make sure there are no previous build files -->
+        <property name="cvc5.buildDir" location="${cvc5.path}/build"/>
+        <fail message="Found `/build` directory in ${cvc5.path}. Please make sure that -Dcvc5.path points to a clean checkout of CVC5 without any build files.">
+            <condition>
+                <available file="${cvc5.buildDir}" type="dir"/>
+            </condition>
+        </fail>
+
+        <!-- build CVC5 for x64 linux -->
+        <echo message="Building CVC5 for x64 linux"/>
+        <property name="cvc5.installDir.x64-linux" location="${cvc5.path}/install/x64-linux"/>
+        <exec executable="./configure.sh" dir="${cvc5.path}" failonerror="true">
+            <arg value="production"/>
+            <arg value="--static"/>
+            <arg value="--java-bindings"/>
+            <arg value="--auto-download"/>
+            <arg value="--prefix=${cvc5.installDir.x64-linux}"/>
+        </exec>
+        <exec executable="make" dir="${cvc5.buildDir}" failonerror="true">
+            <arg value="-j4"/>
+            <arg value="install"/>
+        </exec>
+        <exec executable="rm" failonerror="true">
             <arg value="-rf"/>
-            <arg value="build"/>
+            <arg value="${cvc5.buildDir}"/>
+        </exec>
+        <exec executable="strip" dir="${cvc5.installDir.x64-linux}/lib" failonerror="true">
+            <arg value="libcvc5jni.so"/>
         </exec>
 
-        <echo message="Configuring and building CVC5 in version '${cvc5.version}'"/>
+        <!-- build CVC5 for arm64 linux -->
+        <echo message="Building CVC5 for arm64 linux"/>
+        <property name="cvc5.installDir.arm64-linux" location="${cvc5.path}/install/arm64-linux"/>
         <exec executable="./configure.sh" dir="${cvc5.path}" failonerror="true">
+            <env key="JNI_HOME" value="${jdk-linux-arm64.path}"/>
             <arg value="production"/>
+            <arg value="--arm64"/>
             <arg value="--static"/>
             <arg value="--java-bindings"/>
             <arg value="--auto-download"/>
-            <arg value="--statistics"/>
-            <arg value="--prefix=${cvc5.path}/build/install"/>
+            <arg value="--prefix=${cvc5.installDir.arm64-linux}"/>
+        </exec>
+        <exec executable="make" dir="${cvc5.buildDir}" failonerror="true">
+            <arg value="-j4"/>
+            <arg value="install"/>
+        </exec>
+        <exec executable="rm" failonerror="true">
+            <arg value="-rf"/>
+            <arg value="${cvc5.buildDir}"/>
         </exec>
-        <exec executable="make" dir="${cvc5.path}/build/" failonerror="true">
-            <arg value="-j4" />
+        <exec executable="aarch64-linux-gnu-strip" dir="${cvc5.installDir.arm64-linux}/lib" failonerror="true">
+            <arg value="libcvc5jni.so"/>
+        </exec>
+
+        <!-- build CVC5 for x64 windows -->
+        <echo message="Building CVC5 for x64 windows"/>
+        <property name="cvc5.installDir.x64-windows" location="${cvc5.path}/install/x64-windows"/>
+        <exec executable="./configure.sh" dir="${cvc5.path}" failonerror="true">
+            <env key="JNI_HOME" value="${jdk-windows-x64.path}"/>
+            <arg value="production"/>
+            <arg value="--win64"/>
+            <arg value="--static"/>
+            <arg value="--java-bindings"/>
+            <arg value="--auto-download"/>
+            <arg value="--prefix=${cvc5.installDir.x64-windows}"/>
+        </exec>
+        <exec executable="make" dir="${cvc5.buildDir}" failonerror="true">
+            <arg value="-j4"/>
+            <arg value="install"/>
+        </exec>
+        <exec executable="rm" failonerror="true">
+            <arg value="-rf"/>
+            <arg value="${cvc5.buildDir}"/>
+        </exec>
+        <exec executable="x86_64-w64-mingw32-strip" dir="${cvc5.installDir.x64-windows}/bin" failonerror="true">
+            <arg value="cvc5jni.dll"/>
         </exec>
 
         <!-- get the actual jar location as cvc5.jar is just a link -->
-        <exec executable="readlink" dir="${cvc5.path}/build/src/api/java" outputproperty="cvc5.jar" failonerror="true">
+        <exec executable="readlink" dir="${cvc5.installDir.x64-linux}/share/java" outputproperty="cvc5.jar" failonerror="true">
             <arg value="-f"/>
             <arg value="cvc5.jar"/>
         </exec>
 
         <!-- copy library files into directory to be published for IVY -->
-        <echo message="Copying artifact files into current directory"/>
-        <copy file="${cvc5.path}/build/src/api/java/libcvc5jni.so" tofile="libcvc5j-${cvc5.version}.so"/>
-        <copy file="${cvc5.jar}" tofile="cvc5-${cvc5.version}.jar"/>
-
-        <!-- remove unneeded symbols -->
-        <echo message="Strip unneeded symbols"/>
-        <exec executable="strip" dir="./" failonerror="true">
-            <arg value="libcvc5j-${cvc5.version}.so"/>
-        </exec>
+        <echo message="Copying artifact for Ivy release"/>
+        <copy file="${cvc5.jar}" tofile="${cvc5.distDir}/cvc5-${cvc5.version}.jar"/>
+        <copy file="${cvc5.installDir.x64-linux}/lib/libcvc5jni.so" tofile="${cvc5.distDir}/x64/libcvc5j-${cvc5.version}.so"/>
+        <copy file="${cvc5.installDir.arm64-linux}/lib/libcvc5jni.so" tofile="${cvc5.distDir}/arm64/libcvc5j-${cvc5.version}.so"/>
+        <copy file="${cvc5.installDir.x64-windows}/bin/cvc5jni.dll" tofile="${cvc5.distDir}/x64/libcvc5j-${cvc5.version}.dll"/>
     </target>
 
     <target name="publish-cvc5" depends="package-cvc5, load-ivy"
-        description="Publish CVC5 binaries to Ivy repository.">
-        <ivy:resolve conf="solver-cvc5" file="solvers_ivy_conf/ivy_cvc5.xml" />
-        <publishToRepository solverName="CVC5" solverVersion="${cvc5.version}"/>
+            description="Publish CVC5 binaries to Ivy repository.">
+        <ivy:resolve conf="solver-cvc5" file="solvers_ivy_conf/ivy_cvc5.xml"/>
+        <publishToRepository solverName="CVC5" solverVersion="${cvc5.version}" distDir="${cvc5.distDir}"/>
+
+        <!--
+          We additionally provide x64-files without arch-attribute for backwards compatibility,
+          such that applications can load dependencies without changing their Ivy configuration.
+          Those files are not part of any direct configuration, but will be resolved if the
+          arch-attribute is not used.
+        -->
+        <copy todir="repository/${ivy.organisation}/${ivy.module}/">
+            <fileset dir="repository/${ivy.organisation}/${ivy.module}/x64/">
+                <include name="*-${cvc5.version}.*"/>
+            </fileset>
+        </copy>
     </target>
 </project>
diff --git a/lib/ivy.xml b/lib/ivy.xml
@@ -45,7 +45,9 @@ SPDX-License-Identifier: Apache-2.0
         <conf name="runtime-z3-x64" extends="core" description="only one solver included"/>
         <conf name="runtime-z3-arm64" extends="core" description="only one solver included"/>
         <conf name="runtime-cvc4" extends="core" description="only one solver included"/>
-        <conf name="runtime-cvc5" extends="core" description="only one solver included"/>
+        <conf name="runtime-cvc5" extends="runtime-cvc5-x64,runtime-cvc5-arm64" description="only one solver included"/>
+        <conf name="runtime-cvc5-x64" extends="core" description="only one solver included"/>
+        <conf name="runtime-cvc5-arm64" extends="core" description="only one solver included"/>
         <conf name="runtime-boolector" extends="core" description="only one solver included"/>
         <conf name="runtime-yices2" extends="core" description="only one solver included"/>
         <conf name="runtime-bitwuzla" extends="runtime-bitwuzla-x64,runtime-bitwuzla-arm64" description="only one solver included"/>
@@ -66,10 +68,10 @@ SPDX-License-Identifier: Apache-2.0
 
         <!-- The normal dependencies with all solvers included, except those unter GPL. -->
         <conf name="runtime-x64-without-gpl"
-              extends="runtime-mathsat-x64,runtime-opensmt-x64,runtime-optimathsat,runtime-smtinterpol,runtime-princess,runtime-z3-x64,runtime-cvc4,runtime-cvc5,runtime-boolector,runtime-bitwuzla-x64"
+              extends="runtime-mathsat-x64,runtime-opensmt-x64,runtime-optimathsat,runtime-smtinterpol,runtime-princess,runtime-z3-x64,runtime-cvc4,runtime-cvc5-x64,runtime-boolector,runtime-bitwuzla-x64"
               description="all solvers for x64 architecture included, except those under GPL"/>
         <conf name="runtime-arm64-without-gpl"
-              extends="runtime-mathsat-arm64,runtime-opensmt-arm64,runtime-smtinterpol,runtime-princess,runtime-z3-arm64,runtime-bitwuzla-arm64"
+              extends="runtime-mathsat-arm64,runtime-opensmt-arm64,runtime-smtinterpol,runtime-princess,runtime-cvc5-arm64,runtime-z3-arm64,runtime-bitwuzla-arm64"
               description="all solvers for arm64 architecture included, except those under GPL"/>
 
         <!-- Dependencies needed for building or running tests. -->
@@ -191,7 +193,7 @@ SPDX-License-Identifier: Apache-2.0
         <dependency org="org.sosy_lab" name="javasmt-solver-opensmt" rev="2.8.0-sosy0-ge831bf23" conf="runtime-opensmt-x64->solver-opensmt-x64; runtime-opensmt-arm64->solver-opensmt-arm64; contrib->sources,javadoc"/>
         <dependency org="org.sosy_lab" name="javasmt-solver-optimathsat" rev="1.7.1-sosy0" conf="runtime-optimathsat->solver-optimathsat" />
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc4" rev="1.8-prerelease-2020-06-24-g7825d8f28" conf="runtime-cvc4->solver-cvc4" />
-        <dependency org="org.sosy_lab" name="javasmt-solver-cvc5" rev="1.2.1-gdc565d916" conf="runtime-cvc5->solver-cvc5"/>
+        <dependency org="org.sosy_lab" name="javasmt-solver-cvc5" rev="latest-g4c241968d" conf="runtime-cvc5-x64->solver-cvc5-x64; runtime-cvc5-arm64->solver-cvc5-arm64"/>
         <dependency org="org.sosy_lab" name="javasmt-solver-boolector" rev="3.2.2-g1a89c229" conf="runtime-boolector->solver-boolector" />
         <dependency org="org.sosy_lab" name="javasmt-solver-bitwuzla" rev="0.7.0-13.1-g595512ae" conf="runtime-bitwuzla-x64->solver-bitwuzla-x64; runtime-bitwuzla-arm64->solver-bitwuzla-arm64; contrib->sources,javadoc"/>
 
diff --git a/lib/native/arm64-linux/libcvc5j.so b/lib/native/arm64-linux/libcvc5j.so
@@ -0,0 +1 @@
+../../java/runtime-cvc5/arm64/libcvc5j.so
diff --git a/lib/native/x86_64-linux/libcvc5j.so b/lib/native/x86_64-linux/libcvc5j.so
@@ -1 +1 @@
-../../java/runtime-cvc5/libcvc5j.so
+../../java/runtime-cvc5/x64/libcvc5j.so
diff --git a/lib/native/x86_64-windows/README.md b/lib/native/x86_64-windows/README.md
@@ -39,6 +39,10 @@ For MathSAT5:
 For Bitwuzla:
 - mklink libbitwuzlaj.dll ..\..\java\runtime-bitwuzla\libbitwuzlaj.dll
 
+For CVC5:
+
+- mlink libcvc5j.dll ..\..\java\runtime-cvc5\x64\libcvcj.so
+
 ### With a direct copy of the library:
 
 An alternative simple solution (without the need of administrator rights) is to copy over
@@ -57,6 +61,10 @@ For MathSAT5:
 For Bitwuzla:
 - copy ..\..\java\runtime-bitwuzla\libbitwuzlaj.dll libbitwuzlaj.dll
 
+For CVC5:
+
+- copy ..\..\java\runtime-cvc5\x64\libcvc5j.dll libcvc5j.dll
+
 Or simply use a wildcard:
 - copy ..\..\java\runtime-*\*dll .\
 - copy ..\..\java\runtime-*\x64\*dll .\
diff --git a/solvers_ivy_conf/ivy_cvc5.xml b/solvers_ivy_conf/ivy_cvc5.xml
@@ -11,6 +11,7 @@ SPDX-License-Identifier: Apache-2.0
 -->
 
 <ivy-module version="2.0"
+            xmlns:e="http://ant.apache.org/ivy/extra"
             xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
             xsi:noNamespaceSchemaLocation="http://ant.apache.org/ivy/schemas/ivy.xsd">
     <info organisation="org.sosy_lab" module="javasmt-solver-cvc5">
@@ -22,12 +23,27 @@ SPDX-License-Identifier: Apache-2.0
     </info>
 
     <configurations>
-        <conf name="solver-cvc5" />
+        <!-- default config, provides only x64 for backwards-compatibility -->
+        <conf name="solver-cvc5" extends="solver-cvc5-x64"/>
+
+        <!-- main configurations -->
+        <conf name="solver-cvc5-x64" extends="solver-cvc5-linux-x64, solver-cvc5-windows-x64"/>
+        <conf name="solver-cvc5-arm64" extends="solver-cvc5-linux-arm64"/>
+
+        <!-- basic configurations -->
+        <conf name="solver-cvc5-linux-x64" extends="solver-cvc5-common"/>
+        <conf name="solver-cvc5-linux-arm64" extends="solver-cvc5-common"/>
+        <conf name="solver-cvc5-windows-x64" extends="solver-cvc5-common"/>
+
+        <conf name="solver-cvc5-common" visibility="private"/>
     </configurations>
 
     <publications defaultconf="solver-cvc5">
-        <artifact name="libcvc5j" conf="solver-cvc5" type="shared-object" ext="so"/>
-        <artifact name="cvc5" conf="solver-cvc5"/>
+        <artifact name="libcvc5j" conf="solver-cvc5-linux-x64" e:arch="x64" type="shared-object" ext="so"/>
+        <artifact name="libcvc5j" conf="solver-cvc5-linux-arm64" e:arch="arm64" type="shared-object" ext="so"/>
+        <artifact name="libcvc5j" conf="solver-cvc5-windows-x64" e:arch="x64" type="shared-object" ext="dll"/>
+        <!-- Java code -->
+        <artifact name="cvc5" conf="solver-cvc5-common" ext="jar"/>
     </publications>
 
     <dependencies></dependencies>

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1 @@`
	`1`	`+../../java/runtime-cvc5/arm64/libcvc5j.so`
Original file line number	Diff line number	Diff line change
`@@ -1 +1 @@`
`1`		`-../../java/runtime-cvc5/libcvc5j.so`
	`1`	`+../../java/runtime-cvc5/x64/libcvc5j.so`