From 1ca68360165d30dc6f3891c95eac7805a48712a2 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 29 Mar 2026 10:53:48 +0200 Subject: [PATCH 01/30] update maven-pom-templates to current year. --- solvers_maven_conf/maven_bitwuzla_pom_template.xml | 2 +- solvers_maven_conf/maven_boolector_pom_template.xml | 2 +- solvers_maven_conf/maven_cvc4_pom_template.xml | 2 +- solvers_maven_conf/maven_cvc5_pom_template.xml | 2 +- solvers_maven_conf/maven_javasmt_yices2_pom_template.xml | 2 +- solvers_maven_conf/maven_mathsat_pom_template.xml | 2 +- solvers_maven_conf/maven_opensmt_pom_template.xml | 2 +- solvers_maven_conf/maven_yices2_pom_template.xml | 2 +- solvers_maven_conf/maven_z3_pom_template.xml | 2 +- 9 files changed, 9 insertions(+), 9 deletions(-) diff --git a/solvers_maven_conf/maven_bitwuzla_pom_template.xml b/solvers_maven_conf/maven_bitwuzla_pom_template.xml index 76ee8bc440..a9fb7301f5 100644 --- a/solvers_maven_conf/maven_bitwuzla_pom_template.xml +++ b/solvers_maven_conf/maven_bitwuzla_pom_template.xml @@ -6,7 +6,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 +SPDX-FileCopyrightText: 2026 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> diff --git a/solvers_maven_conf/maven_boolector_pom_template.xml b/solvers_maven_conf/maven_boolector_pom_template.xml index 4612f68a79..f8e12c6509 100644 --- a/solvers_maven_conf/maven_boolector_pom_template.xml +++ b/solvers_maven_conf/maven_boolector_pom_template.xml @@ -6,7 +6,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: 2021 Dirk Beyer +SPDX-FileCopyrightText: 2026 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> diff --git a/solvers_maven_conf/maven_cvc4_pom_template.xml b/solvers_maven_conf/maven_cvc4_pom_template.xml index 0a37bd83a2..6c6e64d193 100644 --- a/solvers_maven_conf/maven_cvc4_pom_template.xml +++ b/solvers_maven_conf/maven_cvc4_pom_template.xml @@ -6,7 +6,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: 2021 Dirk Beyer +SPDX-FileCopyrightText: 2026 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> diff --git a/solvers_maven_conf/maven_cvc5_pom_template.xml b/solvers_maven_conf/maven_cvc5_pom_template.xml index 5ef05c1d8f..f0a34b498e 100644 --- a/solvers_maven_conf/maven_cvc5_pom_template.xml +++ b/solvers_maven_conf/maven_cvc5_pom_template.xml @@ -6,7 +6,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: 2021 Dirk Beyer +SPDX-FileCopyrightText: 2026 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> diff --git a/solvers_maven_conf/maven_javasmt_yices2_pom_template.xml b/solvers_maven_conf/maven_javasmt_yices2_pom_template.xml index 881f2fbef5..b29f21a4b3 100644 --- a/solvers_maven_conf/maven_javasmt_yices2_pom_template.xml +++ b/solvers_maven_conf/maven_javasmt_yices2_pom_template.xml @@ -6,7 +6,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: 2021 Dirk Beyer +SPDX-FileCopyrightText: 2026 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> diff --git a/solvers_maven_conf/maven_mathsat_pom_template.xml b/solvers_maven_conf/maven_mathsat_pom_template.xml index 6b840e4a2f..96ba0d2cc4 100644 --- a/solvers_maven_conf/maven_mathsat_pom_template.xml +++ b/solvers_maven_conf/maven_mathsat_pom_template.xml @@ -6,7 +6,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: 2025 Dirk Beyer +SPDX-FileCopyrightText: 2026 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> diff --git a/solvers_maven_conf/maven_opensmt_pom_template.xml b/solvers_maven_conf/maven_opensmt_pom_template.xml index c712f68c43..1288926d18 100644 --- a/solvers_maven_conf/maven_opensmt_pom_template.xml +++ b/solvers_maven_conf/maven_opensmt_pom_template.xml @@ -6,7 +6,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: 2021 Dirk Beyer +SPDX-FileCopyrightText: 2026 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> diff --git a/solvers_maven_conf/maven_yices2_pom_template.xml b/solvers_maven_conf/maven_yices2_pom_template.xml index 5f5798694a..4d30fb15f6 100644 --- a/solvers_maven_conf/maven_yices2_pom_template.xml +++ b/solvers_maven_conf/maven_yices2_pom_template.xml @@ -6,7 +6,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: 2021 Dirk Beyer +SPDX-FileCopyrightText: 2026 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> diff --git a/solvers_maven_conf/maven_z3_pom_template.xml b/solvers_maven_conf/maven_z3_pom_template.xml index 079e44714f..4c5116e038 100644 --- a/solvers_maven_conf/maven_z3_pom_template.xml +++ b/solvers_maven_conf/maven_z3_pom_template.xml @@ -6,7 +6,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: 2021 Dirk Beyer +SPDX-FileCopyrightText: 2026 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> From 7f54aff6c7bffbe59962c752866fb165a58fd913 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 29 Mar 2026 10:59:40 +0200 Subject: [PATCH 02/30] add maven-pom-template for Z3 legacy. --- .idea/misc.xml | 16 +---- .../maven_z3-legacy_pom_template.xml | 63 +++++++++++++++++++ 2 files changed, 64 insertions(+), 15 deletions(-) create mode 100644 solvers_maven_conf/maven_z3-legacy_pom_template.xml diff --git a/.idea/misc.xml b/.idea/misc.xml index 79d44e380e..b9159b5c43 100644 --- a/.idea/misc.xml +++ b/.idea/misc.xml @@ -1,19 +1,5 @@ - - - - - - + \ No newline at end of file diff --git a/solvers_maven_conf/maven_z3-legacy_pom_template.xml b/solvers_maven_conf/maven_z3-legacy_pom_template.xml new file mode 100644 index 0000000000..2cdc619fef --- /dev/null +++ b/solvers_maven_conf/maven_z3-legacy_pom_template.xml @@ -0,0 +1,63 @@ + + + + + 4.0.0 + org.sosy-lab + javasmt-solver-z3-legacy + pom + javasmt-solver-z3 + ${stage.revision} + SMT solver Z3 (legacy version with interpolation) for use in JavaSMT + https://github.com/sosy-lab/java-smt + + + + MIT License + https://opensource.org/licenses/MIT + + + + + Software Systems Lab + https://www.sosy-lab.org/ + + + + https://github.com/sosy-lab/java-smt/ + scm:git:git://github.com/sosy-lab/java-smt.git + scm:git:git@github.com:sosy-lab/java-smt.git + + + + + Karlheinz Friedberger + kfriedberger@gmail.com + Software Systems Lab + https://www.sosy-lab.org/people/friedberger/ + + project maintainer + + + + Dirk Beyer + dirk.beyer@sosy-lab.org + https://www.sosy-lab.org/people/beyer/ + Software Systems Lab + http://www.sosy-lab.org/ + + project manager + + + + + From 8d46bccf719ee29739a5de7eaf25aaea0bd1ed62 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 29 Mar 2026 10:37:52 +0200 Subject: [PATCH 03/30] The new script is a larger update and rework of the outdated script. --- build.xml | 1 + build/build-maven-central.xml | 275 ++++++++++++++++++++++++++++++++++ 2 files changed, 276 insertions(+) create mode 100644 build/build-maven-central.xml diff --git a/build.xml b/build.xml index ce0a6c7eca..1718992d82 100644 --- a/build.xml +++ b/build.xml @@ -67,6 +67,7 @@ SPDX-License-Identifier: Apache-2.0 + diff --git a/build/build-maven-central.xml b/build/build-maven-central.xml new file mode 100644 index 0000000000..b9a9ee9413 --- /dev/null +++ b/build/build-maven-central.xml @@ -0,0 +1,275 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + sosy_lab + sosy-lab + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +]]> + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file From e1965fa07a03154f4c1c5b9b4cd69608a13294ab Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 30 Mar 2026 21:17:41 +0200 Subject: [PATCH 04/30] revert changes to central files. --- .idea/misc.xml | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/.idea/misc.xml b/.idea/misc.xml index b9159b5c43..79d44e380e 100644 --- a/.idea/misc.xml +++ b/.idea/misc.xml @@ -1,5 +1,19 @@ + + + + + + \ No newline at end of file + From fe16dc994b001e9b0ea7aa9aa92819be69c1471d Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 31 Mar 2026 14:22:33 +0200 Subject: [PATCH 05/30] MathSAT: fix inconsistent package name for Maven (remove the suffix "5"), and update pom-template with text from latest release. --- solvers_maven_conf/maven_mathsat_pom_template.xml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/solvers_maven_conf/maven_mathsat_pom_template.xml b/solvers_maven_conf/maven_mathsat_pom_template.xml index 96ba0d2cc4..4185ff59a0 100644 --- a/solvers_maven_conf/maven_mathsat_pom_template.xml +++ b/solvers_maven_conf/maven_mathsat_pom_template.xml @@ -13,9 +13,9 @@ SPDX-License-Identifier: Apache-2.0 4.0.0 org.sosy-lab - javasmt-solver-mathsat5 + javasmt-solver-mathsat pom - javasmt-solver-mathsat5 + javasmt-solver-mathsat ${stage.revision} Recompiled Version of the SMT solver Mathsat5 for use in JavaSMT https://github.com/sosy-lab/java-smt @@ -27,7 +27,7 @@ SPDX-License-Identifier: Apache-2.0 - MathSAT5 is copyrighted 2009-2020 by Fondazione Bruno Kessler, Trento, Italy, + MathSAT5 is copyrighted 2009-2026 by Fondazione Bruno Kessler, Trento, Italy, University of Trento, Italy, and others. All rights reserved. MathSAT5 is available for research and evaluation purposes only. From 0ab864ab272d23bc0eff731e10d6ba7e2bfafe85 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 31 Mar 2026 14:39:31 +0200 Subject: [PATCH 06/30] more documentation on Maven publishing --- build/build-maven-central.xml | 25 +++++++++++++++++++------ 1 file changed, 19 insertions(+), 6 deletions(-) diff --git a/build/build-maven-central.xml b/build/build-maven-central.xml index b9a9ee9413..2209e82ece 100644 --- a/build/build-maven-central.xml +++ b/build/build-maven-central.xml @@ -20,11 +20,29 @@ SPDX-License-Identifier: Apache-2.0 The script loads artifacts directly from Ivy, generates a POM file, then uploads to the Maven staging server. - There is a manually triggered release process via https://central.sonatype.com/ + There is a manually triggered release process via https://central.sonatype.com/ . Locally, we use the dist-directory for temporary storage. When debugging, you can check that location for files and file-structure. + Prerequisites for publishing: + 1. Account: + Register at https://central.sonatype.com/ and ensure you have access to the + 'org.sosy-lab' namespace. + 2. PGP Key: + - You need a GPG key pair (RSA 2048-bit or higher). + - Your public key MUST be published to a supported keyserver: + e.g., 'gpg - -keyserver keyserver.ubuntu.com - -send-keys ' + - The passphrase can be provided via '-Dgpg.passphrase=...' or in build.properties. + 3. Authentication Token: + - Log in to https://central.sonatype.com/, go to 'Account', and 'Generate User Token'. + - Add the credentials to your '~/.m2/settings.xml' as follows: + + SonatypeCentral + TOKEN_NAME + TOKEN_PASSWORD + + Usage: ant publish-to-maven-central -Dpublish.component=z3 -Dpublish.version=4.16.0 ant publish-to-maven-central -Dpublish.component=java-smt -Dpublish.version=5.0.0 @@ -33,11 +51,6 @@ SPDX-License-Identifier: Apache-2.0 - - From 312cb0452697830a0e59e817c3927061b9ba83d4 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 31 Mar 2026 14:47:40 +0200 Subject: [PATCH 07/30] simplify and unify upload steps. --- build/build-maven-central.xml | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/build/build-maven-central.xml b/build/build-maven-central.xml index 2209e82ece..7b13f73e85 100644 --- a/build/build-maven-central.xml +++ b/build/build-maven-central.xml @@ -96,6 +96,10 @@ SPDX-License-Identifier: Apache-2.0 + + + + @@ -238,21 +242,18 @@ SPDX-License-Identifier: Apache-2.0 - - - - - - - + + + + - + - + @@ -260,7 +261,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -273,9 +274,6 @@ SPDX-License-Identifier: Apache-2.0 - - - From 9f26bed54b5ced0a0e50040a1ffe9a4d97b78b12 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 31 Mar 2026 15:19:51 +0200 Subject: [PATCH 08/30] improve documentation --- build/build-maven-central.xml | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/build/build-maven-central.xml b/build/build-maven-central.xml index 7b13f73e85..6cec1ca722 100644 --- a/build/build-maven-central.xml +++ b/build/build-maven-central.xml @@ -46,6 +46,17 @@ SPDX-License-Identifier: Apache-2.0 Usage: ant publish-to-maven-central -Dpublish.component=z3 -Dpublish.version=4.16.0 ant publish-to-maven-central -Dpublish.component=java-smt -Dpublish.version=5.0.0 + + Finalizing Publication: + 1. Review and Publish: + - Log in to https://central.sonatype.com/publishing/deployments. + - Check that the deployment is validated and contains all expected files. + - Click 'Publish' to start the release process. + 2. Wait for Sync: + - It usually takes about 15-30 minutes for the artifacts to appear in + Maven Central (https://repo1.maven.org/maven2/org/sosy-lab/). + Applications can then download the artifacts using the specified version. + - Search results on https://central.sonatype.com/ might take longer to update. --> From 8c82e1fd25d8691f709f71a02947580fb3be5b71 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 31 Mar 2026 22:40:18 +0200 Subject: [PATCH 09/30] fix Maven directory structure. In Maven, Jars usually do not use "artifact" pattern for plain jars, except for cases like "source"/"javadoc". --- build/build-maven-central.xml | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/build/build-maven-central.xml b/build/build-maven-central.xml index 6cec1ca722..838d8ffd76 100644 --- a/build/build-maven-central.xml +++ b/build/build-maven-central.xml @@ -128,12 +128,29 @@ SPDX-License-Identifier: Apache-2.0 + + conf="${resolve.confs}" + type="shared-object,dll,dylib"/> From ea6e49fa0b9e399b76d32e4a25694ec0c1c18a69 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 31 Mar 2026 23:16:48 +0200 Subject: [PATCH 10/30] fix Maven directory structure: exclude signature-files from hashing. --- build/build-maven-central.xml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/build/build-maven-central.xml b/build/build-maven-central.xml index 838d8ffd76..76f79c5091 100644 --- a/build/build-maven-central.xml +++ b/build/build-maven-central.xml @@ -189,9 +189,9 @@ SPDX-License-Identifier: Apache-2.0 - + - + From 823364e4dfe6789971da053772c16e6b73246b16 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 1 Apr 2026 01:22:06 +0200 Subject: [PATCH 11/30] fix Maven bundle: exclude transitive dependencies. The POM file will contain the dependencies section, and it will reference the latest versions of dependencies, not the actual dependencies. --- build/build-maven-central.xml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/build/build-maven-central.xml b/build/build-maven-central.xml index 76f79c5091..c1c4b40aa9 100644 --- a/build/build-maven-central.xml +++ b/build/build-maven-central.xml @@ -73,9 +73,14 @@ SPDX-License-Identifier: Apache-2.0 - + + + + + + @@ -124,7 +129,8 @@ SPDX-License-Identifier: Apache-2.0 conf="${resolve.confs}" log="download-only" inline="true" - keep="true"/> + keep="true" + transitive="false"/> - - - - @@ -132,6 +123,15 @@ SPDX-License-Identifier: Apache-2.0 keep="true" transitive="false"/> + + + + - From 65750ad86d867968f157e1cc30633af11e92decc Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 1 Apr 2026 09:00:12 +0200 Subject: [PATCH 13/30] remove outdated Ant-script for publishing artifacts in Maven. The old script was limited to OSSRH only, which was shut down in June 2025. The updated replacement is available in build/build-maven-central. --- build/build-maven-publish.xml | 278 ---------------------------------- 1 file changed, 278 deletions(-) delete mode 100644 build/build-maven-publish.xml diff --git a/build/build-maven-publish.xml b/build/build-maven-publish.xml deleted file mode 100644 index 2e33b35b6f..0000000000 --- a/build/build-maven-publish.xml +++ /dev/null @@ -1,278 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - sosy_lab - sosy-lab - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - From 3b20e1be345feaf997cf84ee36f0a92e3e725818 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Thu, 2 Apr 2026 01:19:30 +0200 Subject: [PATCH 14/30] remove outdated Ant-script for publishing artifacts in Maven. --- build.xml | 1 - 1 file changed, 1 deletion(-) diff --git a/build.xml b/build.xml index 1718992d82..768b7b8bd7 100644 --- a/build.xml +++ b/build.xml @@ -66,7 +66,6 @@ SPDX-License-Identifier: Apache-2.0 - From 61445f69cadf756393176b41e7d6adcabcacfa57 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Thu, 2 Apr 2026 01:19:33 +0200 Subject: [PATCH 15/30] rename pom-template to match its component name. --- ...es2_pom_template.xml => maven_javasmt-yices2_pom_template.xml} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename solvers_maven_conf/{maven_javasmt_yices2_pom_template.xml => maven_javasmt-yices2_pom_template.xml} (100%) diff --git a/solvers_maven_conf/maven_javasmt_yices2_pom_template.xml b/solvers_maven_conf/maven_javasmt-yices2_pom_template.xml similarity index 100% rename from solvers_maven_conf/maven_javasmt_yices2_pom_template.xml rename to solvers_maven_conf/maven_javasmt-yices2_pom_template.xml From e45ea5680b5308fc02411e1990fa90353a787cbe Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Thu, 2 Apr 2026 01:19:35 +0200 Subject: [PATCH 16/30] improve script with options for testing. --- build/build-maven-central.xml | 32 ++++++++++++++++++++++++-------- 1 file changed, 24 insertions(+), 8 deletions(-) diff --git a/build/build-maven-central.xml b/build/build-maven-central.xml index 52cf1a1c41..e0c6f96d82 100644 --- a/build/build-maven-central.xml +++ b/build/build-maven-central.xml @@ -44,8 +44,11 @@ SPDX-License-Identifier: Apache-2.0 Usage: - ant publish-to-maven-central -Dpublish.component=z3 -Dpublish.version=4.16.0 - ant publish-to-maven-central -Dpublish.component=java-smt -Dpublish.version=5.0.0 + ant publish-to-maven-central -Dpublish.component=z3 -Dpublish.version=4.16.0 + ant publish-to-maven-central -Dpublish.component=javasmt_yices2 -Dpublish.version=6.0.0-141-g04134287c + ant publish-to-maven-central -Dpublish.component=java-smt -Dpublish.version=5.0.0 + + For testing without upload, add option '-Dpublish.upload=false'. Finalizing Publication: 1. Review and Publish: @@ -63,6 +66,7 @@ SPDX-License-Identifier: Apache-2.0 + @@ -85,14 +89,19 @@ SPDX-License-Identifier: Apache-2.0 + - - + + + + + + - + @@ -107,6 +116,9 @@ SPDX-License-Identifier: Apache-2.0 + + + @@ -165,7 +177,7 @@ SPDX-License-Identifier: Apache-2.0 - @@ -254,7 +266,7 @@ SPDX-License-Identifier: Apache-2.0 --> - + @@ -315,6 +327,10 @@ SPDX-License-Identifier: Apache-2.0 - + + + + \ No newline at end of file From f41b87159abbeb7a2935228266924074ad84dfd5 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Thu, 2 Apr 2026 01:19:37 +0200 Subject: [PATCH 17/30] adding script for testing bundles before pushing them to Maven. split off retrieval of JavaSMT's own jars. use full name for components to make the script more flexible and developer friendly. --- build/build-maven-central.xml | 162 ++++++++++++++------- scripts/test-maven-central-bundle.sh | 210 +++++++++++++++++++++++++++ 2 files changed, 321 insertions(+), 51 deletions(-) create mode 100644 scripts/test-maven-central-bundle.sh diff --git a/build/build-maven-central.xml b/build/build-maven-central.xml index e0c6f96d82..3dbbe1781e 100644 --- a/build/build-maven-central.xml +++ b/build/build-maven-central.xml @@ -44,11 +44,13 @@ SPDX-License-Identifier: Apache-2.0 Usage: - ant publish-to-maven-central -Dpublish.component=z3 -Dpublish.version=4.16.0 - ant publish-to-maven-central -Dpublish.component=javasmt_yices2 -Dpublish.version=6.0.0-141-g04134287c + ant publish-to-maven-central -Dpublish.component=javasmt-solver-z3 -Dpublish.version=4.16.0 + ant publish-to-maven-central -Dpublish.component=javasmt-yices2 -Dpublish.version=6.0.0-141-g04134287c ant publish-to-maven-central -Dpublish.component=java-smt -Dpublish.version=5.0.0 For testing without upload, add option '-Dpublish.upload=false'. + Additionally, we provide a script for testing and debugging the bundle process: + scripts/test-maven-central-bundle.sh Finalizing Publication: 1. Review and Publish: @@ -69,40 +71,46 @@ SPDX-License-Identifier: Apache-2.0 - + - - - - - - - - - - + - + - - - - + + + - - + + + + + + + + + + + + + @@ -125,16 +133,6 @@ SPDX-License-Identifier: Apache-2.0 - - - + dest="${ivy.resolved.file}"/> + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - To align with standard Maven conventions for JAR and POM files, - we do not include the artifact name (Java package name) in the file name. + + + - - Jars: plain name as [module]-[revision](-[classifier]).jar - - Other artifacts: name including the artifact name (library name), - i.e., [module]-[revision]-[artifact](-[arch])(-[classifier]).[ext] + + + - Technical hint: - The first retrieve uses "sync=true" to ensure a clean/empty directory. - The second retrieve uses "sync=false" to _not_ delete files from the first retrieve. - --> + + + + + + + + + - + + + + + conf="*"> - - - - sosy_lab - sosy-lab - - diff --git a/scripts/test-maven-central-bundle.sh b/scripts/test-maven-central-bundle.sh new file mode 100644 index 0000000000..c923cda983 --- /dev/null +++ b/scripts/test-maven-central-bundle.sh @@ -0,0 +1,210 @@ +#!/usr/bin/env bash + +# +# 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 +# + +set -e + +# Colors +RED='\033[0;31m' +GREEN='\033[0;32m' +YELLOW='\033[1;33m' +BLUE='\033[0;34m' +NC='\033[0m' # No Color + +# Extensions to check for each base file +EXTENSIONS=("" ".asc" ".md5" ".sha1" ".sha256" ".sha512") + +# Ensure script is run from project root +if [[ ! -f "build.xml" ]]; then + echo -e "${RED}Error: This script must be run from the project root.${NC}" + exit 1 +fi + +verify_bundle() { + local COMPONENT=$1 + local VERSION=$2 + local FULL_NAME=$3 + local EXPECTED_DEP_STATUS=$4 # "none", "compile", or "compile+optional" + shift 4 + local BASE_FILES=("$@") + + local REL_DIR="org/sosy-lab/${FULL_NAME}/${VERSION}" + local ZIP_FILE="dist/maven-central-bundle/${COMPONENT}-${VERSION}-bundle.zip" + local TEMP_DIR=$(mktemp -d) + local POM_FILE="${TEMP_DIR}/${REL_DIR}/${FULL_NAME}-${VERSION}.pom" + + echo -e "${BLUE}------------------------------------------------------------${NC}" + echo -e "${YELLOW}Testing component: ${COMPONENT} (version: ${VERSION})${NC}" + echo -e "${BLUE}------------------------------------------------------------${NC}" + + # Cleanup local bundle dir for this component if it exists + rm -rf "dist/maven-central-bundle/${REL_DIR}" + + # Execute ant command + echo -e "${BLUE}Executing ant publish-to-maven-central...${NC}" + ant publish-to-maven-central -Dpublish.component="${COMPONENT}" -Dpublish.version="${VERSION}" -Dpublish.upload=false + echo -e "${BLUE}------------------------------------------------------------${NC}" + + # Check if zip file exists + if [[ ! -f "${ZIP_FILE}" ]]; then + echo -e "${RED}Error: Zip file ${ZIP_FILE} was not created.${NC}" + exit 1 + fi + + # Unzip to temp directory + echo -e "${BLUE}Unzipping bundle for verification...${NC}" + unzip -q "${ZIP_FILE}" -d "${TEMP_DIR}" + + # Verify file structure + echo -e "${BLUE}Verifying file structure in the zip bundle...${NC}" + + local EXPECTED_FILES_FILE="${TEMP_DIR}/expected_files.txt" + local ACTUAL_FILES_FILE="${TEMP_DIR}/actual_files.txt" + + # Generate expected files list + for base in "${BASE_FILES[@]}"; do + for ext in "${EXTENSIONS[@]}"; do + echo "${REL_DIR}/${base}${ext}" >> "${EXPECTED_FILES_FILE}" + done + done + sort -o "${EXPECTED_FILES_FILE}" "${EXPECTED_FILES_FILE}" + + # Generate actual files list + find "${TEMP_DIR}/${REL_DIR}" -type f | sed "s|^${TEMP_DIR}/||" | sort > "${ACTUAL_FILES_FILE}" + + # Compare lists + local DIFF=$(diff -u "${EXPECTED_FILES_FILE}" "${ACTUAL_FILES_FILE}" || true) + + local FAILED=0 + if [[ -n "${DIFF}" ]]; then + echo -e "${RED}Verification failed for ${COMPONENT}!${NC}" + echo "Differences found:" + echo "${DIFF}" + FAILED=1 + fi + + # Verify POM content (dependencies) + echo -e "${BLUE}Verifying POM content (dependencies) for ${COMPONENT}...${NC}" + if [[ "$EXPECTED_DEP_STATUS" == "none" ]]; then + if grep -q "" "$POM_FILE"; then + echo -e "${RED}Error: POM for ${COMPONENT} should not have dependencies.${NC}" + FAILED=1 + fi + elif [[ "$EXPECTED_DEP_STATUS" == "compile" ]]; then + if ! grep -q "compile" "$POM_FILE"; then + echo -e "${RED}Error: POM for ${COMPONENT} should have compile dependencies.${NC}" + FAILED=1 + fi + if grep -q "true" "$POM_FILE"; then + echo -e "${RED}Error: POM for ${COMPONENT} should not have optional dependencies.${NC}" + FAILED=1 + fi + elif [[ "$EXPECTED_DEP_STATUS" == "compile+optional" ]]; then + if ! grep -q "compile" "$POM_FILE"; then + echo -e "${RED}Error: POM for ${COMPONENT} should have compile dependencies.${NC}" + FAILED=1 + fi + if ! grep -q "true" "$POM_FILE"; then + echo -e "${RED}Error: POM for ${COMPONENT} should have optional dependencies.${NC}" + FAILED=1 + fi + fi + + rm -rf "${TEMP_DIR}" + if [[ $FAILED -eq 0 ]]; then + echo -e "${GREEN}Verification successful for ${COMPONENT}!${NC}" + return 0 + else + return 1 + fi +} + +# Cleanup all bundles before starting +echo -e "${YELLOW}Cleaning up dist/ directory...${NC}" +rm -rf dist/maven-central-bundle + +FAILED_TESTS=0 + +# Test case: Z3 +Z3_VERSION="4.16.0" +Z3_FULL_NAME="javasmt-solver-z3" +Z3_BASE_FILES=( + "${Z3_FULL_NAME}-${Z3_VERSION}.jar" + "${Z3_FULL_NAME}-${Z3_VERSION}.pom" + "${Z3_FULL_NAME}-${Z3_VERSION}-javadoc.jar" + "${Z3_FULL_NAME}-${Z3_VERSION}-sources.jar" + "${Z3_FULL_NAME}-${Z3_VERSION}-libz3-arm64.dll" + "${Z3_FULL_NAME}-${Z3_VERSION}-libz3-arm64.dylib" + "${Z3_FULL_NAME}-${Z3_VERSION}-libz3-arm64.so" + "${Z3_FULL_NAME}-${Z3_VERSION}-libz3-x64.dll" + "${Z3_FULL_NAME}-${Z3_VERSION}-libz3-x64.dylib" + "${Z3_FULL_NAME}-${Z3_VERSION}-libz3-x64.so" + "${Z3_FULL_NAME}-${Z3_VERSION}-libz3java-arm64.dll" + "${Z3_FULL_NAME}-${Z3_VERSION}-libz3java-arm64.dylib" + "${Z3_FULL_NAME}-${Z3_VERSION}-libz3java-arm64.so" + "${Z3_FULL_NAME}-${Z3_VERSION}-libz3java-x64.dll" + "${Z3_FULL_NAME}-${Z3_VERSION}-libz3java-x64.dylib" + "${Z3_FULL_NAME}-${Z3_VERSION}-libz3java-x64.so" +) + +if ! verify_bundle "javasmt-solver-z3" "${Z3_VERSION}" "${Z3_FULL_NAME}" "none" "${Z3_BASE_FILES[@]}"; then + FAILED_TESTS=$((FAILED_TESTS + 1)) +fi + +# Test case: MathSAT +MATHSAT_VERSION="5.6.10" +MATHSAT_FULL_NAME="javasmt-solver-mathsat" +MATHSAT_BASE_FILES=( + "${MATHSAT_FULL_NAME}-${MATHSAT_VERSION}-libmathsat5j.so" + "${MATHSAT_FULL_NAME}-${MATHSAT_VERSION}-mathsat.dll" + "${MATHSAT_FULL_NAME}-${MATHSAT_VERSION}-mathsat5j.dll" + "${MATHSAT_FULL_NAME}-${MATHSAT_VERSION}-mpir.dll" + "${MATHSAT_FULL_NAME}-${MATHSAT_VERSION}.pom" +) + +if ! verify_bundle "javasmt-solver-mathsat" "${MATHSAT_VERSION}" "${MATHSAT_FULL_NAME}" "none" "${MATHSAT_BASE_FILES[@]}"; then + FAILED_TESTS=$((FAILED_TESTS + 1)) +fi + +# Test case: JavaSMT-bindings for Yices2 +YICES_VERSION="6.0.0-141-g04134287c" +YICES_FULL_NAME="javasmt-yices2" +YICES_BASE_FILES=( + "${YICES_FULL_NAME}-${YICES_VERSION}.jar" + "${YICES_FULL_NAME}-${YICES_VERSION}.pom" + "${YICES_FULL_NAME}-${YICES_VERSION}-sources.jar" +) + +if ! verify_bundle "javasmt-yices2" "${YICES_VERSION}" "${YICES_FULL_NAME}" "compile+optional" "${YICES_BASE_FILES[@]}"; then + FAILED_TESTS=$((FAILED_TESTS + 1)) +fi + +# Test case: JavaSMT (Core) +JAVASMT_VERSION="5.0.0" +JAVASMT_FULL_NAME="java-smt" +JAVASMT_BASE_FILES=( + "${JAVASMT_FULL_NAME}-${JAVASMT_VERSION}.jar" + "${JAVASMT_FULL_NAME}-${JAVASMT_VERSION}.pom" + "${JAVASMT_FULL_NAME}-${JAVASMT_VERSION}-sources.jar" +) + +if ! verify_bundle "java-smt" "${JAVASMT_VERSION}" "${JAVASMT_FULL_NAME}" "compile+optional" "${JAVASMT_BASE_FILES[@]}"; then + FAILED_TESTS=$((FAILED_TESTS + 1)) +fi + +echo -e "${BLUE}------------------------------------------------------------${NC}" +if [[ $FAILED_TESTS -eq 0 ]]; then + echo -e "${GREEN}All tests passed successfully!${NC}" + exit 0 +else + echo -e "${RED}$FAILED_TESTS test(s) failed!${NC}" + exit 1 +fi From bc0335171acfb666e182e9065094292f6165affe Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Thu, 2 Apr 2026 10:43:45 +0200 Subject: [PATCH 18/30] fix naming in pom-file --- build/build-maven-central.xml | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/build/build-maven-central.xml b/build/build-maven-central.xml index 3dbbe1781e..3424cfe74b 100644 --- a/build/build-maven-central.xml +++ b/build/build-maven-central.xml @@ -233,6 +233,7 @@ SPDX-License-Identifier: Apache-2.0 + + + + sosy_lab + sosy-lab + + @@ -281,7 +288,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -328,7 +335,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -391,6 +398,6 @@ SPDX-License-Identifier: Apache-2.0 - \ No newline at end of file From 66cb7398499748e8c0021efd34128408bd0482ee Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 6 Apr 2026 10:52:25 +0200 Subject: [PATCH 19/30] lets include JavaDoc in JavaSMT releases. --- build/build-maven-central.xml | 2 ++ scripts/test-maven-central-bundle.sh | 3 ++- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/build/build-maven-central.xml b/build/build-maven-central.xml index 3424cfe74b..517fd77e47 100644 --- a/build/build-maven-central.xml +++ b/build/build-maven-central.xml @@ -224,6 +224,8 @@ SPDX-License-Identifier: Apache-2.0 dest="${bundle.dir}/${publish.full-name}-${publish.version}.jar"/> + diff --git a/scripts/test-maven-central-bundle.sh b/scripts/test-maven-central-bundle.sh index c923cda983..fe83da8cb9 100644 --- a/scripts/test-maven-central-bundle.sh +++ b/scripts/test-maven-central-bundle.sh @@ -188,12 +188,13 @@ if ! verify_bundle "javasmt-yices2" "${YICES_VERSION}" "${YICES_FULL_NAME}" "com fi # Test case: JavaSMT (Core) -JAVASMT_VERSION="5.0.0" +JAVASMT_VERSION="6.0.0" JAVASMT_FULL_NAME="java-smt" JAVASMT_BASE_FILES=( "${JAVASMT_FULL_NAME}-${JAVASMT_VERSION}.jar" "${JAVASMT_FULL_NAME}-${JAVASMT_VERSION}.pom" "${JAVASMT_FULL_NAME}-${JAVASMT_VERSION}-sources.jar" + "${JAVASMT_FULL_NAME}-${JAVASMT_VERSION}-javadoc.jar" ) if ! verify_bundle "java-smt" "${JAVASMT_VERSION}" "${JAVASMT_FULL_NAME}" "compile+optional" "${JAVASMT_BASE_FILES[@]}"; then From 249031d246e0cd12ac53a36bd169db1c4010da88 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 6 Apr 2026 10:52:27 +0200 Subject: [PATCH 20/30] update some documentation with new version numbers --- doc/Getting-started.md | 76 ++++++++++++++++++++++++++---------------- 1 file changed, 48 insertions(+), 28 deletions(-) diff --git a/doc/Getting-started.md b/doc/Getting-started.md index 8ee5819ffb..0e5bcde1bd 100644 --- a/doc/Getting-started.md +++ b/doc/Getting-started.md @@ -68,43 +68,58 @@ For Maven: org.sosy-lab java-smt - 5.0.0-61-gea80187e + 6.0.0 ``` -Currently, only `SMTInterpol` and `Princess` are automatically fetched from Maven Central, -because they are written in Java and Scala, and thus are available on every machine. -Shared object for other solvers, such as `MathSAT5` and `Z3`, can be added by using additional -dependencies (example for Linux x64): +Since release 6.0.0, JavaSMT does no longer include Java-based solvers automatically, but instead provides them as separate dependencies. +This unifies the installation process for all solvers and allows users to only install the solvers they need. +Solvers, such as `MathSAT5`, `SMTInterpol` and `Z3`, can be added by using additional dependencies (example for Linux x64): ```xml - + org.sosy-lab javasmt-solver-mathsat5 - 5.6.5 + 5.6.15 + libmathsat5j-x64 so - + + + de.uni-freiburg.informatik.ultimate + smtinterpol + 2.5-1242-g5c50fb6d + + + org.sosy-lab javasmt-solver-z3 - 4.8.10 + 4.15.4 org.sosy-lab javasmt-solver-z3 - 4.8.10 + 4.15.4 + libz3-x64 so - libz3 org.sosy-lab javasmt-solver-z3 - 4.8.10 + 4.15.4 + libz3java-x64 so - libz3java ``` @@ -112,11 +127,13 @@ The XML snippets for other solvers available via Maven, such as `Boolector`, `CVC4`, `CVC5`, `OpenSMT`, `Princess`, and `Yices2`, can be found in the [`POM file`](Example-Maven-Project/pom.xml) of our [`Example-Maven-Project`](Example-Maven-Project). -If you are not using Linux and we provide a solver binary for your system, -you might need to set the dependencies accordingly, e.g., +If you are not using Linux, but Windows or macOS, or if you want to use a different architecture, +such as `arm64`, you might need to set the dependencies accordingly, e.g., change the type from `so` to `dll` (for Windows) or `dylib` (for macOS), and specify an architecture (e.g., `x64` or `arm64`). -You can look up the required dependency files and filename extension in the [Ivy repository][]. +You can look up the required dependency files and filename extension in the [Ivy repository][] or [Maven Central][]. +Note that some solvers are not available for all platforms, +so you might need to check the [Readme](../README.md) for supported platforms and solvers. Additionally, you can add and configure some Maven plugins to load the libraries automatically and place them in the correct directories when assembling your application. @@ -142,8 +159,8 @@ And finally configure the classpath for your jar-plugin: ``` -See [`Example-Maven-Project`](Example-Maven-Project) for more information and a working example. -See [`Example-Maven-Web-Project`](Example-Maven-Web-Project) for more information about a Dynamic-Web-Project runnable by Tomcat 9. +See [`Example-Maven-Project`](Example-Maven-Project) for more information and a working example application. +See [`Example-Maven-Web-Project`](Example-Maven-Web-Project) for more information about a Dynamic-Web-Project runnable by Tomcat. ### Manual Installation @@ -156,25 +173,24 @@ In order to perform the manual installation, the following steps should be follo **JavaSMT might not yet support the latest version on the solver's webpage, but only the latest version in the [Ivy index](https://www.sosy-lab.org/ivy/org.sosy_lab/java-smt/). Please file an issue, if the update of a solver library is required.** - - Suppose the version `5.0.0` was chosen. - Ivy description file [`ivy-5.0.0.xml`](https://www.sosy-lab.org/ivy/org.sosy_lab/java-smt/ivy-5.0.0.xml) can + - Suppose the version `6.0.0` was chosen. + Ivy description file [`ivy-6.0.0.xml`](https://www.sosy-lab.org/ivy/org.sosy_lab/java-smt/ivy-6.0.0.xml) can be consulted in order to determine all the files which should be fetched. - The artifacts tag specifies what files the release depends on. - In the example case, those are `java-smt-5.0.0.jar` and (optionally) - `java-smt-5.0.0-sources.jar`, located in the same directory. + In the example case, those are `java-smt-6.0.0.jar` and (optionally) + `java-smt-6.0.0-sources.jar`, located in the same directory. - Finally, the dependencies can be manually followed and resolved. - E.g. in the example, Z3 version `4.13.3` is specified, - which is described by the corresponding [XML](https://www.sosy-lab.org/ivy/org.sosy_lab/javasmt-solver-z3/ivy-4.13.3.xml) + E.g. in the example, Z3 version `4.15.4` is specified, + which is described by the corresponding [XML](https://www.sosy-lab.org/ivy/org.sosy_lab/javasmt-solver-z3/ivy-4.15.4.xml) file, specifying what binaries should be fetched from the corresponding [directory](https://www.sosy-lab.org/ivy/org.sosy_lab/javasmt-solver-z3/). ### Binaries for Native Solvers -When using Ivy or Maven for installation on a 64-bit Linux platform, +When using Ivy for installation on a 64-bit Linux platform, solver binaries for native solvers are downloaded automatically, if available. The [Readme](../README.md) contains a list of solvers and supported platforms. -Everything should work as is after installation. Without Ivy or Maven you need to download and install the binaries manually as described above under [Manual Installation](#manual-installation). You can either copy them into the directory of the JavaSMT JAR file, @@ -229,7 +245,9 @@ can just use the JavaSMT API as follows: If you want to use a custom loading mechanism, you can do so by implementing a simple consumer interface and passing it to the `SolverContextFactory`. -The following example uses the default Java class loader to load the native libraries: +The following example uses the default Java class loader to load the native libraries, +depending on the default environment variables `JAVA_LIBRARY_PATH` and `LD_LIBRARY_PATH` +or option `-Djava.library.path`: ```java SolverContext context = SolverContextFactory.createSolverContext( @@ -305,7 +323,9 @@ Once the constraint is generated, we can solve it and get the model: prover.addConstraint(constraint); boolean isUnsat = prover.isUnsat(); if (!isUnsat) { - Model model = prover.getModel(); + try (Model model = prover.getModel()) { + // Do something with the model + } } } ``` From fb005f9bfefe6c9cf36d4b3ea9c285be67be610d Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 6 Apr 2026 10:52:30 +0200 Subject: [PATCH 21/30] migrate example project to JavaSMT 6.0.0, and simplify some build steps in Maven, and update documentation --- doc/Example-Maven-Project/README.md | 79 +++- doc/Example-Maven-Project/pom.xml | 423 +++++++----------- .../sosy_lab/java_smt_example/SudokuTest.java | 35 +- 3 files changed, 234 insertions(+), 303 deletions(-) diff --git a/doc/Example-Maven-Project/README.md b/doc/Example-Maven-Project/README.md index 6265b7c474..86968a821a 100644 --- a/doc/Example-Maven-Project/README.md +++ b/doc/Example-Maven-Project/README.md @@ -3,24 +3,75 @@ This file is part of JavaSMT, an API wrapper for a collection of SMT solvers: https://github.com/sosy-lab/java-smt -SPDX-FileCopyrightText: 2021 Dirk Beyer +SPDX-FileCopyrightText: 2026 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> -This is an example application for using JavaSMT with Maven. -The example application prints a table of the available SMT solvers, -their version number and supported features. +# JavaSMT Maven Example -The Maven workflow in this project supports the following steps: +This project shows how to use JavaSMT in a Maven-based environment. +It includes a main application that lists available solvers and a test case that solves a Sudoku puzzle. +The configuration in `pom.xml` handles the download and setup of native solver libraries (e.g., Z3, MathSAT5, CVC5) so they can be loaded by the JVM. -- Compiling: `mvn compile` downloads all dependencies and compiles the project. -- Testing: `mvn test` executes the Sudoku example test. -- Packaging: `mvn package` creates a jar file for the example application. - Dependencies like other jar files and binaries for SMT solvers are stored in the directory `dependencies`. -- Running: `java -jar ./target/java-smt-maven-example-VERSION.jar` shows a table in the terminal. +## Prerequisites -Please note that the Maven repository currently only contains release versions -and no snapshots, thus the newest features and bugfixes might be missing. -If a Maven step is not working or more steps are required, -please ask or report an issue [in the project](https://github.com/sosy-lab/java-smt). +* Java 17 or newer. +* Apache Maven. +* Native solvers are only provided for **Linux x64** in this example. + Some solvers like Z3 and MathSAT5 also support Windows or ARM64 platform, if dependencies are adjusted in `pom.xml`. + Java-only solvers (SMTInterpol, Princess) work on all platforms. +* When using Linux, please use Ubuntu 24.04 or newer, as we provide latest solver versions for GLIBC_2.33 or newer. + +## Usage + +### Compile and Build + +Run the following to download dependencies and build the project: +```bash +mvn clean compile +``` +Native libraries will be copied and renamed in `target/dependency`. + +### Run the Solver Overview Table + +This application prints a table of detected solvers and their features. + +```bash +mvn package +java -jar ./target/java-smt-maven-example-VERSION.jar +``` + +Or via Maven, using the preconfigured execution configuration from `pom.xml`: +```bash +mvn compile exec:exec +``` + +Or via Maven, with explicit arguments to set the library path: +```bash +mvn compile exec:exec -Dexec.executable="java" -Dexec.args="-Djava.library.path=target/dependency -cp %classpath org.sosy_lab.java_smt_example.SolverOverviewTable" +``` + +### Run Sudoku Test + +The `SudokuTest` runs against all available solvers. + +```bash +mvn test +``` + +## Project Structure + +* `src/main/java/org/sosy_lab/java_smt_example/SolverOverviewTable.java`: Main application. +* `src/test/java/org/sosy_lab/java_smt_example/SudokuTest.java`: Parameterized JUnit test. +* `pom.xml`: Maven configuration including dependency management and native library handling. + +## Native Library Handling + +JavaSMT backends often require native binaries. This project automates the following steps: +1. Download native libraries via Maven dependencies (using `classifier` and `type`). +2. Copy them to `target/dependency` using `maven-dependency-plugin`. +3. Rename them (e.g., from `javasmt-solver-z3-libz3java-x64.so` to `libz3java.so`) using `maven-antrun-plugin` to match JavaSMT expectations. +4. Set `java.library.path` to this directory during execution. + +For more details, see the [JavaSMT documentation](https://github.com/sosy-lab/java-smt). diff --git a/doc/Example-Maven-Project/pom.xml b/doc/Example-Maven-Project/pom.xml index f182b2cb49..1f550263f4 100644 --- a/doc/Example-Maven-Project/pom.xml +++ b/doc/Example-Maven-Project/pom.xml @@ -16,7 +16,7 @@ SPDX-License-Identifier: Apache-2.0 org.sosy_lab.java_smt_example java-smt-maven-example - 1.12 + 2.0 java-smt-maven-example Example Maven project to show how to use JavaSMT with native solver libraries. https://github.com/sosy-lab/java-smt @@ -73,29 +73,51 @@ SPDX-License-Identifier: Apache-2.0 x64 - 5.0.0 - 0.7.0-13.1-g595512ae + 6.0.0 + 0.8.2-339-g550ed911 3.2.2-g1a89c229 1.8-prerelease-2020-06-24-g7825d8f28 - 1.0.5-g4cb2ab9eb - 5.6.11-glibc2.27 - 2.8.0-sosy0-ge831bf23 - 4.1.1-734-g3732f7e08 - 2.6.2-396-g194350c1 - 4.13.4 + 2026-02-26-d22638a + 5.6.15 + 2.9.0-gef441e1c + 2.5-1242-g5c50fb6d + 2025-11-17 + 2.0 + 5.0.1-1258-gdad634a69 + 2.6.4-264-g553897f5 + 4.15.4 + 4.5.0-gd57a2a6dc + org.sosy-lab java-smt ${javasmt.version} + + + de.uni-freiburg.informatik.ultimate + smtinterpol + ${smtinterpol.version} + + + io.github.uuverifiers + princess_2.13 + ${princess.version} + + + io.github.uuverifiers + ostrich_2.13 + ${ostrich.version} + + org.sosy-lab - javasmt-solver-mathsat5 + javasmt-solver-mathsat ${mathsat.version} libmathsat5j-${system.arch} so @@ -122,12 +144,33 @@ SPDX-License-Identifier: Apache-2.0 libz3java-${system.arch} + + + org.sosy-lab + javasmt-solver-z3-legacy + ${z3-legacy.version} + com.microsoft.z3legacy + + + org.sosy-lab + javasmt-solver-z3-legacy + ${z3-legacy.version} + so + libz3legacy-${system.arch} + + + org.sosy-lab + javasmt-solver-z3-legacy + ${z3-legacy.version} + so + libz3javalegacy-${system.arch} + + org.sosy-lab javasmt-solver-bitwuzla ${bitwuzla.version} - jar org.sosy-lab @@ -165,7 +208,6 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-cvc4 ${cvc4.version} - jar CVC4 @@ -190,48 +232,18 @@ SPDX-License-Identifier: Apache-2.0 libcvc4parser - - - org.sosy-lab - javasmt-solver-cvc5 - ${cvc5.version} - jar - cvc5 - + org.sosy-lab javasmt-solver-cvc5 ${cvc5.version} - so - libcvc5 org.sosy-lab javasmt-solver-cvc5 ${cvc5.version} so - libcvc5jni - - - org.sosy-lab - javasmt-solver-cvc5 - ${cvc5.version} - so - libcvc5parser - - - org.sosy-lab - javasmt-solver-cvc5 - ${cvc5.version} - so - libpoly - - - org.sosy-lab - javasmt-solver-cvc5 - ${cvc5.version} - so - libpolyxx + libcvc5jni-${system.arch} @@ -239,7 +251,12 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-yices2 ${javasmt-yices.version} - jar + + + org.sosy-lab + javasmt-solver-yices2 + + org.sosy-lab @@ -254,7 +271,6 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-opensmt ${opensmt.version} - jar org.sosy-lab @@ -274,225 +290,110 @@ SPDX-License-Identifier: Apache-2.0 - - - - - maven-surefire-plugin - 2.22.1 - - - -Djava.library.path=${project.dependency.path} - - - - maven-jar-plugin - 3.0.2 - - - - - true - ${project.dependency.relativepath} - org.sosy_lab.java_smt_example.SolverOverviewTable - - - - - - - - - org.apache.maven.plugins - maven-dependency-plugin - 3.1.1 - - - - copy - initialize - - copy - - - - - - copy-dependencies - validate - - copy-dependencies - - - - - ${project.dependency.path} - - - - - - - org.sosy-lab - javasmt-solver-mathsat5 - so - libmathsat5j-${system.arch} - libmathsat5j.so - - - - - org.sosy-lab - javasmt-solver-z3 - so - libz3java-${system.arch} - libz3java.so - - - org.sosy-lab - javasmt-solver-z3 - so - libz3-${system.arch} - libz3.so - - - - - org.sosy-lab - javasmt-solver-bitwuzla - so - libbitwuzlaj-${system.arch} - libbitwuzlaj.so - - - - - org.sosy-lab - javasmt-solver-boolector - so - libboolector - libboolector.so - - - org.sosy-lab - javasmt-solver-boolector - so - libminisat - libminisat.so - - - org.sosy-lab - javasmt-solver-boolector - so - libpicosat - libpicosat.so - - - - - org.sosy-lab - javasmt-solver-cvc4 - so - libcvc4 - libcvc4.so - - - org.sosy-lab - javasmt-solver-cvc4 - so - libcvc4jni - libcvc4jni.so - - - org.sosy-lab - javasmt-solver-cvc4 - so - libcvc4parser - libcvc4parser.so - + + + org.apache.maven.plugins + maven-surefire-plugin + 3.5.4 + + -Djava.library.path=${project.dependency.path} + + - - - org.sosy-lab - javasmt-solver-cvc5 - so - libcvc5 - libcvc5.so - - - org.sosy-lab - javasmt-solver-cvc5 - so - libcvc5jni - libcvc5jni.so - - - org.sosy-lab - javasmt-solver-cvc5 - so - libcvc5parser - libcvc5parser.so - - - org.sosy-lab - javasmt-solver-cvc5 - so - libpoly - libpoly.so - - - org.sosy-lab - javasmt-solver-cvc5 - so - libpolyxx - libpolyxx.so - + + + org.codehaus.mojo + exec-maven-plugin + 3.5.0 + + java + + -Djava.library.path=${project.dependency.path} + -classpath + + org.sosy_lab.java_smt_example.SolverOverviewTable + + + - - - org.sosy-lab - javasmt-solver-yices2 - so - libyices2j - libyices2j.so - + + + maven-jar-plugin + 3.5.0 + + + + + true + ${project.dependency.relativepath}/ + org.sosy_lab.java_smt_example.SolverOverviewTable + + + + - - - org.sosy-lab - javasmt-solver-opensmt - so - libopensmtj-${system.arch} - libopensmtj.so - - - + + + org.apache.maven.plugins + maven-dependency-plugin + 3.1.1 + + + copy-natives-temp + initialize + + copy-dependencies + + + ${project.build.directory}/temp-natives + so,dll,dylib + true + + + + copy-all-jars + initialize + + copy-dependencies + + + ${project.dependency.path} + jar + + + + + + org.apache.maven.plugins + maven-antrun-plugin + 3.1.0 + + + rename-natives + process-resources + + run + + + + + + + + + + + + + diff --git a/doc/Example-Maven-Project/src/test/java/org/sosy_lab/java_smt_example/SudokuTest.java b/doc/Example-Maven-Project/src/test/java/org/sosy_lab/java_smt_example/SudokuTest.java index a9f5a0ab98..83c900d860 100644 --- a/doc/Example-Maven-Project/src/test/java/org/sosy_lab/java_smt_example/SudokuTest.java +++ b/doc/Example-Maven-Project/src/test/java/org/sosy_lab/java_smt_example/SudokuTest.java @@ -2,7 +2,7 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2024 Dirk Beyer +// SPDX-FileCopyrightText: 2026 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 @@ -85,36 +85,15 @@ public static List getSolvers() { public Solvers solver; private static final String OS = System.getProperty("os.name").toLowerCase().replace(" ", ""); - private 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"); - /** - * Let's allow to disable some checks on certain combinations of operating systems and solvers, - * because of missing support. - * - *

We update this list, whenever a new solver or operating system is added. - */ + /** Disable some checks on certain combinations of operating systems and solvers, because of missing dependencies. */ private static boolean isOperatingSystemSupported(Solvers solver) { - switch (solver) { - case SMTINTERPOL: - case PRINCESS: - // any operating system is allowed, Java is already available. - return true; - case BOOLECTOR: - case CVC4: - case CVC5: - case OPENSMT: - case YICES2: - return IS_LINUX; - case MATHSAT5: - case BITWUZLA: - return IS_LINUX || IS_WINDOWS; - case Z3: - return IS_LINUX || IS_WINDOWS || IS_MAC; - default: - throw new AssertionError("unexpected solver: " + 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; From 56b3308fc349356eb5e00bd51aad0c24ae51ce5f Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 6 Apr 2026 10:52:34 +0200 Subject: [PATCH 22/30] migrate example web-project to latest versions of JavaSMT and solvers, and update documentation. --- doc/Example-Maven-Web-Project/Dockerfile | 32 ++ doc/Example-Maven-Web-Project/README.md | 111 ++++- doc/Example-Maven-Web-Project/pom.xml | 443 +++++++----------- .../org/sosy_lab/SolverOverviewServlet.java | 2 +- .../java_smt_web_example/SudokuTest.java | 35 +- 5 files changed, 283 insertions(+), 340 deletions(-) create mode 100644 doc/Example-Maven-Web-Project/Dockerfile diff --git a/doc/Example-Maven-Web-Project/Dockerfile b/doc/Example-Maven-Web-Project/Dockerfile new file mode 100644 index 0000000000..01a3683671 --- /dev/null +++ b/doc/Example-Maven-Web-Project/Dockerfile @@ -0,0 +1,32 @@ +# 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 + +FROM ubuntu:24.04 + +# Avoid interactive prompts during apt installations +ENV DEBIAN_FRONTEND=noninteractive + +# 1. Update and install Java 17 + Tomcat 10 +RUN apt-get update && apt-get install -y \ + openjdk-17-jdk \ + tomcat10 \ + && rm -rf /var/lib/apt/lists/* + +# 2. Set the environment so Tomcat knows where everything is +ENV CATALINA_HOME=/usr/share/tomcat10 +ENV CATALINA_BASE=/var/lib/tomcat10 + +# 3. Expose the default Tomcat port +EXPOSE 8080 + +# 4. Clean out default apps and copy your WAR file to the container +RUN rm -rf $CATALINA_BASE/webapps/* +COPY ./target/java-smt-web-example-2.0.war $CATALINA_BASE/webapps/ROOT.war + +# 5. Run Tomcat in the foreground +CMD ["/usr/share/tomcat10/bin/catalina.sh", "run"] diff --git a/doc/Example-Maven-Web-Project/README.md b/doc/Example-Maven-Web-Project/README.md index 21e657d909..ab837b6a97 100644 --- a/doc/Example-Maven-Web-Project/README.md +++ b/doc/Example-Maven-Web-Project/README.md @@ -3,32 +3,93 @@ This file is part of JavaSMT, an API wrapper for a collection of SMT solvers: https://github.com/sosy-lab/java-smt -SPDX-FileCopyrightText: 2021 Dirk Beyer +SPDX-FileCopyrightText: 2026 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> -This is an example web-application for using JavaSMT with Maven. -The example application prints a table of the available SMT solvers, -their version number and supported features. - -The Maven workflow in this project supports the following steps: - -- Compiling: `mvn compile` downloads all dependencies and compiles the project. -- Testing: `mvn test` executes the Sudoku example test. -- Packaging: `mvn package` creates a war file for the example application. - Dependencies like other jar files and binaries for SMT solvers are included in the war file. -- Running: the war file can be applied with your tomcat instance. - On Ubuntu you can use the following commands: - - Install tomcat9 (required once only): - `sudo apt install tomcat9` and `sudo service tomcat9 start` - - Copy the war file to the webapps directory: - `sudo cp target/java-smt-web-example-VERSION.war /var/lib/tomcat9/webapps/`. - The running instance of tomcat9 will automatically unpack the war file. - - Open `http://localhost:8080/java-smt-web-example-VERSION/SolverOverviewServlet`, - and you should see a table of the available SMT solvers. - -Please note that the Maven repository currently only contains release versions -and no snapshots, thus the newest features and bugfixes might be missing. -If a Maven step is not working or more steps are required, -please ask or report an issue [in the project](https://github.com/sosy-lab/java-smt). +# JavaSMT Maven Web Example + +This project shows how to use JavaSMT in a Maven-based web environment (WAR-based). +It includes a servlet that lists available solvers and a test case that solves a Sudoku puzzle. +The configuration in `pom.xml` handles the download and setup of native solver libraries (e.g., Z3, MathSAT5, CVC5) so they can be bundled into the WAR file. + +## Prerequisites + +* Java 17 or newer. +* Apache Maven. +* A servlet container like Apache Tomcat (e.g., version 10 or newer). +* Native solvers are only provided for **Linux x64** in this example. + Some solvers like Z3 and MathSAT5 also support Windows or ARM64 platform, if dependencies are adjusted in `pom.xml`. + Java-only solvers (SMTInterpol, Princess) work on all platforms. +* When using Linux, please use Ubuntu 24.04 or newer, as we provide latest solver versions for GLIBC_2.33 or newer. + +## Usage + +### Compile and Build + +Run the following to download dependencies and build the WAR file: +```bash +mvn clean package +``` +Native libraries will be copied, renamed, and included in `WEB-INF/lib` of the generated WAR file. + +### Run the Solver Overview Servlet + +The WAR file can be deployed to your servlet container. +On Ubuntu with Tomcat, you can use the following steps: + +1. Install Tomcat (required once): + ```bash + sudo apt install tomcat10 + sudo service tomcat10 start + ``` +2. Copy the WAR file to the `webapps` directory: + ```bash + sudo cp target/java-smt-web-example-VERSION.war /var/lib/tomcat10/webapps/ + ``` + Tomcat will automatically unpack the WAR file. +3. Open the following URL in your browser: + `http://localhost:8080/java-smt-web-example-VERSION/SolverOverviewServlet` + You should see a table of the available SMT solvers. + + +### Run the Solver Overview Servlet in a Docker Container + +You can also run the servlet in a Docker container. Here’s how: +0. Compile and package the WAR file as described above. +1. Build the Docker image from `Dockerfile`: + ```bash + podman build -t java-smt-web-example . + ``` +2. Run the Docker container: + ```bash + podman run -p 8080:8080 java-smt-web-example + ``` +3. Access the servlet at `http://localhost:8080/SolverOverviewServlet` in your browser. + + +### Run Sudoku Test + +The `SudokuTest` runs against all available solvers during the build process. + +```bash +mvn test +``` + +## Project Structure + +* `src/main/java/org/sosy_lab/SolverOverviewServlet.java`: Servlet implementation. +* `src/test/java/org/sosy_lab/java_smt_web_example/SudokuTest.java`: Parameterized JUnit test. +* `src/main/webapp/WEB-INF/web.xml`: Web application configuration. +* `pom.xml`: Maven configuration including dependency management and native library handling. + +## Native Library Handling + +JavaSMT backends often require native binaries. This project automates the following steps: +1. Download native libraries via Maven dependencies (using `classifier` and `type`). +2. Copy them to a temporary directory using `maven-dependency-plugin`. +3. Rename them (e.g., from `javasmt-solver-z3-libz3java-x64.so` to `libz3java.so`) using `maven-antrun-plugin` to match JavaSMT expectations. +4. Bundle the renamed libraries into `WEB-INF/lib` of the WAR file using `maven-war-plugin`. + +For more details, see the [JavaSMT documentation](https://github.com/sosy-lab/java-smt). diff --git a/doc/Example-Maven-Web-Project/pom.xml b/doc/Example-Maven-Web-Project/pom.xml index d32c8c1339..c95f4ce0a2 100644 --- a/doc/Example-Maven-Web-Project/pom.xml +++ b/doc/Example-Maven-Web-Project/pom.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: 2025 Dirk Beyer +SPDX-FileCopyrightText: 2026 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> @@ -16,7 +16,7 @@ SPDX-License-Identifier: Apache-2.0 org.sosy_lab.java_smt_web_example java-smt-web-example - 1.12 + 2.0 war java-smt-maven-web-example Example Maven project to show how to use JavaSMT with native solver libraries in a web project. @@ -74,29 +74,51 @@ SPDX-License-Identifier: Apache-2.0 x64 - 5.0.0 - 0.7.0-13.1-g595512ae + 6.0.0 + 0.8.2-339-g550ed911 3.2.2-g1a89c229 1.8-prerelease-2020-06-24-g7825d8f28 - 1.0.5-g4cb2ab9eb - 5.6.11-glibc2.27 - 2.8.0-sosy0-ge831bf23 - 4.1.1-734-g3732f7e08 - 2.6.2-396-g194350c1 - 4.13.4 + 2026-02-26-d22638a + 5.6.15 + 2.9.0-gef441e1c + 2.5-1242-g5c50fb6d + 2025-11-17 + 2.0 + 5.0.1-1258-gdad634a69 + 2.6.4-264-g553897f5 + 4.15.4 + 4.5.0-gd57a2a6dc + org.sosy-lab java-smt ${javasmt.version} + + + de.uni-freiburg.informatik.ultimate + smtinterpol + ${smtinterpol.version} + + + io.github.uuverifiers + princess_2.13 + ${princess.version} + + + io.github.uuverifiers + ostrich_2.13 + ${ostrich.version} + + org.sosy-lab - javasmt-solver-mathsat5 + javasmt-solver-mathsat ${mathsat.version} libmathsat5j-${system.arch} so @@ -123,12 +145,33 @@ SPDX-License-Identifier: Apache-2.0 libz3java-${system.arch} + + + org.sosy-lab + javasmt-solver-z3-legacy + ${z3-legacy.version} + com.microsoft.z3legacy + + + org.sosy-lab + javasmt-solver-z3-legacy + ${z3-legacy.version} + so + libz3legacy-${system.arch} + + + org.sosy-lab + javasmt-solver-z3-legacy + ${z3-legacy.version} + so + libz3javalegacy-${system.arch} + + org.sosy-lab javasmt-solver-bitwuzla ${bitwuzla.version} - jar org.sosy-lab @@ -166,7 +209,6 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-cvc4 ${cvc4.version} - jar CVC4 @@ -191,48 +233,18 @@ SPDX-License-Identifier: Apache-2.0 libcvc4parser - - - org.sosy-lab - javasmt-solver-cvc5 - ${cvc5.version} - jar - cvc5 - - - org.sosy-lab - javasmt-solver-cvc5 - ${cvc5.version} - so - libcvc5 - - - org.sosy-lab - javasmt-solver-cvc5 - ${cvc5.version} - so - libcvc5jni - - - org.sosy-lab - javasmt-solver-cvc5 - ${cvc5.version} - so - libcvc5parser - + org.sosy-lab javasmt-solver-cvc5 ${cvc5.version} - so - libpoly org.sosy-lab javasmt-solver-cvc5 ${cvc5.version} so - libpolyxx + libcvc5jni-${system.arch} @@ -240,7 +252,12 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-yices2 ${javasmt-yices.version} - jar + + + org.sosy-lab + javasmt-solver-yices2 + + org.sosy-lab @@ -255,7 +272,6 @@ SPDX-License-Identifier: Apache-2.0 org.sosy-lab javasmt-solver-opensmt ${opensmt.version} - jar org.sosy-lab @@ -282,263 +298,118 @@ SPDX-License-Identifier: Apache-2.0 - - - - - maven-surefire-plugin - 3.0.0 - - + + org.apache.maven.plugins + maven-surefire-plugin + 3.5.4 + + -Djava.library.path=${project.dependency.path} + + + + + + org.apache.maven.plugins + maven-war-plugin + 3.5.0 + + + + true + + + + + ${project.dependency.path} + + **/*.so + **/*.dll + **/*.dylib + + WEB-INF/lib + + + + + + + maven-jar-plugin + 3.5.0 + + + + - -Djava.library.path=${project.dependency.path} - - - - org.apache.maven.plugins - maven-war-plugin - 3.4.0 - - - - true - - - - - target/dependency - - - libmathsat5j.so - libz3.so - libz3java.so - libboolector.so - libminisat.so - libpicosat.so - libcvc4.so - libcvc4jni.so - libcvc4parser.so - libyices2j.so - libcvc5.so - libcvc5jni.so - libcvc5parser.so - libpoly.so - libpolyxx.so - libyices2j.so - libopensmtj.so - - WEB-INF/lib - - - - - - maven-jar-plugin - 3.4.0 - - - - - true - ${project.dependency.relativepath} - org.sosy_lab.SolverOverviewServlet - - - - - - - + true + ${project.dependency.relativepath}/ + org.sosy_lab.SolverOverviewServlet + + + + + + - org.apache.maven.plugins maven-dependency-plugin 3.1.1 - - copy + copy-natives-temp initialize - copy + copy-dependencies + + ${project.build.directory}/temp-natives + so,dll,dylib + true + - - - copy-dependencies - validate + copy-all-jars + initialize copy-dependencies + + ${project.dependency.path} + jar + + + + + + org.apache.maven.plugins + maven-antrun-plugin + 3.1.0 + + + rename-natives + process-resources + + run + + + + + + + + + + + - - ${project.dependency.path} - - - - - - - org.sosy-lab - javasmt-solver-mathsat5 - so - libmathsat5j-${system.arch} - libmathsat5j.so - - - - - org.sosy-lab - javasmt-solver-z3 - so - libz3java-${system.arch} - libz3java.so - - - org.sosy-lab - javasmt-solver-z3 - so - libz3-${system.arch} - libz3.so - - - - - org.sosy-lab - javasmt-solver-bitwuzla - so - libbitwuzlaj-${system.arch} - libbitwuzlaj.so - - - - - org.sosy-lab - javasmt-solver-boolector - so - libboolector - libboolector.so - - - org.sosy-lab - javasmt-solver-boolector - so - libminisat - libminisat.so - - - org.sosy-lab - javasmt-solver-boolector - so - libpicosat - libpicosat.so - - - - - org.sosy-lab - javasmt-solver-cvc4 - so - libcvc4 - libcvc4.so - - - org.sosy-lab - javasmt-solver-cvc4 - so - libcvc4jni - libcvc4jni.so - - - org.sosy-lab - javasmt-solver-cvc4 - so - libcvc4parser - libcvc4parser.so - - - - - org.sosy-lab - javasmt-solver-cvc5 - so - libcvc5 - libcvc5.so - - - org.sosy-lab - javasmt-solver-cvc5 - so - libcvc5jni - libcvc5jni.so - - - org.sosy-lab - javasmt-solver-cvc5 - so - libcvc5parser - libcvc5parser.so - - - org.sosy-lab - javasmt-solver-cvc5 - so - libpoly - libpoly.so - - - org.sosy-lab - javasmt-solver-cvc5 - so - libpolyxx - libpolyxx.so - - - - - org.sosy-lab - javasmt-solver-yices2 - so - libyices2j - libyices2j.so - - - - - org.sosy-lab - javasmt-solver-opensmt - so - libopensmtj-${system.arch} - libopensmtj.so - - - diff --git a/doc/Example-Maven-Web-Project/src/main/java/org/sosy_lab/SolverOverviewServlet.java b/doc/Example-Maven-Web-Project/src/main/java/org/sosy_lab/SolverOverviewServlet.java index 83179dd2fa..2833d832d8 100644 --- a/doc/Example-Maven-Web-Project/src/main/java/org/sosy_lab/SolverOverviewServlet.java +++ b/doc/Example-Maven-Web-Project/src/main/java/org/sosy_lab/SolverOverviewServlet.java @@ -2,7 +2,7 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2024 Dirk Beyer +// SPDX-FileCopyrightText: 2026 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 diff --git a/doc/Example-Maven-Web-Project/src/test/java/org/sosy_lab/java_smt_web_example/SudokuTest.java b/doc/Example-Maven-Web-Project/src/test/java/org/sosy_lab/java_smt_web_example/SudokuTest.java index 0a091c1604..d59de501fd 100644 --- a/doc/Example-Maven-Web-Project/src/test/java/org/sosy_lab/java_smt_web_example/SudokuTest.java +++ b/doc/Example-Maven-Web-Project/src/test/java/org/sosy_lab/java_smt_web_example/SudokuTest.java @@ -2,7 +2,7 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2024 Dirk Beyer +// SPDX-FileCopyrightText: 2026 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 @@ -85,36 +85,15 @@ public static List getSolvers() { public Solvers solver; private static final String OS = System.getProperty("os.name").toLowerCase().replace(" ", ""); - private 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"); - /** - * Let's allow to disable some checks on certain combinations of operating systems and solvers, - * because of missing support. - * - *

We update this list, whenever a new solver or operating system is added. - */ + /** Disable some checks on certain combinations of operating systems and solvers, because of missing dependencies. */ private static boolean isOperatingSystemSupported(Solvers solver) { - switch (solver) { - case SMTINTERPOL: - case PRINCESS: - // any operating system is allowed, Java is already available. - return true; - case BOOLECTOR: - case CVC4: - case CVC5: - case OPENSMT: - case YICES2: - return IS_LINUX; - case MATHSAT5: - case BITWUZLA: - return IS_LINUX || IS_WINDOWS; - case Z3: - return IS_LINUX || IS_WINDOWS || IS_MAC; - default: - throw new AssertionError("unexpected solver: " + 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; From a3620efd5d6c61473a5db6e074a9f8988bd48dbb Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 6 Apr 2026 11:10:03 +0200 Subject: [PATCH 23/30] update Maven documentation --- doc/Developers-How-to-Release-into-Maven.md | 130 +++++++++----------- 1 file changed, 59 insertions(+), 71 deletions(-) diff --git a/doc/Developers-How-to-Release-into-Maven.md b/doc/Developers-How-to-Release-into-Maven.md index e144439db7..46aeb5f67a 100644 --- a/doc/Developers-How-to-Release-into-Maven.md +++ b/doc/Developers-How-to-Release-into-Maven.md @@ -3,7 +3,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: 2021 Dirk Beyer +SPDX-FileCopyrightText: 2026 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> @@ -13,90 +13,78 @@ SPDX-License-Identifier: Apache-2.0 Please read the hints on release in the [developer documentation](Developers.md) first. We only release something to Maven after doing an Ivy release. -With our project infrastructure is much simpler to test packages from (local) Ivy repository than from Maven. - -Make sure that all necessary dependency libraries are already released on Maven Central, -before (or at least while) publishing a new version of JavaSMT. -Maven does not check for existing or non-existing dependencies automatically. -Dependencies like `SMTIntinterpol`, `Princess`, and `SoSy-Lab Common` need to be available via Maven in the correct version. -A release of `SoSy-Lab Common` can be uploaded to Maven by us, even afterward :-). +Our infrastructure is designed to resolve artifacts from our [Ivy repository](https://www.sosy-lab.org/ivy/) and package them for Maven Central. +Make sure that all necessary dependency libraries are already released on Maven Central +before (or shortly after) publishing a new version of JavaSMT. +Dependencies like `SMTInterpol`, `Princess`, and `SoSy-Lab Common` need to be available via Maven in the correct version. ## Automation vs. Manual Steps -The release to Maven Central is currently not fully automated due to the bug in the -ANT script provided by Maven Central documentation. -For publishing to Maven Central, we use the [Nexus Repository Manager][]. -We first upload files into that repository, and later manually publish them from there. -There is no need to manually change any file for the upload process. - +The release process uses the [Sonatype Central Publishing Portal](https://central.sonatype.com/): +1. **Automated Upload:** Use Ant targets to resolve artifacts from Ivy, generate POMs, sign artifacts, and upload a deployment bundle. +2. **Manual Release:** Log in to the portal to review the validated deployment and finalize the release. ## Requirements -Please make sure that you have a valid user account and configured your local settings accordingly. -For example, insert the following content into `~/.m2/settings.xml`: +### 1. Account +Register at [Sonatype Central](https://central.sonatype.com/) and ensure you have access to the `org.sosy-lab` namespace. + +### 2. PGP Key +- You need a GPG key pair (RSA 2048-bit or higher). +- Your public key **must** be published to a supported keyserver: + `gpg --keyserver keyserver.ubuntu.com --send-keys ` +- For the publication process, the passphrase can be provided via `-Dgpg.passphrase=...` or stored in `build.properties`. + There is no interactive prompt, so ensure the passphrase is accessible to the build process. + +### 3. Authentication Token +- Log in to [Sonatype Central](https://central.sonatype.com/), go to **Account**, and **Generate User Token**. +- Add the credentials to your `~/.m2/settings.xml` as follows: ```xml - - - ossrh - USER - PASSWORD - - - - - gpg - - gpg - - - - - - - centralhttps - central - Maven central https - https://repo1.maven.org/maven2/ - - + + + SonatypeCentral + TOKEN_NAME + TOKEN_PASSWORD + + ``` -If default system settings are not configured for HTTPS, -we get an 501 error when downloading further maven dependencies. -Thus, we add a mirror for HTTPS. +## Publishing -You might need to store `maven-ant-tasks-2.1.3.jar` (or newer version) under `~/.ant/lib/` -to avoid a failure when creating the task `antlib:org.apache.maven.artifact.ant:mvn`. +To publish a component, use the `publish-to-maven-central` Ant target. +This target automatically handles the resolution from Ivy and the bundle creation. +### Commands -## Publishing +For JavaSMT itself: +```bash +ant publish-to-maven-central -Dpublish.component=java-smt -Dpublish.version=5.0.0 +``` + +For binary solvers or bindings: +```bash +# Example for Z3 +ant publish-to-maven-central -Dpublish.component=javasmt-solver-z3 -Dpublish.version=4.15.4 + +# Example for Yices2 bindings +ant publish-to-maven-central -Dpublish.component=javasmt-yices2 -Dpublish.version=6.0.0-141-g04134287c +``` + +### Testing and Debugging +- To prepare the bundle without uploading, add `-Dpublish.upload=false`. +- You can use `scripts/test-maven-central-bundle.sh` to verify the bundle structure locally. + It contains several hardcoded paths and versions, so adjust it as needed for your case. + +## Finalizing Publication -For publishing JavaSMT itself: -- Execute `ant stage` to upload the local build of JavaSMT into the [Nexus Repository Manager][]. - This is ideally done directly after a release to our [Ivy Repository][]. -- Login to the [Nexus Repository Manager][] and freeze (`close`) the entry in the [staging repositories][], - and inspect the files for correctness and completeness! -- Later `release` your staged bundle. - After some delay (a few hours) the release is automatically synced to Maven Central. - -For publishing binary solvers like Boolector, CVC4, MathSAT5, Yices2, or Z3, the process is similar: -- Execute `ant stage-SOLVER` to upload the currently installed binary solvers into the [Nexus Repository Manager] - whenever there was an update for the corresponding solver. - This is ideally done directly after a release of the solver to our [Ivy Repository][]. - For Yices2, we might require the execution of `ant stage-javasmt-yices2` to release the package `javasmt-yices2`. -- Login to the [Nexus Repository Manager][] and freeze (`close`) the entry in the [staging repositories][], - and inspect the files for correctness and completeness! -- Later `release` your staged bundle. - After some delay (a few hours) the release is automatically synced to Maven Central. - -Additional instructions are available at the official [OSSRH][] page and -the [documentation](http://central.sonatype.org/pages/releasing-the-deployment.html). - -[Ivy Repository]: http://www.sosy-lab.org/ivy/org.sosy_lab/ -[OSSRH]: http://central.sonatype.org/pages/ossrh-guide.html -[Nexus Repository Manager]: https://oss.sonatype.org/ -[staging repositories]: https://oss.sonatype.org/#stagingRepositories +1. **Review and Publish:** + - Log in to [Sonatype Central Deployments](https://central.sonatype.com/publishing/deployments). + - Check that the deployment is validated and contains all expected files. + - Click **Publish** to start the release process. +2. **Wait for Sync:** + - It usually takes about 15–30 minutes for the artifacts to appear in [Maven Central](https://repo1.maven.org/maven2/org/sosy-lab/). + - Search results on the Sonatype portal might take longer to update. From 9a154dabb0f244277eb1d25291f47e5d7f35f562 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 6 Apr 2026 11:15:17 +0200 Subject: [PATCH 24/30] remove outdated and unneeded documentation for local setup of a Maven repository --- doc/Maven-for-Developers.md | 644 ------------------------------------ 1 file changed, 644 deletions(-) delete mode 100644 doc/Maven-for-Developers.md diff --git a/doc/Maven-for-Developers.md b/doc/Maven-for-Developers.md deleted file mode 100644 index 24b1ec1d79..0000000000 --- a/doc/Maven-for-Developers.md +++ /dev/null @@ -1,644 +0,0 @@ - - -____________________ - -This documentation is intended for internal use only. -Testing a Maven release is error-prone and complex. -This document aims for helping in some steps. -There is no guarantee for anything. Please test everything for yourself! -____________________ - - -Local test for Maven (Still needs internet to pull dependencies for Maven) -0. If you are only interested in the JavaSMT part and know basic Maven, skip to 13. -1. Install Maven -2. Install Sonatype Nexus Repository Manager 3 (Free Version!) - 2.1 Download Nexus - 2.2 Unpack .tar - 2.3 Move Nexus-version and Sonatype-work folders to where you want them (/usr/local/ for example) - 2.4 Change Folder permissions (chmod something) -3. Start Nexus with ./nexus start (file located in nexus-version/bin/ folder with version being the nexus version you use) - (You can stop it with ./nexus stop ) -4. Open a browser and enter: http://localhost:8081 -5. Press Log in in the top right corner and enter the name: "admin" and search for the password in the file located at Sonatype-work/nexus3/admin.password ) -6. Optional: Change Password -7. Make a new User called "deployment" with a password of your choosing. (You can name it however you want. Just substitute deployment with your version from now on) -8. Go to the Maven repository (~/.m2 most likely in the home dir. If you don't know where it is use this on the command line: mvn help:evaluate -Dexpression=settings.localRepository ) -9. If a settings.xml is present save it, else make a new one. (Or edit your current one if you know what you are doing) -10. Enter the following into the settings.xml: - (The urls are taken from the Nexus repository. You can find them at http://localhost:8081 after logging in in the left menu on browse and copy the url of maven-snapshot/releases) - (The username and password have to match the ones you entered in step 7, it does not matter how they are named) - (If you do not want to use the release or the snapshot repository you can simply omit it here and in all further steps.) - (Difference release vs snapshot: snapshots can be overridden with the same version number by deploying again. Release can NEVER be overridden by deploying) - -```xml - - - - nexusrepo - deployment - the_password_for_the_deployment_user - - - - - - - snapshot - - - nexus-snapshot-repo - my snapshot repo - http://localhost:8081/repository/maven-snapshots/ - - - - - - release - - - nexus-release-repo - my release repo - http://localhost:8081/repository/maven-releases/ - - - - - - - - release - - -``` - -11. If you want to test a Project, download the test Project from Maven with the following command: - mvn archetype:generate -DgroupId=com.mycompany.app -DartifactId=my-app -DarchetypeArtifactId=maven-archetype-quickstart -DarchetypeVersion=1.4 -DinteractiveMode=false -12. Now switch to the new folder called "my-app" and go through the existing pom.xml and copy the parts missing - (copy it into a .xml so that you can read it easier): - -```xml - - - - - 4.0.0 - - com.mycompany.app - - - my-app - - 1.0-SNAPSHOT - - - - - - junit - junit - 4.10 - - - - - - - - nexusrepo - My internal repository - http://localhost:8081/repository/maven-snapshots/ - - - - nexusrepo - My internal repository - http://localhost:8081/repository/maven-releases/ - - - - - - - - - - - maven-compiler-plugin - 3.8.0 - - - 11 - - - - - maven-surefire-plugin - 2.22.1 - - - - maven-jar-plugin - 3.0.2 - - - - com.mycompany.app.App - - - - - - maven-deploy-plugin - 2.8.1 - - - default-deploy - deploy - - deploy - - - - - - - - -``` - - -In this test project you can see and test some basic Maven ideas -i.e. the folder structure, plugins, deployment etc. -Besides the pom.xml you can see the /src folder that will bring you to the test project and the tests for said project. -This folder layout is standard for maven and should be followed (src/main/java and src/test/java, after that you may change the names to your needs of course ;D ) -See: https://maven.apache.org/guides/introduction/introduction-to-the-standard-directory-layout.html -We will cover changes in the JavaSMT example! -Open a terminal in the directory with the pom.xml and you may enter the following example commands: -mvn package // (tests and packages the project. You will get the test results in the cmd and a new folder target appears with the jar and class files etc.) -mvn clean // (cleans the target folder etc.) -mvn clean package // (first cleans, then uses package) -mvn deploy // deploys the current project to the local Maven Repo with the set group/articactId and version and this pom.xml. - This will use the active server from settings.xml. - You should be able to see the project on said server in the browser-interface. - -## JavaSMT example from here: ------------------------------------------------------------------ -13. Use the following on the command line to deploy an artifact of your choice that was not compiled by Maven (For example shared libraries or our projects) - Using a pom.xml for this works BUT you would create 2 deployments. One for the pom.xml and then one extra for the deploy-file goal, so just stick with this for now. - url = url of the server - repository = same name you gave in the entry of the settings.xml - artifactId = name of the file (dependency) after deployment (do not use a file ending here) - file = the file you want to deploy. You must be in the folder of the file or enter the path to it! You need the full filename including ending (.so for example). - version = self-explanatory. Set it to your current version! Will get Appended to your artifactId for the final filename after deployment. No you can't just not enter one, i tried, i truly did.... - groupId = org.sosy-lab (most likely, for testing not relevant) - packaging = file ending i.e. so, jar etc. for the final deployed file - pomDescription = String that describes the artifact (Optional) - - The below is an example for mathsat5 deployment. - You can look at it in the local nexus repo under "Browse" on the left side, maven-releases, org, sosy-lab, javasmt-mathsat5, 1.1 - - -mvn deploy:deploy-file -Durl=http://localhost:8081/repository/maven-releases/ -DrepositoryId=nexusrepo -Dfile=libmathsat5j.so -DgroupId=org.sosy-lab -DartifactId=javasmt-solver-mathsat5 -Dversion=1.1 -Dpackaging=so -DgeneratePom=false - - - The below is an example for Z3 deployment: - files= additional files (separated by a comma and NO spaces. If you use this you need to specify types and classifiers) - classifiers=classifiers for the files (in the order they appear in files separated by a comma with no spaces) - types= types of files (in the order they appear in files separated by a comma with no spaces) - - -mvn deploy:deploy-file -Durl=http://localhost:8081/repository/maven-releases/ -DrepositoryId=nexusrepo -Dfile=lib/java/runtime-z3/com.microsoft.z3.jar -Dfiles=lib/java/runtime-z3/libz3java.so,lib/java/runtime-z3/libz3.so -Dtypes=so,so -DgroupId=org.sosy-lab -Dclassifiers=libz3java,libz3 -DartifactId=javasmt-solver-z3 -Dversion=4.8.9-sosy0 -Dpackaging=jar -DpomFile=solvers_maven_conf/maven_z3_pom.xml -DgeneratePom=false - -For deployment to Maven Central change the first part of the command to: - mvn org.apache.maven.plugins:maven-gpg-plugin:1.3:sign-and-deploy-file - Change url and repository to: - -Durl=${ossrh-staging-repository-url} -DrepositoryId=${ossrh-server-id} - Add to the end: - -Pgpg - - Or simply take a look at the file /build/build-maven-publish.xml - - If you want to use those dependencies you need to rename them and copy them to a location that is checked - by the sosy commons library! - To perform this we need a little bit of user interaction. - - -14. Use Mathsat5/Z3 with Maven: - Open the pom.xml you want to use with JavaSMT and Mathsat5/Z3. - (This assumes that you use the project provided. Meaning that there is the main-file - my-app/src/main/java/com/mycompany/app/SolverOverviewTable.java and the test-file - my-app/src/test/java/com/mycompany/app/SudokuTest.java - You can change the folder structure as described above. Lets say you want - javasmt-maven-example/src/main/java/org/sosy-lab/SolverOverviewTable.java then - you just need to edit the following things: the folder structure itself, the groupId - in the beginning of the pom.xml and the mainClass attribute of the maven-jar-plugin. - Note: the name of the root dir in which the pom.xml resides is irrelevant for Maven.) - Add this to the dependencies: - (I assume you want to use both. Mathsat5 is 1 dependency with 1 solver binary. - Z3 is 3 dependencies with 1 JAR and 2 binaries. If you don't want Z3 you need to remove - all 3 here and 2 items from the copy - -```xml - - org.sosy-lab - java-smt - 3.7.0 - - - org.sosy-lab - javasmt-solver-mathsat5 - 5.6.5 - so - - - - org.sosy-lab - javasmt-solver-z3 - 1.2 - - - org.sosy-lab - javasmt-solver-z3 - 1.2 - so - libz3 - - - org.sosy-lab - javasmt-solver-z3 - 1.2 - so - libz3java - - - - - - junit - junit - 4.11 - test - -``` - - Modify the plugins maven-surefire-plugin and maven-jar-plugin in pluginManagement: - -```xml - - - maven-surefire-plugin - 2.22.1 - - - -Djava.library.path=${project.build.directory}/dependency - - - - maven-jar-plugin - 3.0.2 - - - - - true - ${project.build.directory}/dependency - com.mycompany.app.SolverOverviewTable - - - - -``` - - Additionally add the following to (NOT ). - (If you really wanted it in there you need to execute it in later on!) - is just like in . - -```xml - - - - org.apache.maven.plugins - maven-dependency-plugin - 3.1.1 - - - - copy - initialize - - properties - copy - - - - - - copy-dependencies - validate - - copy-dependencies - - - - - - - - org.sosy-lab - javasmt-solver-mathsat5 - 5.6.5 - so - - ${project.build.directory}/dependency - libmathsat5j.so - - - - org.sosy-lab - javasmt-solver-z3 - 1.2 - so - libz3java - - ${project.build.directory}/dependency - libz3java.so - - - org.sosy-lab - javasmt-solver-z3 - 1.2 - so - libz3 - - ${project.build.directory}/dependency - libz3.so - - - - -``` - - Due to the way org.sosy-lab.commons loads the native solver binaries it is currently not possible to build a single JAR - that runs with Mathsat5/Z3 without any external dependencies. - It is however possible to build a WAR file, see web tutorial below. - -15. Optional/Debug: You may need something to print our stuff like properties in Maven to debug your pom.xml. - The following might help with that: - -```xml - - org.apache.maven.plugins - maven-antrun-plugin - 1.7 - - - compile - - run - - - - - ******** Displaying value of a property ******** - ${java.library.path} - ${org.sosy-lab:common:jar} - - - - - -``` - -16. Web-Tutorial explaining how to create a Tomcat-Server: - - -Download Tomcat (i used the Tomcat 9 tarball): https://tomcat.apache.org/download-90.cgi - - -Extract at a location that you want to use for your server and set permissions. - - -We need to configure the admin login and the java location for the server first. - In the extracted server folder go to the configuration folder and open tomcat-users.xml - Insert the following inside the thingy: - -```xml - - - -``` - - With this you can later deploy/delete war files to and from the server. - You can of course set the username/password however you like. - It is possible that the server later refuses those login details, i too had that problem, - but then it went away and i don't know why. If you have this problem and find a solution please - contact me (Daniel Baier)! - - To configure java you need to know where your default java is located. (It should be Java 8 +) - Search for setenv.sh (on linux) in the bin folder of Tomcat. If its not there, create one. - In there write: - - JRE_HOME=/path/to/your/java - CATALINA_PID="$CATALINA_BASE/tomcat.pid" - - Technically you need to set CATALINA_HOME in the setenv too. However it should be set by default. - (CATALINA_HOME default is your Tomcat folder) - - More information in the RUNNING.txt in the main folder of Tomcat. - - -You can now start your Tomcat 9 server with the startup.sh in the bin folder. - You can stop it with the shutdown.sh in the same folder. - You can access the server GUI via a Web-Browser and the IP: http://localhost:8080 - You can change/access/upload directly to the server via the "Manager App" in the top right corner. - You need your login credentials specified above for that. - In there you can upload via "Deploy" (War file to deploy). - After deploying simply click the WAR in the Applications tab. - - -17. Web-Tutorial explaining how to create a Dynamic Web Project (w Eclipse): - (Simple example with 1 button that does something trivial) - - -Create a new Dynamic Web Project in Eclipse via new -> other -> Web - (If you can't you are missing an extension for web projects. - Most likely you won't be able to install a Server in Eclipse either. - So download it from the marketplace.) - - -Choose a name - Choose the runtime you downloaded (Tomcat 9 most likely) - Module Version 4.0 - Default Configuration for your runtime - EAR Membership simply EAR - Click next twice and set the box to create a web.xml descriptor - - -Open your project in the project explorer, open Java Resources and create a package and a crate a new Servlet in there - When creating a Servlet you need the "doPost" and "doGet" methods so just let them create automatically - In this class (Servlet) you can now add your code to the code of the doGet method i.e.: - Printwriter out = response.getWriter(); // We need this to print something. You need to import the IO package! - out.println("Hallo Welt!"); - - With this every time the servlet is used it will print "Hallo Welt!" on the screen. - - -Next we need a JSP Page to provide a frontend for the user: - Right click WebContent in the project explorer -> new -> JSP File - name it "index.jsp", choose the default options and finish. - (We name it index because that one will be used as it is a standard, you may name if however you like) - In this JSP add the following in the : - -```xml - Welcome -

-
- -
-``` - - This creates a button (type=submit) that has the text "Send" on it. - Now go to WEB-INF/web.xml in your project. - (insert the name of your JSP here if you don't want to name it index) - Here you should be able to see a mapping to your Servlet. - If not, add it yourself (this will assume your servlet is named MyServlet in a package named org.sosy-lab): - -```xml - - - MyServlet - MyServlet - org.sosy-lab.MyServlet - - - MyServlet - /MyServlet - -``` - - This mapping is not needed in an basic example (or at all). - In servlet the description and display-name is optional and does what it says. (You can simply delete those 2 if you want) - In servlet the servlet-class specifies the file you want to map to the servlet-name. - In servlet-mapping you can map this servlet-name to one or more urls. - You may access those urls later with the IP:port/MyServlet etc. - (With IP:port being the IP/port you use for your server. - By default you get the IP:port/MyServlet mapping anyway) - - If you want to test this you can right click the project and execute it with "run with". - You will have to have installed the web development tools/server tools however - and you have to choose/create a Tomcat server. Simply use the Tomcat server files you already downloaded. - -18. Web-Tutorial explaining how to create a WAR file with Maven: - - Now create a new folder (this will be the main folder of your Maven project). - Name it however you like (i.e. MyProject) and enter it. In there create a new folder named "src" and your pom.xml. - Enter the src folder, create a folder main here an copy your web project into this folder so that it looks like this: - You may have to rename some folders to match the pattern below (src/main/java and src/main/webapp is a must!) - - MyProject - |--pom.xml - |--src - |--main - |--java - | |--org - | | |--sosy_lab - | | | |--MyServlet.java - |--webapp - |--META-INF - |--WEB-INF - |--index.jsp - - - More information here: - https://maven.apache.org/guides/introduction/introduction-to-the-standard-directory-layout.html - -19. pom.xml for a web-project / how to create a WAR file with Maven: - - We will package the dependencies, including the native solver files, into the WAR. - The pom looks nearly the same as the normal JAR pom, the differences are: - - ```xml - - war - - - - - org.apache.maven.plugins - maven-war-plugin - 3.3.1 - - - - true - - - - - target/dependency - - libmathsat5j.so - libz3.so - libz3java.so - - WEB-INF/lib - - - - - ``` - - The rest needs to be set up exactly like before (except the jar plugin and the tests if you don't have any) - Now mvn package should create a WAR file in the target directory for you that you may test on your own Tomcat server. From 5872d113f70f88fc539a603b64c239a1b6511f43 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 6 Apr 2026 14:24:09 +0200 Subject: [PATCH 25/30] CVC4: use JAR as packaging type. With version 1.8.1, we can provide sources and JavaDoc. Thus, we can use JAR as default packaging type. --- build/build-maven-central.xml | 3 +-- solvers_maven_conf/maven_cvc4_pom_template.xml | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/build/build-maven-central.xml b/build/build-maven-central.xml index 517fd77e47..f040786ed5 100644 --- a/build/build-maven-central.xml +++ b/build/build-maven-central.xml @@ -96,8 +96,7 @@ SPDX-License-Identifier: Apache-2.0 Get POM template for publication. Each component can have a different metadata, license, authors,... --> + value="solvers_maven_conf/maven_${publish.component}_pom_template.xml"> diff --git a/solvers_maven_conf/maven_cvc4_pom_template.xml b/solvers_maven_conf/maven_cvc4_pom_template.xml index 6c6e64d193..771cd4e451 100644 --- a/solvers_maven_conf/maven_cvc4_pom_template.xml +++ b/solvers_maven_conf/maven_cvc4_pom_template.xml @@ -14,7 +14,7 @@ SPDX-License-Identifier: Apache-2.0 4.0.0 org.sosy-lab javasmt-solver-cvc4 - pom + jar javasmt-solver-cvc4 ${stage.revision} SMT solver CVC4 for use in JavaSMT From 89512ab08ef266661eaf1c4816a54504d7932c60 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 11 Apr 2026 20:45:13 +0200 Subject: [PATCH 26/30] CVC5: use packaging as JAR with JavaDoc available in our latest CVC5 release --- solvers_maven_conf/maven_cvc5_pom_template.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/solvers_maven_conf/maven_cvc5_pom_template.xml b/solvers_maven_conf/maven_cvc5_pom_template.xml index f0a34b498e..8c6dfa81c8 100644 --- a/solvers_maven_conf/maven_cvc5_pom_template.xml +++ b/solvers_maven_conf/maven_cvc5_pom_template.xml @@ -14,7 +14,7 @@ SPDX-License-Identifier: Apache-2.0 4.0.0 org.sosy-lab javasmt-solver-cvc5 - pom + jar javasmt-solver-cvc5 ${stage.revision} SMT solver CVC5 for use in JavaSMT From 2f7645b1d4590f06008215c16383e40fe397bbaf Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 12 Apr 2026 12:22:38 +0200 Subject: [PATCH 27/30] Yices2: use packaging as JAR with JavaDoc available in our latest Yices2 release --- solvers_maven_conf/maven_yices2_pom_template.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/solvers_maven_conf/maven_yices2_pom_template.xml b/solvers_maven_conf/maven_yices2_pom_template.xml index 4d30fb15f6..92a379b5be 100644 --- a/solvers_maven_conf/maven_yices2_pom_template.xml +++ b/solvers_maven_conf/maven_yices2_pom_template.xml @@ -14,7 +14,7 @@ SPDX-License-Identifier: Apache-2.0 4.0.0 org.sosy-lab javasmt-solver-yices2 - pom + jar javasmt-solver-yices2 ${stage.revision} SMT solver Yices for use in JavaSMT From ef19e4c5e1bca93f401c7e5d2da3f20bb40eb4bf Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 12 Apr 2026 15:39:35 +0200 Subject: [PATCH 28/30] Yices2-Bindings: update to latest version --- build/build-maven-central.xml | 18 ++++++++++++++---- .../maven_javasmt-yices2_pom_template.xml | 2 +- 2 files changed, 15 insertions(+), 5 deletions(-) diff --git a/build/build-maven-central.xml b/build/build-maven-central.xml index f040786ed5..c3e3d5fddb 100644 --- a/build/build-maven-central.xml +++ b/build/build-maven-central.xml @@ -87,7 +87,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -168,15 +168,25 @@ SPDX-License-Identifier: Apache-2.0 + + + + + + - - + + + + + + @@ -401,4 +411,4 @@ SPDX-License-Identifier: Apache-2.0 - \ No newline at end of file + diff --git a/solvers_maven_conf/maven_javasmt-yices2_pom_template.xml b/solvers_maven_conf/maven_javasmt-yices2_pom_template.xml index b29f21a4b3..72d77aeb0c 100644 --- a/solvers_maven_conf/maven_javasmt-yices2_pom_template.xml +++ b/solvers_maven_conf/maven_javasmt-yices2_pom_template.xml @@ -14,7 +14,7 @@ SPDX-License-Identifier: Apache-2.0 4.0.0 org.sosy-lab javasmt-yices2 - pom + jar javasmt-yices2 ${stage.revision} JavaSMT bindings for the SMT solver Yices From fa8c457cad721ccb52092005fd718565200771d0 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 12 Apr 2026 15:56:19 +0200 Subject: [PATCH 29/30] improve script --- build/build-maven-central.xml | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/build/build-maven-central.xml b/build/build-maven-central.xml index c3e3d5fddb..7601b068e3 100644 --- a/build/build-maven-central.xml +++ b/build/build-maven-central.xml @@ -165,27 +165,24 @@ SPDX-License-Identifier: Apache-2.0 - + - + - - - - + - + - + From 6b9f1661f297a8ba4f17b0d68d4dddbbbacaa481 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 12 Apr 2026 23:32:06 +0200 Subject: [PATCH 30/30] fix script --- build/build-maven-central.xml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/build/build-maven-central.xml b/build/build-maven-central.xml index 7601b068e3..df98f0304b 100644 --- a/build/build-maven-central.xml +++ b/build/build-maven-central.xml @@ -165,6 +165,9 @@ SPDX-License-Identifier: Apache-2.0 + + +