From: Aina Niemetz Date: Tue, 9 Feb 2021 18:40:06 +0000 (-0800) Subject: google test: main: Migrate interactive_shell_black. (#5878) X-Git-Tag: cvc5-1.0.0~2300 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b05bbf647a72f345329675b34ab0867b134caa1c;p=cvc5.git google test: main: Migrate interactive_shell_black. (#5878) --- diff --git a/test/unit/main/CMakeLists.txt b/test/unit/main/CMakeLists.txt index 59c197f04..55307db95 100644 --- a/test/unit/main/CMakeLists.txt +++ b/test/unit/main/CMakeLists.txt @@ -11,4 +11,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_cxx_unit_test_black(interactive_shell_black main) +cvc4_add_unit_test_black(interactive_shell_black main) diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp new file mode 100644 index 000000000..22b2f05a9 --- /dev/null +++ b/test/unit/main/interactive_shell_black.cpp @@ -0,0 +1,137 @@ +/********************* */ +/*! \file interactive_shell_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Christopher L. Conway, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. 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 +#include + +#include "api/cvc4cpp.h" +#include "expr/expr_manager.h" +#include "expr/symbol_manager.h" +#include "main/interactive_shell.h" +#include "options/base_options.h" +#include "options/language.h" +#include "options/options.h" +#include "parser/parser_builder.h" +#include "smt/command.h" +#include "test.h" + +namespace CVC4 { +namespace test { + +class TestMainBlackInteractiveShell : public TestInternal +{ + protected: + void SetUp() override + { + TestInternal::SetUp(); + d_sin.reset(new std::stringstream); + d_sout.reset(new std::stringstream); + d_options.set(options::in, d_sin.get()); + d_options.set(options::out, d_sout.get()); + d_options.set(options::inputLanguage, language::input::LANG_CVC4); + d_solver.reset(new CVC4::api::Solver(&d_options)); + d_symman.reset(new SymbolManager(d_solver.get())); + } + + void TearDown() override + { + d_sin.reset(nullptr); + d_sout.reset(nullptr); + // ensure that symbol manager is destroyed before solver + d_symman.reset(nullptr); + d_solver.reset(nullptr); + } + + /** + * 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, + uint32_t minCommands, + uint32_t maxCommands) + { + Command* cmd; + uint32_t n = 0; + while (n <= maxCommands && (cmd = shell.readCommand()) != NULL) + { + ++n; + delete cmd; + } + ASSERT_LE(n, maxCommands); + ASSERT_GE(n, minCommands); + } + + std::unique_ptr d_sin; + std::unique_ptr d_sout; + std::unique_ptr d_symman; + std::unique_ptr d_solver; + Options d_options; +}; + +TEST_F(TestMainBlackInteractiveShell, assert_true) +{ + *d_sin << "ASSERT TRUE;\n" << std::flush; + InteractiveShell shell(d_solver.get(), d_symman.get()); + countCommands(shell, 1, 1); +} + +TEST_F(TestMainBlackInteractiveShell, query_false) +{ + *d_sin << "QUERY FALSE;\n" << std::flush; + InteractiveShell shell(d_solver.get(), d_symman.get()); + 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; + /* readCommand may return a sequence, so we can't say for sure + whether it will return 1 or 2... */ + countCommands(shell, 1, 2); +} + +TEST_F(TestMainBlackInteractiveShell, def_use2) +{ + InteractiveShell shell(d_solver.get(), d_symman.get()); + /* readCommand may return a sequence, see above. */ + *d_sin << "x : REAL;\n" << std::flush; + Command* tmp = shell.readCommand(); + *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()); + *d_sin << std::flush; + countCommands(shell, 0, 0); +} + +TEST_F(TestMainBlackInteractiveShell, repeated_empty_lines) +{ + *d_sin << "\n\n\n"; + InteractiveShell shell(d_solver.get(), d_symman.get()); + /* Might return up to four empties, might return nothing */ + countCommands(shell, 0, 3); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h deleted file mode 100644 index d8cbc19cd..000000000 --- a/test/unit/main/interactive_shell_black.h +++ /dev/null @@ -1,130 +0,0 @@ -/********************* */ -/*! \file interactive_shell_black.h - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Aina Niemetz, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. 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 - -//Used in some of the tests -#include -#include - -#include "api/cvc4cpp.h" -#include "expr/expr_manager.h" -#include "expr/symbol_manager.h" -#include "main/interactive_shell.h" -#include "options/base_options.h" -#include "options/language.h" -#include "options/options.h" -#include "parser/parser_builder.h" -#include "smt/command.h" - -using namespace CVC4; -using namespace std; - -class InteractiveShellBlack : public CxxTest::TestSuite -{ - public: - void setUp() override - { - 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_symman.reset(nullptr); - d_solver.reset(new api::Solver(&d_options)); - d_symman.reset(new SymbolManager(d_solver.get())); - } - - void tearDown() override - { - delete d_sin; - delete d_sout; - // ensure that symbol manager is destroyed before solver - d_symman.reset(nullptr); - d_solver.reset(nullptr); - } - - void testAssertTrue() { - *d_sin << "ASSERT TRUE;\n" << flush; - InteractiveShell shell(d_solver.get(), d_symman.get()); - countCommands( shell, 1, 1 ); - } - - void testQueryFalse() { - *d_sin << "QUERY FALSE;\n" << flush; - InteractiveShell shell(d_solver.get(), d_symman.get()); - countCommands( shell, 1, 1 ); - } - - void testDefUse() { - InteractiveShell shell(d_solver.get(), d_symman.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... */ - countCommands( shell, 1, 2 ); - } - - void testDefUse2() { - InteractiveShell shell(d_solver.get(), d_symman.get()); - /* readCommand may return a sequence, see above. */ - *d_sin << "x : REAL;\n" << flush; - Command* tmp = shell.readCommand(); - *d_sin << "ASSERT x > 0;\n" << flush; - countCommands( shell, 1, 1 ); - delete tmp; - } - - void testEmptyLine() { - InteractiveShell shell(d_solver.get(), d_symman.get()); - *d_sin << flush; - countCommands(shell,0,0); - } - - void testRepeatedEmptyLines() { - *d_sin << "\n\n\n"; - InteractiveShell shell(d_solver.get(), d_symman.get()); - /* Might return up to four empties, might return nothing */ - countCommands( shell, 0, 3 ); - } - - private: - std::unique_ptr d_solver; - std::unique_ptr d_symman; - 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); - } -};