From 0c4a6edae95b3ffc76cb82604a3d1694d42625bb Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Tue, 27 Apr 2010 20:44:47 +0000
Subject: [PATCH] Adding Integer and Rational constants to SMT

---
 src/parser/antlr_input.cpp      | 15 +++++++++++++++
 src/parser/antlr_input.h        |  3 +++
 src/parser/parser_state.cpp     |  9 ---------
 src/parser/smt/Smt.g            | 18 ++++++++++++++++--
 test/unit/parser/parser_white.h |  9 +++++++--
 5 files changed, 41 insertions(+), 13 deletions(-)

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index b8caf5ded..47420a015 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -91,6 +91,16 @@ pANTLR3_COMMON_TOKEN_STREAM AntlrInput::getTokenStream() {
   return d_tokenStream;
 }
 
+void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) {
+  pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super);
+  AlwaysAssert(lexer!=NULL);
+  ParserState *parserState = (ParserState*)(lexer->super);
+  AlwaysAssert(parserState!=NULL);
+
+  // Call the error display routine
+  parserState->parseError("Error finding next token.");
+}
+
 void AntlrInput::parseError(const std::string& message)
     throw (ParserException) {
   Debug("parser") << "Throwing exception: "
@@ -125,6 +135,11 @@ void AntlrInput::setLexer(pANTLR3_LEXER pLexer) {
   }
 
   d_tokenStream = buffer->commonTstream;
+
+  // ANTLR isn't using super, AFAICT.
+  d_lexer->super = getParserState();
+  // Override default lexer error reporting
+  d_lexer->rec->reportError = &lexerError;
 }
 
 void AntlrInput::setParser(pANTLR3_PARSER pParser) {
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index dee7c1491..a36853d7b 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -67,6 +67,9 @@ class AntlrInput : public Input {
   /** Turns an ANTLR3 exception into a message for the user and calls <code>parseError</code>. */
   static void reportError(pANTLR3_BASE_RECOGNIZER recognizer);
 
+  /** Builds a message for a lexer error and calls <code>parseError</code>. */
+  static void lexerError(pANTLR3_BASE_RECOGNIZER recognizer);
+
 public:
 
   /** Create a file input.
diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp
index 827d5fcaa..204dd3469 100644
--- a/src/parser/parser_state.cpp
+++ b/src/parser/parser_state.cpp
@@ -115,15 +115,6 @@ ParserState::defineVar(const std::string& name, const Expr& val) {
   Assert(isDeclared(name));
 }
 
-/*
-void
-ParserState::undefineVar(const std::string& name) {
-  Assert(isDeclared(name));
-  d_declScope.unbind(name);
-  Assert(!isDeclared(name));
-}
-*/
-
 Type
 ParserState::mkSort(const std::string& name) {
   Debug("parser") << "newSort(" << name << ")" << std::endl;
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 67290ada2..83e3447ac 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -61,7 +61,9 @@ namespace CVC4 {
 #include "expr/type.h"
 #include "parser/antlr_input.h"
 #include "parser/parser_state.h"
+#include "util/integer.h"
 #include "util/output.h"
+#include "util/rational.h"
 #include <vector>
 
 using namespace CVC4;
@@ -229,6 +231,13 @@ annotatedFormula[CVC4::Expr& expr]
     /* constants */
   | TRUE_TOK          { expr = MK_CONST(true); }
   | FALSE_TOK         { expr = MK_CONST(false); }
+  | NUMERAL_TOK
+    { Integer num( AntlrInput::tokenText($NUMERAL_TOK) );
+      expr = MK_CONST(num); }
+  | RATIONAL_TOK
+    { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string
+      Rational rat( AntlrInput::tokenText($RATIONAL_TOK) );
+      expr = MK_CONST(rat); }
     // NOTE: Theory constants go here
     /* TODO: let, flet, quantifiers, arithmetic constants */
   ;
@@ -525,7 +534,11 @@ WHITESPACE
  * Matches a numeral from the input (non-empty sequence of digits).
  */
 NUMERAL_TOK
-  :  (DIGIT)+
+  : DIGIT+
+  ;
+
+RATIONAL_TOK
+  : DIGIT+ '.' DIGIT+
   ;
 
 /**
@@ -557,7 +570,8 @@ ALPHA
  * Matches the digits (0-9)
  */
 fragment DIGIT :   '0'..'9';
-
+// fragment NON_ZERO_DIGIT : '1'..'9';
+// fragment NUMERAL_SEQ : '0' | NON_ZERO_DIGIT DIGIT*;
 
 /**
  * Matches an allowed escaped character.
diff --git a/test/unit/parser/parser_white.h b/test/unit/parser/parser_white.h
index 317817e15..1d19525d6 100644
--- a/test/unit/parser/parser_white.h
+++ b/test/unit/parser/parser_white.h
@@ -109,7 +109,10 @@ const string goodSmtExprs[] = {
     "(and (iff a b) (not a))",
     "(iff (xor a b) (and (or a b) (not (and a b))))",
     "(ite a (f x) y)",
-    "(if_then_else a (f x) y)"
+    "(if_then_else a (f x) y)",
+    "1",
+    "0"// ,
+//    "1.5"
 };
 
 const int numGoodSmtExprs = sizeof(goodSmtExprs) / sizeof(string);
@@ -134,7 +137,9 @@ const string badSmtExprs[] = {
     "(not a b)", // wrong arity
     "not a", // needs parens
     "(ite a x)", // wrong arity
-    "(a b)" // using non-function as function
+    "(a b)", // using non-function as function
+    ".5", // rational constants must have integer prefix
+    "1." // rational constants must have fractional suffix
 };
 
 const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string);
-- 
2.30.2