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