Only use libedit on tty inputs (#6946)

This PR improves the check when we use libedit: only when the input is an interactive terminal.
This is motivated by a change to the unit test for the interactive mode that now properly redirects standard input (and output).

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 964b88ea0fcd366e0ad05c65ec09bd120e3587d8..763692d07d1871a834615211d0fb2cef71ce3c27 100644 (file)
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -17,11 +17,13 @@
  */
 #include "main/interactive_shell.h"
 
+#include <cstring>
+#include <unistd.h>
+
 #include <algorithm>
 #include <cstdlib>
 #include <iostream>
 #include <set>
-#include <string.h>
 #include <string>
 #include <utility>
 #include <vector>
@@ -104,7 +106,8 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
   }
 
 #if HAVE_LIBEDITLINE
-  if(&d_in == &cin) {
+  if (&d_in == &std::cin && isatty(fileno(stdin)))
+  {
     ::rl_readline_name = const_cast<char*>("cvc5");
 #if EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP
     ::rl_completion_entry_function = commandGenerator;
@@ -155,7 +158,9 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
                  << ": " << strerror(err) << std::endl;
       }
     }
-  } else {
+  }
+  else
+  {
     d_usingEditline = false;
   }
 #else  /* HAVE_LIBEDITLINE */

diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp
index 9a1a46da4417d3c27ebbc58a196ae9e9f524dcd1..9c842adac9636e75f59cdf3c4f716021f2fb2b9f 100644 (file)
--- a/test/unit/main/interactive_shell_black.cpp
+++ b/test/unit/main/interactive_shell_black.cpp
@@ -35,10 +35,15 @@ class TestMainBlackInteractiveShell : public TestInternal
   void SetUp() override
   {
     TestInternal::SetUp();
-    d_sin.reset(new std::stringstream);
-    d_sout.reset(new std::stringstream);
-    d_options.base.in = d_sin.get();
-    d_options.base.out = d_sout.get();
+
+    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_options.base.inputLanguage = language::input::LANG_CVC;
     d_solver.reset(new cvc5::api::Solver(&d_options));
     d_symman.reset(new SymbolManager(d_solver.get()));
@@ -46,7 +51,9 @@ class TestMainBlackInteractiveShell : public TestInternal
 
   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);
@@ -81,6 +88,9 @@ class TestMainBlackInteractiveShell : public TestInternal
   std::unique_ptr<SymbolManager> d_symman;
   std::unique_ptr<cvc5::api::Solver> d_solver;
   Options d_options;
+
+  std::streambuf* d_stdin;
+  std::streambuf* d_stdout;
 };
 
 TEST_F(TestMainBlackInteractiveShell, assert_true)