CvcParserBlack and supporting Makefile changes

3 files changed, 54 insertions, 16 deletions

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index f5ba6f410..cf78d8e34 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -6,13 +6,8 @@ AM_CXXFLAGS_WHITE = -fno-access-control
 AM_CXXFLAGS_BLACK =
 AM_CXXFLAGS_PUBLIC =
 AM_LDFLAGS_WHITE = \
-		@abs_top_builddir@/src/context/libcontext.la \
-		@abs_top_builddir@/src/expr/libexpr.la \
-		@abs_top_builddir@/src/smt/libsmt.la \
-		@abs_top_builddir@/src/theory/libtheory.la \
-		@abs_top_builddir@/src/util/libutil.la \
-		@abs_top_builddir@/src/prop/libprop.la \
-		@abs_top_builddir@/src/prop/minisat/libminisat.la
+	    @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \ 
+	    @abs_top_builddir@/src/libcvc4_noinst.la
 AM_LDFLAGS_BLACK = \
 		$(AM_LDFLAGS_WHITE)
 AM_LDFLAGS_PUBLIC = \
@@ -20,7 +15,8 @@ AM_LDFLAGS_PUBLIC = \
 
 TESTS = \
 	expr/node_white \
-	expr/node_black
+	expr/node_black \
+	parser/cvc/cvc_parser_black
 
 # without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-(
 noinst_LTLIBRARIES = libdummy.la
diff --git a/test/unit/Makefile.in b/test/unit/Makefile.in
index 23153db83..f20905330 100644
--- a/test/unit/Makefile.in
+++ b/test/unit/Makefile.in
@@ -220,13 +220,8 @@ top_srcdir = @top_srcdir@
 @HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS_BLACK = 
 @HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS_PUBLIC = 
 @HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS_WHITE = \
-@HAVE_CXXTESTGEN_TRUE@		@abs_top_builddir@/src/context/libcontext.la \
-@HAVE_CXXTESTGEN_TRUE@		@abs_top_builddir@/src/expr/libexpr.la \
-@HAVE_CXXTESTGEN_TRUE@		@abs_top_builddir@/src/smt/libsmt.la \
-@HAVE_CXXTESTGEN_TRUE@		@abs_top_builddir@/src/theory/libtheory.la \
-@HAVE_CXXTESTGEN_TRUE@		@abs_top_builddir@/src/util/libutil.la \
-@HAVE_CXXTESTGEN_TRUE@		@abs_top_builddir@/src/prop/libprop.la \
-@HAVE_CXXTESTGEN_TRUE@		@abs_top_builddir@/src/prop/minisat/libminisat.la
+@HAVE_CXXTESTGEN_TRUE@	    @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \
+@HAVE_CXXTESTGEN_TRUE@	    @abs_top_builddir@/src/libcvc4_noinst.la
 
 @HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS_BLACK = \
 @HAVE_CXXTESTGEN_TRUE@		$(AM_LDFLAGS_WHITE)
@@ -239,7 +234,8 @@ top_srcdir = @top_srcdir@
 @HAVE_CXXTESTGEN_FALSE@TESTS = no_cxxtest
 @HAVE_CXXTESTGEN_TRUE@TESTS = \
 @HAVE_CXXTESTGEN_TRUE@	expr/node_white \
-@HAVE_CXXTESTGEN_TRUE@	expr/node_black
+@HAVE_CXXTESTGEN_TRUE@	expr/node_black \
+@HAVE_CXXTESTGEN_TRUE@	parser/cvc/cvc_parser_black
 
 
 # without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-(
diff --git a/test/unit/parser/cvc/cvc_parser_black.h b/test/unit/parser/cvc/cvc_parser_black.h
new file mode 100644
index 000000000..b34185e01
--- /dev/null
+++ b/test/unit/parser/cvc/cvc_parser_black.h
@@ -0,0 +1,46 @@
+/* Black box testing of CVC4::Node. */
+
+#include <cxxtest/TestSuite.h>
+//#include <string>
+#include <sstream>
+
+#include "expr/expr_manager.h"
+#include "parser/cvc/cvc_parser.h"
+
+using namespace CVC4;
+using namespace CVC4::parser;
+using namespace std;
+
+const string d_goodInputs[] = {
+      "ASSERT TRUE;",
+      "QUERY TRUE;",
+      "CHECKSAT FALSE;",
+      "a, b : BOOLEAN;",
+      "x, y : INT;",
+      "a, b : BOOLEAN; QUERY (a => b) AND a => b;"
+  };
+
+class CvcParserBlack : public CxxTest::TestSuite {
+private:
+
+  ExprManager *d_exprManager;
+
+
+public:
+  void setUp() {
+//    cout << "In setUp()\n";
+    d_exprManager = new ExprManager();
+//    cout << "Leaving setUp()\n";
+  }
+
+  void testGoodInputs() {
+//    cout << "In testGoodInputs()\n";
+    for( int i=0; i < sizeof(d_goodInputs); ++i ) {
+      istringstream stream(d_goodInputs[i]);
+      CvcParser cvcParser(d_exprManager,stream);
+      TS_ASSERT( !cvcParser.done() );
+      while( !cvcParser.done() ) {
+        TS_ASSERT( cvcParser.parseNextCommand() );
+      }
+  }
+};