diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-20 05:37:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-20 05:37:38 +0000 |
commit | 12c1e41862e4b12c3953272416a1edc103d299ee (patch) | |
tree | 9c7d3a044c33ffc3be177e6ca692eb4149add27c /src/parser/parser.cpp | |
parent | 08df44e6b61999a14dd24a7a134146694dcb3596 (diff) |
Tuesday end-of-day commit.
Expected performance impact outside of datatypes/CVC parser is
negligible.
* CVC language LAMBDA, functional LET, type LET, precedence fixes,
bitvectors, and arrays, with partial parsing support also for
quantifiers, tuples, subranges, subtypes, and records
* support for complex recursive DATATYPE selectors, e.g.
tree = node(children:ARRAY INT OF tree) | leaf(data:INT)
these are complicated because they have to be left unresolved
at parse time and dealt with in a second pass.
* bugfix for Exprs/Types that occurred when setting them to null
(not Nodes/TypeNodes, just Exprs/Types).
* Cleanup/code review items
Diffstat (limited to 'src/parser/parser.cpp')
-rw-r--r-- | src/parser/parser.cpp | 81 |
1 files changed, 56 insertions, 25 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index c8a9876d5..19d1bbcb8 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -29,6 +29,7 @@ #include "expr/kind.h" #include "expr/type.h" #include "util/output.h" +#include "util/options.h" #include "util/Assert.h" #include "parser/cvc/cvc_input.h" #include "parser/smt/smt_input.h" @@ -39,14 +40,15 @@ using namespace CVC4::kind; namespace CVC4 { namespace parser { -Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode) : +Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : d_exprManager(exprManager), d_input(input), d_declScopeAllocated(), d_declScope(&d_declScopeAllocated), d_done(false), d_checksEnabled(true), - d_strictMode(strictMode) { + d_strictMode(strictMode), + d_parseOnly(parseOnly) { d_input->setParser(*this); } @@ -136,7 +138,7 @@ Parser::mkFunction(const std::string& name, const Type& type) { return expr; } -const std::vector<Expr> +std::vector<Expr> Parser::mkVars(const std::vector<std::string> names, const Type& type) { std::vector<Expr> vars; @@ -188,7 +190,7 @@ Parser::defineParameterizedType(const std::string& name, defineType(name, params, type); } -Type +SortType Parser::mkSort(const std::string& name) { Debug("parser") << "newSort(" << name << ")" << std::endl; Type type = d_exprManager->mkSort(name); @@ -196,34 +198,54 @@ Parser::mkSort(const std::string& name) { return type; } -Type +SortConstructorType Parser::mkSortConstructor(const std::string& name, size_t arity) { Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; - Type type = d_exprManager->mkSortConstructor(name, arity); + SortConstructorType type = d_exprManager->mkSortConstructor(name, arity); defineType(name, vector<Type>(arity), type); return type; } -std::vector<Type> +std::vector<SortType> Parser::mkSorts(const std::vector<std::string>& names) { - std::vector<Type> types; + std::vector<SortType> types; for(unsigned i = 0; i < names.size(); ++i) { types.push_back(mkSort(names[i])); } return types; } +SortType Parser::mkUnresolvedType(const std::string& name) { + SortType unresolved = mkSort(name); + d_unresolved.insert(unresolved); + return unresolved; +} + +bool Parser::isUnresolvedType(const std::string& name) { + if(!isDeclared(name, SYM_SORT)) { + return false; + } + return d_unresolved.find(getSort(name)) != d_unresolved.end(); +} + std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { + std::vector<DatatypeType> types = - d_exprManager->mkMutualDatatypeTypes(datatypes); + d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved); + Assert(datatypes.size() == types.size()); + for(unsigned i = 0; i < datatypes.size(); ++i) { DatatypeType t = types[i]; const Datatype& dt = t.getDatatype(); - Debug("parser-idt") << "define " << dt.getName() << " as " << t << std::endl; - defineType(dt.getName(), t); + const std::string& name = dt.getName(); + Debug("parser-idt") << "define " << name << " as " << t << std::endl; + if(isDeclared(name, SYM_SORT)) { + throw ParserException(name + " already declared"); + } + defineType(name, t); for(Datatype::const_iterator j = dt.begin(), j_end = dt.end(); j != j_end; @@ -258,6 +280,12 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { } } } + + // These are no longer used, and the ExprManager would have + // complained of a bad substitution if anything is left unresolved. + // Clear out the set. + d_unresolved.clear(); + return types; } @@ -273,9 +301,9 @@ bool Parser::isDeclared(const std::string& name, SymbolType type) { } void Parser::checkDeclaration(const std::string& varName, - DeclarationCheck check, - SymbolType type) - throw (ParserException) { + DeclarationCheck check, + SymbolType type) + throw(ParserException) { if(!d_checksEnabled) { return; } @@ -283,13 +311,13 @@ void Parser::checkDeclaration(const std::string& varName, switch(check) { case CHECK_DECLARED: if( !isDeclared(varName, type) ) { - parseError("Symbol " + varName + " not declared"); + parseError("Symbol " + varName + " not declared as a " + (type == SYM_VARIABLE ? "variable" : "type")); } break; case CHECK_UNDECLARED: if( isDeclared(varName, type) ) { - parseError("Symbol " + varName + " previously declared"); + parseError("Symbol " + varName + " previously declared as a " + (type == SYM_VARIABLE ? "variable" : "type")); } break; @@ -301,21 +329,20 @@ void Parser::checkDeclaration(const std::string& varName, } } -void Parser::checkFunctionLike(const std::string& name) - throw (ParserException) { - if( d_checksEnabled && !isFunctionLike(name) ) { +void Parser::checkFunctionLike(const std::string& name) throw(ParserException) { + if(d_checksEnabled && !isFunctionLike(name)) { parseError("Expecting function-like symbol, found '" + name + "'"); } } -void Parser::checkArity(Kind kind, unsigned int numArgs) - throw (ParserException) { +void Parser::checkArity(Kind kind, unsigned numArgs) + throw(ParserException) { if(!d_checksEnabled) { return; } - unsigned int min = d_exprManager->minArity(kind); - unsigned int max = d_exprManager->maxArity(kind); + unsigned min = d_exprManager->minArity(kind); + unsigned max = d_exprManager->maxArity(kind); if( numArgs < min || numArgs > max ) { stringstream ss; @@ -331,7 +358,7 @@ void Parser::checkArity(Kind kind, unsigned int numArgs) } } -void Parser::checkOperator(Kind kind, unsigned int numArgs) throw (ParserException) { +void Parser::checkOperator(Kind kind, unsigned numArgs) throw(ParserException) { if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) { parseError( "Operator is not defined in the current logic: " + kindToString(kind) ); } @@ -371,7 +398,11 @@ Command* Parser::nextCommand() throw(ParserException) { } catch(Exception& e) { setDone(); stringstream ss; - ss << e; + // set the language of the stream, otherwise if it contains + // Exprs or Types it prints in the AST language + OutputLanguage outlang = + language::toOutputLanguage(d_input->getLanguage()); + ss << Expr::setlanguage(outlang) << e; parseError( ss.str() ); } } |