Guard parametric datatypes instantiated by non-first-class sorts (#8277)

Fixes cvc5/cvc5-projects#471.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 562337fba29b7c1015efa4514fbcba7b97a4b76a..c65db3dd113063a78a85170ccdd6fe60c54868ee 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1409,7 +1409,7 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK_SORTS(params);
+  CVC5_API_CHECK_DOMAIN_SORTS(params);
   CVC5_API_CHECK(isParametricDatatype() || isSortConstructor())
       << "Expected parametric datatype or sort constructor sort.";
   CVC5_API_CHECK(isSortConstructor()

diff --git a/src/api/cpp/cvc5_checks.h b/src/api/cpp/cvc5_checks.h
index 5bd427e7e07eda20cfe9b40ecfcf269e51531247..097a5538ff5ea14a9731aca1a9f1ce44a2c54f48 100644 (file)
--- a/src/api/cpp/cvc5_checks.h
+++ b/src/api/cpp/cvc5_checks.h
@@ -209,6 +209,29 @@ namespace api {
     }                                                                       \
   } while (0)
 
+/**
+ * Sort check for member functions of classes other than class Solver.
+ * Check if each sort in the given container of sorts is not null, is
+ * associated with the solver object this object is associated with, and is a
+ * first-class sort.
+ */
+#define CVC5_API_CHECK_DOMAIN_SORTS(sorts)                                  \
+  do                                                                        \
+  {                                                                         \
+    size_t i = 0;                                                           \
+    for (const auto& s : sorts)                                             \
+    {                                                                       \
+      CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("sort", s, sorts, i);            \
+      CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(                                 \
+          this->d_solver == s.d_solver, "sort", sorts, i)                   \
+          << "a sort associated with the solver this object is associated " \
+             "with";                                                        \
+      CVC5_API_ARG_CHECK_EXPECTED(s.isFirstClass(), s)                      \
+          << "first-class sort as domain sort";                             \
+      i += 1;                                                               \
+    }                                                                       \
+  } while (0)
+
 /* -------------------------------------------------------------------------- */
 /* Term checks.                                                               */
 /* -------------------------------------------------------------------------- */