diff options
Diffstat (limited to 'src/parser/antlr_parser.cpp')
-rw-r--r-- | src/parser/antlr_parser.cpp | 93 |
1 files changed, 42 insertions, 51 deletions
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 593a89873..d20e59db3 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -60,7 +60,7 @@ Expr AntlrParser::getSymbol(const std::string& name, SymbolType type) { return d_varSymbolTable.getObject(name); default: - Unhandled("Unhandled symbol type!"); + Unhandled(type); } } @@ -72,17 +72,16 @@ Expr AntlrParser::getFunction(const std::string& name) { return getSymbol(name, SYM_FUNCTION); } -const Type* -AntlrParser::getType(const std::string& var_name, - SymbolType type) { +Type* AntlrParser::getType(const std::string& var_name, + SymbolType type) { Assert( isDeclared(var_name, type) ); - const Type* t = getSymbol(var_name,type).getType(); + Type* t = getSymbol(var_name, type).getType(); return t; } -const Type* AntlrParser::getSort(const std::string& name) { +Type* AntlrParser::getSort(const std::string& name) { Assert( isDeclared(name, SYM_SORT) ); - const Type* t = d_sortTable.getObject(name); + Type* t = d_sortTable.getObject(name); return t; } @@ -134,33 +133,30 @@ Expr AntlrParser::mkExpr(Kind kind, const std::vector<Expr>& children) { return result; } -const Type* -AntlrParser::functionType(const Type* domainType, - const Type* rangeType) { - return d_exprManager->mkFunctionType(domainType,rangeType); +Type* AntlrParser::functionType(Type* domainType, + Type* rangeType) { + return d_exprManager->mkFunctionType(domainType, rangeType); } -const Type* -AntlrParser::functionType(const std::vector<const Type*>& argTypes, - const Type* rangeType) { +Type* AntlrParser::functionType(const std::vector<Type*>& argTypes, + Type* rangeType) { Assert( argTypes.size() > 0 ); - return d_exprManager->mkFunctionType(argTypes,rangeType); + return d_exprManager->mkFunctionType(argTypes, rangeType); } -const Type* -AntlrParser::functionType(const std::vector<const Type*>& sorts) { +Type* AntlrParser::functionType(const std::vector<Type*>& sorts) { Assert( sorts.size() > 0 ); if( sorts.size() == 1 ) { return sorts[0]; } else { - std::vector<const Type*> argTypes(sorts); - const Type* rangeType = argTypes.back(); + std::vector<Type*> argTypes(sorts); + Type* rangeType = argTypes.back(); argTypes.pop_back(); - return functionType(argTypes,rangeType); + return functionType(argTypes, rangeType); } } -const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) { +Type* AntlrParser::predicateType(const std::vector<Type*>& sorts) { if(sorts.size() == 0) { return d_exprManager->booleanType(); } else { @@ -168,17 +164,16 @@ const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) { } } -Expr -AntlrParser::mkVar(const std::string& name, const Type* type) { +Expr AntlrParser::mkVar(const std::string& name, Type* type) { Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl; Expr expr = d_exprManager->mkVar(type, name); - defineVar(name,expr); + defineVar(name, expr); return expr; } -const std::vector<Expr> -AntlrParser::mkVars(const std::vector<std::string> names, - const Type* type) { +const std::vector<Expr> +AntlrParser::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)); @@ -186,55 +181,51 @@ AntlrParser::mkVars(const std::vector<std::string> names, return vars; } -void -AntlrParser::defineVar(const std::string& name, const Expr& val) { +void AntlrParser::defineVar(const std::string& name, const Expr& val) { Assert(!isDeclared(name)); - d_varSymbolTable.bindName(name,val); + d_varSymbolTable.bindName(name, val); Assert(isDeclared(name)); } -void -AntlrParser::undefineVar(const std::string& name) { +void AntlrParser::undefineVar(const std::string& name) { Assert(isDeclared(name)); d_varSymbolTable.unbindName(name); Assert(!isDeclared(name)); } -const Type* -AntlrParser::newSort(const std::string& name) { +Type* AntlrParser::newSort(const std::string& name) { Debug("parser") << "newSort(" << name << ")" << std::endl; Assert( !isDeclared(name, SYM_SORT) ); - const Type* type = d_exprManager->mkSort(name); + Type* type = d_exprManager->mkSort(name); d_sortTable.bindName(name, type); Assert( isDeclared(name, SYM_SORT) ); return type; } -const std::vector<const Type*> +const std::vector<Type*> AntlrParser::newSorts(const std::vector<std::string>& names) { - std::vector<const Type*> types; + std::vector<Type*> types; for(unsigned i = 0; i < names.size(); ++i) { types.push_back(newSort(names[i])); } return types; } -void -AntlrParser::setLogic(const std::string& name) { +void AntlrParser::setLogic(const std::string& name) { if( name == "QF_UF" ) { newSort("U"); } else { - Unhandled("setLogic: " + name); + Unhandled(name); } } -const BooleanType* AntlrParser::booleanType() { - return d_exprManager->booleanType(); +BooleanType* AntlrParser::booleanType() { + return d_exprManager->booleanType(); } -const KindType* AntlrParser::kindType() { - return d_exprManager->kindType(); +KindType* AntlrParser::kindType() { + return d_exprManager->kindType(); } unsigned int AntlrParser::minArity(Kind kind) { @@ -251,7 +242,7 @@ unsigned int AntlrParser::minArity(Kind kind) { return 1; case APPLY: - case EQUAL: + case EQUAL: case IFF: case IMPLIES: case PLUS: @@ -262,7 +253,7 @@ unsigned int AntlrParser::minArity(Kind kind) { return 3; default: - Unhandled("kind in minArity"); + Unhandled(kind); } } @@ -277,7 +268,7 @@ unsigned int AntlrParser::maxArity(Kind kind) { case NOT: return 1; - case EQUAL: + case EQUAL: case IFF: case IMPLIES: case XOR: @@ -293,7 +284,7 @@ unsigned int AntlrParser::maxArity(Kind kind) { return UINT_MAX; default: - Unhandled("kind in maxArity"); + Unhandled(kind); } } @@ -309,7 +300,7 @@ bool AntlrParser::isDeclared(const std::string& name, SymbolType type) { case SYM_SORT: return d_sortTable.isBound(name); default: - Unhandled("Unhandled symbol type!"); + Unhandled(type); } } @@ -345,7 +336,7 @@ void AntlrParser::checkDeclaration(const std::string& varName, break; default: - Unhandled("Unknown check type!"); + Unhandled(check); } } @@ -353,7 +344,7 @@ void AntlrParser::checkFunction(const std::string& name) throw (antlr::SemanticException) { if( d_checksEnabled && !isFunction(name) ) { parseError("Expecting function symbol, found '" + name + "'"); - } + } } void AntlrParser::checkArity(Kind kind, unsigned int numArgs) |