blob: e9358a0e521dddf67586aad42961d810cc0447b0 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
|
%{
/********************************************************************
* 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."); }
%%
|
