diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-06 21:11:37 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-06 21:11:37 +0000 |
| commit | f4643b0e2f5ca233dcfeb91fbb424b8caec836e6 (patch) | |
| tree | 12bae96a8b0e26ecf0fd279b5c309a26433ac415 /src/parser/smt2 | |
| parent | c52d38c2a134488c5212f21d963a1ae442206fc1 (diff) | |
Adding AntlrInput::tokenTextSubstr
Diffstat (limited to 'src/parser/smt2')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 4f65fa5e7..fd5e334ed 100644 --- 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 ; |