From: Aina Niemetz Date: Tue, 16 Mar 2021 00:13:08 +0000 (-0700) Subject: New C++ Api: Comprehensive guards for member functions of class Sort. (#6136) X-Git-Tag: cvc5-1.0.0~2072 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3dda54ba7e6952060766775c56969ab920430a8a;p=cvc5.git New C++ Api: Comprehensive guards for member functions of class Sort. (#6136) --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 933177783..9d55a7eb6 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1001,102 +1001,336 @@ std::vector Sort::typeNodeVectorToSorts( return sorts; } -/* Helpers */ -/* -------------------------------------------------------------------------- */ - -/* Split out to avoid nested API calls (problematic with API tracing). */ -/* .......................................................................... */ - -bool Sort::isNullHelper() const { return d_type->isNull(); } - -bool Sort::operator==(const Sort& s) const { return *d_type == *s.d_type; } +bool Sort::operator==(const Sort& s) const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return *d_type == *s.d_type; + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::operator!=(const Sort& s) const { return *d_type != *s.d_type; } +bool Sort::operator!=(const Sort& s) const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return *d_type != *s.d_type; + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::operator<(const Sort& s) const { return *d_type < *s.d_type; } +bool Sort::operator<(const Sort& s) const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return *d_type < *s.d_type; + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::operator>(const Sort& s) const { return *d_type > *s.d_type; } +bool Sort::operator>(const Sort& s) const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return *d_type > *s.d_type; + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::operator<=(const Sort& s) const { return *d_type <= *s.d_type; } +bool Sort::operator<=(const Sort& s) const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return *d_type <= *s.d_type; + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::operator>=(const Sort& s) const { return *d_type >= *s.d_type; } +bool Sort::operator>=(const Sort& s) const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return *d_type >= *s.d_type; + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isNull() const { return isNullHelper(); } +bool Sort::isNull() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return isNullHelper(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isBoolean() const { return d_type->isBoolean(); } +bool Sort::isBoolean() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isBoolean(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isInteger() const { return d_type->isInteger(); } +bool Sort::isInteger() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isInteger(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isReal() const { return d_type->isReal(); } +bool Sort::isReal() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isReal(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isString() const { return d_type->isString(); } +bool Sort::isString() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isString(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isRegExp() const { return d_type->isRegExp(); } +bool Sort::isRegExp() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isRegExp(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isRoundingMode() const { return d_type->isRoundingMode(); } +bool Sort::isRoundingMode() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isRoundingMode(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isBitVector() const { return d_type->isBitVector(); } +bool Sort::isBitVector() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isBitVector(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isFloatingPoint() const { return d_type->isFloatingPoint(); } +bool Sort::isFloatingPoint() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isFloatingPoint(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isDatatype() const { return d_type->isDatatype(); } +bool Sort::isDatatype() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isDatatype(); + //////// + CVC4_API_TRY_CATCH_END; +} bool Sort::isParametricDatatype() const { + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line if (!d_type->isDatatype()) return false; return d_type->isParametricDatatype(); + //////// + CVC4_API_TRY_CATCH_END; } -bool Sort::isConstructor() const { return d_type->isConstructor(); } -bool Sort::isSelector() const { return d_type->isSelector(); } -bool Sort::isTester() const { return d_type->isTester(); } +bool Sort::isConstructor() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isConstructor(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isFunction() const { return d_type->isFunction(); } +bool Sort::isSelector() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isSelector(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isPredicate() const { return d_type->isPredicate(); } +bool Sort::isTester() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isTester(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isTuple() const { return d_type->isTuple(); } +bool Sort::isFunction() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isFunction(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isRecord() const { return d_type->isRecord(); } +bool Sort::isPredicate() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isPredicate(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isArray() const { return d_type->isArray(); } +bool Sort::isTuple() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isTuple(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isSet() const { return d_type->isSet(); } +bool Sort::isRecord() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isRecord(); + //////// + CVC4_API_TRY_CATCH_END; +} + +bool Sort::isArray() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isArray(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isBag() const { return d_type->isBag(); } +bool Sort::isSet() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isSet(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isSequence() const { return d_type->isSequence(); } +bool Sort::isBag() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isBag(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isUninterpretedSort() const { return d_type->isSort(); } +bool Sort::isSequence() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isSequence(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isSortConstructor() const { return d_type->isSortConstructor(); } +bool Sort::isUninterpretedSort() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isSort(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isFirstClass() const { return d_type->isFirstClass(); } +bool Sort::isSortConstructor() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isSortConstructor(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Sort::isFunctionLike() const { return d_type->isFunctionLike(); } +bool Sort::isFirstClass() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isFirstClass(); + //////// + CVC4_API_TRY_CATCH_END; +} + +bool Sort::isFunctionLike() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isFunctionLike(); + //////// + CVC4_API_TRY_CATCH_END; +} bool Sort::isSubsortOf(const Sort& s) const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_SOLVER("sort", s); + //////// all checks before this line return d_type->isSubtypeOf(*s.d_type); + //////// + CVC4_API_TRY_CATCH_END; } bool Sort::isComparableTo(const Sort& s) const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_SOLVER("sort", s); + //////// all checks before this line return d_type->isComparableTo(*s.d_type); + //////// + CVC4_API_TRY_CATCH_END; } Datatype Sort::getDatatype() const { NodeManagerScope scope(d_solver->getNodeManager()); + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isDatatype()) << "Expected datatype sort."; + //////// all checks before this line return Datatype(d_solver, d_type->getDType()); + //////// + CVC4_API_TRY_CATCH_END; } Sort Sort::instantiate(const std::vector& params) const { NodeManagerScope scope(d_solver->getNodeManager()); + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + CVC4_API_CHECK_SORTS(params); CVC4_API_CHECK(isParametricDatatype() || isSortConstructor()) << "Expected parametric datatype or sort constructor sort."; + //////// all checks before this line std::vector tparams = sortVectorToTypeNodes(params); if (d_type->isDatatype()) { @@ -1104,40 +1338,59 @@ Sort Sort::instantiate(const std::vector& params) const } Assert(d_type->isSortConstructor()); return Sort(d_solver, d_solver->getNodeManager()->mkSort(*d_type, tparams)); + //////// + CVC4_API_TRY_CATCH_END; } Sort Sort::substitute(const Sort& sort, const Sort& replacement) const { NodeManagerScope scope(d_solver->getNodeManager()); + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + CVC4_API_CHECK_SORT(sort); + CVC4_API_CHECK_SORT(replacement); + //////// all checks before this line return Sort( d_solver, d_type->substitute(sort.getTypeNode(), replacement.getTypeNode())); + //////// + CVC4_API_TRY_CATCH_END; } Sort Sort::substitute(const std::vector& sorts, const std::vector& replacements) const { NodeManagerScope scope(d_solver->getNodeManager()); + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + CVC4_API_CHECK_SORTS(sorts); + CVC4_API_CHECK_SORTS(replacements); + //////// all checks before this line std::vector tSorts = sortVectorToTypeNodes(sorts), tReplacements = sortVectorToTypeNodes(replacements); - return Sort(d_solver, d_type->substitute(tSorts.begin(), tSorts.end(), tReplacements.begin(), tReplacements.end())); + //////// + CVC4_API_TRY_CATCH_END; } std::string Sort::toString() const { + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line if (d_solver != nullptr) { NodeManagerScope scope(d_solver->getNodeManager()); return d_type->toString(); } return d_type->toString(); + //////// + CVC4_API_TRY_CATCH_END; } const CVC4::TypeNode& Sort::getTypeNode(void) const { return *d_type; } @@ -1146,201 +1399,336 @@ const CVC4::TypeNode& Sort::getTypeNode(void) const { return *d_type; } size_t Sort::getConstructorArity() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this); + //////// all checks before this line return d_type->getNumChildren() - 1; + //////// + CVC4_API_TRY_CATCH_END; } std::vector Sort::getConstructorDomainSorts() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this); + //////// all checks before this line return typeNodeVectorToSorts(d_solver, d_type->getArgTypes()); + //////// + CVC4_API_TRY_CATCH_END; } Sort Sort::getConstructorCodomainSort() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this); + //////// all checks before this line return Sort(d_solver, d_type->getConstructorRangeType()); + //////// + CVC4_API_TRY_CATCH_END; } /* Selector sort ------------------------------------------------------- */ Sort Sort::getSelectorDomainSort() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isSelector()) << "Not a selector sort: " << (*this); + //////// all checks before this line return Sort(d_solver, d_type->getSelectorDomainType()); + //////// + CVC4_API_TRY_CATCH_END; } Sort Sort::getSelectorCodomainSort() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isSelector()) << "Not a selector sort: " << (*this); + //////// all checks before this line return Sort(d_solver, d_type->getSelectorRangeType()); + //////// + CVC4_API_TRY_CATCH_END; } /* Tester sort ------------------------------------------------------- */ Sort Sort::getTesterDomainSort() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isTester()) << "Not a tester sort: " << (*this); + //////// all checks before this line return Sort(d_solver, d_type->getTesterDomainType()); + //////// + CVC4_API_TRY_CATCH_END; } Sort Sort::getTesterCodomainSort() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isTester()) << "Not a tester sort: " << (*this); + //////// all checks before this line return d_solver->getBooleanSort(); + //////// + CVC4_API_TRY_CATCH_END; } /* Function sort ------------------------------------------------------- */ size_t Sort::getFunctionArity() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isFunction()) << "Not a function sort: " << (*this); + //////// all checks before this line return d_type->getNumChildren() - 1; + //////// + CVC4_API_TRY_CATCH_END; } std::vector Sort::getFunctionDomainSorts() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isFunction()) << "Not a function sort: " << (*this); + //////// all checks before this line return typeNodeVectorToSorts(d_solver, d_type->getArgTypes()); + //////// + CVC4_API_TRY_CATCH_END; } Sort Sort::getFunctionCodomainSort() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isFunction()) << "Not a function sort" << (*this); + //////// all checks before this line return Sort(d_solver, d_type->getRangeType()); + //////// + CVC4_API_TRY_CATCH_END; } /* Array sort ---------------------------------------------------------- */ Sort Sort::getArrayIndexSort() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isArray()) << "Not an array sort."; + //////// all checks before this line return Sort(d_solver, d_type->getArrayIndexType()); + //////// + CVC4_API_TRY_CATCH_END; } Sort Sort::getArrayElementSort() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isArray()) << "Not an array sort."; + //////// all checks before this line return Sort(d_solver, d_type->getArrayConstituentType()); + //////// + CVC4_API_TRY_CATCH_END; } /* Set sort ------------------------------------------------------------ */ Sort Sort::getSetElementSort() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isSet()) << "Not a set sort."; + //////// all checks before this line return Sort(d_solver, d_type->getSetElementType()); + //////// + CVC4_API_TRY_CATCH_END; } /* Bag sort ------------------------------------------------------------ */ Sort Sort::getBagElementSort() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isBag()) << "Not a bag sort."; + //////// all checks before this line return Sort(d_solver, d_type->getBagElementType()); + //////// + CVC4_API_TRY_CATCH_END; } /* Sequence sort ------------------------------------------------------- */ Sort Sort::getSequenceElementSort() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isSequence()) << "Not a sequence sort."; + //////// all checks before this line return Sort(d_solver, d_type->getSequenceElementType()); + //////// + CVC4_API_TRY_CATCH_END; } /* Uninterpreted sort -------------------------------------------------- */ std::string Sort::getUninterpretedSortName() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; + //////// all checks before this line return d_type->getName(); + //////// + CVC4_API_TRY_CATCH_END; } bool Sort::isUninterpretedSortParameterized() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; - // This method is not implemented in the NodeManager, since whether a - // uninterpreted sort is parametrized is irrelevant for solving. + //////// all checks before this line + + /* This method is not implemented in the NodeManager, since whether a + * uninterpreted sort is parameterized is irrelevant for solving. */ return d_type->getNumChildren() > 0; + //////// + CVC4_API_TRY_CATCH_END; } std::vector Sort::getUninterpretedSortParamSorts() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; - // This method is not implemented in the NodeManager, since whether a - // uninterpreted sort is parametrized is irrelevant for solving. + //////// all checks before this line + + /* This method is not implemented in the NodeManager, since whether a + * uninterpreted sort is parameterized is irrelevant for solving. */ std::vector params; for (size_t i = 0, nchildren = d_type->getNumChildren(); i < nchildren; i++) { params.push_back((*d_type)[i]); } return typeNodeVectorToSorts(d_solver, params); + //////// + CVC4_API_TRY_CATCH_END; } /* Sort constructor sort ----------------------------------------------- */ std::string Sort::getSortConstructorName() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isSortConstructor()) << "Not a sort constructor sort."; + //////// all checks before this line return d_type->getName(); + //////// + CVC4_API_TRY_CATCH_END; } size_t Sort::getSortConstructorArity() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isSortConstructor()) << "Not a sort constructor sort."; + //////// all checks before this line return d_type->getSortConstructorArity(); + //////// + CVC4_API_TRY_CATCH_END; } /* Bit-vector sort ----------------------------------------------------- */ uint32_t Sort::getBVSize() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isBitVector()) << "Not a bit-vector sort."; + //////// all checks before this line return d_type->getBitVectorSize(); + //////// + CVC4_API_TRY_CATCH_END; } /* Floating-point sort ------------------------------------------------- */ uint32_t Sort::getFPExponentSize() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort."; + //////// all checks before this line return d_type->getFloatingPointExponentSize(); + //////// + CVC4_API_TRY_CATCH_END; } uint32_t Sort::getFPSignificandSize() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort."; + //////// all checks before this line return d_type->getFloatingPointSignificandSize(); + //////// + CVC4_API_TRY_CATCH_END; } /* Datatype sort ------------------------------------------------------- */ std::vector Sort::getDatatypeParamSorts() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort."; - std::vector typeNodes = d_type->getParamTypes(); - return typeNodeVectorToSorts(d_solver, typeNodes); + //////// all checks before this line + return typeNodeVectorToSorts(d_solver, d_type->getParamTypes()); + //////// + CVC4_API_TRY_CATCH_END; } size_t Sort::getDatatypeArity() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isDatatype()) << "Not a datatype sort."; + //////// all checks before this line return d_type->getNumChildren() - 1; + //////// + CVC4_API_TRY_CATCH_END; } /* Tuple sort ---------------------------------------------------------- */ size_t Sort::getTupleLength() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isTuple()) << "Not a tuple sort."; + //////// all checks before this line return d_type->getTupleLength(); + //////// + CVC4_API_TRY_CATCH_END; } std::vector Sort::getTupleSorts() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(isTuple()) << "Not a tuple sort."; - std::vector typeNodes = d_type->getTupleTypes(); - return typeNodeVectorToSorts(d_solver, typeNodes); + //////// all checks before this line + return typeNodeVectorToSorts(d_solver, d_type->getTupleTypes()); + //////// + CVC4_API_TRY_CATCH_END; } /* --------------------------------------------------------------------- */ @@ -1356,6 +1744,14 @@ size_t SortHashFunction::operator()(const Sort& s) const return TypeNodeHashFunction()(*s.d_type); } +/* Helpers */ +/* -------------------------------------------------------------------------- */ + +/* Split out to avoid nested API calls (problematic with API tracing). */ +/* .......................................................................... */ + +bool Sort::isNullHelper() const { return d_type->isNull(); } + /* -------------------------------------------------------------------------- */ /* Op */ /* -------------------------------------------------------------------------- */ @@ -3689,10 +4085,10 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& children) const for (size_t i = 0, size = children.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !children[i].isNull(), "child term", children[i], i) + !children[i].isNull(), "child term", children, i) << "non-null term"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == children[i].d_solver, "child term", children[i], i) + this == children[i].d_solver, "child term", children, i) << "a child term associated to this solver object"; } @@ -3791,10 +4187,10 @@ Term Solver::mkTermHelper(const Op& op, const std::vector& children) const for (size_t i = 0, size = children.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !children[i].isNull(), "child term", children[i], i) + !children[i].isNull(), "child term", children, i) << "non-null term"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == children[i].d_solver, "child term", children[i], i) + this == children[i].d_solver, "child term", children, i) << "child term associated to this solver object"; } checkMkTerm(op.d_kind, children.size()); @@ -3818,14 +4214,12 @@ std::vector Solver::mkDatatypeSortsInternal( std::vector datatypes; for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; ++i) { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == dtypedecls[i].d_solver, - "datatype declaration", - dtypedecls[i], - i) + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == dtypedecls[i].d_solver, "datatype declaration", dtypedecls, i) << "a datatype declaration associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(dtypedecls[i].getNumConstructors() > 0, "datatype declaration", - dtypedecls[i], + dtypedecls, i) << "a datatype declaration with at least one constructor"; datatypes.push_back(dtypedecls[i].getDatatype()); @@ -3834,10 +4228,10 @@ std::vector Solver::mkDatatypeSortsInternal( for (auto& sort : unresolvedSorts) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !sort.isNull(), "unresolved sort", sort, i) + !sort.isNull(), "unresolved sort", unresolvedSorts, i) << "non-null sort"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == sort.d_solver, "unresolved sort", sort, i) + this == sort.d_solver, "unresolved sort", unresolvedSorts, i) << "an unresolved sort associated to this solver object"; i += 1; } @@ -3861,15 +4255,15 @@ Term Solver::synthFunHelper(const std::string& symbol, for (size_t i = 0, n = boundVars.size(); i < n; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == boundVars[i].d_solver, "bound variable", boundVars[i], i) + this == boundVars[i].d_solver, "bound variable", boundVars, i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !boundVars[i].isNull(), "bound variable", boundVars[i], i) + !boundVars[i].isNull(), "bound variable", boundVars, i) << "a non-null term"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", - boundVars[i], + boundVars, i) << "a bound variable"; varTypes.push_back(boundVars[i].d_node->getType()); @@ -4188,13 +4582,13 @@ Sort Solver::mkFunctionSort(const std::vector& sorts, for (size_t i = 0, size = sorts.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !sorts[i].isNull(), "parameter sort", sorts[i], i) + !sorts[i].isNull(), "parameter sort", sorts, i) << "non-null sort"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == sorts[i].d_solver, "parameter sort", sorts[i], i) + this == sorts[i].d_solver, "parameter sort", sorts, i) << "sort associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - sorts[i].isFirstClass(), "parameter sort", sorts[i], i) + sorts[i].isFirstClass(), "parameter sort", sorts, i) << "first-class sort as parameter sort for function sort"; } CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain) @@ -4231,13 +4625,13 @@ Sort Solver::mkPredicateSort(const std::vector& sorts) const for (size_t i = 0, size = sorts.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !sorts[i].isNull(), "parameter sort", sorts[i], i) + !sorts[i].isNull(), "parameter sort", sorts, i) << "non-null sort"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == sorts[i].d_solver, "parameter sort", sorts[i], i) + this == sorts[i].d_solver, "parameter sort", sorts, i) << "sort associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - sorts[i].isFirstClass(), "parameter sort", sorts[i], i) + sorts[i].isFirstClass(), "parameter sort", sorts, i) << "first-class sort as parameter sort for predicate sort"; } std::vector types = Sort::sortVectorToTypeNodes(sorts); @@ -4257,10 +4651,10 @@ Sort Solver::mkRecordSort( for (const auto& p : fields) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !p.second.isNull(), "parameter sort", p.second, i) + !p.second.isNull(), "parameter sort", fields, i) << "non-null sort"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == p.second.d_solver, "parameter sort", p.second, i) + this == p.second.d_solver, "parameter sort", fields, i) << "sort associated to this solver object"; i += 1; f.emplace_back(p.first, *p.second.d_type); @@ -4338,13 +4732,13 @@ Sort Solver::mkTupleSort(const std::vector& sorts) const for (size_t i = 0, size = sorts.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !sorts[i].isNull(), "parameter sort", sorts[i], i) + !sorts[i].isNull(), "parameter sort", sorts, i) << "non-null sort"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == sorts[i].d_solver, "parameter sort", sorts[i], i) + this == sorts[i].d_solver, "parameter sort", sorts, i) << "sort associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !sorts[i].isFunctionLike(), "parameter sort", sorts[i], i) + !sorts[i].isFunctionLike(), "parameter sort", sorts, i) << "non-function-like sort as parameter sort for tuple sort"; } return mkTupleSortHelper(sorts); @@ -4849,10 +5243,10 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, for (size_t i = 0, size = params.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !params[i].isNull(), "parameter sort", params[i], i) + !params[i].isNull(), "parameter sort", params, i) << "non-null sort"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == params[i].d_solver, "parameter sort", params[i], i) + this == params[i].d_solver, "parameter sort", params, i) << "sort associated to this solver object"; } return DatatypeDecl(this, name, params, isCoDatatype); @@ -4982,17 +5376,15 @@ Term Solver::mkTuple(const std::vector& sorts, std::vector args; for (size_t i = 0, size = sorts.size(); i < size; i++) { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !sorts[i].isNull(), "sort", sorts[i], i) + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(!sorts[i].isNull(), "sort", sorts, i) << "non-null sort"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !terms[i].isNull(), "term", terms[i], i) + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(!terms[i].isNull(), "term", terms, i) << "non-null term"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == terms[i].d_solver, "child term", terms[i], i) + this == terms[i].d_solver, "child term", terms, i) << "child term associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == sorts[i].d_solver, "child sort", sorts[i], i) + this == sorts[i].d_solver, "child sort", sorts, i) << "child sort associated to this solver object"; args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_node); } @@ -5385,10 +5777,8 @@ Sort Solver::declareDatatype( DatatypeDecl dtdecl(this, symbol); for (size_t i = 0, size = ctors.size(); i < size; i++) { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == ctors[i].d_solver, - "datatype constructor declaration", - ctors[i], - i) + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == ctors[i].d_solver, "datatype constructor declaration", ctors, i) << "datatype constructor declaration associated to this solver object"; dtdecl.addConstructor(ctors[i]); } @@ -5408,10 +5798,10 @@ Term Solver::declareFun(const std::string& symbol, for (size_t i = 0, size = sorts.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == sorts[i].d_solver, "parameter sort", sorts[i], i) + this == sorts[i].d_solver, "parameter sort", sorts, i) << "parameter sort associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - sorts[i].isFirstClass(), "parameter sort", sorts[i], i) + sorts[i].isFirstClass(), "parameter sort", sorts, i) << "first-class sort as parameter sort for function sort"; } CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) @@ -5460,17 +5850,17 @@ Term Solver::defineFun(const std::string& symbol, for (size_t i = 0, size = bound_vars.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i) + this == bound_vars[i].d_solver, "bound variable", bound_vars, i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", - bound_vars[i], + bound_vars, i) << "a bound variable"; CVC4::TypeNode t = bound_vars[i].d_node->getType(); CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - t.isFirstClass(), "sort of parameter", bound_vars[i], i) + t.isFirstClass(), "sort of parameter", bound_vars, i) << "first-class sort of parameter of defined function"; domain_types.push_back(t); } @@ -5509,18 +5899,18 @@ Term Solver::defineFun(const Term& fun, for (size_t i = 0; i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i) + this == bound_vars[i].d_solver, "bound variable", bound_vars, i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", - bound_vars[i], + bound_vars, i) << "a bound variable"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( domain_sorts[i] == bound_vars[i].getSort(), "sort of parameter", - bound_vars[i], + bound_vars, i) << "'" << domain_sorts[i] << "'"; } @@ -5570,17 +5960,17 @@ Term Solver::defineFunRec(const std::string& symbol, for (size_t i = 0, size = bound_vars.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i) + this == bound_vars[i].d_solver, "bound variable", bound_vars, i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", - bound_vars[i], + bound_vars, i) << "a bound variable"; CVC4::TypeNode t = bound_vars[i].d_node->getType(); CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - t.isFirstClass(), "sort of parameter", bound_vars[i], i) + t.isFirstClass(), "sort of parameter", bound_vars, i) << "first-class sort of parameter of defined function"; domain_types.push_back(t); } @@ -5628,18 +6018,18 @@ Term Solver::defineFunRec(const Term& fun, for (size_t i = 0; i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i) + this == bound_vars[i].d_solver, "bound variable", bound_vars, i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", - bound_vars[i], + bound_vars, i) << "a bound variable"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( domain_sorts[i] == bound_vars[i].getSort(), "sort of parameter", - bound_vars[i], + bound_vars, i) << "'" << domain_sorts[i] << "'"; } @@ -5691,9 +6081,10 @@ void Solver::defineFunsRec(const std::vector& funs, const Term& term = terms[j]; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == fun.d_solver, "function", fun, j) + this == fun.d_solver, "function", funs, j) << "function associated to this solver object"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == term.d_solver, "term", term, j) + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == term.d_solver, "term", terms, j) << "term associated to this solver object"; if (fun.getSort().isFunction()) @@ -5707,19 +6098,19 @@ void Solver::defineFunsRec(const std::vector& funs, for (size_t k = 0, nbvars = bvars.size(); k < nbvars; ++k) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == bvars[k].d_solver, "bound variable", bvars[k], k) + this == bvars[k].d_solver, "bound variable", bvars, k) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( bvars[k].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", - bvars[k], + bvars, k) << "a bound variable"; } CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( domain_sorts[i] == bvars[i].getSort(), "sort of parameter", - bvars[i], + bvars, i) << "'" << domain_sorts[i] << "' in parameter bound_vars[" << j << "]"; @@ -5885,7 +6276,7 @@ std::vector Solver::getValue(const std::vector& terms) const for (size_t i = 0, n = terms.size(); i < n; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == terms[i].d_solver, "term", terms[i], i) + this == terms[i].d_solver, "term", terms, i) << "term associated to this solver object"; /* Can not use emplace_back here since constructor is private. */ res.push_back(getValueHelper(terms[i])); @@ -6082,11 +6473,10 @@ void Solver::blockModelValues(const std::vector& terms) const << "a non-empty set of terms"; for (size_t i = 0, tsize = terms.size(); i < tsize; ++i) { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !terms[i].isNull(), "term", terms[i], i) + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(!terms[i].isNull(), "term", terms, i) << "a non-null term"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == terms[i].d_solver, "term", terms[i], i) + this == terms[i].d_solver, "term", terms, i) << "a term associated to this solver object"; } NodeManagerScope scope(getNodeManager()); @@ -6216,15 +6606,15 @@ Grammar Solver::mkSygusGrammar(const std::vector& boundVars, for (size_t i = 0, n = boundVars.size(); i < n; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == boundVars[i].d_solver, "bound variable", boundVars[i], i) + this == boundVars[i].d_solver, "bound variable", boundVars, i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !boundVars[i].isNull(), "bound variable", boundVars[i], i) + !boundVars[i].isNull(), "bound variable", boundVars, i) << "a non-null term"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", - boundVars[i], + boundVars, i) << "a bound variable"; } @@ -6232,15 +6622,15 @@ Grammar Solver::mkSygusGrammar(const std::vector& boundVars, for (size_t i = 0, n = ntSymbols.size(); i < n; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == ntSymbols[i].d_solver, "non-terminal", ntSymbols[i], i) + this == ntSymbols[i].d_solver, "non-terminal", ntSymbols, i) << "term associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !ntSymbols[i].isNull(), "non-terminal", ntSymbols[i], i) + !ntSymbols[i].isNull(), "non-terminal", ntSymbols, i) << "a non-null term"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( ntSymbols[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "non-terminal", - ntSymbols[i], + ntSymbols, i) << "a bound variable"; } @@ -6396,10 +6786,10 @@ std::vector Solver::getSynthSolutions( for (size_t i = 0, n = terms.size(); i < n; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == terms[i].d_solver, "parameter term", terms[i], i) + this == terms[i].d_solver, "parameter term", terms, i) << "parameter term associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !terms[i].isNull(), "parameter term", terms[i], i) + !terms[i].isNull(), "parameter term", terms, i) << "non-null term"; }