diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-14 15:21:24 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-14 15:52:43 -0400 |
| commit | 52514303081e78c98e504980a50b76a04f4b8762 (patch) | |
| tree | ff913f6d81048da5f02031f8ed43f5e9ab613a79 /src | |
| parent | f0407e1c718050daf021c937708d779bdcc3b191 (diff) | |
SMT-LIB compliance: allow bin/hex set-info, e.g. (set-info :key #xffff). Thanks to David Cok for the bug report.
Diffstat (limited to 'src')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index f1acac6ba..3c68e4e4c 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -708,6 +708,16 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); } | DECIMAL_LITERAL { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); } + | HEX_LITERAL + { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); + std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); + sexpr = Integer(hexString, 16); + } + | BINARY_LITERAL + { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); + std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); + sexpr = Integer(binString, 2); + } | str[s,false] { sexpr = SExpr(s); } // | LPAREN_TOK STRCST_TOK |