From 6a11c95d0e4b8536794329b6bc0d760a965177f0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 11 Mar 2022 14:49:36 -0600 Subject: [PATCH] Guard parametric datatypes instantiated by non-first-class sorts (#8277) Fixes cvc5/cvc5-projects#471. --- src/api/cpp/cvc5.cpp | 2 +- src/api/cpp/cvc5_checks.h | 23 +++++++++++++++++++++++ 2 files changed, 24 insertions(+), 1 deletion(-) 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& 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. */ /* -------------------------------------------------------------------------- */ -- 2.30.2