/*********************                                           -*- 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 "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."); }

%%