From ade732181ad2eabfb3a6eef46bdc9ea42d27246e Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Sun, 24 Oct 2010 16:37:00 +0000
Subject: Adding unit test for InteractiveShell

---
 test/unit/Makefile.am                    |  10 ++-
 test/unit/main/interactive_shell_black.h | 115 +++++++++++++++++++++++++++++++
 2 files changed, 122 insertions(+), 3 deletions(-)
 create mode 100644 test/unit/main/interactive_shell_black.h

(limited to 'test')

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index af9e447ed..d511e48e7 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -39,7 +39,8 @@ UNIT_TESTS = \
 	util/integer_white \
 	util/rational_black \
 	util/rational_white \
-	util/stats_black
+	util/stats_black \
+	main/interactive_shell_black
 
 export VERBOSE = 1
 
@@ -74,11 +75,14 @@ AM_LDFLAGS_BLACK =
 AM_LDFLAGS_PUBLIC =
 AM_LIBADD_WHITE = \
 	@abs_top_builddir@/src/parser/libcvc4parser_noinst.la \
-	@abs_top_builddir@/src/libcvc4_noinst.la
+	@abs_top_builddir@/src/libcvc4_noinst.la \
+	@abs_top_builddir@/src/main/libmain.a
 AM_LIBADD_BLACK = \
 	@abs_top_builddir@/src/parser/libcvc4parser_noinst.la \
-	@abs_top_builddir@/src/libcvc4_noinst.la
+	@abs_top_builddir@/src/libcvc4_noinst.la \
+	@abs_top_builddir@/src/main/libmain.a
 AM_LIBADD_PUBLIC = \
+	@abs_top_builddir@/src/parser/libcvc4parser.la \
 	@abs_top_builddir@/src/libcvc4.la
 
 EXTRA_DIST = \
diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
new file mode 100644
index 000000000..e56e8de8a
--- /dev/null
+++ b/test/unit/main/interactive_shell_black.h
@@ -0,0 +1,115 @@
+/*********************                                                        */
+/*! \file interactive_shell_black.h
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: 
+ ** Minor contributors (to current version): 
+ ** 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.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::InteractiveShell.
+ **
+ ** Black box testing of CVC4::InteractiveShell.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+//Used in some of the tests
+#include <vector>
+#include <sstream>
+
+#include "expr/expr_manager.h"
+#include "main/interactive_shell.h"
+#include "parser/parser_builder.h"
+#include "util/language.h"
+#include "util/options.h"
+
+using namespace CVC4;
+using namespace std;
+
+class InteractiveShellBlack : public CxxTest::TestSuite {
+private:
+  ExprManager* d_exprManager;
+  Options d_options;
+  stringstream* d_sin;
+  stringstream* d_sout;
+
+  /** Read up to maxCommands+1 from the shell and throw an assertion
+      error if it's fewer than minCommands and more than maxCommands.
+      Note that an empty string followed by EOF may be returned as an
+      empty command, and not NULL (subsequent calls to readCommand()
+      should return NULL). E.g., "CHECKSAT;\n" may return two
+      commands: the CHECKSAT, followed by an empty command, followed
+      by NULL. */
+  void countCommands(InteractiveShell& shell, 
+                     int minCommands, 
+                     int maxCommands) {
+    int n = 0;
+    while( n <= maxCommands && shell.readCommand() != NULL ) { ++n; }
+    TS_ASSERT( n <= maxCommands );
+    TS_ASSERT( n >= minCommands );
+  }
+
+ public:
+  void setUp() {
+    d_exprManager = new ExprManager;
+    d_sin = new stringstream;
+    d_sout = new stringstream;
+    d_options.in = d_sin;
+    d_options.out = d_sout;
+    d_options.inputLanguage = language::input::LANG_CVC4;
+  }
+
+  void tearDown() {
+    delete d_exprManager;
+    delete d_sin;
+    delete d_sout;
+  }
+
+  void testAssertTrue() {
+    *d_sin << "ASSERT TRUE;" << flush;
+    InteractiveShell shell(*d_exprManager, d_options);
+    countCommands( shell, 1, 1 );
+  }
+
+  void testQueryFalse() {
+    *d_sin << "QUERY FALSE;" << flush;
+    InteractiveShell shell(*d_exprManager, d_options);
+    countCommands( shell, 1, 1 );
+  }
+
+  void testDefUse() {
+    InteractiveShell shell(*d_exprManager, d_options);
+    *d_sin << "x : REAL; ASSERT x > 0;\n" << flush;
+    /* readCommand may return a sequence, so we can't say for sure
+       whether it will return 1 or 2... */
+    countCommands( shell, 1, 2 );
+  }
+
+  void testDefUse2() {
+    InteractiveShell shell(*d_exprManager, d_options);
+    /* readCommand may return a sequence, see above. */
+    *d_sin << "x : REAL;\n" << flush;
+    shell.readCommand();
+    *d_sin << "ASSERT x > 0;\n" << flush;
+    countCommands( shell, 1, 1 );
+  }
+
+  void testEmptyLine() {
+    InteractiveShell shell(*d_exprManager, d_options);
+    *d_sin << flush;
+    countCommands(shell,0,0);
+  }
+
+  void testRepeatedEmptyLines() {
+    *d_sin << "\n\n\n";
+    InteractiveShell shell(*d_exprManager, d_options);
+    /* Might return up to four empties, might return nothing */
+    countCommands( shell, 0, 3 );
+  }
+
+};
-- 
cgit v1.2.3