From 8bbff8818e7b6e1c697d3dd6d88afbeaae80c0d6 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 5 Jan 2022 12:23:17 -0800
Subject: [PATCH 1/1] api: Add missing guard for Datatype::isFinite(). (#7879)

---
 src/api/cpp/cvc5.cpp                      |  2 ++
 test/unit/api/cpp/datatype_api_black.cpp  | 19 +++++++++++++++++++
 test/unit/api/java/DatatypeTest.java      | 20 ++++++++++++++++++++
 test/unit/api/python/test_datatype_api.py | 18 +++++++++++++++++-
 4 files changed, 58 insertions(+), 1 deletion(-)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index e794606aa..65ea108df 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -4193,6 +4193,8 @@ bool Datatype::isFinite() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_CHECK(!d_dtype->isParametric())
+      << "Invalid call to 'isFinite()', expected non-parametric Datatype";
   //////// all checks before this line
   // we assume that finite model finding is disabled by passing false as the
   // second argument
diff --git a/test/unit/api/cpp/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp
index bf4a2cd11..f241c4821 100644
--- a/test/unit/api/cpp/datatype_api_black.cpp
+++ b/test/unit/api/cpp/datatype_api_black.cpp
@@ -337,6 +337,25 @@ TEST_F(TestApiBlackDatatype, parametricDatatype)
   ASSERT_TRUE(pairIntInt.isSubsortOf(pairIntInt));
 }
 
+TEST_F(TestApiBlackDatatype, isFinite)
+{
+  DatatypeDecl dtypedecl = d_solver.mkDatatypeDecl("dt", {});
+  DatatypeConstructorDecl ctordecl = d_solver.mkDatatypeConstructorDecl("cons");
+  ctordecl.addSelector("sel", d_solver.getBooleanSort());
+  dtypedecl.addConstructor(ctordecl);
+  Sort dtype = d_solver.mkDatatypeSort(dtypedecl);
+  ASSERT_TRUE(dtype.getDatatype().isFinite());
+
+  Sort p = d_solver.mkParamSort("p1");
+  DatatypeDecl pdtypedecl = d_solver.mkDatatypeDecl("dt", {p});
+  DatatypeConstructorDecl pctordecl =
+      d_solver.mkDatatypeConstructorDecl("cons");
+  pctordecl.addSelector("sel", p);
+  pdtypedecl.addConstructor(pctordecl);
+  Sort pdtype = d_solver.mkDatatypeSort(pdtypedecl);
+  ASSERT_THROW(pdtype.getDatatype().isFinite(), CVC5ApiException);
+}
+
 TEST_F(TestApiBlackDatatype, datatypeSimplyRec)
 {
   /* Create mutual datatypes corresponding to this definition block:
diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java
index afca8a92f..246e75ac1 100644
--- a/test/unit/api/java/DatatypeTest.java
+++ b/test/unit/api/java/DatatypeTest.java
@@ -310,6 +310,26 @@ class DatatypeTest
     assertTrue(pairIntInt.isSubsortOf(pairIntInt));
   }
 
+  @Test void datatypeIsFinite() throws CVC5ApiException
+  {
+    List<Sort> v = new ArrayList<>();
+    DatatypeDecl dtypedecl = d_solver.mkDatatypeDecl("dt", v);
+    DatatypeConstructorDecl ctordecl = d_solver.mkDatatypeConstructorDecl("cons");
+    ctordecl.addSelector("sel", d_solver.getBooleanSort());
+    dtypedecl.addConstructor(ctordecl);
+    Sort dtype = d_solver.mkDatatypeSort(dtypedecl);
+    assertTrue(dtype.getDatatype().isFinite());
+
+    Sort p = d_solver.mkParamSort("p1");
+    v.add(p);
+    DatatypeDecl pdtypedecl = d_solver.mkDatatypeDecl("dt", v);
+    DatatypeConstructorDecl pctordecl = d_solver.mkDatatypeConstructorDecl("cons");
+    pctordecl.addSelector("sel", p);
+    pdtypedecl.addConstructor(pctordecl);
+    Sort pdtype = d_solver.mkDatatypeSort(pdtypedecl);
+    assertThrows(CVC5ApiException.class, () -> pdtype.getDatatype().isFinite());
+  }
+
   @Test void datatypeSimplyRec() throws CVC5ApiException
   {
     /* Create mutual datatypes corresponding to this definition block:
diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py
index a883596de..d0cf6d4e5 100644
--- a/test/unit/api/python/test_datatype_api.py
+++ b/test/unit/api/python/test_datatype_api.py
@@ -264,7 +264,7 @@ def test_parametric_datatype(solver):
     v.append(t1)
     v.append(t2)
     pairSpec = solver.mkDatatypeDecl("pair", v)
-        
+
     mkpair = solver.mkDatatypeConstructorDecl("mk-pair")
     mkpair.addSelector("first", t1)
     mkpair.addSelector("second", t2)
@@ -334,6 +334,22 @@ def test_parametric_datatype(solver):
     assert not pairRealInt.isSubsortOf(pairIntInt)
     assert pairIntInt.isSubsortOf(pairIntInt)
 
+def test_is_finite(solver):
+    dtypedecl = solver.mkDatatypeDecl("dt", [])
+    ctordecl = solver.mkDatatypeConstructorDecl("cons")
+    ctordecl.addSelector("sel", solver.getBooleanSort())
+    dtypedecl.addConstructor(ctordecl)
+    dtype = solver.mkDatatypeSort(dtypedecl)
+    assert dtype.getDatatype().isFinite()
+
+    p = solver.mkParamSort("p1")
+    pdtypedecl = solver.mkDatatypeDecl("dt", [p])
+    pctordecl = solver.mkDatatypeConstructorDecl("cons")
+    pctordecl.addSelector("sel", p)
+    pdtypedecl.addConstructor(pctordecl)
+    pdtype = solver.mkDatatypeSort(pdtypedecl)
+    with pytest.raises(RuntimeError):
+        pdtype.getDatatype().isFinite()
 
 def test_datatype_simply_rec(solver):
     # Create mutual datatypes corresponding to this definition block:
-- 
2.30.2