api: java: Support default arity for Solver::mkUnresolvedSort(). (#7842)

diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index 1e24222b3a492fa057e715703354077107a66bf4..d04b766e0633cd187c52cb70cfa114c5a7ea1a23 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -439,6 +439,20 @@ public class Solver implements IPointer, AutoCloseable
 
   private native long mkUnresolvedSort(long pointer, String symbol, int arity);
 
+  /**
+   * Create an unresolved sort.
+   *
+   * This is for creating yet unresolved sort placeholders for mutually
+   * recursive datatypes without sort parameters.
+   *
+   * @param symbol the symbol of the sort
+   * @return the unresolved sort
+   */
+  public Sort mkUnresolvedSort(String symbol) throws CVC5ApiException
+  {
+    return mkUnresolvedSort(symbol, 0);
+  }
+
   /**
    * Create a sort constructor sort.
    * @param symbol the symbol of the sort

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index ca0032c22f238fd626a25284ab099cc2295b5c2b..f6fa3d6f1eca86dffa42b1c52c4a677f57cd19b0 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -336,9 +336,9 @@ class SolverTest
 
   @Test void mkUnresolvedSort() throws CVC5ApiException
   {
-    assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("u", 0));
+    assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("u"));
     assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("u", 1));
-    assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("", 0));
+    assertDoesNotThrow(() -> d_solver.mkUnresolvedSort(""));
     assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("", 1));
   }