diff options
| -rw-r--r-- | src/parser/antlr_input.cpp | 11 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 17 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 60 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.h | 2 |
4 files changed, 86 insertions, 4 deletions
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index cd622b8a6..d498d3c54 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -46,9 +46,10 @@ namespace parser { AntlrInputStream::AntlrInputStream(std::string name, pANTLR3_INPUT_STREAM input, bool fileIsTemporary) : - InputStream(name,fileIsTemporary), + InputStream(name, fileIsTemporary), d_input(input) { assert( input != NULL ); + input->fileName = input->strFactory->newStr8(input->strFactory, (pANTLR3_UINT8)name.c_str()); } AntlrInputStream::~AntlrInputStream() { @@ -286,16 +287,18 @@ void AntlrInput::warning(const std::string& message) { void AntlrInput::parseError(const std::string& message, bool eofException) throw (ParserException) { Debug("parser") << "Throwing exception: " - << getInputStream()->getName() << ":" + << (const char*)d_lexer->rec->state->tokSource->fileName->chars << ":" << d_lexer->getLine(d_lexer) << "." << d_lexer->getCharPositionInLine(d_lexer) << ": " << message << endl; if(eofException) { - throw ParserEndOfFileException(message, getInputStream()->getName(), + throw ParserEndOfFileException(message, + (const char*)d_lexer->rec->state->tokSource->fileName->chars, d_lexer->getLine(d_lexer), d_lexer->getCharPositionInLine(d_lexer)); } else { - throw ParserException(message, getInputStream()->getName(), + throw ParserException(message, + (const char*)d_lexer->rec->state->tokSource->fileName->chars, d_lexer->getLine(d_lexer), d_lexer->getCharPositionInLine(d_lexer)); } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 133cedfbd..29bc8d40f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -188,7 +188,23 @@ parseExpr returns [CVC4::parser::smt2::myExpr expr] * @return the parsed command, or NULL if we've reached the end of the input */ parseCommand returns [CVC4::Command* cmd = NULL] +@declarations { + std::string name; +} : LPAREN_TOK c = command RPAREN_TOK { $cmd = c; } + + /* This extended command has to be in the outermost production so that + * the RPAREN_TOK is properly eaten and we are in a good state to read + * the included file's tokens. */ + | LPAREN_TOK INCLUDE_TOK str[name] RPAREN_TOK + { if(PARSER_STATE->strictModeEnabled()) { + PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode."); + } + PARSER_STATE->includeFile(name); + // The command of the included file will be produced at the next parseCommand() call + cmd = new EmptyCommand("include::" + name); + } + | EOF { $cmd = 0; } ; @@ -1464,6 +1480,7 @@ DECLARE_PREDS_TOK : 'declare-preds'; DEFINE_TOK : 'define'; DECLARE_CONST_TOK : 'declare-const'; SIMPLIFY_TOK : 'simplify'; +INCLUDE_TOK : 'include-file'; // attributes ATTRIBUTE_PATTERN_TOK : ':pattern'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index c042c3992..be4907e8e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -19,6 +19,11 @@ #include "parser/parser.h" #include "parser/smt1/smt1.h" #include "parser/smt2/smt2.h" +#include "parser/antlr_input.h" + +// ANTLR defines these, which is really bad! +#undef true +#undef false namespace CVC4 { namespace parser { @@ -200,5 +205,60 @@ void Smt2::checkThatLogicIsSet() { } } +/* The include are managed in the lexer but called in the parser */ +// Inspired by http://www.antlr3.org/api/C/interop.html + +static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) { + Debug("parser") << "Including " << filename << std::endl; + // Create a new input stream and take advantage of built in stream stacking + // in C target runtime. + // + pANTLR3_INPUT_STREAM in; +#ifdef CVC4_ANTLR3_OLD_INPUT_STREAM + in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str()); +#else /* CVC4_ANTLR3_OLD_INPUT_STREAM */ + in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT); +#endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */ + if( in == NULL ) { + Debug("parser") << "Can't open " << filename << std::endl; + return false; + } + // Same thing as the predefined PUSHSTREAM(in); + lexer->pushCharStream(lexer, in); + // restart it + //lexer->rec->state->tokenStartCharIndex = -10; + //lexer->emit(lexer); + + // Note that the input stream is not closed when it EOFs, I don't bother + // to do it here, but it is up to you to track streams created like this + // and destroy them when the whole parse session is complete. Remember that you + // don't want to do this until all tokens have been manipulated all the way through + // your tree parsers etc as the token does not store the text it just refers + // back to the input stream and trying to get the text for it will abort if you + // close the input stream too early. + + //TODO what said before + return true; +} + +void Smt2::includeFile(const std::string& filename) { + // Get the lexer + AntlrInput* ai = static_cast<AntlrInput*>(getInput()); + pANTLR3_LEXER lexer = ai->getAntlr3Lexer(); + // get the name of the current stream "Does it work inside an include?" + const std::string inputName = ai->getInputStreamName(); + + // Find the directory of the current input file + std::string path; + size_t pos = inputName.rfind('/'); + if(pos != std::string::npos) { + path = std::string(inputName, 0, pos + 1); + } + path.append(filename); + if(!newInputStream(path, lexer)) { + parseError("Couldn't open include file `" + path + "'"); + } +} + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 7a464c773..c50a0972b 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -85,6 +85,8 @@ public: } } + void includeFile(const std::string& filename); + bool isAbstractValue(const std::string& name) { return name.length() >= 2 && name[0] == '@' && name[1] != '0' && name.find_first_not_of("0123456789", 1) == std::string::npos; |