From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 17 Dec 2021 23:50:59 +0000 (-0800)
Subject: api: java: Support default arity for Solver::mkUnresolvedSort(). (#7842)
X-Git-Tag: cvc5-1.0.0~633
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=99992303744ca89478aa077af71e6e5dd7885ee1;p=cvc5.git

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 1e24222b3..d04b766e0 100644
--- 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 ca0032c22..f6fa3d6f1 100644
--- 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));
   }