From: Tim King Date: Fri, 11 Nov 2016 23:46:29 +0000 (-0800) Subject: Applying clang-format to parser.cpp. X-Git-Tag: cvc5-1.0.0~5986 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=17d74f82f0407db60d65d4bd24d35b383f1712ca;p=cvc5.git Applying clang-format to parser.cpp. --- diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index c3c533576..ac93c93d2 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -41,39 +41,39 @@ using namespace CVC4::kind; namespace CVC4 { namespace parser { -Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : - d_exprManager(exprManager), - d_resourceManager(d_exprManager->getResourceManager()), - d_input(input), - d_symtabAllocated(), - d_symtab(&d_symtabAllocated), - d_assertionLevel(0), - d_globalDeclarations(false), - d_anonymousFunctionCount(0), - d_done(false), - d_checksEnabled(true), - d_strictMode(strictMode), - d_parseOnly(parseOnly), - d_canIncludeFile(true), - d_logicIsForced(false), - d_forcedLogic() { +Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, + bool parseOnly) + : d_exprManager(exprManager), + d_resourceManager(d_exprManager->getResourceManager()), + d_input(input), + d_symtabAllocated(), + d_symtab(&d_symtabAllocated), + d_assertionLevel(0), + d_globalDeclarations(false), + d_anonymousFunctionCount(0), + d_done(false), + d_checksEnabled(true), + d_strictMode(strictMode), + d_parseOnly(parseOnly), + d_canIncludeFile(true), + d_logicIsForced(false), + d_forcedLogic() { d_input->setParser(*this); } Expr Parser::getSymbol(const std::string& name, SymbolType type) { checkDeclaration(name, CHECK_DECLARED, type); - assert( isDeclared(name, type) ); + assert(isDeclared(name, type)); - if(type == SYM_VARIABLE) { + if (type == SYM_VARIABLE) { // Functions share var namespace return d_symtab->lookup(name); } - assert(false);//Unhandled(type); + assert(false); // Unhandled(type); return Expr(); } - Expr Parser::getVariable(const std::string& name) { return getSymbol(name, SYM_VARIABLE); } @@ -82,32 +82,30 @@ Expr Parser::getFunction(const std::string& name) { return getSymbol(name, SYM_VARIABLE); } -Type Parser::getType(const std::string& var_name, - SymbolType type) { +Type Parser::getType(const std::string& var_name, SymbolType type) { checkDeclaration(var_name, CHECK_DECLARED, type); - assert( isDeclared(var_name, type) ); + assert(isDeclared(var_name, type)); Type t = getSymbol(var_name, type).getType(); return t; } Type Parser::getSort(const std::string& name) { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); - assert( isDeclared(name, SYM_SORT) ); + assert(isDeclared(name, SYM_SORT)); Type t = d_symtab->lookupType(name); return t; } -Type Parser::getSort(const std::string& name, - const std::vector& params) { +Type Parser::getSort(const std::string& name, const std::vector& params) { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); - assert( isDeclared(name, SYM_SORT) ); + assert(isDeclared(name, SYM_SORT)); Type t = d_symtab->lookupType(name, params); return t; } -size_t Parser::getArity(const std::string& sort_name){ +size_t Parser::getArity(const std::string& sort_name) { checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT); - assert( isDeclared(sort_name, SYM_SORT) ); + assert(isDeclared(sort_name, SYM_SORT)); return d_symtab->lookupArity(sort_name); } @@ -119,12 +117,12 @@ bool Parser::isBoolean(const std::string& name) { /* Returns true if name is bound to a function-like thing (function, * constructor, tester, or selector). */ bool Parser::isFunctionLike(const std::string& name) { - if(!isDeclared(name, SYM_VARIABLE)) { + if (!isDeclared(name, SYM_VARIABLE)) { return false; } Type type = getType(name); - return type.isFunction() || type.isConstructor() || - type.isTester() || type.isSelector(); + return type.isFunction() || type.isConstructor() || type.isTester() || + type.isSelector(); } /* Returns true if name is bound to a defined function. */ @@ -146,9 +144,8 @@ bool Parser::isPredicate(const std::string& name) { return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate(); } -Expr -Parser::mkVar(const std::string& name, const Type& type, uint32_t flags) { - if(d_globalDeclarations) { +Expr Parser::mkVar(const std::string& name, const Type& type, uint32_t flags) { + if (d_globalDeclarations) { flags |= ExprManager::VAR_FLAG_GLOBAL; } Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; @@ -157,17 +154,16 @@ Parser::mkVar(const std::string& name, const Type& type, uint32_t flags) { return expr; } -Expr -Parser::mkBoundVar(const std::string& name, const Type& type) { +Expr Parser::mkBoundVar(const std::string& name, const Type& type) { Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; Expr expr = d_exprManager->mkBoundVar(name, type); defineVar(name, expr, false); return expr; } -Expr -Parser::mkFunction(const std::string& name, const Type& type, uint32_t flags) { - if(d_globalDeclarations) { +Expr Parser::mkFunction(const std::string& name, const Type& type, + uint32_t flags) { + if (d_globalDeclarations) { flags |= ExprManager::VAR_FLAG_GLOBAL; } Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; @@ -176,9 +172,9 @@ Parser::mkFunction(const std::string& name, const Type& type, uint32_t flags) { return expr; } -Expr -Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, uint32_t flags) { - if(d_globalDeclarations) { +Expr Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, + uint32_t flags) { + if (d_globalDeclarations) { flags |= ExprManager::VAR_FLAG_GLOBAL; } stringstream name; @@ -186,63 +182,60 @@ Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, uint32_ return d_exprManager->mkVar(name.str(), type, flags); } -std::vector -Parser::mkVars(const std::vector names, const Type& type, uint32_t flags) { - if(d_globalDeclarations) { +std::vector Parser::mkVars(const std::vector names, + const Type& type, uint32_t flags) { + if (d_globalDeclarations) { flags |= ExprManager::VAR_FLAG_GLOBAL; } std::vector vars; - for(unsigned i = 0; i < names.size(); ++i) { + for (unsigned i = 0; i < names.size(); ++i) { vars.push_back(mkVar(names[i], type, flags)); } return vars; } -std::vector -Parser::mkBoundVars(const std::vector names, const Type& type) { +std::vector Parser::mkBoundVars(const std::vector names, + const Type& type) { std::vector vars; - for(unsigned i = 0; i < names.size(); ++i) { + for (unsigned i = 0; i < names.size(); ++i) { vars.push_back(mkBoundVar(names[i], type)); } return vars; } -void -Parser::defineVar(const std::string& name, const Expr& val, bool levelZero) { - Debug("parser") << "defineVar( " << name << " := " << val << ")" << std::endl;; +void Parser::defineVar(const std::string& name, const Expr& val, + bool levelZero) { + Debug("parser") << "defineVar( " << name << " := " << val << ")" << std::endl; d_symtab->bind(name, val, levelZero); - assert( isDeclared(name) ); + assert(isDeclared(name)); } -void -Parser::defineFunction(const std::string& name, const Expr& val, bool levelZero) { +void Parser::defineFunction(const std::string& name, const Expr& val, + bool levelZero) { d_symtab->bindDefinedFunction(name, val, levelZero); - assert( isDeclared(name) ); + assert(isDeclared(name)); } -void -Parser::defineType(const std::string& name, const Type& type) { +void Parser::defineType(const std::string& name, const Type& type) { d_symtab->bindType(name, type); - assert( isDeclared(name, SYM_SORT) ); + assert(isDeclared(name, SYM_SORT)); } -void -Parser::defineType(const std::string& name, - const std::vector& params, - const Type& type) { +void Parser::defineType(const std::string& name, + const std::vector& params, const Type& type) { d_symtab->bindType(name, params, type); - assert( isDeclared(name, SYM_SORT) ); + assert(isDeclared(name, SYM_SORT)); } -void -Parser::defineParameterizedType(const std::string& name, - const std::vector& params, - const Type& type) { - if(Debug.isOn("parser")) { - Debug("parser") << "defineParameterizedType(" << name << ", " << params.size() << ", ["; - if(params.size() > 0) { +void Parser::defineParameterizedType(const std::string& name, + const std::vector& params, + const Type& type) { + if (Debug.isOn("parser")) { + Debug("parser") << "defineParameterizedType(" << name << ", " + << params.size() << ", ["; + if (params.size() > 0) { copy(params.begin(), params.end() - 1, - ostream_iterator(Debug("parser"), ", ") ); + ostream_iterator(Debug("parser"), ", ")); Debug("parser") << params.back(); } Debug("parser") << "], " << type << ")" << std::endl; @@ -250,9 +243,8 @@ Parser::defineParameterizedType(const std::string& name, defineType(name, params, type); } -SortType -Parser::mkSort(const std::string& name, uint32_t flags) { - if(d_globalDeclarations) { +SortType Parser::mkSort(const std::string& name, uint32_t flags) { + if (d_globalDeclarations) { flags |= ExprManager::VAR_FLAG_GLOBAL; } Debug("parser") << "newSort(" << name << ")" << std::endl; @@ -261,8 +253,8 @@ Parser::mkSort(const std::string& name, uint32_t flags) { return type; } -SortConstructorType -Parser::mkSortConstructor(const std::string& name, size_t arity) { +SortConstructorType Parser::mkSortConstructor(const std::string& name, + size_t arity) { Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; SortConstructorType type = d_exprManager->mkSortConstructor(name, arity); @@ -276,84 +268,79 @@ SortType Parser::mkUnresolvedType(const std::string& name) { return unresolved; } -SortConstructorType -Parser::mkUnresolvedTypeConstructor(const std::string& name, - size_t arity) { +SortConstructorType Parser::mkUnresolvedTypeConstructor(const std::string& name, + size_t arity) { SortConstructorType unresolved = mkSortConstructor(name, arity); d_unresolved.insert(unresolved); return unresolved; } -SortConstructorType -Parser::mkUnresolvedTypeConstructor(const std::string& name, - const std::vector& params) { - Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" - << std::endl; - SortConstructorType unresolved = d_exprManager->mkSortConstructor(name, params.size()); +SortConstructorType Parser::mkUnresolvedTypeConstructor( + const std::string& name, const std::vector& params) { + Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() + << ")" << std::endl; + SortConstructorType unresolved = + d_exprManager->mkSortConstructor(name, params.size()); defineType(name, params, unresolved); - Type t = getSort( name, params ); + Type t = getSort(name, params); d_unresolved.insert(unresolved); return unresolved; } bool Parser::isUnresolvedType(const std::string& name) { - if(!isDeclared(name, SYM_SORT)) { + if (!isDeclared(name, SYM_SORT)) { return false; } return d_unresolved.find(getSort(name)) != d_unresolved.end(); } -std::vector -Parser::mkMutualDatatypeTypes(std::vector& datatypes) { - +std::vector Parser::mkMutualDatatypeTypes( + std::vector& datatypes) { try { std::vector types = - d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved); + d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved); assert(datatypes.size() == types.size()); - for(unsigned i = 0; i < datatypes.size(); ++i) { + for (unsigned i = 0; i < datatypes.size(); ++i) { DatatypeType t = types[i]; const Datatype& dt = t.getDatatype(); const std::string& name = dt.getName(); Debug("parser-idt") << "define " << name << " as " << t << std::endl; - if(isDeclared(name, SYM_SORT)) { + if (isDeclared(name, SYM_SORT)) { throw ParserException(name + " already declared"); } - if( t.isParametric() ) { - std::vector< Type > paramTypes = t.getParamTypes(); - defineType(name, paramTypes, t ); + if (t.isParametric()) { + std::vector paramTypes = t.getParamTypes(); + defineType(name, paramTypes, t); } else { defineType(name, t); } - for(Datatype::const_iterator j = dt.begin(), - j_end = dt.end(); - j != j_end; - ++j) { + for (Datatype::const_iterator j = dt.begin(), j_end = dt.end(); + j != j_end; ++j) { const DatatypeConstructor& ctor = *j; expr::ExprPrintTypes::Scope pts(Debug("parser-idt"), true); Expr constructor = ctor.getConstructor(); Debug("parser-idt") << "+ define " << constructor << std::endl; string constructorName = ctor.getName(); - if(isDeclared(constructorName, SYM_VARIABLE)) { + if (isDeclared(constructorName, SYM_VARIABLE)) { throw ParserException(constructorName + " already declared"); } defineVar(constructorName, constructor); Expr tester = ctor.getTester(); Debug("parser-idt") << "+ define " << tester << std::endl; string testerName = ctor.getTesterName(); - if(isDeclared(testerName, SYM_VARIABLE)) { + if (isDeclared(testerName, SYM_VARIABLE)) { throw ParserException(testerName + " already declared"); } defineVar(testerName, tester); - for(DatatypeConstructor::const_iterator k = ctor.begin(), - k_end = ctor.end(); - k != k_end; - ++k) { + for (DatatypeConstructor::const_iterator k = ctor.begin(), + k_end = ctor.end(); + k != k_end; ++k) { Expr selector = (*k).getSelector(); Debug("parser-idt") << "+++ define " << selector << std::endl; string selectorName = (*k).getName(); - if(isDeclared(selectorName, SYM_VARIABLE)) { + if (isDeclared(selectorName, SYM_VARIABLE)) { throw ParserException(selectorName + " already declared"); } defineVar(selectorName, selector); @@ -365,29 +352,30 @@ Parser::mkMutualDatatypeTypes(std::vector& datatypes) { // complained of a bad substitution if anything is left unresolved. // Clear out the set. d_unresolved.clear(); - - //throw exception if any datatype is not well-founded - for(unsigned i = 0; i < datatypes.size(); ++i) { + + // throw exception if any datatype is not well-founded + for (unsigned i = 0; i < datatypes.size(); ++i) { const Datatype& dt = types[i].getDatatype(); - if( !dt.isCodatatype() && !dt.isWellFounded() ){ + if (!dt.isCodatatype() && !dt.isWellFounded()) { throw ParserException(dt.getName() + " is not well-founded"); } } - + return types; - } catch(IllegalArgumentException& ie) { + } catch (IllegalArgumentException& ie) { throw ParserException(ie.getMessage()); } } bool Parser::isDeclared(const std::string& name, SymbolType type) { - switch(type) { - case SYM_VARIABLE: - return d_reservedSymbols.find(name) != d_reservedSymbols.end() || d_symtab->isBound(name); - case SYM_SORT: - return d_symtab->isBoundType(name); + switch (type) { + case SYM_VARIABLE: + return d_reservedSymbols.find(name) != d_reservedSymbols.end() || + d_symtab->isBound(name); + case SYM_SORT: + return d_symtab->isBoundType(name); } - assert(false);//Unhandled(type); + assert(false); // Unhandled(type); return false; } @@ -397,58 +385,55 @@ void Parser::reserveSymbolAtAssertionLevel(const std::string& varName) { } void Parser::checkDeclaration(const std::string& varName, - DeclarationCheck check, - SymbolType type, - std::string notes) - throw(ParserException) { - if(!d_checksEnabled) { + DeclarationCheck check, SymbolType type, + std::string notes) throw(ParserException) { + if (!d_checksEnabled) { return; } - switch(check) { - case CHECK_DECLARED: - if( !isDeclared(varName, type) ) { - parseError("Symbol '" + varName + "' not declared as a " + - (type == SYM_VARIABLE ? "variable" : "type") + - (notes.size() == 0 ? notes : "\n" + notes)); - } - break; + switch (check) { + case CHECK_DECLARED: + if (!isDeclared(varName, type)) { + parseError("Symbol '" + varName + "' not declared as a " + + (type == SYM_VARIABLE ? "variable" : "type") + + (notes.size() == 0 ? notes : "\n" + notes)); + } + break; - case CHECK_UNDECLARED: - if( isDeclared(varName, type) ) { - parseError("Symbol '" + varName + "' previously declared as a " + - (type == SYM_VARIABLE ? "variable" : "type") + - (notes.size() == 0 ? notes : "\n" + notes)); - } - break; + case CHECK_UNDECLARED: + if (isDeclared(varName, type)) { + parseError("Symbol '" + varName + "' previously declared as a " + + (type == SYM_VARIABLE ? "variable" : "type") + + (notes.size() == 0 ? notes : "\n" + notes)); + } + break; - case CHECK_NONE: - break; + case CHECK_NONE: + break; - default: - assert(false);//Unhandled(check); + default: + assert(false); // Unhandled(check); } } void Parser::checkFunctionLike(const std::string& name) throw(ParserException) { - if(d_checksEnabled && !isFunctionLike(name)) { + if (d_checksEnabled && !isFunctionLike(name)) { parseError("Expecting function-like symbol, found '" + name + "'"); } } -void Parser::checkArity(Kind kind, unsigned numArgs) - throw(ParserException) { - if(!d_checksEnabled) { +void Parser::checkArity(Kind kind, unsigned numArgs) throw(ParserException) { + if (!d_checksEnabled) { return; } unsigned min = d_exprManager->minArity(kind); unsigned max = d_exprManager->maxArity(kind); - if( numArgs < min || numArgs > max ) { + if (numArgs < min || numArgs > max) { stringstream ss; ss << "Expecting "; - if( numArgs < min ) { + if (numArgs < min) { ss << "at least " << min << " "; } else { ss << "at most " << max << " "; @@ -460,24 +445,22 @@ void Parser::checkArity(Kind kind, unsigned numArgs) } 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) ); + if (d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end()) { + parseError("Operator is not defined in the current logic: " + + kindToString(kind)); } checkArity(kind, numArgs); } -void Parser::addOperator(Kind kind) { - d_logicOperators.insert(kind); -} +void Parser::addOperator(Kind kind) { d_logicOperators.insert(kind); } -void Parser::preemptCommand(Command* cmd) { - d_commandQueue.push_back(cmd); -} +void Parser::preemptCommand(Command* cmd) { d_commandQueue.push_back(cmd); } -Command* Parser::nextCommand() throw(ParserException, UnsafeInterruptException) { +Command* Parser::nextCommand() throw(ParserException, + UnsafeInterruptException) { Debug("parser") << "nextCommand()" << std::endl; Command* cmd = NULL; - if(!d_commandQueue.empty()) { + if (!d_commandQueue.empty()) { cmd = d_commandQueue.front(); d_commandQueue.pop_front(); setDone(cmd == NULL); @@ -488,19 +471,17 @@ Command* Parser::nextCommand() throw(ParserException, UnsafeInterruptException) cmd = d_commandQueue.front(); d_commandQueue.pop_front(); setDone(cmd == NULL); - } catch(ParserException& e) { + } catch (ParserException& e) { setDone(); throw; - } catch(exception& e) { + } catch (exception& e) { setDone(); parseError(e.what()); } } Debug("parser") << "nextCommand() => " << cmd << std::endl; - if (cmd != NULL && - dynamic_cast(cmd) == NULL && - dynamic_cast(cmd) == NULL) - { + if (cmd != NULL && dynamic_cast(cmd) == NULL && + dynamic_cast(cmd) == NULL) { // don't count set-option commands as to not get stuck in an infinite // loop of resourcing out const Options& options = d_exprManager->getOptions(); @@ -514,14 +495,14 @@ Expr Parser::nextExpression() throw(ParserException, UnsafeInterruptException) { const Options& options = d_exprManager->getOptions(); d_resourceManager->spendResource(options.getParseStep()); Expr result; - if(!done()) { + if (!done()) { try { result = d_input->parseExpr(); setDone(result.isNull()); - } catch(ParserException& e) { + } catch (ParserException& e) { setDone(); throw; - } catch(exception& e) { + } catch (exception& e) { setDone(); parseError(e.what()); } @@ -531,13 +512,14 @@ Expr Parser::nextExpression() throw(ParserException, UnsafeInterruptException) { } void Parser::attributeNotSupported(const std::string& attr) { - if(d_attributesWarnedAbout.find(attr) == d_attributesWarnedAbout.end()) { + if (d_attributesWarnedAbout.find(attr) == d_attributesWarnedAbout.end()) { stringstream ss; - ss << "warning: Attribute '" << attr << "' not supported (ignoring this and all following uses)"; + ss << "warning: Attribute '" << attr + << "' not supported (ignoring this and all following uses)"; d_input->warning(ss.str()); d_attributesWarnedAbout.insert(attr); } } -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ +} /* CVC4::parser namespace */ +} /* CVC4 namespace */