Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Gereon Kremer, Andrew Reynolds, Aina Niemetz
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 the Solver class of the C++ API.
14 : : */
15 : :
16 : : #include <cvc5/cvc5_types.h>
17 : :
18 : : #include <algorithm>
19 : : #include <limits>
20 : :
21 : : #include "options/option_exception.h"
22 : : #include "options/options_public.h"
23 : : #include "test_api.h"
24 : :
25 : : namespace cvc5::internal {
26 : :
27 : : namespace test {
28 : :
29 : : template <class... Ts>
30 : : struct overloaded : Ts...
31 : : {
32 : : using Ts::operator()...;
33 : : };
34 : : template <class... Ts>
35 : : overloaded(Ts...) -> overloaded<Ts...>;
36 : :
37 : : class TestBlackOptions : public TestApi
38 : : {
39 : : public:
40 : : /**
41 : : * Tests setting options for option "name", including error values.
42 : : */
43 : 27201 : void testSetOption(const std::string& name)
44 : : {
45 : 54310 : auto info = d_solver->getOptionInfo(name);
46 : :
47 : : try
48 : : {
49 : 27201 : std::visit(
50 : 27201 : overloaded{
51 : 1482 : [this, &name](const OptionInfo::VoidInfo& v) {
52 : 1447 : d_solver->setOption(name, "");
53 : 35 : },
54 : 73816 : [this, &name](const OptionInfo::ValueInfo<bool>& v) {
55 : 18454 : d_solver->setOption(name, "false");
56 : 18454 : d_solver->setOption(name, "true");
57 : 18454 : },
58 : 294 : [this, &name](const OptionInfo::ValueInfo<std::string>& v) {
59 : 147 : d_solver->setOption(name, "foo");
60 : 147 : },
61 : 7646 : [this, &name](const OptionInfo::NumberInfo<int64_t>& v) {
62 : 1402 : std::pair<int64_t, int64_t> range{
63 : : std::numeric_limits<int64_t>::min(),
64 : : std::numeric_limits<int64_t>::max()};
65 [ + + ]: 1402 : if (v.minimum)
66 : : {
67 [ + - ][ + - ]: 477 : EXPECT_THROW(
[ - + ]
68 : : d_solver->setOption(name, std::to_string(*v.minimum - 1)),
69 : : CVC5ApiOptionException);
70 [ + - ][ + - ]: 159 : EXPECT_NO_THROW(
71 : : d_solver->setOption(name, std::to_string(*v.minimum)));
72 : 159 : range.first = *v.minimum;
73 : : }
74 [ - + ]: 1402 : if (v.maximum)
75 : : {
76 : 0 : EXPECT_THROW(
77 : : d_solver->setOption(name, std::to_string(*v.maximum + 1)),
78 : : CVC5ApiOptionException);
79 : 0 : EXPECT_NO_THROW(
80 : : d_solver->setOption(name, std::to_string(*v.maximum)));
81 : 0 : range.second = *v.maximum;
82 : : }
83 [ + - ][ + - ]: 1402 : EXPECT_NO_THROW(d_solver->setOption(
84 : : name, std::to_string((range.first + range.second) / 2)));
85 [ + - ][ + - ]: 5608 : EXPECT_THROW(d_solver->setOption(name, "0123abc"),
[ - + ]
86 : : CVC5ApiOptionException);
87 : 1402 : },
88 : 13258 : [this, &name](const OptionInfo::NumberInfo<uint64_t>& v) {
89 : 1718 : std::pair<uint64_t, uint64_t> range{
90 : : std::numeric_limits<uint64_t>::min(),
91 : : std::numeric_limits<uint64_t>::max()};
92 [ + - ][ + - ]: 6872 : EXPECT_THROW(d_solver->setOption(name, "-1"),
[ - + ]
93 : : CVC5ApiOptionException);
94 [ + + ]: 1718 : if (v.minimum)
95 : : {
96 [ + - ][ + - ]: 267 : EXPECT_THROW(
[ - + ]
97 : : d_solver->setOption(name, std::to_string(*v.minimum - 1)),
98 : : CVC5ApiOptionException);
99 [ + - ][ + - ]: 89 : EXPECT_NO_THROW(
100 : : d_solver->setOption(name, std::to_string(*v.minimum)));
101 : 89 : range.first = *v.minimum;
102 : : }
103 [ + + ]: 1718 : if (v.maximum)
104 : : {
105 [ + - ][ + - ]: 657 : EXPECT_THROW(
[ - + ]
106 : : d_solver->setOption(name, std::to_string(*v.maximum + 1)),
107 : : CVC5ApiOptionException);
108 [ + - ][ + - ]: 219 : EXPECT_NO_THROW(
109 : : d_solver->setOption(name, std::to_string(*v.maximum)));
110 : 219 : range.second = *v.maximum;
111 : : }
112 [ + - ][ + - ]: 1718 : EXPECT_NO_THROW(d_solver->setOption(
113 : : name, std::to_string((range.first + range.second) / 2)));
114 [ + - ][ + - ]: 6872 : EXPECT_THROW(d_solver->setOption(name, "0123abc"),
[ - + ]
115 : : CVC5ApiOptionException);
116 : 1718 : },
117 : 2537 : [this, &name](const OptionInfo::NumberInfo<double>& v) {
118 : 279 : std::pair<double, double> range{
119 : : std::numeric_limits<double>::min(),
120 : : std::numeric_limits<double>::max()};
121 [ + + ]: 279 : if (v.minimum)
122 : : {
123 [ + - ][ + - ]: 690 : EXPECT_THROW(
[ - + ]
124 : : d_solver->setOption(name, std::to_string(*v.minimum - 1)),
125 : : CVC5ApiOptionException);
126 [ + - ][ + - ]: 230 : EXPECT_NO_THROW(
127 : : d_solver->setOption(name, std::to_string(*v.minimum)));
128 : 230 : range.first = *v.minimum;
129 : : }
130 [ + + ]: 279 : if (v.maximum)
131 : : {
132 [ + - ][ + - ]: 585 : EXPECT_THROW(
[ - + ]
133 : : d_solver->setOption(name, std::to_string(*v.maximum + 1)),
134 : : CVC5ApiOptionException);
135 [ + - ][ + - ]: 195 : EXPECT_NO_THROW(
136 : : d_solver->setOption(name, std::to_string(*v.maximum)));
137 : 195 : range.second = *v.maximum;
138 : : }
139 [ + - ][ + - ]: 279 : EXPECT_NO_THROW(d_solver->setOption(
140 : : name, std::to_string((range.first + range.second) / 2)));
141 : 279 : },
142 : 69696 : [this, &name](const OptionInfo::ModeInfo& v) {
143 [ + - ][ + - ]: 17840 : EXPECT_THROW(d_solver->setOption(name, "foobarbaz"),
[ - + ]
144 : : CVC5ApiOptionException);
145 [ + + ]: 18448 : for (const auto& m : v.modes)
146 : : {
147 : 14078 : d_solver->setOption(name, m);
148 [ - + ]: 27976 : EXPECT_EQ(d_solver->getOption(name), m);
149 : : }
150 : 4370 : EXPECT_DEATH(d_solver->setOption(name, "help"), "");
151 : 4278 : },
152 : : },
153 : : info.valueInfo);
154 : : }
155 : 796 : catch (const CVC5ApiOptionException&)
156 : : {
157 : : }
158 : 27109 : }
159 : : /**
160 : : * Sets a single valid option for option "name".
161 : : */
162 : 59 : void testSetOptionOnce(const std::string& name)
163 : : {
164 : 118 : auto info = d_solver->getOptionInfo(name);
165 : :
166 : : try
167 : : {
168 : 59 : std::visit(
169 : 59 : overloaded{
170 : 14 : [this, &name](const OptionInfo::VoidInfo& v) {
171 : 14 : d_solver->setOption(name, "");
172 : 0 : },
173 : 68 : [this, &name](const OptionInfo::ValueInfo<bool>& v) {
174 : 34 : d_solver->setOption(name, "false");
175 : 34 : },
176 : 4 : [this, &name](const OptionInfo::ValueInfo<std::string>& v) {
177 : 2 : d_solver->setOption(name, "foo");
178 : 2 : },
179 : 6 : [this, &name](const OptionInfo::NumberInfo<int64_t>& v) {
180 : 3 : std::pair<int64_t, int64_t> range{
181 : : std::numeric_limits<int64_t>::min(),
182 : : std::numeric_limits<int64_t>::max()};
183 : 6 : d_solver->setOption(
184 : 6 : name, std::to_string((range.first + range.second) / 2));
185 : 3 : },
186 : 14 : [this, &name](const OptionInfo::NumberInfo<uint64_t>& v) {
187 : 7 : std::pair<uint64_t, uint64_t> range{
188 : : std::numeric_limits<uint64_t>::min(),
189 : : std::numeric_limits<uint64_t>::max()};
190 : 14 : d_solver->setOption(
191 : 14 : name, std::to_string((range.first + range.second) / 2));
192 : 7 : },
193 : 0 : [this, &name](const OptionInfo::NumberInfo<double>& v) {
194 : 0 : std::pair<double, double> range{
195 : : std::numeric_limits<double>::min(),
196 : : std::numeric_limits<double>::max()};
197 : 0 : d_solver->setOption(
198 : 0 : name, std::to_string((range.first + range.second) / 2));
199 : 0 : },
200 : 18 : [this, &name](const OptionInfo::ModeInfo& v) {
201 [ + - ]: 6 : if (!v.modes.empty())
202 : : {
203 : 6 : d_solver->setOption(name, v.modes[0]);
204 : : }
205 : 6 : },
206 : : },
207 : : info.valueInfo);
208 : : }
209 : 7 : catch (const CVC5ApiOptionException&)
210 : : {
211 : : }
212 : 59 : }
213 : : };
214 : :
215 : 186 : TEST_F(TestBlackOptions, set)
216 : : {
217 : : const std::set<std::string> muted{"copyright",
218 : : "help",
219 : : "show-config",
220 : : "show-debug-tags",
221 : : "show-trace-tags",
222 : 838 : "version"};
223 [ + + ]: 27237 : for (const auto& name : options::getNames())
224 : : {
225 [ + + ]: 27236 : if (name == "safe-mode")
226 : : {
227 : : // don't test safe-mode here, since it will restrict the set of options
228 : : // that can be set afterwards.
229 : 35 : continue;
230 : : }
231 [ + + ]: 27201 : if (muted.count(name))
232 : : {
233 : 223 : testing::internal::CaptureStdout();
234 : : }
235 : 27201 : testSetOption(name);
236 [ + + ]: 27109 : if (muted.count(name))
237 : : {
238 : 223 : testing::internal::GetCapturedStdout();
239 : : }
240 : : }
241 : 1 : }
242 : :
243 : 2 : TEST_F(TestBlackOptions, setSafe)
244 : : {
245 : : const std::set<std::string> muted{"copyright",
246 : : "help",
247 : : "show-config",
248 : : "show-debug-tags",
249 : : "show-trace-tags",
250 : 10 : "version"};
251 : : // set safe options to true
252 : 1 : d_solver->setOption("safe-mode", "safe");
253 : 1 : bool alreadySetRegular = false;
254 [ + + ]: 530 : for (const auto& name : options::getNames())
255 : : {
256 : 529 : auto info = d_solver->getOptionInfo(name);
257 : : // skip if an expert option or has an supported feature
258 : 1401 : if (info.category == cvc5::modes::OptionCategory::EXPERT
259 [ + + ][ + + ]: 529 : || !info.noSupports.empty())
[ + + ]
260 : : {
261 : 343 : continue;
262 : : }
263 [ + + ]: 186 : if (info.category == cvc5::modes::OptionCategory::REGULAR)
264 : : {
265 [ + + ]: 128 : if (alreadySetRegular)
266 : : {
267 : : // skip if already set a regular option
268 : 127 : continue;
269 : : }
270 : 1 : alreadySetRegular = true;
271 : : }
272 [ + + ]: 59 : if (muted.count(name))
273 : : {
274 : 4 : testing::internal::CaptureStdout();
275 : : }
276 : : // set the option once
277 : 59 : testSetOptionOnce(name);
278 [ + + ]: 59 : if (muted.count(name))
279 : : {
280 : 4 : testing::internal::GetCapturedStdout();
281 : : }
282 : : }
283 : 1 : }
284 : :
285 : 2 : TEST_F(TestBlackOptions, getOptionInfoBenchmark)
286 : : {
287 : 2 : auto names = options::getNames();
288 : : std::unordered_set<std::string> ignore = {
289 : : "output",
290 : : "quiet",
291 : : "rweight",
292 : : "trace",
293 : : "verbose",
294 : 9 : };
295 : 529 : auto end = std::remove_if(names.begin(), names.end(), [&](const auto& i){
296 : 529 : return ignore.count(i);
297 : 1 : });
298 : 1 : names.erase(end, names.end());
299 : 1 : size_t ct = 0;
300 [ + + ]: 1001 : for (size_t i = 0; i < 1000; ++i)
301 : : {
302 [ + + ]: 525000 : for (const auto& name : names)
303 : : {
304 : 524000 : ct += d_solver->getOption(name).size();
305 : : }
306 : : }
307 : 1 : std::cout << ct << std::endl;
308 : 1 : }
309 : :
310 : : } // namespace test
311 : : } // namespace cvc5::internal
|
