diff options
Diffstat (limited to 'src/parser/input.cpp')
-rw-r--r-- | src/parser/input.cpp | 284 |
1 files changed, 33 insertions, 251 deletions
diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 3b7b322ca..4d5f348d8 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -13,33 +13,34 @@ ** Parser implementation. **/ -#include <iostream> -#include <fstream> #include <stdint.h> #include "input.h" +#include "parser_exception.h" +#include "parser_options.h" +#include "parser_state.h" #include "expr/command.h" #include "expr/expr.h" -#include "expr/kind.h" -#include "expr/type.h" -#include "util/output.h" -#include "util/Assert.h" -#include "parser/parser_exception.h" #include "parser/cvc/cvc_input.h" #include "parser/smt/smt_input.h" +#include "util/output.h" +#include "util/Assert.h" using namespace std; -using namespace CVC4::kind; namespace CVC4 { namespace parser { -void Input::setDone(bool done) { - d_done = done; +bool Input::done() const { + return d_parserState->done(); } -bool Input::done() const { - return d_done; +void Input::disableChecks() { + d_parserState->disableChecks(); +} + +void Input::enableChecks() { + d_parserState->enableChecks(); } Command* Input::parseNextCommand() throw (ParserException) { @@ -49,10 +50,10 @@ Command* Input::parseNextCommand() throw (ParserException) { try { cmd = doParseCommand(); if(cmd == NULL) { - setDone(); + d_parserState->setDone(); } } catch(ParserException& e) { - setDone(); + d_parserState->setDone(); throw ParserException(e.toString()); } } @@ -67,9 +68,9 @@ Expr Input::parseNextExpression() throw (ParserException) { try { result = doParseExpr(); if(result.isNull()) - setDone(); + d_parserState->setDone(); } catch(ParserException& e) { - setDone(); + d_parserState->setDone(); throw ParserException(e.toString()); } } @@ -77,271 +78,52 @@ Expr Input::parseNextExpression() throw (ParserException) { return result; } -Input::~Input() { +Input::Input(ExprManager* exprManager, const std::string& filename) { + d_parserState = new ParserState(exprManager,filename,this); } -Input::Input(ExprManager* exprManager, const std::string& filename) : - d_exprManager(exprManager), - d_filename(filename), - d_done(false), - d_checksEnabled(true) { +Input::~Input() { + delete d_parserState; } -Input* Input::newFileParser(ExprManager* em, InputLanguage lang, - const std::string& filename, bool useMmap) { +Input* Input::newFileInput(ExprManager* em, InputLanguage lang, + const std::string& filename, bool useMmap) { - Input* parser = 0; + Input* input = 0; switch(lang) { case LANG_CVC4: - parser = new CvcInput(em,filename,useMmap); + input = new CvcInput(em,filename,useMmap); break; case LANG_SMTLIB: - parser = new SmtInput(em,filename,useMmap); + input = new SmtInput(em,filename,useMmap); break; default: Unhandled(lang); } - return parser; -} - -/* -Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang, - istream& input, string filename) { - antlr::CharBuffer* inputBuffer = new CharBuffer(input); - return getNewParser(em, lang, inputBuffer, filename); -} -*/ - -/* -Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang, - std::istream& input, const std::string& name) { - Parser* parser = 0; - - switch(lang) { - case LANG_CVC4: { - antlrLexer = new AntlrCvcLexer(*inputBuffer); - antlrParser = new AntlrCvcParser(*antlrLexer); - break; - } - case LANG_SMTLIB: - parser = new Smt(em,input,name); - break; - - default: - Unhandled("Unknown Input language!"); - } - return parser; + return input; } -*/ -Input* Input::newStringParser(ExprManager* em, InputLanguage lang, - const std::string& input, const std::string& name) { - Input* parser = 0; +Input* Input::newStringInput(ExprManager* em, InputLanguage lang, + const std::string& str, const std::string& name) { + Input* input = 0; switch(lang) { case LANG_CVC4: { - parser = new CvcInput(em,input,name); + input = new CvcInput(em,str,name); break; } case LANG_SMTLIB: - parser = new SmtInput(em,input,name); + input = new SmtInput(em,str,name); break; default: Unhandled(lang); } - return parser; + return input; } -Expr Input::getSymbol(const std::string& name, SymbolType type) { - Assert( isDeclared(name, type) ); - - - switch( type ) { - - case SYM_VARIABLE: // Functions share var namespace - return d_varSymbolTable.getObject(name); - - default: - Unhandled(type); - } -} - - -Expr Input::getVariable(const std::string& name) { - return getSymbol(name, SYM_VARIABLE); -} - -Type* -Input::getType(const std::string& var_name, - SymbolType type) { - Assert( isDeclared(var_name, type) ); - Type* t = getSymbol(var_name,type).getType(); - return t; -} - -Type* Input::getSort(const std::string& name) { - Assert( isDeclared(name, SYM_SORT) ); - Type* t = d_sortTable.getObject(name); - return t; -} - -/* Returns true if name is bound to a boolean variable. */ -bool Input::isBoolean(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name)->isBoolean(); -} - -/* Returns true if name is bound to a function. */ -bool Input::isFunction(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name)->isFunction(); -} - -/* Returns true if name is bound to a function returning boolean. */ -bool Input::isPredicate(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name)->isPredicate(); -} - -Expr -Input::mkVar(const std::string& name, Type* type) { - Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl; - Expr expr = d_exprManager->mkVar(type, name); - defineVar(name,expr); - return expr; -} - -const std::vector<Expr> -Input::mkVars(const std::vector<std::string> names, - Type* type) { - std::vector<Expr> vars; - for(unsigned i = 0; i < names.size(); ++i) { - vars.push_back(mkVar(names[i], type)); - } - return vars; -} - -void -Input::defineVar(const std::string& name, const Expr& val) { - Assert(!isDeclared(name)); - d_varSymbolTable.bindName(name,val); - Assert(isDeclared(name)); -} - -void -Input::undefineVar(const std::string& name) { - Assert(isDeclared(name)); - d_varSymbolTable.unbindName(name); - Assert(!isDeclared(name)); -} - -void -Input::setLogic(const std::string& name) { - if( name == "QF_UF" ) { - newSort("U"); - } else { - Unhandled(name); - } -} - -Type* -Input::newSort(const std::string& name) { - Debug("parser") << "newSort(" << name << ")" << std::endl; - Assert( !isDeclared(name, SYM_SORT) ) ; - Type* type = d_exprManager->mkSort(name); - d_sortTable.bindName(name, type); - Assert( isDeclared(name, SYM_SORT) ) ; - return type; -} - -const std::vector<Type*> -Input::newSorts(const std::vector<std::string>& names) { - std::vector<Type*> types; - for(unsigned i = 0; i < names.size(); ++i) { - types.push_back(newSort(names[i])); - } - return types; -} - -bool Input::isDeclared(const std::string& name, SymbolType type) { - switch(type) { - case SYM_VARIABLE: - return d_varSymbolTable.isBound(name); - case SYM_SORT: - return d_sortTable.isBound(name); - default: - Unhandled(type); - } -} - -void Input::checkDeclaration(const std::string& varName, - DeclarationCheck check, - SymbolType type) - throw (ParserException) { - if(!d_checksEnabled) { - return; - } - - switch(check) { - case CHECK_DECLARED: - if( !isDeclared(varName, type) ) { - parseError("Symbol " + varName + " not declared"); - } - break; - - case CHECK_UNDECLARED: - if( isDeclared(varName, type) ) { - parseError("Symbol " + varName + " previously declared"); - } - break; - - case CHECK_NONE: - break; - - default: - Unhandled(check); - } -} - -void Input::checkFunction(const std::string& name) - throw (ParserException) { - if( d_checksEnabled && !isFunction(name) ) { - parseError("Expecting function symbol, found '" + name + "'"); - } -} - -void Input::checkArity(Kind kind, unsigned int numArgs) - throw (ParserException) { - if(!d_checksEnabled) { - return; - } - - unsigned int min = d_exprManager->minArity(kind); - unsigned int max = d_exprManager->maxArity(kind); - - if( numArgs < min || numArgs > max ) { - stringstream ss; - ss << "Expecting "; - if( numArgs < min ) { - ss << "at least " << min << " "; - } else { - ss << "at most " << max << " "; - } - ss << "arguments for operator '" << kind << "', "; - ss << "found " << numArgs; - parseError(ss.str()); - } -} - -void Input::enableChecks() { - d_checksEnabled = true; -} - -void Input::disableChecks() { - d_checksEnabled = false; -} - - }/* CVC4::parser namespace */ }/* CVC4 namespace */ |