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