diff options
Diffstat (limited to 'lib/SMT/smtlib.lex')
| -rw-r--r-- | lib/SMT/smtlib.lex | 263 |
1 files changed, 0 insertions, 263 deletions
diff --git a/lib/SMT/smtlib.lex b/lib/SMT/smtlib.lex deleted file mode 100644 index c614c683..00000000 --- a/lib/SMT/smtlib.lex +++ /dev/null @@ -1,263 +0,0 @@ -%{ -/*****************************************************************************/ -/*! - * \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); } - -"BitVec" { return BITVEC_TOK; } - -"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; } - - -"bv"[0-9]+ { smtliblval.str = new std::string(smtlibtext); return BV_TOK; } -"bvbin"[0-1]+ { smtliblval.str = new std::string(smtlibtext); return BVBIN_TOK; } -"bvhex"[0-9,A-F,a-f]+ { smtliblval.str = new std::string(smtlibtext); return BVHEX_TOK; } - - -({LETTER})({IDCHAR})* {smtliblval.str = new std::string(smtlibtext); return SYM_TOK; } - -<<EOF>> { return EOF_TOK; } - -. { smtliberror("Illegal input character."); } -%% - |