Adding AntlrInput::tokenTextSubstr

diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 38fe1bce8f7d053fe511ab18ca6c34129c93ab62..4e075e5ddecdbb6e2c8499a56565ccad93da96dd 100644 (file)
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -20,6 +20,8 @@
 
 #include <antlr3.h>
 #include <iostream>
+#include <sstream>
+#include <stdexcept>
 #include <string>
 #include <vector>
 
@@ -143,10 +145,24 @@ public:
 
   /** Retrieve the text associated with a token. */
   static std::string tokenText(pANTLR3_COMMON_TOKEN token);
+
+  /** Retrieve a substring of the text associated with a token.
+   *
+   * @param token the token
+   * @param index the index of the starting character of the substring
+   * @param n the size of the substring. If <code>n</code> is 0, then all of the
+   * characters up to the end of the token text will be included. If <code>n</code>
+   * would make the substring span past the end of the token text, only those
+   * characters up to the end of the token text will be included.
+   */
+  static std::string tokenTextSubstr(pANTLR3_COMMON_TOKEN token, size_t index, size_t n = 0);
+
   /** Retrieve an unsigned from the text of a token */
   static unsigned tokenToUnsigned( pANTLR3_COMMON_TOKEN token );
+
   /** Retrieve an Integer from the text of a token */
   static Integer tokenToInteger( pANTLR3_COMMON_TOKEN token );
+
   /** Retrieve a Rational from the text of a token */
   static Rational tokenToRational(pANTLR3_COMMON_TOKEN token);
 
@@ -191,6 +207,25 @@ inline std::string AntlrInput::tokenText(pANTLR3_COMMON_TOKEN token) {
   return txt;
 }
 
+inline std::string AntlrInput::tokenTextSubstr(pANTLR3_COMMON_TOKEN token,
+                                               size_t index,
+                                               size_t n) {
+  ANTLR3_MARKER start = token->getStartIndex(token);
+  ANTLR3_MARKER end = token->getStopIndex(token);
+  Assert( start < end );
+  if( index > (size_t) end - start ) {
+    stringstream ss;
+    ss << "Out-of-bounds substring index: " << index;
+    throw std::invalid_argument(ss.str());
+  }
+  start += index;
+  if( n==0 || n >= (size_t) end - start ) {
+    return std::string( (const char *)start + index, end-start+1 );
+  } else {
+    return std::string( (const char *)start + index, n );
+  }
+}
+
 inline unsigned AntlrInput::tokenToUnsigned(pANTLR3_COMMON_TOKEN token) {
   unsigned result;
   std::stringstream ss;

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 4f65fa5e76bb803431ef8bdd64981507000c7e8c..fd5e334ed8005da9fd628f8186038ad3567b80e9 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -260,13 +260,13 @@ term[CVC4::Expr& expr]
     { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string
       expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL) ); }
   | HEX_LITERAL
-    { std::string hexString = AntlrInput::tokenText($HEX_LITERAL);
-      AlwaysAssert( hexString.find("#x") == 0 );
-      expr = MK_CONST( BitVector(hexString.erase(0,2), 16) ); }
+    { Assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
+      std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL,2);
+      expr = MK_CONST( BitVector(hexString, 16) ); }
   | BINARY_LITERAL
-    { std::string binString = AntlrInput::tokenText($BINARY_LITERAL);
-      AlwaysAssert( binString.find("#b") == 0 );
-      expr = MK_CONST( BitVector(binString.erase(0,2), 2) ); }
+    { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
+      std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL,2);
+      expr = MK_CONST( BitVector(binString, 2) ); }
     // NOTE: Theory constants go here
   ;
 

diff --git a/test/unit/util/rational_black.h b/test/unit/util/rational_black.h
index 395a5099d56b795935c4c23dfb3924b2c4a7ec95..35d22b1504d2b8bfa1513ccce26a6df94a3857e6 100644 (file)
--- a/test/unit/util/rational_black.h
+++ b/test/unit/util/rational_black.h
@@ -41,8 +41,6 @@ public:
     TS_ASSERT_THROWS( Rational::fromDecimal("1.2.3");, const std::invalid_argument& );
     TS_ASSERT_THROWS( Rational::fromDecimal("1.2/3");, const std::invalid_argument& );
     TS_ASSERT_THROWS( Rational::fromDecimal("Hello, world!");, const std::invalid_argument& );
-
-    Rational(1);
   }
 
 };