Implementing input from stdin (Fixes: #144)

3 files changed, 171 insertions, 17 deletions

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 1f283f476..0597de931 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -12,6 +12,7 @@ UNIT_TESTS = \
 	expr/attribute_black \
 	expr/declaration_scope_black \
 	parser/parser_black \
+	parser/parser_builder_black \
 	prop/cnf_stream_black \
 	context/context_black \
 	context/context_white \
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 6f09820c5..f6d822265 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/** parser_white.h
+/** parser_black.h
  ** Original author: cconway
  ** Major contributors: none
  ** Minor contributors (to current version): dejan, mdeters
@@ -10,17 +10,18 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** White box testing of CVC4::parser::SmtParser.
+ ** Black box testing of CVC4::parser::Parser, including CVC, SMT and
+ ** SMT v2 inputs.
  **/
 
 #include <cxxtest/TestSuite.h>
-//#include <string>
 #include <sstream>
 
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
+#include "parser/parser_options.h"
 #include "parser/smt2/smt2.h"
 #include "expr/command.h"
 #include "util/output.h"
@@ -29,8 +30,6 @@ using namespace CVC4;
 using namespace CVC4::parser;
 using namespace std;
 
-
-
 class ParserBlack {
   InputLanguage d_lang;
   ExprManager *d_exprManager;
@@ -62,10 +61,10 @@ protected:
 //         Debug.on("parser-extra");
 //        cerr << "Testing good input: <<" << goodInput << ">>" << endl;
 //        istringstream stream(goodInputs[i]);
-        ParserBuilder parserBuilder(d_lang,"test");
         Parser *parser =
-          parserBuilder.withStringInput(goodInput)
-            .withExprManager(*d_exprManager)
+          ParserBuilder(*d_exprManager,"test")
+            .withStringInput(goodInput)
+            .withInputLanguage(d_lang)
             .build();
         TS_ASSERT( !parser->done() );
         Command* cmd;
@@ -88,10 +87,11 @@ protected:
   void tryBadInput(const string badInput, bool strictMode = false) {
 //      cerr << "Testing bad input: '" << badInput << "'\n";
 //      Debug.on("parser");
-    ParserBuilder parserBuilder(d_lang,"test");
+
     Parser *parser =
-      parserBuilder.withStringInput(badInput)
-        .withExprManager(*d_exprManager)
+      ParserBuilder(*d_exprManager,"test")
+        .withStringInput(badInput)
+        .withInputLanguage(d_lang)
         .withStrictMode(strictMode)
         .build();
       TS_ASSERT_THROWS
@@ -109,11 +109,13 @@ protected:
 //        cerr << "Testing good expr: '" << goodExpr << "'\n";
         // Debug.on("parser");
 //        istringstream stream(context + goodBooleanExprs[i]);
-        ParserBuilder parserBuilder(d_lang,"test");
+
         Parser *parser =
-          parserBuilder.withStringInput(goodExpr)
-            .withExprManager(*d_exprManager)
+          ParserBuilder(*d_exprManager,"test")
+            .withStringInput(goodExpr)
+            .withInputLanguage(d_lang)
             .build();
+
         TS_ASSERT( !parser->done() );
         setupContext(*parser);
         TS_ASSERT( !parser->done() );
@@ -142,10 +144,11 @@ protected:
 //    Debug.on("parser");
 //    Debug.on("parser-extra");
 //      cout << "Testing bad expr: '" << badExpr << "'\n";
-      ParserBuilder parserBuilder(d_lang,"test");
+      
       Parser *parser =
-        parserBuilder.withStringInput(badExpr)
-          .withExprManager(*d_exprManager)
+        ParserBuilder(*d_exprManager,"test")
+          .withStringInput(badExpr)
+          .withInputLanguage(d_lang)
           .withStrictMode(strictMode)
           .build();
       setupContext(*parser);
diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
new file mode 100644
index 000000000..f254580af
--- /dev/null
+++ b/test/unit/parser/parser_builder_black.h
@@ -0,0 +1,150 @@
+/*********************                                                        */
+/** parser_builder_black.h
+ ** Original author: cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan, mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Black box testing of CVC4::parser::ParserBuilder.
+ **/
+
+#include <cxxtest/TestSuite.h>
+#include <ext/stdio_filebuf.h>
+#include <fstream>
+#include <iostream>
+#include <stdio.h>
+#include <string.h>
+#include <sys/stat.h>
+#include <unistd.h>
+
+#include "expr/command.h"
+#include "parser/parser.h"
+#include "parser/parser_builder.h"
+#include "parser/parser_options.h"
+
+typedef __gnu_cxx::stdio_filebuf<char> filebuf_gnu;
+
+using namespace CVC4;
+using namespace CVC4::parser;
+using namespace std;
+
+class ParserBuilderBlack : public CxxTest::TestSuite {
+
+  ExprManager *d_exprManager;
+
+  void checkEmptyInput(ParserBuilder& builder) {
+    Parser *parser = builder.build();
+    TS_ASSERT( parser != NULL );
+
+    Expr e = parser->nextExpression();
+    TS_ASSERT( e.isNull() );
+
+    delete parser;
+  }
+
+  void checkTrueInput(ParserBuilder& builder) {
+    Parser *parser = builder.build();
+    TS_ASSERT( parser != NULL );
+
+    Expr e = parser->nextExpression();
+    TS_ASSERT_EQUALS( e, d_exprManager->mkConst(true) );
+
+    e = parser->nextExpression();
+    TS_ASSERT( e.isNull() );
+    delete parser;
+  }
+
+  char* mkTemp() {
+    char *filename = strdup("/tmp/testinput.XXXXXX");
+    int fd = mkstemp(filename);
+    TS_ASSERT( fd != -1 );
+    close(fd);
+    return filename;
+  }
+
+public:
+
+  void setUp() {
+    d_exprManager = new ExprManager;
+  }
+
+  void tearDown() {
+    delete d_exprManager;
+  }
+
+  void testEmptyFileInput() {
+    char *filename = mkTemp();
+
+    /* FILE *fp = tmpfile(); */
+    /* filebuf_gnu fs( fd, ios_base::out ); */
+
+    /* ptr = tmpnam(filename); */
+    /* std::fstream fs( ptr, fstream::out ); */
+    /* fs.close(); */
+
+    checkEmptyInput(
+      ParserBuilder(*d_exprManager,filename)
+        .withInputLanguage(LANG_CVC4)
+                    );
+
+    remove(filename);
+    //    mkfifo(ptr, S_IWUSR | s_IRUSR);    
+  }
+
+  void testSimpleFileInput() {
+    char *filename = mkTemp();
+
+    std::fstream fs( filename, fstream::out );
+    fs << "TRUE" << std::endl;
+    fs.close();
+
+    checkTrueInput(
+      ParserBuilder(*d_exprManager,filename)
+        .withInputLanguage(LANG_CVC4)
+                   );
+
+    remove(filename);
+  }
+
+  void testEmptyStringInput() {
+    checkEmptyInput(
+      ParserBuilder(*d_exprManager,"foo")
+        .withInputLanguage(LANG_CVC4)
+        .withStringInput("")
+                    );
+  }
+
+  void testTrueStringInput() {
+    checkTrueInput(
+      ParserBuilder(*d_exprManager,"foo")
+        .withInputLanguage(LANG_CVC4)
+        .withStringInput("TRUE")
+                   );
+  }
+
+  void testEmptyStreamInput() {
+    stringstream ss( "", ios_base::in );
+    checkEmptyInput(
+      ParserBuilder(*d_exprManager,"foo")
+        .withInputLanguage(LANG_CVC4)
+        .withStreamInput(ss)
+                    );
+  }
+
+  void testTrueStreamInput() {
+    stringstream ss( "TRUE", ios_base::in );
+    checkTrueInput(
+      ParserBuilder(*d_exprManager,"foo")
+        .withInputLanguage(LANG_CVC4)
+        .withStreamInput(ss)
+                   );
+  }
+
+
+
+}; // class ParserBuilderBlack