src/options/options_handler.cpp

   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 cvc5 {
  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 OptionsHandler::OptionsHandler(Options* options) : d_options(options) { }
  71
  72 unsigned long OptionsHandler::limitHandler(std::string option,
  73                                            std::string optarg)
  74 {
  75   unsigned long ms;
  76   std::istringstream convert(optarg);
  77   if (!(convert >> ms))
  78   {
  79     throw OptionException("option `" + option
  80                           + "` requires a number as an argument");
  81   }
  82   return ms;
  83 }
  84 // theory/quantifiers/options_handlers.h
  85
  86 void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode)
  87 {
  88   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 }
  94
  95 // theory/bv/options_handlers.h
  96 void OptionsHandler::abcEnabledBuild(std::string option, bool value)
  97 {
  98 #ifndef CVC5_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 /* CVC5_USE_ABC */
 105 }
 106
 107 void OptionsHandler::abcEnabledBuild(std::string option, std::string value)
 108 {
 109 #ifndef CVC5_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 /* CVC5_USE_ABC */
 116 }
 117
 118 void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m)
 119 {
 120   if (m == SatSolverMode::CRYPTOMINISAT
 121       && !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   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   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   if (options::bvSolver() != options::BVSolver::BITBLAST
 149       && (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL
 150           || m == SatSolverMode::KISSAT))
 151   {
 152     if (options::bitblastMode() == options::BitblastMode::LAZY
 153         && options::bitblastMode.wasSetByUser())
 154     {
 155       throwLazyBBUnsupported(m);
 156     }
 157     if (!options::bitvectorToBool.wasSetByUser())
 158     {
 159       options::bitvectorToBool.set(true);
 160     }
 161   }
 162 }
 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 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 void OptionsHandler::setDecisionModeStopOnly(std::string option, DecisionMode m)
 246 {
 247   options::decisionStopOnly.set(m == DecisionMode::RELEVANCY);
 248 }
 249
 250 void OptionsHandler::setProduceAssertions(std::string option, bool value)
 251 {
 252   options::produceAssertions.set(value);
 253   options::interactiveMode.set(value);
 254 }
 255
 256 void OptionsHandler::statsEnabledBuild(std::string option, bool value)
 257 {
 258 #ifndef CVC5_STATISTICS_ON
 259   if(value) {
 260     std::stringstream ss;
 261     ss << "option `" << option << "' requires a statistics-enabled build of CVC4; this binary was not built with statistics support";
 262     throw OptionException(ss.str());
 263   }
 264 #endif /* CVC5_STATISTICS_ON */
 265 }
 266
 267 void OptionsHandler::threadN(std::string option) {
 268   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\"");
 269 }
 270
 271 // expr/options_handlers.h
 272 void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) {
 273   if(depth < -1) {
 274     throw OptionException("--expr-depth requires a positive argument, or -1.");
 275   }
 276 }
 277
 278 void OptionsHandler::setDefaultDagThreshPredicate(std::string option, int dag) {
 279   if(dag < 0) {
 280     throw OptionException("--dag-thresh requires a nonnegative argument.");
 281   }
 282 }
 283
 284 // main/options_handlers.h
 285
 286 static void print_config (const char * str, std::string config) {
 287   std::string s(str);
 288   unsigned sz = 14;
 289   if (s.size() < sz) s.resize(sz, ' ');
 290   std::cout << s << ": " << config << std::endl;
 291 }
 292
 293 static void print_config_cond (const char * str, bool cond = false) {
 294   print_config(str, cond ? "yes" : "no");
 295 }
 296
 297 void OptionsHandler::copyright(std::string option) {
 298   std::cout << Configuration::copyright() << std::endl;
 299   exit(0);
 300 }
 301
 302 void OptionsHandler::showConfiguration(std::string option) {
 303   std::cout << Configuration::about() << std::endl;
 304
 305   print_config ("version", Configuration::getVersionString());
 306
 307   if(Configuration::isGitBuild()) {
 308     const char* branchName = Configuration::getGitBranchName();
 309     if(*branchName == '\0')  { branchName = "-"; }
 310     std::stringstream ss;
 311     ss << "git ["
 312        << branchName << " "
 313        << std::string(Configuration::getGitCommit()).substr(0, 8)
 314        << (Configuration::hasGitModifications() ? " (with modifications)" : "")
 315        << "]";
 316     print_config("scm", ss.str());
 317   } else {
 318     print_config_cond("scm", false);
 319   }
 320
 321   std::cout << std::endl;
 322
 323   std::stringstream ss;
 324   ss << Configuration::getVersionMajor() << "."
 325      << Configuration::getVersionMinor() << "."
 326      << Configuration::getVersionRelease();
 327   print_config("library", ss.str());
 328
 329   std::cout << std::endl;
 330
 331   print_config_cond("debug code", Configuration::isDebugBuild());
 332   print_config_cond("statistics", Configuration::isStatisticsBuild());
 333   print_config_cond("tracing", Configuration::isTracingBuild());
 334   print_config_cond("dumping", Configuration::isDumpingBuild());
 335   print_config_cond("muzzled", Configuration::isMuzzledBuild());
 336   print_config_cond("assertions", Configuration::isAssertionBuild());
 337   print_config_cond("coverage", Configuration::isCoverageBuild());
 338   print_config_cond("profiling", Configuration::isProfilingBuild());
 339   print_config_cond("asan", Configuration::isAsanBuild());
 340   print_config_cond("ubsan", Configuration::isUbsanBuild());
 341   print_config_cond("tsan", Configuration::isTsanBuild());
 342   print_config_cond("competition", Configuration::isCompetitionBuild());
 343
 344   std::cout << std::endl;
 345
 346   print_config_cond("abc", Configuration::isBuiltWithAbc());
 347   print_config_cond("cln", Configuration::isBuiltWithCln());
 348   print_config_cond("glpk", Configuration::isBuiltWithGlpk());
 349   print_config_cond("cadical", Configuration::isBuiltWithCadical());
 350   print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
 351   print_config_cond("gmp", Configuration::isBuiltWithGmp());
 352   print_config_cond("kissat", Configuration::isBuiltWithKissat());
 353   print_config_cond("poly", Configuration::isBuiltWithPoly());
 354   print_config_cond("editline", Configuration::isBuiltWithEditline());
 355   print_config_cond("symfpu", Configuration::isBuiltWithSymFPU());
 356
 357   exit(0);
 358 }
 359
 360 static void printTags(unsigned ntags, char const* const* tags)
 361 {
 362   std::cout << "available tags:";
 363   for (unsigned i = 0; i < ntags; ++ i)
 364   {
 365     std::cout << "  " << tags[i] << std::endl;
 366   }
 367   std::cout << std::endl;
 368 }
 369
 370 void OptionsHandler::showDebugTags(std::string option)
 371 {
 372   if (!Configuration::isDebugBuild())
 373   {
 374     throw OptionException("debug tags not available in non-debug builds");
 375   }
 376   else if (!Configuration::isTracingBuild())
 377   {
 378     throw OptionException("debug tags not available in non-tracing builds");
 379   }
 380   printTags(Configuration::getNumDebugTags(),Configuration::getDebugTags());
 381   exit(0);
 382 }
 383
 384 void OptionsHandler::showTraceTags(std::string option)
 385 {
 386   if (!Configuration::isTracingBuild())
 387   {
 388     throw OptionException("trace tags not available in non-tracing build");
 389   }
 390   printTags(Configuration::getNumTraceTags(), Configuration::getTraceTags());
 391   exit(0);
 392 }
 393
 394 static std::string suggestTags(char const* const* validTags,
 395                                std::string inputTag,
 396                                char const* const* additionalTags)
 397 {
 398   DidYouMean didYouMean;
 399
 400   const char* opt;
 401   for (size_t i = 0; (opt = validTags[i]) != nullptr; ++i)
 402   {
 403     didYouMean.addWord(validTags[i]);
 404   }
 405   if (additionalTags != nullptr)
 406   {
 407     for (size_t i = 0; (opt = additionalTags[i]) != nullptr; ++i)
 408     {
 409       didYouMean.addWord(additionalTags[i]);
 410     }
 411   }
 412
 413   return didYouMean.getMatchAsString(inputTag);
 414 }
 415
 416 void OptionsHandler::enableTraceTag(std::string option, std::string optarg)
 417 {
 418   if(!Configuration::isTracingBuild())
 419   {
 420     throw OptionException("trace tags not available in non-tracing builds");
 421   }
 422   else if(!Configuration::isTraceTag(optarg.c_str()))
 423   {
 424     if (optarg == "help")
 425     {
 426       printTags(
 427           Configuration::getNumTraceTags(), Configuration::getTraceTags());
 428       exit(0);
 429     }
 430
 431     throw OptionException(
 432         std::string("trace tag ") + optarg + std::string(" not available.")
 433         + suggestTags(Configuration::getTraceTags(), optarg, nullptr));
 434   }
 435   Trace.on(optarg);
 436 }
 437
 438 void OptionsHandler::enableDebugTag(std::string option, std::string optarg)
 439 {
 440   if (!Configuration::isDebugBuild())
 441   {
 442     throw OptionException("debug tags not available in non-debug builds");
 443   }
 444   else if (!Configuration::isTracingBuild())
 445   {
 446     throw OptionException("debug tags not available in non-tracing builds");
 447   }
 448
 449   if (!Configuration::isDebugTag(optarg.c_str())
 450       && !Configuration::isTraceTag(optarg.c_str()))
 451   {
 452     if (optarg == "help")
 453     {
 454       printTags(
 455           Configuration::getNumDebugTags(), Configuration::getDebugTags());
 456       exit(0);
 457     }
 458
 459     throw OptionException(std::string("debug tag ") + optarg
 460                           + std::string(" not available.")
 461                           + suggestTags(Configuration::getDebugTags(),
 462                                         optarg,
 463                                         Configuration::getTraceTags()));
 464   }
 465   Debug.on(optarg);
 466   Trace.on(optarg);
 467 }
 468
 469 OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option,
 470                                                       std::string optarg)
 471 {
 472   if(optarg == "help") {
 473     options::languageHelp.set(true);
 474     return language::output::LANG_AUTO;
 475   }
 476
 477   try {
 478     return language::toOutputLanguage(optarg);
 479   } catch(OptionException& oe) {
 480     throw OptionException("Error in " + option + ": " + oe.getMessage() +
 481                           "\nTry --output-language help");
 482   }
 483
 484   Unreachable();
 485 }
 486
 487 InputLanguage OptionsHandler::stringToInputLanguage(std::string option,
 488                                                     std::string optarg)
 489 {
 490   if(optarg == "help") {
 491     options::languageHelp.set(true);
 492     return language::input::LANG_AUTO;
 493   }
 494
 495   try {
 496     return language::toInputLanguage(optarg);
 497   } catch(OptionException& oe) {
 498     throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --lang help");
 499   }
 500
 501   Unreachable();
 502 }
 503
 504 /* options/base_options_handlers.h */
 505 void OptionsHandler::setVerbosity(std::string option, int value)
 506 {
 507   if(Configuration::isMuzzledBuild()) {
 508     DebugChannel.setStream(&cvc5::null_os);
 509     TraceChannel.setStream(&cvc5::null_os);
 510     NoticeChannel.setStream(&cvc5::null_os);
 511     ChatChannel.setStream(&cvc5::null_os);
 512     MessageChannel.setStream(&cvc5::null_os);
 513     WarningChannel.setStream(&cvc5::null_os);
 514   } else {
 515     if(value < 2) {
 516       ChatChannel.setStream(&cvc5::null_os);
 517     } else {
 518       ChatChannel.setStream(&std::cout);
 519     }
 520     if(value < 1) {
 521       NoticeChannel.setStream(&cvc5::null_os);
 522     } else {
 523       NoticeChannel.setStream(&std::cout);
 524     }
 525     if(value < 0) {
 526       MessageChannel.setStream(&cvc5::null_os);
 527       WarningChannel.setStream(&cvc5::null_os);
 528     } else {
 529       MessageChannel.setStream(&std::cout);
 530       WarningChannel.setStream(&std::cerr);
 531     }
 532   }
 533 }
 534
 535 void OptionsHandler::increaseVerbosity(std::string option) {
 536   options::verbosity.set(options::verbosity() + 1);
 537   setVerbosity(option, options::verbosity());
 538 }
 539
 540 void OptionsHandler::decreaseVerbosity(std::string option) {
 541   options::verbosity.set(options::verbosity() - 1);
 542   setVerbosity(option, options::verbosity());
 543 }
 544
 545 }  // namespace options
 546 }  // namespace cvc5