Merge pull request #202 from sosy-lab/windows-support

Add Windows Support for some Solvers (MathSAT5 and Z3).
sosy-lab · Nov 9, 2020 · f2dc9fd · f2dc9fd
2 parents 87a9e58 + 0f04600
commit f2dc9fd
Show file tree

Hide file tree

Showing 17 changed files with 426 additions and 140 deletions.
diff --git a/.appveyor.yml b/.appveyor.yml
@@ -22,15 +22,20 @@ install:
         )
         [System.IO.Compression.ZipFile]::ExtractToDirectory("C:\ant-bin.zip", "C:\ant")
       }
-  - cmd: SET JAVA_HOME=C:\Program Files\Java\jdk14
-  - cmd: SET PATH=C:\ant\apache-ant-1.10.8\bin;%JAVA_HOME%\bin;%PATH%
-  - cmd: SET IVY_CACHE_DIR=C:\ivy
-  - cmd: echo %USERPROFILE%
-  - cmd: echo %PATH%
-  - cmd: java -version
+  - SET JAVA_HOME=C:\Program Files\Java\jdk14
+  - SET PATH=C:\ant\apache-ant-1.10.8\bin;%JAVA_HOME%\bin;%PATH%
+  - SET IVY_CACHE_DIR=C:\ivy
+  - echo %USERPROFILE%
+  - echo %PATH%
+  - java -version
 
 build_script:
   - ant build
+  # Windows does not allow symlinks, thus we need to copy native solver binaries
+  # to make it available for JUnit tests.
+  # See lib\native\x86_64-windows\README.md for details.
+  - copy lib\java\runtime-z3\*dll lib\native\x86_64-windows\
+  - copy lib\java\runtime-mathsat\*dll lib\native\x86_64-windows\
 
 test_script:
   - ant unit-tests

diff --git a/.gitignore b/.gitignore
@@ -42,6 +42,7 @@ lib/native/source/*/*.o
 .idea/uiDesigner.xml
 
 /*.so
+/*.dll
 /*.jar
 
 build.properties

diff --git a/build.xml b/build.xml
@@ -78,7 +78,8 @@ SPDX-License-Identifier: Apache-2.0
 
     <target name="clean" description="Clean">
         <delete includeEmptyDirs="true">
-            <fileset dir="." includes="${class.dir}/** ${ivy.module}-*.jar ivy-*.xml *.so *.jar"/>
+            <fileset dir="." includes="${class.dir}/** ${ivy.module}-*.jar ivy-*.xml *.so *.dll *.dylib *.jar"/>
+            <fileset dir="lib/native/source/libmathsat5j" includes="*.so *.dll *.o"/>
         </delete>
     </target>
 

diff --git a/build/build-publish-solvers.xml b/build/build-publish-solvers.xml
@@ -21,9 +21,12 @@ SPDX-License-Identifier: Apache-2.0
         description="Copy Z3 binaries to the root folder along with the version postfix.
             This package provides the JNI for direct usage.">
         <fail unless="z3.path">
-            Please specify the path to Z3 with the flag -Dz3.path=/path/to/z3.
-            The path has to point to the root Z3 folder.
+            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,
+            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"/>
@@ -36,18 +39,30 @@ 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-${z3.version}.so"/>
         <copy file="${z3.path}/libz3java.so" tofile="libz3java-${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"/>
+        <!-- MacOS files -->
+        <copy file="${z3.path}/libz3.dylib" tofile="libz3-${z3.version}.dylib"/>
+        <copy file="${z3.path}/libz3java.dylib" tofile="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>
 
     <target name="get-z3-version" unless="z3.version">
         <fail unless="z3.path">
-            Please specify the path to Z3 with the flag -Dz3.path=/path/to/z3.
-            The path has to point to the root Z3 folder.
+            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,
+            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="git" dir="${z3.path}" outputproperty="z3.version">
+        <echo>Option -Dz3.version=... not specified. Trying to determine z3.version from git repository. This will crash if git repository is not available.</echo>
+        <exec executable="git" dir="${z3.path}" outputproperty="z3.version" failonerror="true">
             <arg value="describe" />
         </exec>
     </target>
@@ -267,94 +282,116 @@ SPDX-License-Identifier: Apache-2.0
     <!-- SECTION: Publishing [Opti-]MathSAT {{{1
          ===============================================================
     -->
-    <target name="compile-mathsat-bindings"
-        description="Compile MathSAT bindings">
-        <compile-mathsatlike-bindings flag="mathsat"/>
+    <target name="compile-mathsat-bindings-linux"
+        description="Compile MathSAT bindings for Linux">
+        <compile-mathsatlike-bindings-linux flag="mathsat"/>
     </target>
 
-    <target name="compile-optimathsat-bindings"
-        description="Compile OptiMathSAT bindings">
-        <compile-mathsatlike-bindings flag="optimathsat"/>
+    <target name="compile-mathsat-bindings-windows"
+        description="Compile MathSAT bindings for Windows">
+        <compile-mathsatlike-bindings-windows flag="mathsat"/>
     </target>
 
-    <target name="publish-mathsat" depends="compile-mathsat-bindings, load-ivy"
-        description="Publish OptiMathSAT binaries to Ivy repo.">
-
-        <publish-mathsatlike flag="mathsat" />
-    </target>
-
-    <target name="publish-optimathsat" depends="compile-optimathsat-bindings, load-ivy"
-        description="Publish OptiMathSAT binaries to Ivy repo.">
-
-        <publish-mathsatlike flag="optimathsat" />
+    <target name="compile-optimathsat-bindings"
+        description="Compile OptiMathSAT bindings">
+        <compile-mathsatlike-bindings-linux flag="optimathsat"/>
     </target>
 
-    <macrodef name="compile-mathsatlike-bindings">
-       <attribute name="flag"/>
+    <macrodef name="compile-mathsatlike-bindings-linux">
+       <attribute name="flag" default="mathsat"/>
        <sequential>
-           <fail unless="mathsat.path">
-               Please specify the path to the Mathsat5 source folder with the flag -Dmathsat.path=/path/to/mathsat.
-               The path has to point to the root Mathsat5 folder.
-               Note that shell substitutions do not work and a full absolute
-               path has to be specified.
-           </fail>
-
-           <exec executable="lib/native/source/libmathsat5j/compile.sh">
+            <checkPathOption pathOption="mathsat.path" defaultPath="/path/to/mathsat" targetName="Mathsat5 source folder (Linux version)"/>
+            <checkPathOption pathOption="gmp.path" defaultPath="/path/to/gmp" targetName="GMP source folder (Linux version)"/>
+           <exec executable="lib/native/source/libmathsat5j/compile.sh" failonerror="true">
                <arg value="${mathsat.path}" />
                <arg value="${gmp.path}" />
                <arg value="-@{flag}" />
            </exec>
-
        </sequential>
     </macrodef>
 
-    <macrodef name="publish-mathsatlike">
-        <attribute name="flag" default="mathsat"/>
-
+    <macrodef name="compile-mathsatlike-bindings-windows">
+        <attribute name="flag" default="mathsat"/> <!-- unused, OptiMathSAT not yet build for Windows -->
         <sequential>
-            <fail unless="mathsat.version">
-                Please specify the @{flag} version with the flag -Dmathsat.version=... .
-            </fail>
+            <checkPathOption pathOption="mathsat-windows.path" defaultPath="/path/to/mathsat" targetName="Mathsat5 source folder (Windows version)"/>
+            <checkPathOption pathOption="mpir-windows.path" defaultPath="/path/to/mpir" targetName="MPIR source folder (Windows version)"/>
+            <checkPathOption pathOption="jdk-windows.path" defaultPath="/path/to/jdk" targetName="JDK source folder (Windows version)"/>
+            <exec executable="lib/native/source/libmathsat5j/compileForWindows.sh" failonerror="true">
+                <arg value="${mathsat-windows.path}" />
+                <arg value="${mpir-windows.path}" />
+                <arg value="${jdk-windows.path}" />
+            </exec>
+        </sequential>
+    </macrodef>
 
-            <copy file="lib/native/source/libmathsat5j/lib@{flag}5j.so" tofile="lib@{flag}5j-${mathsat.version}.so"/>
+    <target name="publish-mathsat" depends="compile-mathsat-bindings-linux, compile-mathsat-bindings-windows, load-ivy"
+        description="Publish MathSAT binaries to Ivy repo.">
+        <fail unless="mathsat.version">
+            Please specify the MathSAT5 version with the flag -Dmathsat.version=... .
+        </fail>
+        <fail unless="mathsat.version">
+            Please specify the mathsat version with the flag -Dmathsat.version=... .
+        </fail>
 
-            <ivy:resolve conf="solver-@{flag}" file="solvers_ivy_conf/ivy_@{flag}.xml" />
-            <available property="ivy.hasrepository" file="repository/${ivy.organisation}/${ivy.module}" />
-            <fail unless="ivy.hasrepository"
-                message="Cannot publish without 'repository' dir, please run 'svn co https://svn.sosy-lab.org/software/ivy/repository/${ivy.organisation}/${ivy.module} repository/${ivy.organisation}/${ivy.module}'." />
+        <copy file="lib/native/source/libmathsat5j/libmathsat5j.so" tofile="libmathsat5j-${mathsat.version}.so"/>
+        <copy file="lib/native/source/libmathsat5j/mathsat5j.dll" tofile="mathsat5j-${mathsat.version}.dll"/>
+        <copy file="${mathsat-windows.path}/lib/mathsat.dll" tofile="mathsat-${mathsat.version}.dll"/>
+        <copy file="${mathsat-windows.path}/bin/mpir.dll" tofile="mpir-${mathsat.version}.dll"/>
 
-            <ivy:publish
-                pubrevision="${mathsat.version}"
-                resolver="Sosy-Lab-Publish"
-                artifactspattern="[artifact]-[revision].[ext]"
-                status="release"
-                />
-            <echo>
-                You now want to run
-                svn add repository/${ivy.organisation}/${ivy.module}/*-${mathsat.version}*
-                svn ci repository/${ivy.organisation}/${ivy.module} -m"publish version ${mathsat.version} of @{flag} Solver"
-                to make the new version publicly available.</echo>
-        </sequential>
-    </macrodef>
+        <ivy:resolve conf="solver-mathsat" file="solvers_ivy_conf/ivy_mathsat.xml" />
+        <available property="ivy.hasrepository" file="repository/${ivy.organisation}/${ivy.module}" />
+        <fail unless="ivy.hasrepository"
+            message="Cannot publish without 'repository' dir, please run 'svn co https://svn.sosy-lab.org/software/ivy/repository/${ivy.organisation}/${ivy.module} repository/${ivy.organisation}/${ivy.module}'." />
+
+        <ivy:publish
+            pubrevision="${mathsat.version}"
+            resolver="Sosy-Lab-Publish"
+            artifactspattern="[artifact]-[revision].[ext]"
+            status="release"
+            />
+        <echo>
+            You now want to run
+            svn add repository/${ivy.organisation}/${ivy.module}/*-${mathsat.version}*
+            svn ci repository/${ivy.organisation}/${ivy.module} -m"publish version ${mathsat.version} of mathsat Solver"
+            to make the new version publicly available.</echo>
+    </target>
+
+    <target name="publish-optimathsat" depends="compile-optimathsat-bindings, load-ivy"
+        description="Publish OptiMathSAT binaries to Ivy repo.">
+        <fail unless="mathsat.version">
+            Please specify the @{flag} version with the flag -Dmathsat.version=... .
+        </fail>
+
+        <copy file="lib/native/source/libmathsat5j/liboptimathsat5j.so" tofile="liboptimathsat5j-${mathsat.version}.so"/>
+
+        <ivy:resolve conf="solver-optimathsat" file="solvers_ivy_conf/ivy_optimathsat.xml" />
+        <available property="ivy.hasrepository" file="repository/${ivy.organisation}/${ivy.module}" />
+        <fail unless="ivy.hasrepository"
+            message="Cannot publish without 'repository' dir, please run 'svn co https://svn.sosy-lab.org/software/ivy/repository/${ivy.organisation}/${ivy.module} repository/${ivy.organisation}/${ivy.module}'." />
+
+        <ivy:publish
+            pubrevision="${mathsat.version}"
+            resolver="Sosy-Lab-Publish"
+            artifactspattern="[artifact]-[revision].[ext]"
+            status="release"
+            />
+        <echo>
+            You now want to run
+            svn add repository/${ivy.organisation}/${ivy.module}/*-${mathsat.version}*
+            svn ci repository/${ivy.organisation}/${ivy.module} -m"publish version ${mathsat.version} of optimathsat Solver"
+            to make the new version publicly available.</echo>
+    </target>
     <!-- }}} -->
+
     <!-- SECTION: Publishing Yices2 {{{1
          ===============================================================
     -->
     <target name="compile-yices2-bindings"
         description="Compile Yices2 bindings">
         <sequential>
-           <fail unless="yices2.path">
-               Please specify the path to the Yices2 source folder with the flag -Dyices2.path=/path/to/yices2.
-               The path has to point to the root Yices2 folder.
-           </fail>
-           <fail unless="gmp.path">
-               Please specify the path to the GMP source folder with the flag -Dgmp.path=/path/to/gmp.
-               The path has to point to the root GMP folder.
-           </fail>
-           <fail unless="gperf.path">
-               Please specify the path to the GPERF source folder with the flag -Dgperf.path=/path/to/gperf.
-               The path has to point to the root GPERF folder.
-           </fail>
+            <checkPathOption pathOption="yices2.path" defaultPath="/path/to/yices2" targetName="Yices2 source folder"/>
+            <checkPathOption pathOption="gmp.path" defaultPath="/path/to/gmp" targetName="GMP source folder"/>
+            <checkPathOption pathOption="gperf.path" defaultPath="/path/to/gperf" targetName="GPERF source folder"/>
            <exec executable="lib/native/source/yices2j/compile.sh">
                <arg value="${yices2.path}" />
                <arg value="${gmp.path}" />
@@ -418,4 +455,18 @@ SPDX-License-Identifier: Apache-2.0
         </sequential>
     </target>
     <!-- }}} -->
+
+    <macrodef name="checkPathOption">
+        <attribute name="pathOption"/>
+        <attribute name="defaultPath"/>
+        <attribute name="targetName"/>
+        <sequential>
+            <fail unless="@{pathOption}">-
+    Please specify the path to the @{targetName} with the following flag:
+        -D@{pathOption}=@{defaultPath}
+    The path has to point to the root of the @{targetName}.
+    Note that shell substitutions do not work and a full absolute path is preferred.
+            </fail>
+        </sequential>
+    </macrodef>
 </project>
diff --git a/doc/Developers.md b/doc/Developers.md
@@ -121,8 +121,9 @@ This is one of the most critical steps in JavaSMT development.
 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 14.04** binary for the [latest release](https://github.com/Z3Prover/z3/releases)
-and unzip it.
+To publish Z3, download the **Ubuntu 16.04**, **Windows**, and **OSX** binary for the
+[latest release](https://github.com/Z3Prover/z3/releases) and unzip them.
+For simpler handling, we copy the files from their `bin` directories together into one directory.
 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:
@@ -131,19 +132,13 @@ ant publish-z3 -Dz3.path=$Z3_DIR/bin -Dz3.version=$Z3_VERSION
 ```
 Finally follow the instructions shown in the message at the end.
 
-As long as [PR #1650](https://github.com/Z3Prover/z3/pull/1650) is not merged,
-you need to run the following command before running ant:
-```
-patchelf --set-soname libz3.so libz3.so
-```
-
 To publish Z3 from source, [download it](https://github.com/Z3Prover/z3) and build
-it with the following command in its directory on a 64bit Ubuntu 14.04 system
-(building on Ubuntu 16.04 introduces unwanted dependencies to new libstdc++ and libgomp versions):
-
+it with the following command in its directory on a 64bit Ubuntu 16.04 system:
 ```
 ./configure --staticlib --java --git-describe && cd build && make -j 2
 ```
+(Note that additional binaries for other operating systems need to be provided, too.
+This step is currently not fully tested from our side.)
 Then execute the following command in the JavaSMT directory, where `$Z3_DIR` is the absolute path of the Z3 directory:
 ```
 ant publish-z3 -Dz3.path=$Z3_DIR/build
@@ -189,18 +184,39 @@ Finally follow the instructions shown in the message at the end.
 
 ### Publishing (Opti)-MathSAT5
 
-For publishing MathSAT5, you need to use a machine with at least GCC 4.9.
-First, [download the (reentrant!) binary release](http://mathsat.fbk.eu/download.html), unpack it,
-and then execute the following command in the JavaSMT directory,
-where `$MATHSAT_PATH` is the path to the MathSAT directory,
+We publish MathSAT for both Linux and Windows systems at once.
+The build process can fully be done on a Linux system.
+
+For publishing MathSAT5, you need to use a Linux machine with at least GCC 7.5.0 and x86_64-w64-mingw32-gcc 7.3.
+First, [download the (reentrant!) Linux and Windows64 binary release](http://mathsat.fbk.eu/download.html) in the same version, unpack them,
+then provide the necessary dependencies (GMP for Linux and MPIR/JDK for Windows) as described in the compilation scripts.
+(see `lib/native/source/libmathsat5j/`), and then execute the following command in the JavaSMT directory,
+where `$MATHSAT_PATH_LINUX` and `$MATHSAT_PATH_WINDOWS` are the paths to the MathSAT root directory,
 and `$MATHSAT_VERSION` is the version number of MathSAT:
-```
-ant publish-mathsat -Dmathsat.path=$MATHSAT_PATH -Dgmp.path=$GMP_PATH -Dmathsat.version=$MATHSAT_VERSION
-```
+- for direct build and publishing (all-in-one, runtime: less than 5s):
+  ```
+  ant publish-mathsat \
+      -Dmathsat.path=$MATHSAT_PATH_LINUX \
+      -Dgmp.path=$GMP_PATH \
+      -Dmathsat-windows.path=$MATHSAT_PATH_WINDOWS \
+      -Dmpir-windows.path=$MPIR_PATH \
+      -Djdk-windows.path=$JDK_11_PATH \
+      -Dmathsat.version=$MATHSAT_VERSION
+  ```
+  Concrete example (`$WD` is a working directory where all dependencies are located):
+  ```
+  ant publish-mathsat \
+      -Dmathsat.path=$WD/mathsat-5.6.4-linux-x86_64-reentrant \
+      -Dgmp.path=$WD/gmp-6.1.2 \
+      -Dmathsat-windows.path=$WD/mathsat-5.6.4-win64-msvc \
+      -Dmpir-windows.path=$WD/mpir-2.7.2-win \
+      -Djdk-windows.path=$WD/jdk-11 \
+      -Dmathsat.version=5.6.4-debug
+  ```
 Finally follow the instructions shown in the message at the end.
-The same procedure applies to [OptiMathSAT](http://optimathsat.disi.unitn.it/) solver,
-except the publishing command is:
 
+A similar procedure applies to [OptiMathSAT](http://optimathsat.disi.unitn.it/) solver,
+except that Windows is not yet supported and the publishing command is simpler:
 ```
 ant publish-optimathsat -Dmathsat.path=$OPTIMATHSAT_PATH -Dgmp.path=$GMP_PATH -Dmathsat.version=$OPTIMATHSAT_VERSION
 ```