diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-10 18:44:51 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-10 18:44:51 +0000 |
commit | f79afa96e7e7176b974252dd05a9f7bdf70194e8 (patch) | |
tree | cb12c0a880f8fbb356516a86699b0063a7bb8981 /src/parser/cvc | |
parent | 8b2d1d64b886db4cff74e2a7b1370841979001b2 (diff) |
killing expr into node...
Diffstat (limited to 'src/parser/cvc')
-rw-r--r-- | src/parser/cvc/cvc_parser.cpp | 6 | ||||
-rw-r--r-- | src/parser/cvc/cvc_parser.g | 14 | ||||
-rw-r--r-- | src/parser/cvc/cvc_parser.h | 4 |
3 files changed, 12 insertions, 12 deletions
diff --git a/src/parser/cvc/cvc_parser.cpp b/src/parser/cvc/cvc_parser.cpp index adeb5761d..2bb01007a 100644 --- a/src/parser/cvc/cvc_parser.cpp +++ b/src/parser/cvc/cvc_parser.cpp @@ -44,8 +44,8 @@ Command* CvcParser::parseNextCommand() throw(ParserException) { return cmd; } -Expr CvcParser::parseNextExpression() throw(ParserException) { - Expr result; +Node CvcParser::parseNextExpression() throw(ParserException) { + Node result; if(!done()) { try { result = d_antlr_parser->formula(); @@ -62,7 +62,7 @@ CvcParser::~CvcParser() { delete d_antlr_lexer; } -CvcParser::CvcParser(ExprManager*em, istream& input, const char* file_name) : +CvcParser::CvcParser(NodeManager*em, istream& input, const char* file_name) : Parser(em), d_input(input) { if(!d_input) { throw ParserException(string("Read error") + diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 625f2c381..812925b0b 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -34,7 +34,7 @@ options { */ command returns [CVC4::Command* cmd = 0] { - Expr f; + Node f; vector<string> ids; } : ASSERT f = formula { cmd = new AssertCommand(f); } @@ -60,15 +60,15 @@ type : BOOLEAN ; -formula returns [CVC4::Expr formula] +formula returns [CVC4::Node formula] : formula = bool_formula ; -bool_formula returns [CVC4::Expr formula] +bool_formula returns [CVC4::Node formula] { - vector<Expr> formulas; + vector<Node> formulas; vector<Kind> kinds; - Expr f1, f2; + Node f1, f2; Kind k; } : f1 = primary_bool_formula { formulas.push_back(f1); } @@ -79,7 +79,7 @@ bool_formula returns [CVC4::Expr formula] } ; -primary_bool_formula returns [CVC4::Expr formula] +primary_bool_formula returns [CVC4::Node formula] : formula = bool_atom | NOT formula = primary_bool_formula { formula = newExpression(CVC4::NOT, formula); } | LPAREN formula = bool_formula RPAREN @@ -93,7 +93,7 @@ bool_operator returns [CVC4::Kind kind] | IFF { kind = CVC4::IFF; } ; -bool_atom returns [CVC4::Expr atom] +bool_atom returns [CVC4::Node atom] { string p; } diff --git a/src/parser/cvc/cvc_parser.h b/src/parser/cvc/cvc_parser.h index 9cb6b7594..07699916f 100644 --- a/src/parser/cvc/cvc_parser.h +++ b/src/parser/cvc/cvc_parser.h @@ -37,7 +37,7 @@ public: * @param input the input stream to parse * @param file_name the name of the file (for diagnostic output) */ - CvcParser(ExprManager* em, std::istream& input, const char* file_name = ""); + CvcParser(NodeManager* em, std::istream& input, const char* file_name = ""); /** * Destructor. @@ -57,7 +57,7 @@ public: * Parses the next complete expression of the stream. * @return the expression parsed */ - Expr parseNextExpression() throw(ParserException); + Node parseNextExpression() throw(ParserException); protected: |