diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-07 05:51:09 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-07 05:51:09 +0000 |
commit | b3bcafc179201e33c4f41ccf028c12eacc110d69 (patch) | |
tree | 6b35f7e654ac3b2278b9201db331fab980b32cd9 /src/parser/cvc/CvcLexer.g | |
parent | c16be5841e613818d5764e4de99e4694a0703685 (diff) |
antlr parser for the cvc4 language (boolean only)
yet to be finalized, it should work as expected
Diffstat (limited to 'src/parser/cvc/CvcLexer.g')
-rw-r--r-- | src/parser/cvc/CvcLexer.g | 127 |
1 files changed, 127 insertions, 0 deletions
diff --git a/src/parser/cvc/CvcLexer.g b/src/parser/cvc/CvcLexer.g new file mode 100644 index 000000000..8d706963f --- /dev/null +++ b/src/parser/cvc/CvcLexer.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 |