diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-05-13 13:51:07 -0700 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-08-07 11:19:57 -0700 |
commit | 800845fab13fd153dc94f9951bf05c4cf0fd9d63 (patch) | |
tree | 255da7ad77d40fa293ca3ad119ea700213903d05 /src | |
parent | 6b5b18c6bfd924f0e20b0c9439da3113acb76a27 (diff) |
New C++ API: Introduce macros for try-catch blocks in Solver. (#3121)
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 820 |
1 files changed, 409 insertions, 411 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 6374dad14..60dbd6714 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -675,6 +675,14 @@ class CVC4ApiExceptionStream & CVC4ApiExceptionStream().ostream() \ << "Invalid " << what << " '" << arg << "' at index" << idx \ << ", expected " + +#define CVC4_API_SOLVER_TRY_CATCH_BEGIN \ + try \ + { +#define CVC4_API_SOLVER_TRY_CATCH_END \ + } \ + catch (const CVC4::Exception& e) { throw CVC4ApiException(e.getMessage()); } \ + catch (const std::invalid_argument& e) { throw CVC4ApiException(e.what()); } } // namespace /* -------------------------------------------------------------------------- */ @@ -1776,56 +1784,101 @@ Solver::~Solver() {} /* Sorts Handling */ /* -------------------------------------------------------------------------- */ -Sort Solver::getNullSort(void) const { return Type(); } +Sort Solver::getNullSort(void) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return Type(); + CVC4_API_SOLVER_TRY_CATCH_END; +} -Sort Solver::getBooleanSort(void) const { return d_exprMgr->booleanType(); } +Sort Solver::getBooleanSort(void) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return d_exprMgr->booleanType(); + CVC4_API_SOLVER_TRY_CATCH_END; +} -Sort Solver::getIntegerSort(void) const { return d_exprMgr->integerType(); } +Sort Solver::getIntegerSort(void) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return d_exprMgr->integerType(); + CVC4_API_SOLVER_TRY_CATCH_END; +} -Sort Solver::getRealSort(void) const { return d_exprMgr->realType(); } +Sort Solver::getRealSort(void) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return d_exprMgr->realType(); + CVC4_API_SOLVER_TRY_CATCH_END; +} -Sort Solver::getRegExpSort(void) const { return d_exprMgr->regExpType(); } +Sort Solver::getRegExpSort(void) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return d_exprMgr->regExpType(); + CVC4_API_SOLVER_TRY_CATCH_END; +} -Sort Solver::getStringSort(void) const { return d_exprMgr->stringType(); } +Sort Solver::getStringSort(void) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return d_exprMgr->stringType(); + CVC4_API_SOLVER_TRY_CATCH_END; +} Sort Solver::getRoundingmodeSort(void) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return d_exprMgr->roundingModeType(); + CVC4_API_SOLVER_TRY_CATCH_END; } /* Create sorts ------------------------------------------------------- */ Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!indexSort.isNull(), indexSort) << "non-null index sort"; CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) << "non-null element sort"; + return d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type); + CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkBitVectorSort(uint32_t size) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "size > 0"; + return d_exprMgr->mkBitVectorType(size); + CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0"; CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0"; + return d_exprMgr->mkFloatingPointType(exp, sig); + CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(dtypedecl.getNumConstructors() > 0, dtypedecl) << "a datatype declaration with at least one constructor"; + return d_exprMgr->mkDatatypeType(*dtypedecl.d_dtype); + CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain) << "non-null codomain sort"; CVC4_API_ARG_CHECK_EXPECTED(domain.isFirstClass(), domain) @@ -1833,11 +1886,14 @@ Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const CVC4_API_ARG_CHECK_EXPECTED(codomain.isFirstClass(), codomain) << "first-class sort as codomain sort for function sort"; Assert(!codomain.isFunction()); /* A function sort is not first-class. */ + return d_exprMgr->mkFunctionType(*domain.d_type, *codomain.d_type); + CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts) << "at least one parameter sort for function sort"; for (size_t i = 0, size = sorts.size(); i < size; ++i) @@ -1854,17 +1910,22 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const CVC4_API_ARG_CHECK_EXPECTED(codomain.isFirstClass(), codomain) << "first-class sort as codomain sort for function sort"; Assert(!codomain.isFunction()); /* A function sort is not first-class. */ + std::vector<Type> argTypes = sortVectorToTypes(sorts); return d_exprMgr->mkFunctionType(argTypes, *codomain.d_type); + CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkParamSort(const std::string& symbol) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return d_exprMgr->mkSort(symbol, ExprManager::SORT_FLAG_PLACEHOLDER); + CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts) << "at least one parameter sort for predicate sort"; for (size_t i = 0, size = sorts.size(); i < size; ++i) @@ -1877,12 +1938,15 @@ Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const << "first-class sort as parameter sort for predicate sort"; } std::vector<Type> types = sortVectorToTypes(sorts); + return d_exprMgr->mkPredicateType(types); + CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkRecordSort( const std::vector<std::pair<std::string, Sort>>& fields) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; std::vector<std::pair<std::string, Type>> f; size_t i = 0; for (const auto& p : fields) @@ -1893,30 +1957,41 @@ Sort Solver::mkRecordSort( i += 1; f.emplace_back(p.first, *p.second.d_type); } + return d_exprMgr->mkRecordType(Record(f)); + CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkSetSort(Sort elemSort) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) << "non-null element sort"; + return d_exprMgr->mkSetType(*elemSort.d_type); + CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkUninterpretedSort(const std::string& symbol) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return d_exprMgr->mkSort(symbol); + CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkSortConstructorSort(const std::string& symbol, size_t arity) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(arity > 0, arity) << "an arity > 0"; + return d_exprMgr->mkSortConstructor(symbol, arity); + CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; for (size_t i = 0, size = sorts.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( @@ -1927,7 +2002,9 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const << "non-function-like sort as parameter sort for tuple sort"; } std::vector<Type> types = sortVectorToTypes(sorts); + return d_exprMgr->mkTupleType(types); + CVC4_API_SOLVER_TRY_CATCH_END; } std::vector<Type> Solver::sortVectorToTypes( @@ -1944,432 +2021,395 @@ std::vector<Type> Solver::sortVectorToTypes( /* Create consts */ /* -------------------------------------------------------------------------- */ -Term Solver::mkTrue(void) const { return d_exprMgr->mkConst<bool>(true); } +Term Solver::mkTrue(void) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return d_exprMgr->mkConst<bool>(true); + CVC4_API_SOLVER_TRY_CATCH_END; +} -Term Solver::mkFalse(void) const { return d_exprMgr->mkConst<bool>(false); } +Term Solver::mkFalse(void) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return d_exprMgr->mkConst<bool>(false); + CVC4_API_SOLVER_TRY_CATCH_END; +} -Term Solver::mkBoolean(bool val) const { return d_exprMgr->mkConst<bool>(val); } +Term Solver::mkBoolean(bool val) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return d_exprMgr->mkConst<bool>(val); + CVC4_API_SOLVER_TRY_CATCH_END; +} Term Solver::mkPi() const { - try - { - Term res = - d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + Term res = + d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } template <typename T> Term Solver::mkValHelper(T t) const { - try - { - Term res = d_exprMgr->mkConst(t); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } + Term res = d_exprMgr->mkConst(t); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; } /* Split out to avoid nested API calls (problematic with API tracing). */ Term Solver::mkRealFromStrHelper(std::string s) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP * throws an std::invalid_argument exception. For consistency, we treat it * as invalid. */ CVC4_API_ARG_CHECK_EXPECTED(s != ".", s) << "a string representing an integer, real or rational value."; - try - { - CVC4::Rational r = s.find('/') != std::string::npos - ? CVC4::Rational(s) - : CVC4::Rational::fromDecimal(s); - return mkValHelper<CVC4::Rational>(r); - } - catch (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } + + CVC4::Rational r = s.find('/') != std::string::npos + ? CVC4::Rational(s) + : CVC4::Rational::fromDecimal(s); + return mkValHelper<CVC4::Rational>(r); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkReal(const char* s) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_NOT_NULL(s); + return mkRealFromStrHelper(std::string(s)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkReal(const std::string& s) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkRealFromStrHelper(s); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkReal(int32_t val) const { - try - { - return mkValHelper<CVC4::Rational>(CVC4::Rational(val)); - } - catch (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return mkValHelper<CVC4::Rational>(CVC4::Rational(val)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkReal(int64_t val) const { - try - { - return mkValHelper<CVC4::Rational>(CVC4::Rational(val)); - } - catch (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return mkValHelper<CVC4::Rational>(CVC4::Rational(val)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkReal(uint32_t val) const { - try - { - return mkValHelper<CVC4::Rational>(CVC4::Rational(val)); - } - catch (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return mkValHelper<CVC4::Rational>(CVC4::Rational(val)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkReal(uint64_t val) const { - try - { - return mkValHelper<CVC4::Rational>(CVC4::Rational(val)); - } - catch (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return mkValHelper<CVC4::Rational>(CVC4::Rational(val)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkReal(int32_t num, int32_t den) const { - try - { - return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); - } - catch (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkReal(int64_t num, int64_t den) const { - try - { - return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); - } - catch (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkReal(uint32_t num, uint32_t den) const { - try - { - return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); - } - catch (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkReal(uint64_t num, uint64_t den) const { - try - { - return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); - } - catch (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkRegexpEmpty() const { - try - { - Term res = - d_exprMgr->mkExpr(CVC4::kind::REGEXP_EMPTY, std::vector<CVC4::Expr>()); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + + Term res = + d_exprMgr->mkExpr(CVC4::kind::REGEXP_EMPTY, std::vector<CVC4::Expr>()); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkRegexpSigma() const { - try - { - Term res = - d_exprMgr->mkExpr(CVC4::kind::REGEXP_SIGMA, std::vector<CVC4::Expr>()); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + Term res = + d_exprMgr->mkExpr(CVC4::kind::REGEXP_SIGMA, std::vector<CVC4::Expr>()); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkEmptySet(Sort s) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isSet(), s) << "null sort or set sort"; + return mkValHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkSepNil(Sort sort) const { - try - { - CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; - Term res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; + + Term res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkString(const char* s, bool useEscSequences) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkValHelper<CVC4::String>(CVC4::String(s, useEscSequences)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkString(const std::string& s, bool useEscSequences) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkValHelper<CVC4::String>(CVC4::String(s, useEscSequences)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkString(const unsigned char c) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkValHelper<CVC4::String>(CVC4::String(std::string(1, c))); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkString(const std::vector<unsigned>& s) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkValHelper<CVC4::String>(CVC4::String(s)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkUniverseSet(Sort sort) const { - try - { - CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; - Term res = - d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET); - // TODO(#2771): Reenable? - // (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; + + Term res = + d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET); + // TODO(#2771): Reenable? + // (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } /* Split out to avoid nested API calls (problematic with API tracing). */ Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0"; - try - { - return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val)); - } - catch (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } + + return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkBitVector(uint32_t size, uint64_t val) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkBVFromIntHelper(size, val); + CVC4_API_SOLVER_TRY_CATCH_END; } /* Split out to avoid nested API calls (problematic with API tracing). */ Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s) << "base 2, 10, or 16"; - try - { - return mkValHelper<CVC4::BitVector>(CVC4::BitVector(s, base)); - } - catch (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } + + return mkValHelper<CVC4::BitVector>(CVC4::BitVector(s, base)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkBVFromStrHelper(uint32_t size, std::string s, uint32_t base) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s) << "base 2, 10, or 16"; - try - { - Integer val(s, base); - CVC4_API_CHECK(val.modByPow2(size) == val) - << "Overflow in bitvector construction (specified bitvector size " - << size << " too small to hold value " << s << ")"; - return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val)); - } - catch (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } + + Integer val(s, base); + CVC4_API_CHECK(val.modByPow2(size) == val) + << "Overflow in bitvector construction (specified bitvector size " << size + << " too small to hold value " << s << ")"; + return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkBitVector(const char* s, uint32_t base) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_NOT_NULL(s); + return mkBVFromStrHelper(std::string(s), base); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkBitVector(const std::string& s, uint32_t base) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkBVFromStrHelper(s, base); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkBitVector(uint32_t size, const char* s, uint32_t base) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_NOT_NULL(s); + return mkBVFromStrHelper(size, s, base); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkBitVector(uint32_t size, std::string& s, uint32_t base) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkBVFromStrHelper(size, s, base); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; + return mkValHelper<CVC4::FloatingPoint>( FloatingPoint::makeInf(FloatingPointSize(exp, sig), false)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; + return mkValHelper<CVC4::FloatingPoint>( FloatingPoint::makeInf(FloatingPointSize(exp, sig), true)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkNaN(uint32_t exp, uint32_t sig) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; + return mkValHelper<CVC4::FloatingPoint>( FloatingPoint::makeNaN(FloatingPointSize(exp, sig))); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; + return mkValHelper<CVC4::FloatingPoint>( FloatingPoint::makeZero(FloatingPointSize(exp, sig), false)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; + return mkValHelper<CVC4::FloatingPoint>( FloatingPoint::makeZero(FloatingPointSize(exp, sig), true)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkRoundingMode(RoundingMode rm) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkValHelper<CVC4::RoundingMode>(s_rmodes.at(rm)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; + return mkValHelper<CVC4::UninterpretedConstant>( CVC4::UninterpretedConstant(*sort.d_type, index)); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkAbstractValue(const std::string& index) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!index.empty(), index) << "a non-empty string"; - try - { - CVC4::Integer idx(index, 10); - CVC4_API_ARG_CHECK_EXPECTED(idx > 0, index) - << "a string representing an integer > 0"; - return d_exprMgr->mkConst(CVC4::AbstractValue(idx)); - // do not call getType(), for abstract values, type can not be computed - // until it is substituted away - } - catch (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } + + CVC4::Integer idx(index, 10); + CVC4_API_ARG_CHECK_EXPECTED(idx > 0, index) + << "a string representing an integer > 0"; + return d_exprMgr->mkConst(CVC4::AbstractValue(idx)); + // do not call getType(), for abstract values, type can not be computed + // until it is substituted away + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkAbstractValue(uint64_t index) const { - try - { - CVC4_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0"; - return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(index))); - // do not call getType(), for abstract values, type can not be computed - // until it is substituted away - } - catch (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0"; + + return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(index))); + // do not call getType(), for abstract values, type can not be computed + // until it is substituted away + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0"; @@ -2381,8 +2421,10 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const CVC4_API_ARG_CHECK_EXPECTED( val.getSort().isBitVector() && val.d_expr->isConst(), val) << "bit-vector constant"; + return mkValHelper<CVC4::FloatingPoint>( CVC4::FloatingPoint(exp, sig, val.d_expr->getConst<BitVector>())); + CVC4_API_SOLVER_TRY_CATCH_END; } /* Create constants */ @@ -2390,18 +2432,14 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const Term Solver::mkConst(Sort sort, const std::string& symbol) const { - try - { - CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; - Term res = symbol.empty() ? d_exprMgr->mkVar(*sort.d_type) - : d_exprMgr->mkVar(symbol, *sort.d_type); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; + + Term res = symbol.empty() ? d_exprMgr->mkVar(*sort.d_type) + : d_exprMgr->mkVar(symbol, *sort.d_type); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } /* Create variables */ @@ -2409,18 +2447,14 @@ Term Solver::mkConst(Sort sort, const std::string& symbol) const Term Solver::mkVar(Sort sort, const std::string& symbol) const { - try - { - CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; - Term res = symbol.empty() ? d_exprMgr->mkBoundVar(*sort.d_type) - : d_exprMgr->mkBoundVar(symbol, *sort.d_type); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; + + Term res = symbol.empty() ? d_exprMgr->mkBoundVar(*sort.d_type) + : d_exprMgr->mkBoundVar(symbol, *sort.d_type); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } /* Create terms */ @@ -2477,239 +2511,191 @@ void Solver::checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const Term Solver::mkTerm(Kind kind) const { - try + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_KIND_CHECK_EXPECTED( + kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind) + << "PI or REGEXP_EMPTY or REGEXP_SIGMA"; + + Term res; + if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA) { - CVC4_API_KIND_CHECK_EXPECTED( - kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind) - << "PI or REGEXP_EMPTY or REGEXP_SIGMA"; - Term res; - if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA) - { - CVC4::Kind k = extToIntKind(kind); - Assert(isDefinedIntKind(k)); - res = d_exprMgr->mkExpr(k, std::vector<Expr>()); - } - else - { - Assert(kind == PI); - res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI); - } - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; + CVC4::Kind k = extToIntKind(kind); + Assert(isDefinedIntKind(k)); + res = d_exprMgr->mkExpr(k, std::vector<Expr>()); } - catch (const CVC4::TypeCheckingException& e) + else { - throw CVC4ApiException(e.getMessage()); + Assert(kind == PI); + res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI); } + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTerm(Kind kind, Term child) const { - try - { - CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term"; - checkMkTerm(kind, 1); - Term res = d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term"; + + checkMkTerm(kind, 1); + Term res = d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTerm(Kind kind, Term child1, Term child2) const { - try - { - CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; - CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; - checkMkTerm(kind, 2); - Term res = - d_exprMgr->mkExpr(extToIntKind(kind), *child1.d_expr, *child2.d_expr); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; + CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; + + checkMkTerm(kind, 2); + Term res = + d_exprMgr->mkExpr(extToIntKind(kind), *child1.d_expr, *child2.d_expr); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const { - try - { - CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; - CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; - CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term"; - checkMkTerm(kind, 3); - std::vector<Expr> echildren{*child1.d_expr, *child2.d_expr, *child3.d_expr}; - CVC4::Kind k = extToIntKind(kind); - Assert(isDefinedIntKind(k)); - Term res = kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren) - : d_exprMgr->mkExpr(k, echildren); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; + CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; + CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term"; + + checkMkTerm(kind, 3); + std::vector<Expr> echildren{*child1.d_expr, *child2.d_expr, *child3.d_expr}; + CVC4::Kind k = extToIntKind(kind); + Assert(isDefinedIntKind(k)); + Term res = kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren) + : d_exprMgr->mkExpr(k, echildren); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const { - try + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + for (size_t i = 0, size = children.size(); i < size; ++i) { - for (size_t i = 0, size = children.size(); i < size; ++i) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !children[i].isNull(), "parameter term", children[i], i) - << "non-null term"; - } - checkMkTerm(kind, children.size()); - std::vector<Expr> echildren = termVectorToExprs(children); - CVC4::Kind k = extToIntKind(kind); - Assert(isDefinedIntKind(k)); - Term res = kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren) - : d_exprMgr->mkExpr(k, echildren); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + !children[i].isNull(), "parameter term", children[i], i) + << "non-null term"; } + + checkMkTerm(kind, children.size()); + std::vector<Expr> echildren = termVectorToExprs(children); + CVC4::Kind k = extToIntKind(kind); + Assert(isDefinedIntKind(k)); + Term res = kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren) + : d_exprMgr->mkExpr(k, echildren); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTerm(Kind kind, OpTerm opTerm) const { - try - { - checkMkOpTerm(kind, opTerm, 0); - const CVC4::Kind int_kind = extToIntKind(kind); - Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + checkMkOpTerm(kind, opTerm, 0); + const CVC4::Kind int_kind = extToIntKind(kind); + Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child) const { - try - { - CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term"; - checkMkOpTerm(kind, opTerm, 1); - const CVC4::Kind int_kind = extToIntKind(kind); - Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, *child.d_expr); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term"; + + checkMkOpTerm(kind, opTerm, 1); + const CVC4::Kind int_kind = extToIntKind(kind); + Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, *child.d_expr); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const { - try - { - CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; - CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; - checkMkOpTerm(kind, opTerm, 2); - const CVC4::Kind int_kind = extToIntKind(kind); - Term res = d_exprMgr->mkExpr( - int_kind, *opTerm.d_expr, *child1.d_expr, *child2.d_expr); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; + CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; + + checkMkOpTerm(kind, opTerm, 2); + const CVC4::Kind int_kind = extToIntKind(kind); + Term res = d_exprMgr->mkExpr( + int_kind, *opTerm.d_expr, *child1.d_expr, *child2.d_expr); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTerm( Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) const { - try - { - CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; - CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; - CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term"; - checkMkOpTerm(kind, opTerm, 3); - const CVC4::Kind int_kind = extToIntKind(kind); - Term res = d_exprMgr->mkExpr(int_kind, - *opTerm.d_expr, - *child1.d_expr, - *child2.d_expr, - *child3.d_expr); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; + CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; + CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term"; + + checkMkOpTerm(kind, opTerm, 3); + const CVC4::Kind int_kind = extToIntKind(kind); + Term res = d_exprMgr->mkExpr( + int_kind, *opTerm.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTerm(Kind kind, OpTerm opTerm, const std::vector<Term>& children) const { - try - { - for (size_t i = 0, size = children.size(); i < size; ++i) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !children[i].isNull(), "parameter term", children[i], i) - << "non-null term"; - } - checkMkOpTerm(kind, opTerm, children.size()); - const CVC4::Kind int_kind = extToIntKind(kind); - std::vector<Expr> echildren = termVectorToExprs(children); - Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, echildren); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + for (size_t i = 0, size = children.size(); i < size; ++i) { - throw CVC4ApiException(e.getMessage()); + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + !children[i].isNull(), "parameter term", children[i], i) + << "non-null term"; } + + checkMkOpTerm(kind, opTerm, children.size()); + const CVC4::Kind int_kind = extToIntKind(kind); + std::vector<Expr> echildren = termVectorToExprs(children); + Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, echildren); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkTuple(const std::vector<Sort>& sorts, const std::vector<Term>& terms) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(sorts.size() == terms.size()) << "Expected the same number of sorts and elements"; - try - { - std::vector<CVC4::Expr> args; - for (size_t i = 0, size = sorts.size(); i < size; i++) - { - args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_expr); - } - Sort s = mkTupleSort(sorts); - Datatype dt = s.getDatatype(); - Term res = d_exprMgr->mkExpr(extToIntKind(APPLY_CONSTRUCTOR), - *dt[0].getConstructorTerm().d_expr, - args); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) + std::vector<CVC4::Expr> args; + for (size_t i = 0, size = sorts.size(); i < size; i++) { - throw CVC4ApiException(e.getMessage()); + args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_expr); } + + Sort s = mkTupleSort(sorts); + Datatype dt = s.getDatatype(); + Term res = d_exprMgr->mkExpr(extToIntKind(APPLY_CONSTRUCTOR), + *dt[0].getConstructorTerm().d_expr, + args); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; } std::vector<Expr> Solver::termVectorToExprs( @@ -2728,20 +2714,28 @@ std::vector<Expr> Solver::termVectorToExprs( OpTerm Solver::mkOpTerm(Kind kind, Kind k) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP"; + return *mkValHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get(); + CVC4_API_SOLVER_TRY_CATCH_END; } OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_KIND_CHECK_EXPECTED(kind == RECORD_UPDATE_OP, kind) << "RECORD_UPDATE_OP"; + return *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get(); + CVC4_API_SOLVER_TRY_CATCH_END; } OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_KIND_CHECK(kind); + OpTerm res; switch (kind) { @@ -2806,11 +2800,14 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) const } Assert(!res.isNull()); return res; + CVC4_API_SOLVER_TRY_CATCH_END; } OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_KIND_CHECK(kind); + OpTerm res; switch (kind) { @@ -2855,6 +2852,7 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) const } Assert(!res.isNull()); return res; + CVC4_API_SOLVER_TRY_CATCH_END; } /* Non-SMT-LIB commands */ |