diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/antlr_parser.cpp | 24 | ||||
-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 | 18 | ||||
-rw-r--r-- | src/parser/smt/smt_parser.h | 4 |
10 files changed, 57 insertions, 57 deletions
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index d81336b53..a50b1f18f 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -65,29 +65,29 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) : antlr::LLkParser(lexer, k) { } -Node AntlrParser::getVariable(std::string var_name) { - Node e = d_var_symbol_table.getObject(var_name); +Expr AntlrParser::getVariable(std::string var_name) { + Expr e = d_var_symbol_table.getObject(var_name); Debug("parser") << "getvar " << var_name << " gives " << e << endl; return e; } -Node AntlrParser::getTrueExpr() const { +Expr AntlrParser::getTrueExpr() const { return d_expr_manager->mkExpr(TRUE); } -Node AntlrParser::getFalseExpr() const { +Expr AntlrParser::getFalseExpr() const { return d_expr_manager->mkExpr(FALSE); } -Node AntlrParser::newExpression(Kind kind, const Node& child) { +Expr AntlrParser::newExpression(Kind kind, const Expr& child) { return d_expr_manager->mkExpr(kind, child); } -Node AntlrParser::newExpression(Kind kind, const Node& child_1, const Node& child_2) { +Expr AntlrParser::newExpression(Kind kind, const Expr& child_1, const Expr& child_2) { return d_expr_manager->mkExpr(kind, child_1, child_2); } -Node AntlrParser::newExpression(Kind kind, const std::vector<Node>& children) { +Expr AntlrParser::newExpression(Kind kind, const std::vector<Expr>& children) { return d_expr_manager->mkExpr(kind, children); } @@ -112,7 +112,7 @@ void AntlrParser::setBenchmarkStatus(BenchmarkStatus status) { void AntlrParser::addExtraSorts(const std::vector<std::string>& extra_sorts) { } -void AntlrParser::setExpressionManager(NodeManager* em) { +void AntlrParser::setExpressionManager(ExprManager* em) { d_expr_manager = em; } @@ -132,7 +132,7 @@ void AntlrParser::rethrow(antlr::SemanticException& e, string new_message) LT(0).get()->getColumn()); } -Node AntlrParser::createPrecedenceExpr(const vector<Node>& exprs, const vector< +Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs, const vector< Kind>& kinds) { return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1); } @@ -154,7 +154,7 @@ unsigned AntlrParser::findPivot(const std::vector<Kind>& kinds, return pivot; } -Node AntlrParser::createPrecedenceExpr(const std::vector<Node>& exprs, +Expr AntlrParser::createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index) { if(start_index == end_index) @@ -162,8 +162,8 @@ Node AntlrParser::createPrecedenceExpr(const std::vector<Node>& exprs, unsigned pivot = findPivot(kinds, start_index, end_index - 1); - Node child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot); - Node child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index); + Expr child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot); + Expr 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 26f206e43..ad23d45f8 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/node.h" -#include "expr/node_manager.h" +#include "expr/expr.h" +#include "expr/expr_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(NodeManager* expr_manager); + void setExpressionManager(ExprManager* expr_manager); protected: @@ -89,7 +89,7 @@ protected: * @param var_name the name of the variable * @return the variable expression */ - Node getVariable(std::string var_name); + Expr getVariable(std::string var_name); /** * Types of symbols. @@ -113,40 +113,40 @@ protected: * Returns the true expression. * @return the true expression */ - Node getTrueExpr() const; + Expr getTrueExpr() const; /** * Returns the false expression. * @return the false expression */ - Node getFalseExpr() const; + Expr getFalseExpr() const; /** * Creates a new unary CVC4 expression using the expression manager. * @param kind the kind of the expression * @param child the child */ - Node newExpression(Kind kind, const Node& child); + Expr newExpression(Kind kind, const Expr& 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 */ - Node newExpression(Kind kind, const Node& child_1, const Node& child_2); + Expr newExpression(Kind kind, const Expr& child_1, const Expr& 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 */ - Node newExpression(Kind kind, const std::vector<Node>& children); + Expr newExpression(Kind kind, const std::vector<Expr>& 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. */ - Node createPrecedenceExpr(const std::vector<Node>& exprs, const std::vector<Kind>& kinds); + Expr createPrecedenceExpr(const std::vector<Expr>& 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. */ - Node createPrecedenceExpr(const std::vector<Node>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index); + Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index); /** The status of the benchmark */ BenchmarkStatus d_benchmark_status; /** The expression manager */ - NodeManager* d_expr_manager; + ExprManager* d_expr_manager; /** The symbol table lookup */ - SymbolTable<Node> d_var_symbol_table; + SymbolTable<Expr> 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 2bb01007a..adeb5761d 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; } -Node CvcParser::parseNextExpression() throw(ParserException) { - Node result; +Expr CvcParser::parseNextExpression() throw(ParserException) { + Expr result; if(!done()) { try { result = d_antlr_parser->formula(); @@ -62,7 +62,7 @@ CvcParser::~CvcParser() { delete d_antlr_lexer; } -CvcParser::CvcParser(NodeManager*em, istream& input, const char* file_name) : +CvcParser::CvcParser(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/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 812925b0b..625f2c381 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] { - Node f; + Expr f; vector<string> ids; } : ASSERT f = formula { cmd = new AssertCommand(f); } @@ -60,15 +60,15 @@ type : BOOLEAN ; -formula returns [CVC4::Node formula] +formula returns [CVC4::Expr formula] : formula = bool_formula ; -bool_formula returns [CVC4::Node formula] +bool_formula returns [CVC4::Expr formula] { - vector<Node> formulas; + vector<Expr> formulas; vector<Kind> kinds; - Node f1, f2; + Expr f1, f2; Kind k; } : f1 = primary_bool_formula { formulas.push_back(f1); } @@ -79,7 +79,7 @@ bool_formula returns [CVC4::Node formula] } ; -primary_bool_formula returns [CVC4::Node formula] +primary_bool_formula returns [CVC4::Expr 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::Node atom] +bool_atom returns [CVC4::Expr atom] { string p; } diff --git a/src/parser/cvc/cvc_parser.h b/src/parser/cvc/cvc_parser.h index 07699916f..9cb6b7594 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(NodeManager* em, std::istream& input, const char* file_name = ""); + CvcParser(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: diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index c6d5bcb5c..8d4af5ba1 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -28,7 +28,7 @@ using namespace std; namespace CVC4 { namespace parser { -Parser::Parser(NodeManager* em) : +Parser::Parser(ExprManager* em) : d_expr_manager(em), d_done(false) { } diff --git a/src/parser/parser.h b/src/parser/parser.h index 7f63261c7..7755d65f0 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -22,9 +22,9 @@ namespace CVC4 { // Forward declarations -class Node; +class Expr; class Command; -class NodeManager; +class ExprManager; namespace parser { @@ -44,7 +44,7 @@ public: * Construct the parser that uses the given expression manager. * @param em the expression manager. */ - Parser(NodeManager* em); + Parser(ExprManager* em); /** * Destructor. @@ -60,7 +60,7 @@ public: /** * Parse the next expression of the stream */ - virtual Node parseNextExpression() throw (ParserException) = 0; + virtual Expr 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 */ - NodeManager* d_expr_manager; + ExprManager* 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 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: |