From: Aina Niemetz Date: Wed, 17 Mar 2021 18:19:35 +0000 (-0700) Subject: New C++ Api: Comprehensive guards for member functions of class Term. (#6150) X-Git-Tag: cvc5-1.0.0~2062 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c21a80e2f9d54596f2b1f993be4dbd271c3651aa;p=cvc5.git New C++ Api: Comprehensive guards for member functions of class Term. (#6150) --- diff --git a/src/api/checks.h b/src/api/checks.h index aa2919d86..85322048c 100644 --- a/src/api/checks.h +++ b/src/api/checks.h @@ -285,6 +285,35 @@ namespace api { } \ } while (0) +/** + * Term check for member functions of classes other than class Solver. + * Check if each term in both the given container is not null, associated with + * 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) \ + 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( \ + 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( \ + 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())) \ + << "Expecting terms of comparable sort at index " << i; \ + i += 1; \ + } \ + } while (0) + /* -------------------------------------------------------------------------- */ /* DatatypeDecl checks. */ /* -------------------------------------------------------------------------- */ diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 9d55a7eb6..84c95c9a1 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2050,72 +2050,66 @@ Term::~Term() } } -bool Term::isNullHelper() const +bool Term::operator==(const Term& t) const { - /* Split out to avoid nested API calls (problematic with API tracing). */ - return d_node->isNull(); + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return *d_node == *t.d_node; + //////// + CVC4_API_TRY_CATCH_END; } -Kind Term::getKindHelper() const +bool Term::operator!=(const Term& t) const { - // Sequence kinds do not exist internally, so we must convert their internal - // (string) versions back to sequence. All operators where this is - // necessary are such that their first child is of sequence type, which - // we check here. - if (d_node->getNumChildren() > 0 && (*d_node)[0].getType().isSequence()) - { - switch (d_node->getKind()) - { - case CVC4::Kind::STRING_CONCAT: return SEQ_CONCAT; - case CVC4::Kind::STRING_LENGTH: return SEQ_LENGTH; - case CVC4::Kind::STRING_SUBSTR: return SEQ_EXTRACT; - case CVC4::Kind::STRING_UPDATE: return SEQ_UPDATE; - case CVC4::Kind::STRING_CHARAT: return SEQ_AT; - case CVC4::Kind::STRING_STRCTN: return SEQ_CONTAINS; - case CVC4::Kind::STRING_STRIDOF: return SEQ_INDEXOF; - case CVC4::Kind::STRING_STRREPL: return SEQ_REPLACE; - case CVC4::Kind::STRING_STRREPLALL: return SEQ_REPLACE_ALL; - case CVC4::Kind::STRING_REV: return SEQ_REV; - case CVC4::Kind::STRING_PREFIX: return SEQ_PREFIX; - case CVC4::Kind::STRING_SUFFIX: return SEQ_SUFFIX; - default: - // fall through to conversion below - break; - } - } - // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to - // INTERNAL_KIND. - if(isCastedReal()) - { - return CONST_RATIONAL; - } - return intToExtKind(d_node->getKind()); + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return *d_node != *t.d_node; + //////// + CVC4_API_TRY_CATCH_END; } -bool Term::isCastedReal() const +bool Term::operator<(const Term& t) const { - if(d_node->getKind() == kind::CAST_TO_REAL) - { - return (*d_node)[0].isConst() && (*d_node)[0].getType().isInteger(); - } - return false; + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return *d_node < *t.d_node; + //////// + CVC4_API_TRY_CATCH_END; } -bool Term::operator==(const Term& t) const { return *d_node == *t.d_node; } - -bool Term::operator!=(const Term& t) const { return *d_node != *t.d_node; } - -bool Term::operator<(const Term& t) const { return *d_node < *t.d_node; } - -bool Term::operator>(const Term& t) const { return *d_node > *t.d_node; } +bool Term::operator>(const Term& t) const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return *d_node > *t.d_node; + //////// + CVC4_API_TRY_CATCH_END; +} -bool Term::operator<=(const Term& t) const { return *d_node <= *t.d_node; } +bool Term::operator<=(const Term& t) const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return *d_node <= *t.d_node; + //////// + CVC4_API_TRY_CATCH_END; +} -bool Term::operator>=(const Term& t) const { return *d_node >= *t.d_node; } +bool Term::operator>=(const Term& t) const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return *d_node >= *t.d_node; + //////// + CVC4_API_TRY_CATCH_END; +} size_t Term::getNumChildren() const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + // special case for apply kinds if (isApplyKind(d_node->getKind())) { @@ -2126,99 +2120,122 @@ size_t Term::getNumChildren() const return 0; } return d_node->getNumChildren(); + //////// + CVC4_API_TRY_CATCH_END; } Term Term::operator[](size_t index) const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; - - // check the index within the number of children CVC4_API_CHECK(index < getNumChildren()) << "index out of bound"; + CVC4_API_CHECK(!isApplyKind(d_node->getKind()) || d_node->hasOperator()) + << "Expected apply kind to have operator when accessing child of Term"; + //////// all checks before this line // special cases for apply kinds if (isApplyKind(d_node->getKind())) { - CVC4_API_CHECK(d_node->hasOperator()) - << "Expected apply kind to have operator when accessing child of Term"; if (index == 0) { // return the operator return Term(d_solver, d_node->getOperator()); } - // otherwise we are looking up child at (index-1) - index--; + else + { + index -= 1; + } } + // otherwise we are looking up child at (index-1) return Term(d_solver, (*d_node)[index]); + //////// + CVC4_API_TRY_CATCH_END; } uint64_t Term::getId() const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line return d_node->getId(); + //////// + CVC4_API_TRY_CATCH_END; } Kind Term::getKind() const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line return getKindHelper(); + //////// + CVC4_API_TRY_CATCH_END; } Sort Term::getSort() const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; NodeManagerScope scope(d_solver->getNodeManager()); + //////// all checks before this line return Sort(d_solver, d_node->getType()); + //////// + CVC4_API_TRY_CATCH_END; } -Term Term::substitute(const Term& e, const Term& replacement) const +Term Term::substitute(const Term& term, const Term& replacement) const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; - CVC4_API_CHECK(!e.isNull()) - << "Expected non-null term to replace in substitute"; - CVC4_API_CHECK(!replacement.isNull()) - << "Expected non-null term as replacement in substitute"; - CVC4_API_CHECK(e.getSort().isComparableTo(replacement.getSort())) + CVC4_API_CHECK_TERM(term); + CVC4_API_CHECK_TERM(replacement); + CVC4_API_CHECK(term.getSort().isComparableTo(replacement.getSort())) << "Expecting terms of comparable sort in substitute"; - return Term(d_solver, - d_node->substitute(TNode(*e.d_node), TNode(*replacement.d_node))); + //////// all checks before this line + return Term( + d_solver, + d_node->substitute(TNode(*term.d_node), TNode(*replacement.d_node))); + //////// + CVC4_API_TRY_CATCH_END; } -Term Term::substitute(const std::vector& es, +Term Term::substitute(const std::vector& terms, const std::vector& replacements) const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; - CVC4_API_CHECK(es.size() == replacements.size()) + CVC4_API_CHECK(terms.size() == replacements.size()) << "Expecting vectors of the same arity in substitute"; - for (unsigned i = 0, nterms = es.size(); i < nterms; i++) - { - CVC4_API_CHECK(!es[i].isNull()) - << "Expected non-null term to replace in substitute"; - CVC4_API_CHECK(!replacements[i].isNull()) - << "Expected non-null term as replacement in substitute"; - CVC4_API_CHECK(es[i].getSort().isComparableTo(replacements[i].getSort())) - << "Expecting terms of comparable sort in substitute"; - } - - std::vector nodes = Term::termVectorToNodes(es); + CVC4_API_TERM_CHECK_TERMS_WITH_TERMS_COMPARABLE_TO(terms, replacements); + //////// all checks before this line + std::vector nodes = Term::termVectorToNodes(terms); std::vector nodeReplacements = Term::termVectorToNodes(replacements); return Term(d_solver, d_node->substitute(nodes.begin(), nodes.end(), nodeReplacements.begin(), nodeReplacements.end())); + //////// + CVC4_API_TRY_CATCH_END; } bool Term::hasOp() const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line return d_node->hasOperator(); + //////// + CVC4_API_TRY_CATCH_END; } Op Term::getOp() const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(d_node->hasOperator()) << "Expecting Term to have an Op when calling getOp()"; + //////// all checks before this line // special cases for parameterized operators that are not indexed operators // the API level differs from the internal structure @@ -2239,26 +2256,41 @@ Op Term::getOp() const // Notice this is the only case where getKindHelper is used, since the // cases above do not have special cases for intToExtKind. return Op(d_solver, getKindHelper()); + //////// + CVC4_API_TRY_CATCH_END; } -bool Term::isNull() const { return isNullHelper(); } +bool Term::isNull() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return isNullHelper(); + //////// + CVC4_API_TRY_CATCH_END; +} Term Term::getConstArrayBase() const { NodeManagerScope scope(d_solver->getNodeManager()); + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; // CONST_ARRAY kind maps to STORE_ALL internal kind CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::STORE_ALL) << "Expecting a CONST_ARRAY Term when calling getConstArrayBase()"; + //////// all checks before this line return Term(d_solver, d_node->getConst().getValue()); + //////// + CVC4_API_TRY_CATCH_END; } std::vector Term::getConstSequenceElements() const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::CONST_SEQUENCE) << "Expecting a CONST_SEQUENCE Term when calling " "getConstSequenceElements()"; + //////// all checks before this line const std::vector& elems = d_node->getConst().getVec(); std::vector terms; for (const Node& t : elems) @@ -2266,128 +2298,113 @@ std::vector Term::getConstSequenceElements() const terms.push_back(Term(d_solver, t)); } return terms; + //////// + CVC4_API_TRY_CATCH_END; } Term Term::notTerm() const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; - try - { - Node res = d_node->notNode(); - (void)res.getType(true); /* kick off type checking */ - return Term(d_solver, res); - } - catch (const CVC4::TypeCheckingExceptionPrivate& e) - { - throw CVC4ApiException(e.getMessage()); - } + //////// all checks before this line + Node res = d_node->notNode(); + (void)res.getType(true); /* kick off type checking */ + return Term(d_solver, res); + //////// + CVC4_API_TRY_CATCH_END; } Term Term::andTerm(const Term& t) const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; - CVC4_API_ARG_CHECK_NOT_NULL(t); - try - { - Node res = d_node->andNode(*t.d_node); - (void)res.getType(true); /* kick off type checking */ - return Term(d_solver, res); - } - catch (const CVC4::TypeCheckingExceptionPrivate& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_CHECK_TERM(t); + //////// all checks before this line + Node res = d_node->andNode(*t.d_node); + (void)res.getType(true); /* kick off type checking */ + return Term(d_solver, res); + //////// + CVC4_API_TRY_CATCH_END; } Term Term::orTerm(const Term& t) const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; - CVC4_API_ARG_CHECK_NOT_NULL(t); - try - { - Node res = d_node->orNode(*t.d_node); - (void)res.getType(true); /* kick off type checking */ - return Term(d_solver, res); - } - catch (const CVC4::TypeCheckingExceptionPrivate& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_CHECK_TERM(t); + //////// all checks before this line + Node res = d_node->orNode(*t.d_node); + (void)res.getType(true); /* kick off type checking */ + return Term(d_solver, res); + //////// + CVC4_API_TRY_CATCH_END; } Term Term::xorTerm(const Term& t) const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; - CVC4_API_ARG_CHECK_NOT_NULL(t); - try - { - Node res = d_node->xorNode(*t.d_node); - (void)res.getType(true); /* kick off type checking */ - return Term(d_solver, res); - } - catch (const CVC4::TypeCheckingExceptionPrivate& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_CHECK_TERM(t); + //////// all checks before this line + Node res = d_node->xorNode(*t.d_node); + (void)res.getType(true); /* kick off type checking */ + return Term(d_solver, res); + //////// + CVC4_API_TRY_CATCH_END; } Term Term::eqTerm(const Term& t) const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; - CVC4_API_ARG_CHECK_NOT_NULL(t); - try - { - Node res = d_node->eqNode(*t.d_node); - (void)res.getType(true); /* kick off type checking */ - return Term(d_solver, res); - } - catch (const CVC4::TypeCheckingExceptionPrivate& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_CHECK_TERM(t); + //////// all checks before this line + Node res = d_node->eqNode(*t.d_node); + (void)res.getType(true); /* kick off type checking */ + return Term(d_solver, res); + //////// + CVC4_API_TRY_CATCH_END; } Term Term::impTerm(const Term& t) const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; - CVC4_API_ARG_CHECK_NOT_NULL(t); - try - { - Node res = d_node->impNode(*t.d_node); - (void)res.getType(true); /* kick off type checking */ - return Term(d_solver, res); - } - catch (const CVC4::TypeCheckingExceptionPrivate& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_CHECK_TERM(t); + //////// all checks before this line + Node res = d_node->impNode(*t.d_node); + (void)res.getType(true); /* kick off type checking */ + return Term(d_solver, res); + //////// + CVC4_API_TRY_CATCH_END; } Term Term::iteTerm(const Term& then_t, const Term& else_t) const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; - CVC4_API_ARG_CHECK_NOT_NULL(then_t); - CVC4_API_ARG_CHECK_NOT_NULL(else_t); - try - { - Node res = d_node->iteNode(*then_t.d_node, *else_t.d_node); - (void)res.getType(true); /* kick off type checking */ - return Term(d_solver, res); - } - catch (const CVC4::TypeCheckingExceptionPrivate& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_CHECK_TERM(then_t); + CVC4_API_CHECK_TERM(else_t); + //////// all checks before this line + Node res = d_node->iteNode(*then_t.d_node, *else_t.d_node); + (void)res.getType(true); /* kick off type checking */ + return Term(d_solver, res); + //////// + CVC4_API_TRY_CATCH_END; } std::string Term::toString() const { + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line if (d_solver != nullptr) { NodeManagerScope scope(d_solver->getNodeManager()); return d_node->toString(); } return d_node->toString(); + //////// + CVC4_API_TRY_CATCH_END; } Term::const_iterator::const_iterator() @@ -2552,52 +2569,109 @@ bool isUInt64(const Node& node) } } // namespace detail -bool Term::isInt32() const { return detail::isInt32(*d_node); } +bool Term::isInt32() const +{ + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return detail::isInt32(*d_node); + //////// + CVC4_API_TRY_CATCH_END; +} + std::int32_t Term::getInt32() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(detail::isInt32(*d_node)) << "Term should be a Int32 when calling getInt32()"; + //////// all checks before this line return detail::getInteger(*d_node).getSignedInt(); + //////// + CVC4_API_TRY_CATCH_END; } + bool Term::isUInt32() const { return detail::isUInt32(*d_node); } std::uint32_t Term::getUInt32() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(detail::isUInt32(*d_node)) << "Term should be a UInt32 when calling getUInt32()"; + //////// all checks before this line return detail::getInteger(*d_node).getUnsignedInt(); + //////// + CVC4_API_TRY_CATCH_END; } + bool Term::isInt64() const { return detail::isInt64(*d_node); } std::int64_t Term::getInt64() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(detail::isInt64(*d_node)) << "Term should be a Int64 when calling getInt64()"; + //////// all checks before this line return detail::getInteger(*d_node).getLong(); + //////// + CVC4_API_TRY_CATCH_END; } -bool Term::isUInt64() const { return detail::isUInt64(*d_node); } + +bool Term::isUInt64() const +{ + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return detail::isUInt64(*d_node); + //////// + CVC4_API_TRY_CATCH_END; +} + std::uint64_t Term::getUInt64() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(detail::isUInt64(*d_node)) << "Term should be a UInt64 when calling getUInt64()"; + //////// all checks before this line return detail::getInteger(*d_node).getUnsignedLong(); + //////// + CVC4_API_TRY_CATCH_END; } + bool Term::isInteger() const { return detail::isInteger(*d_node); } std::string Term::getInteger() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(detail::isInteger(*d_node)) << "Term should be an Int when calling getIntString()"; + //////// all checks before this line return detail::getInteger(*d_node).toString(); + //////// + CVC4_API_TRY_CATCH_END; } bool Term::isString() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line return d_node->getKind() == CVC4::Kind::CONST_STRING; + //////// + CVC4_API_TRY_CATCH_END; } std::wstring Term::getString() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::CONST_STRING) << "Term should be a String when calling getString()"; + //////// all checks before this line return d_node->getConst().toWString(); + //////// + CVC4_API_TRY_CATCH_END; } std::vector Term::termVectorToNodes(const std::vector& terms) @@ -2657,6 +2731,63 @@ size_t TermHashFunction::operator()(const Term& t) const return NodeHashFunction()(*t.d_node); } +/* Helpers */ +/* -------------------------------------------------------------------------- */ + +/* Split out to avoid nested API calls (problematic with API tracing). */ +/* .......................................................................... */ + +bool Term::isNullHelper() const +{ + /* Split out to avoid nested API calls (problematic with API tracing). */ + return d_node->isNull(); +} + +Kind Term::getKindHelper() const +{ + /* Sequence kinds do not exist internally, so we must convert their internal + * (string) versions back to sequence. All operators where this is + * necessary are such that their first child is of sequence type, which + * we check here. */ + if (d_node->getNumChildren() > 0 && (*d_node)[0].getType().isSequence()) + { + switch (d_node->getKind()) + { + case CVC4::Kind::STRING_CONCAT: return SEQ_CONCAT; + case CVC4::Kind::STRING_LENGTH: return SEQ_LENGTH; + case CVC4::Kind::STRING_SUBSTR: return SEQ_EXTRACT; + case CVC4::Kind::STRING_UPDATE: return SEQ_UPDATE; + case CVC4::Kind::STRING_CHARAT: return SEQ_AT; + case CVC4::Kind::STRING_STRCTN: return SEQ_CONTAINS; + case CVC4::Kind::STRING_STRIDOF: return SEQ_INDEXOF; + case CVC4::Kind::STRING_STRREPL: return SEQ_REPLACE; + case CVC4::Kind::STRING_STRREPLALL: return SEQ_REPLACE_ALL; + case CVC4::Kind::STRING_REV: return SEQ_REV; + case CVC4::Kind::STRING_PREFIX: return SEQ_PREFIX; + case CVC4::Kind::STRING_SUFFIX: return SEQ_SUFFIX; + default: + // fall through to conversion below + break; + } + } + // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to + // INTERNAL_KIND. + if (isCastedReal()) + { + return CONST_RATIONAL; + } + return intToExtKind(d_node->getKind()); +} + +bool Term::isCastedReal() const +{ + if (d_node->getKind() == kind::CAST_TO_REAL) + { + return (*d_node)[0].isConst() && (*d_node)[0].getType().isInteger(); + } + return false; +} + /* -------------------------------------------------------------------------- */ /* Datatypes */ /* -------------------------------------------------------------------------- */ diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 8e7971e68..7e169a6c8 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -998,15 +998,15 @@ class CVC4_EXPORT Term Sort getSort() const; /** - * @return the result of replacing "e" by "replacement" in this term + * @return the result of replacing 'term' by 'replacement' in this term */ - Term substitute(const Term& e, const Term& replacement) const; + Term substitute(const Term& term, const Term& replacement) const; /** - * @return the result of simulatenously replacing "es" by "replacements" in - * this term + * @return the result of simulatenously replacing 'terms' by 'replacements' + * in this term */ - Term substitute(const std::vector& es, + Term substitute(const std::vector& terms, const std::vector& replacements) const; /**