[Unit Tests] Fix shell test for Editline (#7117)

When using --editline, our interactive_shell_black unit test was not
working because the unit test was redirecting std::cin and std::cout
to std::stringstreams, which does not work with Editline. This commit
refactors our InteractiveShell class to explicitly take the input and
output streams as arguments, which fixes the issue because we do not use
Editline for input streams that are not std::cin. Additionally, the
commit updates the unit test to use SMT-LIB syntax instead of the
deprecated CVC language.

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 28b786437d22722a2960db10628d4f798a4b1ca5..ec3e10b5e754ed9aaa395352d0b82049393c5eb8 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -194,7 +194,9 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
         pExecutor->doCommand(cmd);
       }
       InteractiveShell shell(pExecutor->getSolver(),
-                             pExecutor->getSymbolManager());
+                             pExecutor->getSymbolManager(),
+                             dopts.in(),
+                             dopts.out());
 
       CVC5Message() << Configuration::getPackageName() << " "
                     << Configuration::getVersionString();

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index ea408012a627a5b4066ab81e212373d5de0602f4..86f3449792e86ceb5623b4b5cd5630c6c634ddb2 100644 (file)
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -85,11 +85,11 @@ static set<string> s_declarations;
 
 #endif /* HAVE_LIBEDITLINE */
 
-InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
-    : d_solver(solver),
-      d_in(solver->getDriverOptions().in()),
-      d_out(solver->getDriverOptions().out()),
-      d_quit(false)
+InteractiveShell::InteractiveShell(api::Solver* solver,
+                                   SymbolManager* sm,
+                                   std::istream& in,
+                                   std::ostream& out)
+    : d_solver(solver), d_in(in), d_out(out), d_quit(false)
 {
   ParserBuilder parserBuilder(solver, sm, true);
   /* Create parser with bogus input. */

diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index bf05a1ec7c920d6d239c2b42e5ecaa1486cf19ab..6029d6b0e2652011835b5760280804535a548876 100644 (file)
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -35,6 +35,29 @@ class SymbolManager;
 
 class InteractiveShell
 {
+ public:
+  InteractiveShell(api::Solver* solver,
+                   SymbolManager* sm,
+                   std::istream& in,
+                   std::ostream& out);
+
+  /**
+   * Close out the interactive session.
+   */
+  ~InteractiveShell();
+
+  /**
+   * Read a command from the interactive shell. This will read as
+   * many lines as necessary to parse a well-formed command.
+   */
+  Command* readCommand();
+
+  /**
+   * Return the internal parser being used.
+   */
+  parser::Parser* getParser() { return d_parser; }
+
+ private:
   api::Solver* d_solver;
   std::istream& d_in;
   std::ostream& d_out;
@@ -46,26 +69,6 @@ class InteractiveShell
 
   static const std::string INPUT_FILENAME;
   static const unsigned s_historyLimit = 500;
-
-public:
- InteractiveShell(api::Solver* solver, SymbolManager* sm);
-
- /**
-  * Close out the interactive session.
-  */
- ~InteractiveShell();
-
- /**
-  * Read a command from the interactive shell. This will read as
-  * many lines as necessary to parse a well-formed command.
-  */
- Command* readCommand();
-
- /**
-  * Return the internal parser being used.
-  */
- parser::Parser* getParser() { return d_parser; }
-
 };/* class InteractiveShell */
 
 }  // namespace cvc5

diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp
index 7b5f39f48bf34f2437127108f45bc8af12d17086..2170c490f69a462ac8a5a331413b32dccb70020c 100644 (file)
--- a/test/unit/main/interactive_shell_black.cpp
+++ b/test/unit/main/interactive_shell_black.cpp
@@ -37,23 +37,16 @@ class TestMainBlackInteractiveShell : public TestInternal
     TestInternal::SetUp();
 
     d_sin = std::make_unique<std::stringstream>();
-    d_stdin = std::cin.rdbuf();
-    std::cin.rdbuf(d_sin->rdbuf());
-
     d_sout = std::make_unique<std::stringstream>();
-    d_stdout = std::cout.rdbuf();
-    std::cout.rdbuf(d_sout->rdbuf());
 
     d_solver.reset(new cvc5::api::Solver());
-    d_solver->setOption("input-language", "cvc");
+    d_solver->setOption("input-language", "smt2");
     d_symman.reset(new SymbolManager(d_solver.get()));
   }
 
   void TearDown() override
   {
-    std::cin.rdbuf(d_stdin);
     d_sin.reset(nullptr);
-    std::cout.rdbuf(d_stdout);
     d_sout.reset(nullptr);
     // ensure that symbol manager is destroyed before solver
     d_symman.reset(nullptr);
@@ -87,29 +80,26 @@ class TestMainBlackInteractiveShell : public TestInternal
   std::unique_ptr<std::stringstream> d_sout;
   std::unique_ptr<SymbolManager> d_symman;
   std::unique_ptr<cvc5::api::Solver> d_solver;
-
-  std::streambuf* d_stdin;
-  std::streambuf* d_stdout;
 };
 
 TEST_F(TestMainBlackInteractiveShell, assert_true)
 {
-  *d_sin << "ASSERT TRUE;\n" << std::flush;
-  InteractiveShell shell(d_solver.get(), d_symman.get());
+  *d_sin << "(assert true)\n" << std::flush;
+  InteractiveShell shell(d_solver.get(), d_symman.get(), *d_sin, *d_sout);
   countCommands(shell, 1, 1);
 }
 
 TEST_F(TestMainBlackInteractiveShell, query_false)
 {
-  *d_sin << "QUERY FALSE;\n" << std::flush;
-  InteractiveShell shell(d_solver.get(), d_symman.get());
+  *d_sin << "(check-sat)\n" << std::flush;
+  InteractiveShell shell(d_solver.get(), d_symman.get(), *d_sin, *d_sout);
   countCommands(shell, 1, 1);
 }
 
 TEST_F(TestMainBlackInteractiveShell, def_use1)
 {
-  InteractiveShell shell(d_solver.get(), d_symman.get());
-  *d_sin << "x : REAL; ASSERT x > 0;\n" << std::flush;
+  InteractiveShell shell(d_solver.get(), d_symman.get(), *d_sin, *d_sout);
+  *d_sin << "(declare-const x Real) (assert (> x 0))\n" << std::flush;
   /* readCommand may return a sequence, so we can't say for sure
      whether it will return 1 or 2... */
   countCommands(shell, 1, 2);
@@ -117,18 +107,18 @@ TEST_F(TestMainBlackInteractiveShell, def_use1)
 
 TEST_F(TestMainBlackInteractiveShell, def_use2)
 {
-  InteractiveShell shell(d_solver.get(), d_symman.get());
+  InteractiveShell shell(d_solver.get(), d_symman.get(), *d_sin, *d_sout);
   /* readCommand may return a sequence, see above. */
-  *d_sin << "x : REAL;\n" << std::flush;
+  *d_sin << "(declare-const x Real)\n" << std::flush;
   Command* tmp = shell.readCommand();
-  *d_sin << "ASSERT x > 0;\n" << std::flush;
+  *d_sin << "(assert (> x 0))\n" << std::flush;
   countCommands(shell, 1, 1);
   delete tmp;
 }
 
 TEST_F(TestMainBlackInteractiveShell, empty_line)
 {
-  InteractiveShell shell(d_solver.get(), d_symman.get());
+  InteractiveShell shell(d_solver.get(), d_symman.get(), *d_sin, *d_sout);
   *d_sin << std::flush;
   countCommands(shell, 0, 0);
 }
@@ -136,7 +126,7 @@ TEST_F(TestMainBlackInteractiveShell, empty_line)
 TEST_F(TestMainBlackInteractiveShell, repeated_empty_lines)
 {
   *d_sin << "\n\n\n";
-  InteractiveShell shell(d_solver.get(), d_symman.get());
+  InteractiveShell shell(d_solver.get(), d_symman.get(), *d_sin, *d_sout);
   /* Might return up to four empties, might return nothing */
   countCommands(shell, 0, 3);
 }