From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 14 Mar 2014 19:21:24 +0000 (-0400)
Subject: SMT-LIB compliance: allow bin/hex set-info, e.g. (set-info :key #xffff).  Thanks... 
X-Git-Tag: cvc5-1.0.0~7016
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=52514303081e78c98e504980a50b76a04f4b8762;p=cvc5.git

SMT-LIB compliance: allow bin/hex set-info, e.g. (set-info :key #xffff).  Thanks to David Cok for the bug report.
---

diff --git a/THANKS b/THANKS
index b9f4c9d2b..8cd0737a2 100644
--- 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 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