From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 8 Dec 2021 03:22:04 +0000 (-0800)
Subject: api: Fix Sort::getDatatypeArity() for non-parametric datatypes. (#7766)
X-Git-Tag: cvc5-1.0.0~705
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fd127d90b9cf4c769c1fe1a9b16b811847a0eed9;p=cvc5.git

api: Fix Sort::getDatatypeArity() for non-parametric datatypes. (#7766)

Fixes cvc5/cvc5-projects#380
---

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 39410a4e6..e062e60ed 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1763,7 +1763,7 @@ size_t Sort::getDatatypeArity() const
   CVC5_API_CHECK_NOT_NULL;
   CVC5_API_CHECK(isDatatype()) << "Not a datatype sort.";
   //////// all checks before this line
-  return d_type->getNumChildren() - 1;
+  return d_type->isParametricDatatype() ? d_type->getNumChildren() - 1 : 0;
   ////////
   CVC5_API_TRY_CATCH_END;
 }
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 0f6e2759c..23aec2386 100644
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -2671,5 +2671,12 @@ TEST_F(TestApiBlackSolver, doubleUseCons)
                CVC5ApiException);
 }
 
+TEST_F(TestApiBlackSolver, getDatatypeArity)
+{
+  DatatypeConstructorDecl ctor1 = d_solver.mkDatatypeConstructorDecl("_x21");
+  DatatypeConstructorDecl ctor2 = d_solver.mkDatatypeConstructorDecl("_x31");
+  Sort s3 = d_solver.declareDatatype(std::string("_x17"), {ctor1, ctor2});
+  ASSERT_EQ(s3.getDatatypeArity(), 0);
+}
 }  // namespace test
 }  // namespace cvc5