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/parser/smt2 | |
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/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 2 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 4 |
2 files changed, 3 insertions, 3 deletions
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"); |