1 files changed, 127 insertions, 0 deletions
diff --git a/src/parser/cvc/cvc_lexer.g b/src/parser/cvc/cvc_lexer.g
new file mode 100644
index 000000000..8d706963f
--- /dev/null
+++ b/src/parser/cvc/cvc_lexer.g
@@ -0,0 +1,127 @@
+options {
+  language = "Cpp";            // C++ output for antlr
+  namespaceStd  = "std";       // Cosmetic option to get rid of long defines in generated code
+  namespaceAntlr = "antlr";    // Cosmetic option to get rid of long defines in generated code
+  namespace = "CVC4::parser";  // Wrap everything in the smtparser namespace
+}
+   
+/**
+ * AntlrCvcLexer class is a stream tokenizer (lexer) for the CVC language. 
+ */
+class AntlrCvcLexer extends Lexer;
+
+options {
+  exportVocab = CvcVocabulary;  // Name of the shared token vocabulary
+  testLiterals = false;         // Do not check for literals by default
+  defaultErrorHandler = false;  // Skip the defaul error handling, just break with exceptions
+  k = 2;  
+}
+ 
+tokens {
+  // Types 
+  BOOLEAN       = "BOOLEAN";
+  // Boolean oparators
+  AND           = "AND";
+  IF            = "IF";
+  THEN          = "THEN";
+  ELSE          = "ELSE";
+  ELSEIF        = "ELSIF";
+  ENDIF         = "ENDIF";
+  NOT           = "NOT";
+  OR            = "OR";
+  TRUE          = "TRUE";
+  FALSE         = "FALSE";
+  XOR           = "XOR";
+  IMPLIES       = "=>";
+  IFF           = "<=>";
+  // Commands
+  ASSERT        = "ASSERT";
+  QUERY         = "QUERY";
+  CHECKSAT      = "CHECKSAT";
+  PRINT         = "PRINT";
+  EXHO          = "ECHO";
+  
+  PUSH          = "PUSH";
+  POP           = "POP";
+  POPTO         = "POPTO";
+}
+
+/**
+ * Matches any letter ('a'-'z' and 'A'-'Z').
+ */
+protected 
+ALPHA options{ paraphrase = "a letter"; } 
+  : 'a'..'z' 
+  | 'A'..'Z'
+  ;
+  
+/**
+ * Matches the digits (0-9)
+ */
+protected 
+DIGIT options{ paraphrase = "a digit"; } 
+  : '0'..'9'
+  ;
+
+/**
+ * Matches the ':'
+ */
+COLON options{ paraphrase = "a comma"; } 
+  : ':'
+  ;
+
+/**
+ * Matches the ','
+ */
+COMMA options{ paraphrase = "a comma"; } 
+  : ','
+  ;
+
+/**
+ * Matches an identifier from the input. An identifier is a sequence of letters,
+ * digits and "_", "'", "." symbols, starting with a letter. 
+ */
+IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; }
+  : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
+  ;
+      
+/**
+ * Matches the left bracket ('(').
+ */
+LPAREN options { paraphrase = "a left parenthesis '('"; }      
+  : '(';
+  
+/**
+ * Matches the right bracket ('(').
+ */
+RPAREN options { paraphrase = "a right parenthesis ')'"; }  
+  : ')';
+
+/**
+ * Matches and skips whitespace in the input and ignores it. 
+ */
+WHITESPACE options { paraphrase = "whitespace"; }
+  : (' ' | '\t' | '\f')              { $setType(antlr::Token::SKIP); }
+  ;
+
+/**
+ * Mathces and skips the newline symbols in the input.
+ */
+NEWLINE options { paraphrase = "a newline"; }  
+  : ('\r' '\n' | '\r' | '\n')       { $setType(antlr::Token::SKIP); newline(); }
+  ;
+
+/**
+ * Mathces the comments and ignores them
+ */
+COMMENT options { paraphrase = "comment"; }
+  : ';' (~('\n' | '\r'))*                    { $setType(antlr::Token::SKIP); }
+  ;
+      
+/**
+ * Matches a numeral from the input (non-empty sequence of digits).
+ */
+NUMERAL options { paraphrase = "a numeral"; }
+  : (DIGIT)+
+  ;
+     
+\ No newline at end of file