Adding Integer and Rational constants to SMT

4 files changed, 34 insertions, 11 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.