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
|
/********************* */
/*! \file interactive_shell_black.h
** \verbatim
** Top contributors (to current version):
** Christopher L. Conway, Aina Niemetz, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 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 <cxxtest/TestSuite.h>
//Used in some of the tests
#include <vector>
#include <sstream>
#include "api/cvc4cpp.h"
#include "expr/expr_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_solver.reset(new api::Solver(&d_options));
}
void tearDown() override
{
delete d_sin;
delete d_sout;
}
void testAssertTrue() {
*d_sin << "ASSERT TRUE;\n" << flush;
InteractiveShell shell(d_solver.get());
countCommands( shell, 1, 1 );
}
void testQueryFalse() {
*d_sin << "QUERY FALSE;\n" << flush;
InteractiveShell shell(d_solver.get());
countCommands( shell, 1, 1 );
}
void testDefUse() {
InteractiveShell shell(d_solver.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());
/* 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_sin << flush;
countCommands(shell,0,0);
}
void testRepeatedEmptyLines() {
*d_sin << "\n\n\n";
InteractiveShell shell(d_solver.get());
/* Might return up to four empties, might return nothing */
countCommands( shell, 0, 3 );
}
private:
std::unique_ptr<api::Solver> d_solver;
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);
}
};
|
