From 99992303744ca89478aa077af71e6e5dd7885ee1 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 17 Dec 2021 15:50:59 -0800 Subject: [PATCH] api: java: Support default arity for Solver::mkUnresolvedSort(). (#7842) --- src/api/java/io/github/cvc5/api/Solver.java | 14 ++++++++++++++ test/unit/api/java/SolverTest.java | 4 ++-- 2 files changed, 16 insertions(+), 2 deletions(-) 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)); } -- 2.30.2