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