From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 9 Oct 2010 10:10:47 +0000 (+0000)
Subject: reverting some changes to parser from last commit
X-Git-Tag: cvc5-1.0.0~8813
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7a059452ebf5729723f610da9258a47007e38253;p=cvc5.git

reverting some changes to parser from last commit
---

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 09e65526d..90e13022c 100644
--- 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 bc0142089..4d1e64176 100644
--- 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 4f55edad5..288c3b1d5 100644
--- 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 c661f00d9..407021b50 100644
--- 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() {