diff options
Diffstat (limited to 'src/api/cvc4cpp.h')
-rw-r--r-- | src/api/cvc4cpp.h | 53 |
1 files changed, 53 insertions, 0 deletions
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. |