From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 16 Dec 2020 09:33:03 +0000 (-0600)
Subject: Use uint64 utility when parsing tuple selectors in smt2 (#5681)
X-Git-Tag: cvc5-1.0.0~2438
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5b90fdad09209da667cc281f5425300a4b2bb9c9;p=cvc5.git

Use uint64 utility when parsing tuple selectors in smt2 (#5681)

The smt2 parser is now 100% independent from the Expr-layer.
---

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 2474c89c2..f069a486f 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -18,7 +18,6 @@
 #include <algorithm>
 
 #include "base/check.h"
-#include "expr/expr.h"
 #include "options/options.h"
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
@@ -1072,13 +1071,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
-    std::string indexString = p.d_expr.toString();
-    Integer x = p.d_expr.getExpr().getConst<Rational>().getNumerator();
-    if (!x.fitsUnsignedInt())
+    if (!p.d_expr.isUInt64())
     {
-      parseError("index of tupSel is larger than size of unsigned int");
+      parseError("index of tupSel is larger than size of uint64_t");
     }
-    unsigned int n = x.toUnsignedInt();
+    uint64_t n = p.d_expr.getUInt64();
     if (args.size() != 1)
     {
       parseError("tupSel should only be applied to one tuple argument");