Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Black box testing of the Solver class of the C++ API.
11 : : */
12 : :
13 : : #include <cvc5/cvc5_types.h>
14 : :
15 : : #include <algorithm>
16 : : #include <limits>
17 : :
18 : : #include "options/option_exception.h"
19 : : #include "options/options_public.h"
20 : : #include "test_api.h"
21 : :
22 : : namespace cvc5::internal {
23 : :
24 : : namespace test {
25 : :
26 : : template <class... Ts>
27 : : struct overloaded : Ts...
28 : : {
29 : : using Ts::operator()...;
30 : : };
31 : : template <class... Ts>
32 : : overloaded(Ts...) -> overloaded<Ts...>;
33 : :
34 : : class TestBlackOptions : public TestApi
35 : : {
36 : : public:
37 : : /**
38 : : * Tests setting options for option "name", including error values.
39 : : */
40 : 27704 : void testSetOption(const std::string& name)
41 : : {
42 : 27704 : auto info = d_solver->getOptionInfo(name);
43 : :
44 : : try
45 : : {
46 : 27704 : std::visit(
47 : 27704 : overloaded{
48 : 1482 : [this, &name](const OptionInfo::VoidInfo&) {
49 : 1447 : d_solver->setOption(name, "");
50 : 35 : },
51 : 74796 : [this, &name](const OptionInfo::ValueInfo<bool>&) {
52 : 18699 : d_solver->setOption(name, "false");
53 : 18699 : d_solver->setOption(name, "true");
54 : 18699 : },
55 : 294 : [this, &name](const OptionInfo::ValueInfo<std::string>&) {
56 : 147 : d_solver->setOption(name, "foo");
57 : 147 : },
58 : 8670 : [this, &name](const OptionInfo::NumberInfo<int64_t>& v) {
59 : 1402 : std::pair<int64_t, int64_t> range{
60 : : std::numeric_limits<int64_t>::min(),
61 : : std::numeric_limits<int64_t>::max()};
62 [ + + ]: 1402 : if (v.minimum)
63 : : {
64 : 574 : EXPECT_THROW(
65 : : d_solver->setOption(name, std::to_string(*v.minimum - 1)),
66 : 287 : CVC5ApiOptionException);
67 [ + - ][ + - ]: 287 : EXPECT_NO_THROW(
[ - - ]
68 : 287 : d_solver->setOption(name, std::to_string(*v.minimum)));
69 : 287 : range.first = *v.minimum;
70 : : }
71 [ + + ]: 1402 : if (v.maximum)
72 : : {
73 : 256 : EXPECT_THROW(
74 : : d_solver->setOption(name, std::to_string(*v.maximum + 1)),
75 : 128 : CVC5ApiOptionException);
76 [ + - ][ + - ]: 128 : EXPECT_NO_THROW(
[ - - ]
77 : 128 : d_solver->setOption(name, std::to_string(*v.maximum)));
78 : 128 : range.second = *v.maximum;
79 : : }
80 : : // Compute the midpoint without overflowing. Note that neither
81 : : // (first + second) nor the span (second - first) is
82 : : // representable in general, e.g., for [-1, INT64_MAX].
83 [ + - ][ + - ]: 1402 : EXPECT_NO_THROW(d_solver->setOption(
[ - - ]
84 : : name,
85 : : std::to_string(range.first / 2 + range.second / 2
86 : : + (range.first % 2 + range.second % 2)
87 : 1402 : / 2)));
88 : 4206 : EXPECT_THROW(d_solver->setOption(name, "0123abc"),
89 : 1402 : CVC5ApiOptionException);
90 : 1402 : },
91 : 16144 : [this, &name](const OptionInfo::NumberInfo<uint64_t>& v) {
92 : 1976 : std::pair<uint64_t, uint64_t> range{
93 : : std::numeric_limits<uint64_t>::min(),
94 : : std::numeric_limits<uint64_t>::max()};
95 : 5928 : EXPECT_THROW(d_solver->setOption(name, "-1"),
96 : 1976 : CVC5ApiOptionException);
97 [ + + ]: 1976 : if (v.minimum)
98 : : {
99 : 538 : EXPECT_THROW(
100 : : d_solver->setOption(name, std::to_string(*v.minimum - 1)),
101 : 269 : CVC5ApiOptionException);
102 [ + - ][ + - ]: 269 : EXPECT_NO_THROW(
[ - - ]
103 : 269 : d_solver->setOption(name, std::to_string(*v.minimum)));
104 : 269 : range.first = *v.minimum;
105 : : }
106 [ + + ]: 1976 : if (v.maximum)
107 : : {
108 : 618 : EXPECT_THROW(
109 : : d_solver->setOption(name, std::to_string(*v.maximum + 1)),
110 : 309 : CVC5ApiOptionException);
111 [ + - ][ + - ]: 309 : EXPECT_NO_THROW(
[ - - ]
112 : 309 : d_solver->setOption(name, std::to_string(*v.maximum)));
113 : 309 : range.second = *v.maximum;
114 : : }
115 : : // Compute the midpoint without overflowing: range.second is
116 : : // UINT64_MAX unless the option declares a maximum.
117 [ + - ][ + - ]: 1976 : EXPECT_NO_THROW(d_solver->setOption(
[ - - ]
118 : : name,
119 : : std::to_string(range.first
120 : 1976 : + (range.second - range.first) / 2)));
121 : 5928 : EXPECT_THROW(d_solver->setOption(name, "0123abc"),
122 : 1976 : CVC5ApiOptionException);
123 : 1976 : },
124 : 2537 : [this, &name](const OptionInfo::NumberInfo<double>& v) {
125 : 279 : std::pair<double, double> range{
126 : : std::numeric_limits<double>::min(),
127 : : std::numeric_limits<double>::max()};
128 [ + + ]: 279 : if (v.minimum)
129 : : {
130 : 460 : EXPECT_THROW(
131 : : d_solver->setOption(name, std::to_string(*v.minimum - 1)),
132 : 230 : CVC5ApiOptionException);
133 [ + - ][ + - ]: 230 : EXPECT_NO_THROW(
[ - - ]
134 : 230 : d_solver->setOption(name, std::to_string(*v.minimum)));
135 : 230 : range.first = *v.minimum;
136 : : }
137 [ + + ]: 279 : if (v.maximum)
138 : : {
139 : 390 : EXPECT_THROW(
140 : : d_solver->setOption(name, std::to_string(*v.maximum + 1)),
141 : 195 : CVC5ApiOptionException);
142 [ + - ][ + - ]: 195 : EXPECT_NO_THROW(
[ - - ]
143 : 195 : d_solver->setOption(name, std::to_string(*v.maximum)));
144 : 195 : range.second = *v.maximum;
145 : : }
146 [ + - ][ + - ]: 279 : EXPECT_NO_THROW(d_solver->setOption(
[ - - ]
147 : 279 : name, std::to_string((range.first + range.second) / 2)));
148 : 279 : },
149 : 69736 : [this, &name](const OptionInfo::ModeInfo& v) {
150 : 13380 : EXPECT_THROW(d_solver->setOption(name, "foobarbaz"),
151 : 4460 : CVC5ApiOptionException);
152 [ + + ]: 18458 : for (const auto& m : v.modes)
153 : : {
154 : 14088 : d_solver->setOption(name, m);
155 [ - + ]: 27996 : EXPECT_EQ(d_solver->getOption(name), m);
156 : : }
157 : 4370 : EXPECT_DEATH(d_solver->setOption(name, "help"), "");
158 : 4278 : },
159 : : },
160 : : info.valueInfo);
161 : : }
162 [ - + ]: 796 : catch (const CVC5ApiOptionException&)
163 : : {
164 : 796 : }
165 : 27612 : }
166 : : /**
167 : : * Sets a single valid option for option "name".
168 : : */
169 : 64 : void testSetOptionOnce(const std::string& name)
170 : : {
171 : 64 : auto info = d_solver->getOptionInfo(name);
172 : :
173 : : try
174 : : {
175 : 64 : std::visit(
176 : 64 : overloaded{
177 : 14 : [this, &name](const OptionInfo::VoidInfo&) {
178 : 14 : d_solver->setOption(name, "");
179 : 0 : },
180 : 76 : [this, &name](const OptionInfo::ValueInfo<bool>&) {
181 : 38 : d_solver->setOption(name, "false");
182 : 38 : },
183 : 4 : [this, &name](const OptionInfo::ValueInfo<std::string>&) {
184 : 2 : d_solver->setOption(name, "foo");
185 : 2 : },
186 : 6 : [this, &name](const OptionInfo::NumberInfo<int64_t>&) {
187 : 3 : std::pair<int64_t, int64_t> range{
188 : : std::numeric_limits<int64_t>::min(),
189 : : std::numeric_limits<int64_t>::max()};
190 : 6 : d_solver->setOption(
191 : 6 : name, std::to_string((range.first + range.second) / 2));
192 : 3 : },
193 : 14 : [this, &name](const OptionInfo::NumberInfo<uint64_t>&) {
194 : 7 : std::pair<uint64_t, uint64_t> range{
195 : : std::numeric_limits<uint64_t>::min(),
196 : : std::numeric_limits<uint64_t>::max()};
197 : 14 : d_solver->setOption(
198 : 14 : name, std::to_string((range.first + range.second) / 2));
199 : 7 : },
200 : 0 : [this, &name](const OptionInfo::NumberInfo<double>&) {
201 : 0 : std::pair<double, double> range{
202 : : std::numeric_limits<double>::min(),
203 : : std::numeric_limits<double>::max()};
204 : 0 : d_solver->setOption(
205 : 0 : name, std::to_string((range.first + range.second) / 2));
206 : 0 : },
207 : 21 : [this, &name](const OptionInfo::ModeInfo& v) {
208 [ + - ]: 7 : if (!v.modes.empty())
209 : : {
210 : 7 : d_solver->setOption(name, v.modes[0]);
211 : : }
212 : 7 : },
213 : : },
214 : : info.valueInfo);
215 : : }
216 [ - + ]: 7 : catch (const CVC5ApiOptionException&)
217 : : {
218 : 7 : }
219 : 64 : }
220 : : };
221 : :
222 : 188 : TEST_F(TestBlackOptions, set)
223 : : {
224 : : const std::set<std::string> muted{"copyright",
225 : : "help",
226 : : "show-config",
227 : : "show-debug-tags",
228 : : "show-trace-tags",
229 : 837 : "version"};
230 [ + + ]: 27740 : for (const auto& name : options::getNames())
231 : : {
232 [ + + ]: 27739 : if (name == "safe-mode")
233 : : {
234 : : // don't test safe-mode here, since it will restrict the set of options
235 : : // that can be set afterwards.
236 : 35 : continue;
237 : : }
238 [ + + ]: 27704 : if (muted.count(name))
239 : : {
240 : 223 : testing::internal::CaptureStdout();
241 : : }
242 : 27704 : testSetOption(name);
243 [ + + ]: 27612 : if (muted.count(name))
244 : : {
245 : 223 : testing::internal::GetCapturedStdout();
246 : : }
247 : 1 : }
248 : 1 : }
249 : :
250 : 4 : TEST_F(TestBlackOptions, setSafe)
251 : : {
252 : : const std::set<std::string> muted{"copyright",
253 : : "help",
254 : : "show-config",
255 : : "show-debug-tags",
256 : : "show-trace-tags",
257 : 9 : "version"};
258 : : // set safe options to true
259 : 1 : d_solver->setOption("safe-mode", "safe");
260 : 1 : bool alreadySetRegular = false;
261 [ + + ]: 538 : for (const auto& name : options::getNames())
262 : : {
263 : 537 : auto info = d_solver->getOptionInfo(name);
264 : : // skip if an expert option or has an supported feature
265 : 1426 : if (info.category == cvc5::modes::OptionCategory::EXPERT
266 [ + + ][ + + ]: 537 : || !info.noSupports.empty())
[ + + ]
267 : : {
268 : 352 : continue;
269 : : }
270 [ + + ]: 185 : if (info.category == cvc5::modes::OptionCategory::REGULAR)
271 : : {
272 [ + + ]: 122 : if (alreadySetRegular)
273 : : {
274 : : // skip if already set a regular option
275 : 121 : continue;
276 : : }
277 : 1 : alreadySetRegular = true;
278 : : }
279 [ + + ]: 64 : if (muted.count(name))
280 : : {
281 : 4 : testing::internal::CaptureStdout();
282 : : }
283 : : // set the option once
284 : 64 : testSetOptionOnce(name);
285 [ + + ]: 64 : if (muted.count(name))
286 : : {
287 : 4 : testing::internal::GetCapturedStdout();
288 : : }
289 [ + + ]: 538 : }
290 : 1 : }
291 : :
292 : 4 : TEST_F(TestBlackOptions, getOptionInfoBenchmark)
293 : : {
294 : 1 : auto names = options::getNames();
295 : : std::unordered_set<std::string> ignore = {
296 : : "output",
297 : : "quiet",
298 : : "rweight",
299 : : "trace",
300 : : "verbose",
301 : 8 : };
302 : 538 : auto end = std::remove_if(names.begin(), names.end(), [&](const auto& i) {
303 : 537 : return ignore.count(i);
304 : : });
305 : 1 : names.erase(end, names.end());
306 : 1 : size_t ct = 0;
307 [ + + ]: 1001 : for (size_t i = 0; i < 1000; ++i)
308 : : {
309 [ + + ]: 533000 : for (const auto& name : names)
310 : : {
311 : 532000 : ct += d_solver->getOption(name).size();
312 : : }
313 : : }
314 : 1 : std::cout << ct << std::endl;
315 : 1 : }
316 : :
317 : : } // namespace test
318 : : } // namespace cvc5::internal
|
