src/parser/smtlib_scanner.lpp

   1 %{
   2 /*****************************************************************************/
   3 /*!
   4  * \file smtlib.lex
   5  *
   6  * Author: Clark Barrett
   7  *
   8  * Created: 2005
   9  *
  10  * <hr>
  11  *
  12  * License to use, copy, modify, sell and/or distribute this software
  13  * and its documentation for any purpose is hereby granted without
  14  * royalty, subject to the terms and conditions defined in the \ref
  15  * LICENSE file provided with this distribution.
  16  *
  17  * <hr>
  18  *
  19  */
  20 /*****************************************************************************/
  21
  22 #include <iostream>
  23 #include "parser_temp.h"
  24 #include "expr_manager.h" /* for the benefit of parsesmtlib_defs.h */
  25 #include "parsesmtlib_defs.h"
  26 #include "debug.h"
  27
  28 namespace CVC4 {
  29   extern ParserTemp* parserTemp;
  30 }
  31
  32 /* prefixing hack from gdb (via automake docs) */
  33 #define yymaxdepth smtlib_maxdepth
  34 #define yyparse smtlib_parse
  35 #define yylex   smtlib_lex
  36 #define yyerror smtlib_error
  37 #define yylval  smtlib_lval
  38 #define yychar  smtlib_char
  39 #define yydebug smtlib_debug
  40 #define yypact  smtlib_pact
  41 #define yyr1    smtlib_r1
  42 #define yyr2    smtlib_r2
  43 #define yydef   smtlib_def
  44 #define yychk   smtlib_chk
  45 #define yypgo   smtlib_pgo
  46 #define yyact   smtlib_act
  47 #define yyexca  smtlib_exca
  48 #define yyerrflag smtlib_errflag
  49 #define yynerrs smtlib_nerrs
  50 #define yyps    smtlib_ps
  51 #define yypv    smtlib_pv
  52 #define yys     smtlib_s
  53 #define yy_yys  smtlib_yys
  54 #define yystate smtlib_state
  55 #define yytmp   smtlib_tmp
  56 #define yyv     smtlib_v
  57 #define yy_yyv  smtlib_yyv
  58 #define yyval   smtlib_val
  59 #define yylloc  smtlib_lloc
  60 #define yyreds  smtlib_reds
  61 #define yytoks  smtlib_toks
  62 #define yylhs   smtlib_yylhs
  63 #define yylen   smtlib_yylen
  64 #define yydefred smtlib_yydefred
  65 #define yydgoto smtlib_yydgoto
  66 #define yysindex smtlib_yysindex
  67 #define yyrindex smtlib_yyrindex
  68 #define yygindex smtlib_yygindex
  69 #define yytable  smtlib_yytable
  70 #define yycheck  smtlib_yycheck
  71 #define yyname   smtlib_yyname
  72 #define yyrule   smtlib_yyrule
  73
  74 extern int smtlib_inputLine;
  75 extern char *smtlibtext;
  76
  77 extern int smtliberror (const char *msg);
  78
  79 static int smtlibinput(std::istream& is, char* buf, int size) {
  80   int res;
  81   if(is) {
  82     // If interactive, read line by line; otherwise read as much as we
  83     // can gobble
  84     if(CVC4::parserTemp->interactive) {
  85       // Print the current prompt
  86       std::cout << CVC4::parserTemp->getPrompt() << std::flush;
  87       // Set the prompt to "middle of the command" one
  88       CVC4::parserTemp->setPrompt2();
  89       // Read the line
  90       is.getline(buf, size-1);
  91     } else // Set the terminator char to 0
  92       is.getline(buf, size-1, 0);
  93     // If failbit is set, but eof is not, it means the line simply
  94     // didn't fit; so we clear the state and keep on reading.
  95     bool partialStr = is.fail() && !is.eof();
  96     if(partialStr)
  97       is.clear();
  98
  99     for(res = 0; res<size && buf[res] != 0; res++);
 100     if(res == size) smtliberror("Lexer bug: overfilled the buffer");
 101     if(!partialStr) { // Insert \n into the buffer
 102       buf[res++] = '\n';
 103       buf[res] = '\0';
 104     }
 105   } else {
 106     res = YY_NULL;
 107   }
 108   return res;
 109 }
 110
 111 // Redefine the input buffer function to read from an istream
 112 #define YY_INPUT(buf,result,max_size) \
 113   result = smtlibinput(*CVC4::parserTemp->is, buf, max_size);
 114
 115 int smtlib_bufSize() { return YY_BUF_SIZE; }
 116 YY_BUFFER_STATE smtlib_buf_state() { return YY_CURRENT_BUFFER; }
 117
 118 /* some wrappers for methods that need to refer to a struct.
 119    These are used by CVC4::Parser. */
 120 void *smtlib_createBuffer(int sz) {
 121   return (void *)smtlib_create_buffer(NULL, sz);
 122 }
 123 void smtlib_deleteBuffer(void *buf_state) {
 124   smtlib_delete_buffer((struct yy_buffer_state *)buf_state);
 125 }
 126 void smtlib_switchToBuffer(void *buf_state) {
 127   smtlib_switch_to_buffer((struct yy_buffer_state *)buf_state);
 128 }
 129 void *smtlib_bufState() {
 130   return (void *)smtlib_buf_state();
 131 }
 132
 133 void smtlib_setInteractive(bool is_interactive) {
 134   yy_set_interactive(is_interactive);
 135 }
 136
 137 // File-static (local to this file) variables and functions
 138 static std::string _string_lit;
 139
 140  static char escapeChar(char c) {
 141    switch(c) {
 142    case 'n': return '\n';
 143    case 't': return '\t';
 144    default: return c;
 145    }
 146  }
 147
 148 // for now, we don't have subranges.
 149 //
 150 // ".."         { return DOTDOT_TOK; }
 151 /*OPCHAR        (['!#?\_$&\|\\@])*/
 152
 153 %}
 154
 155 %option interactive
 156 %option noyywrap
 157 %option nounput
 158 %option noreject
 159 %option noyymore
 160 %option yylineno
 161
 162 %x      COMMENT
 163 %x      STRING_LITERAL
 164 %x      USER_VALUE
 165 %s      PAT_MODE
 166
 167 LETTER  ([a-zA-Z])
 168 DIGIT   ([0-9])
 169 OPCHAR  (['\.\_])
 170 IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
 171 %%
 172
 173 [\n]            { CVC4::parserTemp->lineNum++; }
 174 [ \t\r\f]       { /* skip whitespace */ }
 175
 176 {DIGIT}+"\."{DIGIT}+ { smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; }
 177 {DIGIT}+        { smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK;
 178                 }
 179
 180 ";"             { BEGIN COMMENT; }
 181 <COMMENT>"\n"   { BEGIN INITIAL; /* return to normal mode */
 182                   CVC4::parserTemp->lineNum++; }
 183 <COMMENT>.      { /* stay in comment mode */ }
 184
 185 <INITIAL>"\""           { BEGIN STRING_LITERAL;
 186                           _string_lit.erase(_string_lit.begin(),
 187                                             _string_lit.end()); }
 188 <STRING_LITERAL>"\\".   { /* escape characters (like \n or \") */
 189                           _string_lit.insert(_string_lit.end(),
 190                                              escapeChar(smtlibtext[1])); }
 191 <STRING_LITERAL>"\""    { BEGIN INITIAL; /* return to normal mode */
 192                           smtliblval.str = new std::string(_string_lit);
 193                           return STRING_TOK; }
 194 <STRING_LITERAL>.       { _string_lit.insert(_string_lit.end(),*smtlibtext); }
 195
 196 <INITIAL>":pat"         { BEGIN PAT_MODE;
 197                           return PAT_TOK;}
 198 <PAT_MODE>"}"           { BEGIN INITIAL;
 199                           return RCURBRACK_TOK; }
 200 <INITIAL>"{"            { BEGIN USER_VALUE;
 201                           _string_lit.erase(_string_lit.begin(),
 202                                             _string_lit.end()); }
 203 <USER_VALUE>"\\"[{}] { /* escape characters */
 204                           _string_lit.insert(_string_lit.end(),smtlibtext[1]); }
 205
 206 <USER_VALUE>"}"         { BEGIN INITIAL; /* return to normal mode */
 207                           smtliblval.str = new std::string(_string_lit);
 208                           return USER_VAL_TOK; }
 209
 210 <USER_VALUE>"\n"        { _string_lit.insert(_string_lit.end(),'\n');
 211                           CVC4::parserTemp->lineNum++; }
 212 <USER_VALUE>.           { _string_lit.insert(_string_lit.end(),*smtlibtext); }
 213
 214 "true"          { return TRUE_TOK; }
 215 "false"         { return FALSE_TOK; }
 216 "ite"           { return ITE_TOK; }
 217 "not"           { return NOT_TOK; }
 218 "implies"       { return IMPLIES_TOK; }
 219 "if_then_else"  { return IF_THEN_ELSE_TOK; }
 220 "and"           { return AND_TOK; }
 221 "or"            { return OR_TOK; }
 222 "xor"           { return XOR_TOK; }
 223 "iff"           { return IFF_TOK; }
 224 "exists"        { return EXISTS_TOK; }
 225 "forall"        { return FORALL_TOK; }
 226 "let"           { return LET_TOK; }
 227 "flet"          { return FLET_TOK; }
 228 "notes"         { return NOTES_TOK; }
 229 "cvc_command"   { return CVC_COMMAND_TOK; }
 230 "logic"         { return LOGIC_TOK; }
 231 "sat"           { return SAT_TOK; }
 232 "unsat"         { return UNSAT_TOK; }
 233 "unknown"       { return UNKNOWN_TOK; }
 234 "assumption"    { return ASSUMPTION_TOK; }
 235 "formula"       { return FORMULA_TOK; }
 236 "status"        { return STATUS_TOK; }
 237 "benchmark"     { return BENCHMARK_TOK; }
 238 "extrasorts"    { return EXTRASORTS_TOK; }
 239 "extrafuns"     { return EXTRAFUNS_TOK; }
 240 "extrapreds"    { return EXTRAPREDS_TOK; }
 241 "distinct"      { return DISTINCT_TOK; }
 242 ":pattern"      { return PAT_TOK; }
 243 ":"             { return COLON_TOK; }
 244 "\["            { return LBRACKET_TOK; }
 245 "\]"            { return RBRACKET_TOK; }
 246 "{"             { return LCURBRACK_TOK;}
 247 "}"             { return RCURBRACK_TOK;}
 248 "("             { return LPAREN_TOK; }
 249 ")"             { return RPAREN_TOK; }
 250 "$"             { return DOLLAR_TOK; }
 251 "?"             { return QUESTION_TOK; }
 252
 253 [=<>&@#+\-*/%|~]+ { smtliblval.str = new std::string(smtlibtext); return AR_SYMB; }
 254 ({LETTER})({IDCHAR})* {smtliblval.str = new std::string(smtlibtext); return SYM_TOK; }
 255
 256 <<EOF>>         { return EOF_TOK; }
 257
 258 . { smtliberror("Illegal input character."); }
 259 %%
 260