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 | |
parent | 8b2d1d64b886db4cff74e2a7b1370841979001b2 (diff) |
killing expr into node...
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/antlr_parser.cpp | 25 | ||||
-rw-r--r-- | src/parser/antlr_parser.h | 26 | ||||
-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 | ||||
-rw-r--r-- | src/parser/parser.cpp | 2 | ||||
-rw-r--r-- | src/parser/parser.h | 10 | ||||
-rw-r--r-- | src/parser/smt/smt_parser.cpp | 6 | ||||
-rw-r--r-- | src/parser/smt/smt_parser.g | 14 | ||||
-rw-r--r-- | src/parser/smt/smt_parser.h | 4 | ||||
-rw-r--r-- | src/parser/symbol_table.h | 2 |
11 files changed, 55 insertions, 58 deletions
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 04a82f721..d81336b53 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -8,7 +8,6 @@ #include <iostream> #include "antlr_parser.h" -#include "expr/expr_manager.h" #include "util/output.h" using namespace std; @@ -66,29 +65,29 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) : antlr::LLkParser(lexer, k) { } -Expr AntlrParser::getVariable(std::string var_name) { - Expr e = d_var_symbol_table.getObject(var_name); +Node AntlrParser::getVariable(std::string var_name) { + Node e = d_var_symbol_table.getObject(var_name); Debug("parser") << "getvar " << var_name << " gives " << e << endl; return e; } -Expr AntlrParser::getTrueExpr() const { +Node AntlrParser::getTrueExpr() const { return d_expr_manager->mkExpr(TRUE); } -Expr AntlrParser::getFalseExpr() const { +Node AntlrParser::getFalseExpr() const { return d_expr_manager->mkExpr(FALSE); } -Expr AntlrParser::newExpression(Kind kind, const Expr& child) { +Node AntlrParser::newExpression(Kind kind, const Node& child) { return d_expr_manager->mkExpr(kind, child); } -Expr AntlrParser::newExpression(Kind kind, const Expr& child_1, const Expr& child_2) { +Node AntlrParser::newExpression(Kind kind, const Node& child_1, const Node& child_2) { return d_expr_manager->mkExpr(kind, child_1, child_2); } -Expr AntlrParser::newExpression(Kind kind, const std::vector<Expr>& children) { +Node AntlrParser::newExpression(Kind kind, const std::vector<Node>& children) { return d_expr_manager->mkExpr(kind, children); } @@ -113,7 +112,7 @@ void AntlrParser::setBenchmarkStatus(BenchmarkStatus status) { void AntlrParser::addExtraSorts(const std::vector<std::string>& extra_sorts) { } -void AntlrParser::setExpressionManager(ExprManager* em) { +void AntlrParser::setExpressionManager(NodeManager* em) { d_expr_manager = em; } @@ -133,7 +132,7 @@ void AntlrParser::rethrow(antlr::SemanticException& e, string new_message) LT(0).get()->getColumn()); } -Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs, const vector< +Node AntlrParser::createPrecedenceExpr(const vector<Node>& exprs, const vector< Kind>& kinds) { return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1); } @@ -155,7 +154,7 @@ unsigned AntlrParser::findPivot(const std::vector<Kind>& kinds, return pivot; } -Expr AntlrParser::createPrecedenceExpr(const std::vector<Expr>& exprs, +Node AntlrParser::createPrecedenceExpr(const std::vector<Node>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index) { if(start_index == end_index) @@ -163,8 +162,8 @@ Expr AntlrParser::createPrecedenceExpr(const std::vector<Expr>& exprs, unsigned pivot = findPivot(kinds, start_index, end_index - 1); - Expr child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot); - Expr child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index); + Node child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot); + Node child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index); return d_expr_manager->mkExpr(kinds[pivot], child_1, child_2); } diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index ad23d45f8..26f206e43 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -15,8 +15,8 @@ #include <antlr/LLkParser.hpp> #include <antlr/SemanticException.hpp> -#include "expr/expr.h" -#include "expr/expr_manager.h" +#include "expr/node.h" +#include "expr/node_manager.h" #include "util/command.h" #include "util/Assert.h" #include "parser/symbol_table.h" @@ -48,7 +48,7 @@ public: * Set's the expression manager to use when creating/managing expression. * @param expr_manager the expression manager */ - void setExpressionManager(ExprManager* expr_manager); + void setExpressionManager(NodeManager* expr_manager); protected: @@ -89,7 +89,7 @@ protected: * @param var_name the name of the variable * @return the variable expression */ - Expr getVariable(std::string var_name); + Node getVariable(std::string var_name); /** * Types of symbols. @@ -113,40 +113,40 @@ protected: * Returns the true expression. * @return the true expression */ - Expr getTrueExpr() const; + Node getTrueExpr() const; /** * Returns the false expression. * @return the false expression */ - Expr getFalseExpr() const; + Node getFalseExpr() const; /** * Creates a new unary CVC4 expression using the expression manager. * @param kind the kind of the expression * @param child the child */ - Expr newExpression(Kind kind, const Expr& child); + Node newExpression(Kind kind, const Node& child); /** * Creates a new binary CVC4 expression using the expression manager. * @param kind the kind of the expression * @param children the children of the expression */ - Expr newExpression(Kind kind, const Expr& child_1, const Expr& child_2); + Node newExpression(Kind kind, const Node& child_1, const Node& child_2); /** * Creates a new CVC4 expression using the expression manager. * @param kind the kind of the expression * @param children the children of the expression */ - Expr newExpression(Kind kind, const std::vector<Expr>& children); + Node newExpression(Kind kind, const std::vector<Node>& children); /** * Creates a new expression based on the given string of expressions and kinds. * The expression is created so that it respects the kinds precedence table. */ - Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds); + Node createPrecedenceExpr(const std::vector<Node>& exprs, const std::vector<Kind>& kinds); /** * Creates a new predicated over the given sorts. @@ -193,16 +193,16 @@ private: * Creates a new expression based on the given string of expressions and kinds. * The expression is created so that it respects the kinds precedence table. */ - Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index); + Node createPrecedenceExpr(const std::vector<Node>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index); /** The status of the benchmark */ BenchmarkStatus d_benchmark_status; /** The expression manager */ - ExprManager* d_expr_manager; + NodeManager* d_expr_manager; /** The symbol table lookup */ - SymbolTable<Expr> d_var_symbol_table; + SymbolTable<Node> d_var_symbol_table; }; std::ostream& operator<<(std::ostream& out, AntlrParser::BenchmarkStatus status); 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: diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 8d4af5ba1..c6d5bcb5c 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -28,7 +28,7 @@ using namespace std; namespace CVC4 { namespace parser { -Parser::Parser(ExprManager* em) : +Parser::Parser(NodeManager* em) : d_expr_manager(em), d_done(false) { } diff --git a/src/parser/parser.h b/src/parser/parser.h index 7755d65f0..7f63261c7 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -22,9 +22,9 @@ namespace CVC4 { // Forward declarations -class Expr; +class Node; class Command; -class ExprManager; +class NodeManager; namespace parser { @@ -44,7 +44,7 @@ public: * Construct the parser that uses the given expression manager. * @param em the expression manager. */ - Parser(ExprManager* em); + Parser(NodeManager* em); /** * Destructor. @@ -60,7 +60,7 @@ public: /** * Parse the next expression of the stream */ - virtual Expr parseNextExpression() throw (ParserException) = 0; + virtual Node parseNextExpression() throw (ParserException) = 0; /** * Check if we are done -- either the end of input has been reached. @@ -73,7 +73,7 @@ protected: void setDone(bool done = true); /** Expression manager the parser will be using */ - ExprManager* d_expr_manager; + NodeManager* d_expr_manager; /** Are we done */ bool d_done; diff --git a/src/parser/smt/smt_parser.cpp b/src/parser/smt/smt_parser.cpp index 65d36690c..411866540 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; } -Expr SmtParser::parseNextExpression() throw(ParserException) { - Expr result; +Node SmtParser::parseNextExpression() throw(ParserException) { + Node result; if(!done()) { try { result = d_antlr_parser->an_formula(); @@ -59,7 +59,7 @@ SmtParser::~SmtParser() { delete d_antlr_lexer; } -SmtParser::SmtParser(ExprManager* em, istream& input, const char* file_name) : +SmtParser::SmtParser(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/smt/smt_parser.g b/src/parser/smt/smt_parser.g index f68d783bc..c2f5c145b 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::Expr atom] +prop_atom returns [CVC4::Node atom] { std::string p; } @@ -78,7 +78,7 @@ prop_atom returns [CVC4::Expr 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::Expr atom] +an_atom returns [CVC4::Node atom] : atom = prop_atom ; @@ -97,18 +97,18 @@ connective returns [CVC4::Kind kind] /** * Matches an annotated formula. */ -an_formula returns [CVC4::Expr formula] +an_formula returns [CVC4::Node formula] { Kind kind; - vector<Expr> children; + vector<Node> children; } : formula = an_atom | LPAREN kind = connective an_formulas[children] RPAREN { formula = newExpression(kind, children); } ; -an_formulas[std::vector<Expr>& formulas] +an_formulas[std::vector<Node>& formulas] { - Expr f; + Node 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; - Expr formula; + Node formula; vector<string> sorts; } : C_LOGIC IDENTIFIER diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h index a68f0e783..7dedcd5b4 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(ExprManager* em, std::istream& input, const char* file_name = ""); + SmtParser(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: diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h index 32532c734..2c4f0e8b7 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -16,8 +16,6 @@ #include <stack> #include <ext/hash_map> -#include "expr/expr.h" - namespace __gnu_cxx { template<> struct hash<std::string> { |