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 39410a4e67d15da912bf5e0aec02528a4b7b5e4d..e062e60ed15e1f73675d5fb109ce450f17cb0d92 100644 (file)
--- 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 0f6e2759cfd77a82a5c8e90ee7bb3d75370cd80e..23aec2386e3dfeaf1a45e84c67e203f3e589a267 100644 (file)
--- 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