Properly guard sort instantiate (#8247)

Fixes cvc5/cvc5-projects#387.

Adds a prefix of that unit test before the first exception.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index d1e0dc12ea8f5944cbfbd07c3fca8f7727295a30..d16dbfa5a7b216db7ce3a9e8ee2bfc9edea4c1bb 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1373,9 +1373,12 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
   CVC5_API_CHECK_DOMAIN_SORTS(params);
   CVC5_API_CHECK(isParametricDatatype() || isSortConstructor())
       << "Expected parametric datatype or sort constructor sort.";
-  CVC5_API_CHECK(isSortConstructor()
+  CVC5_API_CHECK(!isParametricDatatype()
                  || d_type->getNumChildren() == params.size() + 1)
       << "Arity mismatch for instantiated parametric datatype";
+  CVC5_API_CHECK(!isSortConstructor()
+                 || d_type->getSortConstructorArity() == params.size())
+      << "Arity mismatch for instantiated sort constructor";
   //////// all checks before this line
   std::vector<cvc5::TypeNode> tparams = sortVectorToTypeNodes(params);
   if (d_type->isDatatype())

diff --git a/test/unit/api/cpp/CMakeLists.txt b/test/unit/api/cpp/CMakeLists.txt
index c10214803a47348b53fa1923bdd55b4b2d9b81d6..0125d69623c91b12d4329f4f9fa3aef33601ef5f 100644 (file)
--- a/test/unit/api/cpp/CMakeLists.txt
+++ b/test/unit/api/cpp/CMakeLists.txt
@@ -16,6 +16,7 @@ cvc5_add_unit_test_black(datatype_api_black api)
 cvc5_add_unit_test_black(grammar_black api)
 cvc5_add_unit_test_black(op_black api)
 cvc5_add_unit_test_white(op_white api)
+cvc5_add_unit_test_black(parametric_datatype_black api)
 cvc5_add_unit_test_black(result_black api)
 cvc5_add_unit_test_black(solver_black api)
 cvc5_add_unit_test_white(solver_white api)

diff --git a/test/unit/api/cpp/parametric_datatype_black.cpp b/test/unit/api/cpp/parametric_datatype_black.cpp
new file mode 100644 (file)
index 0000000..6c4bb80
--- /dev/null
+++ b/test/unit/api/cpp/parametric_datatype_black.cpp
@@ -0,0 +1,47 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Blackbox tests involving parametric datatypes.
+ */
+
+#include "test_api.h"
+#include "base/configuration.h"
+
+namespace cvc5 {
+
+using namespace api;
+
+namespace test {
+
+class TestApiBlackParametricDatatype : public TestApi
+{
+};
+
+TEST_F(TestApiBlackParametricDatatype, proj_issue387)
+{
+  Sort s1 = d_solver.getBooleanSort();
+
+  Sort u1 = d_solver.mkSortConstructorSort("_x0", 1);
+  Sort u2 = d_solver.mkSortConstructorSort("_x1", 1);
+  Sort p1 = d_solver.mkParamSort("_x4");
+  Sort p2 = d_solver.mkParamSort("_x27");
+  Sort p3 = d_solver.mkParamSort("_x3");
+
+  DatatypeDecl dtdecl1 = d_solver.mkDatatypeDecl("_x0", p1);
+  DatatypeConstructorDecl ctordecl1 =
+      d_solver.mkDatatypeConstructorDecl("_x18");
+  ASSERT_THROW(ctordecl1.addSelector("_x17", u2.instantiate({p1, p1})),
+               CVC5ApiException);
+}
+
+}  // namespace test
+}  // namespace cvc5