diff options
Diffstat (limited to 'src/parser/smt')
-rw-r--r-- | src/parser/smt/smt_parser.cpp | 6 | ||||
-rw-r--r-- | src/parser/smt/smt_parser.g | 18 | ||||
-rw-r--r-- | src/parser/smt/smt_parser.h | 4 |
3 files changed, 14 insertions, 14 deletions
diff --git a/src/parser/smt/smt_parser.cpp b/src/parser/smt/smt_parser.cpp index 411866540..65d36690c 100644 --- a/src/parser/smt/smt_parser.cpp +++ b/src/parser/smt/smt_parser.cpp @@ -41,8 +41,8 @@ Command* SmtParser::parseNextCommand() throw(ParserException) { return cmd; } -Node SmtParser::parseNextExpression() throw(ParserException) { - Node result; +Expr SmtParser::parseNextExpression() throw(ParserException) { + Expr result; if(!done()) { try { result = d_antlr_parser->an_formula(); @@ -59,7 +59,7 @@ SmtParser::~SmtParser() { delete d_antlr_lexer; } -SmtParser::SmtParser(NodeManager* em, istream& input, const char* file_name) : +SmtParser::SmtParser(ExprManager* 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/smt/smt_parser.g b/src/parser/smt/smt_parser.g index c2f5c145b..b1bb35e6f 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -60,7 +60,7 @@ pred_symb returns [std::string p] /** * Matches a propositional atom from the input. */ -prop_atom returns [CVC4::Node atom] +prop_atom returns [CVC4::Expr atom] { std::string p; } @@ -78,14 +78,14 @@ prop_atom returns [CVC4::Node atom] * enclosed in brackets. The prop_atom rule from the original SMT grammar is inlined * here in order to get rid of the ugly antlr non-determinism warrnings. */ -an_atom returns [CVC4::Node atom] +an_atom returns [CVC4::Expr atom] : atom = prop_atom ; /** * Matches on of the unary Boolean conectives. */ -connective returns [CVC4::Kind kind] +bool_connective returns [CVC4::Kind kind] : NOT { kind = CVC4::NOT; } | IMPLIES { kind = CVC4::IMPLIES; } | AND { kind = CVC4::AND; } @@ -97,18 +97,18 @@ connective returns [CVC4::Kind kind] /** * Matches an annotated formula. */ -an_formula returns [CVC4::Node formula] +an_formula returns [CVC4::Expr formula] { Kind kind; - vector<Node> children; + vector<Expr> children; } : formula = an_atom - | LPAREN kind = connective an_formulas[children] RPAREN { formula = newExpression(kind, children); } + | LPAREN kind = bool_connective an_formulas[children] RPAREN { formula = newExpression(kind, children); } ; -an_formulas[std::vector<Node>& formulas] +an_formulas[std::vector<Expr>& formulas] { - Node f; + Expr f; } : ( f = an_formula { formulas.push_back(f); } )+ ; @@ -149,7 +149,7 @@ status returns [ AntlrParser::BenchmarkStatus status ] bench_attribute returns [ Command* smt_command = 0] { BenchmarkStatus b_status = SMT_UNKNOWN; - Node formula; + Expr formula; vector<string> sorts; } : C_LOGIC IDENTIFIER diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h index 7dedcd5b4..a68f0e783 100644 --- a/src/parser/smt/smt_parser.h +++ b/src/parser/smt/smt_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) */ - SmtParser(NodeManager* em, std::istream& input, const char* file_name = ""); + SmtParser(ExprManager* 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 */ - Node parseNextExpression() throw(ParserException); + Expr parseNextExpression() throw(ParserException); protected: |