From: Aina Niemetz Date: Fri, 11 Mar 2022 23:08:31 +0000 (-0800) Subject: api: Make checks header private. (#8283) X-Git-Tag: cvc5-1.0.0~273 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4a1fea076666a8e8c98085da48a849f3f6c0f64f;p=cvc5.git api: Make checks header private. (#8283) --- diff --git a/src/api/cpp/cvc5_checks.h b/src/api/cpp/cvc5_checks.h index 097a5538f..db628e1b6 100644 --- a/src/api/cpp/cvc5_checks.h +++ b/src/api/cpp/cvc5_checks.h @@ -15,7 +15,7 @@ * These macros implement guards for the cvc5 C++ API functions. */ -#include "cvc5_public.h" +#include "cvc5_private.h" #ifndef CVC5__API__CHECKS_H #define CVC5__API__CHECKS_H @@ -415,7 +415,7 @@ namespace api { this == s.d_solver, "sort", sorts, i) \ << "a sorts associated with this solver"; \ CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ - !s.isFunctionLike(), "sort", sorts, i) \ + !s.getTypeNode().isFunctionLike(), "sort", sorts, i) \ << "non-function-like sort"; \ i += 1; \ } \ @@ -426,14 +426,14 @@ namespace api { * Check if domain sort is not null, associated with this solver, and a * first-class sort. */ -#define CVC5_API_SOLVER_CHECK_DOMAIN_SORT(sort) \ - do \ - { \ - CVC5_API_ARG_CHECK_NOT_NULL(sort); \ - CVC5_API_CHECK(this == sort.d_solver) \ - << "Given sort is not associated with this solver"; \ - CVC5_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) \ - << "first-class sort as domain sort"; \ +#define CVC5_API_SOLVER_CHECK_DOMAIN_SORT(sort) \ + do \ + { \ + CVC5_API_ARG_CHECK_NOT_NULL(sort); \ + CVC5_API_CHECK(this == sort.d_solver) \ + << "Given sort is not associated with this solver"; \ + CVC5_API_ARG_CHECK_EXPECTED(sort.getTypeNode().isFirstClass(), sort) \ + << "first-class sort as domain sort"; \ } while (0) /** @@ -452,7 +452,7 @@ namespace api { this == s.d_solver, "domain sort", sorts, i) \ << "a sort associated with this solver object"; \ CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ - s.isFirstClass(), "domain sort", sorts, i) \ + s.getTypeNode().isFirstClass(), "domain sort", sorts, i) \ << "first-class sort as domain sort"; \ i += 1; \ } \ @@ -601,7 +601,10 @@ namespace api { bound_vars, \ i); \ CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ - domain_sorts[i].isFirstClass(), "domain sort", domain_sorts, i) \ + domain_sorts[i].getTypeNode().isFirstClass(), \ + "domain sort", \ + domain_sorts, \ + i) \ << "first-class sort of parameter of defined function"; \ i += 1; \ } \ @@ -628,14 +631,15 @@ namespace api { * Check if given datatype declaration is not null and associated with this * solver. */ -#define CVC5_API_SOLVER_CHECK_DTDECL(decl) \ - do \ - { \ - CVC5_API_ARG_CHECK_NOT_NULL(decl); \ - CVC5_API_CHECK(this == decl.d_solver) \ - << "Given datatype declaration is not associated with this solver"; \ - CVC5_API_ARG_CHECK_EXPECTED(dtypedecl.getNumConstructors() > 0, dtypedecl) \ - << "a datatype declaration with at least one constructor"; \ +#define CVC5_API_SOLVER_CHECK_DTDECL(decl) \ + do \ + { \ + CVC5_API_ARG_CHECK_NOT_NULL(decl); \ + CVC5_API_CHECK(this == decl.d_solver) \ + << "Given datatype declaration is not associated with this solver"; \ + CVC5_API_ARG_CHECK_EXPECTED( \ + dtypedecl.getDatatype().getNumConstructors() > 0, dtypedecl) \ + << "a datatype declaration with at least one constructor"; \ } while (0) /** @@ -643,22 +647,25 @@ namespace api { * Check if each datatype declaration in the given container of declarations is * not null and associated with this solver. */ -#define CVC5_API_SOLVER_CHECK_DTDECLS(decls) \ - do \ - { \ - size_t i = 0; \ - for (const auto& d : decls) \ - { \ - CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL( \ - "datatype declaration", d, decls, i); \ - CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ - this == d.d_solver, "datatype declaration", decls, i) \ - << "a datatype declaration associated with this solver"; \ - CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ - d.getNumConstructors() > 0, "datatype declaration", decls, i) \ - << "a datatype declaration with at least one constructor"; \ - i += 1; \ - } \ +#define CVC5_API_SOLVER_CHECK_DTDECLS(decls) \ + do \ + { \ + size_t i = 0; \ + for (const auto& d : decls) \ + { \ + CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL( \ + "datatype declaration", d, decls, i); \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + this == d.d_solver, "datatype declaration", decls, i) \ + << "a datatype declaration associated with this solver"; \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + d.getDatatype().getNumConstructors() > 0, \ + "datatype declaration", \ + decls, \ + i) \ + << "a datatype declaration with at least one constructor"; \ + i += 1; \ + } \ } while (0) /**