diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/Makefile.am | 4 | ||||
-rw-r--r-- | src/parser/parser.h | 8 | ||||
-rw-r--r-- | src/parser/parser_exception.h | 10 | ||||
-rw-r--r-- | src/parser/parser_state.h | 17 | ||||
-rw-r--r-- | src/parser/pl.ypp | 23 | ||||
-rw-r--r-- | src/parser/pl_scanner.lpp | 28 | ||||
-rw-r--r-- | src/parser/smtlib.ypp | 6 | ||||
-rw-r--r-- | src/parser/smtlib_scanner.lpp | 4 |
8 files changed, 56 insertions, 44 deletions
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 918ab2fb2..2a1b83dba 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -1,5 +1,5 @@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall +INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@ +AM_CXXFLAGS = -Wall -fvisibility=hidden noinst_LIBRARIES = libparser.a diff --git a/src/parser/parser.h b/src/parser/parser.h index 967f20e95..36b8c34eb 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -10,13 +10,14 @@ ** Parser abstraction. **/ -#ifndef __CVC4_PARSER_H -#define __CVC4_PARSER_H +#ifndef __CVC4__PARSER__PARSER_H +#define __CVC4__PARSER__PARSER_H #include "core/exception.h" #include "core/lang.h" namespace CVC4 { +namespace parser { class ValidityChecker; class Expr; @@ -59,6 +60,7 @@ namespace CVC4 { class ParserTemp; extern ParserTemp* parserTemp; +}/* CVC4::parser namespace */ }/* CVC4 namespace */ -#endif /* __CVC4_PARSER_H */ +#endif /* __CVC4__PARSER__PARSER_H */ diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index 18f027e44..89490fad8 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -10,14 +10,15 @@ ** Exception class. **/ -#ifndef __CVC4_PARSER_EXCEPTION_H -#define __CVC4_PARSER_EXCEPTION_H +#ifndef __CVC4__PARSER__PARSER_EXCEPTION_H +#define __CVC4__PARSER__PARSER_EXCEPTION_H -#include "core/exception.h" +#include "util/exception.h" #include <string> #include <iostream> namespace CVC4 { +namespace parser { class ParserException: public Exception { public: @@ -32,6 +33,7 @@ namespace CVC4 { } }; // end of class ParserException +}/* CVC4::parser namespace */ }/* CVC4 namespace */ -#endif /* __CVC4_PARSER_EXCEPTION_H */ +#endif /* __CVC4__PARSER__PARSER_EXCEPTION_H */ diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index f82980196..c1fd0ae96 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -14,17 +14,19 @@ ** New York University **/ -#ifndef __CVC4_PARSER_STATE_H -#define __CVC4_PARSER_STATE_H +#ifndef __CVC4__PARSER__PARSER_STATE_H +#define __CVC4__PARSER__PARSER_STATE_H #include <iostream> #include <sstream> #include "cvc4_expr.h" -#include "exception.h" +#include "util/exception.h" namespace CVC4 { -class ValidityChecker; +class SmtEngine; + +namespace parser { class ParserState { private: @@ -37,7 +39,7 @@ private: // The currently used prompt std::string prompt; public: - ValidityChecker* vc; + SmtEngine* vc; std::istream* is; // The current input line int lineNum; @@ -89,6 +91,7 @@ public: void setPrompt2() { prompt = prompt2; } }; -} /* CVC4 namespace */ +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_PARSER_STATE_H */ +#endif /* __CVC4__PARSER__PARSER_STATE_H */ diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp index d8fd57c8c..012f468eb 100644 --- a/src/parser/pl.ypp +++ b/src/parser/pl.ypp @@ -13,19 +13,22 @@ %{ -#include "vc.h" -#include "parser_exception.h" -#include "parser_state.h" +#include "cvc4.h" +#include "parser/parser_exception.h" +#include "parser/parser_state.h" //#include "rational.h" // Exported shared data namespace CVC4 { - extern ParserState* parserState; -} + namespace parser { + extern ParserState* parserState; + }/* CVC4::parser namespace */ +}/* CVC4 hnamespace */ + // Define shortcuts for various things -#define TMP CVC4::parserState -#define EXPR CVC4::parserState->expr -#define VC (CVC4::parserState->vc) +#define TMP CVC4::parser::parserState +#define EXPR CVC4::parser::parserState->expr +#define VC (CVC4::parser::parserState->vc) #define RAT(args) CVC4::newRational args // Suppress the bogus warning suppression in bison (it generates @@ -38,9 +41,9 @@ extern int PLlex(void); int PLerror(const char *s) { std::ostringstream ss; - ss << CVC4::parserState->fileName << ":" << CVC4::parserState->lineNum + ss << CVC4::parser::parserState->fileName << ":" << CVC4::parser::parserState->lineNum << ": " << s; - return CVC4::parserState->error(ss.str()); + return CVC4::parser::parserState->error(ss.str()); } diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp index ba8a8e85d..262eb5c88 100644 --- a/src/parser/pl_scanner.lpp +++ b/src/parser/pl_scanner.lpp @@ -21,30 +21,32 @@ %{ #include <iostream> -#include "expr_manager.h" /* for the benefit of parsePL_defs.h */ -#include "parser_state.h" -#include "pl.hpp" -#include "debug.h" +#include "expr/expr_manager.h" /* for the benefit of parsePL_defs.h */ +#include "parser/parser_state.h" +#include "parser/pl.hpp" +#include "util/debug.h" namespace CVC4 { - extern ParserState* parserState; -} + namespace parser { + extern ParserState* parserState; + }/* CVC4::parser namespace */ +}/* CVC4 namespace */ extern int PL_inputLine; extern char *PLtext; -extern int PLerror (const char *msg); +extern int PLerror(const char *msg); static int PLinput(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::parserState->interactive) { + if(CVC4::parser::parserState->interactive) { // Print the current prompt - std::cout << CVC4::parserState->getPrompt() << std::flush; + std::cout << CVC4::parser::parserState->getPrompt() << std::flush; // Set the prompt to "middle of the command" one - CVC4::parserState->setPrompt2(); + CVC4::parser::parserState->setPrompt2(); // Read the line is.getline(buf, size-1); } else // Set the terminator char to 0 @@ -69,7 +71,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::parserState->is, buf, max_size); + result = PLinput(*CVC4::parser::parserState->is, buf, max_size); int PL_bufSize() { return YY_BUF_SIZE; } YY_BUFFER_STATE PL_buf_state() { return YY_CURRENT_BUFFER; } @@ -123,7 +125,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) %% -[\n] { CVC4::parserState->lineNum++; } +[\n] { CVC4::parser::parserState->lineNum++; } [ \t\r\f] { /* skip whitespace */ } @@ -136,7 +138,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) "%" { BEGIN COMMENT; } <COMMENT>"\n" { BEGIN INITIAL; /* return to normal mode */ - CVC4::parserState->lineNum++; } + CVC4::parser::parserState->lineNum++; } <COMMENT>. { /* stay in comment mode */ } <INITIAL>"\"" { BEGIN STRING_LITERAL; diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp index 0f3aa8cf4..692a9cda5 100644 --- a/src/parser/smtlib.ypp +++ b/src/parser/smtlib.ypp @@ -11,9 +11,9 @@ ** commands in SMT-LIB language. **/ -#include "vc.h" -#include "parser_exception.h" -#include "parser_state.h" +#include "cvc4.h" +#include "parser/parser_exception.h" +#include "parser/parser_state.h" // Exported shared data namespace CVC4 { diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp index bb5802aed..b367b0d93 100644 --- a/src/parser/smtlib_scanner.lpp +++ b/src/parser/smtlib_scanner.lpp @@ -20,8 +20,8 @@ %{ #include <iostream> -#include "smtlib.hpp" -#include "debug.h" +#include "parser/smtlib.hpp" +#include "util/debug.h" namespace CVC4 { extern ParserTemp* parserTemp; |