SMT-LIB compliance: allow bin/hex set-info, e.g. (set-info :key #xffff). Thanks...

diff --git a/THANKS b/THANKS
index b9f4c9d2b702985ebe078b4d187713da67882981..8cd0737a262f2a24eee98262ef97e5a872bbd403 100644 (file)
--- a/THANKS
+++ b/THANKS
@@ -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 f1acac6ba321acb3317f3687f7fc6c90ef6ae948..3c68e4e4c0d126f91fbbb8b9535f6b95a35d126f 100644 (file)
--- 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