src/options/options_handler.cpp

   1 /*********************                                                        */
   2 /*! \file options_handler.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Aina Niemetz, Mathias Preiner
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 OptionsHandler::OptionsHandler(Options* options) : d_options(options) { }
  71
  72 void OptionsHandler::notifyBeforeSearch(const std::string& option)
  73 {
  74   try{
  75     d_options->d_beforeSearchListeners.notify();
  76   } catch (ModalException&){
  77     std::stringstream ss;
  78     ss << "cannot change option `" << option << "' after final initialization";
  79     throw ModalException(ss.str());
  80   }
  81 }
  82
  83 unsigned long OptionsHandler::limitHandler(std::string option,
  84                                            std::string optarg)
  85 {
  86   unsigned long ms;
  87   std::istringstream convert(optarg);
  88   if (!(convert >> ms))
  89   {
  90     throw OptionException("option `" + option
  91                           + "` requires a number as an argument");
  92   }
  93   return ms;
  94 }
  95
  96 /* options/base_options_handlers.h */
  97 void OptionsHandler::notifyPrintSuccess(std::string option) {
  98   d_options->d_setPrintSuccessListeners.notify();
  99 }
 100
 101 // theory/quantifiers/options_handlers.h
 102
 103 void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode)
 104 {
 105   if (mode == InstWhenMode::PRE_FULL)
 106   {
 107     throw OptionException(std::string("Mode pre-full for ") + option
 108                           + " is not supported in this release.");
 109   }
 110 }
 111
 112 // theory/bv/options_handlers.h
 113 void OptionsHandler::abcEnabledBuild(std::string option, bool value)
 114 {
 115 #ifndef CVC4_USE_ABC
 116   if(value) {
 117     std::stringstream ss;
 118     ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
 119     throw OptionException(ss.str());
 120   }
 121 #endif /* CVC4_USE_ABC */
 122 }
 123
 124 void OptionsHandler::abcEnabledBuild(std::string option, std::string value)
 125 {
 126 #ifndef CVC4_USE_ABC
 127   if(!value.empty()) {
 128     std::stringstream ss;
 129     ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
 130     throw OptionException(ss.str());
 131   }
 132 #endif /* CVC4_USE_ABC */
 133 }
 134
 135 void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m)
 136 {
 137   if (m == SatSolverMode::CRYPTOMINISAT
 138       && !Configuration::isBuiltWithCryptominisat())
 139   {
 140     std::stringstream ss;
 141     ss << "option `" << option
 142        << "' requires a CryptoMiniSat build of CVC4; this binary was not built "
 143           "with CryptoMiniSat support";
 144     throw OptionException(ss.str());
 145   }
 146
 147   if (m == SatSolverMode::CADICAL && !Configuration::isBuiltWithCadical())
 148   {
 149     std::stringstream ss;
 150     ss << "option `" << option
 151        << "' requires a CaDiCaL build of CVC4; this binary was not built with "
 152           "CaDiCaL support";
 153     throw OptionException(ss.str());
 154   }
 155
 156   if (m == SatSolverMode::KISSAT && !Configuration::isBuiltWithKissat())
 157   {
 158     std::stringstream ss;
 159     ss << "option `" << option
 160        << "' requires a Kissat build of CVC4; this binary was not built with "
 161           "Kissat support";
 162     throw OptionException(ss.str());
 163   }
 164
 165   if (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL
 166       || m == SatSolverMode::KISSAT)
 167   {
 168     if (options::bitblastMode() == options::BitblastMode::LAZY
 169         && options::bitblastMode.wasSetByUser())
 170     {
 171       throwLazyBBUnsupported(m);
 172     }
 173     if (!options::bitvectorToBool.wasSetByUser())
 174     {
 175       options::bitvectorToBool.set(true);
 176     }
 177   }
 178 }
 179
 180 void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m)
 181 {
 182   if (m == options::BitblastMode::LAZY)
 183   {
 184     if (!options::bitvectorPropagate.wasSetByUser())
 185     {
 186       options::bitvectorPropagate.set(true);
 187     }
 188     if (!options::bitvectorEqualitySolver.wasSetByUser())
 189     {
 190       options::bitvectorEqualitySolver.set(true);
 191     }
 192     if (!options::bitvectorEqualitySlicer.wasSetByUser())
 193     {
 194       if (options::incrementalSolving() || options::produceModels())
 195       {
 196         options::bitvectorEqualitySlicer.set(options::BvSlicerMode::OFF);
 197       }
 198       else
 199       {
 200         options::bitvectorEqualitySlicer.set(options::BvSlicerMode::AUTO);
 201       }
 202     }
 203
 204     if (!options::bitvectorInequalitySolver.wasSetByUser())
 205     {
 206       options::bitvectorInequalitySolver.set(true);
 207     }
 208     if (!options::bitvectorAlgebraicSolver.wasSetByUser())
 209     {
 210       options::bitvectorAlgebraicSolver.set(true);
 211     }
 212     if (options::bvSatSolver() != options::SatSolverMode::MINISAT)
 213     {
 214       throwLazyBBUnsupported(options::bvSatSolver());
 215     }
 216   }
 217   else if (m == BitblastMode::EAGER)
 218   {
 219     if (!options::bitvectorToBool.wasSetByUser())
 220     {
 221       options::bitvectorToBool.set(true);
 222     }
 223   }
 224 }
 225
 226 void OptionsHandler::setBitblastAig(std::string option, bool arg)
 227 {
 228   if(arg) {
 229     if(options::bitblastMode.wasSetByUser()) {
 230       if (options::bitblastMode() != options::BitblastMode::EAGER)
 231       {
 232         throw OptionException("bitblast-aig must be used with eager bitblaster");
 233       }
 234     } else {
 235       options::BitblastMode mode = stringToBitblastMode("", "eager");
 236       options::bitblastMode.set(mode);
 237     }
 238     if(!options::bitvectorAigSimplifications.wasSetByUser()) {
 239       options::bitvectorAigSimplifications.set("balance;drw");
 240     }
 241   }
 242 }
 243
 244 // printer/options_handlers.h
 245 const std::string OptionsHandler::s_instFormatHelp = "\
 246 Inst format modes currently supported by the --inst-format option:\n\
 247 \n\
 248 default \n\
 249 + Print instantiations as a list in the output language format.\n\
 250 \n\
 251 szs\n\
 252 + Print instantiations as SZS compliant proof.\n\
 253 ";
 254
 255 InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option,
 256                                                       std::string optarg)
 257 {
 258   if(optarg == "default") {
 259     return InstFormatMode::DEFAULT;
 260   } else if(optarg == "szs") {
 261     return InstFormatMode::SZS;
 262   } else if(optarg == "help") {
 263     puts(s_instFormatHelp.c_str());
 264     exit(1);
 265   } else {
 266     throw OptionException(std::string("unknown option for --inst-format: `") +
 267                           optarg + "'.  Try --inst-format help.");
 268   }
 269 }
 270
 271 // decision/options_handlers.h
 272 void OptionsHandler::setDecisionModeStopOnly(std::string option, DecisionMode m)
 273 {
 274   options::decisionStopOnly.set(m == DecisionMode::RELEVANCY);
 275 }
 276
 277 void OptionsHandler::setProduceAssertions(std::string option, bool value)
 278 {
 279   options::produceAssertions.set(value);
 280   options::interactiveMode.set(value);
 281 }
 282
 283 void OptionsHandler::proofEnabledBuild(std::string option, bool value)
 284 {
 285 #ifdef CVC4_PROOF
 286   if (value && options::bitblastMode() == options::BitblastMode::EAGER
 287       && options::bvSatSolver() != options::SatSolverMode::MINISAT
 288       && options::bvSatSolver() != options::SatSolverMode::CRYPTOMINISAT)
 289   {
 290     throw OptionException(
 291         "Eager BV proofs only supported when MiniSat or CryptoMiniSat is used");
 292   }
 293 #else
 294   if(value) {
 295     std::stringstream ss;
 296     ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support";
 297     throw OptionException(ss.str());
 298   }
 299 #endif /* CVC4_PROOF */
 300 }
 301
 302 void OptionsHandler::LFSCEnabledBuild(std::string option, bool value) {
 303 #ifndef CVC4_USE_LFSC
 304   if (value) {
 305     std::stringstream ss;
 306     ss << "option `" << option << "' requires a build of CVC4 with integrated "
 307                                   "LFSC; this binary was not built with LFSC";
 308     throw OptionException(ss.str());
 309   }
 310 #endif /* CVC4_USE_LFSC */
 311 }
 312
 313 void OptionsHandler::notifyDumpToFile(std::string option) {
 314   d_options->d_dumpToFileListeners.notify();
 315 }
 316
 317
 318 void OptionsHandler::notifySetRegularOutputChannel(std::string option) {
 319   d_options->d_setRegularChannelListeners.notify();
 320 }
 321
 322 void OptionsHandler::notifySetDiagnosticOutputChannel(std::string option) {
 323   d_options->d_setDiagnosticChannelListeners.notify();
 324 }
 325
 326 void OptionsHandler::statsEnabledBuild(std::string option, bool value)
 327 {
 328 #ifndef CVC4_STATISTICS_ON
 329   if(value) {
 330     std::stringstream ss;
 331     ss << "option `" << option << "' requires a statistics-enabled build of CVC4; this binary was not built with statistics support";
 332     throw OptionException(ss.str());
 333   }
 334 #endif /* CVC4_STATISTICS_ON */
 335 }
 336
 337 void OptionsHandler::threadN(std::string option) {
 338   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\"");
 339 }
 340
 341 void OptionsHandler::notifyDumpMode(std::string option)
 342 {
 343   d_options->d_setDumpModeListeners.notify();
 344 }
 345
 346
 347 // expr/options_handlers.h
 348 void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) {
 349   if(depth < -1) {
 350     throw OptionException("--expr-depth requires a positive argument, or -1.");
 351   }
 352 }
 353
 354 void OptionsHandler::setDefaultDagThreshPredicate(std::string option, int dag) {
 355   if(dag < 0) {
 356     throw OptionException("--dag-thresh requires a nonnegative argument.");
 357   }
 358 }
 359
 360 void OptionsHandler::notifySetDefaultExprDepth(std::string option) {
 361   d_options->d_setDefaultExprDepthListeners.notify();
 362 }
 363
 364 void OptionsHandler::notifySetDefaultDagThresh(std::string option) {
 365   d_options->d_setDefaultDagThreshListeners.notify();
 366 }
 367
 368 void OptionsHandler::notifySetPrintExprTypes(std::string option) {
 369   d_options->d_setPrintExprTypesListeners.notify();
 370 }
 371
 372
 373 // main/options_handlers.h
 374
 375 static void print_config (const char * str, std::string config) {
 376   std::string s(str);
 377   unsigned sz = 14;
 378   if (s.size() < sz) s.resize(sz, ' ');
 379   std::cout << s << ": " << config << std::endl;
 380 }
 381
 382 static void print_config_cond (const char * str, bool cond = false) {
 383   print_config(str, cond ? "yes" : "no");
 384 }
 385
 386 void OptionsHandler::copyright(std::string option) {
 387   std::cout << Configuration::copyright() << std::endl;
 388   exit(0);
 389 }
 390
 391 void OptionsHandler::showConfiguration(std::string option) {
 392   std::cout << Configuration::about() << std::endl;
 393
 394   print_config ("version", Configuration::getVersionString());
 395
 396   if(Configuration::isGitBuild()) {
 397     const char* branchName = Configuration::getGitBranchName();
 398     if(*branchName == '\0')  { branchName = "-"; }
 399     std::stringstream ss;
 400     ss << "git ["
 401        << branchName << " "
 402        << std::string(Configuration::getGitCommit()).substr(0, 8)
 403        << (Configuration::hasGitModifications() ? " (with modifications)" : "")
 404        << "]";
 405     print_config("scm", ss.str());
 406   } else {
 407     print_config_cond("scm", false);
 408   }
 409
 410   std::cout << std::endl;
 411
 412   std::stringstream ss;
 413   ss << Configuration::getVersionMajor() << "."
 414      << Configuration::getVersionMinor() << "."
 415      << Configuration::getVersionRelease();
 416   print_config("library", ss.str());
 417
 418   std::cout << std::endl;
 419
 420   print_config_cond("debug code", Configuration::isDebugBuild());
 421   print_config_cond("statistics", Configuration::isStatisticsBuild());
 422   print_config_cond("tracing", Configuration::isTracingBuild());
 423   print_config_cond("dumping", Configuration::isDumpingBuild());
 424   print_config_cond("muzzled", Configuration::isMuzzledBuild());
 425   print_config_cond("assertions", Configuration::isAssertionBuild());
 426   print_config_cond("proof", Configuration::isProofBuild());
 427   print_config_cond("coverage", Configuration::isCoverageBuild());
 428   print_config_cond("profiling", Configuration::isProfilingBuild());
 429   print_config_cond("asan", Configuration::isAsanBuild());
 430   print_config_cond("ubsan", Configuration::isUbsanBuild());
 431   print_config_cond("tsan", Configuration::isTsanBuild());
 432   print_config_cond("competition", Configuration::isCompetitionBuild());
 433
 434   std::cout << std::endl;
 435
 436   print_config_cond("abc", Configuration::isBuiltWithAbc());
 437   print_config_cond("cln", Configuration::isBuiltWithCln());
 438   print_config_cond("glpk", Configuration::isBuiltWithGlpk());
 439   print_config_cond("cadical", Configuration::isBuiltWithCadical());
 440   print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
 441   print_config_cond("drat2er", Configuration::isBuiltWithDrat2Er());
 442   print_config_cond("gmp", Configuration::isBuiltWithGmp());
 443   print_config_cond("kissat", Configuration::isBuiltWithKissat());
 444   print_config_cond("lfsc", Configuration::isBuiltWithLfsc());
 445   print_config_cond("poly", Configuration::isBuiltWithPoly());
 446   print_config_cond("editline", Configuration::isBuiltWithEditline());
 447   print_config_cond("symfpu", Configuration::isBuiltWithSymFPU());
 448
 449   exit(0);
 450 }
 451
 452 static void printTags(unsigned ntags, char const* const* tags)
 453 {
 454   std::cout << "available tags:";
 455   for (unsigned i = 0; i < ntags; ++ i)
 456   {
 457     std::cout << "  " << tags[i] << std::endl;
 458   }
 459   std::cout << std::endl;
 460 }
 461
 462 void OptionsHandler::showDebugTags(std::string option)
 463 {
 464   if (!Configuration::isDebugBuild())
 465   {
 466     throw OptionException("debug tags not available in non-debug builds");
 467   }
 468   else if (!Configuration::isTracingBuild())
 469   {
 470     throw OptionException("debug tags not available in non-tracing builds");
 471   }
 472   printTags(Configuration::getNumDebugTags(),Configuration::getDebugTags());
 473   exit(0);
 474 }
 475
 476 void OptionsHandler::showTraceTags(std::string option)
 477 {
 478   if (!Configuration::isTracingBuild())
 479   {
 480     throw OptionException("trace tags not available in non-tracing build");
 481   }
 482   printTags(Configuration::getNumTraceTags(), Configuration::getTraceTags());
 483   exit(0);
 484 }
 485
 486 static std::string suggestTags(char const* const* validTags,
 487                                std::string inputTag,
 488                                char const* const* additionalTags)
 489 {
 490   DidYouMean didYouMean;
 491
 492   const char* opt;
 493   for (size_t i = 0; (opt = validTags[i]) != nullptr; ++i)
 494   {
 495     didYouMean.addWord(validTags[i]);
 496   }
 497   if (additionalTags != nullptr)
 498   {
 499     for (size_t i = 0; (opt = additionalTags[i]) != nullptr; ++i)
 500     {
 501       didYouMean.addWord(additionalTags[i]);
 502     }
 503   }
 504
 505   return didYouMean.getMatchAsString(inputTag);
 506 }
 507
 508 void OptionsHandler::enableTraceTag(std::string option, std::string optarg)
 509 {
 510   if(!Configuration::isTracingBuild())
 511   {
 512     throw OptionException("trace tags not available in non-tracing builds");
 513   }
 514   else if(!Configuration::isTraceTag(optarg.c_str()))
 515   {
 516     if (optarg == "help")
 517     {
 518       printTags(
 519           Configuration::getNumTraceTags(), Configuration::getTraceTags());
 520       exit(0);
 521     }
 522
 523     throw OptionException(
 524         std::string("trace tag ") + optarg + std::string(" not available.")
 525         + suggestTags(Configuration::getTraceTags(), optarg, nullptr));
 526   }
 527   Trace.on(optarg);
 528 }
 529
 530 void OptionsHandler::enableDebugTag(std::string option, std::string optarg)
 531 {
 532   if (!Configuration::isDebugBuild())
 533   {
 534     throw OptionException("debug tags not available in non-debug builds");
 535   }
 536   else if (!Configuration::isTracingBuild())
 537   {
 538     throw OptionException("debug tags not available in non-tracing builds");
 539   }
 540
 541   if (!Configuration::isDebugTag(optarg.c_str())
 542       && !Configuration::isTraceTag(optarg.c_str()))
 543   {
 544     if (optarg == "help")
 545     {
 546       printTags(
 547           Configuration::getNumDebugTags(), Configuration::getDebugTags());
 548       exit(0);
 549     }
 550
 551     throw OptionException(std::string("debug tag ") + optarg
 552                           + std::string(" not available.")
 553                           + suggestTags(Configuration::getDebugTags(),
 554                                         optarg,
 555                                         Configuration::getTraceTags()));
 556   }
 557   Debug.on(optarg);
 558   Trace.on(optarg);
 559 }
 560
 561 OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option,
 562                                                       std::string optarg)
 563 {
 564   if(optarg == "help") {
 565     options::languageHelp.set(true);
 566     return language::output::LANG_AUTO;
 567   }
 568
 569   try {
 570     return language::toOutputLanguage(optarg);
 571   } catch(OptionException& oe) {
 572     throw OptionException("Error in " + option + ": " + oe.getMessage() +
 573                           "\nTry --output-language help");
 574   }
 575
 576   Unreachable();
 577 }
 578
 579 InputLanguage OptionsHandler::stringToInputLanguage(std::string option,
 580                                                     std::string optarg)
 581 {
 582   if(optarg == "help") {
 583     options::languageHelp.set(true);
 584     return language::input::LANG_AUTO;
 585   }
 586
 587   try {
 588     return language::toInputLanguage(optarg);
 589   } catch(OptionException& oe) {
 590     throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --language help");
 591   }
 592
 593   Unreachable();
 594 }
 595
 596 /* options/base_options_handlers.h */
 597 void OptionsHandler::setVerbosity(std::string option, int value)
 598 {
 599   if(Configuration::isMuzzledBuild()) {
 600     DebugChannel.setStream(&CVC4::null_os);
 601     TraceChannel.setStream(&CVC4::null_os);
 602     NoticeChannel.setStream(&CVC4::null_os);
 603     ChatChannel.setStream(&CVC4::null_os);
 604     MessageChannel.setStream(&CVC4::null_os);
 605     WarningChannel.setStream(&CVC4::null_os);
 606   } else {
 607     if(value < 2) {
 608       ChatChannel.setStream(&CVC4::null_os);
 609     } else {
 610       ChatChannel.setStream(&std::cout);
 611     }
 612     if(value < 1) {
 613       NoticeChannel.setStream(&CVC4::null_os);
 614     } else {
 615       NoticeChannel.setStream(&std::cout);
 616     }
 617     if(value < 0) {
 618       MessageChannel.setStream(&CVC4::null_os);
 619       WarningChannel.setStream(&CVC4::null_os);
 620     } else {
 621       MessageChannel.setStream(&std::cout);
 622       WarningChannel.setStream(&std::cerr);
 623     }
 624   }
 625 }
 626
 627 void OptionsHandler::increaseVerbosity(std::string option) {
 628   options::verbosity.set(options::verbosity() + 1);
 629   setVerbosity(option, options::verbosity());
 630 }
 631
 632 void OptionsHandler::decreaseVerbosity(std::string option) {
 633   options::verbosity.set(options::verbosity() - 1);
 634   setVerbosity(option, options::verbosity());
 635 }
 636
 637
 638 }/* CVC4::options namespace */
 639 }/* CVC4 namespace */