Bitwuzla: add ant-steps for building a Windows-DLL

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

@@ -13,6 +13,9 @@ SPDX-License-Identifier: Apache-2.0
 <!-- vim: set tabstop=8 shiftwidth=4 expandtab sts=4 filetype=ant fdm=marker: -->
 <project name="publish-solvers-bitwuzla" basedir="." xmlns:ivy="antlib:org.apache.ivy.ant">
 
+    <property name="bitwuzla.buildForLinux" value="true"/>
+    <property name="bitwuzla.buildForWindows" value="true"/>
+
     <import file="macros.xml"/>
 
     <!-- This file is split into several parts:
@@ -30,11 +33,8 @@ SPDX-License-Identifier: Apache-2.0
     -->
 
     <target name="set-properties-for-bitwuzla">
-        <fail unless="bitwuzla.path">
-            Please specify the path to Bitwuzla with the flag -Dbitwuzla.path=/path/to/bitwuzla.
-            The path has to point to the root Bitwuzla folder, i.e.,
-            a checkout of the official git repository from 'https://github.com/bitwuzla/bitwuzla'.
-        </fail>
+        <checkPathOption pathOption="bitwuzla.path" defaultPath="/path/to/bitwuzla" targetName="Bitwuzla source folder (git checkout from 'https://github.com/bitwuzla/bitwuzla)"/>
+        <checkPathOption pathOption="jdk-windows.path" defaultPath="/path/to/jdk" targetName="JDK source folder (Windows version)"/>
         <fail unless="bitwuzla.customRev">
             Please specify a custom revision with the flag -Dbitwuzla.customRev=XXX.
             The custom revision should be a version number of Bitwuzla.
@@ -59,10 +59,20 @@ SPDX-License-Identifier: Apache-2.0
         <property name="bitwuzla.version" value="${bitwuzla.customRev}-g${bitwuzla.revision}"/>
         <property name="bitwuzla.installPath" location="${bitwuzla.path}/install"/>
         <property name="source.path" location="lib/native/source/libbitwuzla"/>
-        <property name="source.installPath" location="lib/native/source/libbitwuzla/install"/>
+        <property name="source.installPathLinux" location="${source.path}/install-linux"/>
+        <property name="source.installPathWindows" location="${source.path}/install-windows"/>
+
+        <!-- cleanup target directories, will be created and filled during the build-process -->
+        <delete dir="${source.installPathLinux}" quiet="true"/>
+        <delete dir="${source.installPathWindows}" quiet="true"/>
+        <delete dir="${source.path}/build" quiet="true"/>
+        <delete dir="${source.path}/doc" quiet="true"/>
+        <delete dir="${source.path}/install" quiet="true"/>
     </target>
 
-    <target name="build-bitwuzla-linux" depends="set-properties-for-bitwuzla">
+    <target name="compile-bitwuzla-linux" if="${bitwuzla.buildForLinux}"
+            depends="set-properties-for-bitwuzla">
+        <delete dir="${bitwuzla.installPath}" quiet="true"/>
         <echo message="Building Bitwuzla in version '${bitwuzla.version}' for Linux"/>
 
         <!-- configure and build Bitwuzla -->
@@ -77,17 +87,43 @@ SPDX-License-Identifier: Apache-2.0
         </exec>
 
         <!-- copy Bitwuzla include files to JavaSMT -->
-        <delete dir="${source.installPath}" quiet="true"/>
-        <copy todir="${source.installPath}">
+        <copy todir="${source.installPathLinux}">
             <fileset dir="${bitwuzla.installPath}"/>
         </copy>
     </target>
 
-    <target name="build-bitwuzla" depends="build-bitwuzla-linux"/>
+    <target name="compile-bitwuzla-windows" if="${bitwuzla.buildForWindows}"
+            depends="set-properties-for-bitwuzla">
+        <delete dir="${bitwuzla.installPath}" quiet="true"/>
+        <echo message="Building Bitwuzla in version '${bitwuzla.version}' for Windows"/>
+
+        <!-- configure and build Bitwuzla -->
+        <exec executable="./configure.py" dir="${bitwuzla.path}" failonerror="true">
+            <arg value="--win64"/>
+            <arg value="--static"/>
+            <arg value="--wipe"/>
+            <arg value="--prefix"/>
+            <arg value="${bitwuzla.installPath}"/>
+        </exec>
+        <exec executable="ninja" dir="${bitwuzla.path}/build/" failonerror="true">
+            <arg value="install"/>
+        </exec>
+
+        <!-- copy Bitwuzla include files to JavaSMT -->
+        <copy todir="${source.installPathWindows}">
+            <fileset dir="${bitwuzla.installPath}"/>
+        </copy>
+    </target>
 
     <!-- Run swig to generate a new wrapper. Only executed if rebuildWrapper was specified. -->
     <!-- Depends on build-bitwuzla for generating the API files. -->
-    <target name="build-wrapper" if="${bitwuzla.rebuildWrapper}" depends="build-bitwuzla">
+    <target name="build-wrapper" if="${bitwuzla.rebuildWrapper}"
+            depends="compile-bitwuzla-linux, compile-bitwuzla-windows">
+        <fail unless="bitwuzla.buildForLinux">
+            This ant-step uses the Linux dependencies for building the SWIG-wrapper.
+            The Windows dependencies are identical and would also work.
+        </fail>
+
         <!-- create output directory for the swig proxies -->
         <delete dir="${source.path}/src" quiet="true"/>
         <mkdir dir="${source.path}/src/org/sosy_lab/java_smt/solvers/bitwuzla/api"/>
@@ -96,7 +132,7 @@ SPDX-License-Identifier: Apache-2.0
         <exec executable="swig" dir="${source.path}" failonerror="true">
             <arg value="-java"/>
             <arg value="-c++"/>
-            <arg value="-Iinstall"/>
+            <arg value="-I${source.installPathLinux}"/>
             <arg value="-package"/>
             <arg value="org.sosy_lab.java_smt.solvers.bitwuzla.api"/>
             <arg value="-outdir"/>
@@ -118,65 +154,131 @@ SPDX-License-Identifier: Apache-2.0
         </exec>
     </target>
 
-    <!-- Skip rebuilding the swig header if rebuildWrapper was not specified -->
-    <target name="skip-wrapper" unless="${bitwuzla.rebuildWrapper}" depends="build-bitwuzla">
-        <echo>WARNING: Skipping the build step for the SWIG wrapper.
-        If the Bitwuzla API has changed since the last release, the wrapper should be updated.
-        Use option -Dbitwuzla.rebuildWrapper to run SWIG and automatically generate a new wrapper.</echo>
-    </target>
-
-    <target name="package-bitwuzla" depends="build-bitwuzla, build-wrapper, skip-wrapper">
-        <!-- compile java proxies and create jar file -->
-        <delete dir="${source.path}/build"/>
+    <target name="build-bitwuzla-bindings-jni"
+            depends="compile-bitwuzla-linux, compile-bitwuzla-windows, build-wrapper">
+    <!-- compile java proxies and create jar file -->
         <mkdir dir="${source.path}/build"/>
         <javac release="11" srcdir="${source.path}/src/" destdir="${source.path}/build" includeantruntime="false" failonerror="true">
             <include name="org/sosy_lab/java_smt/solvers/bitwuzla/api/*.java"/>
         </javac>
         <jar destfile="bitwuzla-${bitwuzla.version}.jar" basedir="${source.path}/build"/>
 
         <!-- generate and package javadoc documentation -->
-        <delete dir="${source.path}/doc"/>
         <mkdir dir="${source.path}/doc"/>
         <javadoc sourcepath="${source.path}/src" destdir="${source.path}/doc"/>
         <jar destfile="bitwuzla-${bitwuzla.version}-javadoc.jar" basedir="${source.path}/doc"/>
 
         <!-- package swig generated source code -->
         <jar destfile="bitwuzla-${bitwuzla.version}-sources.jar" basedir="${source.path}/src"/>
+    </target>
 
+    <target name="build-bitwuzla-bindings-linux" if="${bitwuzla.buildForLinux}"
+            depends="build-bitwuzla-bindings-jni">
         <!-- compile the swig wrapper -->
         <exec executable="g++" dir="${source.path}" failonerror="true">
             <arg value="-fPIC"/>
             <arg value="-c"/>
             <arg value="bitwuzla_wrap.cpp"/>
             <arg value="-I${source.path}/include"/>
-            <arg value="-I${bitwuzla.installPath}/include"/>
+            <arg value="-I${source.installPathLinux}/include"/>
             <arg value="-I${java.home}/include"/>
             <arg value="-I${java.home}/include/linux"/>
         </exec>
 
         <!-- link the wrapper to create libbitwuzlaJNI.so -->
+        <!-- Licensing:
+             GMP is licensed under LGPL:
+              - https://www.gnu.org/licenses/lgpl-3.0.html
+             Bitwuzla is licensed under MIT license:
+              - https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
+             Based on that information, we provide the whole library including its dependencies under the MIT license.
+        -->
         <exec executable="g++" dir="${source.path}" failonerror="true">
             <arg value="-shared"/>
             <arg value="-o"/>
             <arg value="libbitwuzlaj.so"/>
             <arg value="bitwuzla_wrap.o"/>
             <arg value="-Wl,--whole-archive"/>
-            <arg value="${bitwuzla.installPath}/lib/x86_64-linux-gnu/libbitwuzla.a"/>
-            <arg value="${bitwuzla.installPath}/lib/x86_64-linux-gnu/libbitwuzlabb.a"/>
-            <arg value="${bitwuzla.installPath}/lib/x86_64-linux-gnu/libbitwuzlabv.a"/>
-            <arg value="${bitwuzla.installPath}/lib/x86_64-linux-gnu/libbitwuzlals.a"/>
-            <arg value="${bitwuzla.installPath}/lib/x86_64-linux-gnu/libgmp.a"/>
-            <arg value="${bitwuzla.installPath}/lib/x86_64-linux-gnu/libgmpxx.a"/>
+            <arg value="${source.installPathLinux}/lib/x86_64-linux-gnu/libbitwuzla.a"/>
+            <arg value="${source.installPathLinux}/lib/x86_64-linux-gnu/libbitwuzlabb.a"/>
+            <arg value="${source.installPathLinux}/lib/x86_64-linux-gnu/libbitwuzlabv.a"/>
+            <arg value="${source.installPathLinux}/lib/x86_64-linux-gnu/libbitwuzlals.a"/>
+            <arg value="${source.installPathLinux}/lib/x86_64-linux-gnu/libgmp.a"/>
+            <arg value="${source.installPathLinux}/lib/x86_64-linux-gnu/libgmpxx.a"/>
             <arg value="-Wl,--no-whole-archive,--allow-multiple-definition"/>
             <arg value="-Wl,-z,defs"/>
         </exec>
+    </target>
 
-        <!-- copy library files into directory to be published for Ivy -->
-        <move file="${source.path}/libbitwuzlaj.so" tofile="libbitwuzlaj-${bitwuzla.version}.so" failonerror="true"/>
+    <target name="build-bitwuzla-bindings-windows" if="${bitwuzla.buildForWindows}"
+            depends="build-bitwuzla-bindings-jni">
+        <!-- compile the swig wrapper -->
+        <exec executable="x86_64-w64-mingw32-g++" dir="${source.path}" failonerror="true">
+            <arg value="-std=c++17"/>
+            <arg value="-fPIC"/>
+            <arg value="-c"/>
+            <arg value="bitwuzla_wrap.cpp"/>
+            <arg value="-I${source.path}/include"/>
+            <arg value="-I${source.installPathWindows}/include"/>
+            <arg value="-I${jdk-windows.path}/include"/>
+            <arg value="-I${jdk-windows.path}/include/win32"/>
+        </exec>
+
+        <!-- link the wrapper to create libbitwuzlaj.so -->
+        <!-- Note:
+             libwinpthread is required when using mingw-posix-threads.
+             We do not want to install mingw or cygwin on the target-system.
+        -->
+        <!-- Licensing:
+             GCC-based libgcc and libstd++ is licensed under GPL,
+             with an explicit allowance for combining with non-GPL-libraries:
+              - https://www.gnu.org/licenses/gcc-exception-3.1-faq.en.html
+              - https://gcc.gnu.org/onlinedocs/libstdc++/manual/license.html
+             Winpthreads is licensed under MIT:
+              - https://sourceforge.net/p/mingw-w64/mingw-w64/ci/master/tree/mingw-w64-libraries/winpthreads/COPYING
+             GMP is licensed under LGPL:
+              - https://www.gnu.org/licenses/lgpl-3.0.html
+             Bitwuzla is licensed under MIT license:
+              - https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
+             Based on that information, we provide the whole library including its dependencies under the MIT license.
+        -->
+        <exec executable="x86_64-w64-mingw32-g++" dir="${source.path}" failonerror="true">
+            <arg value="-std=c++17"/>
+            <arg value="-shared"/>
+            <arg value="-o"/>
+            <arg value="libbitwuzlaj.dll"/>
+            <arg value="bitwuzla_wrap.o"/>
+            <arg value="-Wl,--whole-archive"/>
+            <arg value="/usr/x86_64-w64-mingw32/lib/libwinpthread.a"/>
+            <arg value="${source.installPathWindows}/lib/libgmp.a"/>
+            <arg value="${source.installPathWindows}/lib/libgmpxx.a"/>
+            <arg value="${source.installPathWindows}/lib/libbitwuzlabb.a"/>
+            <arg value="${source.installPathWindows}/lib/libbitwuzlabv.a"/>
+            <arg value="${source.installPathWindows}/lib/libbitwuzlals.a"/>
+            <arg value="${source.installPathWindows}/lib/libbitwuzla.a"/>
+            <arg value="-Wl,--no-whole-archive"/>
+            <arg value="-static-libgcc"/>
+            <arg value="-static-libstdc++"/>
+            <arg value="-lpsapi"/>
+            <arg value="-Wl,--allow-multiple-definition"/>
+        </exec>
+    </target>
+
+    <target name="build-bitwuzla-linux" if="${bitwuzla.buildForLinux}"
+            depends="compile-bitwuzla-linux, build-wrapper, build-bitwuzla-bindings-linux">
     </target>
 
-    <target name="publish-bitwuzla" depends="package-bitwuzla, load-ivy"
+    <target name="build-bitwuzla-windows" if="${bitwuzla.buildForWindows}"
+            depends="compile-bitwuzla-windows, build-wrapper, build-bitwuzla-bindings-windows">
+    </target>
+
+    <target name="publish-bitwuzla"
+            depends="build-bitwuzla-linux, build-bitwuzla-windows, load-ivy"
             description="Publish Bitwuzla binaries to Ivy repository.">
+        <!-- copy library files into directory to be published for Ivy -->
+        <move file="${source.path}/libbitwuzlaj.so" tofile="libbitwuzlaj-${bitwuzla.version}.so" failonerror="true"/>
+        <move file="${source.path}/libbitwuzlaj.dll" tofile="libbitwuzlaj-${bitwuzla.version}.dll" failonerror="true"/>
+
         <ivy:resolve conf="solver-bitwuzla" file="solvers_ivy_conf/ivy_bitwuzla.xml"/>
         <publishToRepository solverName="Bitwuzla" solverVersion="${bitwuzla.version}"/>
     </target>

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

@@ -164,14 +164,19 @@ in which the following command can be run.
 To publish Bitwuzla, checkout the [Bitwuzla repository](https://github.com/bitwuzla/bitwuzla).
 Then execute the following command in the JavaSMT directory:
 ```
-ant publish-bitwuzla -Dbitwuzla.path=$BITWUZLA_DIR -Dbitwuzla.customRev=$VERSION -Dbitwuzla.rebuildWrapper=$BOOL
+ant publish-bitwuzla \
+    -Dbitwuzla.path=$BITWUZLA_DIR -Dbitwuzla.customRev=$VERSION \
+    -Dbitwuzla.rebuildWrapper=$BOOL -Djdk-windows.path=$JNI_DIR
 ```
 Example:
 ```
-ant publish-bitwuzla -Dbitwuzla.path=../bitwuzla/ -Dbitwuzla.customRev=0.4.0 -Dbitwuzla.rebuildWrapper=false
+ant publish-bitwuzla \
+    -Dbitwuzla.path=../bitwuzla/ -Dbitwuzla.customRev=0.4.0 \
+    -Dbitwuzla.rebuildWrapper=false -Djdk-windows.path=/dependencies/jdk-11/
 ```
 The build-scripts Bitwuzla will download and build necessary dependencies like GMP automatically.
 Our build script will automatically append the git-revision of Bitwuzla, if available.
+The build-steps will produce a Linux and a Windows library and publish them.
 
 Finally, follow the instructions shown in the message at the end.
 The instructions for publication via SVN into the Ivy repository are not intended to be executed in the Docker environment,

docker/ubuntu2204.Dockerfile

@@ -20,7 +20,7 @@ ENV LANGUAGE en_US.UTF-8
 # Install basic packages for building several solvers
 RUN apt-get update \
  && apt-get install -y \
-        wget curl git build-essential cmake patchelf \
+        wget curl git build-essential cmake patchelf unzip \
         openjdk-11-jdk ant maven \
         gcc-mingw-w64-x86-64-posix g++-mingw-w64-x86-64-posix \
         zlib1g-dev m4 \
@@ -63,17 +63,21 @@ RUN wget http://prdownloads.sourceforge.net/swig/swig-4.1.1.tar.gz \
  && ./configure \
  && make -j4 \
  && make install \
- && cd -- \
- && rm -rf swig-4.1.1.tar.gz swig-4.1.1
+ && rm -rf swig-4.1.1.tar.gz swig-4.1.1 \
+ && cd --
 
 RUN wget https://gmplib.org/download/gmp/gmp-6.2.1.tar.lz \
  && tar xf gmp-6.2.1.tar.lz \
  && cd gmp-6.2.1 \
  && ./configure --enable-cxx --with-pic --disable-shared --enable-fat \
  && make -j4 \
  && make install \
- && cd -- \
- && rm -rf gmp-6.2.1.tar.lz gmp-6.2.1
+ && rm -rf gmp-6.2.1.tar.lz gmp-6.2.1 \
+ && cd --
+
+RUN wget https://download.java.net/openjdk/jdk11/ri/openjdk-11+28_windows-x64_bin.zip \
+ && unzip openjdk-11+28_windows-x64_bin.zip \
+ && rm openjdk-11+28_windows-x64_bin.zip
 
 # Add the user "developer" with UID:1000, GID:1000, home at /developer.
 # This allows to map the docker-internal user to the local user 1000:1000 outside of the container.

solvers_ivy_conf/ivy_bitwuzla.xml

@@ -24,17 +24,17 @@ SPDX-License-Identifier: Apache-2.0
 
     <configurations>
         <!-- TODO: Add windows support -->
-        <conf name="solver-bitwuzla" />
-        <conf name="solver-bitwuzla" extends="solver-bitwuzla-linux"/>
+        <conf name="solver-bitwuzla" extends="solver-bitwuzla-linux, solver-bitwuzla-windows"/>
         <conf name="solver-bitwuzla-linux" extends="solver-bitwuzla-common"/>
+        <conf name="solver-bitwuzla-windows" extends="solver-bitwuzla-common"/>
         <conf name="solver-bitwuzla-common" visibility="private"/>
         <conf name="sources"/>
         <conf name="javadoc"/>
     </configurations>
 
     <publications defaultconf="solver-bitwuzla">
-        <!-- Linux native libraries -->
-        <artifact name="libbitwuzlaj" conf="solver-bitwuzla" type="shared-object" ext="so"/>
+        <artifact name="libbitwuzlaj" conf="solver-bitwuzla-linux" type="shared-object" ext="so"/>
+        <artifact name="libbitwuzlaj" conf="solver-bitwuzla-windows" type="shared-object" ext="dll"/>
         <!-- Java code, docs and source -->
         <artifact name="bitwuzla" conf="solver-bitwuzla-common" ext="jar"/>
         <artifact name="bitwuzla" conf="sources" e:classifier="sources" type="source" ext="jar"/>