From 7c49fa8f77a021acfd031f29f6952c1b8b2366e4 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 23 Mar 2025 15:43:59 +0100 Subject: [PATCH 1/9] 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 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 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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 @@ + + + + + + + + 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 @@ + + + + + + + + + + + + + + + + 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 +// +// 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 Date: Mon, 24 Mar 2025 12:54:50 +0100 Subject: [PATCH 2/9] 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 - + + + + + + + + + + + + + + + + @@ -72,6 +87,8 @@ SPDX-License-Identifier: Apache-2.0 + + From 7cdb93719d7d4880a00fecef4fa4204ba95ca670 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 24 Mar 2025 12:56:00 +0100 Subject: [PATCH 3/9] 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 From aec0884ccdaccd6694f58c40e25e43118dde6e2a Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 3 Sep 2025 11:32:11 +0200 Subject: [PATCH 4/9] IvyExampleProject: Copy solver binaries and remove the symlinks --- doc/Example-Ivy-Project/build.xml | 47 ++++++++++++++----- .../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/arm64-macosx/libz3.dylib | 1 - .../lib/native/arm64-macosx/libz3java.dylib | 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 - .../lib/native/x86_64-macosx/libz3.dylib | 1 - .../lib/native/x86_64-macosx/libz3java.dylib | 1 - 15 files changed, 36 insertions(+), 25 deletions(-) delete mode 120000 doc/Example-Ivy-Project/lib/native/arm64-linux/libbitwuzlaj.so delete mode 120000 doc/Example-Ivy-Project/lib/native/arm64-linux/libmathsat5j.so delete mode 120000 doc/Example-Ivy-Project/lib/native/arm64-linux/libopensmtj.so delete mode 120000 doc/Example-Ivy-Project/lib/native/arm64-linux/libz3.so delete mode 120000 doc/Example-Ivy-Project/lib/native/arm64-linux/libz3java.so delete mode 120000 doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3.dylib delete mode 120000 doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3java.dylib delete mode 120000 doc/Example-Ivy-Project/lib/native/x86_64-linux/libbitwuzlaj.so delete mode 120000 doc/Example-Ivy-Project/lib/native/x86_64-linux/libmathsat5j.so delete mode 120000 doc/Example-Ivy-Project/lib/native/x86_64-linux/libopensmtj.so delete mode 120000 doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3.so delete mode 120000 doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3java.so delete mode 120000 doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3.dylib delete mode 120000 doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3java.dylib diff --git a/doc/Example-Ivy-Project/build.xml b/doc/Example-Ivy-Project/build.xml index b315efc27a..bedc9b252f 100644 --- a/doc/Example-Ivy-Project/build.xml +++ b/doc/Example-Ivy-Project/build.xml @@ -36,22 +36,49 @@ SPDX-License-Identifier: Apache-2.0 - + - - - + + + + - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + @@ -87,11 +114,9 @@ SPDX-License-Identifier: Apache-2.0 - - + - diff --git a/doc/Example-Ivy-Project/lib/native/arm64-linux/libbitwuzlaj.so b/doc/Example-Ivy-Project/lib/native/arm64-linux/libbitwuzlaj.so deleted file mode 120000 index 372f592128..0000000000 --- a/doc/Example-Ivy-Project/lib/native/arm64-linux/libbitwuzlaj.so +++ /dev/null @@ -1 +0,0 @@ -../../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 deleted file mode 120000 index c7eaf57210..0000000000 --- a/doc/Example-Ivy-Project/lib/native/arm64-linux/libmathsat5j.so +++ /dev/null @@ -1 +0,0 @@ -../../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 deleted file mode 120000 index 8aadd048bf..0000000000 --- a/doc/Example-Ivy-Project/lib/native/arm64-linux/libopensmtj.so +++ /dev/null @@ -1 +0,0 @@ -../../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 deleted file mode 120000 index 7252d0c3c0..0000000000 --- a/doc/Example-Ivy-Project/lib/native/arm64-linux/libz3.so +++ /dev/null @@ -1 +0,0 @@ -../../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 deleted file mode 120000 index 934e062ea2..0000000000 --- a/doc/Example-Ivy-Project/lib/native/arm64-linux/libz3java.so +++ /dev/null @@ -1 +0,0 @@ -../../java/default/arm64/libz3java.so \ No newline at end of file diff --git a/doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3.dylib b/doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3.dylib deleted file mode 120000 index 590d25fa37..0000000000 --- a/doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3.dylib +++ /dev/null @@ -1 +0,0 @@ -../../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 deleted file mode 120000 index 397941ff52..0000000000 --- a/doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3java.dylib +++ /dev/null @@ -1 +0,0 @@ -../../java/default/arm64/libz3java.dylib \ 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 deleted file mode 120000 index ef45bf4c23..0000000000 --- a/doc/Example-Ivy-Project/lib/native/x86_64-linux/libbitwuzlaj.so +++ /dev/null @@ -1 +0,0 @@ -../../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 deleted file mode 120000 index c734ccd975..0000000000 --- a/doc/Example-Ivy-Project/lib/native/x86_64-linux/libmathsat5j.so +++ /dev/null @@ -1 +0,0 @@ -../../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 deleted file mode 120000 index e613c908c0..0000000000 --- a/doc/Example-Ivy-Project/lib/native/x86_64-linux/libopensmtj.so +++ /dev/null @@ -1 +0,0 @@ -../../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 deleted file mode 120000 index e2423e093d..0000000000 --- a/doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3.so +++ /dev/null @@ -1 +0,0 @@ -../../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 deleted file mode 120000 index 392351c46a..0000000000 --- a/doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3java.so +++ /dev/null @@ -1 +0,0 @@ -../../java/default/x64/libz3java.so \ 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 deleted file mode 120000 index 898516499b..0000000000 --- a/doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3.dylib +++ /dev/null @@ -1 +0,0 @@ -../../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 deleted file mode 120000 index 1c865209db..0000000000 --- a/doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3java.dylib +++ /dev/null @@ -1 +0,0 @@ -../../java/default/x64/libz3java.dylib \ No newline at end of file From f17ec991d6ed9423c1830d97a29af4285ff729d2 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 3 Sep 2025 11:26:43 +0200 Subject: [PATCH 5/9] IvyExampleProject: Update to latest JavaSMT release --- doc/Example-Ivy-Project/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/Example-Ivy-Project/ivy.xml b/doc/Example-Ivy-Project/ivy.xml index bdbe362cef..b5a9d0238c 100644 --- a/doc/Example-Ivy-Project/ivy.xml +++ b/doc/Example-Ivy-Project/ivy.xml @@ -11,6 +11,6 @@ SPDX-License-Identifier: Apache-2.0 - + From 72a5ae8d6cb5d73673670633413c497ace47fd15 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 25 May 2026 17:27:50 +0200 Subject: [PATCH 6/9] Update JavaSMT version in the Ivy example project --- doc/Example-Ivy-Project/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/Example-Ivy-Project/ivy.xml b/doc/Example-Ivy-Project/ivy.xml index b5a9d0238c..33ac381d1b 100644 --- a/doc/Example-Ivy-Project/ivy.xml +++ b/doc/Example-Ivy-Project/ivy.xml @@ -11,6 +11,6 @@ SPDX-License-Identifier: Apache-2.0 - + From bbcd67647c26811e671aee0187458ec38323da99 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 26 May 2026 11:20:25 +0200 Subject: [PATCH 7/9] Add tests for the Ivy example project and make it better aligned with the other template projects --- doc/Example-Ivy-Project/README.md | 7 +- doc/Example-Ivy-Project/build.xml | 31 ++- doc/Example-Ivy-Project/ivy.xml | 17 +- doc/Example-Ivy-Project/lib/ivy-settings.xml | 15 +- doc/Example-Ivy-Project/src/example/Main.java | 34 --- .../java_smt_example/SolverOverviewTable.java | 46 +++++ .../sosy_lab/java_smt_example/SudokuTest.java | 195 ++++++++++++++++++ 7 files changed, 293 insertions(+), 52 deletions(-) delete mode 100644 doc/Example-Ivy-Project/src/example/Main.java create mode 100644 doc/Example-Ivy-Project/src/main/org/sosy_lab/java_smt_example/SolverOverviewTable.java create mode 100644 doc/Example-Ivy-Project/src/test/org/sosy_lab/java_smt_example/SudokuTest.java diff --git a/doc/Example-Ivy-Project/README.md b/doc/Example-Ivy-Project/README.md index 6d94b06f17..7e95a4d431 100644 --- a/doc/Example-Ivy-Project/README.md +++ b/doc/Example-Ivy-Project/README.md @@ -10,14 +10,15 @@ 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. +number and supported features. -The project supports the following build steps: +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. \ No newline at end of file +Calling `ant` with no target will build and then execute the project. diff --git a/doc/Example-Ivy-Project/build.xml b/doc/Example-Ivy-Project/build.xml index bedc9b252f..cffc070cde 100644 --- a/doc/Example-Ivy-Project/build.xml +++ b/doc/Example-Ivy-Project/build.xml @@ -15,7 +15,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -39,40 +39,40 @@ SPDX-License-Identifier: Apache-2.0 - + - + - + - + - + - + @@ -84,13 +84,26 @@ SPDX-License-Identifier: Apache-2.0 - + + + + + + + + + + + + + - + + + + + + + - + + + + + + + + + + diff --git a/doc/Example-Ivy-Project/lib/ivy-settings.xml b/doc/Example-Ivy-Project/lib/ivy-settings.xml index 1da8869609..0f8c6e63e7 100644 --- a/doc/Example-Ivy-Project/lib/ivy-settings.xml +++ b/doc/Example-Ivy-Project/lib/ivy-settings.xml @@ -11,13 +11,18 @@ SPDX-License-Identifier: Apache-2.0 --> - + - - - - + + + + + + + + + -// -// 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"); - } - } - } -} diff --git a/doc/Example-Ivy-Project/src/main/org/sosy_lab/java_smt_example/SolverOverviewTable.java b/doc/Example-Ivy-Project/src/main/org/sosy_lab/java_smt_example/SolverOverviewTable.java new file mode 100644 index 0000000000..29ee5ab3b5 --- /dev/null +++ b/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 +// +// 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. + * + *

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 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() {} +} diff --git a/doc/Example-Ivy-Project/src/test/org/sosy_lab/java_smt_example/SudokuTest.java b/doc/Example-Ivy-Project/src/test/org/sosy_lab/java_smt_example/SudokuTest.java new file mode 100644 index 0000000000..2f081cacf2 --- /dev/null +++ b/doc/Example-Ivy-Project/src/test/org/sosy_lab/java_smt_example/SudokuTest.java @@ -0,0 +1,195 @@ +// 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 +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt_example; + +import com.google.common.base.Joiner; +import com.google.common.base.Splitter; +import org.junit.jupiter.api.AfterEach; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; +import org.junit.jupiter.params.Parameter; +import org.junit.jupiter.params.ParameterizedClass; +import org.junit.jupiter.params.provider.MethodSource; +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.BasicLogManager; +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; +import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.example.Sudoku; +import org.sosy_lab.java_smt.example.Sudoku.SudokuSolver; + +import java.util.Arrays; +import java.util.List; +import java.util.logging.Level; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertNotNull; +import static org.junit.jupiter.api.Assumptions.assumeTrue; + + +/** + * This program parses a String-given Sudoku and solves it with an SMT solver. + * + *

This program is just an example and clearly SMT is not the best solution for solving Sudoku. + * There might be other algorithms out there that are better suited for solving Sudoku. + * + *

The more numbers are available in a Sudoku, the easier it can be solved. A completely empty + * Sudoku will cause the longest runtime in the solver, because it will guess a lot of values. + * + *

The Sudoku is read from a String and should be formatted as the following example: + * + * 

+ * 2..9.6..1
+ * ..6.4...9
+ * ...52.4..
+ * 3.2..7.5.
+ * ...2..1..
+ * .9.3..7..
+ * .87.5.31.
+ * 6.3.1.8..
+ * 4....9...
+ *
+ * + *

The solution will then be printed on StdOut and checked by an assertion, just like the + * following solution: + * + * 

+ * 248976531
+ * 536148279
+ * 179523468
+ * 312487956
+ * 764295183
+ * 895361742
+ * 987652314
+ * 623714895
+ * 451839627
+ *
+ */ +@ParameterizedClass +@MethodSource("getAllSolvers") +public class SudokuTest { + + public static List getAllSolvers() { + return Arrays.asList(Solvers.values()); + } + + @Parameter(0) + public Solvers solver; + + private static final String OS = System.getProperty("os.name").toLowerCase().replace(" ", ""); + private static final boolean IS_LINUX = OS.startsWith("linux"); + private static final boolean IS_X64 = System.getProperty("os.arch").contains("64"); + + /** + * Disable some checks on certain combinations of operating systems and solvers, because of missing dependencies. + */ + private static boolean isOperatingSystemSupported(Solvers solver) { + return switch (solver) { + case SMTINTERPOL, PRINCESS -> true; // Java-based solvers should work on all platforms + default -> IS_LINUX && IS_X64; // this example only includes Linux x64 binaries for native solvers + }; + } + + private Configuration config; + private LogManager logger; + private ShutdownNotifier notifier; + + private SolverContext context; + + private static final String input = """ + 2..9.6..1 + ..6.4...9 + ...52.4.. + 3.2..7.5. + ...2..1.. + .9.3..7.. + .87.5.31. + 6.3.1.8.. + 4....9... + """; + + private static final String sudokuSolution = """ + 248976531 + 536148279 + 179523468 + 312487956 + 764295183 + 895361742 + 987652314 + 623714895 + 451839627 + """; + + @BeforeEach + public void init() throws InvalidConfigurationException { + config = Configuration.defaultConfiguration(); + logger = BasicLogManager.create(config); + notifier = ShutdownNotifier.createDummy(); + } + + /* + * We close our context after we are done with a solver to not waste memory. + */ + @AfterEach + public final void closeSolver() { + if (context != null) { + context.close(); + } + } + + @Test + public void checkSudoku() + throws InvalidConfigurationException, InterruptedException, SolverException { + assumeTrue(isOperatingSystemSupported(solver)); + + logger.log(Level.INFO, "Executing " + solver + "..."); + + context = SolverContextFactory.createSolverContext(config, logger, notifier, solver); + Integer[][] grid = readGridFromString(input); + + SudokuSolver sudoku = new Sudoku.BooleanBasedSudokuSolver(context); + Integer[][] solution = sudoku.solve(grid); + + assertNotNull(solution); + assertEquals(sudokuSolution, solutionToString(solution)); + } + + private String solutionToString(Integer[][] solution) { + StringBuilder sb = new StringBuilder(); + for (Integer[] s1 : solution) { + sb.append(Joiner.on("").join(s1)).append('\n'); + } + return sb.toString(); + } + + /** + * a simple parser for a half-filled Sudoku. + * + *

Use digits 0-9 as values, other values will be set to 'unknown'. + */ + private Integer[][] readGridFromString(String puzzle) { + List lines = Splitter.on('\n').splitToList(puzzle); + Integer[][] grid = new Integer[lines.size()][lines.size()]; + + for (int row = 0; row < lines.size(); row++) { + for (int col = 0; col < lines.get(row).length(); col++) { + char nextNumber = lines.get(row).charAt(col); + if ('0' <= nextNumber && nextNumber <= '9') { + grid[row][col] = nextNumber - '0'; + } + } + } + return grid; + } +} + From c8696795201d5067bcf9b6b7d1c4f9cd9d7c9f4a Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 30 May 2026 11:35:07 +0200 Subject: [PATCH 8/9] Fix macOS paths in Ivy example project --- doc/Example-Ivy-Project/build.xml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/doc/Example-Ivy-Project/build.xml b/doc/Example-Ivy-Project/build.xml index cffc070cde..59f4a26044 100644 --- a/doc/Example-Ivy-Project/build.xml +++ b/doc/Example-Ivy-Project/build.xml @@ -63,17 +63,17 @@ SPDX-License-Identifier: Apache-2.0 - - + + - - + + - + From b5ca507ea344b04c2710da7ec0ed0d4c7397a7c6 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 30 May 2026 11:36:19 +0200 Subject: [PATCH 9/9] Add support for other platforms in Ivy example project --- .../sosy_lab/java_smt_example/SudokuTest.java | 66 +++++++++++++++---- 1 file changed, 54 insertions(+), 12 deletions(-) diff --git a/doc/Example-Ivy-Project/src/test/org/sosy_lab/java_smt_example/SudokuTest.java b/doc/Example-Ivy-Project/src/test/org/sosy_lab/java_smt_example/SudokuTest.java index 2f081cacf2..b1f92c8157 100644 --- a/doc/Example-Ivy-Project/src/test/org/sosy_lab/java_smt_example/SudokuTest.java +++ b/doc/Example-Ivy-Project/src/test/org/sosy_lab/java_smt_example/SudokuTest.java @@ -10,12 +10,14 @@ import com.google.common.base.Joiner; import com.google.common.base.Splitter; +import com.google.common.base.StandardSystemProperty; import org.junit.jupiter.api.AfterEach; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; import org.junit.jupiter.params.Parameter; import org.junit.jupiter.params.ParameterizedClass; import org.junit.jupiter.params.provider.MethodSource; +import org.sosy_lab.common.NativeLibraries; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; @@ -30,6 +32,7 @@ import java.util.Arrays; import java.util.List; +import java.util.Locale; import java.util.logging.Level; import static org.junit.jupiter.api.Assertions.assertEquals; @@ -86,19 +89,16 @@ public static List getAllSolvers() { @Parameter(0) public Solvers solver; - private static final String OS = System.getProperty("os.name").toLowerCase().replace(" ", ""); + private static final String OS = + StandardSystemProperty.OS_NAME.value().toLowerCase(Locale.getDefault()).replace(" ", ""); + private static final String ARCH = + StandardSystemProperty.OS_ARCH.value().toLowerCase(Locale.getDefault()).replace(" ", ""); + + protected static final boolean IS_WINDOWS = OS.startsWith("windows"); + private static final boolean IS_MAC = OS.startsWith("macos"); private static final boolean IS_LINUX = OS.startsWith("linux"); - private static final boolean IS_X64 = System.getProperty("os.arch").contains("64"); - /** - * Disable some checks on certain combinations of operating systems and solvers, because of missing dependencies. - */ - private static boolean isOperatingSystemSupported(Solvers solver) { - return switch (solver) { - case SMTINTERPOL, PRINCESS -> true; // Java-based solvers should work on all platforms - default -> IS_LINUX && IS_X64; // this example only includes Linux x64 binaries for native solvers - }; - } + private static final boolean IS_ARCH_ARM64 = ARCH.equals("aarch64"); private Configuration config; private LogManager logger; @@ -147,10 +147,52 @@ public final void closeSolver() { } } + private boolean isSufficientVersionOfLibcxx(String library) { + try { + NativeLibraries.loadLibrary(library); + } catch (UnsatisfiedLinkError e) { + for (String dependency : getRequiredLibcxx(library)) { + if (e.getMessage().contains("version `" + dependency + "' not found")) { + return false; + } + } + } + return true; + } + + private String[] getRequiredLibcxx(String library) { + return switch (library) { + case "z3" -> new String[]{"GLIBC_2.34", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "bitwuzlaj" -> new String[]{"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "opensmtj" -> new String[]{"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + case "mathsat5j" -> new String[]{"GLIBC_2.33", "GLIBC_2.38"}; + case "cvc5jni" -> new String[]{"GLIBC_2.32"}; + case "yices2java" -> new String[]{"GLIBC_2.34"}; + default -> new String[]{}; + }; + } + + private boolean isSupportedOperatingSystemAndArchitecture(Solvers solver) { + return switch (solver) { + case SMTINTERPOL, PRINCESS -> + // Any operating system and any architecture is allowed, Java is sufficient + true; + case BOOLECTOR, CVC4 -> IS_LINUX && !IS_ARCH_ARM64; + case YICES2 -> (IS_LINUX && !IS_ARCH_ARM64 && isSufficientVersionOfLibcxx("yices2java")) + || (IS_WINDOWS && !IS_ARCH_ARM64); + case CVC5 -> (IS_LINUX && isSufficientVersionOfLibcxx("cvc5jni")) || IS_WINDOWS || IS_MAC; + case OPENSMT -> IS_LINUX && isSufficientVersionOfLibcxx("opensmtj"); + case BITWUZLA -> (IS_LINUX && isSufficientVersionOfLibcxx("bitwuzlaj")) || (IS_WINDOWS && !IS_ARCH_ARM64); + case MATHSAT5 -> (IS_LINUX && isSufficientVersionOfLibcxx("mathsat5j")) || (IS_WINDOWS && !IS_ARCH_ARM64); + case Z3 -> (IS_LINUX && isSufficientVersionOfLibcxx("z3")) || IS_WINDOWS || IS_MAC; + case Z3_WITH_INTERPOLATION -> IS_LINUX && !IS_ARCH_ARM64; + }; + } + @Test public void checkSudoku() throws InvalidConfigurationException, InterruptedException, SolverException { - assumeTrue(isOperatingSystemSupported(solver)); + assumeTrue(isSupportedOperatingSystemAndArchitecture(solver)); logger.log(Level.INFO, "Executing " + solver + "...");