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