From: Aina Niemetz Date: Fri, 12 Mar 2021 22:45:14 +0000 (-0800) Subject: New C++ Api: Move checks to separate file. (#6138) X-Git-Tag: cvc5-1.0.0~2084 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5074aeb52163135386c71e802ebc9f97fb5c9013;p=cvc5.git New C++ Api: Move checks to separate file. (#6138) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index b96d925aa..005911ca8 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -12,6 +12,7 @@ # Collect libcvc4 source files libcvc4_add_sources( + api/checks.h api/cvc4cpp.cpp api/cvc4cpp.h api/cvc4cppkind.h diff --git a/src/api/checks.h b/src/api/checks.h new file mode 100644 index 000000000..bc99825db --- /dev/null +++ b/src/api/checks.h @@ -0,0 +1,174 @@ +/********************* */ +/*! \file cvc4cpp.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 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.\endverbatim + ** + ** \brief Check macros for the CVC5 C++ API. + ** + ** These macros implement guards for the CVC5 C++ API functions. + **/ + +#include "cvc4_public.h" + +#ifndef CVC5__API__CHECKS_H +#define CVC5__API__CHECKS_H + +namespace cvc4 { +namespace api { + +/* -------------------------------------------------------------------------- */ +/* Basic check macros. */ +/* -------------------------------------------------------------------------- */ + +/** + * The base check macro. + * Throws a CVC4ApiException if 'cond' is false. + */ +#define CVC4_API_CHECK(cond) \ + CVC4_PREDICT_TRUE(cond) \ + ? (void)0 : OstreamVoider() & CVC4ApiExceptionStream().ostream() + +/** + * The base check macro for throwing recoverable exceptions. + * Throws a CVC4RecoverableApiException if 'cond' is false. + */ +#define CVC4_API_RECOVERABLE_CHECK(cond) \ + CVC4_PREDICT_TRUE(cond) \ + ? (void)0 : OstreamVoider() & CVC4ApiRecoverableExceptionStream().ostream() + +/* -------------------------------------------------------------------------- */ +/* Not null checks. */ +/* -------------------------------------------------------------------------- */ + +/** Check it 'this' is not a null object. */ +#define CVC4_API_CHECK_NOT_NULL \ + CVC4_API_CHECK(!isNullHelper()) \ + << "Invalid call to '" << __PRETTY_FUNCTION__ \ + << "', expected non-null object"; + +/** Check if given argument is not a null object. */ +#define CVC4_API_ARG_CHECK_NOT_NULL(arg) \ + CVC4_API_CHECK(!arg.isNull()) << "Invalid null argument for '" << #arg << "'"; + +/** Check if given argument is not a null pointer. */ +#define CVC4_API_ARG_CHECK_NOT_NULLPTR(arg) \ + CVC4_API_CHECK(arg != nullptr) \ + << "Invalid null argument for '" << #arg << "'"; +/** + * Check if given argument at given index in container 'args' is not a null + * object. + */ +#define CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL(what, arg, args, idx) \ + CVC4_API_CHECK(!arg.isNull()) << "Invalid null " << (what) << " in '" \ + << #args << "' at index " << (idx); + +/* -------------------------------------------------------------------------- */ +/* Kind checks. */ +/* -------------------------------------------------------------------------- */ + +/** Check if given kind is a valid kind. */ +#define CVC4_API_KIND_CHECK(kind) \ + CVC4_API_CHECK(isDefinedKind(kind)) \ + << "Invalid kind '" << kindToString(kind) << "'"; + +/** + * Check if given kind is a valid kind. + * Creates a stream to provide a message that identifies what kind was expected + * if given kind is invalid. + */ +#define CVC4_API_KIND_CHECK_EXPECTED(cond, kind) \ + CVC4_PREDICT_TRUE(cond) \ + ? (void)0 \ + : OstreamVoider() \ + & CVC4ApiExceptionStream().ostream() \ + << "Invalid kind '" << kindToString(kind) << "', expected " + +/* -------------------------------------------------------------------------- */ +/* Argument checks. */ +/* -------------------------------------------------------------------------- */ + +/** + * Check condition 'cond' for given argument 'arg'. + * Creates a stream to provide a message that identifies what was expected to + * hold if condition is false and throws a non-recoverable exception. + */ +#define CVC4_API_ARG_CHECK_EXPECTED(cond, arg) \ + CVC4_PREDICT_TRUE(cond) \ + ? (void)0 \ + : OstreamVoider() \ + & CVC4ApiExceptionStream().ostream() \ + << "Invalid argument '" << arg << "' for '" << #arg \ + << "', expected " + +/** + * Check condition 'cond' for given argument 'arg'. + * Creates a stream to provide a message that identifies what was expected to + * hold if condition is false and throws a recoverable exception. + */ +#define CVC4_API_RECOVERABLE_ARG_CHECK_EXPECTED(cond, arg) \ + CVC4_PREDICT_TRUE(cond) \ + ? (void)0 \ + : OstreamVoider() \ + & CVC4ApiRecoverableExceptionStream().ostream() \ + << "Invalid argument '" << arg << "' for '" << #arg \ + << "', expected " + +/** + * Check condition 'cond' for given argument 'arg'. + * Provides a more specific error message than CVC4_API_ARG_CHECK_EXPECTED, + * it identifies that this check is a size check. + * Creates a stream to provide a message that identifies what was expected to + * hold if condition is false and throws a recoverable exception. + */ +#define CVC4_API_ARG_SIZE_CHECK_EXPECTED(cond, arg) \ + CVC4_PREDICT_TRUE(cond) \ + ? (void)0 \ + : OstreamVoider() \ + & CVC4ApiExceptionStream().ostream() \ + << "Invalid size of argument '" << #arg << "', expected " + +/** + * Check condition 'cond' for given argument 'arg' at given index. + * Argument 'what' identifies what is being checked (e.g., "term"). + * Creates a stream to provide a message that identifies what was expected to + * hold if condition is false. + * Usage: + * CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(, "what", , ) + * << "message"; + */ +#define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, arg, idx) \ + CVC4_PREDICT_TRUE(cond) \ + ? (void)0 \ + : OstreamVoider() \ + & CVC4ApiExceptionStream().ostream() \ + << "Invalid " << what << " '" << arg << "' at index " << idx \ + << ", expected " + +/* -------------------------------------------------------------------------- */ +/* Solver checks. */ +/* -------------------------------------------------------------------------- */ + +/** Sort checks for member functions of class Solver. */ +#define CVC4_API_SOLVER_CHECK_SORT(sort) \ + CVC4_API_CHECK(this == sort.d_solver) \ + << "Given sort is not associated with this solver"; + +/** Term checks for member functions of class Solver. */ +#define CVC4_API_SOLVER_CHECK_TERM(term) \ + CVC4_API_CHECK(this == term.d_solver) \ + << "Given term is not associated with this solver"; + +/** Op checks for member functions of class Solver. */ +#define CVC4_API_SOLVER_CHECK_OP(op) \ + CVC4_API_CHECK(this == op.d_solver) \ + << "Given operator is not associated with this solver"; + +} // namespace api +} // namespace cvc4 +#endif diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 4450082cb..06fe1e788 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -36,6 +36,7 @@ #include #include +#include "api/checks.h" #include "base/check.h" #include "base/configuration.h" #include "expr/dtype.h" @@ -823,68 +824,6 @@ class CVC4ApiRecoverableExceptionStream std::stringstream d_stream; }; -#define CVC4_API_CHECK(cond) \ - CVC4_PREDICT_TRUE(cond) \ - ? (void)0 : OstreamVoider() & CVC4ApiExceptionStream().ostream() - -#define CVC4_API_RECOVERABLE_CHECK(cond) \ - CVC4_PREDICT_TRUE(cond) \ - ? (void)0 : OstreamVoider() & CVC4ApiRecoverableExceptionStream().ostream() - -#define CVC4_API_CHECK_NOT_NULL \ - CVC4_API_CHECK(!isNullHelper()) \ - << "Invalid call to '" << __PRETTY_FUNCTION__ \ - << "', expected non-null object"; - -#define CVC4_API_ARG_CHECK_NOT_NULL(arg) \ - CVC4_API_CHECK(!arg.isNull()) << "Invalid null argument for '" << #arg << "'"; - -#define CVC4_API_ARG_CHECK_NOT_NULLPTR(arg) \ - CVC4_API_CHECK(arg != nullptr) \ - << "Invalid null argument for '" << #arg << "'"; - -#define CVC4_API_KIND_CHECK(kind) \ - CVC4_API_CHECK(isDefinedKind(kind)) \ - << "Invalid kind '" << kindToString(kind) << "'"; - -#define CVC4_API_KIND_CHECK_EXPECTED(cond, kind) \ - CVC4_PREDICT_TRUE(cond) \ - ? (void)0 \ - : OstreamVoider() \ - & CVC4ApiExceptionStream().ostream() \ - << "Invalid kind '" << kindToString(kind) << "', expected " - -#define CVC4_API_ARG_CHECK_EXPECTED(cond, arg) \ - CVC4_PREDICT_TRUE(cond) \ - ? (void)0 \ - : OstreamVoider() \ - & CVC4ApiExceptionStream().ostream() \ - << "Invalid argument '" << arg << "' for '" << #arg \ - << "', expected " - -#define CVC4_API_RECOVERABLE_ARG_CHECK_EXPECTED(cond, arg) \ - CVC4_PREDICT_TRUE(cond) \ - ? (void)0 \ - : OstreamVoider() \ - & CVC4ApiRecoverableExceptionStream().ostream() \ - << "Invalid argument '" << arg << "' for '" << #arg \ - << "', expected " - -#define CVC4_API_ARG_SIZE_CHECK_EXPECTED(cond, arg) \ - CVC4_PREDICT_TRUE(cond) \ - ? (void)0 \ - : OstreamVoider() \ - & CVC4ApiExceptionStream().ostream() \ - << "Invalid size of argument '" << #arg << "', expected " - -#define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, arg, idx) \ - CVC4_PREDICT_TRUE(cond) \ - ? (void)0 \ - : OstreamVoider() \ - & CVC4ApiExceptionStream().ostream() \ - << "Invalid " << what << " '" << arg << "' at index " << idx \ - << ", expected " - #define CVC4_API_TRY_CATCH_BEGIN \ try \ { @@ -901,18 +840,6 @@ class CVC4ApiRecoverableExceptionStream catch (const CVC4::Exception& e) { throw CVC4ApiException(e.getMessage()); } \ catch (const std::invalid_argument& e) { throw CVC4ApiException(e.what()); } -#define CVC4_API_SOLVER_CHECK_SORT(sort) \ - CVC4_API_CHECK(this == sort.d_solver) \ - << "Given sort is not associated with this solver"; - -#define CVC4_API_SOLVER_CHECK_TERM(term) \ - CVC4_API_CHECK(this == term.d_solver) \ - << "Given term is not associated with this solver"; - -#define CVC4_API_SOLVER_CHECK_OP(op) \ - CVC4_API_CHECK(this == op.d_solver) \ - << "Given operator is not associated with this solver"; - } // namespace /* -------------------------------------------------------------------------- */