path: root/lib/SMT/smtlib.lex

%{
/*****************************************************************************/
/*!
 * \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 "SMTParser.h"
#include "smtlib_parser.h"

using namespace klee;
using namespace klee::expr;

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) {
    // 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(*SMTParser::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 SMTParser. */
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 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]            { SMTParser::parserTemp->lineNum++; }
[ \t\r\f]	{ /* skip whitespace */ }

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

";"		{ BEGIN COMMENT; }
<COMMENT>"\n"	{ BEGIN INITIAL; /* return to normal mode */ 
                  SMTParser::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');
                          SMTParser::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; }
"sorts"         { return SORTS_TOK; }
"funs"          { return FUNS_TOK; }
"preds"         { return PREDS_TOK; }
"extensions"    { return EXTENSIONS_TOK; }
"definition"    { return DEFINITION_TOK; }
"axioms"        { return AXIOMS_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; }
"language"      { return LANGUAGE_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; }


"bit0"          { return BIT0_TOK; }
"bit1"          { return BIT1_TOK; }

"concat"        { return BVCONCAT_TOK; }
"extract"       { return BVEXTRACT_TOK; }

"bvnot"         { return BVNOT_TOK; }
"bvand"         { return BVAND_TOK; }
"bvor"          { return BVOR_TOK; }
"bvneg"         { return BVNEG_TOK; }
"bvnand"        { return BVNAND_TOK; }
"bvnor"         { return BVNOR_TOK; }
"bvxor"         { return BVXOR_TOK; }
"bvxnor"        { return BVXNOR_TOK; }

"="             { return EQ_TOK; }
"bvcomp"        { return BVCOMP_TOK; }
"bvult"         { return BVULT_TOK; }
"bvule"         { return BVULE_TOK; }
"bvugt"         { return BVUGT_TOK; }
"bvuge"         { return BVUGE_TOK; }
"bvslt"         { return BVSLT_TOK; }
"bvsle"         { return BVSLE_TOK; }
"bvsgt"         { return BVSGT_TOK; }
"bvsge"         { return BVSGE_TOK; }

"bvadd"         { return BVADD_TOK; }
"bvsub"         { return BVSUB_TOK; }
"bvmul"         { return BVMUL_TOK; }
"bvudiv"        { return BVUDIV_TOK; }
"bvurem"        { return BVUREM_TOK; }
"bvsdiv"        { return BVSDIV_TOK; }
"bvsrem"        { return BVSREM_TOK; }
"bvsmod"        { return BVSMOD_TOK; }

"bvshl"         { return BVSHL_TOK; }
"bvlshr"        { return BVLSHR_TOK; }
"bvashr"        { return BVASHR_TOK; }

"repeat"        { return REPEAT_TOK; }
"zero_extend"   { return ZEXT_TOK; }
"sign_extend"   { return SEXT_TOK; }
"rotate_left"   { return ROL_TOK; }
"rotate_right"  { return ROR_TOK; }


({LETTER})({IDCHAR})* {smtliblval.str = new std::string(smtlibtext); return SYM_TOK; }

<<EOF>>         { return EOF_TOK; }

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