From d7928407399b8528998ce3e21526ec51dbdc5dcb Mon Sep 17 00:00:00 2001
From: Josh Berdine <josh@berdine.net>
Date: Tue, 8 Apr 2025 22:36:57 +0100
Subject: [PATCH] Add Z3_is_recursive_datatype_sort to the API (#7615)

It does not seem to be possible to test if a datatype sort is recursive.
---
 src/api/api_datatype.cpp | 10 ++++++++++
 src/api/z3_api.h         |  7 +++++++
 2 files changed, 17 insertions(+)

diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp
index 5c85ea2cd..2509434f8 100644
--- a/src/api/api_datatype.cpp
+++ b/src/api/api_datatype.cpp
@@ -443,6 +443,16 @@ extern "C" {
         Z3_CATCH;
     }
 
+    bool Z3_API Z3_is_recursive_datatype_sort(Z3_context c, Z3_sort t) {
+        Z3_TRY;
+        LOG_Z3_is_recursive_datatype_sort(c, t);
+        RESET_ERROR_CODE();
+        sort * s = to_sort(t);
+        datatype_util& dt_util = mk_c(c)->dtutil();
+        return dt_util.is_datatype(s) && dt_util.is_recursive(s);
+        Z3_CATCH_RETURN(false);
+    }
+
     unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t) {
         Z3_TRY;
         LOG_Z3_get_datatype_sort_num_constructors(c, t);
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index dafc26881..b0ac82cab 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -4588,6 +4588,13 @@ extern "C" {
     */
     Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(Z3_context c, Z3_sort t, unsigned i);
 
+    /**
+       \brief Check if \c s is a recursive datatype sort.
+
+       def_API('Z3_is_recursive_datatype_sort', BOOL, (_in(CONTEXT), _in(SORT)))
+     */
+    bool Z3_API Z3_is_recursive_datatype_sort(Z3_context c, Z3_sort s);
+
     /**
         \brief Return number of constructors for datatype.