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 | |
| 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.
| -rw-r--r-- | THANKS | 2 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 10 |
2 files changed, 11 insertions, 1 deletions
@@ -4,7 +4,7 @@ submitting a number of patches in September 2012 related to SMT-LIBv2 compliance. Thanks to David Cok of GrammaTech, Inc., for suggesting numerous improvements -in CVC4's SMT-LIBv2 compliance in May 2013. +in CVC4's SMT-LIBv2 compliance in 2013 and 2014. Thanks to Adam Buchbinder at Google for submitting patches in November 2013 to fix a number of issues with CVC3 (which were also applicable to CVC4's 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 |