Merge pull request #639 from sosy-lab/638-include-javadocsources-for-all-solvers

Add JavaDoc and sources for JavaSMT and all solvers

Author: kfriedberger

build/build-documentation.xml

@@ -60,7 +60,7 @@ SPDX-License-Identifier: Apache-2.0
                 <exclude name="**/*Test.java"/>
                 <exclude name="${documentation.javadoc.exclude}"/>
             </fileset>
-            <link href="https://docs.oracle.com/en/java/javase/11/docs/api/"/>
+            <link href="https://docs.oracle.com/en/java/javase/17/docs/api/"/>
             <link href="https://guava.dev/releases/snapshot/api/docs/"/>
             <link href="https://truth.dev/api/latest/"/>
             <link href="https://sosy-lab.github.io/java-common-lib/api/"/>

build/build-publish-solvers/build-documentation-yices2.xml

@@ -0,0 +1,45 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
+
+<project name="documentation-yices2" basedir=".">
+    <!-- Targets for building documentation for the Yices2 bindings. -->
+    <property name="yices.javadoc" value="downloads/javadoc/javasmt-yices"/>
+
+    <target name="javadoc-yices2" depends="build-project">
+        <delete dir="yices.javadoc"/>
+        <javadoc destdir="${yices.javadoc}"
+                 classpathref="classpath"
+                 locale="en_US"
+                 encoding="utf-8"
+                 windowtitle="${ant.project.name}"
+                 failonerror="true"
+                 failonwarning="true">
+            <fileset dir="${source.dir}/org/sosy_lab/java_smt/solvers/yices2">
+                <include name="**/*.java"/>
+                <exclude name="**/*Test.java"/>
+            </fileset>
+            <link href="https://docs.oracle.com/en/java/javase/17/docs/api/"/>
+            <link href="https://guava.dev/releases/snapshot/api/docs/"/>
+            <link href="https://sosy-lab.github.io/java-common-lib/api/"/>
+            <link href="https://sosy-lab.github.io/java-smt/api/"/>
+            <arg line="${javadoc.doclint}"/>
+        </javadoc>
+    </target>
+
+    <target name="javadoc-jar-yices2" depends="javadoc-yices2,determine-version,build" description="Pack Javadoc into a JAR">
+        <property name="javadoc-jar.file" value="javasmt-yices2-${version}-javadoc.jar"/>
+        <jar jarfile="${javadoc-jar.file}">
+            <metainf dir="." includes="LICENSE"/>
+            <fileset dir="${yices.javadoc}"/>
+        </jar>
+    </target>
+</project>

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

@@ -106,7 +106,7 @@ SPDX-License-Identifier: Apache-2.0
 
         <!-- Compile java proxies and create jar file -->
         <mkdir dir="${bitwuzla.path}/install/java/build"/>
-        <javac release="11" debug="true" srcdir="${source.path}/libbitwuzla/src/" destdir="${bitwuzla.path}/install/java/build" includeantruntime="false" failonerror="true">
+        <javac release="17" debug="true" srcdir="${source.path}/libbitwuzla/src/" destdir="${bitwuzla.path}/install/java/build" includeantruntime="false" failonerror="true">
             <include name="org/sosy_lab/java_smt/solvers/bitwuzla/api/*.java"/>
         </javac>
         <jar destfile="${bitwuzla.dist.dir}/bitwuzla-${bitwuzla.version}.jar" basedir="${bitwuzla.path}/install/java/build"/>

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

@@ -5,7 +5,7 @@ This file is part of JavaSMT,
 an API wrapper for a collection of SMT solvers:
 https://github.com/sosy-lab/java-smt
 
-SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
@@ -18,16 +18,20 @@ SPDX-License-Identifier: Apache-2.0
     <property name="cvc5.downloads" value="./downloads/cvc5"/>
     <property name="cvc5.distDir" value="${ivy.solver.dist.dir}/cvc5"/>
 
-    <target name="download-cvc5">
+    <target name="init-cvc5" description="Clean up CVC5 binaries and Java bindings.">
         <fail unless="cvc5.version">
             Please specify a version with the flag -Dcvc5.version=XXX.
             The version must match one of the daily builds from https://github.com/cvc5/cvc5/releases
         </fail>
 
+        <delete dir="${cvc5.distDir}" quiet="true"/>
+
         <mkdir dir="${cvc5.downloads}"/>
         <mkdir dir="${cvc5.distDir}/x64"/>
         <mkdir dir="${cvc5.distDir}/arm64"/>
+    </target>
 
+    <target name="download-cvc5" depends="init-cvc5" description="Download CVC5 binaries and Java bindings.">
         <!-- Download binaries for Linux on x64 -->
         <get src="${cvc5.url}/cvc5-Linux-x86_64-static-${cvc5.version}.zip" dest="${cvc5.downloads}" verbose="true"/>
         <unzip src="${cvc5.downloads}/cvc5-Linux-x86_64-static-${cvc5.version}.zip" dest="${cvc5.distDir}/x64">
@@ -63,17 +67,87 @@ SPDX-License-Identifier: Apache-2.0
             <mapper type="merge" to="libcvc5jni-${cvc5.version}.dll"/>
         </unzip>
 
+        <!-- Download binaries for Windows on arm64 -->
         <get src="${cvc5.url}/cvc5-Win64-arm64-static-${cvc5.version}.zip" dest="${cvc5.downloads}" verbose="true"/>
         <unzip src="${cvc5.downloads}/cvc5-Win64-arm64-static-${cvc5.version}.zip" dest="${cvc5.distDir}/arm64">
             <patternset><include name="cvc5-Win64-arm64-static/bin/cvc5jni.dll"/></patternset>
             <mapper type="merge" to="libcvc5jni-${cvc5.version}.dll"/>
         </unzip>
 
         <!-- Download the Java bindings -->
-        <get src="${cvc5.url}/cvc5-Linux-arm64-java-api-${cvc5.version}.jar" dest="${cvc5.distDir}/cvc5-${cvc5.version}.jar" verbose="true"/>
+        <get src="${cvc5.url}/cvc5-Linux-arm64-java-api-${cvc5.version}.jar" dest="${cvc5.downloads}/cvc5-${cvc5.version}.jar" verbose="true"/>
+        <!-- Remove bundled binary -->
+        <zip destfile="${cvc5.distDir}/cvc5-${cvc5.version}.jar">
+            <zipfileset src="${cvc5.downloads}/cvc5-${cvc5.version}.jar">
+                <exclude name="cvc5-libs/**/*"/>
+            </zipfileset>
+        </zip>
+    </target>
+
+    <target name="download-cvc5-sources" depends="init-cvc5" description="Download CVC5 source code.">
+        <!-- Download the source code and get the exact version matching the downloaded binaries -->
+        <delete dir="${cvc5.downloads}/cvc5-sources" quiet="true"/>
+        <exec executable="git" dir="${cvc5.downloads}" failonerror="true">
+            <arg value="clone"/>
+            <arg value="https://github.com/cvc5/cvc5.git"/>
+            <arg value="cvc5-sources"/>
+        </exec>
+        <!-- Get the git revision from CVC5 version -->
+        <loadresource property="cvc5.gitVersion">
+            <concat>${cvc5.version}</concat>
+            <filterchain>
+                <replaceregex pattern="\d{4}-\d{2}-\d{2}-(.*)" replace="\1"/>
+            </filterchain>
+        </loadresource>
+        <!-- Checkout the matching version -->
+        <exec executable="git" dir="${cvc5.downloads}/cvc5-sources" failonerror="true">
+            <arg value="checkout"/>
+            <arg value="${cvc5.gitVersion}"/>
+        </exec>
+    </target>
+
+    <target name="package-cvc5-sources" depends="download-cvc5-sources" description="Package CVC5 source code into a JAR file.">
+        <jar destfile="${cvc5.distDir}/cvc5-${cvc5.version}-sources.jar" whenmanifestonly="fail">
+            <zipfileset dir="${cvc5.downloads}/cvc5-sources/src/api/java" includes="**/*.java"/>
+            <zipfileset dir="${cvc5.downloads}/cvc5-sources" includes="COPYING" prefix="META-INF"/>
+            <manifest>
+                <attribute name="Implementation-Title" value="cvc5"/>
+                <attribute name="Implementation-Version" value="${cvc5.version}"/>
+            </manifest>
+        </jar>
+    </target>
+
+    <target name="package-cvc5-javadoc" depends="download-cvc5-sources" description="Generate Javadoc for CVC5 Java API and package it into a JAR file.">
+        <delete dir="${cvc5.downloads}/cvc5-javadoc" quiet="true"/>
+        <javadoc destdir="${cvc5.downloads}/cvc5-javadoc"
+                 classpathref="classpath"
+                 locale="en_US"
+                 encoding="utf-8"
+                 windowtitle="cvc5"
+                 failonerror="true"
+                 failonwarning="false">
+            <fileset dir="${cvc5.downloads}/cvc5-sources/src/api/java">
+                <include name="**/*.java"/>
+            </fileset>
+            <link href="https://docs.oracle.com/en/java/javase/17/docs/api/"/>
+            <doctitle><![CDATA[<h1>cvc5</h1>]]></doctitle>
+            <tag name="api.note" description="Note:"/>
+            <arg line="${javadoc.doclint}"/>
+            <arg line="--allow-script-in-comments"/>
+            <!-- JVM inherits system language. We need to force it to use en_US instead of local language. -->
+            <arg value="-J-Duser.language=en" />
+            <arg value="-J-Duser.country=US" />
+            <arg value="-locale" /><arg value="en_US" />
+            <arg value="-docencoding" /><arg value="UTF-8" />
+            <arg value="-charset" /><arg value="UTF-8" />
+        </javadoc>
+        <jar jarfile="${cvc5.distDir}/cvc5-${cvc5.version}-javadoc.jar" whenmanifestonly="fail">
+            <zipfileset dir="${cvc5.downloads}/cvc5-sources" includes="COPYING" prefix="META-INF"/>
+            <zipfileset dir="${cvc5.downloads}/cvc5-javadoc"/>
+        </jar>
     </target>
 
-    <target name="publish-cvc5" depends="download-cvc5, load-ivy" description="Publish CVC5 binaries to Ivy repository.">
+    <target name="publish-cvc5" depends="download-cvc5, package-cvc5-sources, package-cvc5-javadoc, 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}" distDir="${cvc5.distDir}"/>
 

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

@@ -194,7 +194,7 @@ SPDX-License-Identifier: Apache-2.0
     <target name="build-opensmt-bindings-jni" depends="build-opensmt-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">
+        <javac release="17" srcdir="${source.path}/src/" destdir="${source.path}/build" debug="true" includeantruntime="false" failonerror="true">
             <include name="org/sosy_lab/java_smt/solvers/opensmt/api/*.java"/>
         </javac>
         <jar destfile="${opensmt.dist.dir}/opensmt-${opensmt.version}.jar" basedir="${source.path}/build"/>

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

@@ -256,6 +256,8 @@ SPDX-License-Identifier: Apache-2.0
             <copy file="${yices2.buildDir}/yices2_java_bindings/dist/lib/libyices2java.so" tofile="${yices2.distDir}/x64/libyices2java-${yices2.version}.so" failonerror="true"/>
             <copy file="${yices2.buildDir}/yices2_java_bindings/dist/lib/yices2java.dll" tofile="${yices2.distDir}/x64/yices2java-${yices2.version}.dll" failonerror="true"/>
             <copy file="${yices2.buildDir}/yices2_java_bindings/dist/lib/yices.jar" tofile="${yices2.distDir}/yices-${yices2.version}.jar" failonerror="true"/>
+            <copy file="${yices2.buildDir}/yices2_java_bindings/dist/lib/yices-sources.jar" tofile="${yices2.distDir}/yices-${yices2.version}-sources.jar" failonerror="true"/>
+            <copy file="${yices2.buildDir}/yices2_java_bindings/dist/lib/yices-javadoc.jar" tofile="${yices2.distDir}/yices-${yices2.version}-javadoc.jar" failonerror="true"/>
 
             <ivy:resolve conf="solver-yices2" file="solvers_ivy_conf/ivy_yices2.xml" />
 
@@ -276,7 +278,9 @@ SPDX-License-Identifier: Apache-2.0
     </target>
 
     <import file="build-jar-yices2.xml"/>
-    <target name="dist-yices2" depends="jar-yices2, sources-yices2" description="Make a distributable release with yices2 only"/>
+    <import file="build-documentation-yices2.xml"/>
+
+    <target name="dist-yices2" depends="jar-yices2, sources-yices2, javadoc-jar-yices2" description="Make a distributable release with yices2 only"/>
 
     <target name="publish-artifacts-yices2" depends="load-ivy, determine-version, dist-yices2"
          description="Publish Java bindings for Yices2 to Ivy repo.">

build/build-publish-solvers/solver-z3-legacy.xml

@@ -14,6 +14,8 @@ SPDX-License-Identifier: Apache-2.0
 <project name="publish-solvers-z3-legacy" basedir="." xmlns:ivy="antlib:org.apache.ivy.ant">
 
     <property name="z3legacy.dist.dir" value="${ivy.solver.dist.dir}/z3legacy"/>
+    <property name="z3legacy.project.name" value="Java Bindings for Z3 (4.5.0)"/>
+    <property name="z3legacy.javadoc.dir" value="downloads/javadoc/z3-legacy"/>
 
     <import file="macros.xml"/>
 
@@ -74,7 +76,7 @@ SPDX-License-Identifier: Apache-2.0
             <arg value="--java"/>
         </exec>
         <exec executable="make" dir="${z3.path}/build" failonerror="true">
-            <arg value="-j"/>
+            <arg value="-j8"/>
         </exec>
         <exec executable="make" dir="${z3.path}/build" failonerror="true">
             <arg value="install"/>
@@ -99,7 +101,7 @@ SPDX-License-Identifier: Apache-2.0
             <arg value="--java"/>
         </exec>
         <exec executable="make" dir="${z3.path}/build" failonerror="true">
-            <arg value="-j"/>
+            <arg value="-j8"/>
         </exec>
         <exec executable="make" dir="${z3.path}/build" failonerror="true">
             <arg value="install"/>
@@ -130,7 +132,54 @@ SPDX-License-Identifier: Apache-2.0
         <copy file="${z3.installPathLinuxX64}/lib/com.microsoft.z3legacy.jar" tofile="${z3legacy.dist.dir}/com.microsoft.z3legacy-${z3.legacy.version}.jar" failonerror="true"/>
     </target>
 
-    <target name="publish-z3-legacy" depends="package-z3-legacy, load-ivy"
+    <target name="prepare-z3-legacy-sources" depends="set-properties-for-z3-legacy">
+        <delete dir="${z3.path}/build"/>
+        <exec executable="python3" dir="${z3.path}" failonerror="true">
+            <arg value="scripts/mk_make.py"/>
+            <arg value="--java"/>
+        </exec>
+    </target>
+
+    <target name="package-z3-legacy-sources" depends="prepare-z3-legacy-sources">
+        <jar destfile="${z3legacy.dist.dir}/com.microsoft.z3legacy-${z3.legacy.version}-sources.jar" whenmanifestonly="fail">
+            <zipfileset dir="${z3.path}/src/api/java" includes="**/*.java"/>
+            <zipfileset dir="${z3.path}/" includes="LICENSE.txt" prefix="META-INF"/>
+            <manifest>
+                <attribute name="Implementation-Title" value="${z3legacy.project.name}"/>
+                <attribute name="Implementation-Version" value="${z3.legacy.version}"/>
+            </manifest>
+        </jar>
+    </target>
+
+    <target name="package-z3-legacy-javadoc" depends="prepare-z3-legacy-sources">
+        <delete dir="${z3legacy.javadoc.dir}" quiet="true"/>
+        <javadoc destdir="${z3legacy.javadoc.dir}"
+                 classpathref="classpath"
+                 locale="en_US"
+                 encoding="utf-8"
+                 windowtitle="${z3legacy.project.name}"
+                 failonerror="false"
+                 failonwarning="false">
+            <fileset dir="${z3.path}/src/api/java">
+                <include name="**/*.java"/>
+            </fileset>
+            <link href="https://docs.oracle.com/en/java/javase/11/docs/api/"/>
+            <doctitle><![CDATA[<h1>${z3legacy.project.name}</h1>]]></doctitle>
+            <arg line="${javadoc.doclint}"/>
+            <!-- JVM inherits system language. We need to force it to use en_US instead of local language. -->
+            <arg value="-J-Duser.language=en" />
+            <arg value="-J-Duser.country=US" />
+            <arg value="-locale" /><arg value="en_US" />
+            <arg value="-docencoding" /><arg value="UTF-8" />
+            <arg value="-charset" /><arg value="UTF-8" />
+        </javadoc>
+        <jar jarfile="${z3legacy.dist.dir}/com.microsoft.z3legacy-${z3.legacy.version}-javadoc.jar" whenmanifestonly="fail">
+            <zipfileset dir="${z3.path}/" includes="LICENSE.txt" prefix="META-INF"/>
+            <fileset dir="${z3legacy.javadoc.dir}"/>
+        </jar>
+    </target>
+
+    <target name="publish-z3-legacy" depends="package-z3-legacy, package-z3-legacy-sources, package-z3-legacy-javadoc, load-ivy"
         description="Publish Z3 legacy binaries to Ivy repo.">
         <ivy:resolve conf="solver-z3-legacy,solver-z3-legacy-x64" file="solvers_ivy_conf/ivy_z3-legacy.xml"/>
         <publishToRepository solverName="Z3-legacy" solverVersion="${z3.legacy.version}" distDir="${z3legacy.dist.dir}"/>

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

@@ -164,7 +164,6 @@ SPDX-License-Identifier: Apache-2.0
             windowtitle="${z3.project.name}"
             failonerror="false"
             failonwarning="false"
-            overview="doc/javadoc_overview.html"
             >
             <fileset dir="${z3.path}/src/api/java">
                 <include name="**/*.java"/>

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

@@ -439,40 +439,32 @@ In `solvers_ivy_conf/ivy_javasmt_yices2.xml` update the version of the `javasmt-
 dependency:
 
 ```xml
-<dependency org="org.sosy_lab" name="javasmt-solver-yices2" rev="2.8.0-prerelease" conf="runtime->solver-yices2"/>
+<dependency org="org.sosy_lab" name="javasmt-solver-yices2" rev="2.8.0-prerelease" .../>
 ```
 
 Then, in `lib/ivy.xml` start looking for the following section:
 
 ```xml
 <!-- additional JavaSMT components with Solver Binaries -->
-<dependency org="org.sosy_lab" name="javasmt-yices2" rev="5.0.1-722-g90a66d7fa" conf="runtime-yices2->runtime; contrib->sources"/>        
+<dependency org="org.sosy_lab" name="javasmt-yices2" rev="6.0.0-141-g04134287c" conf="runtime-yices2->runtime; contrib->sources,javadoc"/>        
 ```
 
-Remove the dependency and replace it with the line from `ivy_javasmt_yices2.xml`, except that
-`conf` has been changed to `runtime-yices2->solver-yices2`:
+Remove the dependency and replace it with a dependency on the solvers:
 
 ```xml
-<dependency org="org.sosy_lab" name="javasmt-solver-yices2" rev="2.8.0-prerelease" conf="runtime-yices2->solver-yices2"/>
+<dependency org="org.sosy_lab" name="javasmt-solver-yices2" rev="2.8.0-prerelease" conf="runtime-yices2->solver-yices2; contrib->sources,javadoc"/>
+<dependency org="org.sosy_lab" name="javasmt-solver-yices2" rev="2.8.0-prerelease" conf="runtime->solver-yices2; contrib->sources,javadoc"/>
 ```
 
-Then run `ant` to build the project
-
-Now go to the dependency in `ivy.xml` again and change `conf` back to `runtime->solver-yices2`:
-
-```xml
-<dependency org="org.sosy_lab" name="javasmt-solver-yices2" rev="2.8.0-prerelease" conf="runtime->solver-yices2"/>
-```
-
-Then publish the GPL components of JavaSMT:
+Then publish the Yices components of JavaSMT:
 ```shell
-ant publish-artifacts-yices2 -Dversion=yices2.8-prerelease
+ant publish-artifacts-yices2
 ```
 
 Finally, return the dependency in `ivy.xml` to its original form, but with the version updated:
 
 ```xml
-<dependency org="org.sosy_lab" name="javasmt-yices2" rev="yices2.8-prerelease" conf="runtime-yices2->runtime; contrib->sources"/>
+<dependency org="org.sosy_lab" name="javasmt-yices2" rev="yices2.8-prerelease" conf="runtime-yices2->runtime; contrib->sources,javadoc"/>
 ```
 
 Optionally, you may now publish a new version of JavaSMT: