diff options
author | Gereon Kremer <nafur42@gmail.com> | 2021-05-20 04:08:56 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-20 02:08:56 +0000 |
commit | a95980ecd80b971086c328c3e1bb731852890a07 (patch) | |
tree | 8b9be61587f4c29e24c9f15edb9f31f955c4aef9 /src | |
parent | 8bb85b0f1664f6d03bcbf3997533140204c29251 (diff) |
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<uint32> for the SMT-LIB parser and the String class.
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cpp/cvc5.cpp | 530 | ||||
-rw-r--r-- | src/api/cpp/cvc5.h | 266 | ||||
-rw-r--r-- | src/api/python/cvc5.pxd | 8 | ||||
-rw-r--r-- | src/api/python/cvc5.pxi | 29 | ||||
-rw-r--r-- | src/parser/parser.cpp | 43 | ||||
-rw-r--r-- | src/parser/parser.h | 10 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 2 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 4 | ||||
-rw-r--r-- | src/smt/command.cpp | 4 | ||||
-rw-r--r-- | src/util/string.cpp | 9 | ||||
-rw-r--r-- | src/util/string.h | 1 |
11 files changed, 728 insertions, 178 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<ArrayStoreAll>().getValue()); - //////// - CVC5_API_TRY_CATCH_END; -} - std::vector<Term> 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<Rational>(); + switch (node.getKind()) + { + case cvc5::Kind::CAST_TO_REAL: return node[0].getConst<Rational>(); + case cvc5::Kind::CONST_RATIONAL: return node.getConst<Rational>(); + default: + CVC5_API_CHECK(false) << "Node is not a rational."; + return node.getConst<Rational>(); + } } Integer getInteger(const cvc5::Node& node) { @@ -2582,6 +2575,20 @@ bool checkReal64Bounds(const Rational& r) && checkIntegerBounds<std::uint64_t>(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<cvc5::String>().toWString(); //////// @@ -2720,6 +2754,387 @@ std::vector<Node> Term::termVectorToNodes(const std::vector<Term>& 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<std::int32_t, std::uint32_t> 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<std::int64_t, std::uint64_t> 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<ArrayStoreAll>(); + 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<bool>(); + //////// + 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<BitVector>().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<AbstractValue>().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> 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<Term> 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<FloatingPoint>(); + 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<FloatingPoint>(); + 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<FloatingPoint>(); + 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<FloatingPoint>(); + 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<FloatingPoint>().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<std::uint32_t, std::uint32_t, Term> 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<FloatingPoint>(); + return std::make_tuple(fp.getSize().exponentWidth(), + fp.getSize().significandWidth(), + d_solver->mkValHelper<BitVector>(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<Term>& 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> 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<Term> 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> 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<Term> res; + const Sequence& seq = d_node->getConst<Sequence>(); + 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<Sort, std::int32_t> 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<UninterpretedConstant>(); + 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>(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<uint32_t>(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<unsigned> cpts; - cpts.push_back(val); - return mkValHelper<cvc5::String>(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>(cvc5::String(std::string(1, c))); - //////// - CVC5_API_TRY_CATCH_END; -} - -Term Solver::mkString(const std::vector<uint32_t>& 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<uint32_t>& 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 @@ -1054,13 +1054,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 * @return the elements of the constant 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<int32_t, uint32_t> 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<int64_t, uint64_t> 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<Term> 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<uint32_t, uint32_t, Term> 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<Term> 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<Term> 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<Sort, int32_t> getUninterpretedValue() const; protected: /** @@ -1281,6 +1426,15 @@ class CVC5_EXPORT Term /** Helper to convert a vector of Terms to internal Nodes. */ std::vector<Node> static termVectorToNodes(const std::vector<Term>& terms); + /** Helper method to collect all elements of a set. */ + static void collectSet(std::set<Term>& set, + const cvc5::Node& node, + const Solver* slv); + /** Helper method to collect all elements of a sequence. */ + static void collectSequence(std::vector<Term>& 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<uint32_t>& 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 "<functional>" namespace "std" nogil: hash() size_t operator()(T t) +cdef extern from "<string>" 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(<unsigned> ord(u)) - term.cterm = self.csolver.mkString(<const vector[unsigned]&> 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(<unsigned> u) - term.cterm = self.csolver.mkString(<const vector[unsigned]&> 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<unsigned> Parser::processAdHocStringEsc(const std::string& s) +std::wstring Parser::processAdHocStringEsc(const std::string& s) { std::wstring ws; { @@ -763,7 +763,7 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s) } } - std::vector<unsigned> str; + std::wstring res; unsigned i = 0; while (i < ws.size()) { @@ -771,7 +771,7 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s) if (ws[i] != '\\') { // don't worry about printable here - str.push_back(static_cast<unsigned>(ws[i])); + res.push_back(ws[i]); ++i; continue; } @@ -789,49 +789,49 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s) { case 'n': { - str.push_back(static_cast<unsigned>('\n')); + res.push_back('\n'); i++; } break; case 't': { - str.push_back(static_cast<unsigned>('\t')); + res.push_back('\t'); i++; } break; case 'v': { - str.push_back(static_cast<unsigned>('\v')); + res.push_back('\v'); i++; } break; case 'b': { - str.push_back(static_cast<unsigned>('\b')); + res.push_back('\b'); i++; } break; case 'r': { - str.push_back(static_cast<unsigned>('\r')); + res.push_back('\r'); i++; } break; case 'f': { - str.push_back(static_cast<unsigned>('\f')); + res.push_back('\f'); i++; } break; case 'a': { - str.push_back(static_cast<unsigned>('\a')); + res.push_back('\a'); i++; } break; case '\\': { - str.push_back(static_cast<unsigned>('\\')); + res.push_back('\\'); i++; } break; @@ -846,7 +846,7 @@ std::vector<unsigned> 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<unsigned> Parser::processAdHocStringEsc(const std::string& s) && ws[i + 2] < '8') { num = num * 8 + static_cast<unsigned>(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<unsigned> 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<wchar_t>(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<unsigned> 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<api::Term>& 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<unsigned>(s[i]); + } +} + String::String(const std::vector<unsigned> &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)) { |