diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-17 07:19:39 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-17 07:19:39 +0000 |
commit | acd68152ff9600bdff208376f2cd43f09d45cdc8 (patch) | |
tree | 978e80b102b5cad5e169bd0808e7b53b0911b2e6 /src/parser | |
parent | 4081193ea4337de29755a61bf04aa44305a9e789 (diff) |
fixes and additions
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/Makefile.am | 25 | ||||
-rw-r--r-- | src/parser/parser_state.h | 89 | ||||
-rw-r--r-- | src/parser/pl.ypp | 55 | ||||
-rw-r--r-- | src/parser/pl_scanner.lpp | 105 | ||||
-rw-r--r-- | src/parser/smtlib.ypp | 69 | ||||
-rw-r--r-- | src/parser/smtlib_scanner.lpp | 93 |
6 files changed, 208 insertions, 228 deletions
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 0ebcad8c7..8cf9f4a6d 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -10,9 +10,26 @@ libparser_a_SOURCES = \ parser.cpp BUILT_SOURCES = \ - pl_scanner.lpp \ - pl.ypp \ - smtlib_scanner.lpp \ - smtlib.ypp + pl_scanner.cpp \ + pl.cpp \ + pl.h \ + smtlib_scanner.cpp \ + smtlib.cpp \ + smtlib.h + +# produce headers too +AM_YFLAGS = -d + +pl_scanner.cpp: pl_scanner.lpp + $(LEX) $(AM_LFLAGS) $(LFLAGS) -P PL -o $@ $< +smtlib_scanner.cpp: smtlib_scanner.lpp + $(LEX) $(AM_LFLAGS) $(LFLAGS) -P smtlib -o $@ $< + +pl_scanner.o: pl.h +pl.cpp: pl.ypp + $(YACC) $(AM_YFLAGS) $(YFLAGS) -p PL -o $@ $< +smtlib_scanner.o: smtlib.h +smtlib.cpp: smtlib.ypp + $(YACC) $(AM_YFLAGS) $(YFLAGS) -p smtlib -o $@ $< diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h new file mode 100644 index 000000000..4444925e2 --- /dev/null +++ b/src/parser/parser_state.h @@ -0,0 +1,89 @@ +/********************* -*- C++ -*- */ +/** parser_state.h + ** This file is part of the CVC4 prototype. + ** + ** Extra state of the parser shared by the lexer and parser. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_PARSER_STATE_H +#define __CVC4_PARSER_STATE_H + +#include <iostream> +#include <sstream> +#include "expr.h" +#include "exception.h" + +namespace CVC4 { + +class ValidityChecker; + +class ParserState { +private: + // Counter for uniqueID of bound variables + int d_uid; + // The main prompt when running interactive + std::string prompt1; + // The interactive prompt in the middle of a multi-line command + std::string prompt2; + // The currently used prompt + std::string prompt; +public: + ValidityChecker* vc; + std::istream* is; + // The current input line + int lineNum; + // File name + std::string fileName; + // The last parsed Expr + Expr expr; + // Whether we are done or not + bool done; + // Whether we are running interactive + bool interactive; + // Whether arrays are enabled for smt-lib format + bool arrFlag; + // Whether bit-vectors are enabled for smt-lib format + bool bvFlag; + // Size of bit-vectors for smt-lib format + int bvSize; + // Did we encounter a formula query (smtlib) + bool queryParsed; + // Default constructor + ParserState() : d_uid(0), + prompt1("CVC> "), + prompt2("- "), + prompt("CVC> "), + vc(0), + is(0), + lineNum(1), + fileName(), + expr(Expr::null()), + done(false), + interactive(false), + arrFlag(false), + bvFlag(false), + bvSize(0), + queryParsed(false) { } + // Parser error handling (implemented in parser.cpp) + int error(const std::string& s); + // Get the next uniqueID as a string + std::string uniqueID() { + std::ostringstream ss; + ss << d_uid++; + return ss.str(); + } + // Get the current prompt + std::string getPrompt() { return prompt; } + // Set the prompt to the main one + void setPrompt1() { prompt = prompt1; } + // Set the prompt to the secondary one + void setPrompt2() { prompt = prompt2; } +}; + +} /* CVC4 namespace */ + +#endif /* __CVC4_PARSER_STATE_H */ diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp index dfed55dbb..e9aeab78e 100644 --- a/src/parser/pl.ypp +++ b/src/parser/pl.ypp @@ -1,43 +1,32 @@ +/********************* -*- C++ -*- */ +/** smtlib.ypp + ** This file is part of the CVC4 prototype. + ** + ** Reference-counted encapsulation of a pointer to an expression. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** + ** This file contains the bison code for the parser that reads in CVC + ** commands in the presentation language (hence "PL"). + **/ + %{ -/*****************************************************************************/ -/*! - * \file PL.y - * - * Author: Sergey Berezin - * - * Created: Feb 06 03:00:43 GMT 2003 - * - * <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> - * - */ -/*****************************************************************************/ -/* PL.y - Aaron Stump, 4/14/01 - - This file contains the bison code for the parser that reads in CVC - commands in the presentation language (hence "PL"). -*/ #include "vc.h" #include "parser_exception.h" -#include "parser_temp.h" -#include "rational.h" +#include "parser_state.h" +//#include "rational.h" // Exported shared data namespace CVC4 { - extern ParserTemp* parserTemp; + extern ParserState* parserState; } // Define shortcuts for various things -#define TMP CVC4::parserTemp -#define EXPR CVC4::parserTemp->expr -#define VC (CVC4::parserTemp->vc) +#define TMP CVC4::parserState +#define EXPR CVC4::parserState->expr +#define VC (CVC4::parserState->vc) #define RAT(args) CVC4::newRational args // Suppress the bogus warning suppression in bison (it generates @@ -50,9 +39,9 @@ extern int PLlex(void); int PLerror(const char *s) { std::ostringstream ss; - ss << CVC4::parserTemp->fileName << ":" << CVC4::parserTemp->lineNum + ss << CVC4::parserState->fileName << ":" << CVC4::parserState->lineNum << ": " << s; - return CVC4::parserTemp->error(ss.str()); + return CVC4::parserState->error(ss.str()); } diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp index d203a1e9a..d70937e34 100644 --- a/src/parser/pl_scanner.lpp +++ b/src/parser/pl_scanner.lpp @@ -1,76 +1,34 @@ +/********************* -*- C++ -*- */ +/** pl_scanner.lpp + ** This file is part of the CVC4 prototype. + ** + ** Reference-counted encapsulation of a pointer to an expression. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +%option interactive +%option noyywrap +%option nounput +%option noreject +%option noyymore +%option yylineno +%option prefix="PL" + %{ -/*****************************************************************************/ -/*! - * \file PL.lex - * - * Author: Sergey Berezin - * - * Created: Feb 06 03:00:43 GMT 2003 - * - * <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 parsePL_defs.h */ -#include "parsePL_defs.h" +#include "parser_state.h" +#include "pl.h" #include "debug.h" namespace CVC4 { - extern ParserTemp* parserTemp; + extern ParserState* parserState; } -/* prefixing hack from gdb (via automake docs) */ -#define yymaxdepth PL_maxdepth -#define yyparse PL_parse -#define yylex PL_lex -#define yyerror PL_error -#define yylval PL_lval -#define yychar PL_char -#define yydebug PL_debug -#define yypact PL_pact -#define yyr1 PL_r1 -#define yyr2 PL_r2 -#define yydef PL_def -#define yychk PL_chk -#define yypgo PL_pgo -#define yyact PL_act -#define yyexca PL_exca -#define yyerrflag PL_errflag -#define yynerrs PL_nerrs -#define yyps PL_ps -#define yypv PL_pv -#define yys PL_s -#define yy_yys PL_yys -#define yystate PL_state -#define yytmp PL_tmp -#define yyv PL_v -#define yy_yyv PL_yyv -#define yyval PL_val -#define yylloc PL_lloc -#define yyreds PL_reds -#define yytoks PL_toks -#define yylhs PL_yylhs -#define yylen PL_yylen -#define yydefred PL_yydefred -#define yydgoto PL_yydgoto -#define yysindex PL_yysindex -#define yyrindex PL_yyrindex -#define yygindex PL_yygindex -#define yytable PL_yytable -#define yycheck PL_yycheck -#define yyname PL_yyname -#define yyrule PL_yyrule - extern int PL_inputLine; extern char *PLtext; @@ -81,11 +39,11 @@ static int PLinput(std::istream& is, char* buf, int size) { if(is) { // If interactive, read line by line; otherwise read as much as we // can gobble - if(CVC4::parserTemp->interactive) { + if(CVC4::parserState->interactive) { // Print the current prompt - std::cout << CVC4::parserTemp->getPrompt() << std::flush; + std::cout << CVC4::parserState->getPrompt() << std::flush; // Set the prompt to "middle of the command" one - CVC4::parserTemp->setPrompt2(); + CVC4::parserState->setPrompt2(); // Read the line is.getline(buf, size-1); } else // Set the terminator char to 0 @@ -110,7 +68,7 @@ static int PLinput(std::istream& is, char* buf, int size) { // Redefine the input buffer function to read from an istream #define YY_INPUT(buf,result,max_size) \ - result = PLinput(*CVC4::parserTemp->is, buf, max_size); + result = PLinput(*CVC4::parserState->is, buf, max_size); int PL_bufSize() { return YY_BUF_SIZE; } YY_BUFFER_STATE PL_buf_state() { return YY_CURRENT_BUFFER; } @@ -152,13 +110,6 @@ static std::string _string_lit; %} -%option interactive -%option noyywrap -%option nounput -%option noreject -%option noyymore -%option yylineno - %x COMMENT %x STRING_LITERAL @@ -171,7 +122,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) %% -[\n] { CVC4::parserTemp->lineNum++; } +[\n] { CVC4::parserState->lineNum++; } [ \t\r\f] { /* skip whitespace */ } @@ -184,7 +135,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) "%" { BEGIN COMMENT; } <COMMENT>"\n" { BEGIN INITIAL; /* return to normal mode */ - CVC4::parserTemp->lineNum++; } + CVC4::parserState->lineNum++; } <COMMENT>. { /* stay in comment mode */ } <INITIAL>"\"" { BEGIN STRING_LITERAL; diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp index 1bc22675a..97f61e715 100644 --- a/src/parser/smtlib.ypp +++ b/src/parser/smtlib.ypp @@ -1,45 +1,34 @@ -%{ -/*****************************************************************************/ -/*! - * \file smtlib.y - * - * Author: Clark Barrett - * - * Created: Apr 30 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> - * - */ -/*****************************************************************************/ -/* - This file contains the bison code for the parser that reads in CVC - commands in SMT-LIB language. -*/ +%{/******************* -*- C++ -*- */ +/** smtlib.ypp + ** This file is part of the CVC4 prototype. + ** + ** Reference-counted encapsulation of a pointer to an expression. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** + ** This file contains the bison code for the parser that reads in CVC + ** commands in SMT-LIB language. + **/ #include "vc.h" #include "parser_exception.h" -#include "parser_temp.h" +#include "parser_state.h" // Exported shared data -namespace CVC4 { +namespace CVC3 { extern ParserTemp* parserTemp; } // Define shortcuts for various things -#define TMP CVC4::parserTemp -#define EXPR CVC4::parserTemp->expr -#define VC (CVC4::parserTemp->vc) -#define ARRAYSENABLED (CVC4::parserTemp->arrFlag) -#define BVENABLED (CVC4::parserTemp->bvFlag) -#define BVSIZE (CVC4::parserTemp->bvSize) -#define RAT(args) CVC4::newRational args -#define QUERYPARSED CVC4::parserTemp->queryParsed +#define TMP CVC3::parserTemp +#define EXPR CVC3::parserTemp->expr +#define VC (CVC3::parserTemp->vc) +#define ARRAYSENABLED (CVC3::parserTemp->arrFlag) +#define BVENABLED (CVC3::parserTemp->bvFlag) +#define BVSIZE (CVC3::parserTemp->bvSize) +#define RAT(args) CVC3::newRational args +#define QUERYPARSED CVC3::parserTemp->queryParsed // Suppress the bogus warning suppression in bison (it generates // compile error) @@ -51,9 +40,9 @@ extern int smtliblex(void); int smtliberror(const char *s) { std::ostringstream ss; - ss << CVC4::parserTemp->fileName << ":" << CVC4::parserTemp->lineNum + ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum << ": " << s; - return CVC4::parserTemp->error(ss.str()); + return CVC3::parserTemp->error(ss.str()); } @@ -66,9 +55,9 @@ int smtliberror(const char *s) %union { std::string *str; std::vector<std::string> *strvec; - CVC4::Expr *node; - std::vector<CVC4::Expr> *vec; - std::pair<std::vector<CVC4::Expr>, std::vector<std::string> > *pat_ann; + CVC3::Expr *node; + std::vector<CVC3::Expr> *vec; + std::pair<std::vector<CVC3::Expr>, std::vector<std::string> > *pat_ann; }; @@ -1548,6 +1537,4 @@ fun_pred_symb: } ; - - %% diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp index d5bdaaf26..b78b27a0d 100644 --- a/src/parser/smtlib_scanner.lpp +++ b/src/parser/smtlib_scanner.lpp @@ -1,76 +1,31 @@ -%{ -/*****************************************************************************/ -/*! - * \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> - * - */ -/*****************************************************************************/ +/********************* -*- C++ -*- */ +/** smtlib_scanner.lpp + ** This file is part of the CVC4 prototype. + ** + ** Reference-counted encapsulation of a pointer to an expression. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ +%option interactive +%option noyywrap +%option nounput +%option noreject +%option noyymore +%option yylineno +%option prefix="smtlib" + +%{ #include <iostream> -#include "parser_temp.h" -#include "expr_manager.h" /* for the benefit of parsesmtlib_defs.h */ -#include "parsesmtlib_defs.h" +#include "smtlib.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; @@ -152,13 +107,6 @@ static std::string _string_lit; %} -%option interactive -%option noyywrap -%option nounput -%option noreject -%option noyymore -%option yylineno - %x COMMENT %x STRING_LITERAL %x USER_VALUE @@ -257,4 +205,3 @@ IDCHAR ({LETTER}|{DIGIT}|{OPCHAR}) . { smtliberror("Illegal input character."); } %% - |