diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 14 | ||||
-rw-r--r-- | src/parser/parser_state.cpp | 28 | ||||
-rw-r--r-- | src/parser/parser_state.h | 12 | ||||
-rw-r--r-- | src/parser/smt/Smt.g | 10 |
4 files changed, 32 insertions, 32 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 16bde1de3..3f4435966 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -123,7 +123,7 @@ command returns [CVC4::Command* cmd = 0] declaration[CVC4::Command*& cmd] @init { std::vector<std::string> ids; - Type* t; + Type t; Debug("parser-extra") << "declaration: " << AntlrInput::tokenText(LT(1)) << std::endl; } : // FIXME: These could be type or function declarations, if that matters. @@ -132,7 +132,7 @@ declaration[CVC4::Command*& cmd] ; /** Match the right-hand side of a declaration. Returns the type. */ -declType[CVC4::Type*& t, std::vector<std::string>& idList] +declType[CVC4::Type& t, std::vector<std::string>& idList] @init { Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl; } @@ -148,10 +148,10 @@ declType[CVC4::Type*& t, std::vector<std::string>& idList] * Match the type in a declaration and do the declaration binding. * TODO: Actually parse sorts into Type objects. */ -type[CVC4::Type*& t] +type[CVC4::Type& t] @init { - Type* t2; - std::vector<Type*> typeList; + Type t2; + std::vector<Type> typeList; Debug("parser-extra") << "type: " << AntlrInput::tokenText(LT(1)) << std::endl; } : /* Simple type */ @@ -199,7 +199,7 @@ identifier[std::string& id, * Matches a type. * TODO: parse more types */ -baseType[CVC4::Type*& t] +baseType[CVC4::Type& t] @init { std::string id; Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl; @@ -211,7 +211,7 @@ baseType[CVC4::Type*& t] /** * Matches a type identifier */ -typeSymbol[CVC4::Type*& t] +typeSymbol[CVC4::Type& t] @init { std::string id; Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl; diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp index 5f07b16b7..57914c9de 100644 --- a/src/parser/parser_state.cpp +++ b/src/parser/parser_state.cpp @@ -62,38 +62,38 @@ Expr ParserState::getVariable(const std::string& name) { return getSymbol(name, SYM_VARIABLE); } -Type* +Type ParserState::getType(const std::string& var_name, SymbolType type) { Assert( isDeclared(var_name, type) ); - Type* t = getSymbol(var_name,type).getType(); + Type t = getSymbol(var_name,type).getType(); return t; } -Type* ParserState::getSort(const std::string& name) { +Type ParserState::getSort(const std::string& name) { Assert( isDeclared(name, SYM_SORT) ); - Type *t = d_declScope.lookupType(name); + Type t = d_declScope.lookupType(name); return t; } /* Returns true if name is bound to a boolean variable. */ bool ParserState::isBoolean(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name)->isBoolean(); + return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean(); } /* Returns true if name is bound to a function. */ bool ParserState::isFunction(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name)->isFunction(); + return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction(); } /* Returns true if name is bound to a function returning boolean. */ bool ParserState::isPredicate(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name)->isPredicate(); + return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate(); } Expr -ParserState::mkVar(const std::string& name, Type* type) { - Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl; +ParserState::mkVar(const std::string& name, const Type& type) { + Debug("parser") << "mkVar(" << name << "," << type << ")" << std::endl; Expr expr = d_exprManager->mkVar(name, type); defineVar(name,expr); return expr; @@ -101,7 +101,7 @@ ParserState::mkVar(const std::string& name, Type* type) { const std::vector<Expr> ParserState::mkVars(const std::vector<std::string> names, - Type* type) { + const Type& type) { std::vector<Expr> vars; for(unsigned i = 0; i < names.size(); ++i) { vars.push_back(mkVar(names[i],type)); @@ -134,19 +134,19 @@ ParserState::setLogic(const std::string& name) { } } -Type* +Type ParserState::mkSort(const std::string& name) { Debug("parser") << "newSort(" << name << ")" << std::endl; Assert( !isDeclared(name, SYM_SORT) ) ; - Type* type = d_exprManager->mkSort(name); + Type type = d_exprManager->mkSort(name); d_declScope.bindType(name, type); Assert( isDeclared(name, SYM_SORT) ) ; return type; } -const std::vector<Type*> +const std::vector<Type> ParserState::mkSorts(const std::vector<std::string>& names) { - std::vector<Type*> types; + std::vector<Type> types; for(unsigned i = 0; i < names.size(); ++i) { types.push_back(mkSort(names[i])); } diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index de624e3a0..3ca9c2c0e 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -174,7 +174,7 @@ public: /** * Returns a sort, given a name */ - Type* getSort(const std::string& sort_name); + Type getSort(const std::string& sort_name); /** * Checks if a symbol has been declared. @@ -216,15 +216,15 @@ public: * @param var_name the symbol to lookup * @param type the (namespace) type of the symbol */ - Type* getType(const std::string& var_name, SymbolType type = SYM_VARIABLE); + Type getType(const std::string& var_name, SymbolType type = SYM_VARIABLE); /** Create a new CVC4 variable expression of the given type. */ - Expr mkVar(const std::string& name, Type* type); + Expr mkVar(const std::string& name, const Type& type); /** Create a set of new CVC4 variable expressions of the given type. */ const std::vector<Expr> - mkVars(const std::vector<std::string> names, Type* type); + mkVars(const std::vector<std::string> names, const Type& type); /** Create a new variable definition (e.g., from a let binding). */ void defineVar(const std::string& name, const Expr& val); @@ -234,12 +234,12 @@ public: /** * Creates a new sort with the given name. */ - Type* mkSort(const std::string& name); + Type mkSort(const std::string& name); /** * Creates a new sorts with the given names. */ - const std::vector<Type*> + const std::vector<Type> mkSorts(const std::vector<std::string>& names); /** Is the symbol bound to a boolean variable? */ diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 25c2fbc89..15f0c8844 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -285,7 +285,7 @@ attribute functionDeclaration @declarations { std::string name; - std::vector<Type*> sorts; + std::vector<Type> sorts; } : LPAREN_TOK functionName[name,CHECK_UNDECLARED] t = sortSymbol // require at least one sort @@ -305,10 +305,10 @@ functionDeclaration predicateDeclaration @declarations { std::string name; - std::vector<Type*> p_sorts; + std::vector<Type> p_sorts; } : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK - { Type *t; + { Type t; if( p_sorts.empty() ) { t = EXPR_MANAGER->booleanType(); } else { @@ -329,7 +329,7 @@ sortDeclaration /** * Matches a sequence of sort symbols and fills them into the given vector. */ -sortList[std::vector<CVC4::Type*>& sorts] +sortList[std::vector<CVC4::Type>& sorts] : ( t = sortSymbol { sorts.push_back(t); })* ; @@ -341,7 +341,7 @@ sortName[std::string& name, CVC4::parser::DeclarationCheck check] : identifier[name,check,SYM_SORT] ; -sortSymbol returns [CVC4::Type* t] +sortSymbol returns [CVC4::Type t] @declarations { std::string name; } |