cppapi: Remove Datatype::hasNestedRecursion(). (#7878)

Datatypes with nested recursion are a highly experimental feature and we
currentle don't even have a decision procedure for them.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 65ea108df19e4164405bc0cf3180d55eb371270e..a6036485fb9d48754558b634024a5de6e376dad4 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -4212,15 +4212,6 @@ bool Datatype::isWellFounded() const
   ////////
   CVC5_API_TRY_CATCH_END;
 }
-bool Datatype::hasNestedRecursion() const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK_NOT_NULL;
-  //////// all checks before this line
-  return d_dtype->hasNestedRecursion();
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
 
 bool Datatype::isNull() const
 {

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 21f51a9c8aa8c45a95b14b328c5903094b97f1d5..2ebbff313ff5b939665d5f1217babc496390d426 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -2311,17 +2311,6 @@ class CVC5_EXPORT Datatype
    */
   bool isWellFounded() const;
 
-  /**
-   * Does this datatype have nested recursion? This method returns false if a
-   * value of this datatype includes a subterm of its type that is nested
-   * beneath a non-datatype type constructor. For example, a datatype
-   * T containing a constructor having a selector with codomain type (Set T)
-   * has nested recursion.
-   *
-   * @return true if this datatype has nested recursion
-   */
-  bool hasNestedRecursion() const;
-
   /**
    * @return true if this Datatype is a null object
    */

diff --git a/src/api/java/io/github/cvc5/api/Datatype.java b/src/api/java/io/github/cvc5/api/Datatype.java
index b96781fd59957426129c031998969e013b597a7b..47732b7ddb697d114fbd60d3d9010149207bd53c 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Datatype.java
+++ b/src/api/java/io/github/cvc5/api/Datatype.java
@@ -174,22 +174,6 @@ public class Datatype extends AbstractPointer implements Iterable<DatatypeConstr
 
   private native boolean isWellFounded(long pointer);
 
-  /**
-   * Does this datatype have nested recursion? This method returns false if a
-   * value of this datatype includes a subterm of its type that is nested
-   * beneath a non-datatype type constructor. For example, a datatype
-   * T containing a constructor having a selector with codomain type (Set T)
-   * has nested recursion.
-   *
-   * @return true if this datatype has nested recursion
-   */
-  public boolean hasNestedRecursion()
-  {
-    return hasNestedRecursion(pointer);
-  }
-
-  private native boolean hasNestedRecursion(long pointer);
-
   /**
    * @return true if this Datatype is a null object
    */

diff --git a/src/api/java/jni/datatype.cpp b/src/api/java/jni/datatype.cpp
index 6cc8ba58e91e8f48cf305f968a86f97de74fb0b6..1957e94f9ad07bd83f50505e49ec5fff0ab50b26 100644 (file)
--- a/src/api/java/jni/datatype.cpp
+++ b/src/api/java/jni/datatype.cpp
@@ -218,20 +218,6 @@ JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Datatype_isWellFounded(
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
-/*
- * Class:     io_github_cvc5_api_Datatype
- * Method:    hasNestedRecursion
- * Signature: (J)Z
- */
-JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Datatype_hasNestedRecursion(
-    JNIEnv* env, jobject, jlong pointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  Datatype* current = (Datatype*)pointer;
-  return (jboolean)current->hasNestedRecursion();
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
-
 /*
  * Class:     io_github_cvc5_api_Datatype
  * Method:    isNull

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 43108d2426b9e38cfda3a862ea7baffa40549fba..226bd2645ec3b2a0cebaa741c1298f129615f740 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -58,7 +58,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint isRecord() except +
         bint isFinite() except +
         bint isWellFounded() except +
-        bint hasNestedRecursion() except +
         bint isNull() except +
         string toString() except +
         cppclass const_iterator:

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 0ef8dce55498bf354696d989acb966f93394f7c1..e455c1872b986a8498c0eaf7180c7d85652c1177 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -189,10 +189,6 @@ cdef class Datatype:
         """:return: True if this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() <cvc5::api::Datatype::isWellFounded>`)."""
         return self.cd.isWellFounded()
 
-    def hasNestedRecursion(self):
-        """:return: True if this datatype has nested recursion (see :cpp:func:`Datatype::hasNestedRecursion() <cvc5::api::Datatype::hasNestedRecursion>`)."""
-        return self.cd.hasNestedRecursion()
-
     def isNull(self):
         """:return: True if this Datatype is a null object."""
         return self.cd.isNull()

diff --git a/test/unit/api/cpp/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp
index f241c4821af4dc79ff11fea05715acf9eb8b2898..949c137cbbb3dba807e4ea85260b5a9771c7d5d1 100644 (file)
--- a/test/unit/api/cpp/datatype_api_black.cpp
+++ b/test/unit/api/cpp/datatype_api_black.cpp
@@ -408,9 +408,6 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec)
   ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
   ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded());
   ASSERT_TRUE(dtsorts[2].getDatatype().isWellFounded());
-  ASSERT_FALSE(dtsorts[0].getDatatype().hasNestedRecursion());
-  ASSERT_FALSE(dtsorts[1].getDatatype().hasNestedRecursion());
-  ASSERT_FALSE(dtsorts[2].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -441,7 +438,6 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec)
       dtsorts[0].getDatatype()[0][0].getCodomainSort().getArrayElementSort(),
       dtsorts[0]);
   ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
-  ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -478,8 +474,6 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec)
   ASSERT_EQ(dtsorts.size(), 2);
   ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
   ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded());
-  ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
-  ASSERT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -516,8 +510,6 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec)
   ASSERT_EQ(dtsorts.size(), 2);
   ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
   ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded());
-  ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
-  ASSERT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -553,7 +545,6 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec)
   ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
   ASSERT_EQ(dtsorts.size(), 1);
   ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
-  ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
 }
 
 TEST_F(TestApiBlackDatatype, datatypeSpecializedCons)

diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java
index 246e75ac1527f56fd65ba6b0e1faf6ebb6ff26f9..f1d51e15063962d7bbd6bf0c4606c18a0e14cdf6 100644 (file)
--- a/test/unit/api/java/DatatypeTest.java
+++ b/test/unit/api/java/DatatypeTest.java
@@ -382,9 +382,6 @@ class DatatypeTest
     assertTrue(dtsorts.get(0).getDatatype().isWellFounded());
     assertTrue(dtsorts.get(1).getDatatype().isWellFounded());
     assertTrue(dtsorts.get(2).getDatatype().isWellFounded());
-    assertFalse(dtsorts.get(0).getDatatype().hasNestedRecursion());
-    assertFalse(dtsorts.get(1).getDatatype().hasNestedRecursion());
-    assertFalse(dtsorts.get(2).getDatatype().hasNestedRecursion());
 
     /* Create mutual datatypes corresponding to this definition block:
      *   DATATYPE
@@ -420,7 +417,6 @@ class DatatypeTest
                      .getArrayElementSort(),
         dtsorts.get(0));
     assertTrue(dtsorts.get(0).getDatatype().isWellFounded());
-    assertTrue(dtsorts.get(0).getDatatype().hasNestedRecursion());
 
     /* Create mutual datatypes corresponding to this definition block:
      *   DATATYPE
@@ -458,8 +454,6 @@ class DatatypeTest
     assertEquals(dtsorts.size(), 2);
     assertTrue(dtsorts.get(0).getDatatype().isWellFounded());
     assertTrue(dtsorts.get(1).getDatatype().isWellFounded());
-    assertTrue(dtsorts.get(0).getDatatype().hasNestedRecursion());
-    assertTrue(dtsorts.get(1).getDatatype().hasNestedRecursion());
 
     /* Create mutual datatypes corresponding to this definition block:
      *   DATATYPE
@@ -497,8 +491,6 @@ class DatatypeTest
     assertEquals(dtsorts.size(), 2);
     assertTrue(dtsorts.get(0).getDatatype().isWellFounded());
     assertTrue(dtsorts.get(1).getDatatype().isWellFounded());
-    assertTrue(dtsorts.get(0).getDatatype().hasNestedRecursion());
-    assertTrue(dtsorts.get(1).getDatatype().hasNestedRecursion());
 
     /* Create mutual datatypes corresponding to this definition block:
      *   DATATYPE
@@ -535,7 +527,6 @@ class DatatypeTest
     dtsorts = atomic.get();
     assertEquals(dtsorts.size(), 1);
     assertTrue(dtsorts.get(0).getDatatype().isWellFounded());
-    assertTrue(dtsorts.get(0).getDatatype().hasNestedRecursion());
   }
 
   @Test void datatypeSpecializedCons() throws CVC5ApiException

diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py
index d0cf6d4e50cc3a42edf219e335fa62188f3dea8b..a818c512ea33d49669b61dae699d8311ac76170b 100644 (file)
--- a/test/unit/api/python/test_datatype_api.py
+++ b/test/unit/api/python/test_datatype_api.py
@@ -397,9 +397,6 @@ def test_datatype_simply_rec(solver):
     assert dtsorts[0].getDatatype().isWellFounded()
     assert dtsorts[1].getDatatype().isWellFounded()
     assert dtsorts[2].getDatatype().isWellFounded()
-    assert not dtsorts[0].getDatatype().hasNestedRecursion()
-    assert not dtsorts[1].getDatatype().hasNestedRecursion()
-    assert not dtsorts[2].getDatatype().hasNestedRecursion()
 
     # Create mutual datatypes corresponding to this definition block:
     #   DATATYPE
@@ -428,7 +425,6 @@ def test_datatype_simply_rec(solver):
     assert dtsorts[0].getDatatype()[0][0].getCodomainSort().getArrayElementSort() \
         == dtsorts[0]
     assert dtsorts[0].getDatatype().isWellFounded()
-    assert dtsorts[0].getDatatype().hasNestedRecursion()
 
     # Create mutual datatypes corresponding to this definition block:
     #   DATATYPE
@@ -464,8 +460,6 @@ def test_datatype_simply_rec(solver):
     assert len(dtsorts) == 2
     assert dtsorts[0].getDatatype().isWellFounded()
     assert dtsorts[1].getDatatype().isWellFounded()
-    assert dtsorts[0].getDatatype().hasNestedRecursion()
-    assert dtsorts[1].getDatatype().hasNestedRecursion()
 
     # Create mutual datatypes corresponding to this definition block:
     #   DATATYPE
@@ -500,8 +494,6 @@ def test_datatype_simply_rec(solver):
     assert len(dtsorts) == 2
     assert dtsorts[0].getDatatype().isWellFounded()
     assert dtsorts[1].getDatatype().isWellFounded()
-    assert dtsorts[0].getDatatype().hasNestedRecursion()
-    assert dtsorts[1].getDatatype().hasNestedRecursion()
 
     # Create mutual datatypes corresponding to this definition block:
     #   DATATYPE
@@ -535,7 +527,6 @@ def test_datatype_simply_rec(solver):
     dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes)
     assert len(dtsorts) == 1
     assert dtsorts[0].getDatatype().isWellFounded()
-    assert dtsorts[0].getDatatype().hasNestedRecursion()
 
 
 def test_datatype_specialized_cons(solver):