diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-16 20:24:37 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-16 20:24:37 +0000 |
commit | 9576517676138a8ca2887a967f1b056662ef6754 (patch) | |
tree | f0040a8189d20496dcaa760055b2b818f8a57525 /src/parser | |
parent | 12ad4cf2de936acbf8c21117804c69b2deaa7272 (diff) |
* test/unit/Makefile.am, test/unit/expr/attribute_white.h,
test/unit/expr/node_white.h: add whitebox attribute test (pulled out
attribute stuff from node_white)
* test/unit/parser/parser_black.h: fix memory leaks uncovered by
valgrind
* src/theory/interrupted.h: actually make this "lightweight" (not
derived from CVC4::Exception), as promised in my last commit
* src/theory/uf/theory_uf.h, test/unit/expr/attribute_black.h: match
the new-style cleanup function definition
* src/expr/attribute.cpp, src/expr/attribute.h: support for attribute
deletion, custom cleanup functions, clearer cleanup function
definition.
* src/expr/node_manager.h, src/expr/node_manager.cpp: reclaim
remaining zombies in dtor, rename NodeValueSet ==> "NodeValuePool",
and enable freeing of NodeValues
* src/expr/type.h, src/expr/type.cpp: reference-counting for types,
customized cleanup function for types, also code cleanup
* (various): changed "const Type*" to "Type*" (to enable
reference-counting etc. Types are still immutable.)
* src/util/output.h: add ::isOn()-- which queries whether a
Debug/Trace flag is currently on or not.
* src/smt/smt_engine.cpp, src/parser/antlr_parser.cpp,
src/expr/type.cpp, src/expr/expr_manager.cpp, various others:
minor code cleanup
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/antlr_parser.cpp | 93 | ||||
-rw-r--r-- | src/parser/antlr_parser.h | 28 | ||||
-rw-r--r-- | src/parser/cvc/cvc_parser.g | 50 | ||||
-rw-r--r-- | src/parser/smt/smt_lexer.g | 4 | ||||
-rw-r--r-- | src/parser/smt/smt_parser.g | 76 |
5 files changed, 121 insertions, 130 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) diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index 94d919555..e970ebd52 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -137,7 +137,7 @@ protected: /** * Returns a sort, given a name */ - const Type* getSort(const std::string& sort_name); + Type* getSort(const std::string& sort_name); /** * Types of symbols. Used to define namespaces. @@ -193,7 +193,7 @@ protected: * @param name the symbol to lookup * @param type the (namespace) type of the symbol */ - const Type* getType(const std::string& var_name, + Type* getType(const std::string& var_name, SymbolType type = SYM_VARIABLE); /** @@ -244,13 +244,13 @@ protected: Expr mkExpr(Kind kind, const std::vector<Expr>& children); /** Create a new CVC4 variable expression of the given type. */ - Expr mkVar(const std::string& name, const Type* type); + Expr mkVar(const std::string& name, 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, - const Type* type); + Type* type); /** Create a new variable definition (e.g., from a let binding). */ void defineVar(const std::string& name, const Expr& val); @@ -258,12 +258,12 @@ protected: void undefineVar(const std::string& name); /** Returns a function type over the given domain and range types. */ - const Type* functionType(const Type* domain, const Type* range); + Type* functionType(Type* domain, Type* range); /** Returns a function type over the given types. argTypes must be non-empty. */ - const Type* functionType(const std::vector<const Type*>& argTypes, - const Type* rangeType); + Type* functionType(const std::vector<Type*>& argTypes, + Type* rangeType); /** * Returns a function type over the given types. If types has only @@ -271,7 +271,7 @@ protected: * * @param types a non-empty list of input and output types. */ - const Type* functionType(const std::vector<const Type*>& types); + Type* functionType(const std::vector<Type*>& types); /** * Returns a predicate type over the given sorts. If sorts is empty, @@ -279,17 +279,17 @@ protected: * @param sorts a list of input types */ - const Type* predicateType(const std::vector<const Type*>& sorts); + Type* predicateType(const std::vector<Type*>& sorts); /** * Creates a new sort with the given name. */ - const Type* newSort(const std::string& name); + Type* newSort(const std::string& name); /** * Creates a new sorts with the given names. */ - const std::vector<const Type*> + const std::vector<Type*> newSorts(const std::vector<std::string>& names); /** Is the symbol bound to a boolean variable? */ @@ -302,10 +302,10 @@ protected: bool isPredicate(const std::string& name); /** Returns the boolean type. */ - const BooleanType* booleanType(); + BooleanType* booleanType(); /** Returns the kind type (i.e., the type of types). */ - const KindType* kindType(); + KindType* kindType(); /** Returns the minimum arity of the given kind. */ static unsigned int minArity(Kind kind); @@ -346,7 +346,7 @@ private: SymbolTable<Expr> d_varSymbolTable; /** The sort table */ - SymbolTable<const Type*> d_sortTable; + SymbolTable<Type*> d_sortTable; /** Are semantic checks enabled during parsing? */ bool d_checksEnabled; diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 9492b36d9..55ae0ff73 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -89,15 +89,15 @@ command returns [CVC4::Command* cmd = 0] declaration returns [CVC4::DeclarationCommand* cmd] { vector<string> ids; - const Type* t; + Type* t; Debug("parser") << "declaration: " << LT(1)->getText() << endl; -} +} : identifierList[ids, CHECK_UNDECLARED] COLON t = declType[ids] SEMICOLON { cmd = new DeclarationCommand(ids,t); } ; /** Match the right-hand side of a declaration. Returns the type. */ -declType[std::vector<std::string>& idList] returns [const CVC4::Type* t] +declType[std::vector<std::string>& idList] returns [CVC4::Type* t] { Debug("parser") << "declType: " << LT(1)->getText() << endl; } @@ -111,9 +111,9 @@ declType[std::vector<std::string>& idList] returns [const CVC4::Type* t] * Match the type in a declaration and do the declaration binding. * TODO: Actually parse sorts into Type objects. */ -type returns [const CVC4::Type* t] +type returns [CVC4::Type* t] { - const Type *t1, *t2; + Type *t1, *t2; Debug("parser") << "type: " << LT(1)->getText() << endl; } : /* Simple type */ @@ -122,10 +122,10 @@ type returns [const CVC4::Type* t] t1 = baseType RIGHT_ARROW t2 = baseType { t = functionType(t1,t2); } | /* Multi-parameter function type */ - LPAREN t1 = baseType - { std::vector<const Type*> argTypes; + LPAREN t1 = baseType + { std::vector<Type*> argTypes; argTypes.push_back(t1); } - (COMMA t1 = baseType { argTypes.push_back(t1); } )+ + (COMMA t1 = baseType { argTypes.push_back(t1); } )+ RPAREN RIGHT_ARROW t2 = baseType { t = functionType(argTypes,t2); } ; @@ -136,7 +136,7 @@ type returns [const CVC4::Type* t] * @param idList the list to fill with identifiers. * @param check what kinds of check to perform on the symbols */ -identifierList[std::vector<std::string>& idList, +identifierList[std::vector<std::string>& idList, DeclarationCheck check = CHECK_NONE] { string id; @@ -150,10 +150,10 @@ identifierList[std::vector<std::string>& idList, * Matches an identifier and returns a string. */ identifier[DeclarationCheck check = CHECK_NONE, - SymbolType type = SYM_VARIABLE] + SymbolType type = SYM_VARIABLE] returns [std::string id] : x:IDENTIFIER - { id = x->getText(); + { id = x->getText(); checkDeclaration(id, check, type); } ; @@ -161,7 +161,7 @@ returns [std::string id] * Matches a type. * TODO: parse more types */ -baseType returns [const CVC4::Type* t] +baseType returns [CVC4::Type* t] { std::string id; Debug("parser") << "base type: " << LT(1)->getText() << endl; @@ -173,7 +173,7 @@ baseType returns [const CVC4::Type* t] /** * Matches a type identifier */ -typeSymbol returns [const CVC4::Type* t] +typeSymbol returns [CVC4::Type* t] { std::string id; Debug("parser") << "type symbol: " << LT(1)->getText() << endl; @@ -228,7 +228,7 @@ impliesFormula returns [CVC4::Expr f] Expr e; Debug("parser") << "=> Formula: " << LT(1)->getText() << endl; } - : f = orFormula + : f = orFormula ( IMPLIES e = impliesFormula { f = mkExpr(CVC4::kind::IMPLIES, f, e); } )? @@ -259,7 +259,7 @@ xorFormula returns [CVC4::Expr f] Debug("parser") << "XOR formula: " << LT(1)->getText() << endl; } : f = andFormula - ( XOR e = andFormula + ( XOR e = andFormula { f = mkExpr(CVC4::kind::XOR,f, e); } )* ; @@ -289,7 +289,7 @@ notFormula returns [CVC4::Expr f] Debug("parser") << "NOT formula: " << LT(1)->getText() << endl; } : /* negation */ - NOT f = notFormula + NOT f = notFormula { f = mkExpr(CVC4::kind::NOT, f); } | /* a boolean atom */ f = predFormula @@ -300,7 +300,7 @@ predFormula returns [CVC4::Expr f] Debug("parser") << "predicate formula: " << LT(1)->getText() << endl; } : { Expr e; } - f = term + f = term (EQUAL e = term { f = mkExpr(CVC4::kind::EQUAL, f, e); } )? @@ -315,8 +315,8 @@ term returns [CVC4::Expr t] Debug("parser") << "term: " << LT(1)->getText() << endl; } : /* function application */ - // { isFunction(LT(1)->getText()) }? - { Expr f; + // { isFunction(LT(1)->getText()) }? + { Expr f; std::vector<CVC4::Expr> args; } f = functionSymbol[CHECK_DECLARED] { args.push_back( f ); } @@ -343,16 +343,16 @@ term returns [CVC4::Expr t] /** * Parses an ITE term. */ -iteTerm returns [CVC4::Expr t] +iteTerm returns [CVC4::Expr t] { Expr iteCondition, iteThen, iteElse; Debug("parser") << "ite: " << LT(1)->getText() << endl; } - : IF iteCondition = formula + : IF iteCondition = formula THEN iteThen = formula iteElse = iteElseTerm - ENDIF - { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); } + ENDIF + { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); } ; /** @@ -379,8 +379,8 @@ functionSymbol[DeclarationCheck check = CHECK_NONE] returns [CVC4::Expr f] { Debug("parser") << "function symbol: " << LT(1)->getText() << endl; std::string name; -} +} : name = identifier[check,SYM_FUNCTION] - { checkFunction(name); + { checkFunction(name); f = getFunction(name); } ; diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g index e3985818c..d694cd93f 100644 --- a/src/parser/smt/smt_lexer.g +++ b/src/parser/smt/smt_lexer.g @@ -115,11 +115,11 @@ C_IDENTIFIER options { paraphrase = "an attribute (e.g., ':x')"; testLiterals = ; VAR_IDENTIFIER options { paraphrase = "a variable (e.g., '?x')"; testLiterals = false; } - : '?' IDENTIFIER + : '?' IDENTIFIER ; FUN_IDENTIFIER options { paraphrase = "a function variable (e.g, '$x')"; testLiterals = false; } - : '$' IDENTIFIER + : '$' IDENTIFIER ; diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index d1ac50651..f9758dc5c 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -102,12 +102,12 @@ benchAttribute returns [Command* smt_command = 0] { smt_command = new AssertCommand(formula); } | FORMULA_ATTR formula = annotatedFormula { smt_command = new CheckSatCommand(formula); } - | STATUS_ATTR b_status = status - { smt_command = new SetBenchmarkStatusCommand(b_status); } - | EXTRAFUNS_ATTR LPAREN (functionDeclaration)+ RPAREN - | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN - | EXTRASORTS_ATTR LPAREN (sortDeclaration)+ RPAREN - | NOTES_ATTR STRING_LITERAL + | STATUS_ATTR b_status = status + { smt_command = new SetBenchmarkStatusCommand(b_status); } + | EXTRAFUNS_ATTR LPAREN (functionDeclaration)+ RPAREN + | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN + | EXTRASORTS_ATTR LPAREN (sortDeclaration)+ RPAREN + | NOTES_ATTR STRING_LITERAL | annotation ; @@ -119,12 +119,12 @@ annotatedFormula returns [CVC4::Expr formula] { Debug("parser") << "annotated formula: " << LT(1)->getText() << endl; Kind kind = CVC4::kind::UNDEFINED_KIND; - vector<Expr> args; + vector<Expr> args; std::string name; Expr expr1, expr2, expr3; } : /* a built-in operator application */ - LPAREN kind = builtinOp annotatedFormulas[args] RPAREN + LPAREN kind = builtinOp annotatedFormulas[args] RPAREN { checkArity(kind, args.size()); formula = mkExpr(kind,args); } @@ -134,16 +134,16 @@ annotatedFormula returns [CVC4::Expr formula] { std::vector<Expr> diseqs; for(unsigned i = 0; i < args.size(); ++i) { for(unsigned j = i+1; j < args.size(); ++j) { - diseqs.push_back(mkExpr(CVC4::kind::NOT, + diseqs.push_back(mkExpr(CVC4::kind::NOT, mkExpr(CVC4::kind::EQUAL,args[i],args[j]))); } } formula = mkExpr(CVC4::kind::AND, diseqs); } | /* An ite expression */ - LPAREN (ITE | IF_THEN_ELSE) + LPAREN (ITE | IF_THEN_ELSE) { Expr test, trueExpr, falseExpr; } - test = annotatedFormula + test = annotatedFormula trueExpr = annotatedFormula falseExpr = annotatedFormula RPAREN @@ -164,12 +164,12 @@ annotatedFormula returns [CVC4::Expr formula] formula=annotatedFormula { undefineVar(name); } RPAREN - + | /* A non-built-in function application */ // Semantic predicate not necessary if parenthesized subexpressions // are disallowed - // { isFunction(LT(2)->getText()) }? + // { isFunction(LT(2)->getText()) }? { Expr f; } LPAREN f = functionSymbol @@ -180,7 +180,7 @@ annotatedFormula returns [CVC4::Expr formula] | /* a variable */ { std::string name; } - ( name = identifier[CHECK_DECLARED] + ( name = identifier[CHECK_DECLARED] | name = variable[CHECK_DECLARED] | name = function_var[CHECK_DECLARED] ) { formula = getVariable(name); } @@ -195,7 +195,7 @@ annotatedFormula returns [CVC4::Expr formula] * Matches a sequence of annotaed formulas and puts them into the formulas * vector. * @param formulas the vector to fill with formulas - */ + */ annotatedFormulas[std::vector<Expr>& formulas] { Expr f; @@ -222,7 +222,7 @@ builtinOp returns [CVC4::Kind kind] ; /** - * Matches a (possibly undeclared) predicate identifier (returning the string). + * Matches a (possibly undeclared) predicate identifier (returning the string). * @param check what kind of check to do with the symbol */ predicateName[DeclarationCheck check = CHECK_NONE] returns [std::string p] @@ -241,14 +241,14 @@ functionName[DeclarationCheck check = CHECK_NONE] returns [std::string name] * Matches an previously declared function symbol (returning an Expr) */ functionSymbol returns [CVC4::Expr fun] -{ +{ string name; } : name = functionName[CHECK_DECLARED] { checkFunction(name); fun = getFunction(name); } ; - + /** * Matches an attribute name from the input (:attribute_name). */ @@ -272,12 +272,12 @@ function_var[DeclarationCheck check = CHECK_NONE] returns [std::string name] * Matches the sort symbol, which can be an arbitrary identifier. * @param check the check to perform on the name */ -sortName[DeclarationCheck check = CHECK_NONE] returns [std::string name] - : name = identifier[check,SYM_SORT] +sortName[DeclarationCheck check = CHECK_NONE] returns [std::string name] + : name = identifier[check,SYM_SORT] ; -sortSymbol returns [const CVC4::Type* t] -{ +sortSymbol returns [CVC4::Type* t] +{ std::string name; } : name = sortName { t = getSort(name); } @@ -286,47 +286,47 @@ sortSymbol returns [const CVC4::Type* t] functionDeclaration { string name; - const Type* t; - std::vector<const Type*> sorts; + Type* t; + std::vector<Type*> sorts; } - : LPAREN name = functionName[CHECK_UNDECLARED] + : LPAREN name = functionName[CHECK_UNDECLARED] t = sortSymbol // require at least one sort { sorts.push_back(t); } sortList[sorts] RPAREN { t = functionType(sorts); - mkVar(name, t); } + mkVar(name, t); } ; - + /** * Matches the declaration of a predicate and declares it */ predicateDeclaration { string p_name; - std::vector<const Type*> p_sorts; - const Type *t; + std::vector<Type*> p_sorts; + Type *t; } : LPAREN p_name = predicateName[CHECK_UNDECLARED] sortList[p_sorts] RPAREN { t = predicateType(p_sorts); - mkVar(p_name, t); } + mkVar(p_name, t); } ; -sortDeclaration +sortDeclaration { string name; } : name = sortName[CHECK_UNDECLARED] { newSort(name); } ; - + /** * Matches a sequence of sort symbols and fills them into the given vector. */ -sortList[std::vector<const Type*>& sorts] +sortList[std::vector<Type*>& sorts] { - const Type* t; + Type* t; } - : ( t = sortSymbol { sorts.push_back(t); })* + : ( t = sortSymbol { sorts.push_back(t); })* ; /** @@ -350,11 +350,11 @@ annotation * @param check what kinds of check to do on the symbol * @return the id string */ -identifier[DeclarationCheck check = CHECK_NONE, - SymbolType type = SYM_VARIABLE] +identifier[DeclarationCheck check = CHECK_NONE, + SymbolType type = SYM_VARIABLE] returns [std::string id] { - Debug("parser") << "identifier: " << LT(1)->getText() + Debug("parser") << "identifier: " << LT(1)->getText() << " check? " << toString(check) << " type? " << toString(type) << endl; } |