Add JavaSMT project template for Ivy/Ant

doc/Example-Ivy-Project/README.md

@@ -0,0 +1,24 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
+
+This is an example application for using JavaSMT with Ant/Ivy.
+The example application prints a table of the available SMT solvers, along with their version
+number and supported features.
+
+The project supports the following build targets:
+
+- `resolve` retrieve dependencies with Ivy
+- `compile` compile the project
+- `test` run the tests
+- `package` build a .jar
+- `run` run the program
+- `clean` clean the project
+
+Calling `ant` with no target will build and then execute the project.

doc/Example-Ivy-Project/build.xml

@@ -0,0 +1,135 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
+
+<project xmlns:ivy="antlib:org.apache.ivy.ant" name="javasmt-ivy-example" default="run">
+    <!-- Organization and module name for the project -->
+    <property name="project.organization" value="org.sosy_lab.java_smt_example"/>
+    <property name="project.module" value="${ant.project.name}"/>
+    <property name="project.jar" value="${project.module}.jar"/>
+
+    <!-- Path to the "main" function -->
+    <property name="project.main" value="org.sosy_lab.java_smt_example.SolverOverviewTable"/>
+
+    <target name="download-ivy" unless="skip.download">
+        <mkdir dir="lib"/>
+        <get src="https://repo1.maven.org/maven2/org/apache/ivy/ivy/2.5.0/ivy-2.5.0.jar"
+             dest="lib/ivy.jar" usetimestamp="true"/>
+    </target>
+
+    <target name="init-ivy" depends="download-ivy">
+        <path id="ivy.path">
+            <fileset dir="lib" includes="*.jar"/>
+        </path>
+        <taskdef resource="org/apache/ivy/ant/antlib.xml" uri="antlib:org.apache.ivy.ant" classpathref="ivy.path"/>
+        <ivy:settings file="lib/ivy-settings.xml"/>
+    </target>
+
+    <target name="resolve" depends="init-ivy" description="--> retrieve dependencies with Ivy">
+        <ivy:resolve log="download-only"/>
+        <ivy:retrieve pattern="lib/java/[conf]/([arch]/)[artifact](-[classifier]).[ext]"/>
+    </target>
+
+    <target name="copy" depends="resolve" description="--> copy solver libraries">
+        <mkdir dir="lib/native/x86_64-windows"/>
+        <copy todir="lib/native/x86_64-windows" flatten="true">
+            <fileset dir="lib/java/runtime">
+                <include name="**/*.dll"/>
+                <exclude name="arm64/*.dll"/>
+            </fileset>
+        </copy>
+        <mkdir dir="lib/native/arm64-windows"/>
+        <copy todir="lib/native/arm64-windows" flatten="true">
+            <fileset dir="lib/java/runtime">
+                <include name="arm64/*.dll"/>
+            </fileset>
+        </copy>
+        <mkdir dir="lib/native/x86_64-linux"/>
+        <copy todir="lib/native/x86_64-linux" flatten="true">
+            <fileset dir="lib/java/runtime">
+                <include name="**/*.so"/>
+                <exclude name="arm64/*.so"/>
+            </fileset>
+        </copy>
+        <mkdir dir="lib/native/arm64-linux"/>
+        <copy todir="lib/native/arm64-linux" flatten="true">
+            <fileset dir="lib/java/runtime">
+                <include name="arm64/*.so"/>
+            </fileset>
+        </copy>
+        <mkdir dir="lib/native/x86_64-macosx"/>
+        <copy todir="lib/native/x86_64-macosx" flatten="true">
+            <fileset dir="lib/java/runtime">
+                <include name="**/*.dylib"/>
+                <exclude name="arm64/*.dylib"/>
+            </fileset>
+        </copy>
+        <mkdir dir="lib/native/arm64-macosx"/>
+        <copy todir="lib/native/arm64-macosx" flatten="true">
+            <fileset dir="lib/java/runtime">
+                <include name="arm64/*.dylib"/>
+            </fileset>
+        </copy>
+    </target>
+
+    <target name="compile" depends="copy" description="--> compile the project">
+        <mkdir dir="build"/>
+        <path id="classpath.build">
+            <pathelement location="build"/>
+            <fileset dir="lib/java" includes="**/*.jar"/>
+        </path>
+        <javac srcdir="src" destdir="build" classpathref="classpath.build" includeantruntime="false"/>
+    </target>
+
+    <target name="test" depends="compile">
+        <java classpathref="classpath.build" classname="org.junit.platform.console.ConsoleLauncher" fork="true"
+              failonerror="true">
+            <arg value="execute"/>
+            <arg value="--scan-classpath"/>
+            <arg line="--reports-dir build/test-report"/>
+        </java>
+        <junitreport todir="build/test-report">
+            <fileset dir="build/test-report" includes="TEST-*.xml"/>
+            <report format="noframes" todir="build/test-report/html"/>
+        </junitreport>
+    </target>
+
+    <target name="package" depends="compile" description="--> build a .jar">
+        <manifestclasspath property="classpath.jar" jarfile="${project.jar}">
+            <classpath>
+                <fileset dir="lib/java/runtime" includes="*.jar"/>
+            </classpath>
+        </manifestclasspath>
+        <jar basedir="build"
+             destfile="${project.jar}"
+             includes="**"
+             whenmanifestonly="fail">
+            <manifest>
+                <attribute name="Class-Path" value="${classpath.jar}"/>
+                <attribute name="Main-Class" value="${project.main}"/>
+            </manifest>
+        </jar>
+    </target>
+
+    <target name="run" depends="package" description="--> run the program">
+        <java jar="${project.jar}" fork="true"/>
+    </target>
+
+    <target name="clean" description="--> clean the project">
+        <delete includeemptydirs="true" quiet="true">
+            <fileset dir=".">
+                <include name="build/**"/>
+                <include name="lib/ivy.jar"/>
+                <include name="lib/java/**"/>
+                <include name="lib/native/**"/>
+                <include name="${project.jar}"/>
+            </fileset>
+        </delete>
+    </target>
+</project>

doc/Example-Ivy-Project/ivy.xml

@@ -0,0 +1,31 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
+
+<ivy-module version="2.0">
+    <info organisation="${project.organization}" module="${project.module}"/>
+
+    <configurations>
+        <conf name="test" extends="runtime" visibility="private"/>
+        <conf name="runtime"/>
+    </configurations>
+
+    <dependencies>
+        <!-- JavaSMT -->
+        <dependency org="org.sosy_lab" name="java-smt" rev="6.0.0-148-gba08f432a" conf="runtime->runtime-x64,runtime-arm64"/>
+
+        <!-- JUnit6 -->
+        <dependency org="org.junit.jupiter" name="junit-jupiter-api" rev="6.1.0" conf="test->default"/>
+        <dependency org="org.junit.jupiter" name="junit-jupiter-params" rev="6.1.0" conf="test->default"/>
+        <dependency org="org.junit.jupiter" name="junit-jupiter-engine" rev="6.1.0" conf="test->default"/>
+
+        <!-- JUnit6 console launcher -->
+        <dependency org="org.junit.platform" name="junit-platform-console" rev="6.1.0" conf="test->default"/>
+    </dependencies>
+</ivy-module>

doc/Example-Ivy-Project/lib/ivy-settings.xml

@@ -0,0 +1,30 @@
+<?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: 2025 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
+
+<ivysettings>
+    <settings defaultResolver="default"/>
+    <property name="ivy.repo.url" value="https://www.sosy-lab.org/ivy"/>
+    <resolvers>
+        <chain name="default">
+            <!-- Download packages from Sosy-Labs -->
+            <url name="Sosy-Lab" descriptor="required">
+                <ivy pattern="${ivy.repo.url}/[organisation]/[module]/ivy-[revision].xml"/>
+                <artifact pattern="${ivy.repo.url}/[organisation]/[module]/([arch]/)[artifact]-[revision](-[classifier]).[ext]"/>
+            </url>
+            <!-- Use Maven central as a fallback -->
+            <ibiblio name="central" m2compatible="true"/>
+        </chain>
+    </resolvers>
+
+    <caches defaultCacheDir="${user.home}/.ivy2/cache"
+            artifactPattern="[organisation]/[module]/[type]s/([arch]/)[artifact]-[revision](-[classifier]).[ext]"/>
+</ivysettings>

doc/Example-Ivy-Project/src/main/org/sosy_lab/java_smt_example/SolverOverviewTable.java

@@ -0,0 +1,46 @@
+// 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
+
+package org.sosy_lab.java_smt_example;
+
+import java.util.ArrayList;
+import java.util.Comparator;
+import java.util.List;
+import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
+import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.example.SolverOverviewTable.RowBuilder;
+import org.sosy_lab.java_smt.example.SolverOverviewTable.SolverInfo;
+
+/**
+ * This program takes all installed solvers and checks them for version, theories and features and
+ * prints them to StdOut in a nice table.
+ *
+ * <p>This is just a copy of org.sosy_lab.java_smt.example.SolverOverviewTable
+ */
+public class SolverOverviewTable {
+
+  public static void main(String[] args) throws SolverException, InterruptedException {
+
+    final org.sosy_lab.java_smt.example.SolverOverviewTable infoProvider =
+        new org.sosy_lab.java_smt.example.SolverOverviewTable();
+    final List<SolverInfo> infos = new ArrayList<>();
+    for (Solvers s : Solvers.values()) {
+      infos.add(infoProvider.getSolverInformation(s));
+    }
+
+    infos.sort(Comparator.comparing(SolverInfo::getName)); // alphabetical ordering
+
+    RowBuilder rowBuilder = new RowBuilder();
+    for (SolverInfo info : infos) {
+      rowBuilder.addSolver(info);
+    }
+    System.out.println(rowBuilder);
+  }
+
+  private SolverOverviewTable() {}
+}