diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-01-10 10:47:53 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-01-10 10:47:53 -0800 |
commit | 51cb061609e10ff68fb9db053d23ea9dd72ddea2 (patch) | |
tree | 37e66c9a6200f45f90d48ab9d3b305e37f154d68 /src/api | |
parent | fb145effd5bfe67090736969478ff54cf7f62984 (diff) |
New C++ API: Get rid of mkConst functions (simplify API). (#2783)
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 238 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 187 | ||||
-rw-r--r-- | src/api/cvc4cppkind.h | 40 |
3 files changed, 56 insertions, 409 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 */ diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index ef82a9174..1d98f127d 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2088,183 +2088,38 @@ class CVC4_PUBLIC Solver Term mkNegZero(uint32_t exp, uint32_t sig) const; /** - * Create constant of kind: - * - CONST_ROUNDINGMODE + * Create a roundingmode constant. * @param rm the floating point rounding mode this constant represents */ - Term mkConst(RoundingMode rm) const; - - /* - * Create constant of kind: - * - EMPTYSET - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg the argument to this kind - */ - Term mkConst(Kind kind, Sort arg) const; - - /** - * Create constant of kind: - * - UNINTERPRETED_CONSTANT - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg1 the first argument to this kind - * @param arg2 the second argument to this kind - */ - Term mkConst(Kind kind, Sort arg1, int32_t arg2) const; - - /** - * Create constant of kind: - * - BOOLEAN - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg the argument to this kind - */ - Term mkConst(Kind kind, bool arg) const; - - /** - * Create constant of kind: - * - ABSTRACT_VALUE - * - CONST_RATIONAL (for integers, reals) - * - CONST_STRING - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg the argument to this kind - */ - Term mkConst(Kind kind, const char* arg) const; - - /** - * Create constant of kind: - * - ABSTRACT_VALUE - * - CONST_RATIONAL (for integers, reals) - * - CONST_STRING - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg the argument to this kind - */ - Term mkConst(Kind kind, const std::string& arg) const; - - /** - * Create constant of kind: - * - CONST_BITVECTOR - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg1 the first argument to this kind - * @param arg2 the second argument to this kind - */ - Term mkConst(Kind kind, const char* arg1, uint32_t arg2) const; + Term mkRoundingMode(RoundingMode rm) const; /** - * Create constant of kind: - * - CONST_BITVECTOR - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg1 the first argument to this kind - * @param arg2 the second argument to this kind + * Create uninterpreted constant. + * @param arg1 Sort of the constant + * @param arg2 Index of the constant */ - Term mkConst(Kind kind, const std::string& arg1, uint32_t arg2) const; + Term mkUninterpretedConst(Sort sort, int32_t index) const; /** - * Create constant of kind: - * - ABSTRACT_VALUE - * - CONST_RATIONAL (for integers, reals) - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg the argument to this kind + * Create an abstract value constant. + * @param index Index of the abstract value */ - Term mkConst(Kind kind, uint32_t arg) const; + Term mkAbstractValue(const std::string& index) const; /** - * Create constant of kind: - * - ABSTRACT_VALUE - * - CONST_RATIONAL (for integers, reals) - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg the argument to this kind + * Create an abstract value constant. + * @param index Index of the abstract value */ - Term mkConst(Kind kind, int32_t arg) const; + Term mkAbstractValue(uint64_t index) const; /** - * Create constant of kind: - * - ABSTRACT_VALUE - * - CONST_RATIONAL (for integers, reals) - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg the argument to this kind - */ - Term mkConst(Kind kind, int64_t arg) const; - - /** - * Create constant of kind: - * - ABSTRACT_VALUE - * - CONST_RATIONAL (for integers, reals) - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg the argument to this kind - */ - Term mkConst(Kind kind, uint64_t arg) const; - - /** - * Create constant of kind: - * - CONST_RATIONAL (for rationals) - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg1 the first argument to this kind - * @param arg2 the second argument to this kind - */ - Term mkConst(Kind kind, int32_t arg1, int32_t arg2) const; - - /** - * Create constant of kind: - * - CONST_RATIONAL (for rationals) - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg1 the first argument to this kind - * @param arg2 the second argument to this kind - */ - Term mkConst(Kind kind, int64_t arg1, int64_t arg2) const; - - /** - * Create constant of kind: - * - CONST_RATIONAL (for rationals) - * - CONST_BITVECTOR - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg1 the first argument to this kind - * @param arg2 the second argument to this kind - */ - Term mkConst(Kind kind, uint32_t arg1, uint32_t arg2) const; - - /** - * Create constant of kind: - * - CONST_RATIONAL (for rationals) - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg1 the first argument to this kind - * @param arg2 the second argument to this kind - */ - Term mkConst(Kind kind, uint64_t arg1, uint64_t arg2) const; - - /** - * Create constant of kind: - * - CONST_BITVECTOR - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg1 the first argument to this kind - * @param arg2 the second argument to this kind - */ - Term mkConst(Kind kind, uint32_t arg1, uint64_t arg2) const; - - /** - * Create constant of kind: - * - CONST_FLOATINGPOINT (requires CVC4 to be compiled with symFPU support) - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg1 the first argument to this kind - * @param arg2 the second argument to this kind - * @param arg3 the third argument to this kind + * Create a floating-point constant (requires CVC4 to be compiled with symFPU + * support). + * @param exp Size of the exponent + * @param sig Size of the significand + * @param val Value of the floating-point constant as a bit-vector term */ - Term mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const; + Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const; /* .................................................................... */ /* Create Variables */ @@ -2644,12 +2499,6 @@ class CVC4_PUBLIC Solver Term mkBVFromStrHelper(uint32_t size, std::string s, uint32_t base) const; /* Helper for mkBitVector functions that take an integer as argument. */ Term mkBVFromIntHelper(uint32_t size, uint64_t val) const; - /* Helper for mkConst functions that take a string as argument. */ - Term mkConstFromStrHelper(Kind kind, std::string s) const; - Term mkConstFromStrHelper(Kind kind, std::string s, uint32_t a) const; - /* Helper for mkConst functions that take an integer as argument. */ - template <typename T> - Term mkConstFromIntHelper(Kind kind, T a) const; /** * Helper function that ensures that a given term is of sort real (as opposed diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index a940dbefa..a7f6926bb 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -62,7 +62,7 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Sort of the constant * -[2]: Index of the constant * Create with: - * mkConst(Kind, Sort, int32_t) + * mkUninterpretedConst(Sort sort, int32_t index) */ UNINTERPRETED_CONSTANT, /** @@ -70,12 +70,8 @@ enum CVC4_PUBLIC Kind : int32_t * Parameters: 1 * -[1]: Index of the abstract value * Create with: - * mkConst(Kind kind, const char* arg) - * mkConst(Kind kind, const std::string& arg) - * mkConst(Kind kind, uint32_t arg) - * mkConst(Kind kind, int32_t arg) - * mkConst(Kind kind, int64_t arg) - * mkConst(Kind kind, uint64_t arg) + * mkAbstractValue(const std::string& index); + * mkAbstractValue(uint64_t index); */ ABSTRACT_VALUE, #if 0 @@ -204,7 +200,6 @@ enum CVC4_PUBLIC Kind : int32_t * mkTrue() * mkFalse() * mkBoolean(bool val) - * mkConst(Kind kind, bool arg) */ CONST_BOOLEAN, /* Logical not. @@ -568,20 +563,10 @@ enum CVC4_PUBLIC Kind : int32_t * mkReal(int64_t val) * mkReal(uint32_t val) * mkReal(uint64_t val) - * mkRational(int32_t num, int32_t den) - * mkRational(int64_t num, int64_t den) - * mkRational(uint32_t num, uint32_t den) - * mkRational(uint64_t num, uint64_t den) - * mkConst(Kind kind, const char* s, uint32_t base = 10) - * mkConst(Kind kind, const std::string& s, uint32_t base = 10) - * mkConst(Kind kind, uint32_t arg) - * mkConst(Kind kind, int64_t arg) - * mkConst(Kind kind, uint64_t arg) - * mkConst(Kind kind, int32_t arg) - * mkConst(Kind kind, int32_t arg1, int32_t arg2) - * mkConst(Kind kind, int64_t arg1, int64_t arg2) - * mkConst(Kind kind, uint32_t arg1, uint32_t arg2) - * mkConst(Kind kind, uint64_t arg1, uint64_t arg2) + * mkReal(int32_t num, int32_t den) + * mkReal(int64_t num, int64_t den) + * mkReal(uint32_t num, uint32_t den) + * mkReal(uint64_t num, uint64_t den) */ CONST_RATIONAL, /** @@ -661,9 +646,6 @@ enum CVC4_PUBLIC Kind : int32_t * mkBitVector(uint32_t size, uint64_t val) * mkBitVector(const char* s, uint32_t base = 2) * mkBitVector(std::string& s, uint32_t base = 2) - * mkConst(Kind kind, const char* s, uint32_t base = 10) - * mkConst(Kind kind, const std::string& s, uint32_t base = 10) - * mkConst(Kind kind, uint32_t arg1, uint64_t arg2) */ CONST_BITVECTOR, /** @@ -1166,13 +1148,13 @@ enum CVC4_PUBLIC Kind : int32_t * -[2]: Size of the significand * -[3]: Value of the floating-point constant as a bit-vector term * Create with: - * mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) + * mkFloatingPoint(uint32_t sig, uint32_t exp, Term val) */ CONST_FLOATINGPOINT, /** * Floating-point rounding mode term. * Create with: - * mkConst(RoundingMode rm) + * mkRoundingMode(RoundingMode rm) */ CONST_ROUNDINGMODE, /** @@ -1830,7 +1812,6 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Sort of the set elements * Create with: * mkEmptySet(Sort sort) - * mkConst(Sort sort) */ EMPTYSET, /** @@ -1919,7 +1900,6 @@ enum CVC4_PUBLIC Kind : int32_t * All set variables must be interpreted as subsets of it. * Create with: * mkUniverseSet(Sort sort) - * mkConst(Kind kind, Sort sort) */ UNIVERSE_SET, /** @@ -2122,8 +2102,6 @@ enum CVC4_PUBLIC Kind : int32_t * mkString(const std::string& s) * mkString(const unsigned char c) * mkString(const std::vector<unsigned>& s) - * mkConst(Kind kind, const char* s) - * mkConst(Kind kind, const std::string& s) */ CONST_STRING, /** |