From 7f4fe916ceda4a42ccbad740d620e5ef852f0280 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 5 Jan 2022 13:20:05 -0800 Subject: [PATCH] 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. --- src/api/cpp/cvc5.cpp | 9 --------- src/api/cpp/cvc5.h | 11 ----------- src/api/java/io/github/cvc5/api/Datatype.java | 16 ---------------- src/api/java/jni/datatype.cpp | 14 -------------- src/api/python/cvc5.pxd | 1 - src/api/python/cvc5.pxi | 4 ---- test/unit/api/cpp/datatype_api_black.cpp | 9 --------- test/unit/api/java/DatatypeTest.java | 9 --------- test/unit/api/python/test_datatype_api.py | 9 --------- 9 files changed, 82 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 65ea108df..a6036485f 100644 --- 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 21f51a9c8..2ebbff313 100644 --- 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 b96781fd5..47732b7dd 100644 --- 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 IterablehasNestedRecursion(); - 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 43108d242..226bd2645 100644 --- 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 0ef8dce55..e455c1872 100644 --- 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() `).""" return self.cd.isWellFounded() - def hasNestedRecursion(self): - """:return: True if this datatype has nested recursion (see :cpp:func:`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 f241c4821..949c137cb 100644 --- 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 246e75ac1..f1d51e150 100644 --- 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 d0cf6d4e5..a818c512e 100644 --- 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): -- 2.30.2