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

3 files changed, 12 insertions, 12 deletions

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: