summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/cvc/Cvc.g14
-rw-r--r--src/parser/parser_state.cpp28
-rw-r--r--src/parser/parser_state.h12
-rw-r--r--src/parser/smt/Smt.g10
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback