update example maven projects to JavaSMT 5.0.0 and Java 17.

xeren · Jul 8, 2024 · 1d4cc82 · 1d4cc82
1 parent 83a2b98
commit 1d4cc82
Show file tree

Hide file tree

Showing 5 changed files with 114 additions and 108 deletions.
diff --git a/doc/Example-Maven-Project/pom.xml b/doc/Example-Maven-Project/pom.xml
@@ -16,7 +16,7 @@ SPDX-License-Identifier: Apache-2.0
 
   <groupId>org.sosy_lab.java_smt_example</groupId>
   <artifactId>java-smt-maven-example</artifactId>
-  <version>1.9</version>
+  <version>1.10</version>
   <name>java-smt-maven-example</name>
   <description>Example Maven project to show how to use JavaSMT with native solver libraries.</description>
   <url>https://github.com/sosy-lab/java-smt</url>
@@ -63,21 +63,22 @@ SPDX-License-Identifier: Apache-2.0
 
   <properties>
     <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
-    <maven.compiler.source>11</maven.compiler.source>
-    <maven.compiler.target>11</maven.compiler.target>
-    <maven.compiler.release>11</maven.compiler.release>
+    <maven.compiler.source>17</maven.compiler.source>
+    <maven.compiler.target>17</maven.compiler.target>
+    <maven.compiler.release>17</maven.compiler.release>
     <project.dependency.relativepath>dependency</project.dependency.relativepath>
     <project.dependency.path>${project.build.directory}/${project.dependency.relativepath}</project.dependency.path>
 
-    <javasmt.version>4.1.0</javasmt.version>
+    <javasmt.version>5.0.0</javasmt.version>
+    <bitwuzla.version>0.4.0-g4dbf3b1f</bitwuzla.version>
     <boolector.version>3.2.2-g1a89c229</boolector.version>
     <cvc4.version>1.8-prerelease-2020-06-24-g7825d8f28</cvc4.version>
     <cvc5.version>1.0.5-g4cb2ab9eb</cvc5.version>
     <mathsat.version>5.6.10</mathsat.version>
-    <opensmt.version>2.5.2-g7f502169</opensmt.version>
-    <javasmt-yices.version>4.1.0-1-gc58fe5b4</javasmt-yices.version>
+    <opensmt.version>2.6.0-g2f72cc0e</opensmt.version>
+    <javasmt-yices.version>4.1.1-734-g3732f7e08</javasmt-yices.version>
     <yices.version>2.6.2-396-g194350c1</yices.version>
-    <z3.version>4.12.2</z3.version>
+    <z3.version>4.12.5</z3.version>
   </properties>
 
   <dependencies>
@@ -119,6 +120,22 @@ SPDX-License-Identifier: Apache-2.0
       <classifier>libz3java</classifier>
     </dependency>
 
+    <!-- Bitwuzla has two dependencies (on Linux) -->
+    <dependency>
+      <groupId>org.sosy-lab</groupId>
+      <artifactId>javasmt-solver-bitwuzla</artifactId>
+      <version>${bitwuzla.version}</version>
+      <type>jar</type>
+      <classifier>bitwuzla</classifier>
+    </dependency>
+    <dependency>
+      <groupId>org.sosy-lab</groupId>
+      <artifactId>javasmt-solver-bitwuzla</artifactId>
+      <version>${bitwuzla.version}</version>
+      <type>so</type>
+      <classifier>libbitwuzlaj</classifier>
+    </dependency>
+
     <!-- Boolector has three dependencies (on Linux) -->
     <dependency>
       <groupId>org.sosy-lab</groupId>
@@ -368,6 +385,15 @@ SPDX-License-Identifier: Apache-2.0
                 <destFileName>libz3.so</destFileName>
               </artifactItem>
 
+              <!-- Bitwuzla has one dependency (on Linux) -->
+              <artifactItem>
+                <groupId>org.sosy-lab</groupId>
+                <artifactId>javasmt-solver-bitwuzla</artifactId>
+                <type>so</type>
+                <classifier>libbitwuzlaj</classifier>
+                <destFileName>libbitwuzlaj.so</destFileName>
+              </artifactItem>
+
               <!-- Boolector has three dependencies (on Linux) -->
               <artifactItem>
                 <groupId>org.sosy-lab</groupId>

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
@@ -2,7 +2,7 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2021 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -15,10 +15,13 @@
 
 import com.google.common.base.Joiner;
 import com.google.common.base.Splitter;
+import java.util.Arrays;
 import java.util.List;
 import org.junit.After;
 import org.junit.Before;
 import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.Parameterized;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.common.configuration.Configuration;
 import org.sosy_lab.common.configuration.InvalidConfigurationException;
@@ -28,7 +31,7 @@
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.SolverContext;
 import org.sosy_lab.java_smt.api.SolverException;
-import org.sosy_lab.java_smt.example.Sudoku.IntegerBasedSudokuSolver;
+import org.sosy_lab.java_smt.example.Sudoku;
 import org.sosy_lab.java_smt.example.Sudoku.SudokuSolver;
 
 /**
@@ -69,8 +72,17 @@
  * 451839627
  * </pre>
  */
+@RunWith(Parameterized.class)
 public class SudokuTest {
 
+  @Parameterized.Parameters(name = "{0}")
+  public static List<Solvers> getSolvers() {
+    return Arrays.asList(Solvers.values());
+  }
+
+  @Parameterized.Parameter(0)
+  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");
@@ -95,6 +107,7 @@ private static boolean isOperatingSystemSupported(Solvers solver) {
       case YICES2:
         return IS_LINUX;
       case MATHSAT5:
+      case BITWUZLA:
         return IS_LINUX || IS_WINDOWS;
       case Z3:
         return IS_LINUX || IS_WINDOWS || IS_MAC;
@@ -149,50 +162,14 @@ public final void closeSolver() {
   }
 
   @Test
-  public void princessSudokuTest()
-      throws InvalidConfigurationException, InterruptedException, SolverException {
-    checkSudoku(Solvers.PRINCESS);
-  }
-
-  @Test
-  public void z3SudokuTest()
-      throws InvalidConfigurationException, InterruptedException, SolverException {
-    checkSudoku(Solvers.Z3);
-  }
-
-  @Test
-  public void mathsatSudokuTest()
-      throws InvalidConfigurationException, InterruptedException, SolverException {
-    checkSudoku(Solvers.MATHSAT5);
-  }
-
-  @Test
-  public void boolectorSudokuTest()
-      throws InvalidConfigurationException, InterruptedException, SolverException {
-    // Boolector does not support Integer logic
-    // checkSudoku(Solvers.BOOLECTOR);
-  }
-
-  @Test
-  public void cvc4SudokuTest()
-      throws InvalidConfigurationException, InterruptedException, SolverException {
-    checkSudoku(Solvers.CVC4);
-  }
-
-  @Test
-  public void yices2SudokuTest()
-      throws InvalidConfigurationException, InterruptedException, SolverException {
-    checkSudoku(Solvers.YICES2);
-  }
-
-  private void checkSudoku(Solvers solver)
+  public void checkSudoku()
       throws InvalidConfigurationException, InterruptedException, SolverException {
     assumeTrue(isOperatingSystemSupported(solver));
 
     context = SolverContextFactory.createSolverContext(config, logger, notifier, solver);
     Integer[][] grid = readGridFromString(input);
 
-    SudokuSolver<?> sudoku = new IntegerBasedSudokuSolver(context);
+    SudokuSolver<?> sudoku = new Sudoku.BooleanBasedSudokuSolver(context);
     Integer[][] solution = sudoku.solve(grid);
 
     assertNotNull(solution);

diff --git a/doc/Example-Maven-Web-Project/pom.xml b/doc/Example-Maven-Web-Project/pom.xml
@@ -16,9 +16,8 @@ SPDX-License-Identifier: Apache-2.0
 
   <groupId>org.sosy_lab.java_smt_web_example</groupId>
   <artifactId>java-smt-web-example</artifactId>
-  <version>1.9</version>
+  <version>1.10</version>
   <packaging>war</packaging>
-
   <name>java-smt-maven-web-example</name>
   <description>Example Maven project to show how to use JavaSMT with native solver libraries in a web project.</description>
   <url>https://github.com/sosy-lab/java-smt</url>
@@ -65,21 +64,22 @@ SPDX-License-Identifier: Apache-2.0
 
   <properties>
     <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
-    <maven.compiler.source>11</maven.compiler.source>
-    <maven.compiler.target>11</maven.compiler.target>
-    <maven.compiler.release>11</maven.compiler.release>
+    <maven.compiler.source>17</maven.compiler.source>
+    <maven.compiler.target>17</maven.compiler.target>
+    <maven.compiler.release>17</maven.compiler.release>
     <project.dependency.relativepath>dependency</project.dependency.relativepath>
     <project.dependency.path>${project.build.directory}/${project.dependency.relativepath}</project.dependency.path>
 
-    <javasmt.version>4.1.0</javasmt.version>
+    <javasmt.version>5.0.0</javasmt.version>
+    <bitwuzla.version>0.4.0-g4dbf3b1f</bitwuzla.version>
     <boolector.version>3.2.2-g1a89c229</boolector.version>
     <cvc4.version>1.8-prerelease-2020-06-24-g7825d8f28</cvc4.version>
     <cvc5.version>1.0.5-g4cb2ab9eb</cvc5.version>
     <mathsat.version>5.6.10</mathsat.version>
-    <opensmt.version>2.5.2-g7f502169</opensmt.version>
-    <javasmt-yices.version>4.1.0-1-gc58fe5b4</javasmt-yices.version>
+    <opensmt.version>2.6.0-g2f72cc0e</opensmt.version>
+    <javasmt-yices.version>4.1.1-734-g3732f7e08</javasmt-yices.version>
     <yices.version>2.6.2-396-g194350c1</yices.version>
-    <z3.version>4.12.2</z3.version>
+    <z3.version>4.12.5</z3.version>
   </properties>
 
   <dependencies>
@@ -121,6 +121,22 @@ SPDX-License-Identifier: Apache-2.0
       <classifier>libz3java</classifier>
     </dependency>
 
+    <!-- Bitwuzla has two dependencies (on Linux) -->
+    <dependency>
+      <groupId>org.sosy-lab</groupId>
+      <artifactId>javasmt-solver-bitwuzla</artifactId>
+      <version>${bitwuzla.version}</version>
+      <type>jar</type>
+      <classifier>bitwuzla</classifier>
+    </dependency>
+    <dependency>
+      <groupId>org.sosy-lab</groupId>
+      <artifactId>javasmt-solver-bitwuzla</artifactId>
+      <version>${bitwuzla.version}</version>
+      <type>so</type>
+      <classifier>libbitwuzlaj</classifier>
+    </dependency>
+
     <!-- Boolector has three dependencies (on Linux) -->
     <dependency>
       <groupId>org.sosy-lab</groupId>
@@ -268,7 +284,7 @@ SPDX-License-Identifier: Apache-2.0
     <dependency>
       <groupId>jakarta.servlet</groupId>
       <artifactId>jakarta.servlet-api</artifactId>
-      <version>6.0.0</version>
+      <version>6.1.0</version>
     </dependency>
   </dependencies>
 
@@ -279,7 +295,7 @@ SPDX-License-Identifier: Apache-2.0
           <!-- This step starts its own JVM that ignores system properties set by the user,
                because why would those ever be important?! -->
           <artifactId>maven-surefire-plugin</artifactId>
-          <version>2.22.1</version>
+          <version>3.0.0</version>
           <configuration>
             <!-- For solvers with native binaries, you need to add the classpath to test properly.
                  This path needs to be the location of the sosy-lab.commons.jar and the solver binaries.
@@ -290,7 +306,7 @@ SPDX-License-Identifier: Apache-2.0
         <plugin>
           <groupId>org.apache.maven.plugins</groupId>
           <artifactId>maven-war-plugin</artifactId>
-          <version>3.3.1</version>
+          <version>3.4.0</version>
           <configuration>
             <archive>
               <manifest>
@@ -328,7 +344,7 @@ SPDX-License-Identifier: Apache-2.0
         </plugin>
         <plugin>
           <artifactId>maven-jar-plugin</artifactId>
-          <version>3.0.2</version>
+          <version>3.4.0</version>
           <configuration>
             <archive>
               <manifest>
@@ -416,6 +432,15 @@ SPDX-License-Identifier: Apache-2.0
               <destFileName>libz3.so</destFileName>
             </artifactItem>
 
+            <!-- Bitwuzla has one dependency (on Linux) -->
+            <artifactItem>
+              <groupId>org.sosy-lab</groupId>
+              <artifactId>javasmt-solver-bitwuzla</artifactId>
+              <type>so</type>
+              <classifier>libbitwuzlaj</classifier>
+              <destFileName>libbitwuzlaj.so</destFileName>
+            </artifactItem>
+
             <!-- Boolector has three dependencies (on Linux) -->
             <artifactItem>
               <groupId>org.sosy-lab</groupId>

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
@@ -2,21 +2,20 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2021 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
 package org.sosy_lab;
 
+import jakarta.servlet.ServletException;
+import jakarta.servlet.annotation.WebServlet;
+import jakarta.servlet.http.HttpServlet;
+import jakarta.servlet.http.HttpServletRequest;
+import jakarta.servlet.http.HttpServletResponse;
 import java.io.IOException;
 import java.io.PrintWriter;
 
-import javax.servlet.ServletException;
-import javax.servlet.annotation.WebServlet;
-import javax.servlet.http.HttpServlet;
-import javax.servlet.http.HttpServletRequest;
-import javax.servlet.http.HttpServletResponse;
-
 import java.util.ArrayList;
 import java.util.Comparator;
 import java.util.List;