From: Gereon Kremer Date: Tue, 15 Dec 2020 19:09:54 +0000 (+0100) Subject: Add getters to retrieve constants from api::Term (#5677) X-Git-Tag: cvc5-1.0.0~2445 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aa1b0e19f9ccfc5338a1d056f03b36c0bec6b4b4;p=cvc5.git Add getters to retrieve constants from api::Term (#5677) This PR adds method to obtain constant values from api::Term that are either integers or strings. --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 80fb8a5fb..8044508c7 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2073,6 +2073,106 @@ CVC4::Expr Term::getExpr(void) const // to the new API. !!! const CVC4::Node& Term::getNode(void) const { return *d_node; } +namespace detail { +const Rational& getRational(const CVC4::Node& node) +{ + return node.getConst(); +} +Integer getInteger(const CVC4::Node& node) +{ + return node.getConst().getNumerator(); +} +template +bool checkIntegerBounds(const Integer& i) +{ + return i >= std::numeric_limits::min() + && i <= std::numeric_limits::max(); +} +bool checkReal32Bounds(const Rational& r) +{ + return checkIntegerBounds(r.getNumerator()) + && checkIntegerBounds(r.getDenominator()); +} +bool checkReal64Bounds(const Rational& r) +{ + return checkIntegerBounds(r.getNumerator()) + && checkIntegerBounds(r.getDenominator()); +} + +bool isInteger(const Node& node) +{ + return node.getKind() == CVC4::Kind::CONST_RATIONAL + && node.getConst().isIntegral(); +} +bool isInt32(const Node& node) +{ + return isInteger(node) + && checkIntegerBounds(getInteger(node)); +} +bool isUInt32(const Node& node) +{ + return isInteger(node) + && checkIntegerBounds(getInteger(node)); +} +bool isInt64(const Node& node) +{ + return isInteger(node) + && checkIntegerBounds(getInteger(node)); +} +bool isUInt64(const Node& node) +{ + return isInteger(node) + && checkIntegerBounds(getInteger(node)); +} +} // namespace detail + +bool Term::isInt32() const { return detail::isInt32(*d_node); } +std::int32_t Term::getInt32() const +{ + CVC4_API_CHECK(detail::isInt32(*d_node)) + << "Term should be a Int32 when calling getInt32()"; + return detail::getInteger(*d_node).getSignedInt(); +} +bool Term::isUInt32() const { return detail::isUInt32(*d_node); } +std::uint32_t Term::getUInt32() const +{ + CVC4_API_CHECK(detail::isUInt32(*d_node)) + << "Term should be a UInt32 when calling getUInt32()"; + return detail::getInteger(*d_node).getUnsignedInt(); +} +bool Term::isInt64() const { return detail::isInt64(*d_node); } +std::int64_t Term::getInt64() const +{ + CVC4_API_CHECK(detail::isInt64(*d_node)) + << "Term should be a Int64 when calling getInt64()"; + return detail::getInteger(*d_node).getLong(); +} +bool Term::isUInt64() const { return detail::isUInt64(*d_node); } +std::uint64_t Term::getUInt64() const +{ + CVC4_API_CHECK(detail::isUInt64(*d_node)) + << "Term should be a UInt64 when calling getUInt64()"; + return detail::getInteger(*d_node).getUnsignedLong(); +} +bool Term::isInteger() const { return detail::isInteger(*d_node); } +std::string Term::getInteger() const +{ + CVC4_API_CHECK(detail::isInteger(*d_node)) + << "Term should be an Int when calling getIntString()"; + return detail::getInteger(*d_node).toString(); +} + +bool Term::isString() const +{ + return d_node->getKind() == CVC4::Kind::CONST_STRING; +} +std::wstring Term::getString() const +{ + CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::CONST_STRING) + << "Term should be a String when calling getString()"; + return d_node->getConst().toWString(); +} + std::ostream& operator<<(std::ostream& out, const Term& t) { out << t.toString(); diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index eb55e4007..98752c697 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1151,6 +1151,59 @@ class CVC4_PUBLIC Term // to the new API. !!! const CVC4::Node& getNode(void) const; + /** + * Returns true if the term is an integer that fits within std::int32_t. + */ + bool isInt32() const; + /** + * Returns the stored integer as a std::int32_t. Asserts isInt32(). + */ + std::int32_t getInt32() const; + /** + * Returns true if the term is an integer that fits within std::uint32_t. + */ + bool isUInt32() const; + /** + * Returns the stored integer as a std::uint32_t. Asserts isUInt32(). + */ + std::uint32_t getUInt32() const; + /** + * Returns true if the term is an integer that fits within std::int64_t. + */ + bool isInt64() const; + /** + * Returns the stored integer as a std::int64_t. Asserts isInt64(). + */ + std::int64_t getInt64() const; + /** + * Returns true if the term is an integer that fits within std::uint64_t. + */ + bool isUInt64() const; + /** + * Returns the stored integer as a std::uint64_t. Asserts isUInt64(). + */ + std::uint64_t getUInt64() const; + /** + * Returns true if the term is an integer. + */ + bool isInteger() const; + /** + * Returns the stored integer in (decimal) string representation. Asserts + * isInteger(). + */ + std::string getInteger() const; + + /** + * Returns true if the term is a string constant. + */ + bool isString() const; + /** + * Returns the stored string constant. This method is not to be confused with + * toString() which returns the term in some string representation, whatever + * data it may hold. Asserts isString(). + */ + std::wstring getString() const; + protected: /** * The associated solver object. diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp index fec71b26b..9cc8fb773 100644 --- a/src/util/integer_gmp_imp.cpp +++ b/src/util/integer_gmp_imp.cpp @@ -403,7 +403,7 @@ unsigned int Integer::getUnsignedInt() const this, "Overflow detected in Integer::getUnsignedInt()"); CheckArgument( - fitsSignedInt(), this, "Overflow detected in Integer::getUnsignedInt()"); + fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()"); return (unsigned int)d_value.get_ui(); } diff --git a/src/util/string.cpp b/src/util/string.cpp index 0d40ebb05..e625c2199 100644 --- a/src/util/string.cpp +++ b/src/util/string.cpp @@ -291,6 +291,16 @@ std::string String::toString(bool useEscSequences) const { return str.str(); } +std::wstring String::toWString() const +{ + std::wstring res(size(), static_cast(0)); + for (std::size_t i = 0; i < size(); ++i) + { + res[i] = static_cast(d_str[i]); + } + return res; +} + bool String::isLeq(const String &y) const { for (unsigned i = 0; i < size(); ++i) diff --git a/src/util/string.h b/src/util/string.h index 7102ec1f2..9e503bb07 100644 --- a/src/util/string.h +++ b/src/util/string.h @@ -114,6 +114,13 @@ class CVC4_PUBLIC String { * CVC4::String( s ).toString() = s. */ std::string toString(bool useEscSequences = false) const; + /* toWString + * Converts this string to a std::wstring. + * + * Unlike toString(), this method uses no escape sequences as both this class + * and std::wstring use 32bit characters. + */ + std::wstring toWString() const; /** is this the empty string? */ bool empty() const { return d_str.empty(); } /** is less than or equal to string y */ diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp index f616a1a30..6b032ebd6 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/term_black.cpp @@ -671,6 +671,80 @@ TEST_F(TestApiTermBlack, termChildren) ASSERT_THROW(tnull[0], CVC4ApiException); } +TEST_F(TestApiTermBlack, getInteger) +{ + Term int1 = d_solver.mkInteger("-18446744073709551616"); + Term int2 = d_solver.mkInteger("-18446744073709551615"); + Term int3 = d_solver.mkInteger("-4294967296"); + Term int4 = d_solver.mkInteger("-4294967295"); + Term int5 = d_solver.mkInteger("-10"); + Term int6 = d_solver.mkInteger("0"); + Term int7 = d_solver.mkInteger("10"); + Term int8 = d_solver.mkInteger("4294967295"); + Term int9 = d_solver.mkInteger("4294967296"); + Term int10 = d_solver.mkInteger("18446744073709551615"); + Term int11 = d_solver.mkInteger("18446744073709551616"); + + EXPECT_TRUE(!int1.isInt32() && !int1.isUInt32() && !int1.isInt64() + && !int1.isUInt64() && int1.isInteger()); + EXPECT_EQ(int1.getInteger(), "-18446744073709551616"); + EXPECT_TRUE(!int2.isInt32() && !int2.isUInt32() && !int2.isInt64() + && !int2.isUInt64() && int2.isInteger()); + EXPECT_EQ(int2.getInteger(), "-18446744073709551615"); + EXPECT_TRUE(!int3.isInt32() && !int3.isUInt32() && int3.isInt64() + && !int3.isUInt64() && int3.isInteger()); + EXPECT_EQ(int3.getInt64(), -4294967296); + EXPECT_EQ(int3.getInteger(), "-4294967296"); + EXPECT_TRUE(!int4.isInt32() && !int4.isUInt32() && int4.isInt64() + && !int4.isUInt64() && int4.isInteger()); + EXPECT_EQ(int4.getInt64(), -4294967295); + EXPECT_EQ(int4.getInteger(), "-4294967295"); + EXPECT_TRUE(int5.isInt32() && !int5.isUInt32() && int5.isInt64() + && !int5.isUInt64() && int5.isInteger()); + EXPECT_EQ(int5.getInt32(), -10); + EXPECT_EQ(int5.getInt64(), -10); + EXPECT_EQ(int5.getInteger(), "-10"); + EXPECT_TRUE(int6.isInt32() && int6.isUInt32() && int6.isInt64() + && int6.isUInt64() && int6.isInteger()); + EXPECT_EQ(int6.getInt32(), 0); + EXPECT_EQ(int6.getUInt32(), 0); + EXPECT_EQ(int6.getInt64(), 0); + EXPECT_EQ(int6.getUInt64(), 0); + EXPECT_EQ(int6.getInteger(), "0"); + EXPECT_TRUE(int7.isInt32() && int7.isUInt32() && int7.isInt64() + && int7.isUInt64() && int7.isInteger()); + EXPECT_EQ(int7.getInt32(), 10); + EXPECT_EQ(int7.getUInt32(), 10); + EXPECT_EQ(int7.getInt64(), 10); + EXPECT_EQ(int7.getUInt64(), 10); + EXPECT_EQ(int7.getInteger(), "10"); + EXPECT_TRUE(!int8.isInt32() && int8.isUInt32() && int8.isInt64() + && int8.isUInt64() && int8.isInteger()); + EXPECT_EQ(int8.getUInt32(), 4294967295); + EXPECT_EQ(int8.getInt64(), 4294967295); + EXPECT_EQ(int8.getUInt64(), 4294967295); + EXPECT_EQ(int8.getInteger(), "4294967295"); + EXPECT_TRUE(!int9.isInt32() && !int9.isUInt32() && int9.isInt64() + && int9.isUInt64() && int9.isInteger()); + EXPECT_EQ(int9.getInt64(), 4294967296); + EXPECT_EQ(int9.getUInt64(), 4294967296); + EXPECT_EQ(int9.getInteger(), "4294967296"); + EXPECT_TRUE(!int10.isInt32() && !int10.isUInt32() && !int10.isInt64() + && int10.isUInt64() && int10.isInteger()); + EXPECT_EQ(int10.getUInt64(), 18446744073709551615ull); + EXPECT_EQ(int10.getInteger(), "18446744073709551615"); + EXPECT_TRUE(!int11.isInt32() && !int11.isUInt32() && !int11.isInt64() + && !int11.isUInt64() && int11.isInteger()); + EXPECT_EQ(int11.getInteger(), "18446744073709551616"); +} + +TEST_F(TestApiTermBlack, getString) +{ + Term s1 = d_solver.mkString("abcde"); + EXPECT_TRUE(s1.isString()); + EXPECT_EQ(s1.getString(), L"abcde"); +} + TEST_F(TestApiTermBlack, substitute) { Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");