1 files changed, 39 insertions, 38 deletions

diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
index cf68b5465..44b3660c9 100644
--- a/test/unit/main/interactive_shell_black.h
+++ b/test/unit/main/interactive_shell_black.h
@@ -2,7 +2,7 @@
 /*! \file interactive_shell_black.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Morgan Deters, Tim King
+ **   Christopher L. Conway, Aina Niemetz, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -20,6 +20,7 @@
 #include <vector>
 #include <sstream>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr_manager.h"
 #include "main/interactive_shell.h"
 #include "options/base_options.h"
@@ -31,64 +32,38 @@
 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) {
-    Command* cmd;
-    int n = 0;
-    while( n <= maxCommands && (cmd = shell.readCommand()) != NULL ) {
-      ++n;
-      delete cmd;
-    }
-    TS_ASSERT( n <= maxCommands );
-    TS_ASSERT( n >= minCommands );
-  }
-
+class InteractiveShellBlack : public CxxTest::TestSuite
+{
  public:
-  void setUp() {
+  void setUp()
+  {
     d_sin = new stringstream;
     d_sout = new stringstream;
     d_options.set(options::in, d_sin);
     d_options.set(options::out, d_sout);
     d_options.set(options::inputLanguage, language::input::LANG_CVC4);
-    d_exprManager = new ExprManager(d_options);
+    d_solver.reset(new api::Solver(&d_options));
   }
 
   void tearDown() {
-    delete d_exprManager;
     delete d_sin;
     delete d_sout;
   }
 
   void testAssertTrue() {
     *d_sin << "ASSERT TRUE;\n" << flush;
-    InteractiveShell shell(*d_exprManager);
+    InteractiveShell shell(d_solver.get());
     countCommands( shell, 1, 1 );
   }
 
   void testQueryFalse() {
     *d_sin << "QUERY FALSE;\n" << flush;
-    InteractiveShell shell(*d_exprManager);
+    InteractiveShell shell(d_solver.get());
     countCommands( shell, 1, 1 );
   }
 
   void testDefUse() {
-    InteractiveShell shell(*d_exprManager);
+    InteractiveShell shell(d_solver.get());
     *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... */
@@ -96,7 +71,7 @@ private:
   }
 
   void testDefUse2() {
-    InteractiveShell shell(*d_exprManager);
+    InteractiveShell shell(d_solver.get());
     /* readCommand may return a sequence, see above. */
     *d_sin << "x : REAL;\n" << flush;
     Command* tmp = shell.readCommand();
@@ -106,16 +81,42 @@ private:
   }
 
   void testEmptyLine() {
-    InteractiveShell shell(*d_exprManager);
+    InteractiveShell shell(d_solver.get());
     *d_sin << flush;
     countCommands(shell,0,0);
   }
 
   void testRepeatedEmptyLines() {
     *d_sin << "\n\n\n";
-    InteractiveShell shell(*d_exprManager);
+    InteractiveShell shell(d_solver.get());
     /* Might return up to four empties, might return nothing */
     countCommands( shell, 0, 3 );
   }
 
+ private:
+  std::unique_ptr<api::Solver> d_solver;
+  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)
+  {
+    Command* cmd;
+    int n = 0;
+    while (n <= maxCommands && (cmd = shell.readCommand()) != NULL)
+    {
+      ++n;
+      delete cmd;
+    }
+    TS_ASSERT(n <= maxCommands);
+    TS_ASSERT(n >= minCommands);
+  }
 };