From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 11 Mar 2022 20:49:36 +0000 (-0600)
Subject: Guard parametric datatypes instantiated by non-first-class sorts (#8277)
X-Git-Tag: cvc5-1.0.0~277
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6a11c95d0e4b8536794329b6bc0d760a965177f0;p=cvc5.git

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 562337fba..c65db3dd1 100644
--- 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 5bd427e7e..097a5538f 100644
--- 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.                                                               */
 /* -------------------------------------------------------------------------- */