summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/antlr_parser.cpp24
-rw-r--r--src/parser/antlr_parser.h26
-rw-r--r--src/parser/cvc/cvc_parser.cpp6
-rw-r--r--src/parser/cvc/cvc_parser.g14
-rw-r--r--src/parser/cvc/cvc_parser.h4
-rw-r--r--src/parser/parser.cpp2
-rw-r--r--src/parser/parser.h10
-rw-r--r--src/parser/smt/smt_parser.cpp6
-rw-r--r--src/parser/smt/smt_parser.g18
-rw-r--r--src/parser/smt/smt_parser.h4
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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback