From cf79199f0dde04e709acbf355c5be769f8647533 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 2 Sep 2021 13:05:59 -0700 Subject: [PATCH] [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. --- src/main/driver_unified.cpp | 4 +- src/main/interactive_shell.cpp | 10 ++--- src/main/interactive_shell.h | 43 ++++++++++++---------- test/unit/main/interactive_shell_black.cpp | 34 ++++++----------- 4 files changed, 43 insertions(+), 48 deletions(-) diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 28b786437..ec3e10b5e 100644 --- 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& 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 ea408012a..86f344979 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -85,11 +85,11 @@ static set 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 bf05a1ec7..6029d6b0e 100644 --- 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 7b5f39f48..2170c490f 100644 --- 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(); - d_stdin = std::cin.rdbuf(); - std::cin.rdbuf(d_sin->rdbuf()); - d_sout = std::make_unique(); - 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 d_sout; std::unique_ptr d_symman; std::unique_ptr 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); } -- 2.30.2