diff options
Diffstat (limited to 'stp/parser/PL.lex')
| -rw-r--r-- | stp/parser/PL.lex | 128 |
1 files changed, 0 insertions, 128 deletions
diff --git a/stp/parser/PL.lex b/stp/parser/PL.lex deleted file mode 100644 index e9358a0e..00000000 --- a/stp/parser/PL.lex +++ /dev/null @@ -1,128 +0,0 @@ -%{ -/******************************************************************** - * AUTHORS: Vijay Ganesh, David L. Dill - * - * BEGIN DATE: November, 2005 - * - * LICENSE: Please view LICENSE file in the home dir of this Program - ********************************************************************/ -#include <iostream> -#include "../AST/AST.h" -#include "parsePL_defs.h" - -extern char *yytext; -extern int yyerror (const char *msg); -%} - -%option noyywrap -%option nounput -%option noreject -%option noyymore -%option yylineno -%x COMMENT -%x STRING_LITERAL -LETTER ([a-zA-Z]) -HEX ([0-9a-fA-F]) -BITS ([0-1]) -DIGIT ([0-9]) -OPCHAR (['?\_$]) -ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) -%% - -[()[\]{},.;:'!#?_=] { return yytext[0];} - -[\n] { /*Skip new line */ } -[ \t\r\f] { /* skip whitespace */ } -0b{BITS}+ { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+2, 2)); return BVCONST_TOK;} -0bin{BITS}+ { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+4, 2)); return BVCONST_TOK;} -0h{HEX}+ { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+2, 16)); return BVCONST_TOK;} -0hex{HEX}+ { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+4, 16)); return BVCONST_TOK;} -{DIGIT}+ { yylval.uintval = strtoul(yytext, NULL, 10); return NUMERAL_TOK;} - -"%" { BEGIN COMMENT;} -<COMMENT>"\n" { BEGIN INITIAL; /* return to normal mode */} -<COMMENT>. { /* stay in comment mode */} - -"ARRAY" { return ARRAY_TOK; } -"OF" { return OF_TOK; } -"WITH" { return WITH_TOK; } -"AND" { return AND_TOK;} -"NAND" { return NAND_TOK;} -"NOR" { return NOR_TOK;} -"NOT" { return NOT_TOK; } -"OR" { return OR_TOK; } -"/=" { return NEQ_TOK; } - ":=" { return ASSIGN_TOK;} -"=>" { return IMPLIES_TOK; } -"<=>" { return IFF_TOK; } -"XOR" { return XOR_TOK; } -"IF" { return IF_TOK; } -"THEN" { return THEN_TOK; } -"ELSE" { return ELSE_TOK; } -"ELSIF" { return ELSIF_TOK; } -"END" { return END_TOK; } -"ENDIF" { return ENDIF_TOK; } -"BV" { return BV_TOK;} -"BITVECTOR" { return BV_TOK;} -"BOOLEAN" { return BOOLEAN_TOK;} -"<<" { return BVLEFTSHIFT_TOK;} -">>" { return BVRIGHTSHIFT_TOK;} -"BVPLUS" { return BVPLUS_TOK;} -"BVSUB" { return BVSUB_TOK;} -"BVUMINUS" { return BVUMINUS_TOK;} -"BVMULT" { return BVMULT_TOK;} -"BVDIV" { return BVDIV_TOK;} -"BVMOD" { return BVMOD_TOK;} -"SBVDIV" { return SBVDIV_TOK;} -"SBVMOD" { return SBVMOD_TOK;} -"~" { return BVNEG_TOK;} -"&" { return BVAND_TOK;} -"|" { return BVOR_TOK;} -"BVXOR" { return BVXOR_TOK;} -"BVNAND" { return BVNAND_TOK;} -"BVNOR" { return BVNOR_TOK;} -"BVXNOR" { return BVXNOR_TOK;} -"@" { return BVCONCAT_TOK;} -"BVLT" { return BVLT_TOK;} -"BVGT" { return BVGT_TOK;} -"BVLE" { return BVLE_TOK;} -"BVGE" { return BVGE_TOK;} -"BVSLT" { return BVSLT_TOK;} -"BVSGT" { return BVSGT_TOK;} -"BVSLE" { return BVSLE_TOK;} -"BVSGE" { return BVSGE_TOK;} -"BVSX" { return BVSX_TOK;} -"SBVLT" { return BVSLT_TOK;} -"SBVGT" { return BVSGT_TOK;} -"SBVLE" { return BVSLE_TOK;} -"SBVGE" { return BVSGE_TOK;} -"SX" { return BVSX_TOK;} -"BOOLEXTRACT" { return BOOLEXTRACT_TOK;} -"BOOLBV" { return BOOL_TO_BV_TOK;} -"ASSERT" { return ASSERT_TOK; } -"QUERY" { return QUERY_TOK; } -"FALSE" { return FALSELIT_TOK;} -"TRUE" { return TRUELIT_TOK;} -"IN" { return IN_TOK;} -"LET" { return LET_TOK;} -"COUNTEREXAMPLE" { return COUNTEREXAMPLE_TOK;} -"COUNTERMODEL" { return COUNTEREXAMPLE_TOK;} - "PUSH" { return PUSH_TOK;} - "POP" { return POP_TOK;} - -(({LETTER})|(_)({ANYTHING}))({ANYTHING})* { - BEEV::ASTNode nptr = BEEV::globalBeevMgr_for_parser->CreateSymbol(yytext); - - // Check valuesize to see if it's a prop var. I don't like doing - // type determination in the lexer, but it's easier than rewriting - // the whole grammar to eliminate the term/formula distinction. - yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(nptr)); - //yylval.node = new BEEV::ASTNode(nptr); - if ((yylval.node)->GetType() == BEEV::BOOLEAN_TYPE) - return FORMID_TOK; - else - return TERMID_TOK; -} - -. { yyerror("Illegal input character."); } -%% |