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 [ + + ]: 50028 : for (const auto& t : tags)
50 : : {
51 : 49995 : 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 : 78094 : 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 : 31260 : Language OptionsHandler::stringToLanguage(const std::string& flag,
115 : : const std::string& optarg) const
116 : : {
117 [ - + ]: 31260 : 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 : : smt2-tptp custom SMT-LIB v2.6-derived output format for tptpmodels
131 : : ast internal format (simple syntax trees)
132 : 0 : )FOOBAR" << std::endl;
133 : 0 : throw OptionException("help is not a valid language");
134 : : }
135 : :
136 : : try
137 : : {
138 : 31260 : return language::toLanguage(optarg);
139 : : }
140 [ - + ]: 247 : catch (OptionException& oe)
141 : : {
142 : 741 : throw OptionException("Error in " + flag + ": " + oe.getMessage()
143 : 988 : + "\nTry --lang help");
144 : 247 : }
145 : :
146 : : Unreachable();
147 : : }
148 : :
149 : 24661 : void OptionsHandler::setInputLanguage(const std::string& flag,
150 : : const Language lang) const
151 : : {
152 [ + - ][ - + ]: 24661 : if (lang == Language::LANG_AST || lang == Language::LANG_SMTLIB_V2_6_TPTP)
153 : : {
154 : 0 : throw OptionException("This language is not allowed for " + flag);
155 : : }
156 [ + + ]: 24661 : if (!d_options->printer.outputLanguageWasSetByUser)
157 : : {
158 : 20553 : d_options->write_printer().outputLanguage = lang;
159 : 20553 : ioutils::setDefaultOutputLanguage(lang);
160 : : }
161 : 24661 : }
162 : :
163 : 646 : void OptionsHandler::setVerbosity(CVC5_UNUSED const std::string& flag,
164 : : const int value) const
165 : : {
166 [ - + ]: 646 : if (Configuration::isMuzzledBuild())
167 : : {
168 : 0 : TraceChannel.setStream(&cvc5::internal::null_os);
169 : 0 : WarningChannel.setStream(&cvc5::internal::null_os);
170 : : }
171 : : else
172 : : {
173 [ + + ]: 646 : if (value < 0)
174 : : {
175 : 634 : WarningChannel.setStream(&cvc5::internal::null_os);
176 : : }
177 : : else
178 : : {
179 : 12 : WarningChannel.setStream(&std::cerr);
180 : : }
181 : : }
182 : 646 : }
183 : :
184 : 633 : void OptionsHandler::decreaseVerbosity(CVC5_UNUSED const std::string& flag,
185 : : CVC5_UNUSED bool value)
186 : : {
187 : 633 : d_options->write_base().verbosity -= 1;
188 : 633 : setVerbosity(flag, d_options->base.verbosity);
189 : 633 : }
190 : :
191 : 3 : void OptionsHandler::increaseVerbosity(CVC5_UNUSED const std::string& flag,
192 : : CVC5_UNUSED bool value)
193 : : {
194 : 3 : d_options->write_base().verbosity += 1;
195 : 3 : setVerbosity(flag, d_options->base.verbosity);
196 : 3 : }
197 : :
198 : 63 : void OptionsHandler::setStats(CVC5_UNUSED const std::string& flag,
199 : : const bool value) const
200 : : {
201 : : #ifndef CVC5_STATISTICS_ON
202 : : if (value)
203 : : {
204 : : std::stringstream ss;
205 : : ss << "option `" << flag
206 : : << "' requires a statistics-enabled build of cvc5; this binary was not "
207 : : "built with statistics support";
208 : : throw OptionException(ss.str());
209 : : }
210 : : #endif /* CVC5_STATISTICS_ON */
211 [ + + ]: 63 : if (!value)
212 : : {
213 : 33 : d_options->write_base().statisticsAll = false;
214 : 33 : d_options->write_base().statisticsEveryQuery = false;
215 : 33 : d_options->write_base().statisticsInternal = false;
216 : : }
217 : 63 : }
218 : :
219 : 184 : void OptionsHandler::setStatsDetail(CVC5_UNUSED const std::string& flag,
220 : : const bool value) const
221 : : {
222 : : #ifndef CVC5_STATISTICS_ON
223 : : if (value)
224 : : {
225 : : std::stringstream ss;
226 : : ss << "option `" << flag
227 : : << "' requires a statistics-enabled build of cvc5; this binary was not "
228 : : "built with statistics support";
229 : : throw OptionException(ss.str());
230 : : }
231 : : #endif /* CVC5_STATISTICS_ON */
232 [ + + ]: 184 : if (value)
233 : : {
234 : 92 : d_options->write_base().statistics = true;
235 : : }
236 : 184 : }
237 : :
238 : 11 : void OptionsHandler::enableTraceTag(CVC5_UNUSED const std::string& flag,
239 : : const std::string& optarg) const
240 : : {
241 [ - + ]: 11 : if (!Configuration::isTracingBuild())
242 : : {
243 : 0 : throw OptionException("trace tags not available in non-tracing builds");
244 : : }
245 : 11 : const auto tags = selectTags(Configuration::getTraceTags(), optarg);
246 [ + + ]: 11 : if (tags.empty())
247 : : {
248 [ - + ]: 8 : if (optarg == "help")
249 : : {
250 : 0 : d_options->write_driver().showTraceTags = true;
251 : 0 : showTraceTags("", true);
252 : 0 : return;
253 : : }
254 : :
255 : 8 : throw OptionException(
256 : 16 : std::string("no trace tag matching ") + optarg
257 : 32 : + std::string(" was found.")
258 : 32 : + suggestTags(Configuration::getTraceTags(), optarg, {}));
259 : : }
260 [ + + ]: 6 : for (const auto& tag : tags)
261 : : {
262 : 3 : TraceChannel.on(tag);
263 : : }
264 [ + - ]: 11 : }
265 : :
266 : 4418 : void OptionsHandler::enableOutputTag(CVC5_UNUSED const std::string& flag,
267 : : const OutputTag optarg) const
268 : : {
269 : 4418 : const size_t tagid = static_cast<size_t>(optarg);
270 [ - + ][ - + ]: 4418 : Assert(d_options->base.outputTagHolder.size() > tagid)
[ - - ]
271 : 0 : << "Output tag is larger than the bitset that holds it.";
272 : 4418 : d_options->write_base().outputTagHolder.set(tagid);
273 : 4418 : }
274 : :
275 : 35 : void OptionsHandler::setResourceWeight(CVC5_UNUSED const std::string& flag,
276 : : const std::string& optarg) const
277 : : {
278 : 35 : d_options->write_base().resourceWeightHolder.emplace_back(optarg);
279 : 35 : }
280 : :
281 : 300 : void OptionsHandler::checkBvSatSolver(const std::string& flag,
282 : : const BvSatSolverMode m) const
283 : : {
284 : 300 : if (m == BvSatSolverMode::CRYPTOMINISAT
285 [ + + ][ - + ]: 300 : && !Configuration::isBuiltWithCryptominisat())
[ - + ]
286 : : {
287 : 0 : std::stringstream ss;
288 : : ss << "option `" << flag
289 : : << "' requires a CryptoMiniSat build of cvc5; this binary was not built "
290 : 0 : "with CryptoMiniSat support";
291 : 0 : throw OptionException(ss.str());
292 : 0 : }
293 : :
294 [ + + ][ + - ]: 300 : if (m == BvSatSolverMode::KISSAT && !Configuration::isBuiltWithKissat())
[ + + ]
295 : : {
296 : 90 : std::stringstream ss;
297 : : ss << "option `" << flag
298 : : << "' requires a Kissat build of cvc5; this binary was not built with "
299 : 90 : "Kissat support";
300 : 90 : throw OptionException(ss.str());
301 : 90 : }
302 : :
303 [ - + ]: 210 : if (d_options->bv.bvSolver != options::BVSolver::BITBLAST
304 [ - - ][ - - ]: 0 : && (m == BvSatSolverMode::CRYPTOMINISAT || m == BvSatSolverMode::CADICAL
305 [ - - ]: 0 : || m == BvSatSolverMode::KISSAT))
306 : : {
307 [ - - ]: 0 : if (d_options->bv.bitblastMode == options::BitblastMode::LAZY
308 [ - - ]: 0 : && d_options->bv.bitblastModeWasSetByUser)
309 : : {
310 : 0 : std::stringstream ss;
311 : 0 : ss << m << " does not support lazy bit-blasting." << std::endl
312 : 0 : << "Try --bv-sat-solver=minisat";
313 : 0 : throw OptionException(ss.str());
314 : 0 : }
315 [ - - ]: 0 : if (!d_options->bv.bitvectorToBoolWasSetByUser)
316 : : {
317 : 0 : d_options->write_bv().bitvectorToBool = true;
318 : : }
319 : : }
320 : 210 : }
321 : :
322 : : namespace {
323 : 111826 : void print_config(std::ostream& out, const char* str, const std::string& config)
324 : : {
325 : 111826 : std::string s(str);
326 : 111826 : constexpr unsigned sz = 14;
327 [ + - ]: 111826 : if (s.size() < sz) s.resize(sz, ' ');
328 : 111826 : out << s << ": " << config << std::endl;
329 : 111826 : }
330 : :
331 : 98923 : void print_config_cond(std::ostream& out, const char* str, bool cond = false)
332 : : {
333 [ + + ]: 98923 : print_config(out, str, cond ? "yes" : "no");
334 : 98923 : }
335 : : } // namespace
336 : :
337 : 4335 : void OptionsHandler::showConfiguration(CVC5_UNUSED const std::string& flag,
338 : : const bool value) const
339 : : {
340 [ + + ]: 4335 : if (!value) return;
341 : 4301 : std::ostream& o = d_options->base.out;
342 : 4301 : print_config(o, "package", Configuration::getPackageName());
343 : 4301 : print_config(o, "version", Configuration::getVersionString());
344 [ + - ]: 4301 : if (Configuration::isGitBuild())
345 : : {
346 : 4301 : print_config(o, "scm", Configuration::getGitInfo());
347 : : }
348 : : else
349 : : {
350 : 0 : print_config_cond(o, "scm", false);
351 : : }
352 : :
353 : 4301 : o << std::endl;
354 : :
355 : 4301 : print_config_cond(o, "safe-mode", Configuration::isSafeBuild());
356 : 4301 : print_config_cond(o, "stable-mode", Configuration::isStableBuild());
357 : 4301 : print_config_cond(o, "debug code", Configuration::isDebugBuild());
358 : 4301 : print_config_cond(o, "statistics", configuration::isStatisticsBuild());
359 : 4301 : print_config_cond(o, "tracing", Configuration::isTracingBuild());
360 : 4301 : print_config_cond(o, "muzzled", Configuration::isMuzzledBuild());
361 : 4301 : print_config_cond(o, "assertions", Configuration::isAssertionBuild());
362 : 4301 : print_config_cond(o, "coverage", Configuration::isCoverageBuild());
363 : 4301 : print_config_cond(o, "profiling", Configuration::isProfilingBuild());
364 : 4301 : print_config_cond(o, "asan", Configuration::isAsanBuild());
365 : 4301 : print_config_cond(o, "ubsan", Configuration::isUbsanBuild());
366 : 4301 : print_config_cond(o, "tsan", Configuration::isTsanBuild());
367 : 4301 : print_config_cond(o, "competition", Configuration::isCompetitionBuild());
368 : 4301 : print_config_cond(o, "portfolio", Configuration::isBuiltWithPortfolio());
369 : :
370 : 4301 : o << std::endl;
371 : :
372 : 4301 : print_config_cond(o, "cln", Configuration::isBuiltWithCln());
373 : 4301 : print_config_cond(o, "glpk", Configuration::isBuiltWithGlpk());
374 : 4301 : print_config_cond(
375 : 4301 : o, "cryptominisat", Configuration::isBuiltWithCryptominisat());
376 : 4301 : print_config_cond(o, "gmp", Configuration::isBuiltWithGmp());
377 : 4301 : print_config_cond(o, "kissat", Configuration::isBuiltWithKissat());
378 : 4301 : print_config_cond(o, "poly", Configuration::isBuiltWithPoly());
379 : 4301 : print_config_cond(o, "cocoa", Configuration::isBuiltWithCoCoA());
380 : 4301 : print_config_cond(o, "normaliz", Configuration::isBuiltWithNormaliz());
381 : 4301 : print_config_cond(o, "editline", Configuration::isBuiltWithEditline());
382 : : }
383 : :
384 : 167 : void OptionsHandler::showCopyright(CVC5_UNUSED const std::string& flag,
385 : : const bool value) const
386 : : {
387 [ + + ]: 167 : if (!value) return;
388 : 83 : d_options->base.out << Configuration::copyright() << std::endl;
389 : : }
390 : :
391 : 6 : void OptionsHandler::showVersion(CVC5_UNUSED const std::string& flag,
392 : : const bool value) const
393 : : {
394 [ + + ]: 6 : if (!value) return;
395 : 4 : d_options->base.out << Configuration::aboutAndCopyright() << std::endl;
396 : : }
397 : :
398 : 66 : void OptionsHandler::showTraceTags(CVC5_UNUSED const std::string& flag,
399 : : const bool value) const
400 : : {
401 [ + + ]: 66 : if (!value) return;
402 [ - + ]: 33 : if (!Configuration::isTracingBuild())
403 : : {
404 : 0 : throw OptionException("trace tags not available in non-tracing build");
405 : : }
406 : 33 : printTags(d_options->base.out, Configuration::getTraceTags());
407 : : }
408 : :
409 : 124 : void OptionsHandler::strictParsing(CVC5_UNUSED const std::string& flag,
410 : : const bool value) const
411 : : {
412 [ + + ]: 124 : if (value)
413 : : {
414 : 66 : d_options->write_parser().parsingMode = options::ParsingMode::STRICT;
415 : : }
416 [ + + ]: 58 : else if (d_options->parser.parsingMode == options::ParsingMode::STRICT)
417 : : {
418 : 30 : d_options->write_parser().parsingMode = options::ParsingMode::DEFAULT;
419 : : }
420 : 124 : }
421 : :
422 : : } // namespace options
423 : : } // namespace cvc5::internal
|
