Update CVC5 to 1.2.X

.appveyor.yml

@@ -44,6 +44,7 @@ build_script:
       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
+      Copy-Item -Path "lib\java\runtime-cvc5\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force
 
 test_script:
   - ant unit-tests

README.md

@@ -65,7 +65,7 @@ JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started.
 | [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:   |                     |  |  |                                                        |  |  |
+| [CVC5](https://cvc5.github.io/) |  :heavy_check_mark:  |  :heavy_check_mark:  |  :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 |

build/build-maven-publish.xml

@@ -229,15 +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="libcvc5" classifier="libcvc5" fileending="so"/>
-        <stage-solver-file filename="libcvc5jni" classifier="libcvc5jni" fileending="so"/>
-        <stage-solver-file filename="libcvc5parser" classifier="libcvc5parser" fileending="so"/>
-        <stage-solver-file filename="libpoly" classifier="libpoly" fileending="so"/>
-        <stage-solver-file filename="libpolyxx" classifier="libpolyxx" fileending="so"/>
+        <stage-solver-file filename="libcvc5jni" classifier="libcvc5jni-x64" filedirectory="${libDir.x64}" fileending="so"/>
+        <stage-solver-file filename="libcvc5jni" classifier="libcvc5jni-arm64" filedirectory="${libDir.arm64}" fileending="so"/>
+        <stage-solver-file filename="libcvc5jni" classifier="libcvc5jni-x64" filedirectory="${libDir.x64}" fileending="dll"/>
     </target>
 
     <!--

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

@@ -12,35 +12,28 @@ 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:
-          - 'auto-download' loads all dependencies automatically,
-          - 'statistics' for the new statistics stuff,
-          - 'prefix' because i don't want it to use system installed or install systemwide,
-          - 'fPIC' for position-independent code, required for shared libraries.
-          The full cmdline for building CVC5 is (note the double-dashes!):
-            ./configure.sh production - -java-bindings - -auto-download - -statistics - -prefix=$WORKSPACE/cvc5-main/build/install -DVAR=fPIC
-          Theoretically CVC5s performance should be improveable by using -best (uses the best
+          - '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,
+          - '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.
     -->
-    <!-- SECTION: Publishing CVC5
-         ==================================================================
-    -->
-    <target name="package-cvc5" depends="">
-        <!-- Copy CVC5 binaries to the root folder along with the version postfix. -->
-        <fail unless="cvc5.path">
-            Please specify the path to CVC5 with the flag -Dcvc5.path=/path/to/cvc5.
-            The path has to point to the root CVC5 folder, i.e.,
-            a checkout of the official git repository from 'https://github.com/cvc5/cvc5'.
-            Note that shell substitutions do not work and a full absolute path has to be specified.
-        </fail>
+    <target name="set-properties-for-cvc5">
+        <checkPathOption pathOption="cvc5.path" defaultPath="/path/to/cvc5" targetName="CVC5 directory (Git checkout from https://github.com/cvc5/cvc5)"/>
         <fail unless="cvc5.customRev">
             Please specify a custom revision with the flag -Dcvc5.customRev=XXX.
             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,96 +44,105 @@ 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">
-            <arg value="-rf"/>
-            <arg value="build"/>
-        </exec>
+        <!-- set a path to the build folder, which is cleaned before building any binary files -->
+        <property name="cvc5.buildDir" location="${cvc5.path}/build"/>
+
+        <property name="cvc5.installDir.x64-linux" location="${cvc5.path}/install/x64-linux"/>
+        <property name="cvc5.installDir.arm64-linux" location="${cvc5.path}/install/arm64-linux"/>
+        <property name="cvc5.installDir.x64-windows" location="${cvc5.path}/install/x64-windows"/>
+    </target>
 
-        <echo message="Configuring and building CVC5 in version '${cvc5.version}'"/>
+    <target name="compile-cvc5-linux-x64" depends="set-properties-for-cvc5">
+        <echo message="Building CVC5 for x64 linux"/>
+        <delete dir="${cvc5.buildDir}" quiet="true"/>
         <exec executable="./configure.sh" dir="${cvc5.path}" failonerror="true">
-            <!--<arg value="production"/>-->
+            <arg value="production"/>
+            <arg value="--static"/>
             <arg value="--java-bindings"/>
             <arg value="--auto-download"/>
-            <arg value="--statistics"/>
-            <arg value="--prefix=${cvc5.path}/build/install"/>
-            <arg value="-DVAR=fPIC"/>
+            <arg value="--prefix=${cvc5.installDir.x64-linux}"/>
         </exec>
-        <exec executable="make" dir="${cvc5.path}/build/" failonerror="true">
-            <arg value="-j4" />
+        <exec executable="make" dir="${cvc5.buildDir}" failonerror="true">
+            <arg value="-j4"/>
+            <arg value="install"/>
         </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">
-            <arg value="-f"/>
-            <arg value="cvc5.jar"/>
+        <exec executable="strip" dir="${cvc5.installDir.x64-linux}/lib" failonerror="true">
+            <arg value="libcvc5jni.so"/>
         </exec>
+    </target>
 
-        <!-- copy library files into directory to be published for IVY -->
-        <echo message="Copying artifact files into current directory"/>
-        <copy file="${cvc5.path}/build/src/libcvc5.so" tofile="libcvc5-${cvc5.version}.so"/>
-        <copy file="${cvc5.path}/build/src/parser/libcvc5parser.so" tofile="libcvc5parser-${cvc5.version}.so"/>
-        <copy file="${cvc5.path}/build/src/api/java/libcvc5jni.so" tofile="libcvc5jni-${cvc5.version}.so"/>
-        <copy file="${cvc5.jar}" tofile="cvc5-${cvc5.version}.jar"/>
-        <copy file="${cvc5.path}/build/deps/lib/libpolyxx.so" tofile="libpolyxx-${cvc5.version}.so"/>
-        <copy file="${cvc5.path}/build/deps/lib/libpoly.so" tofile="libpoly-${cvc5.version}.so"/>
-
-        <!-- remove unneeded symbols -->
-        <echo message="Strip unneeded symbols"/>
-        <exec executable="strip" dir="./" failonerror="true">
-            <arg value="libcvc5-${cvc5.version}.so"/>
-        </exec>
-        <exec executable="strip" dir="./" failonerror="true">
-            <arg value="libcvc5jni-${cvc5.version}.so"/>
-        </exec>
-        <exec executable="strip" dir="./" failonerror="true">
-            <arg value="libcvc5parser-${cvc5.version}.so"/>
+    <target name="compile-cvc5-linux-arm64" depends="set-properties-for-cvc5">
+        <echo message="Building CVC5 for arm64 linux"/>
+        <delete dir="${cvc5.buildDir}" quiet="true"/>
+        <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="--prefix=${cvc5.installDir.arm64-linux}"/>
         </exec>
-        <exec executable="strip" dir="./" failonerror="true">
-            <arg value="libpoly-${cvc5.version}.so"/>
+        <exec executable="make" dir="${cvc5.buildDir}" failonerror="true">
+            <arg value="-j4"/>
+            <arg value="install"/>
         </exec>
-        <exec executable="strip" dir="./" failonerror="true">
-            <arg value="libpolyxx-${cvc5.version}.so"/>
+        <exec executable="aarch64-linux-gnu-strip" dir="${cvc5.installDir.arm64-linux}/lib" failonerror="true">
+            <arg value="libcvc5jni.so"/>
         </exec>
+    </target>
 
-        <!-- fix RPATH and library dependencies -->
-        <echo message="Fixing library path for all artifact libraries"/>
-        <exec executable="patchelf" dir="./" failonerror="true">
-            <arg value="--set-rpath"/><arg value="$ORIGIN"/>
-            <arg value="--replace-needed"/><arg value="libpolyxx.so.0"/><arg value="libpolyxx.so"/>
-            <arg value="--replace-needed"/><arg value="libpoly.so.0"/><arg value="libpoly.so"/>
-            <arg value="libcvc5-${cvc5.version}.so"/>
-        </exec>
-        <exec executable="patchelf" dir="./" failonerror="true">
-            <arg value="--set-rpath"/><arg value="$ORIGIN"/>
-            <arg value="--replace-needed"/><arg value="libcvc5.so.1"/><arg value="libcvc5.so"/>
-            <arg value="libcvc5jni-${cvc5.version}.so"/>
-        </exec>
-        <exec executable="patchelf" dir="./" failonerror="true">
-            <arg value="--set-rpath"/><arg value="$ORIGIN"/>
-            <arg value="--replace-needed"/><arg value="libcvc5.so.1"/><arg value="libcvc5.so"/>
-            <arg value="libcvc5parser-${cvc5.version}.so"/>
+    <target name="compile-cvc5-windows-x64" depends="set-properties-for-cvc5">
+        <echo message="Building CVC5 for x64 windows"/>
+        <delete dir="${cvc5.buildDir}" quiet="true"/>
+        <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>
-        <!-- patchelf finds two dependencies and needs to be called twice for libpolyxx.so -->
-        <exec executable="patchelf" dir="./" failonerror="true">
-            <arg value="--set-rpath"/><arg value="$ORIGIN"/>
-            <arg value="--replace-needed"/><arg value="libpoly.so.0"/><arg value="libpoly.so"/>
-            <arg value="libpolyxx-${cvc5.version}.so"/>
+        <exec executable="make" dir="${cvc5.buildDir}" failonerror="true">
+            <arg value="-j4"/>
+            <arg value="install"/>
         </exec>
-        <exec executable="patchelf" dir="./" failonerror="true">
-            <arg value="--replace-needed"/><arg value="libpoly.so.0"/><arg value="libpoly.so"/>
-            <arg value="libpolyxx-${cvc5.version}.so"/>
+        <exec executable="x86_64-w64-mingw32-strip" dir="${cvc5.installDir.x64-windows}/bin" failonerror="true">
+            <arg value="cvc5jni.dll"/>
         </exec>
-        <exec executable="patchelf" dir="./" failonerror="true">
-            <arg value="--set-rpath"/><arg value="$ORIGIN"/>
-            <arg value="libpoly-${cvc5.version}.so"/>
+    </target>
+
+    <target name="package-cvc5" depends="compile-cvc5-linux-x64, compile-cvc5-linux-arm64, compile-cvc5-windows-x64">
+        <!-- get the actual jar location as cvc5.jar is just a link -->
+        <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 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/libcvc5jni-${cvc5.version}.so"/>
+        <copy file="${cvc5.installDir.arm64-linux}/lib/libcvc5jni.so" tofile="${cvc5.distDir}/arm64/libcvc5jni-${cvc5.version}.so"/>
+        <copy file="${cvc5.installDir.x64-windows}/bin/cvc5jni.dll" tofile="${cvc5.distDir}/x64/libcvc5jni-${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>

doc/Developers-How-to-Release-into-Ivy.md

@@ -114,23 +114,36 @@ ant publish-z3 -Dz3.path=$Z3_DIR/build
 ```
 Finally follow the instructions shown in the message at the end.
 
-
-### Publishing CVC5 (previously CVC4)
+### Publishing CVC5
 
 We prefer to compile our own CVC5 binaries and Java bindings.
 For simple usage, we provide a Docker definition/environment under `/docker`,
 in which the following command can be run.
 
-To publish CVC5, checkout the [CVC5 repository](https://github.com/cvc5/cvc5).
-Then execute the following command in the JavaSMT directory,
-where `$CVC5_DIR` is the path to the CVC5 directory and `$CVC5_VERSION` is the version number:
+To publish CVC5, checkout the [CVC5 repository](https://github.com/cvc5/cvc5) and download the
+JDK for windows and arm64 from Oracle. We will build bindings for several platforms and
+the JDKs are needed to cross-compile. To start building, execute the following command
+in the JavaSMT directory, where `$CVC5_DIR` is the path to the CVC5 directory and
+`$CVC5_VERSION` is the version number:
+
 ```
-ant publish-cvc5 -Dcvc5.path=$CVC5_DIR -Dcvc5.customRev=$CVC5_VERSION
+ant publish-cvc5 \
+    -Dcvc5.path=$CVC5_DIR\
+    -Dcvc5.customRev=$CVC5_VERSION \
+    -Djdk-windows.path=$JDK_DIR_WINDOWS \
+    -Djdk-linux-arm64.path=$JDK_DIR_LINUX_ARM64
 ```
+
 Example:
+
 ```
-ant publish-cvc5 -Dcvc5.path=../CVC5 -Dcvc5.customRev=1.0.1
+ant publish-cvc5 \
+    -Dcvc5.path=../CVC5 \
+    -Dcvc5.customRev=1.2.1 \
+    -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/
 ```
+
 During the build process, our script automatically appends the git-revision after the version.
 Finally, follow the instructions shown in the message at the end.
 

docker/ubuntu1804.Dockerfile

@@ -28,15 +28,15 @@ RUN apt-get update \
  && apt-get clean
 
 # Yices2 requires some dependencies
-RUN  apt-get update \
+RUN apt-get update \
  && apt-get install -y \
         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 \
+        python3 python3-venv python3-toml python3-pyparsing flex libssl-dev cmake \
  && 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 \

docker/ubuntu2204.Dockerfile

@@ -37,7 +37,7 @@ RUN  apt-get update \
 # CVC5 requires some dependencies
 RUN apt-get update \
  && apt-get install -y \
-        python3 python3-toml python3-pyparsing flex libssl-dev cmake \
+        python3 python3-venv python3-toml python3-pyparsing flex libssl-dev cmake \
  && apt-get clean
 
 # Bitwuzla requires Ninja and Meson (updated version from pip), and uses SWIG >4.0 from dependencies.