diff options
Diffstat (limited to 'src/api/cpp/cvc5_checks.h')
-rw-r--r-- | src/api/cpp/cvc5_checks.h | 268 |
1 files changed, 134 insertions, 134 deletions
diff --git a/src/api/cpp/cvc5_checks.h b/src/api/cpp/cvc5_checks.h index 02ab7d39f..f210dddf6 100644 --- a/src/api/cpp/cvc5_checks.h +++ b/src/api/cpp/cvc5_checks.h @@ -30,16 +30,16 @@ namespace api { * The base check macro. * Throws a CVC4ApiException if 'cond' is false. */ -#define CVC4_API_CHECK(cond) \ - CVC4_PREDICT_TRUE(cond) \ +#define CVC5_API_CHECK(cond) \ + CVC5_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) \ +#define CVC5_API_RECOVERABLE_CHECK(cond) \ + CVC5_PREDICT_TRUE(cond) \ ? (void)0 : OstreamVoider() & CVC4ApiRecoverableExceptionStream().ostream() /* -------------------------------------------------------------------------- */ @@ -47,25 +47,25 @@ namespace api { /* -------------------------------------------------------------------------- */ /** Check it 'this' is not a null object. */ -#define CVC4_API_CHECK_NOT_NULL \ - CVC4_API_CHECK(!isNullHelper()) \ +#define CVC5_API_CHECK_NOT_NULL \ + CVC5_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 << "'"; +#define CVC5_API_ARG_CHECK_NOT_NULL(arg) \ + CVC5_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) \ +#define CVC5_API_ARG_CHECK_NOT_NULLPTR(arg) \ + CVC5_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 '" \ +#define CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL(what, arg, args, idx) \ + CVC5_API_CHECK(!arg.isNull()) << "Invalid null " << (what) << " in '" \ << #args << "' at index " << (idx); /* -------------------------------------------------------------------------- */ @@ -73,8 +73,8 @@ namespace api { /* -------------------------------------------------------------------------- */ /** Check if given kind is a valid kind. */ -#define CVC4_API_KIND_CHECK(kind) \ - CVC4_API_CHECK(isDefinedKind(kind)) \ +#define CVC5_API_KIND_CHECK(kind) \ + CVC5_API_CHECK(isDefinedKind(kind)) \ << "Invalid kind '" << kindToString(kind) << "'"; /** @@ -82,8 +82,8 @@ namespace api { * 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) \ +#define CVC5_API_KIND_CHECK_EXPECTED(cond, kind) \ + CVC5_PREDICT_TRUE(cond) \ ? (void)0 \ : OstreamVoider() \ & CVC4ApiExceptionStream().ostream() \ @@ -98,8 +98,8 @@ namespace api { * 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) \ +#define CVC5_API_ARG_CHECK_EXPECTED(cond, arg) \ + CVC5_PREDICT_TRUE(cond) \ ? (void)0 \ : OstreamVoider() \ & CVC4ApiExceptionStream().ostream() \ @@ -111,8 +111,8 @@ namespace api { * 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) \ +#define CVC5_API_RECOVERABLE_ARG_CHECK_EXPECTED(cond, arg) \ + CVC5_PREDICT_TRUE(cond) \ ? (void)0 \ : OstreamVoider() \ & CVC4ApiRecoverableExceptionStream().ostream() \ @@ -121,13 +121,13 @@ namespace api { /** * Check condition 'cond' for given argument 'arg'. - * Provides a more specific error message than CVC4_API_ARG_CHECK_EXPECTED, + * Provides a more specific error message than CVC5_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) \ +#define CVC5_API_ARG_SIZE_CHECK_EXPECTED(cond, arg) \ + CVC5_PREDICT_TRUE(cond) \ ? (void)0 \ : OstreamVoider() \ & CVC4ApiExceptionStream().ostream() \ @@ -139,11 +139,11 @@ namespace api { * 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( + * CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( * <condition>, "what", <container>, <idx>) << "message"; */ -#define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, args, idx) \ - CVC4_PREDICT_TRUE(cond) \ +#define CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, args, idx) \ + CVC5_PREDICT_TRUE(cond) \ ? (void)0 \ : OstreamVoider() \ & CVC4ApiExceptionStream().ostream() \ @@ -159,8 +159,8 @@ namespace api { * Check if given solver matches the solver object this object is associated * with. */ -#define CVC4_API_ARG_CHECK_SOLVER(what, arg) \ - CVC4_API_CHECK(this->d_solver == arg.d_solver) \ +#define CVC5_API_ARG_CHECK_SOLVER(what, arg) \ + CVC5_API_CHECK(this->d_solver == arg.d_solver) \ << "Given " << (what) << " is not associated with the solver this " \ << "object is associated with"; @@ -173,11 +173,11 @@ namespace api { * Check if given sort is not null and associated with the solver object this * object is associated with. */ -#define CVC4_API_CHECK_SORT(sort) \ +#define CVC5_API_CHECK_SORT(sort) \ do \ { \ - CVC4_API_ARG_CHECK_NOT_NULL(sort); \ - CVC4_API_ARG_CHECK_SOLVER("sort", sort); \ + CVC5_API_ARG_CHECK_NOT_NULL(sort); \ + CVC5_API_ARG_CHECK_SOLVER("sort", sort); \ } while (0) /** @@ -185,14 +185,14 @@ namespace api { * Check if each sort in the given container of sorts is not null and * associated with the solver object this object is associated with. */ -#define CVC4_API_CHECK_SORTS(sorts) \ +#define CVC5_API_CHECK_SORTS(sorts) \ do \ { \ size_t i = 0; \ for (const auto& s : sorts) \ { \ - CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("sort", s, sorts, i); \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + 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"; \ @@ -209,11 +209,11 @@ namespace api { * Check if given term is not null and associated with the solver object this * object is associated with. */ -#define CVC4_API_CHECK_TERM(term) \ +#define CVC5_API_CHECK_TERM(term) \ do \ { \ - CVC4_API_ARG_CHECK_NOT_NULL(term); \ - CVC4_API_ARG_CHECK_SOLVER("term", term); \ + CVC5_API_ARG_CHECK_NOT_NULL(term); \ + CVC5_API_ARG_CHECK_SOLVER("term", term); \ } while (0) /** @@ -221,14 +221,14 @@ namespace api { * Check if each term in the given container of terms is not null and * associated with the solver object this object is associated with. */ -#define CVC4_API_CHECK_TERMS(terms) \ +#define CVC5_API_CHECK_TERMS(terms) \ do \ { \ size_t i = 0; \ for (const auto& s : terms) \ { \ - CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", s, terms, i); \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", s, terms, i); \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ this->d_solver == s.d_solver, "term", terms, i) \ << "a term associated with the solver this object is associated " \ "with"; \ @@ -242,19 +242,19 @@ namespace api { * not null and associated with the solver object this object is associated * with. */ -#define CVC4_API_CHECK_TERMS_MAP(map) \ +#define CVC5_API_CHECK_TERMS_MAP(map) \ do \ { \ size_t i = 0; \ for (const auto& p : map) \ { \ - CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", p.first, map, i); \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", p.first, map, i); \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ this->d_solver == p.first.d_solver, "term", map, i) \ << "a term associated with the solver this object is associated " \ "with"; \ - CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("sort", p.second, map, i); \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("sort", p.second, map, i); \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ this->d_solver == p.second.d_solver, "sort", map, i) \ << "a sort associated with the solver this object is associated " \ "with"; \ @@ -267,18 +267,18 @@ namespace api { * Check if each term in the given container is not null, associated with the * solver object this object is associated with, and of the given sort. */ -#define CVC4_API_CHECK_TERMS_WITH_SORT(terms, sort) \ +#define CVC5_API_CHECK_TERMS_WITH_SORT(terms, sort) \ do \ { \ size_t i = 0; \ for (const auto& t : terms) \ { \ - CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", t, terms, i); \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", t, terms, i); \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ this->d_solver == t.d_solver, "term", terms, i) \ << "a term associated with the solver this object is associated " \ "with"; \ - CVC4_API_CHECK(t.getSort() == sort) \ + CVC5_API_CHECK(t.getSort() == sort) \ << "Expected term with sort " << sort << " at index " << i << " in " \ << #terms; \ i += 1; \ @@ -291,24 +291,24 @@ namespace api { * the solver object this object is associated with, and their sorts are * pairwise comparable to. */ -#define CVC4_API_TERM_CHECK_TERMS_WITH_TERMS_COMPARABLE_TO(terms1, terms2) \ +#define CVC5_API_TERM_CHECK_TERMS_WITH_TERMS_COMPARABLE_TO(terms1, terms2) \ do \ { \ size_t i = 0; \ for (const auto& t1 : terms1) \ { \ const auto& t2 = terms2[i]; \ - CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", t1, terms1, i); \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", t1, terms1, i); \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ this->d_solver == t1.d_solver, "term", terms1, i) \ << "a term associated with the solver this object is associated " \ "with"; \ - CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", t2, terms2, i); \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", t2, terms2, i); \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ this->d_solver == t2.d_solver, "term", terms2, i) \ << "a term associated with the solver this object is associated " \ "with"; \ - CVC4_API_CHECK(t1.getSort().isComparableTo(t2.getSort())) \ + CVC5_API_CHECK(t1.getSort().isComparableTo(t2.getSort())) \ << "Expecting terms of comparable sort at index " << i; \ i += 1; \ } \ @@ -323,11 +323,11 @@ namespace api { * Check if given datatype declaration is not null and associated with the * solver object this DatatypeDecl object is associated with. */ -#define CVC4_API_CHECK_DTDECL(decl) \ +#define CVC5_API_CHECK_DTDECL(decl) \ do \ { \ - CVC4_API_ARG_CHECK_NOT_NULL(decl); \ - CVC4_API_ARG_CHECK_SOLVER("datatype declaration", decl); \ + CVC5_API_ARG_CHECK_NOT_NULL(decl); \ + CVC5_API_ARG_CHECK_SOLVER("datatype declaration", decl); \ } while (0) /* -------------------------------------------------------------------------- */ @@ -340,11 +340,11 @@ namespace api { * Sort checks for member functions of class Solver. * Check if given sort is not null and associated with this solver. */ -#define CVC4_API_SOLVER_CHECK_SORT(sort) \ +#define CVC5_API_SOLVER_CHECK_SORT(sort) \ do \ { \ - CVC4_API_ARG_CHECK_NOT_NULL(sort); \ - CVC4_API_CHECK(this == sort.d_solver) \ + CVC5_API_ARG_CHECK_NOT_NULL(sort); \ + CVC5_API_CHECK(this == sort.d_solver) \ << "Given sort is not associated with this solver"; \ } while (0) @@ -353,14 +353,14 @@ namespace api { * Check if each sort in the given container of sorts is not null and * associated with this solver. */ -#define CVC4_API_SOLVER_CHECK_SORTS(sorts) \ +#define CVC5_API_SOLVER_CHECK_SORTS(sorts) \ do \ { \ size_t i = 0; \ for (const auto& s : sorts) \ { \ - CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("sorts", s, sorts, i); \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("sorts", s, sorts, i); \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ this == s.d_solver, "sort", sorts, i) \ << "a sort associated with this solver"; \ i += 1; \ @@ -372,17 +372,17 @@ namespace api { * Check if each sort in the given container of sorts is not null, associated * with this solver, and not function-like. */ -#define CVC4_API_SOLVER_CHECK_SORTS_NOT_FUNCTION_LIKE(sorts) \ +#define CVC5_API_SOLVER_CHECK_SORTS_NOT_FUNCTION_LIKE(sorts) \ do \ { \ size_t i = 0; \ for (const auto& s : sorts) \ { \ - CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("sorts", s, sorts, i); \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("sorts", s, sorts, i); \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ this == s.d_solver, "sort", sorts, i) \ << "a sorts associated with this solver"; \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ !s.isFunctionLike(), "sort", sorts, i) \ << "non-function-like sort"; \ i += 1; \ @@ -394,14 +394,14 @@ namespace api { * Check if domain sort is not null, associated with this solver, and a * first-class sort. */ -#define CVC4_API_SOLVER_CHECK_DOMAIN_SORT(sort) \ - do \ - { \ - CVC4_API_ARG_CHECK_NOT_NULL(sort); \ - CVC4_API_CHECK(this == sort.d_solver) \ - << "Given sort is not associated with this solver"; \ - CVC4_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.isFirstClass(), sort) \ + << "first-class sort as domain sort"; \ } while (0) /** @@ -409,21 +409,21 @@ namespace api { * Check if each domain sort in the given container of sorts is not null, * associated with this solver, and a first-class sort. */ -#define CVC4_API_SOLVER_CHECK_DOMAIN_SORTS(sorts) \ - do \ - { \ - size_t i = 0; \ - for (const auto& s : sorts) \ - { \ - CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("domain sort", s, sorts, i); \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ - this == s.d_solver, "domain sort", sorts, i) \ - << "a sort associated with this solver object"; \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ - s.isFirstClass(), "domain sort", sorts, i) \ - << "first-class sort as domain sort"; \ - i += 1; \ - } \ +#define CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts) \ + do \ + { \ + size_t i = 0; \ + for (const auto& s : sorts) \ + { \ + CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("domain sort", s, sorts, i); \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + 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) \ + << "first-class sort as domain sort"; \ + i += 1; \ + } \ } while (0) /** @@ -431,15 +431,15 @@ namespace api { * Check if codomain sort is not null, associated with this solver, and a * first-class, non-function sort. */ -#define CVC4_API_SOLVER_CHECK_CODOMAIN_SORT(sort) \ +#define CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort) \ do \ { \ - CVC4_API_ARG_CHECK_NOT_NULL(sort); \ - CVC4_API_CHECK(this == sort.d_solver) \ + CVC5_API_ARG_CHECK_NOT_NULL(sort); \ + CVC5_API_CHECK(this == sort.d_solver) \ << "Given sort is not associated with this solver"; \ - CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) \ + CVC5_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) \ << "first-class sort as codomain sort"; \ - CVC4_API_ARG_CHECK_EXPECTED(!sort.isFunction(), sort) \ + CVC5_API_ARG_CHECK_EXPECTED(!sort.isFunction(), sort) \ << "function sort as codomain sort"; \ } while (0) @@ -449,11 +449,11 @@ namespace api { * Term checks for member functions of class Solver. * Check if given term is not null and associated with this solver. */ -#define CVC4_API_SOLVER_CHECK_TERM(term) \ +#define CVC5_API_SOLVER_CHECK_TERM(term) \ do \ { \ - CVC4_API_ARG_CHECK_NOT_NULL(term); \ - CVC4_API_CHECK(this == term.d_solver) \ + CVC5_API_ARG_CHECK_NOT_NULL(term); \ + CVC5_API_CHECK(this == term.d_solver) \ << "Given term is not associated with this solver"; \ } while (0) @@ -462,14 +462,14 @@ namespace api { * Check if each term in the given container of terms is not null and * associated with this solver. */ -#define CVC4_API_SOLVER_CHECK_TERMS(terms) \ +#define CVC5_API_SOLVER_CHECK_TERMS(terms) \ do \ { \ size_t i = 0; \ for (const auto& t : terms) \ { \ - CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("terms", t, terms, i); \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("terms", t, terms, i); \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ this == t.d_solver, "term", terms, i) \ << "a term associated with this solver"; \ i += 1; \ @@ -481,11 +481,11 @@ namespace api { * Check if given term is not null, associated with this solver, and of given * sort. */ -#define CVC4_API_SOLVER_CHECK_TERM_WITH_SORT(term, sort) \ +#define CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(term, sort) \ do \ { \ - CVC4_API_SOLVER_CHECK_TERM(term); \ - CVC4_API_CHECK(term.getSort() == sort) \ + CVC5_API_SOLVER_CHECK_TERM(term); \ + CVC5_API_CHECK(term.getSort() == sort) \ << "Expected term with sort " << sort; \ } while (0) @@ -494,17 +494,17 @@ namespace api { * Check if each term in the given container is not null, associated with this * solver, and of the given sort. */ -#define CVC4_API_SOLVER_CHECK_TERMS_WITH_SORT(terms, sort) \ +#define CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(terms, sort) \ do \ { \ size_t i = 0; \ for (const auto& t : terms) \ { \ - CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", t, terms, i); \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", t, terms, i); \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ this == t.d_solver, "term", terms, i) \ << "a term associated with this solver"; \ - CVC4_API_CHECK(t.getSort() == sort) \ + CVC5_API_CHECK(t.getSort() == sort) \ << "Expected term with sort " << sort << " at index " << i << " in " \ << #terms; \ i += 1; \ @@ -516,18 +516,18 @@ namespace api { * Check if each term in the given container is not null, associated with this * solver, and a bound variable. */ -#define CVC4_API_SOLVER_CHECK_BOUND_VARS(bound_vars) \ +#define CVC5_API_SOLVER_CHECK_BOUND_VARS(bound_vars) \ do \ { \ size_t i = 0; \ for (const auto& bv : bound_vars) \ { \ - CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL( \ + CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL( \ "bound variable", bv, bound_vars, i); \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ this == bv.d_solver, "bound variable", bound_vars, i) \ << "a term associated with this solver object"; \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ bv.d_node->getKind() == cvc5::Kind::BOUND_VARIABLE, \ "bound variable", \ bound_vars, \ @@ -544,33 +544,33 @@ namespace api { * solver, a bound variable, matches theh corresponding sort in 'domain_sorts', * and is a first-class term. */ -#define CVC4_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN( \ +#define CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN( \ fun, bound_vars, domain_sorts) \ do \ { \ size_t size = bound_vars.size(); \ - CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bound_vars) \ + CVC5_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bound_vars) \ << "'" << domain_sorts.size() << "'"; \ size_t i = 0; \ for (const auto& bv : bound_vars) \ { \ - CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL( \ + CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL( \ "bound variable", bv, bound_vars, i); \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ this == bv.d_solver, "bound variable", bound_vars, i) \ << "a term associated with this solver object"; \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ bv.d_node->getKind() == cvc5::Kind::BOUND_VARIABLE, \ "bound variable", \ bound_vars, \ i) \ << "a bound variable"; \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ domain_sorts[i] == bound_vars[i].getSort(), \ "sort of parameter", \ bound_vars, \ i); \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ domain_sorts[i].isFirstClass(), "domain sort", domain_sorts, i) \ << "first-class sort of parameter of defined function"; \ i += 1; \ @@ -583,11 +583,11 @@ namespace api { * Op checks for member functions of class Solver. * Check if given operator is not null and associated with this solver. */ -#define CVC4_API_SOLVER_CHECK_OP(op) \ +#define CVC5_API_SOLVER_CHECK_OP(op) \ do \ { \ - CVC4_API_ARG_CHECK_NOT_NULL(op); \ - CVC4_API_CHECK(this == op.d_solver) \ + CVC5_API_ARG_CHECK_NOT_NULL(op); \ + CVC5_API_CHECK(this == op.d_solver) \ << "Given operator is not associated with this solver"; \ } while (0) @@ -598,13 +598,13 @@ namespace api { * Check if given datatype declaration is not null and associated with this * solver. */ -#define CVC4_API_SOLVER_CHECK_DTDECL(decl) \ +#define CVC5_API_SOLVER_CHECK_DTDECL(decl) \ do \ { \ - CVC4_API_ARG_CHECK_NOT_NULL(decl); \ - CVC4_API_CHECK(this == decl.d_solver) \ + CVC5_API_ARG_CHECK_NOT_NULL(decl); \ + CVC5_API_CHECK(this == decl.d_solver) \ << "Given datatype declaration is not associated with this solver"; \ - CVC4_API_ARG_CHECK_EXPECTED(dtypedecl.getNumConstructors() > 0, dtypedecl) \ + CVC5_API_ARG_CHECK_EXPECTED(dtypedecl.getNumConstructors() > 0, dtypedecl) \ << "a datatype declaration with at least one constructor"; \ } while (0) @@ -613,18 +613,18 @@ namespace api { * Check if each datatype declaration in the given container of declarations is * not null and associated with this solver. */ -#define CVC4_API_SOLVER_CHECK_DTDECLS(decls) \ +#define CVC5_API_SOLVER_CHECK_DTDECLS(decls) \ do \ { \ size_t i = 0; \ for (const auto& d : decls) \ { \ - CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL( \ + CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL( \ "datatype declaration", d, decls, i); \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ this == d.d_solver, "datatype declaration", decls, i) \ << "a datatype declaration associated with this solver"; \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ d.getNumConstructors() > 0, "datatype declaration", decls, i) \ << "a datatype declaration with at least one constructor"; \ i += 1; \ @@ -636,15 +636,15 @@ namespace api { * Check if each datatype constructor declaration in the given container of * declarations is not null and associated with this solver. */ -#define CVC4_API_SOLVER_CHECK_DTCTORDECLS(decls) \ +#define CVC5_API_SOLVER_CHECK_DTCTORDECLS(decls) \ do \ { \ size_t i = 0; \ for (const auto& d : decls) \ { \ - CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL( \ + CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL( \ "datatype constructor declaration", d, decls, i); \ - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \ this == d.d_solver, "datatype constructor declaration", decls, i) \ << "a datatype constructor declaration associated with this solver " \ "object"; \ |