diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-31 23:07:12 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-31 23:07:12 +0000 |
commit | 1b054a43b2f5d6725eae8ef8677ae34cbe749e57 (patch) | |
tree | 1c08ad4ffccb80041d26b17938764a86a94cfcce /src/parser | |
parent | ca5ec6ea328417757aa4e393ed029b5ed2c76939 (diff) |
Finishing parser cleanup. Code is now review-ready.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 18 | ||||
-rw-r--r-- | src/parser/input.cpp | 120 | ||||
-rw-r--r-- | src/parser/input.h | 46 | ||||
-rw-r--r-- | src/parser/smt/Smt.g | 21 |
4 files changed, 29 insertions, 176 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index f32da2eac..4cb4d577b 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -133,7 +133,9 @@ declType[CVC4::Type*& t, std::vector<std::string>& idList] Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl; } : /* A sort declaration (e.g., "T : TYPE") */ - TYPE_TOK { ANTLR_INPUT->newSorts(idList); t = ANTLR_INPUT->kindType(); } + TYPE_TOK + { ANTLR_INPUT->newSorts(idList); + t = EXPR_MANAGER->kindType(); } | /* A variable declaration */ type[t] { ANTLR_INPUT->mkVars(idList,t); } ; @@ -144,21 +146,21 @@ declType[CVC4::Type*& t, std::vector<std::string>& idList] */ type[CVC4::Type*& t] @init { + Type* t2; std::vector<Type*> typeList; Debug("parser-extra") << "type: " << AntlrInput::tokenText(LT(1)) << std::endl; } : /* Simple type */ baseType[t] | /* Single-parameter function type */ - baseType[t] { typeList.push_back(t); } - ARROW_TOK baseType[t] - { t = ANTLR_INPUT->functionType(typeList,t); } + baseType[t] ARROW_TOK baseType[t2] + { t = EXPR_MANAGER->mkFunctionType(t,t2); } | /* Multi-parameter function type */ LPAREN baseType[t] { typeList.push_back(t); } (COMMA baseType[t] { typeList.push_back(t); } )+ RPAREN ARROW_TOK baseType[t] - { t = ANTLR_INPUT->functionType(typeList,t); } + { t = EXPR_MANAGER->mkFunctionType(typeList,t); } ; /** @@ -198,7 +200,7 @@ baseType[CVC4::Type*& t] std::string id; Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl; } - : BOOLEAN_TOK { t = ANTLR_INPUT->booleanType(); } + : BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); } | typeSymbol[t] ; @@ -415,9 +417,9 @@ functionSymbol[CVC4::Expr& f] Debug("parser-extra") << "function symbol: " << AntlrInput::tokenText(LT(1)) << std::endl; std::string name; } - : identifier[name,CHECK_DECLARED,SYM_FUNCTION] + : identifier[name,CHECK_DECLARED,SYM_VARIABLE] { ANTLR_INPUT->checkFunction(name); - f = ANTLR_INPUT->getFunction(name); } + f = ANTLR_INPUT->getVariable(name); } ; diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 06faf5106..01de4ea4f 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -163,7 +163,6 @@ Expr Input::getSymbol(const std::string& name, SymbolType type) { switch( type ) { case SYM_VARIABLE: // Functions share var namespace - case SYM_FUNCTION: return d_varSymbolTable.getObject(name); default: @@ -176,10 +175,6 @@ Expr Input::getVariable(const std::string& name) { return getSymbol(name, SYM_VARIABLE); } -Expr Input::getFunction(const std::string& name) { - return getSymbol(name, SYM_FUNCTION); -} - Type* Input::getType(const std::string& var_name, SymbolType type) { @@ -201,46 +196,12 @@ bool Input::isBoolean(const std::string& name) { /* Returns true if name is bound to a function. */ bool Input::isFunction(const std::string& name) { - return isDeclared(name, SYM_FUNCTION) && getType(name)->isFunction(); + 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_FUNCTION) && getType(name)->isPredicate(); -} - -Type* -Input::functionType(Type* domainType, - Type* rangeType) { - return d_exprManager->mkFunctionType(domainType,rangeType); -} - -Type* -Input::functionType(const std::vector<Type*>& argTypes, - Type* rangeType) { - Assert( argTypes.size() > 0 ); - return d_exprManager->mkFunctionType(argTypes,rangeType); -} - -Type* -Input::functionType(const std::vector<Type*>& sorts) { - Assert( sorts.size() > 0 ); - if( sorts.size() == 1 ) { - return sorts[0]; - } else { - std::vector<Type*> argTypes(sorts); - Type* rangeType = argTypes.back(); - argTypes.pop_back(); - return functionType(argTypes,rangeType); - } -} - -Type* Input::predicateType(const std::vector<Type*>& sorts) { - if(sorts.size() == 0) { - return d_exprManager->booleanType(); - } else { - return d_exprManager->mkFunctionType(sorts, d_exprManager->booleanType()); - } + return isDeclared(name, SYM_VARIABLE) && getType(name)->isPredicate(); } Expr @@ -303,80 +264,9 @@ Input::newSorts(const std::vector<std::string>& names) { return types; } -BooleanType* Input::booleanType() { - return d_exprManager->booleanType(); -} - -KindType* Input::kindType() { - return d_exprManager->kindType(); -} - -unsigned int Input::minArity(Kind kind) { - switch(kind) { - case FALSE: - case SKOLEM: - case TRUE: - case VARIABLE: - return 0; - - case AND: - case NOT: - case OR: - return 1; - - case APPLY_UF: - case DISTINCT: - case EQUAL: - case IFF: - case IMPLIES: - case PLUS: - case XOR: - return 2; - - case ITE: - return 3; - - default: - Unhandled(kind); - } -} - -unsigned int Input::maxArity(Kind kind) { - switch(kind) { - case FALSE: - case SKOLEM: - case TRUE: - case VARIABLE: - return 0; - - case NOT: - return 1; - - case EQUAL: - case IFF: - case IMPLIES: - case XOR: - return 2; - - case ITE: - return 3; - - case AND: - case APPLY_UF: - case DISTINCT: - case PLUS: - case OR: - return UINT_MAX; - - default: - Unhandled(kind); - } -} - bool Input::isDeclared(const std::string& name, SymbolType type) { switch(type) { - case SYM_VARIABLE: // Functions share var namespace - case SYM_FUNCTION: + case SYM_VARIABLE: return d_varSymbolTable.isBound(name); case SYM_SORT: return d_sortTable.isBound(name); @@ -427,8 +317,8 @@ void Input::checkArity(Kind kind, unsigned int numArgs) return; } - unsigned int min = minArity(kind); - unsigned int max = maxArity(kind); + unsigned int min = d_exprManager->minArity(kind); + unsigned int max = d_exprManager->maxArity(kind); if( numArgs < min || numArgs > max ) { stringstream ss; diff --git a/src/parser/input.h b/src/parser/input.h index 42a94ab41..90cdc4e8d 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -66,8 +66,6 @@ inline std::string toString(DeclarationCheck check) { enum SymbolType { /** Variables */ SYM_VARIABLE, - /** Functions */ - SYM_FUNCTION, /** Sorts */ SYM_SORT }; @@ -77,7 +75,6 @@ enum SymbolType { inline std::string toString(SymbolType type) { switch(type) { case SYM_VARIABLE: return "SYM_VARIABLE"; - case SYM_FUNCTION: return "SYM_FUNCTION"; case SYM_SORT: return "SYM_SORT"; default: Unreachable(); } @@ -207,13 +204,6 @@ public: Expr getVariable(const std::string& var_name); /** - * Returns a function, given a name and a type. - * @param name the name of the function - * @return the function expression - */ - Expr getFunction(const std::string& name); - - /** * Returns a sort, given a name */ Type* getSort(const std::string& sort_name); @@ -278,30 +268,6 @@ public: /** Remove a variable definition (e.g., from a let binding). */ void undefineVar(const std::string& name); - /** Returns a function type over the given domain and range types. */ - Type* functionType(Type* domain, Type* range); - - /** Returns a function type over the given types. argTypes must be - non-empty. */ - Type* functionType(const std::vector<Type*>& argTypes, - Type* rangeType); - - /** - * Returns a function type over the given types. If types has only - * one element, then the type is just types[0]. - * - * @param types a non-empty list of input and output types. - */ - Type* functionType(const std::vector<Type*>& types); - - /** - * Returns a predicate type over the given sorts. If sorts is empty, - * then the type is just BOOLEAN. - - * @param sorts a list of input types - */ - Type* predicateType(const std::vector<Type*>& sorts); - /** * Creates a new sort with the given name. */ @@ -322,18 +288,6 @@ public: /** Is the symbol bound to a predicate? */ bool isPredicate(const std::string& name); - /** Returns the boolean type. */ - BooleanType* booleanType(); - - /** Returns the kind type (i.e., the type of types). */ - KindType* kindType(); - - /** Returns the minimum arity of the given kind. */ - static unsigned int minArity(Kind kind); - - /** Returns the maximum arity of the given kind. */ - static unsigned int maxArity(Kind kind); - /** Throws a <code>ParserException</code> with the given error message. * Implementations should fill in the <code>ParserException</code> with * line number information, etc. */ diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 56bedce81..d03cbf47e 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -255,7 +255,7 @@ predicateName[std::string& name, CVC4::parser::DeclarationCheck check] * @param check what kind of check to do with the symbol */ functionName[std::string& name, CVC4::parser::DeclarationCheck check] - : identifier[name,check,SYM_FUNCTION] + : identifier[name,check,SYM_VARIABLE] ; /** @@ -267,7 +267,7 @@ functionSymbol[CVC4::Expr& fun] } : functionName[name,CHECK_DECLARED] { ANTLR_INPUT->checkFunction(name); - fun = ANTLR_INPUT->getFunction(name); } + fun = ANTLR_INPUT->getVariable(name); } ; /** @@ -277,8 +277,6 @@ attribute : ATTR_IDENTIFIER ; - - functionDeclaration @declarations { std::string name; @@ -288,7 +286,11 @@ functionDeclaration t = sortSymbol // require at least one sort { sorts.push_back(t); } sortList[sorts] RPAREN_TOK - { t = ANTLR_INPUT->functionType(sorts); + { if( sorts.size() == 1 ) { + Assert( t == sorts[0] ); + } else { + t = EXPR_MANAGER->mkFunctionType(sorts); + } ANTLR_INPUT->mkVar(name, t); } ; @@ -301,7 +303,12 @@ predicateDeclaration std::vector<Type*> p_sorts; } : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK - { Type *t = ANTLR_INPUT->predicateType(p_sorts); + { Type *t; + if( p_sorts.empty() ) { + t = EXPR_MANAGER->booleanType(); + } else { + t = EXPR_MANAGER->mkPredicateType(p_sorts); + } ANTLR_INPUT->mkVar(name, t); } ; @@ -395,7 +402,7 @@ fun_identifier[std::string& id, { id = AntlrInput::tokenText($FUN_IDENTIFIER); Debug("parser") << "fun_identifier: " << id << " check? " << toString(check) << std::endl; - ANTLR_INPUT->checkDeclaration(id, check, SYM_FUNCTION); } + ANTLR_INPUT->checkDeclaration(id, check); } ; |