killing expr into node...

3 files changed, 12 insertions, 12 deletions

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: