GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/options/options_handler.cpp Lines: 120 281 42.7 %
Date: 2021-03-22 Branches: 155 662 23.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file options_handler.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Tim King, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Interface for custom handlers and predicates options.
13
 **
14
 ** Interface for custom handlers and predicates options.
15
 **/
16
17
#include "options/options_handler.h"
18
19
#include <ostream>
20
#include <string>
21
#include <cerrno>
22
23
#include "cvc4autoconfig.h"
24
25
#include "base/check.h"
26
#include "base/configuration.h"
27
#include "base/configuration_private.h"
28
#include "base/exception.h"
29
#include "base/modal_exception.h"
30
#include "base/output.h"
31
#include "lib/strtok_r.h"
32
#include "options/base_options.h"
33
#include "options/bv_options.h"
34
#include "options/decision_options.h"
35
#include "options/didyoumean.h"
36
#include "options/language.h"
37
#include "options/option_exception.h"
38
#include "options/smt_options.h"
39
#include "options/theory_options.h"
40
41
namespace CVC4 {
42
namespace options {
43
44
// helper functions
45
namespace {
46
47
void throwLazyBBUnsupported(options::SatSolverMode m)
48
{
49
  std::string sat_solver;
50
  if (m == options::SatSolverMode::CADICAL)
51
  {
52
    sat_solver = "CaDiCaL";
53
  }
54
  else if (m == options::SatSolverMode::KISSAT)
55
  {
56
    sat_solver = "Kissat";
57
  }
58
  else
59
  {
60
    Assert(m == options::SatSolverMode::CRYPTOMINISAT);
61
    sat_solver = "CryptoMiniSat";
62
  }
63
  std::string indent(25, ' ');
64
  throw OptionException(sat_solver + " does not support lazy bit-blasting.\n"
65
                        + indent + "Try --bv-sat-solver=minisat");
66
}
67
68
}  // namespace
69
70
27316
OptionsHandler::OptionsHandler(Options* options) : d_options(options) { }
71
72
6
unsigned long OptionsHandler::limitHandler(std::string option,
73
                                           std::string optarg)
74
{
75
  unsigned long ms;
76
12
  std::istringstream convert(optarg);
77
6
  if (!(convert >> ms))
78
  {
79
    throw OptionException("option `" + option
80
                          + "` requires a number as an argument");
81
  }
82
12
  return ms;
83
}
84
// theory/quantifiers/options_handlers.h
85
86
3
void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode)
87
{
88
3
  if (mode == InstWhenMode::PRE_FULL)
89
  {
90
    throw OptionException(std::string("Mode pre-full for ") + option
91
                          + " is not supported in this release.");
92
  }
93
3
}
94
95
// theory/bv/options_handlers.h
96
void OptionsHandler::abcEnabledBuild(std::string option, bool value)
97
{
98
#ifndef CVC4_USE_ABC
99
  if(value) {
100
    std::stringstream ss;
101
    ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
102
    throw OptionException(ss.str());
103
  }
104
#endif /* CVC4_USE_ABC */
105
}
106
107
void OptionsHandler::abcEnabledBuild(std::string option, std::string value)
108
{
109
#ifndef CVC4_USE_ABC
110
  if(!value.empty()) {
111
    std::stringstream ss;
112
    ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
113
    throw OptionException(ss.str());
114
  }
115
#endif /* CVC4_USE_ABC */
116
}
117
118
12
void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m)
119
{
120
12
  if (m == SatSolverMode::CRYPTOMINISAT
121
12
      && !Configuration::isBuiltWithCryptominisat())
122
  {
123
    std::stringstream ss;
124
    ss << "option `" << option
125
       << "' requires a CryptoMiniSat build of CVC4; this binary was not built "
126
          "with CryptoMiniSat support";
127
    throw OptionException(ss.str());
128
  }
129
130
12
  if (m == SatSolverMode::CADICAL && !Configuration::isBuiltWithCadical())
131
  {
132
    std::stringstream ss;
133
    ss << "option `" << option
134
       << "' requires a CaDiCaL build of CVC4; this binary was not built with "
135
          "CaDiCaL support";
136
    throw OptionException(ss.str());
137
  }
138
139
12
  if (m == SatSolverMode::KISSAT && !Configuration::isBuiltWithKissat())
140
  {
141
    std::stringstream ss;
142
    ss << "option `" << option
143
       << "' requires a Kissat build of CVC4; this binary was not built with "
144
          "Kissat support";
145
    throw OptionException(ss.str());
146
  }
147
148
24
  if (options::bvSolver() != options::BVSolver::BITBLAST
149
22
      && (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL
150
2
          || m == SatSolverMode::KISSAT))
151
  {
152
20
    if (options::bitblastMode() == options::BitblastMode::LAZY
153
10
        && options::bitblastMode.wasSetByUser())
154
    {
155
      throwLazyBBUnsupported(m);
156
    }
157
10
    if (!options::bitvectorToBool.wasSetByUser())
158
    {
159
10
      options::bitvectorToBool.set(true);
160
    }
161
  }
162
12
}
163
164
void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m)
165
{
166
  if (m == options::BitblastMode::LAZY)
167
  {
168
    if (!options::bitvectorPropagate.wasSetByUser())
169
    {
170
      options::bitvectorPropagate.set(true);
171
    }
172
    if (!options::bitvectorEqualitySolver.wasSetByUser())
173
    {
174
      options::bitvectorEqualitySolver.set(true);
175
    }
176
177
    if (!options::bitvectorInequalitySolver.wasSetByUser())
178
    {
179
      options::bitvectorInequalitySolver.set(true);
180
    }
181
    if (!options::bitvectorAlgebraicSolver.wasSetByUser())
182
    {
183
      options::bitvectorAlgebraicSolver.set(true);
184
    }
185
    if (options::bvSatSolver() != options::SatSolverMode::MINISAT)
186
    {
187
      throwLazyBBUnsupported(options::bvSatSolver());
188
    }
189
  }
190
  else if (m == BitblastMode::EAGER)
191
  {
192
    if (!options::bitvectorToBool.wasSetByUser())
193
    {
194
      options::bitvectorToBool.set(true);
195
    }
196
  }
197
}
198
199
void OptionsHandler::setBitblastAig(std::string option, bool arg)
200
{
201
  if(arg) {
202
    if(options::bitblastMode.wasSetByUser()) {
203
      if (options::bitblastMode() != options::BitblastMode::EAGER)
204
      {
205
        throw OptionException("bitblast-aig must be used with eager bitblaster");
206
      }
207
    } else {
208
      options::BitblastMode mode = stringToBitblastMode("", "eager");
209
      options::bitblastMode.set(mode);
210
    }
211
    if(!options::bitvectorAigSimplifications.wasSetByUser()) {
212
      options::bitvectorAigSimplifications.set("balance;drw");
213
    }
214
  }
215
}
216
217
// printer/options_handlers.h
218
8892
const std::string OptionsHandler::s_instFormatHelp = "\
219
Inst format modes currently supported by the --inst-format option:\n\
220
\n\
221
default \n\
222
+ Print instantiations as a list in the output language format.\n\
223
\n\
224
szs\n\
225
+ Print instantiations as SZS compliant proof.\n\
226
";
227
228
InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option,
229
                                                      std::string optarg)
230
{
231
  if(optarg == "default") {
232
    return InstFormatMode::DEFAULT;
233
  } else if(optarg == "szs") {
234
    return InstFormatMode::SZS;
235
  } else if(optarg == "help") {
236
    puts(s_instFormatHelp.c_str());
237
    exit(1);
238
  } else {
239
    throw OptionException(std::string("unknown option for --inst-format: `") +
240
                          optarg + "'.  Try --inst-format help.");
241
  }
242
}
243
244
// decision/options_handlers.h
245
77
void OptionsHandler::setDecisionModeStopOnly(std::string option, DecisionMode m)
246
{
247
77
  options::decisionStopOnly.set(m == DecisionMode::RELEVANCY);
248
77
}
249
250
8
void OptionsHandler::setProduceAssertions(std::string option, bool value)
251
{
252
8
  options::produceAssertions.set(value);
253
20
  options::interactiveMode.set(value);
254
8
}
255
256
26
void OptionsHandler::proofEnabledBuild(std::string option, bool value)
257
{
258
#ifdef CVC4_PROOF
259
50
  if (value && options::bitblastMode() == options::BitblastMode::EAGER
260
      && options::bvSatSolver() != options::SatSolverMode::MINISAT
261
26
      && options::bvSatSolver() != options::SatSolverMode::CRYPTOMINISAT)
262
  {
263
    throw OptionException(
264
        "Eager BV proofs only supported when MiniSat or CryptoMiniSat is used");
265
  }
266
#else
267
  if(value) {
268
    std::stringstream ss;
269
    ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support";
270
    throw OptionException(ss.str());
271
  }
272
#endif /* CVC4_PROOF */
273
26
}
274
275
void OptionsHandler::LFSCEnabledBuild(std::string option, bool value) {
276
#ifndef CVC4_USE_LFSC
277
  if (value) {
278
    std::stringstream ss;
279
    ss << "option `" << option << "' requires a build of CVC4 with integrated "
280
                                  "LFSC; this binary was not built with LFSC";
281
    throw OptionException(ss.str());
282
  }
283
#endif /* CVC4_USE_LFSC */
284
}
285
286
void OptionsHandler::statsEnabledBuild(std::string option, bool value)
287
{
288
#ifndef CVC4_STATISTICS_ON
289
  if(value) {
290
    std::stringstream ss;
291
    ss << "option `" << option << "' requires a statistics-enabled build of CVC4; this binary was not built with statistics support";
292
    throw OptionException(ss.str());
293
  }
294
#endif /* CVC4_STATISTICS_ON */
295
}
296
297
void OptionsHandler::threadN(std::string option) {
298
  throw OptionException(option + " is not a real option by itself.  Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\"");
299
}
300
301
// expr/options_handlers.h
302
void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) {
303
  if(depth < -1) {
304
    throw OptionException("--expr-depth requires a positive argument, or -1.");
305
  }
306
}
307
308
1
void OptionsHandler::setDefaultDagThreshPredicate(std::string option, int dag) {
309
1
  if(dag < 0) {
310
    throw OptionException("--dag-thresh requires a nonnegative argument.");
311
  }
312
1
}
313
314
// main/options_handlers.h
315
316
68544
static void print_config (const char * str, std::string config) {
317
137088
  std::string s(str);
318
68544
  unsigned sz = 14;
319
68544
  if (s.size() < sz) s.resize(sz, ' ');
320
68544
  std::cout << s << ": " << config << std::endl;
321
68544
}
322
323
61200
static void print_config_cond (const char * str, bool cond = false) {
324
61200
  print_config(str, cond ? "yes" : "no");
325
61200
}
326
327
void OptionsHandler::copyright(std::string option) {
328
  std::cout << Configuration::copyright() << std::endl;
329
  exit(0);
330
}
331
332
2448
void OptionsHandler::showConfiguration(std::string option) {
333
2448
  std::cout << Configuration::about() << std::endl;
334
335
2448
  print_config ("version", Configuration::getVersionString());
336
337
2448
  if(Configuration::isGitBuild()) {
338
2448
    const char* branchName = Configuration::getGitBranchName();
339
2448
    if(*branchName == '\0')  { branchName = "-"; }
340
4896
    std::stringstream ss;
341
    ss << "git ["
342
       << branchName << " "
343
4896
       << std::string(Configuration::getGitCommit()).substr(0, 8)
344
2448
       << (Configuration::hasGitModifications() ? " (with modifications)" : "")
345
7344
       << "]";
346
2448
    print_config("scm", ss.str());
347
  } else {
348
    print_config_cond("scm", false);
349
  }
350
351
2448
  std::cout << std::endl;
352
353
2448
  std::stringstream ss;
354
2448
  ss << Configuration::getVersionMajor() << "."
355
2448
     << Configuration::getVersionMinor() << "."
356
2448
     << Configuration::getVersionRelease();
357
2448
  print_config("library", ss.str());
358
359
2448
  std::cout << std::endl;
360
361
2448
  print_config_cond("debug code", Configuration::isDebugBuild());
362
2448
  print_config_cond("statistics", Configuration::isStatisticsBuild());
363
2448
  print_config_cond("tracing", Configuration::isTracingBuild());
364
2448
  print_config_cond("dumping", Configuration::isDumpingBuild());
365
2448
  print_config_cond("muzzled", Configuration::isMuzzledBuild());
366
2448
  print_config_cond("assertions", Configuration::isAssertionBuild());
367
2448
  print_config_cond("proof", Configuration::isProofBuild());
368
2448
  print_config_cond("coverage", Configuration::isCoverageBuild());
369
2448
  print_config_cond("profiling", Configuration::isProfilingBuild());
370
2448
  print_config_cond("asan", Configuration::isAsanBuild());
371
2448
  print_config_cond("ubsan", Configuration::isUbsanBuild());
372
2448
  print_config_cond("tsan", Configuration::isTsanBuild());
373
2448
  print_config_cond("competition", Configuration::isCompetitionBuild());
374
375
2448
  std::cout << std::endl;
376
377
2448
  print_config_cond("abc", Configuration::isBuiltWithAbc());
378
2448
  print_config_cond("cln", Configuration::isBuiltWithCln());
379
2448
  print_config_cond("glpk", Configuration::isBuiltWithGlpk());
380
2448
  print_config_cond("cadical", Configuration::isBuiltWithCadical());
381
2448
  print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
382
2448
  print_config_cond("drat2er", Configuration::isBuiltWithDrat2Er());
383
2448
  print_config_cond("gmp", Configuration::isBuiltWithGmp());
384
2448
  print_config_cond("kissat", Configuration::isBuiltWithKissat());
385
2448
  print_config_cond("lfsc", Configuration::isBuiltWithLfsc());
386
2448
  print_config_cond("poly", Configuration::isBuiltWithPoly());
387
2448
  print_config_cond("editline", Configuration::isBuiltWithEditline());
388
2448
  print_config_cond("symfpu", Configuration::isBuiltWithSymFPU());
389
390
2448
  exit(0);
391
}
392
393
static void printTags(unsigned ntags, char const* const* tags)
394
{
395
  std::cout << "available tags:";
396
  for (unsigned i = 0; i < ntags; ++ i)
397
  {
398
    std::cout << "  " << tags[i] << std::endl;
399
  }
400
  std::cout << std::endl;
401
}
402
403
void OptionsHandler::showDebugTags(std::string option)
404
{
405
  if (!Configuration::isDebugBuild())
406
  {
407
    throw OptionException("debug tags not available in non-debug builds");
408
  }
409
  else if (!Configuration::isTracingBuild())
410
  {
411
    throw OptionException("debug tags not available in non-tracing builds");
412
  }
413
  printTags(Configuration::getNumDebugTags(),Configuration::getDebugTags());
414
  exit(0);
415
}
416
417
void OptionsHandler::showTraceTags(std::string option)
418
{
419
  if (!Configuration::isTracingBuild())
420
  {
421
    throw OptionException("trace tags not available in non-tracing build");
422
  }
423
  printTags(Configuration::getNumTraceTags(), Configuration::getTraceTags());
424
  exit(0);
425
}
426
427
static std::string suggestTags(char const* const* validTags,
428
                               std::string inputTag,
429
                               char const* const* additionalTags)
430
{
431
  DidYouMean didYouMean;
432
433
  const char* opt;
434
  for (size_t i = 0; (opt = validTags[i]) != nullptr; ++i)
435
  {
436
    didYouMean.addWord(validTags[i]);
437
  }
438
  if (additionalTags != nullptr)
439
  {
440
    for (size_t i = 0; (opt = additionalTags[i]) != nullptr; ++i)
441
    {
442
      didYouMean.addWord(additionalTags[i]);
443
    }
444
  }
445
446
  return didYouMean.getMatchAsString(inputTag);
447
}
448
449
void OptionsHandler::enableTraceTag(std::string option, std::string optarg)
450
{
451
  if(!Configuration::isTracingBuild())
452
  {
453
    throw OptionException("trace tags not available in non-tracing builds");
454
  }
455
  else if(!Configuration::isTraceTag(optarg.c_str()))
456
  {
457
    if (optarg == "help")
458
    {
459
      printTags(
460
          Configuration::getNumTraceTags(), Configuration::getTraceTags());
461
      exit(0);
462
    }
463
464
    throw OptionException(
465
        std::string("trace tag ") + optarg + std::string(" not available.")
466
        + suggestTags(Configuration::getTraceTags(), optarg, nullptr));
467
  }
468
  Trace.on(optarg);
469
}
470
471
void OptionsHandler::enableDebugTag(std::string option, std::string optarg)
472
{
473
  if (!Configuration::isDebugBuild())
474
  {
475
    throw OptionException("debug tags not available in non-debug builds");
476
  }
477
  else if (!Configuration::isTracingBuild())
478
  {
479
    throw OptionException("debug tags not available in non-tracing builds");
480
  }
481
482
  if (!Configuration::isDebugTag(optarg.c_str())
483
      && !Configuration::isTraceTag(optarg.c_str()))
484
  {
485
    if (optarg == "help")
486
    {
487
      printTags(
488
          Configuration::getNumDebugTags(), Configuration::getDebugTags());
489
      exit(0);
490
    }
491
492
    throw OptionException(std::string("debug tag ") + optarg
493
                          + std::string(" not available.")
494
                          + suggestTags(Configuration::getDebugTags(),
495
                                        optarg,
496
                                        Configuration::getTraceTags()));
497
  }
498
  Debug.on(optarg);
499
  Trace.on(optarg);
500
}
501
502
86
OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option,
503
                                                      std::string optarg)
504
{
505
86
  if(optarg == "help") {
506
5456
    options::languageHelp.set(true);
507
    return language::output::LANG_AUTO;
508
  }
509
510
  try {
511
86
    return language::toOutputLanguage(optarg);
512
  } catch(OptionException& oe) {
513
    throw OptionException("Error in " + option + ": " + oe.getMessage() +
514
                          "\nTry --output-language help");
515
  }
516
517
  Unreachable();
518
}
519
520
653
InputLanguage OptionsHandler::stringToInputLanguage(std::string option,
521
                                                    std::string optarg)
522
{
523
653
  if(optarg == "help") {
524
    options::languageHelp.set(true);
525
    return language::input::LANG_AUTO;
526
  }
527
528
  try {
529
653
    return language::toInputLanguage(optarg);
530
  } catch(OptionException& oe) {
531
    throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --lang help");
532
  }
533
534
  Unreachable();
535
}
536
537
/* options/base_options_handlers.h */
538
181
void OptionsHandler::setVerbosity(std::string option, int value)
539
{
540
181
  if(Configuration::isMuzzledBuild()) {
541
    DebugChannel.setStream(&CVC4::null_os);
542
    TraceChannel.setStream(&CVC4::null_os);
543
    NoticeChannel.setStream(&CVC4::null_os);
544
    ChatChannel.setStream(&CVC4::null_os);
545
    MessageChannel.setStream(&CVC4::null_os);
546
    WarningChannel.setStream(&CVC4::null_os);
547
  } else {
548
181
    if(value < 2) {
549
179
      ChatChannel.setStream(&CVC4::null_os);
550
    } else {
551
2
      ChatChannel.setStream(&std::cout);
552
    }
553
181
    if(value < 1) {
554
178
      NoticeChannel.setStream(&CVC4::null_os);
555
    } else {
556
3
      NoticeChannel.setStream(&std::cout);
557
    }
558
181
    if(value < 0) {
559
178
      MessageChannel.setStream(&CVC4::null_os);
560
178
      WarningChannel.setStream(&CVC4::null_os);
561
    } else {
562
3
      MessageChannel.setStream(&std::cout);
563
3
      WarningChannel.setStream(&std::cerr);
564
    }
565
  }
566
181
}
567
568
3
void OptionsHandler::increaseVerbosity(std::string option) {
569
3
  options::verbosity.set(options::verbosity() + 1);
570
3
  setVerbosity(option, options::verbosity());
571
3
}
572
573
178
void OptionsHandler::decreaseVerbosity(std::string option) {
574
178
  options::verbosity.set(options::verbosity() - 1);
575
178
  setVerbosity(option, options::verbosity());
576
178
}
577
578
579
}/* CVC4::options namespace */
580
32144
}/* CVC4 namespace */