Extracted the public Expr and ExprManager interface to encapsulate the optimized expressions and the internal expression manager.

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: