blob: e9a58b1a922219ea3733c6815ca0a1f1a8cb3db1 (
plain)
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
|
/********************* -*- C++ -*- */
/** smtlib_scanner.lpp
** This file is part of the CVC4 prototype.
** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.
**
** Lexer for smtlib format.
**/
%option interactive
%option noyywrap
%option nounput
%option noreject
%option noyymore
%option yylineno
%option prefix="smtlib"
%{
#include <iostream>
#include "parser_state.h"
#include "smt/smt_engine.h"
#include "util/command.h"
#include "smtlib.hpp"
namespace CVC4 {
namespace parser {
extern ParserState* _global_parser_state;
}
}
using CVC4::parser::_global_parser_state;
extern char *smtlibtext;
// Redefine the input buffer function to read from an istream
#define YY_INPUT(buffer,result,max_size) result = _global_parser_state->read(buffer, max_size);
%}
%x COMMENT
%x STRING_LITERAL
//%x SYM_TOK
%x USER_VALUE
LETTER ([a-zA-Z])
DIGIT ([0-9])
OPCHAR (['\.\_])
IDCHAR ({LETTER}|{DIGIT}|{OPCHAR})
%%
[\n] { _global_parser_state->increaseLineNumber(); }
[ \t\r\f] { /* skip whitespace */ }
{DIGIT}+"\."{DIGIT}+ { smtliblval.p_string = new std::string(smtlibtext); return NUMERAL_TOK; }
{DIGIT}+ { smtliblval.p_string = new std::string(smtlibtext); return NUMERAL_TOK; }
";" { BEGIN COMMENT; }
<COMMENT>"\n" { BEGIN INITIAL; _global_parser_state->increaseLineNumber(); }
<COMMENT>. { /* stay in comment mode */ }
"\"" { BEGIN STRING_LITERAL; _global_parser_state->newStringLiteral(); }
<STRING_LITERAL>"\\". { _global_parser_state->appendCharToStringLiteral(smtlibtext, true); }
<STRING_LITERAL>"\"" { BEGIN INITIAL;
/* return to normal mode */
smtliblval.p_string = new std::string(_global_parser_state->getStringLiteral());
return STRING_TOK;
}
<STRING_LITERAL>. { _global_parser_state->appendCharToStringLiteral(smtlibtext, false); }
"{" { BEGIN USER_VALUE; _global_parser_state->newStringLiteral(); }
<USER_VALUE>"\\"[{}] { _global_parser_state->appendCharToStringLiteral(smtlibtext, true); }
<USER_VALUE>"}" { BEGIN INITIAL;
/* return to normal mode */
smtliblval.p_string = new std::string(_global_parser_state->getStringLiteral());
return USER_VAL_TOK;
}
<USER_VALUE>. { _global_parser_state->appendCharToStringLiteral(smtlibtext, false); }
"true" { return TRUE_TOK; }
"false" { return FALSE_TOK; }
"ite" { return ITE_TOK; }
"not" { return NOT_TOK; }
"implies" { return IMPLIES_TOK; }
"if_then_else" { return IF_THEN_ELSE_TOK; }
"and" { return AND_TOK; }
"or" { return OR_TOK; }
"xor" { return XOR_TOK; }
"iff" { return IFF_TOK; }
"let" { return LET_TOK; }
"flet" { return FLET_TOK; }
"notes" { return NOTES_TOK; }
"logic" { return LOGIC_TOK; }
"sat" { return SAT_TOK; }
"unsat" { return UNSAT_TOK; }
"unknown" { return UNKNOWN_TOK; }
"assumption" { return ASSUMPTION_TOK; }
"formula" { return FORMULA_TOK; }
"status" { return STATUS_TOK; }
"benchmark" { return BENCHMARK_TOK; }
"extrasorts" { return EXTRASORTS_TOK; }
"extrafuns" { return EXTRAFUNS_TOK; }
"extrapreds" { return EXTRAPREDS_TOK; }
"distinct" { return DISTINCT_TOK; }
":" { return COLON_TOK; }
"\[" { return LBRACKET_TOK; }
"\]" { return RBRACKET_TOK; }
"(" { return LPAREN_TOK; }
")" { return RPAREN_TOK; }
"$" { return DOLLAR_TOK; }
"?" { return QUESTION_TOK; }
({LETTER})({IDCHAR})* { smtliblval.p_string = new std::string(smtlibtext); return SYM_TOK; }
<<EOF>> { return EOF_TOK; }
. { _global_parser_state->parseError("Illegal input character."); }
%%
|
