From 7c49fa8f77a021acfd031f29f6952c1b8b2366e4 Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Sun, 23 Mar 2025 15:43:59 +0100
Subject: [PATCH 1/3] Add JavaSMT project template for Ivy/Ant

---
 doc/Example-Ivy-Project/README.md             | 23 ++++++
 doc/Example-Ivy-Project/build.xml             | 80 +++++++++++++++++++
 doc/Example-Ivy-Project/ivy.xml               | 16 ++++
 doc/Example-Ivy-Project/lib/ivy-settings.xml  | 25 ++++++
 .../lib/native/arm64-linux/libbitwuzlaj.so    |  1 +
 .../lib/native/arm64-linux/libmathsat5j.so    |  1 +
 .../lib/native/arm64-linux/libopensmtj.so     |  1 +
 .../lib/native/arm64-linux/libz3.so           |  1 +
 .../lib/native/arm64-linux/libz3java.so       |  1 +
 .../lib/native/x86_64-linux/libbitwuzlaj.so   |  1 +
 .../lib/native/x86_64-linux/libmathsat5j.so   |  1 +
 .../lib/native/x86_64-linux/libopensmtj.so    |  1 +
 .../lib/native/x86_64-linux/libz3.so          |  1 +
 .../lib/native/x86_64-linux/libz3java.so      |  1 +
 doc/Example-Ivy-Project/src/example/Main.java | 34 ++++++++
 15 files changed, 188 insertions(+)
 create mode 100644 doc/Example-Ivy-Project/README.md
 create mode 100644 doc/Example-Ivy-Project/build.xml
 create mode 100644 doc/Example-Ivy-Project/ivy.xml
 create mode 100644 doc/Example-Ivy-Project/lib/ivy-settings.xml
 create mode 120000 doc/Example-Ivy-Project/lib/native/arm64-linux/libbitwuzlaj.so
 create mode 120000 doc/Example-Ivy-Project/lib/native/arm64-linux/libmathsat5j.so
 create mode 120000 doc/Example-Ivy-Project/lib/native/arm64-linux/libopensmtj.so
 create mode 120000 doc/Example-Ivy-Project/lib/native/arm64-linux/libz3.so
 create mode 120000 doc/Example-Ivy-Project/lib/native/arm64-linux/libz3java.so
 create mode 120000 doc/Example-Ivy-Project/lib/native/x86_64-linux/libbitwuzlaj.so
 create mode 120000 doc/Example-Ivy-Project/lib/native/x86_64-linux/libmathsat5j.so
 create mode 120000 doc/Example-Ivy-Project/lib/native/x86_64-linux/libopensmtj.so
 create mode 120000 doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3.so
 create mode 120000 doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3java.so
 create mode 100644 doc/Example-Ivy-Project/src/example/Main.java

diff --git a/doc/Example-Ivy-Project/README.md b/doc/Example-Ivy-Project/README.md
new file mode 100644
index 0000000000..6d94b06f17
--- /dev/null
+++ b/doc/Example-Ivy-Project/README.md
@@ -0,0 +1,23 @@
+<!--
+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.
+
+The project supports the following build steps:
+
+- `resolve` retrieve dependencies with Ivy
+- `compile` compile the project
+- `package` build a .jar
+- `run` run the program
+- `clean` clean the project
+
+Calling `ant` with no target will build and then execute the project.
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/build.xml b/doc/Example-Ivy-Project/build.xml
new file mode 100644
index 0000000000..5adde30f10
--- /dev/null
+++ b/doc/Example-Ivy-Project/build.xml
@@ -0,0 +1,80 @@
+<!--
+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="example.Main"/>
+
+    <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="compile" depends="resolve" 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"/>
+    </target>
+
+    <target name="package" depends="compile" description="--> build a .jar">
+        <manifestclasspath property="classpath.jar" jarfile="${project.jar}">
+            <classpath>
+                <fileset dir="lib/java/default" 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="${project.jar}"/>
+            </fileset>
+            <fileset dir="lib/java"/>
+        </delete>
+    </target>
+</project>
diff --git a/doc/Example-Ivy-Project/ivy.xml b/doc/Example-Ivy-Project/ivy.xml
new file mode 100644
index 0000000000..bdbe362cef
--- /dev/null
+++ b/doc/Example-Ivy-Project/ivy.xml
@@ -0,0 +1,16 @@
+<!--
+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}"/>
+    <dependencies>
+        <dependency org="org.sosy_lab" name="java-smt" rev="5.0.1-362-g3846f26ca" conf="default->runtime-x64,runtime-arm64"/>
+    </dependencies>
+</ivy-module>
diff --git a/doc/Example-Ivy-Project/lib/ivy-settings.xml b/doc/Example-Ivy-Project/lib/ivy-settings.xml
new file mode 100644
index 0000000000..1da8869609
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/ivy-settings.xml
@@ -0,0 +1,25 @@
+<?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="Sosy-Lab"/>
+    <property name="ivy.repo.url" value="https://www.sosy-lab.org/ivy"/>
+    <resolvers>
+        <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>
+    </resolvers>
+
+    <caches defaultCacheDir="${user.home}/.ivy2/cache"
+            artifactPattern="[organisation]/[module]/[type]s/([arch]/)[artifact]-[revision](-[classifier]).[ext]"/>
+</ivysettings>
diff --git a/doc/Example-Ivy-Project/lib/native/arm64-linux/libbitwuzlaj.so b/doc/Example-Ivy-Project/lib/native/arm64-linux/libbitwuzlaj.so
new file mode 120000
index 0000000000..372f592128
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/arm64-linux/libbitwuzlaj.so
@@ -0,0 +1 @@
+../../java/default/arm64/libbitwuzlaj.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/arm64-linux/libmathsat5j.so b/doc/Example-Ivy-Project/lib/native/arm64-linux/libmathsat5j.so
new file mode 120000
index 0000000000..c7eaf57210
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/arm64-linux/libmathsat5j.so
@@ -0,0 +1 @@
+../../java/default/arm64/libmathsat5j.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/arm64-linux/libopensmtj.so b/doc/Example-Ivy-Project/lib/native/arm64-linux/libopensmtj.so
new file mode 120000
index 0000000000..8aadd048bf
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/arm64-linux/libopensmtj.so
@@ -0,0 +1 @@
+../../java/default/arm64/libopensmtj.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/arm64-linux/libz3.so b/doc/Example-Ivy-Project/lib/native/arm64-linux/libz3.so
new file mode 120000
index 0000000000..7252d0c3c0
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/arm64-linux/libz3.so
@@ -0,0 +1 @@
+../../java/default/arm64/libz3.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/arm64-linux/libz3java.so b/doc/Example-Ivy-Project/lib/native/arm64-linux/libz3java.so
new file mode 120000
index 0000000000..934e062ea2
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/arm64-linux/libz3java.so
@@ -0,0 +1 @@
+../../java/default/arm64/libz3java.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/x86_64-linux/libbitwuzlaj.so b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libbitwuzlaj.so
new file mode 120000
index 0000000000..ef45bf4c23
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libbitwuzlaj.so
@@ -0,0 +1 @@
+../../java/default/x64/libbitwuzlaj.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/x86_64-linux/libmathsat5j.so b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libmathsat5j.so
new file mode 120000
index 0000000000..c734ccd975
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libmathsat5j.so
@@ -0,0 +1 @@
+../../java/default/x64/libmathsat5j.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/x86_64-linux/libopensmtj.so b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libopensmtj.so
new file mode 120000
index 0000000000..e613c908c0
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libopensmtj.so
@@ -0,0 +1 @@
+../../java/default/x64/libopensmtj.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3.so b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3.so
new file mode 120000
index 0000000000..e2423e093d
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3.so
@@ -0,0 +1 @@
+../../java/default/x64/libz3.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3java.so b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3java.so
new file mode 120000
index 0000000000..392351c46a
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3java.so
@@ -0,0 +1 @@
+../../java/default/x64/libz3java.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/src/example/Main.java b/doc/Example-Ivy-Project/src/example/Main.java
new file mode 100644
index 0000000000..4a6298c944
--- /dev/null
+++ b/doc/Example-Ivy-Project/src/example/Main.java
@@ -0,0 +1,34 @@
+// 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
+
+package example;
+
+import org.sosy_lab.common.ShutdownNotifier;
+import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
+import org.sosy_lab.common.log.LogManager;
+import org.sosy_lab.java_smt.SolverContextFactory;
+import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
+import org.sosy_lab.java_smt.api.SolverContext;
+
+public class Main {
+  public static void main(String[] args) {
+    Configuration config = Configuration.defaultConfiguration();
+    LogManager logger = LogManager.createNullLogManager();
+    ShutdownNotifier notifier = ShutdownNotifier.createDummy();
+
+    for (Solvers solver : Solvers.values()) {
+      try (SolverContext context =
+          SolverContextFactory.createSolverContext(config, logger, notifier, solver)) {
+        System.out.println(solver + ", " + context.getVersion());
+      } catch (InvalidConfigurationException e) {
+        System.out.println(solver + " not available");
+      }
+    }
+  }
+}

From 0eb07752fff6f1d773249601789ef22da5f04b3a Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Mon, 24 Mar 2025 12:54:50 +0100
Subject: [PATCH 2/3] IvyExampleProject: Copy library files for windows

---
 doc/Example-Ivy-Project/build.xml | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/doc/Example-Ivy-Project/build.xml b/doc/Example-Ivy-Project/build.xml
index 5adde30f10..b315efc27a 100644
--- a/doc/Example-Ivy-Project/build.xml
+++ b/doc/Example-Ivy-Project/build.xml
@@ -36,7 +36,22 @@ SPDX-License-Identifier: Apache-2.0
         <ivy:retrieve pattern="lib/java/[conf]/([arch]/)[artifact](-[classifier]).[ext]"/>
     </target>
 
-    <target name="compile" depends="resolve" description="--> compile the project">
+    <target name="install" depends="resolve">
+        <mkdir dir="lib/native/x86_64-windows"/>
+        <copy todir="lib/native/x86_64-windows">
+            <fileset dir="lib/java/default/x64">
+                <include name="*.dll"/>
+            </fileset>
+        </copy>
+        <mkdir dir="lib/native/arm64-windows"/>
+        <copy todir="lib/native/arm64-windows">
+            <fileset dir="lib/java/default/arm64">
+                <include name="*.dll"/>
+            </fileset>
+        </copy>
+    </target>
+
+    <target name="compile" depends="install" description="--> compile the project">
         <mkdir dir="build"/>
         <path id="classpath.build">
             <pathelement location="build"/>
@@ -72,6 +87,8 @@ SPDX-License-Identifier: Apache-2.0
                 <include name="build/**"/>
                 <include name="lib/ivy.jar"/>
                 <include name="lib/java/**"/>
+                <include name="lib/native/x86_64-windows/**"/>
+                <include name="lib/native/arm64-windows/**"/>
                 <include name="${project.jar}"/>
             </fileset>
             <fileset dir="lib/java"/>

From 7cdb93719d7d4880a00fecef4fa4204ba95ca670 Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Mon, 24 Mar 2025 12:56:00 +0100
Subject: [PATCH 3/3] IvyExampleProject: Add symlinks for macOS

---
 doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3.dylib      | 1 +
 doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3java.dylib  | 1 +
 doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3.dylib     | 1 +
 doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3java.dylib | 1 +
 4 files changed, 4 insertions(+)
 create mode 120000 doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3.dylib
 create mode 120000 doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3java.dylib
 create mode 120000 doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3.dylib
 create mode 120000 doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3java.dylib

diff --git a/doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3.dylib b/doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3.dylib
new file mode 120000
index 0000000000..590d25fa37
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3.dylib
@@ -0,0 +1 @@
+../../java/default/arm64/libz3.dylib
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3java.dylib b/doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3java.dylib
new file mode 120000
index 0000000000..397941ff52
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3java.dylib
@@ -0,0 +1 @@
+../../java/default/arm64/libz3java.dylib
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3.dylib b/doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3.dylib
new file mode 120000
index 0000000000..898516499b
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3.dylib
@@ -0,0 +1 @@
+../../java/default/x64/libz3.dylib
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3java.dylib b/doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3java.dylib
new file mode 120000
index 0000000000..1c865209db
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3java.dylib
@@ -0,0 +1 @@
+../../java/default/x64/libz3java.dylib
\ No newline at end of file