Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Aina Niemetz, Andrew Reynolds, Andres Noetzli
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Black box testing of cvc5::InteractiveShell.
14 : : */
15 : :
16 : : #include <cvc5/cvc5.h>
17 : : #include <cvc5/cvc5_parser.h>
18 : :
19 : : #include <memory>
20 : : #include <sstream>
21 : : #include <vector>
22 : :
23 : : #include "main/command_executor.h"
24 : : #include "main/interactive_shell.h"
25 : : #include "options/base_options.h"
26 : : #include "options/language.h"
27 : : #include "options/options.h"
28 : : #include "test.h"
29 : :
30 : : using namespace cvc5::parser;
31 : :
32 : : namespace cvc5::internal {
33 : : namespace test {
34 : :
35 : : class TestMainBlackInteractiveShell : public TestInternal
36 : : {
37 : : protected:
38 : 6 : void SetUp() override
39 : : {
40 : 6 : TestInternal::SetUp();
41 : :
42 : 6 : d_sin = std::make_unique<std::stringstream>();
43 : 6 : d_sout = std::make_unique<std::stringstream>();
44 : :
45 : 6 : d_solver.reset(new cvc5::Solver(d_tm));
46 : 6 : d_solver->setOption("input-language", "smt2");
47 : 6 : d_cexec.reset(new main::CommandExecutor(d_solver));
48 : 6 : }
49 : :
50 : 6 : void TearDown() override
51 : : {
52 : 6 : d_sin.reset(nullptr);
53 : 6 : d_sout.reset(nullptr);
54 : : // ensure that command executor is destroyed before solver
55 : 6 : d_cexec.reset(nullptr);
56 : 6 : d_solver.reset(nullptr);
57 : 6 : }
58 : :
59 : : /**
60 : : * Read up to maxIterations+1 from the shell and throw an assertion error if
61 : : * it's fewer than minIterations and more than maxIterations. Note that an
62 : : * empty string followed by EOF may be returned as an empty command, and
63 : : * not NULL (subsequent calls to readAndExecCommands() should return nullptr).
64 : : * E.g., "(check-sat)\n" may return two commands: the check-sat, followed by
65 : : * an empty command, followed by nullptr.
66 : : */
67 : 6 : void countCommands(InteractiveShell& shell,
68 : : uint32_t minIterations,
69 : : uint32_t maxIterations)
70 : : {
71 : 6 : uint32_t n = 0;
72 [ + - ]: 13 : while (n <= maxIterations)
73 : : {
74 [ + + ]: 13 : if (!shell.readAndExecCommands())
75 : : {
76 : 6 : break;
77 : : }
78 : 7 : n++;
79 : : }
80 [ - + ]: 6 : ASSERT_LE(n, maxIterations);
81 [ - + ]: 6 : ASSERT_GE(n, minIterations);
82 : : }
83 : :
84 : : std::unique_ptr<std::stringstream> d_sin;
85 : : std::unique_ptr<std::stringstream> d_sout;
86 : : std::unique_ptr<main::CommandExecutor> d_cexec;
87 : : cvc5::TermManager d_tm;
88 : : std::unique_ptr<cvc5::Solver> d_solver;
89 : : };
90 : :
91 : 2 : TEST_F(TestMainBlackInteractiveShell, assert_true)
92 : : {
93 : 1 : *d_sin << "(assert true)\n" << std::flush;
94 : 2 : InteractiveShell shell(d_cexec.get(), *d_sin, *d_sout);
95 : 1 : countCommands(shell, 1, 1);
96 : 1 : }
97 : :
98 : 2 : TEST_F(TestMainBlackInteractiveShell, query_false)
99 : : {
100 : 1 : *d_sin << "(check-sat)\n" << std::flush;
101 : 2 : InteractiveShell shell(d_cexec.get(), *d_sin, *d_sout);
102 : 1 : countCommands(shell, 1, 1);
103 : 1 : }
104 : :
105 : 2 : TEST_F(TestMainBlackInteractiveShell, def_use1)
106 : : {
107 : 2 : InteractiveShell shell(d_cexec.get(), *d_sin, *d_sout);
108 : 1 : *d_sin << "(declare-const x Real) (assert (> x 0))\n" << std::flush;
109 : : // may read two commands in a single line
110 : 1 : countCommands(shell, 1, 2);
111 : 1 : }
112 : :
113 : 2 : TEST_F(TestMainBlackInteractiveShell, def_use2)
114 : : {
115 : 2 : InteractiveShell shell(d_cexec.get(), *d_sin, *d_sout);
116 : : /* readCommand may return a sequence, see above. */
117 : 1 : *d_sin << "(declare-const x Real)\n" << std::flush;
118 : 1 : shell.readAndExecCommands();
119 : 1 : *d_sin << "(assert (> x 0))\n" << std::flush;
120 : 1 : countCommands(shell, 1, 1);
121 : 1 : }
122 : :
123 : 2 : TEST_F(TestMainBlackInteractiveShell, empty_line)
124 : : {
125 : 2 : InteractiveShell shell(d_cexec.get(), *d_sin, *d_sout);
126 : 1 : *d_sin << std::flush;
127 : 1 : countCommands(shell, 0, 0);
128 : 1 : }
129 : :
130 : 2 : TEST_F(TestMainBlackInteractiveShell, repeated_empty_lines)
131 : : {
132 : 1 : *d_sin << "\n\n\n";
133 : 2 : InteractiveShell shell(d_cexec.get(), *d_sin, *d_sout);
134 : : /* Might return up to four empties, might return nothing */
135 : 1 : countCommands(shell, 0, 3);
136 : 1 : }
137 : : } // namespace test
138 : : } // namespace cvc5::internal
|
