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/cvc | |
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/cvc')
-rw-r--r-- | src/parser/cvc/cvc_parser.g | 50 |
1 files changed, 25 insertions, 25 deletions
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); } ; |