From a95980ecd80b971086c328c3e1bb731852890a07 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 20 May 2021 04:08:56 +0200 Subject: [PATCH] Add more getters for api::Term (#6496) This PR adds more getter functions for api::Term to retrieve values from constant terms (and terms that the average API use might consider constant). It also introduces std::wstring as regular representation for string constants instead of std::vector for the SMT-LIB parser and the String class. --- src/api/cpp/cvc5.cpp | 530 ++++++++++++++++++++++++++++----- src/api/cpp/cvc5.h | 266 +++++++++++++---- src/api/python/cvc5.pxd | 8 +- src/api/python/cvc5.pxi | 29 +- src/parser/parser.cpp | 43 +-- src/parser/parser.h | 10 +- src/parser/smt2/Smt2.g | 2 +- src/parser/smt2/smt2.cpp | 4 +- src/smt/command.cpp | 4 +- src/util/string.cpp | 9 + src/util/string.h | 1 + test/unit/api/solver_black.cpp | 10 - test/unit/api/term_black.cpp | 360 ++++++++++++++++++---- 13 files changed, 1035 insertions(+), 241 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 066ea0082..d7959c950 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -2309,20 +2309,6 @@ bool Term::isNull() const CVC5_API_TRY_CATCH_END; } -Term Term::getConstArrayBase() const -{ - NodeManagerScope scope(d_solver->getNodeManager()); - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK_NOT_NULL; - // CONST_ARRAY kind maps to STORE_ALL internal kind - CVC5_API_CHECK(d_node->getKind() == cvc5::Kind::STORE_ALL) - << "Expecting a CONST_ARRAY Term when calling getConstArrayBase()"; - //////// all checks before this line - return Term(d_solver, d_node->getConst().getValue()); - //////// - CVC5_API_TRY_CATCH_END; -} - std::vector Term::getConstSequenceElements() const { CVC5_API_TRY_CATCH_BEGIN; @@ -2559,7 +2545,14 @@ const cvc5::Node& Term::getNode(void) const { return *d_node; } namespace detail { const Rational& getRational(const cvc5::Node& node) { - return node.getConst(); + switch (node.getKind()) + { + case cvc5::Kind::CAST_TO_REAL: return node[0].getConst(); + case cvc5::Kind::CONST_RATIONAL: return node.getConst(); + default: + CVC5_API_CHECK(false) << "Node is not a rational."; + return node.getConst(); + } } Integer getInteger(const cvc5::Node& node) { @@ -2582,6 +2575,20 @@ bool checkReal64Bounds(const Rational& r) && checkIntegerBounds(r.getDenominator()); } +bool isReal(const Node& node) +{ + return node.getKind() == cvc5::Kind::CONST_RATIONAL + || node.getKind() == cvc5::Kind::CAST_TO_REAL; +} +bool isReal32(const Node& node) +{ + return isReal(node) && checkReal32Bounds(getRational(node)); +} +bool isReal64(const Node& node) +{ + return isReal(node) && checkReal64Bounds(getRational(node)); +} + bool isInteger(const Node& node) { return node.getKind() == cvc5::Kind::CONST_RATIONAL @@ -2605,7 +2612,7 @@ bool isUInt64(const Node& node) } } // namespace detail -bool Term::isInt32() const +bool Term::isInt32Value() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -2615,45 +2622,62 @@ bool Term::isInt32() const CVC5_API_TRY_CATCH_END; } -std::int32_t Term::getInt32() const +std::int32_t Term::getInt32Value() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(detail::isInt32(*d_node)) - << "Term should be a Int32 when calling getInt32()"; + CVC5_API_ARG_CHECK_EXPECTED(detail::isInt32(*d_node), *d_node) + << "Term to be a 32-bit integer value when calling getInt32Value()"; //////// all checks before this line return detail::getInteger(*d_node).getSignedInt(); //////// CVC5_API_TRY_CATCH_END; } -bool Term::isUInt32() const { return detail::isUInt32(*d_node); } -std::uint32_t Term::getUInt32() const +bool Term::isUInt32Value() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return detail::isUInt32(*d_node); + //////// + CVC5_API_TRY_CATCH_END; +} +std::uint32_t Term::getUInt32Value() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(detail::isUInt32(*d_node)) - << "Term should be a UInt32 when calling getUInt32()"; + CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt32(*d_node), *d_node) + << "Term to be a unsigned 32-bit integer value when calling " + "getUInt32Value()"; //////// all checks before this line return detail::getInteger(*d_node).getUnsignedInt(); //////// CVC5_API_TRY_CATCH_END; } -bool Term::isInt64() const { return detail::isInt64(*d_node); } -std::int64_t Term::getInt64() const +bool Term::isInt64Value() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(detail::isInt64(*d_node)) - << "Term should be a Int64 when calling getInt64()"; + //////// all checks before this line + return detail::isInt64(*d_node); + //////// + CVC5_API_TRY_CATCH_END; +} +std::int64_t Term::getInt64Value() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_ARG_CHECK_EXPECTED(detail::isInt64(*d_node), *d_node) + << "Term to be a 64-bit integer value when calling getInt64Value()"; //////// all checks before this line return detail::getInteger(*d_node).getLong(); //////// CVC5_API_TRY_CATCH_END; } -bool Term::isUInt64() const +bool Term::isUInt64Value() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -2663,32 +2687,41 @@ bool Term::isUInt64() const CVC5_API_TRY_CATCH_END; } -std::uint64_t Term::getUInt64() const +std::uint64_t Term::getUInt64Value() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(detail::isUInt64(*d_node)) - << "Term should be a UInt64 when calling getUInt64()"; + CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt64(*d_node), *d_node) + << "Term to be a unsigned 64-bit integer value when calling " + "getUInt64Value()"; //////// all checks before this line return detail::getInteger(*d_node).getUnsignedLong(); //////// CVC5_API_TRY_CATCH_END; } -bool Term::isInteger() const { return detail::isInteger(*d_node); } -std::string Term::getInteger() const +bool Term::isIntegerValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return detail::isInteger(*d_node); + //////// + CVC5_API_TRY_CATCH_END; +} +std::string Term::getIntegerValue() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(detail::isInteger(*d_node)) - << "Term should be an Int when calling getIntString()"; + CVC5_API_ARG_CHECK_EXPECTED(detail::isInteger(*d_node), *d_node) + << "Term to be an integer value when calling getIntegerValue()"; //////// all checks before this line return detail::getInteger(*d_node).toString(); //////// CVC5_API_TRY_CATCH_END; } -bool Term::isString() const +bool Term::isStringValue() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -2698,12 +2731,13 @@ bool Term::isString() const CVC5_API_TRY_CATCH_END; } -std::wstring Term::getString() const +std::wstring Term::getStringValue() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(d_node->getKind() == cvc5::Kind::CONST_STRING) - << "Term should be a String when calling getString()"; + CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::CONST_STRING, + *d_node) + << "Term to be a string value when calling getStringValue()"; //////// all checks before this line return d_node->getConst().toWString(); //////// @@ -2720,6 +2754,387 @@ std::vector Term::termVectorToNodes(const std::vector& terms) return res; } +bool Term::isReal32Value() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return detail::isReal32(*d_node); + //////// + CVC5_API_TRY_CATCH_END; +} +std::pair Term::getReal32Value() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_ARG_CHECK_EXPECTED(detail::isReal32(*d_node), *d_node) + << "Term to be a 32-bit rational value when calling getReal32Value()"; + //////// all checks before this line + const Rational& r = detail::getRational(*d_node); + return std::make_pair(r.getNumerator().getSignedInt(), + r.getDenominator().getUnsignedInt()); + //////// + CVC5_API_TRY_CATCH_END; +} +bool Term::isReal64Value() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return detail::isReal64(*d_node); + //////// + CVC5_API_TRY_CATCH_END; +} +std::pair Term::getReal64Value() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_ARG_CHECK_EXPECTED(detail::isReal64(*d_node), *d_node) + << "Term to be a 64-bit rational value when calling getReal64Value()"; + //////// all checks before this line + const Rational& r = detail::getRational(*d_node); + return std::make_pair(r.getNumerator().getLong(), + r.getDenominator().getUnsignedLong()); + //////// + CVC5_API_TRY_CATCH_END; +} +bool Term::isRealValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return detail::isReal(*d_node); + //////// + CVC5_API_TRY_CATCH_END; +} +std::string Term::getRealValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_ARG_CHECK_EXPECTED(detail::isReal(*d_node), *d_node) + << "Term to be a rational value when calling getRealValue()"; + //////// all checks before this line + return detail::getRational(*d_node).toString(); + //////// + CVC5_API_TRY_CATCH_END; +} + +bool Term::isConstArray() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_node->getKind() == cvc5::Kind::STORE_ALL; + //////// + CVC5_API_TRY_CATCH_END; +} +Term Term::getConstArrayBase() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::STORE_ALL, + *d_node) + << "Term to be a constant array when calling getConstArrayBase()"; + //////// all checks before this line + const auto& ar = d_node->getConst(); + return Term(d_solver, ar.getValue()); + //////// + CVC5_API_TRY_CATCH_END; +} + +bool Term::isBooleanValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_node->getKind() == cvc5::Kind::CONST_BOOLEAN; + //////// + CVC5_API_TRY_CATCH_END; +} +bool Term::getBooleanValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::CONST_BOOLEAN, + *d_node) + << "Term to be a Boolean value when calling getBooleanValue()"; + //////// all checks before this line + return d_node->getConst(); + //////// + CVC5_API_TRY_CATCH_END; +} + +bool Term::isBitVectorValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_node->getKind() == cvc5::Kind::CONST_BITVECTOR; + //////// + CVC5_API_TRY_CATCH_END; +} +std::string Term::getBitVectorValue(std::uint32_t base) const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::CONST_BITVECTOR, + *d_node) + << "Term to be a bit-vector value when calling getBitVectorValue()"; + //////// all checks before this line + return d_node->getConst().toString(base); + //////// + CVC5_API_TRY_CATCH_END; +} + +bool Term::isAbstractValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_node->getKind() == cvc5::Kind::ABSTRACT_VALUE; + //////// + CVC5_API_TRY_CATCH_END; +} +std::string Term::getAbstractValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::ABSTRACT_VALUE, + *d_node) + << "Term to be an abstract value when calling " + "getAbstractValue()"; + //////// all checks before this line + return d_node->getConst().getIndex().toString(); + //////// + CVC5_API_TRY_CATCH_END; +} + +bool Term::isTupleValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_node->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR && d_node->isConst() + && d_node->getType().getDType().isTuple(); + //////// + CVC5_API_TRY_CATCH_END; +} +std::vector Term::getTupleValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR + && d_node->isConst() + && d_node->getType().getDType().isTuple(), + *d_node) + << "Term to be a tuple value when calling getTupleValue()"; + //////// all checks before this line + std::vector res; + for (size_t i = 0, n = d_node->getNumChildren(); i < n; ++i) + { + res.emplace_back(Term(d_solver, (*d_node)[i])); + } + return res; + //////// + CVC5_API_TRY_CATCH_END; +} + +bool Term::isFloatingPointPosZero() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + if (d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT) + { + const auto& fp = d_node->getConst(); + return fp.isZero() && fp.isPositive(); + } + return false; + //////// + CVC5_API_TRY_CATCH_END; +} +bool Term::isFloatingPointNegZero() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + if (d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT) + { + const auto& fp = d_node->getConst(); + return fp.isZero() && fp.isNegative(); + } + return false; + //////// + CVC5_API_TRY_CATCH_END; +} +bool Term::isFloatingPointPosInf() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + if (d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT) + { + const auto& fp = d_node->getConst(); + return fp.isInfinite() && fp.isPositive(); + } + return false; + //////// + CVC5_API_TRY_CATCH_END; +} +bool Term::isFloatingPointNegInf() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + if (d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT) + { + const auto& fp = d_node->getConst(); + return fp.isInfinite() && fp.isNegative(); + } + return false; + //////// + CVC5_API_TRY_CATCH_END; +} +bool Term::isFloatingPointNaN() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT + && d_node->getConst().isNaN(); + //////// + CVC5_API_TRY_CATCH_END; +} +bool Term::isFloatingPointValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT; + //////// + CVC5_API_TRY_CATCH_END; +} +std::tuple Term::getFloatingPointValue() + const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_ARG_CHECK_EXPECTED( + d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT, *d_node) + << "Term to be a floating-point value when calling " + "getFloatingPointValue()"; + //////// all checks before this line + const auto& fp = d_node->getConst(); + return std::make_tuple(fp.getSize().exponentWidth(), + fp.getSize().significandWidth(), + d_solver->mkValHelper(fp.pack())); + //////// + CVC5_API_TRY_CATCH_END; +} + +bool Term::isSetValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_node->getType().isSet() && d_node->isConst(); + //////// + CVC5_API_TRY_CATCH_END; +} + +void Term::collectSet(std::set& set, + const cvc5::Node& node, + const Solver* slv) +{ + // We asserted that node has a set type, and node.isConst() + // Thus, node only contains of EMPTYSET, UNION and SINGLETON. + switch (node.getKind()) + { + case cvc5::Kind::EMPTYSET: break; + case cvc5::Kind::SINGLETON: set.emplace(Term(slv, node[0])); break; + case cvc5::Kind::UNION: + { + for (const auto& sub : node) + { + collectSet(set, sub, slv); + } + break; + } + default: + CVC5_API_ARG_CHECK_EXPECTED(false, node) + << "Term to be a set value when calling getSetValue()"; + break; + } +} + +std::set Term::getSetValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_ARG_CHECK_EXPECTED(d_node->getType().isSet() && d_node->isConst(), + *d_node) + << "Term to be a set value when calling getSetValue()"; + //////// all checks before this line + std::set res; + Term::collectSet(res, *d_node, d_solver); + return res; + //////// + CVC5_API_TRY_CATCH_END; +} + +bool Term::isSequenceValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_node->getKind() == cvc5::Kind::CONST_SEQUENCE; + //////// + CVC5_API_TRY_CATCH_END; +} +std::vector Term::getSequenceValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::CONST_SEQUENCE, + *d_node) + << "Term to be a sequence value when calling getSequenceValue()"; + //////// all checks before this line + std::vector res; + const Sequence& seq = d_node->getConst(); + for (const auto& node: seq.getVec()) + { + res.emplace_back(Term(d_solver, node)); + } + return res; + //////// + CVC5_API_TRY_CATCH_END; +} + +bool Term::isUninterpretedValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_node->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT; + //////// + CVC5_API_TRY_CATCH_END; +} +std::pair Term::getUninterpretedValue() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_ARG_CHECK_EXPECTED( + d_node->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT, *d_node) + << "Term to be an uninterpreted value when calling " + "getUninterpretedValue()"; + //////// all checks before this line + const auto& uc = d_node->getConst(); + return std::make_pair(Sort(d_solver, uc.getType()), + uc.getIndex().toUnsignedInt()); + //////// + CVC5_API_TRY_CATCH_END; +} + std::ostream& operator<<(std::ostream& out, const Term& t) { out << t.toString(); @@ -4445,21 +4860,6 @@ Term Solver::mkBVFromStrHelper(uint32_t size, return mkValHelper(cvc5::BitVector(size, val)); } -Term Solver::mkCharFromStrHelper(const std::string& s) const -{ - CVC5_API_CHECK(s.find_first_not_of("0123456789abcdefABCDEF", 0) - == std::string::npos - && s.size() <= 5 && s.size() > 0) - << "Unexpected string for hexadecimal character " << s; - uint32_t val = static_cast(std::stoul(s, 0, 16)); - CVC5_API_CHECK(val < String::num_codes()) - << "Not a valid code point for hexadecimal character " << s; - //////// all checks before this line - std::vector cpts; - cpts.push_back(val); - return mkValHelper(cvc5::String(cpts)); -} - Term Solver::getValueHelper(const Term& term) const { // Note: Term is checked in the caller to avoid double checks @@ -5296,17 +5696,7 @@ Term Solver::mkString(const std::string& s, bool useEscSequences) const CVC5_API_TRY_CATCH_END; } -Term Solver::mkString(const unsigned char c) const -{ - NodeManagerScope scope(getNodeManager()); - CVC5_API_TRY_CATCH_BEGIN; - //////// all checks before this line - return mkValHelper(cvc5::String(std::string(1, c))); - //////// - CVC5_API_TRY_CATCH_END; -} - -Term Solver::mkString(const std::vector& s) const +Term Solver::mkString(const std::wstring& s) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; @@ -5316,16 +5706,6 @@ Term Solver::mkString(const std::vector& s) const CVC5_API_TRY_CATCH_END; } -Term Solver::mkChar(const std::string& s) const -{ - NodeManagerScope scope(getNodeManager()); - CVC5_API_TRY_CATCH_BEGIN; - //////// all checks before this line - return mkCharFromStrHelper(s); - //////// - CVC5_API_TRY_CATCH_END; -} - Term Solver::mkEmptySequence(const Sort& sort) const { NodeManagerScope scope(getNodeManager()); diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 16f58ee80..42d162e18 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -1053,13 +1053,6 @@ class CVC5_EXPORT Term */ bool isNull() const; - /** - * Return the base (element stored at all indices) of a constant array - * throws an exception if the kind is not CONST_ARRAY - * @return the base value - */ - Term getConstArrayBase() const; - /** * Return the elements of a constant sequence * throws an exception if the kind is not CONST_SEQUENCE @@ -1213,63 +1206,215 @@ class CVC5_EXPORT Term const_iterator end() const; /** - * @return true if the term is an integer that fits within std::int32_t. + * @return true if the term is an integer value that fits within int32_t. */ - bool isInt32() const; + bool isInt32Value() const; /** - * @return the stored integer as a std::int32_t. - * Note: Asserts isInt32(). + * Asserts isInt32Value(). + * @return the integer term as a int32_t. */ - std::int32_t getInt32() const; + int32_t getInt32Value() const; /** - * @return true if the term is an integer that fits within std::uint32_t. + * @return true if the term is an integer value that fits within uint32_t. */ - bool isUInt32() const; + bool isUInt32Value() const; /** - * @return the stored integer as a std::uint32_t. - * Note: Asserts isUInt32(). + * Asserts isUInt32Value(). + * @return the integer term as a uint32_t. */ - std::uint32_t getUInt32() const; + uint32_t getUInt32Value() const; /** - * @return true if the term is an integer that fits within std::int64_t. + * @return true if the term is an integer value that fits within int64_t. */ - bool isInt64() const; + bool isInt64Value() const; /** - * @return the stored integer as a std::int64_t. - * Note: Asserts isInt64(). + * Asserts isInt64Value(). + * @return the integer term as a int64_t. */ - std::int64_t getInt64() const; + int64_t getInt64Value() const; /** - * @return true if the term is an integer that fits within std::uint64_t. + * @return true if the term is an integer value that fits within uint64_t. */ - bool isUInt64() const; + bool isUInt64Value() const; /** - * @return the stored integer as a std::uint64_t. - * Note: Asserts isUInt64(). + * Asserts isUInt64Value(). + * @return the integer term as a uint64_t. */ - std::uint64_t getUInt64() const; + uint64_t getUInt64Value() const; /** - * @return true if the term is an integer. + * @return true if the term is an integer value. */ - bool isInteger() const; + bool isIntegerValue() const; /** - * @return the stored integer in (decimal) string representation. - * Note: Asserts isInteger(). + * Asserts isIntegerValue(). + * @return the integer term in (decimal) string representation. */ - std::string getInteger() const; + std::string getIntegerValue() const; /** - * @return true if the term is a string constant. + * @return true if the term is a string value. */ - bool isString() const; + bool isStringValue() const; /** - * @return the stored string constant. - * - * Note: This method is not to be confused with toString() which returns the - * term in some string representation, whatever data it may hold. - * Asserts isString(). + * Note: This method is not to be confused with toString() which returns + * the term in some string representation, whatever data it may hold. Asserts + * isStringValue(). + * @return the string term as a native string value. + */ + std::wstring getStringValue() const; + + /** + * @return true if the term is a rational value whose numerator and + * denominator fit within int32_t and uint32_t, respectively. + */ + bool isReal32Value() const; + /** + * Asserts isReal32Value(). + * @return the representation of a rational value as a pair of its numerator + * and denominator. + */ + std::pair getReal32Value() const; + /** + * @return true if the term is a rational value whose numerator and + * denominator fit within int64_t and uint64_t, respectively. */ - std::wstring getString() const; + bool isReal64Value() const; + /** + * Asserts isReal64Value(). + * @return the representation of a rational value as a pair of its numerator + * and denominator. + */ + std::pair getReal64Value() const; + /** + * @return true if the term is a rational value. + */ + bool isRealValue() const; + /** + * Asserts isRealValue(). + * @return the representation of a rational value as a (decimal) string. + */ + std::string getRealValue() const; + + /** + * @return true if the term is a constant array. + */ + bool isConstArray() const; + /** + * Asserts isConstArray(). + * @return the base (element stored at all indices) of a constant array + */ + Term getConstArrayBase() const; + + /** + * @return true if the term is a Boolean value. + */ + bool isBooleanValue() const; + /** + * Asserts isBooleanValue(). + * @return the representation of a Boolean value as a native Boolean value. + */ + bool getBooleanValue() const; + + /** + * @return true if the term is a bit-vector value. + */ + bool isBitVectorValue() const; + /** + * Asserts isBitVectorValue(). + * @return the representation of a bit-vector value in string representation. + * Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexadecimal + * string). + */ + std::string getBitVectorValue(uint32_t base = 2) const; + + /** + * @return true if the term is an abstract value. + */ + bool isAbstractValue() const; + /** + * Asserts isAbstractValue(). + * @return the representation of an abstract value as a string. + */ + std::string getAbstractValue() const; + + /** + * @return true if the term is a tuple value. + */ + bool isTupleValue() const; + /** + * Asserts isTupleValue(). + * @return the representation of a tuple value as a vector of terms. + */ + std::vector getTupleValue() const; + + /** + * @return true if the term is the floating-point value for positive zero. + */ + bool isFloatingPointPosZero() const; + /** + * @return true if the term is the floating-point value for negative zero. + */ + bool isFloatingPointNegZero() const; + /** + * @return true if the term is the floating-point value for positive + * infinity. + */ + bool isFloatingPointPosInf() const; + /** + * @return true if the term is the floating-point value for negative + * infinity. + */ + bool isFloatingPointNegInf() const; + /** + * @return true if the term is the floating-point value for not a number. + */ + bool isFloatingPointNaN() const; + /** + * @return true if the term is a floating-point value. + */ + bool isFloatingPointValue() const; + /** + * Asserts isFloatingPointValue(). + * @return the representation of a floating-point value as a tuple of the + * exponent width, the significand width and a bit-vector value. + */ + std::tuple getFloatingPointValue() const; + + /** + * @return true if the term is a set value. + */ + bool isSetValue() const; + /** + * Asserts isSetValue(). + * @return the representation of a set value as a set of terms. + */ + std::set getSetValue() const; + + /** + * @return true if the term is a sequence value. + */ + bool isSequenceValue() const; + /** + * Asserts isSequenceValue(). + * Note that it is usually necessary for sequences to call + * `Solver::simplify()` to turn a sequence that is constructed by, e.g., + * concatenation of unit sequences, into a sequence value. + * @return the representation of a sequence value as a vector of terms. + */ + std::vector getSequenceValue() const; + + /** + * @return true if the term is a value from an uninterpreted sort. + */ + bool isUninterpretedValue() const; + /** + bool @return() const; + * Asserts isUninterpretedValue(). + * @return the representation of an uninterpreted value as a pair of its + sort and its + * index. + */ + std::pair getUninterpretedValue() const; protected: /** @@ -1281,6 +1426,15 @@ class CVC5_EXPORT Term /** Helper to convert a vector of Terms to internal Nodes. */ std::vector static termVectorToNodes(const std::vector& terms); + /** Helper method to collect all elements of a set. */ + static void collectSet(std::set& set, + const cvc5::Node& node, + const Solver* slv); + /** Helper method to collect all elements of a sequence. */ + static void collectSequence(std::vector& seq, + const cvc5::Node& node, + const Solver* slv); + /** * Constructor. * @param slv the associated solver object @@ -3070,35 +3224,23 @@ class CVC5_EXPORT Solver Term mkSepNil(const Sort& sort) const; /** - * Create a String constant. + * Create a String constant from a `std::string` which may contain SMT-LIB + * compatible escape sequences like `\u1234` to encode unicode characters. * @param s the string this constant represents - * @param useEscSequences determines whether escape sequences in \p s should - * be converted to the corresponding character + * @param useEscSequences determines whether escape sequences in `s` should + * be converted to the corresponding unicode character * @return the String constant */ Term mkString(const std::string& s, bool useEscSequences = false) const; /** - * Create a String constant. - * @param c the character this constant represents - * @return the String constant - */ - Term mkString(const unsigned char c) const; - - /** - * Create a String constant. - * @param s a list of unsigned (unicode) values this constant represents as - * string + * Create a String constant from a `std::wstring`. + * This method does not support escape sequences as `std::wstring` already + * supports unicode characters. + * @param s the string this constant represents * @return the String constant */ - Term mkString(const std::vector& s) const; - - /** - * Create a character constant from a given string. - * @param s the string denoting the code point of the character (in base 16) - * @return the character constant - */ - Term mkChar(const std::string& s) const; + Term mkString(const std::wstring& s) const; /** * Create an empty sequence of the given element sort. @@ -3216,12 +3358,14 @@ class CVC5_EXPORT Solver /** * Create an abstract value constant. + * The given index needs to be a positive integer in base 10. * @param index Index of the abstract value */ Term mkAbstractValue(const std::string& index) const; /** * Create an abstract value constant. + * The given index needs to be positive. * @param index Index of the abstract value */ Term mkAbstractValue(uint64_t index) const; diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index a044c79f5..24f8ac0a0 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -1,6 +1,7 @@ # import dereference and increment operators from cython.operator cimport dereference as deref, preincrement as inc from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t +from libc.stddef cimport wchar_t from libcpp.set cimport set from libcpp.string cimport string from libcpp.vector cimport vector @@ -19,6 +20,9 @@ cdef extern from "" namespace "std" nogil: hash() size_t operator()(T t) +cdef extern from "" namespace "std": + cdef cppclass wstring: + wstring(const wchar_t*, size_t) except + cdef extern from "api/cpp/cvc5.h" namespace "cvc5": cdef cppclass Options: @@ -191,7 +195,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term mkEmptySet(Sort s) except + Term mkSepNil(Sort sort) except + Term mkString(const string& s) except + - Term mkString(const vector[unsigned]& s) except + + Term mkString(const wstring& s) except + Term mkEmptySequence(Sort sort) except + Term mkUniverseSet(Sort sort) except + Term mkBitVector(uint32_t size) except + @@ -372,7 +376,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term operator*() except + const_iterator begin() except + const_iterator end() except + - bint isInteger() except + + bint isIntegerValue() except + cdef cppclass TermHashFunction: TermHashFunction() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index a512a17a8..6d197168d 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -3,6 +3,7 @@ from fractions import Fraction import sys from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t +from libc.stddef cimport wchar_t from libcpp.pair cimport pair from libcpp.set cimport set @@ -26,9 +27,14 @@ from cvc5 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY from cvc5 cimport Term as c_Term from cvc5 cimport hash as c_hash +from cvc5 cimport wstring as c_wstring from cvc5kinds cimport Kind as c_Kind +cdef extern from "Python.h": + wchar_t* PyUnicode_AsWideCharString(object, Py_ssize_t *) + void PyMem_Free(void*) + ################################## DECORATORS ################################# def expand_list_arg(num_req_args=0): ''' @@ -735,23 +741,12 @@ cdef class Solver: term.cterm = self.csolver.mkSepNil(sort.csort) return term - def mkString(self, str_or_vec): + def mkString(self, str s): cdef Term term = Term(self) - cdef vector[unsigned] v - if isinstance(str_or_vec, str): - for u in str_or_vec: - v.push_back( ord(u)) - term.cterm = self.csolver.mkString( v) - elif isinstance(str_or_vec, list): - for u in str_or_vec: - if not isinstance(u, int): - raise ValueError("List should contain ints but got: {}" - .format(str_or_vec)) - v.push_back( u) - term.cterm = self.csolver.mkString( v) - else: - raise ValueError("Expected string or vector of ASCII codes" - " but got: {}".format(str_or_vec)) + cdef Py_ssize_t size + cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size) + term.cterm = self.csolver.mkString(c_wstring(tmp, size)) + PyMem_Free(tmp) return term def mkEmptySequence(self, Sort sort): @@ -1599,7 +1594,7 @@ cdef class Term: return term def isInteger(self): - return self.cterm.isInteger() + return self.cterm.isIntegerValue() def toPythonObj(self): ''' diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index f3a0d5c83..d57ec0c9a 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -741,7 +741,7 @@ void Parser::reset() {} SymbolManager* Parser::getSymbolManager() { return d_symman; } -std::vector Parser::processAdHocStringEsc(const std::string& s) +std::wstring Parser::processAdHocStringEsc(const std::string& s) { std::wstring ws; { @@ -763,7 +763,7 @@ std::vector Parser::processAdHocStringEsc(const std::string& s) } } - std::vector str; + std::wstring res; unsigned i = 0; while (i < ws.size()) { @@ -771,7 +771,7 @@ std::vector Parser::processAdHocStringEsc(const std::string& s) if (ws[i] != '\\') { // don't worry about printable here - str.push_back(static_cast(ws[i])); + res.push_back(ws[i]); ++i; continue; } @@ -789,49 +789,49 @@ std::vector Parser::processAdHocStringEsc(const std::string& s) { case 'n': { - str.push_back(static_cast('\n')); + res.push_back('\n'); i++; } break; case 't': { - str.push_back(static_cast('\t')); + res.push_back('\t'); i++; } break; case 'v': { - str.push_back(static_cast('\v')); + res.push_back('\v'); i++; } break; case 'b': { - str.push_back(static_cast('\b')); + res.push_back('\b'); i++; } break; case 'r': { - str.push_back(static_cast('\r')); + res.push_back('\r'); i++; } break; case 'f': { - str.push_back(static_cast('\f')); + res.push_back('\f'); i++; } break; case 'a': { - str.push_back(static_cast('\a')); + res.push_back('\a'); i++; } break; case '\\': { - str.push_back(static_cast('\\')); + res.push_back('\\'); i++; } break; @@ -846,7 +846,7 @@ std::vector Parser::processAdHocStringEsc(const std::string& s) shex << ws[i + 1] << ws[i + 2]; unsigned val; shex >> std::hex >> val; - str.push_back(val); + res.push_back(val); i += 3; isValid = true; } @@ -875,25 +875,25 @@ std::vector Parser::processAdHocStringEsc(const std::string& s) && ws[i + 2] < '8') { num = num * 8 + static_cast(ws[i + 2]) - 48; - str.push_back(num); + res.push_back(num); i += 3; } else { - str.push_back(num); + res.push_back(num); i += 2; } } else { - str.push_back(num); + res.push_back(num); i++; } } } } } - return str; + return res; } api::Term Parser::mkStringConstant(const std::string& s) @@ -903,9 +903,18 @@ api::Term Parser::mkStringConstant(const std::string& s) return d_solver->mkString(s, true); } // otherwise, we must process ad-hoc escape sequences - std::vector str = processAdHocStringEsc(s); + std::wstring str = processAdHocStringEsc(s); return d_solver->mkString(str); } +api::Term Parser::mkCharConstant(const std::string& s) +{ + Assert(s.find_first_not_of("0123456789abcdefABCDEF", 0) == std::string::npos + && s.size() <= 5 && s.size() > 0) + << "Unexpected string for hexadecimal character " << s; + wchar_t val = static_cast(std::stoul(s, 0, 16)); + return d_solver->mkString(std::wstring(1, val)); +} + } // namespace parser } // namespace cvc5 diff --git a/src/parser/parser.h b/src/parser/parser.h index b127221d7..8add1c698 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -757,6 +757,14 @@ public: */ api::Term mkStringConstant(const std::string& s); + /** + * Make string constant from a single character in hex representation + * + * This makes the string constant based on the character from the strings, + * represented as a hexadecimal code point. + */ + api::Term mkCharConstant(const std::string& s); + /** ad-hoc string escaping * * Returns the (internal) vector of code points corresponding to processing @@ -767,7 +775,7 @@ public: * \\, \x[N] and octal escape sequences of the form \[c1]([c2]([c3])?)? where * c1, c2, c3 are digits from 0 to 7. */ - std::vector processAdHocStringEsc(const std::string& s); + std::wstring processAdHocStringEsc(const std::string& s); }; /* class Parser */ } // namespace parser diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 58f229cfe..483da3ff0 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1726,7 +1726,7 @@ termAtomic[cvc5::api::Term& atomTerm] | CHAR_TOK HEX_LITERAL { std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); - atomTerm = SOLVER->mkChar(hexStr); + atomTerm = PARSER_STATE->mkCharConstant(hexStr); } | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals] { diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 7893dd333..c22b95af2 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1046,11 +1046,11 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) else if (p.d_kind == api::APPLY_SELECTOR && !p.d_expr.isNull()) { // tuple selector case - if (!p.d_expr.isUInt64()) + if (!p.d_expr.isUInt64Value()) { parseError("index of tupSel is larger than size of uint64_t"); } - uint64_t n = p.d_expr.getUInt64(); + uint64_t n = p.d_expr.getUInt64Value(); if (args.size() != 1) { parseError("tupSel should only be applied to one tuple argument"); diff --git a/src/smt/command.cpp b/src/smt/command.cpp index e49658c9d..e4e8aff1a 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -51,10 +51,10 @@ std::string sexprToString(api::Term sexpr) // call Term::toString as its result depends on the output language. // Notice that we only check for string constants. The sexprs generated by the // parser don't contains other constants, so we can ignore them. - if (sexpr.isString()) + if (sexpr.isStringValue()) { // convert std::wstring to std::string - std::wstring wstring = sexpr.getString(); + std::wstring wstring = sexpr.getStringValue(); return std::string(wstring.cbegin(), wstring.cend()); } diff --git a/src/util/string.cpp b/src/util/string.cpp index 5f2bd5b83..50b0a7199 100644 --- a/src/util/string.cpp +++ b/src/util/string.cpp @@ -30,6 +30,15 @@ namespace cvc5 { static_assert(UCHAR_MAX == 255, "Unsigned char is assumed to have 256 values."); +String::String(const std::wstring& s) +{ + d_str.resize(s.size()); + for (size_t i = 0, n = s.size(); i < n; ++i) + { + d_str[i] = static_cast(s[i]); + } +} + String::String(const std::vector &s) : d_str(s) { #ifdef CVC5_ASSERTIONS diff --git a/src/util/string.h b/src/util/string.h index 6e9bb2866..3f6384082 100644 --- a/src/util/string.h +++ b/src/util/string.h @@ -69,6 +69,7 @@ class String : d_str(toInternal(s, useEscSequences)) { } + explicit String(const std::wstring& s); explicit String(const char* s, bool useEscSequences = false) : d_str(toInternal(std::string(s), useEscSequences)) { diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index f7e6a3783..bc8f3ed74 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -684,16 +684,6 @@ TEST_F(TestApiBlackSolver, mkString) "\"asdf\\u{5c}nasdf\""); } -TEST_F(TestApiBlackSolver, mkChar) -{ - ASSERT_NO_THROW(d_solver.mkChar(std::string("0123"))); - ASSERT_NO_THROW(d_solver.mkChar("aA")); - ASSERT_THROW(d_solver.mkChar(""), CVC5ApiException); - ASSERT_THROW(d_solver.mkChar("0g0"), CVC5ApiException); - ASSERT_THROW(d_solver.mkChar("100000"), CVC5ApiException); - ASSERT_EQ(d_solver.mkChar("abc"), d_solver.mkChar("ABC")); -} - TEST_F(TestApiBlackSolver, mkTerm) { Sort bv32 = d_solver.mkBitVectorSort(32); diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp index 9dd803c93..50ef8bf0f 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/term_black.cpp @@ -689,64 +689,318 @@ TEST_F(TestApiBlackTerm, getInteger) ASSERT_THROW(d_solver.mkInteger("-01"), CVC5ApiException); ASSERT_THROW(d_solver.mkInteger("-00"), CVC5ApiException); - ASSERT_TRUE(!int1.isInt32() && !int1.isUInt32() && !int1.isInt64() - && !int1.isUInt64() && int1.isInteger()); - ASSERT_EQ(int1.getInteger(), "-18446744073709551616"); - ASSERT_TRUE(!int2.isInt32() && !int2.isUInt32() && !int2.isInt64() - && !int2.isUInt64() && int2.isInteger()); - ASSERT_EQ(int2.getInteger(), "-18446744073709551615"); - ASSERT_TRUE(!int3.isInt32() && !int3.isUInt32() && int3.isInt64() - && !int3.isUInt64() && int3.isInteger()); - ASSERT_EQ(int3.getInt64(), -4294967296); - ASSERT_EQ(int3.getInteger(), "-4294967296"); - ASSERT_TRUE(!int4.isInt32() && !int4.isUInt32() && int4.isInt64() - && !int4.isUInt64() && int4.isInteger()); - ASSERT_EQ(int4.getInt64(), -4294967295); - ASSERT_EQ(int4.getInteger(), "-4294967295"); - ASSERT_TRUE(int5.isInt32() && !int5.isUInt32() && int5.isInt64() - && !int5.isUInt64() && int5.isInteger()); - ASSERT_EQ(int5.getInt32(), -10); - ASSERT_EQ(int5.getInt64(), -10); - ASSERT_EQ(int5.getInteger(), "-10"); - ASSERT_TRUE(int6.isInt32() && int6.isUInt32() && int6.isInt64() - && int6.isUInt64() && int6.isInteger()); - ASSERT_EQ(int6.getInt32(), 0); - ASSERT_EQ(int6.getUInt32(), 0); - ASSERT_EQ(int6.getInt64(), 0); - ASSERT_EQ(int6.getUInt64(), 0); - ASSERT_EQ(int6.getInteger(), "0"); - ASSERT_TRUE(int7.isInt32() && int7.isUInt32() && int7.isInt64() - && int7.isUInt64() && int7.isInteger()); - ASSERT_EQ(int7.getInt32(), 10); - ASSERT_EQ(int7.getUInt32(), 10); - ASSERT_EQ(int7.getInt64(), 10); - ASSERT_EQ(int7.getUInt64(), 10); - ASSERT_EQ(int7.getInteger(), "10"); - ASSERT_TRUE(!int8.isInt32() && int8.isUInt32() && int8.isInt64() - && int8.isUInt64() && int8.isInteger()); - ASSERT_EQ(int8.getUInt32(), 4294967295); - ASSERT_EQ(int8.getInt64(), 4294967295); - ASSERT_EQ(int8.getUInt64(), 4294967295); - ASSERT_EQ(int8.getInteger(), "4294967295"); - ASSERT_TRUE(!int9.isInt32() && !int9.isUInt32() && int9.isInt64() - && int9.isUInt64() && int9.isInteger()); - ASSERT_EQ(int9.getInt64(), 4294967296); - ASSERT_EQ(int9.getUInt64(), 4294967296); - ASSERT_EQ(int9.getInteger(), "4294967296"); - ASSERT_TRUE(!int10.isInt32() && !int10.isUInt32() && !int10.isInt64() - && int10.isUInt64() && int10.isInteger()); - ASSERT_EQ(int10.getUInt64(), 18446744073709551615ull); - ASSERT_EQ(int10.getInteger(), "18446744073709551615"); - ASSERT_TRUE(!int11.isInt32() && !int11.isUInt32() && !int11.isInt64() - && !int11.isUInt64() && int11.isInteger()); - ASSERT_EQ(int11.getInteger(), "18446744073709551616"); + ASSERT_TRUE(!int1.isInt32Value() && !int1.isUInt32Value() + && !int1.isInt64Value() && !int1.isUInt64Value() + && int1.isIntegerValue()); + ASSERT_EQ(int1.getIntegerValue(), "-18446744073709551616"); + ASSERT_TRUE(!int2.isInt32Value() && !int2.isUInt32Value() + && !int2.isInt64Value() && !int2.isUInt64Value() + && int2.isIntegerValue()); + ASSERT_EQ(int2.getIntegerValue(), "-18446744073709551615"); + ASSERT_TRUE(!int3.isInt32Value() && !int3.isUInt32Value() + && int3.isInt64Value() && !int3.isUInt64Value() + && int3.isIntegerValue()); + ASSERT_EQ(int3.getInt64Value(), -4294967296); + ASSERT_EQ(int3.getIntegerValue(), "-4294967296"); + ASSERT_TRUE(!int4.isInt32Value() && !int4.isUInt32Value() + && int4.isInt64Value() && !int4.isUInt64Value() + && int4.isIntegerValue()); + ASSERT_EQ(int4.getInt64Value(), -4294967295); + ASSERT_EQ(int4.getIntegerValue(), "-4294967295"); + ASSERT_TRUE(int5.isInt32Value() && !int5.isUInt32Value() + && int5.isInt64Value() && !int5.isUInt64Value() + && int5.isIntegerValue()); + ASSERT_EQ(int5.getInt32Value(), -10); + ASSERT_EQ(int5.getInt64Value(), -10); + ASSERT_EQ(int5.getIntegerValue(), "-10"); + ASSERT_TRUE(int6.isInt32Value() && int6.isUInt32Value() && int6.isInt64Value() + && int6.isUInt64Value() && int6.isIntegerValue()); + ASSERT_EQ(int6.getInt32Value(), 0); + ASSERT_EQ(int6.getUInt32Value(), 0); + ASSERT_EQ(int6.getInt64Value(), 0); + ASSERT_EQ(int6.getUInt64Value(), 0); + ASSERT_EQ(int6.getIntegerValue(), "0"); + ASSERT_TRUE(int7.isInt32Value() && int7.isUInt32Value() && int7.isInt64Value() + && int7.isUInt64Value() && int7.isIntegerValue()); + ASSERT_EQ(int7.getInt32Value(), 10); + ASSERT_EQ(int7.getUInt32Value(), 10); + ASSERT_EQ(int7.getInt64Value(), 10); + ASSERT_EQ(int7.getUInt64Value(), 10); + ASSERT_EQ(int7.getIntegerValue(), "10"); + ASSERT_TRUE(!int8.isInt32Value() && int8.isUInt32Value() + && int8.isInt64Value() && int8.isUInt64Value() + && int8.isIntegerValue()); + ASSERT_EQ(int8.getUInt32Value(), 4294967295); + ASSERT_EQ(int8.getInt64Value(), 4294967295); + ASSERT_EQ(int8.getUInt64Value(), 4294967295); + ASSERT_EQ(int8.getIntegerValue(), "4294967295"); + ASSERT_TRUE(!int9.isInt32Value() && !int9.isUInt32Value() + && int9.isInt64Value() && int9.isUInt64Value() + && int9.isIntegerValue()); + ASSERT_EQ(int9.getInt64Value(), 4294967296); + ASSERT_EQ(int9.getUInt64Value(), 4294967296); + ASSERT_EQ(int9.getIntegerValue(), "4294967296"); + ASSERT_TRUE(!int10.isInt32Value() && !int10.isUInt32Value() + && !int10.isInt64Value() && int10.isUInt64Value() + && int10.isIntegerValue()); + ASSERT_EQ(int10.getUInt64Value(), 18446744073709551615ull); + ASSERT_EQ(int10.getIntegerValue(), "18446744073709551615"); + ASSERT_TRUE(!int11.isInt32Value() && !int11.isUInt32Value() + && !int11.isInt64Value() && !int11.isUInt64Value() + && int11.isIntegerValue()); + ASSERT_EQ(int11.getIntegerValue(), "18446744073709551616"); } TEST_F(TestApiBlackTerm, getString) { Term s1 = d_solver.mkString("abcde"); - ASSERT_TRUE(s1.isString()); - ASSERT_EQ(s1.getString(), L"abcde"); + ASSERT_TRUE(s1.isStringValue()); + ASSERT_EQ(s1.getStringValue(), L"abcde"); +} + +TEST_F(TestApiBlackTerm, getReal) +{ + Term real1 = d_solver.mkReal("0"); + Term real2 = d_solver.mkReal(".0"); + Term real3 = d_solver.mkReal("-17"); + Term real4 = d_solver.mkReal("-3/5"); + Term real5 = d_solver.mkReal("12.7"); + Term real6 = d_solver.mkReal("1/4294967297"); + Term real7 = d_solver.mkReal("4294967297"); + Term real8 = d_solver.mkReal("1/18446744073709551617"); + Term real9 = d_solver.mkReal("18446744073709551617"); + + ASSERT_TRUE(real1.isRealValue() && real1.isReal64Value() + && real1.isReal32Value()); + ASSERT_TRUE(real2.isRealValue() && real2.isReal64Value() + && real2.isReal32Value()); + ASSERT_TRUE(real3.isRealValue() && real3.isReal64Value() + && real3.isReal32Value()); + ASSERT_TRUE(real4.isRealValue() && real4.isReal64Value() + && real4.isReal32Value()); + ASSERT_TRUE(real5.isRealValue() && real5.isReal64Value() + && real5.isReal32Value()); + ASSERT_TRUE(real6.isRealValue() && real6.isReal64Value()); + ASSERT_TRUE(real7.isRealValue() && real7.isReal64Value()); + ASSERT_TRUE(real8.isRealValue()); + ASSERT_TRUE(real9.isRealValue()); + + ASSERT_EQ(std::make_pair(0, 1u), real1.getReal32Value()); + ASSERT_EQ(std::make_pair(0l, 1ul), real1.getReal64Value()); + ASSERT_EQ("0", real1.getRealValue()); + + ASSERT_EQ(std::make_pair(0, 1u), real2.getReal32Value()); + ASSERT_EQ(std::make_pair(0l, 1ul), real2.getReal64Value()); + ASSERT_EQ("0", real2.getRealValue()); + + ASSERT_EQ(std::make_pair(-17, 1u), real3.getReal32Value()); + ASSERT_EQ(std::make_pair(-17l, 1ul), real3.getReal64Value()); + ASSERT_EQ("-17", real3.getRealValue()); + + ASSERT_EQ(std::make_pair(-3, 5u), real4.getReal32Value()); + ASSERT_EQ(std::make_pair(-3l, 5ul), real4.getReal64Value()); + ASSERT_EQ("-3/5", real4.getRealValue()); + + ASSERT_EQ(std::make_pair(127, 10u), real5.getReal32Value()); + ASSERT_EQ(std::make_pair(127l, 10ul), real5.getReal64Value()); + ASSERT_EQ("127/10", real5.getRealValue()); + + ASSERT_EQ(std::make_pair(1l, 4294967297ul), real6.getReal64Value()); + ASSERT_EQ("1/4294967297", real6.getRealValue()); + + ASSERT_EQ(std::make_pair(4294967297l, 1ul), real7.getReal64Value()); + ASSERT_EQ("4294967297", real7.getRealValue()); + + ASSERT_EQ("1/18446744073709551617", real8.getRealValue()); + + ASSERT_EQ("18446744073709551617", real9.getRealValue()); +} + +TEST_F(TestApiBlackTerm, getConstArrayBase) +{ + Sort intsort = d_solver.getIntegerSort(); + Sort arrsort = d_solver.mkArraySort(intsort, intsort); + Term one = d_solver.mkInteger(1); + Term constarr = d_solver.mkConstArray(arrsort, one); + + ASSERT_TRUE(constarr.isConstArray()); + ASSERT_EQ(one, constarr.getConstArrayBase()); +} + +TEST_F(TestApiBlackTerm, getBoolean) +{ + Term b1 = d_solver.mkBoolean(true); + Term b2 = d_solver.mkBoolean(false); + + ASSERT_TRUE(b1.isBooleanValue()); + ASSERT_TRUE(b2.isBooleanValue()); + ASSERT_TRUE(b1.getBooleanValue()); + ASSERT_FALSE(b2.getBooleanValue()); +} + +TEST_F(TestApiBlackTerm, getBitVector) +{ + Term b1 = d_solver.mkBitVector(8, 15); + Term b2 = d_solver.mkBitVector("00001111", 2); + Term b3 = d_solver.mkBitVector("15", 10); + Term b4 = d_solver.mkBitVector("0f", 16); + Term b5 = d_solver.mkBitVector(8, "00001111", 2); + Term b6 = d_solver.mkBitVector(8, "15", 10); + Term b7 = d_solver.mkBitVector(8, "0f", 16); + + ASSERT_TRUE(b1.isBitVectorValue()); + ASSERT_TRUE(b2.isBitVectorValue()); + ASSERT_TRUE(b3.isBitVectorValue()); + ASSERT_TRUE(b4.isBitVectorValue()); + ASSERT_TRUE(b5.isBitVectorValue()); + ASSERT_TRUE(b6.isBitVectorValue()); + ASSERT_TRUE(b7.isBitVectorValue()); + + ASSERT_EQ("00001111", b1.getBitVectorValue(2)); + ASSERT_EQ("15", b1.getBitVectorValue(10)); + ASSERT_EQ("f", b1.getBitVectorValue(16)); + ASSERT_EQ("00001111", b2.getBitVectorValue(2)); + ASSERT_EQ("15", b2.getBitVectorValue(10)); + ASSERT_EQ("f", b2.getBitVectorValue(16)); + ASSERT_EQ("1111", b3.getBitVectorValue(2)); + ASSERT_EQ("15", b3.getBitVectorValue(10)); + ASSERT_EQ("f", b3.getBitVectorValue(16)); + ASSERT_EQ("00001111", b4.getBitVectorValue(2)); + ASSERT_EQ("15", b4.getBitVectorValue(10)); + ASSERT_EQ("f", b4.getBitVectorValue(16)); + ASSERT_EQ("00001111", b5.getBitVectorValue(2)); + ASSERT_EQ("15", b5.getBitVectorValue(10)); + ASSERT_EQ("f", b5.getBitVectorValue(16)); + ASSERT_EQ("00001111", b6.getBitVectorValue(2)); + ASSERT_EQ("15", b6.getBitVectorValue(10)); + ASSERT_EQ("f", b6.getBitVectorValue(16)); + ASSERT_EQ("00001111", b7.getBitVectorValue(2)); + ASSERT_EQ("15", b7.getBitVectorValue(10)); + ASSERT_EQ("f", b7.getBitVectorValue(16)); +} + +TEST_F(TestApiBlackTerm, getAbstractValue) +{ + Term v1 = d_solver.mkAbstractValue(1); + Term v2 = d_solver.mkAbstractValue("15"); + Term v3 = d_solver.mkAbstractValue("18446744073709551617"); + + ASSERT_TRUE(v1.isAbstractValue()); + ASSERT_TRUE(v2.isAbstractValue()); + ASSERT_TRUE(v3.isAbstractValue()); + ASSERT_EQ("1", v1.getAbstractValue()); + ASSERT_EQ("15", v2.getAbstractValue()); + ASSERT_EQ("18446744073709551617", v3.getAbstractValue()); +} + +TEST_F(TestApiBlackTerm, getTuple) +{ + Sort s1 = d_solver.getIntegerSort(); + Sort s2 = d_solver.getRealSort(); + Sort s3 = d_solver.getStringSort(); + + Term t1 = d_solver.mkInteger(15); + Term t2 = d_solver.mkReal(17, 25); + Term t3 = d_solver.mkString("abc"); + + Term tup = d_solver.mkTuple({s1, s2, s3}, {t1, t2, t3}); + + ASSERT_TRUE(tup.isTupleValue()); + ASSERT_EQ(std::vector({t1, t2, t3}), tup.getTupleValue()); +} + +TEST_F(TestApiBlackTerm, getFloatingPoint) +{ + Term bvval = d_solver.mkBitVector("0000110000000011"); + Term fp = d_solver.mkFloatingPoint(5, 11, bvval); + + ASSERT_TRUE(fp.isFloatingPointValue()); + ASSERT_FALSE(fp.isFloatingPointPosZero()); + ASSERT_FALSE(fp.isFloatingPointNegZero()); + ASSERT_FALSE(fp.isFloatingPointPosInf()); + ASSERT_FALSE(fp.isFloatingPointNegInf()); + ASSERT_FALSE(fp.isFloatingPointNaN()); + ASSERT_EQ(std::make_tuple(5u, 11u, bvval), fp.getFloatingPointValue()); + + ASSERT_TRUE(d_solver.mkPosZero(5, 11).isFloatingPointPosZero()); + ASSERT_TRUE(d_solver.mkNegZero(5, 11).isFloatingPointNegZero()); + ASSERT_TRUE(d_solver.mkPosInf(5, 11).isFloatingPointPosInf()); + ASSERT_TRUE(d_solver.mkNegInf(5, 11).isFloatingPointNegInf()); + ASSERT_TRUE(d_solver.mkNaN(5, 11).isFloatingPointNaN()); +} + +TEST_F(TestApiBlackTerm, getSet) +{ + Sort s = d_solver.mkSetSort(d_solver.getIntegerSort()); + + Term i1 = d_solver.mkInteger(5); + Term i2 = d_solver.mkInteger(7); + + Term s1 = d_solver.mkEmptySet(s); + Term s2 = d_solver.mkTerm(Kind::SINGLETON, i1); + Term s3 = d_solver.mkTerm(Kind::SINGLETON, i1); + Term s4 = d_solver.mkTerm(Kind::SINGLETON, i2); + Term s5 = + d_solver.mkTerm(Kind::UNION, s2, d_solver.mkTerm(Kind::UNION, s3, s4)); + + ASSERT_TRUE(s1.isSetValue()); + ASSERT_TRUE(s2.isSetValue()); + ASSERT_TRUE(s3.isSetValue()); + ASSERT_TRUE(s4.isSetValue()); + ASSERT_FALSE(s5.isSetValue()); + s5 = d_solver.simplify(s5); + ASSERT_TRUE(s5.isSetValue()); + + ASSERT_EQ(std::set({}), s1.getSetValue()); + ASSERT_EQ(std::set({i1}), s2.getSetValue()); + ASSERT_EQ(std::set({i1}), s3.getSetValue()); + ASSERT_EQ(std::set({i2}), s4.getSetValue()); + ASSERT_EQ(std::set({i1, i2}), s5.getSetValue()); +} + +TEST_F(TestApiBlackTerm, getSequence) +{ + Sort s = d_solver.mkSequenceSort(d_solver.getIntegerSort()); + + Term i1 = d_solver.mkInteger(5); + Term i2 = d_solver.mkInteger(7); + + Term s1 = d_solver.mkEmptySequence(s); + Term s2 = d_solver.mkTerm(Kind::SEQ_UNIT, i1); + Term s3 = d_solver.mkTerm(Kind::SEQ_UNIT, i1); + Term s4 = d_solver.mkTerm(Kind::SEQ_UNIT, i2); + Term s5 = d_solver.mkTerm( + Kind::SEQ_CONCAT, s2, d_solver.mkTerm(Kind::SEQ_CONCAT, s3, s4)); + + ASSERT_TRUE(s1.isSequenceValue()); + ASSERT_TRUE(!s2.isSequenceValue()); + ASSERT_TRUE(!s3.isSequenceValue()); + ASSERT_TRUE(!s4.isSequenceValue()); + ASSERT_TRUE(!s5.isSequenceValue()); + + s2 = d_solver.simplify(s2); + s3 = d_solver.simplify(s3); + s4 = d_solver.simplify(s4); + s5 = d_solver.simplify(s5); + + ASSERT_EQ(std::vector({}), s1.getSequenceValue()); + ASSERT_EQ(std::vector({i1}), s2.getSequenceValue()); + ASSERT_EQ(std::vector({i1}), s3.getSequenceValue()); + ASSERT_EQ(std::vector({i2}), s4.getSequenceValue()); + ASSERT_EQ(std::vector({i1, i1, i2}), s5.getSequenceValue()); +} + +TEST_F(TestApiBlackTerm, getUninterpretedConst) +{ + Sort s = d_solver.mkUninterpretedSort("test"); + Term t1 = d_solver.mkUninterpretedConst(s, 3); + Term t2 = d_solver.mkUninterpretedConst(s, 5); + + ASSERT_TRUE(t1.isUninterpretedValue()); + ASSERT_TRUE(t2.isUninterpretedValue()); + + ASSERT_EQ(std::make_pair(s, 3), t1.getUninterpretedValue()); + ASSERT_EQ(std::make_pair(s, 5), t2.getUninterpretedValue()); } TEST_F(TestApiBlackTerm, substitute) -- 2.30.2