diff options
Diffstat (limited to 'src/parser/antlr_parser.cpp')
-rw-r--r-- | src/parser/antlr_parser.cpp | 58 |
1 files changed, 12 insertions, 46 deletions
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 5a9af8d4a..bd263f72d 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -51,8 +51,7 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) : Expr AntlrParser::getSymbol(std::string name, SymbolType type) { Assert( isDeclared(name,type) ); switch( type ) { - case SYM_VARIABLE: // Predicates and functions share var namespace - // case SYM_PREDICATE: + case SYM_VARIABLE: // Functions share var namespace case SYM_FUNCTION: return d_varSymbolTable.getObject(name); default: @@ -68,10 +67,6 @@ Expr AntlrParser::getFunction(std::string name) { return getSymbol(name,SYM_FUNCTION); } -// Expr AntlrParser::getPredicate(std::string name) { -// return getSymbol(name,SYM_PREDICATE); -// } - const Type* AntlrParser::getType(std::string var_name, SymbolType type) { @@ -96,8 +91,7 @@ bool AntlrParser::isFunction(std::string name) { return isDeclared(name,SYM_FUNCTION) && getType(name)->isFunction(); } -/* Returns true if name is either a boolean variable OR a function - returning boolean. */ +/* Returns true if name is bound to a function returning boolean. */ bool AntlrParser::isPredicate(std::string name) { return isDeclared(name,SYM_FUNCTION) && getType(name)->isPredicate(); } @@ -135,45 +129,32 @@ Expr AntlrParser::mkExpr(Kind kind, const std::vector<Expr>& children) { return result; } -const FunctionType* +const Type* AntlrParser::functionType(const Type* domainType, const Type* rangeType) { return d_exprManager->mkFunctionType(domainType,rangeType); } -const FunctionType* +const Type* AntlrParser::functionType(const std::vector<const Type*>& argTypes, const Type* rangeType) { Assert( argTypes.size() > 0 ); return d_exprManager->mkFunctionType(argTypes,rangeType); } -const FunctionType* +const Type* AntlrParser::functionType(const std::vector<const Type*>& sorts) { - Assert( sorts.size() > 1 ); - std::vector<const Type*> argTypes(sorts); - const Type* rangeType = argTypes.back(); - argTypes.pop_back(); - return functionType(argTypes,rangeType); -} - -Expr AntlrParser::newFunction(std::string name, - const std::vector<const Type*>& sorts) { Assert( sorts.size() > 0 ); if( sorts.size() == 1 ) { - return mkVar(name, sorts[0]); + return sorts[0]; } else { - return mkVar(name, functionType(sorts)); + std::vector<const Type*> argTypes(sorts); + const Type* rangeType = argTypes.back(); + argTypes.pop_back(); + return functionType(argTypes,rangeType); } } -const std::vector<Expr> -AntlrParser::newFunctions(const std::vector<std::string>& names, - const std::vector<const Type*>& sorts) { - const FunctionType* t = functionType(sorts); - return mkVars(names, t); -} - const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) { if(sorts.size() == 0) { return d_exprManager->booleanType(); @@ -182,20 +163,6 @@ const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) { } } -Expr -AntlrParser::newPredicate(std::string name, - const std::vector<const Type*>& sorts) { - const Type* t = predicateType(sorts); - return mkVar(name, t); -} - -const std::vector<Expr> -AntlrParser::newPredicates(const std::vector<std::string>& names, - const std::vector<const Type*>& sorts) { - const Type* t = predicateType(sorts); - return mkVars(names, t); -} - Expr AntlrParser::mkVar(const std::string name, const Type* type) { Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl; @@ -301,7 +268,7 @@ unsigned int AntlrParser::maxArity(Kind kind) { return UINT_MAX; default: - Unhandled("kind in minArity"); + Unhandled("kind in maxArity"); } } @@ -311,8 +278,7 @@ void AntlrParser::setExpressionManager(ExprManager* em) { bool AntlrParser::isDeclared(string name, SymbolType type) { switch(type) { - case SYM_VARIABLE: // Predicates and functions share var namespace - // case SYM_PREDICATE: + case SYM_VARIABLE: // Functions share var namespace case SYM_FUNCTION: return d_varSymbolTable.isBound(name); case SYM_SORT: |