src/options/options_handler.cpp

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