path: root/src/parser/smtlib_scanner.lpp

%{
/*****************************************************************************/
/*!
 * \file smtlib.lex
 * 
 * Author: Clark Barrett
 * 
 * Created: 2005
 *
 * <hr>
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/

#include <iostream>
#include "parser_temp.h"
#include "expr_manager.h" /* for the benefit of parsesmtlib_defs.h */
#include "parsesmtlib_defs.h"
#include "debug.h"

namespace CVC4 {
  extern ParserTemp* parserTemp;
}

/* prefixing hack from gdb (via automake docs) */
#define	yymaxdepth smtlib_maxdepth
#define	yyparse	smtlib_parse
#define	yylex	smtlib_lex
#define	yyerror	smtlib_error
#define	yylval	smtlib_lval
#define	yychar	smtlib_char
#define	yydebug	smtlib_debug
#define	yypact	smtlib_pact	
#define	yyr1	smtlib_r1			
#define	yyr2	smtlib_r2			
#define	yydef	smtlib_def		
#define	yychk	smtlib_chk		
#define	yypgo	smtlib_pgo		
#define	yyact	smtlib_act		
#define	yyexca	smtlib_exca
#define yyerrflag smtlib_errflag
#define yynerrs	smtlib_nerrs
#define	yyps	smtlib_ps
#define	yypv	smtlib_pv
#define	yys	smtlib_s
#define	yy_yys	smtlib_yys
#define	yystate	smtlib_state
#define	yytmp	smtlib_tmp
#define	yyv	smtlib_v
#define	yy_yyv	smtlib_yyv
#define	yyval	smtlib_val
#define	yylloc	smtlib_lloc
#define yyreds	smtlib_reds
#define yytoks	smtlib_toks
#define yylhs	smtlib_yylhs
#define yylen	smtlib_yylen
#define yydefred smtlib_yydefred
#define yydgoto	smtlib_yydgoto
#define yysindex smtlib_yysindex
#define yyrindex smtlib_yyrindex
#define yygindex smtlib_yygindex
#define yytable	 smtlib_yytable
#define yycheck	 smtlib_yycheck
#define yyname   smtlib_yyname
#define yyrule   smtlib_yyrule

extern int smtlib_inputLine;
extern char *smtlibtext;

extern int smtliberror (const char *msg);

static int smtlibinput(std::istream& is, char* buf, int size) {
  int res;
  if(is) {
    // If interactive, read line by line; otherwise read as much as we
    // can gobble
    if(CVC4::parserTemp->interactive) {
      // Print the current prompt
      std::cout << CVC4::parserTemp->getPrompt() << std::flush;
      // Set the prompt to "middle of the command" one
      CVC4::parserTemp->setPrompt2();
      // Read the line
      is.getline(buf, size-1);
    } else // Set the terminator char to 0
      is.getline(buf, size-1, 0);
    // If failbit is set, but eof is not, it means the line simply
    // didn't fit; so we clear the state and keep on reading.
    bool partialStr = is.fail() && !is.eof();
    if(partialStr)
      is.clear();

    for(res = 0; res<size && buf[res] != 0; res++);
    if(res == size) smtliberror("Lexer bug: overfilled the buffer");
    if(!partialStr) { // Insert \n into the buffer
      buf[res++] = '\n';
      buf[res] = '\0';
    }
  } else {
    res = YY_NULL;
  }
  return res;
}

// Redefine the input buffer function to read from an istream
#define YY_INPUT(buf,result,max_size) \
  result = smtlibinput(*CVC4::parserTemp->is, buf, max_size);

int smtlib_bufSize() { return YY_BUF_SIZE; }
YY_BUFFER_STATE smtlib_buf_state() { return YY_CURRENT_BUFFER; }

/* some wrappers for methods that need to refer to a struct.
   These are used by CVC4::Parser. */
void *smtlib_createBuffer(int sz) {
  return (void *)smtlib_create_buffer(NULL, sz);
}
void smtlib_deleteBuffer(void *buf_state) {
  smtlib_delete_buffer((struct yy_buffer_state *)buf_state);
}
void smtlib_switchToBuffer(void *buf_state) {
  smtlib_switch_to_buffer((struct yy_buffer_state *)buf_state);
}
void *smtlib_bufState() {
  return (void *)smtlib_buf_state();
}

void smtlib_setInteractive(bool is_interactive) {
  yy_set_interactive(is_interactive);
}

// File-static (local to this file) variables and functions
static std::string _string_lit;

 static char escapeChar(char c) {
   switch(c) {
   case 'n': return '\n';
   case 't': return '\t';
   default: return c;
   }
 }

// for now, we don't have subranges.  
//
// ".."		{ return DOTDOT_TOK; }
/*OPCHAR	(['!#?\_$&\|\\@])*/

%}

%option interactive
%option noyywrap
%option nounput
%option noreject
%option noyymore
%option yylineno

%x	COMMENT
%x	STRING_LITERAL
%x      USER_VALUE
%s      PAT_MODE

LETTER	([a-zA-Z])
DIGIT	([0-9])
OPCHAR	(['\.\_])
IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
%%

[\n]            { CVC4::parserTemp->lineNum++; }
[ \t\r\f]	{ /* skip whitespace */ }

{DIGIT}+"\."{DIGIT}+ { smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; }
{DIGIT}+	{ smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; 
		}

";"		{ BEGIN COMMENT; }
<COMMENT>"\n"	{ BEGIN INITIAL; /* return to normal mode */ 
                  CVC4::parserTemp->lineNum++; }
<COMMENT>.	{ /* stay in comment mode */ }

<INITIAL>"\""		{ BEGIN STRING_LITERAL; 
                          _string_lit.erase(_string_lit.begin(),
                                            _string_lit.end()); }
<STRING_LITERAL>"\\".	{ /* escape characters (like \n or \") */
                          _string_lit.insert(_string_lit.end(),
                                             escapeChar(smtlibtext[1])); }
<STRING_LITERAL>"\""	{ BEGIN INITIAL; /* return to normal mode */ 
			  smtliblval.str = new std::string(_string_lit);
                          return STRING_TOK; }
<STRING_LITERAL>.	{ _string_lit.insert(_string_lit.end(),*smtlibtext); }

<INITIAL>":pat"		{ BEGIN PAT_MODE;
                          return PAT_TOK;}
<PAT_MODE>"}"	        { BEGIN INITIAL; 
                          return RCURBRACK_TOK; }
<INITIAL>"{"		{ BEGIN USER_VALUE;
                          _string_lit.erase(_string_lit.begin(),
                                            _string_lit.end()); }
<USER_VALUE>"\\"[{}] { /* escape characters */
                          _string_lit.insert(_string_lit.end(),smtlibtext[1]); }

<USER_VALUE>"}"	        { BEGIN INITIAL; /* return to normal mode */ 
			  smtliblval.str = new std::string(_string_lit);
                          return USER_VAL_TOK; }

<USER_VALUE>"\n"        { _string_lit.insert(_string_lit.end(),'\n');
                          CVC4::parserTemp->lineNum++; }
<USER_VALUE>.	        { _string_lit.insert(_string_lit.end(),*smtlibtext); }

"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; }
"exists"        { return EXISTS_TOK; }
"forall"        { return FORALL_TOK; }
"let"           { return LET_TOK; }
"flet"          { return FLET_TOK; }
"notes"         { return NOTES_TOK; }
"cvc_command"   { return CVC_COMMAND_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; }
":pattern"      { return PAT_TOK; } 
":"             { return COLON_TOK; }
"\["            { return LBRACKET_TOK; }
"\]"            { return RBRACKET_TOK; }
"{"             { return LCURBRACK_TOK;}
"}"             { return RCURBRACK_TOK;}
"("             { return LPAREN_TOK; }
")"             { return RPAREN_TOK; }
"$"             { return DOLLAR_TOK; }
"?"             { return QUESTION_TOK; }

[=<>&@#+\-*/%|~]+ { smtliblval.str = new std::string(smtlibtext); return AR_SYMB; }
({LETTER})({IDCHAR})* {smtliblval.str = new std::string(smtlibtext); return SYM_TOK; }

<<EOF>>         { return EOF_TOK; }

. { smtliberror("Illegal input character."); }
%%