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 : : * Interface for custom handlers and predicates options.
11 : : */
12 : :
13 : : #include "options/options_handler.h"
14 : :
15 : : #include <iostream>
16 : : #include <ostream>
17 : : #include <regex>
18 : : #include <string>
19 : :
20 : : #include "base/check.h"
21 : : #include "base/configuration.h"
22 : : #include "base/configuration_private.h"
23 : : #include "base/cvc5config.h"
24 : : #include "base/exception.h"
25 : : #include "base/modal_exception.h"
26 : : #include "base/output.h"
27 : : #include "lib/strtok_r.h"
28 : : #include "options/base_options.h"
29 : : #include "options/bv_options.h"
30 : : #include "options/decision_options.h"
31 : : #include "options/io_utils.h"
32 : : #include "options/language.h"
33 : : #include "options/main_options.h"
34 : : #include "options/option_exception.h"
35 : : #include "options/parser_options.h"
36 : : #include "options/smt_options.h"
37 : : #include "options/theory_options.h"
38 : : #include "util/didyoumean.h"
39 : :
40 : : namespace cvc5::internal {
41 : : namespace options {
42 : :
43 : : // helper functions
44 : : namespace {
45 : :
46 : 33 : void printTags(std::ostream& out, const std::vector<std::string>& tags)
47 : : {
48 : 33 : out << "available tags:" << std::endl;
49 [ + + ]: 49929 : for (const auto& t : tags)
50 : : {
51 : 49896 : out << " " << t << std::endl;
52 : : }
53 : 33 : out << std::endl;
54 : 33 : }
55 : :
56 : 8 : std::string suggestTags(const std::vector<std::string>& validTags,
57 : : const std::string& inputTag,
58 : : const std::vector<std::string>& additionalTags)
59 : : {
60 : 8 : DidYouMean didYouMean;
61 : 8 : didYouMean.addWords(validTags);
62 : 8 : didYouMean.addWords(additionalTags);
63 : 16 : return didYouMean.getMatchAsString(inputTag);
64 : 8 : }
65 : :
66 : : /**
67 : : * Select all tags from validTags that match the given (globbing) pattern.
68 : : * The pattern may contain `*` as wildcards. These are internally converted to
69 : : * `.*` and matched using std::regex. If no wildcards are present, regular
70 : : * string comparisons are used.
71 : : */
72 : 11 : std::vector<std::string> selectTags(const std::vector<std::string>& validTags,
73 : : std::string pattern)
74 : : {
75 : 11 : bool isRegex = false;
76 : 11 : size_t pos = 0;
77 [ - + ]: 11 : while ((pos = pattern.find('*', pos)) != std::string::npos)
78 : : {
79 : 0 : pattern.replace(pos, 1, ".*");
80 : 0 : pos += 2;
81 : 0 : isRegex = true;
82 : : }
83 : 11 : std::vector<std::string> results;
84 [ - + ]: 11 : if (isRegex)
85 : : {
86 : 0 : std::regex re(pattern);
87 : 0 : std::copy_if(validTags.begin(),
88 : : validTags.end(),
89 : : std::back_inserter(results),
90 : 0 : [&re](const auto& tag) { return std::regex_match(tag, re); });
91 : 0 : }
92 : : else
93 : : {
94 : 11 : if (std::find(validTags.begin(), validTags.end(), pattern)
95 [ + + ]: 22 : != validTags.end())
96 : : {
97 : 3 : results.emplace_back(pattern);
98 : : }
99 : : }
100 : 11 : return results;
101 : 0 : }
102 : :
103 : : } // namespace
104 : :
105 : 146334 : OptionsHandler::OptionsHandler(Options* options) : d_options(options) {}
106 : :
107 : 2 : void OptionsHandler::setErrStream(CVC5_UNUSED const std::string& flag,
108 : : const ManagedErr& me) const
109 : : {
110 [ - + ]: 2 : Warning.setStream(me);
111 : 2 : TraceChannel.setStream(me);
112 : 2 : }
113 : :
114 : 31476 : Language OptionsHandler::stringToLanguage(const std::string& flag,
115 : : const std::string& optarg) const
116 : : {
117 [ - + ]: 31476 : if (optarg == "help")
118 : : {
119 : 0 : *d_options->base.out << R"FOOBAR(
120 : : Languages currently supported as arguments to the -L / --lang option:
121 : : auto attempt to automatically determine language
122 : : smt | smtlib | smt2 |
123 : : smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard
124 : : sygus | sygus2 SyGuS version 2.0
125 : :
126 : : Languages currently supported as arguments to the --output-lang option:
127 : : auto match output language to input language
128 : : smt | smtlib | smt2 |
129 : : smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard
130 : : ast internal format (simple syntax trees)
131 : 0 : )FOOBAR" << std::endl;
132 : 0 : throw OptionException("help is not a valid language");
133 : : }
134 : :
135 : : try
136 : : {
137 : 31476 : return language::toLanguage(optarg);
138 : : }
139 [ - + ]: 247 : catch (OptionException& oe)
140 : : {
141 : 741 : throw OptionException("Error in " + flag + ": " + oe.getMessage()
142 : 988 : + "\nTry --lang help");
143 : 247 : }
144 : :
145 : : Unreachable();
146 : : }
147 : :
148 : 24338 : void OptionsHandler::setInputLanguage(const std::string& flag,
149 : : const Language lang) const
150 : : {
151 [ - + ]: 24338 : if (lang == Language::LANG_AST)
152 : : {
153 : 0 : throw OptionException("Language LANG_AST is not allowed for " + flag);
154 : : }
155 [ + + ]: 24338 : if (!d_options->printer.outputLanguageWasSetByUser)
156 : : {
157 : 20288 : d_options->write_printer().outputLanguage = lang;
158 : 20288 : ioutils::setDefaultOutputLanguage(lang);
159 : : }
160 : 24338 : }
161 : :
162 : 869 : void OptionsHandler::setVerbosity(CVC5_UNUSED const std::string& flag,
163 : : const int value) const
164 : : {
165 [ - + ]: 869 : if (Configuration::isMuzzledBuild())
166 : : {
167 : 0 : TraceChannel.setStream(&cvc5::internal::null_os);
168 : 0 : WarningChannel.setStream(&cvc5::internal::null_os);
169 : : }
170 : : else
171 : : {
172 [ + + ]: 869 : if (value < 0)
173 : : {
174 : 621 : WarningChannel.setStream(&cvc5::internal::null_os);
175 : : }
176 : : else
177 : : {
178 : 248 : WarningChannel.setStream(&std::cerr);
179 : : }
180 : : }
181 : 869 : }
182 : :
183 : 621 : void OptionsHandler::decreaseVerbosity(CVC5_UNUSED const std::string& flag,
184 : : CVC5_UNUSED bool value)
185 : : {
186 : 621 : d_options->write_base().verbosity -= 1;
187 : 621 : setVerbosity(flag, d_options->base.verbosity);
188 : 621 : }
189 : :
190 : 3 : void OptionsHandler::increaseVerbosity(CVC5_UNUSED const std::string& flag,
191 : : CVC5_UNUSED bool value)
192 : : {
193 : 3 : d_options->write_base().verbosity += 1;
194 : 3 : setVerbosity(flag, d_options->base.verbosity);
195 : 3 : }
196 : :
197 : 63 : void OptionsHandler::setStats(CVC5_UNUSED const std::string& flag,
198 : : const bool value) const
199 : : {
200 : : #ifndef CVC5_STATISTICS_ON
201 : : if (value)
202 : : {
203 : : std::stringstream ss;
204 : : ss << "option `" << flag
205 : : << "' requires a statistics-enabled build of cvc5; this binary was not "
206 : : "built with statistics support";
207 : : throw OptionException(ss.str());
208 : : }
209 : : #endif /* CVC5_STATISTICS_ON */
210 [ + + ]: 63 : if (!value)
211 : : {
212 : 33 : d_options->write_base().statisticsAll = false;
213 : 33 : d_options->write_base().statisticsEveryQuery = false;
214 : 33 : d_options->write_base().statisticsInternal = false;
215 : : }
216 : 63 : }
217 : :
218 : 184 : void OptionsHandler::setStatsDetail(CVC5_UNUSED const std::string& flag,
219 : : const bool value) const
220 : : {
221 : : #ifndef CVC5_STATISTICS_ON
222 : : if (value)
223 : : {
224 : : std::stringstream ss;
225 : : ss << "option `" << flag
226 : : << "' requires a statistics-enabled build of cvc5; this binary was not "
227 : : "built with statistics support";
228 : : throw OptionException(ss.str());
229 : : }
230 : : #endif /* CVC5_STATISTICS_ON */
231 [ + + ]: 184 : if (value)
232 : : {
233 : 92 : d_options->write_base().statistics = true;
234 : : }
235 : 184 : }
236 : :
237 : 11 : void OptionsHandler::enableTraceTag(CVC5_UNUSED const std::string& flag,
238 : : const std::string& optarg) const
239 : : {
240 [ - + ]: 11 : if (!Configuration::isTracingBuild())
241 : : {
242 : 0 : throw OptionException("trace tags not available in non-tracing builds");
243 : : }
244 : 11 : const auto tags = selectTags(Configuration::getTraceTags(), optarg);
245 [ + + ]: 11 : if (tags.empty())
246 : : {
247 [ - + ]: 8 : if (optarg == "help")
248 : : {
249 : 0 : d_options->write_driver().showTraceTags = true;
250 : 0 : showTraceTags("", true);
251 : 0 : return;
252 : : }
253 : :
254 : 8 : throw OptionException(
255 : 16 : std::string("no trace tag matching ") + optarg
256 : 32 : + std::string(" was found.")
257 : 32 : + suggestTags(Configuration::getTraceTags(), optarg, {}));
258 : : }
259 [ + + ]: 6 : for (const auto& tag : tags)
260 : : {
261 : 3 : TraceChannel.on(tag);
262 : : }
263 [ + - ]: 11 : }
264 : :
265 : 4339 : void OptionsHandler::enableOutputTag(CVC5_UNUSED const std::string& flag,
266 : : const OutputTag optarg) const
267 : : {
268 : 4339 : const size_t tagid = static_cast<size_t>(optarg);
269 [ - + ][ - + ]: 4339 : Assert(d_options->base.outputTagHolder.size() > tagid)
[ - - ]
270 : 0 : << "Output tag is larger than the bitset that holds it.";
271 : 4339 : d_options->write_base().outputTagHolder.set(tagid);
272 : 4339 : }
273 : :
274 : 35 : void OptionsHandler::setResourceWeight(CVC5_UNUSED const std::string& flag,
275 : : const std::string& optarg) const
276 : : {
277 : 35 : d_options->write_base().resourceWeightHolder.emplace_back(optarg);
278 : 35 : }
279 : :
280 : 441 : void OptionsHandler::checkBvSatSolver(const std::string& flag,
281 : : const BvSatSolverMode m) const
282 : : {
283 : 441 : if (m == BvSatSolverMode::CRYPTOMINISAT
284 [ + + ][ - + ]: 441 : && !Configuration::isBuiltWithCryptominisat())
[ - + ]
285 : : {
286 : 0 : std::stringstream ss;
287 : : ss << "option `" << flag
288 : : << "' requires a CryptoMiniSat build of cvc5; this binary was not built "
289 : 0 : "with CryptoMiniSat support";
290 : 0 : throw OptionException(ss.str());
291 : 0 : }
292 : :
293 [ + + ][ + - ]: 441 : if (m == BvSatSolverMode::KISSAT && !Configuration::isBuiltWithKissat())
[ + + ]
294 : : {
295 : 90 : std::stringstream ss;
296 : : ss << "option `" << flag
297 : : << "' requires a Kissat build of cvc5; this binary was not built with "
298 : 90 : "Kissat support";
299 : 90 : throw OptionException(ss.str());
300 : 90 : }
301 : :
302 [ - + ]: 351 : if (d_options->bv.bvSolver != options::BVSolver::BITBLAST
303 [ - - ][ - - ]: 0 : && (m == BvSatSolverMode::CRYPTOMINISAT || m == BvSatSolverMode::CADICAL
304 [ - - ]: 0 : || m == BvSatSolverMode::KISSAT))
305 : : {
306 [ - - ]: 0 : if (d_options->bv.bitblastMode == options::BitblastMode::LAZY
307 [ - - ]: 0 : && d_options->bv.bitblastModeWasSetByUser)
308 : : {
309 : 0 : std::stringstream ss;
310 : 0 : ss << m << " does not support lazy bit-blasting." << std::endl
311 : 0 : << "Try --bv-sat-solver=minisat";
312 : 0 : throw OptionException(ss.str());
313 : 0 : }
314 [ - - ]: 0 : if (!d_options->bv.bitvectorToBoolWasSetByUser)
315 : : {
316 : 0 : d_options->write_bv().bitvectorToBool = true;
317 : : }
318 : : }
319 : 351 : }
320 : :
321 : : namespace {
322 : 106125 : void print_config(std::ostream& out, const char* str, const std::string& config)
323 : : {
324 : 106125 : std::string s(str);
325 : 106125 : constexpr unsigned sz = 14;
326 [ + - ]: 106125 : if (s.size() < sz) s.resize(sz, ' ');
327 : 106125 : out << s << ": " << config << std::endl;
328 : 106125 : }
329 : :
330 : 93390 : void print_config_cond(std::ostream& out, const char* str, bool cond = false)
331 : : {
332 [ + + ]: 93390 : print_config(out, str, cond ? "yes" : "no");
333 : 93390 : }
334 : : } // namespace
335 : :
336 : 4279 : void OptionsHandler::showConfiguration(CVC5_UNUSED const std::string& flag,
337 : : const bool value) const
338 : : {
339 [ + + ]: 4279 : if (!value) return;
340 : 4245 : std::ostream& o = d_options->base.out;
341 : 4245 : print_config(o, "package", Configuration::getPackageName());
342 : 4245 : print_config(o, "version", Configuration::getVersionString());
343 [ + - ]: 4245 : if (Configuration::isGitBuild())
344 : : {
345 : 4245 : print_config(o, "scm", Configuration::getGitInfo());
346 : : }
347 : : else
348 : : {
349 : 0 : print_config_cond(o, "scm", false);
350 : : }
351 : :
352 : 4245 : o << std::endl;
353 : :
354 : 4245 : print_config_cond(o, "safe-mode", Configuration::isSafeBuild());
355 : 4245 : print_config_cond(o, "stable-mode", Configuration::isStableBuild());
356 : 4245 : print_config_cond(o, "debug code", Configuration::isDebugBuild());
357 : 4245 : print_config_cond(o, "statistics", configuration::isStatisticsBuild());
358 : 4245 : print_config_cond(o, "tracing", Configuration::isTracingBuild());
359 : 4245 : print_config_cond(o, "muzzled", Configuration::isMuzzledBuild());
360 : 4245 : print_config_cond(o, "assertions", Configuration::isAssertionBuild());
361 : 4245 : print_config_cond(o, "coverage", Configuration::isCoverageBuild());
362 : 4245 : print_config_cond(o, "profiling", Configuration::isProfilingBuild());
363 : 4245 : print_config_cond(o, "asan", Configuration::isAsanBuild());
364 : 4245 : print_config_cond(o, "ubsan", Configuration::isUbsanBuild());
365 : 4245 : print_config_cond(o, "tsan", Configuration::isTsanBuild());
366 : 4245 : print_config_cond(o, "competition", Configuration::isCompetitionBuild());
367 : 4245 : print_config_cond(o, "portfolio", Configuration::isBuiltWithPortfolio());
368 : :
369 : 4245 : o << std::endl;
370 : :
371 : 4245 : print_config_cond(o, "cln", Configuration::isBuiltWithCln());
372 : 4245 : print_config_cond(o, "glpk", Configuration::isBuiltWithGlpk());
373 : 4245 : print_config_cond(
374 : 4245 : o, "cryptominisat", Configuration::isBuiltWithCryptominisat());
375 : 4245 : print_config_cond(o, "gmp", Configuration::isBuiltWithGmp());
376 : 4245 : print_config_cond(o, "kissat", Configuration::isBuiltWithKissat());
377 : 4245 : print_config_cond(o, "poly", Configuration::isBuiltWithPoly());
378 : 4245 : print_config_cond(o, "cocoa", Configuration::isBuiltWithCoCoA());
379 : 4245 : print_config_cond(o, "editline", Configuration::isBuiltWithEditline());
380 : : }
381 : :
382 : 167 : void OptionsHandler::showCopyright(CVC5_UNUSED const std::string& flag,
383 : : const bool value) const
384 : : {
385 [ + + ]: 167 : if (!value) return;
386 : 83 : d_options->base.out << Configuration::copyright() << std::endl;
387 : : }
388 : :
389 : 6 : void OptionsHandler::showVersion(CVC5_UNUSED const std::string& flag,
390 : : const bool value) const
391 : : {
392 [ + + ]: 6 : if (!value) return;
393 : 4 : d_options->base.out << Configuration::aboutAndCopyright() << std::endl;
394 : : }
395 : :
396 : 66 : void OptionsHandler::showTraceTags(CVC5_UNUSED const std::string& flag,
397 : : const bool value) const
398 : : {
399 [ + + ]: 66 : if (!value) return;
400 [ - + ]: 33 : if (!Configuration::isTracingBuild())
401 : : {
402 : 0 : throw OptionException("trace tags not available in non-tracing build");
403 : : }
404 : 33 : printTags(d_options->base.out, Configuration::getTraceTags());
405 : : }
406 : :
407 : 124 : void OptionsHandler::strictParsing(CVC5_UNUSED const std::string& flag,
408 : : const bool value) const
409 : : {
410 [ + + ]: 124 : if (value)
411 : : {
412 : 66 : d_options->write_parser().parsingMode = options::ParsingMode::STRICT;
413 : : }
414 [ + + ]: 58 : else if (d_options->parser.parsingMode == options::ParsingMode::STRICT)
415 : : {
416 : 30 : d_options->write_parser().parsingMode = options::ParsingMode::DEFAULT;
417 : : }
418 : 124 : }
419 : :
420 : : } // namespace options
421 : : } // namespace cvc5::internal
|
