reverting some changes to parser from last commit

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 09e65526d3ca2541132bb0d2d7c5fc103f3d9220..90e13022cbf0ad2648ce23b14eb29d56462855b2 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -326,6 +326,29 @@ Command* Parser::nextCommand() throw(ParserException) {
   return cmd;
 }
 
+Expr Parser::nextExpression() throw(ParserException) {
+  Debug("parser") << "nextExpression()" << std::endl;
+  Expr result;
+  if(!done()) {
+    try {
+      result = d_input->parseExpr();
+      if(result.isNull()) {
+        setDone();
+      }
+    } catch(ParserException& e) {
+      setDone();
+      throw;
+    } catch(Exception& e) {
+      setDone();
+      stringstream ss;
+      ss << e;
+      parseError( ss.str() );
+    }
+  }
+  Debug("parser") << "nextExpression() => " << result << std::endl;
+  return result;
+}
+
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */

diff --git a/src/parser/parser.h b/src/parser/parser.h
index bc01420895a5d70962addc6befe95bb8941c2698..4d1e6417637a9331bcca6b163ee94e546e6bbd20 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -350,6 +350,7 @@ public:
   bool isPredicate(const std::string& name);
 
   Command* nextCommand() throw(ParserException);
+  Expr nextExpression() throw(ParserException);
 
   inline void parseError(const std::string& msg) throw (ParserException) {
     d_input->parseError(msg);

diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 4f55edad57a1fe11787ad5a5472220e89e3de0d0..288c3b1d5715972585efb5e9e7b2ccab30e781df 100644 (file)
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -14,7 +14,7 @@
  ** \brief Black box testing of CVC4::parser::Parser, including CVC, SMT and
  ** SMT v2 inputs.
  **
- ** Black box testing of CVC4::parser::Parser, including CVC, SMT and
+ ** Black box testing of CVC4::parser::Parser, including CVC, SMT, and
  ** SMT v2 inputs.
  **/
 
@@ -139,17 +139,19 @@ protected:
       }
   }
 
-  /* NOTE: The check implemented here may fail if a bad expression expression string
-   * has a prefix that is parseable as a good expression. E.g., the bad SMT v2 expression
-   * "#b10@@@@@@" will actually return the bit-vector 10 and ignore the tail of the
-   * input. It's more trouble than it's worth to check that the whole input was
-   * consumed here, so just be careful to avoid valid prefixes in tests.
+  /* NOTE: The check implemented here may fail if a bad expression
+   * expression string has a prefix that is parseable as a good
+   * expression. E.g., the bad SMT v2 expression "#b10@@@@@@" will
+   * actually return the bit-vector 10 and ignore the tail of the
+   * input. It's more trouble than it's worth to check that the whole
+   * input was consumed here, so just be careful to avoid valid
+   * prefixes in tests.
    */
   void tryBadExpr(const string badExpr, bool strictMode = false) {
 //    Debug.on("parser");
 //    Debug.on("parser-extra");
 //      cout << "Testing bad expr: '" << badExpr << "'\n";
-      
+
       Parser *parser =
         ParserBuilder(*d_exprManager,"test")
           .withStringInput(badExpr)
@@ -174,7 +176,6 @@ protected:
   }
 
   void setUp() {
-cout << "SET UP\n";
     d_exprManager = new ExprManager;
   }
 

diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index c661f00d90186c764c8ede34ed6d9e9d17376189..407021b50482d2463dd7120d8add94f812304b2d 100644 (file)
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -97,7 +97,7 @@ public:
                     );
 
     remove(filename);
-    //    mkfifo(ptr, S_IWUSR | s_IRUSR);    
+    //    mkfifo(ptr, S_IWUSR | s_IRUSR);
   }
 
   void testSimpleFileInput() {