diff options
Diffstat (limited to 'src/api/cvc4cpp.cpp')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 238 |
1 files changed, 29 insertions, 209 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index f9dfaa143..5321a90ec 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2303,254 +2303,74 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const FloatingPoint::makeZero(FloatingPointSize(exp, sig), true)); } -Term Solver::mkConst(RoundingMode rm) const +Term Solver::mkRoundingMode(RoundingMode rm) const { return mkConstHelper<CVC4::RoundingMode>(s_rmodes.at(rm)); } -Term Solver::mkConst(Kind kind, Sort arg) const +Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const { - try - { - CVC4_API_ARG_CHECK_EXPECTED( - (kind == EMPTYSET && arg.isNull()) || arg.isSet(), arg) - << "null sort or set sort"; - CVC4_API_KIND_CHECK_EXPECTED(kind == EMPTYSET || kind == UNIVERSE_SET, kind) - << "EMPTY_SET or UNIVERSE_SET"; - if (kind == EMPTYSET) - { - return mkConstHelper<CVC4::EmptySet>(CVC4::EmptySet(*arg.d_type)); - } - else - { - Term res = d_exprMgr->mkNullaryOperator(*arg.d_type, extToIntKind(kind)); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } -} - -Term Solver::mkConst(Kind kind, Sort arg1, int32_t arg2) const -{ - CVC4_API_ARG_CHECK_EXPECTED(!arg1.isNull(), arg1) << "non-null sort"; - CVC4_API_KIND_CHECK_EXPECTED(kind == UNINTERPRETED_CONSTANT, kind) - << "UNINTERPRETED_CONSTANT"; + CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; return mkConstHelper<CVC4::UninterpretedConstant>( - CVC4::UninterpretedConstant(*arg1.d_type, arg2)); -} - -Term Solver::mkConst(Kind kind, bool arg) const -{ - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_BOOLEAN, kind) << "CONST_BOOLEAN"; - return mkConstHelper<bool>(arg); -} - -/* Split out to avoid nested API calls (problematic with API tracing). */ -Term Solver::mkConstFromStrHelper(Kind kind, std::string s) const -{ - CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; - CVC4_API_KIND_CHECK_EXPECTED( - kind == ABSTRACT_VALUE || kind == CONST_RATIONAL || kind == CONST_STRING, - kind) - << "ABSTRACT_VALUE or CONST_RATIONAL or CONST_STRING"; - if (kind == ABSTRACT_VALUE) - { - try - { - return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(s, 10))); - // 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()); - } - } - else if (kind == CONST_RATIONAL) - { - return mkRealFromStrHelper(s); - } - return mkConstHelper<CVC4::String>(CVC4::String(s)); -} - -Term Solver::mkConst(Kind kind, const char* arg) const -{ - CVC4_API_ARG_CHECK_NOT_NULL(arg); - return mkConstFromStrHelper(kind, std::string(arg)); -} - -Term Solver::mkConst(Kind kind, const std::string& arg) const -{ - return mkConstFromStrHelper(kind, arg); + CVC4::UninterpretedConstant(*sort.d_type, index)); } -/* Split out to avoid nested API calls (problematic with API tracing). */ -Term Solver::mkConstFromStrHelper(Kind kind, std::string s, uint32_t a) const -{ - CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_BITVECTOR, kind) - << "CONST_BITVECTOR"; - return mkBVFromStrHelper(s, a); -} - -Term Solver::mkConst(Kind kind, const char* arg1, uint32_t arg2) const -{ - CVC4_API_ARG_CHECK_NOT_NULL(arg1); - return mkConstFromStrHelper(kind, std::string(arg1), arg2); -} - -Term Solver::mkConst(Kind kind, const std::string& arg1, uint32_t arg2) const +Term Solver::mkAbstractValue(const std::string& index) const { - return mkConstFromStrHelper(kind, arg1, arg2); -} - -/* Split out to avoid nested API calls (problematic with API tracing). */ -template <typename T> -Term Solver::mkConstFromIntHelper(Kind kind, T a) const -{ - CVC4_API_KIND_CHECK_EXPECTED(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL, - kind) - << "ABSTRACT_VALUE or CONST_RATIONAL"; - if (kind == ABSTRACT_VALUE) - { - try - { - return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(a))); - // 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_ARG_CHECK_EXPECTED(!index.empty(), index) << "a non-empty string"; try { - return mkConstHelper<CVC4::Rational>(CVC4::Rational(a)); + 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()); } -} - -Term Solver::mkConst(Kind kind, int32_t arg) const -{ - return mkConstFromIntHelper<int64_t>(kind, static_cast<int64_t>(arg)); -} - -Term Solver::mkConst(Kind kind, int64_t arg) const -{ - return mkConstFromIntHelper<int64_t>(kind, arg); -} - -Term Solver::mkConst(Kind kind, uint32_t arg) const -{ - return mkConstFromIntHelper<uint64_t>(kind, static_cast<uint64_t>(arg)); -} - -Term Solver::mkConst(Kind kind, uint64_t arg) const -{ - return mkConstFromIntHelper<uint64_t>(kind, arg); -} - -Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2) const -{ - CVC4_API_KIND_CHECK_EXPECTED( - kind == CONST_BITVECTOR || kind == CONST_RATIONAL, kind) - << "CONST_BITVECTOR or CONST_RATIONAL"; - if (kind == CONST_BITVECTOR) - { - return mkBVFromIntHelper(arg1, arg2); - } - try - { - return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2)); - } - catch (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } -} - -Term Solver::mkConst(Kind kind, int32_t arg1, int32_t arg2) const -{ - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind) - << "CONST_RATIONAL"; - try - { - return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2)); - } - catch (const std::invalid_argument& e) + catch (const CVC4::TypeCheckingException& e) { - throw CVC4ApiException(e.what()); + throw CVC4ApiException(e.getMessage()); } } -Term Solver::mkConst(Kind kind, int64_t arg1, int64_t arg2) const +Term Solver::mkAbstractValue(uint64_t index) const { - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind) - << "CONST_RATIONAL"; try { - return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2)); + 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()); } -} - -Term Solver::mkConst(Kind kind, uint64_t arg1, uint64_t arg2) const -{ - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind) - << "CONST_RATIONAL"; - try - { - return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2)); - } - catch (const std::invalid_argument& e) + catch (const CVC4::TypeCheckingException& e) { - throw CVC4ApiException(e.what()); + throw CVC4ApiException(e.getMessage()); } } -Term Solver::mkConst(Kind kind, uint32_t arg1, uint64_t arg2) const -{ - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_BITVECTOR, kind) - << "CONST_BITVECTOR"; - return mkBVFromIntHelper(arg1, arg2); -} - -Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const +Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const { CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_FLOATINGPOINT, kind) - << "CONST_FLOATINGPOINT"; - CVC4_API_ARG_CHECK_EXPECTED(arg1 > 0, arg1) << "a value > 0"; - CVC4_API_ARG_CHECK_EXPECTED(arg2 > 0, arg2) << "a value > 0"; - uint32_t bw = arg1 + arg2; - CVC4_API_ARG_CHECK_EXPECTED(bw == arg3.getSort().getBVSize(), arg3) + CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0"; + CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "a value > 0"; + uint32_t bw = exp + sig; + CVC4_API_ARG_CHECK_EXPECTED(bw == val.getSort().getBVSize(), val) << "a bit-vector constant with bit-width '" << bw << "'"; - CVC4_API_ARG_CHECK_EXPECTED(!arg3.isNull(), arg3) << "non-null term"; + CVC4_API_ARG_CHECK_EXPECTED(!val.isNull(), val) << "non-null term"; CVC4_API_ARG_CHECK_EXPECTED( - arg3.getSort().isBitVector() && arg3.d_expr->isConst(), arg3) + val.getSort().isBitVector() && val.d_expr->isConst(), val) << "bit-vector constant"; return mkConstHelper<CVC4::FloatingPoint>( - CVC4::FloatingPoint(arg1, arg2, arg3.d_expr->getConst<BitVector>())); + CVC4::FloatingPoint(exp, sig, val.d_expr->getConst<BitVector>())); } /* Create variables */ |