src/options/options_handler.cpp

   1 /*********************                                                        */
   2 /*! \file options_handler.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Andrew Reynolds, Aina Niemetz
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 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/configuration.h"
  26 #include "base/configuration_private.h"
  27 #include "base/cvc4_assert.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/arith_heuristic_pivot_rule.h"
  33 #include "options/arith_propagation_mode.h"
  34 #include "options/arith_unate_lemma_mode.h"
  35 #include "options/base_options.h"
  36 #include "options/bv_bitblast_mode.h"
  37 #include "options/bv_options.h"
  38 #include "options/decision_mode.h"
  39 #include "options/decision_options.h"
  40 #include "options/datatypes_modes.h"
  41 #include "options/didyoumean.h"
  42 #include "options/language.h"
  43 #include "options/option_exception.h"
  44 #include "options/printer_modes.h"
  45 #include "options/smt_options.h"
  46 #include "options/theory_options.h"
  47 #include "options/theoryof_mode.h"
  48 #include "options/ufss_mode.h"
  49
  50 namespace CVC4 {
  51 namespace options {
  52
  53 // helper functions
  54 namespace {
  55
  56 void throwLazyBBUnsupported(theory::bv::SatSolverMode m)
  57 {
  58   std::string sat_solver;
  59   if (m == theory::bv::SAT_SOLVER_CADICAL)
  60   {
  61     sat_solver = "CaDiCaL";
  62   }
  63   else
  64   {
  65     Assert(m == theory::bv::SAT_SOLVER_CRYPTOMINISAT);
  66     sat_solver = "CryptoMiniSat";
  67   }
  68   std::string indent(25, ' ');
  69   throw OptionException(sat_solver + " does not support lazy bit-blasting.\n"
  70                         + indent + "Try --bv-sat-solver=minisat");
  71 }
  72
  73 }  // namespace
  74
  75 OptionsHandler::OptionsHandler(Options* options) : d_options(options) { }
  76
  77 void OptionsHandler::notifyForceLogic(const std::string& option){
  78   d_options->d_forceLogicListeners.notify();
  79 }
  80
  81 void OptionsHandler::notifyBeforeSearch(const std::string& option)
  82 {
  83   try{
  84     d_options->d_beforeSearchListeners.notify();
  85   } catch (ModalException&){
  86     std::stringstream ss;
  87     ss << "cannot change option `" << option << "' after final initialization";
  88     throw ModalException(ss.str());
  89   }
  90 }
  91
  92
  93 void OptionsHandler::notifyTlimit(const std::string& option) {
  94   d_options->d_tlimitListeners.notify();
  95 }
  96
  97 void OptionsHandler::notifyTlimitPer(const std::string& option) {
  98   d_options->d_tlimitPerListeners.notify();
  99 }
 100
 101 void OptionsHandler::notifyRlimit(const std::string& option) {
 102   d_options->d_rlimitListeners.notify();
 103 }
 104
 105 void OptionsHandler::notifyRlimitPer(const std::string& option) {
 106   d_options->d_rlimitPerListeners.notify();
 107 }
 108
 109 unsigned long OptionsHandler::limitHandler(std::string option,
 110                                            std::string optarg)
 111 {
 112   unsigned long ms;
 113   std::istringstream convert(optarg);
 114   if (!(convert >> ms))
 115   {
 116     throw OptionException("option `" + option
 117                           + "` requires a number as an argument");
 118   }
 119   return ms;
 120 }
 121
 122 /* options/base_options_handlers.h */
 123 void OptionsHandler::notifyPrintSuccess(std::string option) {
 124   d_options->d_setPrintSuccessListeners.notify();
 125 }
 126
 127 // theory/arith/options_handlers.h
 128 const std::string OptionsHandler::s_arithUnateLemmasHelp = "\
 129 Unate lemmas are generated before SAT search begins using the relationship\n\
 130 of constant terms and polynomials.\n\
 131 Modes currently supported by the --unate-lemmas option:\n\
 132 + none \n\
 133 + ineqs \n\
 134   Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n\
 135 + eqs \n\
 136   Outputs lemmas of the general forms\n\
 137   (= p c) implies (<= p d) for c < d, or\n\
 138   (= p c) implies (not (= p d)) for c != d.\n\
 139 + all \n\
 140   A combination of inequalities and equalities.\n\
 141 ";
 142
 143 const std::string OptionsHandler::s_arithPropagationModeHelp = "\
 144 This decides on kind of propagation arithmetic attempts to do during the search.\n\
 145 + none\n\
 146 + unate\n\
 147  use constraints to do unate propagation\n\
 148 + bi (Bounds Inference)\n\
 149   infers bounds on basic variables using the upper and lower bounds of the\n\
 150   non-basic variables in the tableau.\n\
 151 +both\n\
 152 ";
 153
 154 const std::string OptionsHandler::s_errorSelectionRulesHelp = "\
 155 This decides on the rule used by simplex during heuristic rounds\n\
 156 for deciding the next basic variable to select.\n\
 157 Heuristic pivot rules available:\n\
 158 +min\n\
 159   The minimum abs() value of the variable's violation of its bound. (default)\n\
 160 +max\n\
 161   The maximum violation the bound\n\
 162 +varord\n\
 163   The variable order\n\
 164 ";
 165
 166 ArithUnateLemmaMode OptionsHandler::stringToArithUnateLemmaMode(
 167     std::string option, std::string optarg)
 168 {
 169   if(optarg == "all") {
 170     return ALL_PRESOLVE_LEMMAS;
 171   } else if(optarg == "none") {
 172     return NO_PRESOLVE_LEMMAS;
 173   } else if(optarg == "ineqs") {
 174     return INEQUALITY_PRESOLVE_LEMMAS;
 175   } else if(optarg == "eqs") {
 176     return EQUALITY_PRESOLVE_LEMMAS;
 177   } else if(optarg == "help") {
 178     puts(s_arithUnateLemmasHelp.c_str());
 179     exit(1);
 180   } else {
 181     throw OptionException(std::string("unknown option for --unate-lemmas: `") +
 182                           optarg + "'.  Try --unate-lemmas help.");
 183   }
 184 }
 185
 186 ArithPropagationMode OptionsHandler::stringToArithPropagationMode(
 187     std::string option, std::string optarg)
 188 {
 189   if(optarg == "none") {
 190     return NO_PROP;
 191   } else if(optarg == "unate") {
 192     return UNATE_PROP;
 193   } else if(optarg == "bi") {
 194     return BOUND_INFERENCE_PROP;
 195   } else if(optarg == "both") {
 196     return BOTH_PROP;
 197   } else if(optarg == "help") {
 198     puts(s_arithPropagationModeHelp.c_str());
 199     exit(1);
 200   } else {
 201     throw OptionException(std::string("unknown option for --arith-prop: `") +
 202                           optarg + "'.  Try --arith-prop help.");
 203   }
 204 }
 205
 206 ErrorSelectionRule OptionsHandler::stringToErrorSelectionRule(
 207     std::string option, std::string optarg)
 208 {
 209   if(optarg == "min") {
 210     return MINIMUM_AMOUNT;
 211   } else if(optarg == "varord") {
 212     return VAR_ORDER;
 213   } else if(optarg == "max") {
 214     return MAXIMUM_AMOUNT;
 215   } else if(optarg == "help") {
 216     puts(s_errorSelectionRulesHelp.c_str());
 217     exit(1);
 218   } else {
 219     throw OptionException(std::string("unknown option for --heuristic-pivot-rule: `") +
 220                           optarg + "'.  Try --heuristic-pivot-rule help.");
 221   }
 222 }
 223 // theory/quantifiers/options_handlers.h
 224
 225 const std::string OptionsHandler::s_instWhenHelp = "\
 226 Modes currently supported by the --inst-when option:\n\
 227 \n\
 228 full-last-call (default)\n\
 229 + Alternate running instantiation rounds at full effort and last\n\
 230   call.  In other words, interleave instantiation and theory combination.\n\
 231 \n\
 232 full\n\
 233 + Run instantiation round at full effort, before theory combination.\n\
 234 \n\
 235 full-delay \n\
 236 + Run instantiation round at full effort, before theory combination, after\n\
 237   all other theories have finished.\n\
 238 \n\
 239 full-delay-last-call \n\
 240 + Alternate running instantiation rounds at full effort after all other\n\
 241   theories have finished, and last call.  \n\
 242 \n\
 243 last-call\n\
 244 + Run instantiation at last call effort, after theory combination and\n\
 245   and theories report sat.\n\
 246 \n\
 247 ";
 248
 249 const std::string OptionsHandler::s_literalMatchHelp = "\
 250 Literal match modes currently supported by the --literal-match option:\n\
 251 \n\
 252 none \n\
 253 + Do not use literal matching.\n\
 254 \n\
 255 use (default)\n\
 256 + Consider phase requirements of triggers conservatively. For example, the\n\
 257   trigger P( x ) in forall( x ). ( P( x ) V ~Q( x ) ) will not be matched with\n\
 258   terms in the equivalence class of true, and likewise Q( x ) will not be matched\n\
 259   terms in the equivalence class of false. Extends to equality.\n\
 260 \n\
 261 agg-predicate \n\
 262 + Consider phase requirements aggressively for predicates. In the above example,\n\
 263   only match P( x ) with terms that are in the equivalence class of false.\n\
 264 \n\
 265 agg \n\
 266 + Consider the phase requirements aggressively for all triggers.\n\
 267 \n\
 268 ";
 269
 270 const std::string OptionsHandler::s_mbqiModeHelp = "\
 271 Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\
 272 \n\
 273 default \n\
 274 + Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\
 275   Modulo Theories.\n\
 276 \n\
 277 none \n\
 278 + Disable model-based quantifier instantiation.\n\
 279 \n\
 280 gen-ev \n\
 281 + Use model-based quantifier instantiation algorithm from CADE 24 finite\n\
 282   model finding paper based on generalizing evaluations.\n\
 283 \n\
 284 abs \n\
 285 + Use abstract MBQI algorithm (uses disjoint sets). \n\
 286 \n\
 287 ";
 288
 289 const std::string OptionsHandler::s_qcfWhenModeHelp = "\
 290 Quantifier conflict find modes currently supported by the --quant-cf-when option:\n\
 291 \n\
 292 default \n\
 293 + Default, apply conflict finding at full effort.\n\
 294 \n\
 295 last-call \n\
 296 + Apply conflict finding at last call, after theory combination and \n\
 297   and all theories report sat. \n\
 298 \n\
 299 std \n\
 300 + Apply conflict finding at standard effort.\n\
 301 \n\
 302 std-h \n\
 303 + Apply conflict finding at standard effort when heuristic says to. \n\
 304 \n\
 305 ";
 306
 307 const std::string OptionsHandler::s_qcfModeHelp = "\
 308 Quantifier conflict find modes currently supported by the --quant-cf option:\n\
 309 \n\
 310 prop-eq \n\
 311 + Default, apply QCF algorithm to propagate equalities as well as conflicts. \n\
 312 \n\
 313 conflict \n\
 314 + Apply QCF algorithm to find conflicts only.\n\
 315 \n\
 316 ";
 317
 318 const std::string OptionsHandler::s_userPatModeHelp = "\
 319 User pattern modes currently supported by the --user-pat option:\n\
 320 \n\
 321 trust \n\
 322 + When provided, use only user-provided patterns for a quantified formula.\n\
 323 \n\
 324 use \n\
 325 + Use both user-provided and auto-generated patterns when patterns\n\
 326   are provided for a quantified formula.\n\
 327 \n\
 328 resort \n\
 329 + Use user-provided patterns only after auto-generated patterns saturate.\n\
 330 \n\
 331 ignore \n\
 332 + Ignore user-provided patterns. \n\
 333 \n\
 334 interleave \n\
 335 + Alternate between use/resort. \n\
 336 \n\
 337 ";
 338
 339 const std::string OptionsHandler::s_triggerSelModeHelp = "\
 340 Trigger selection modes currently supported by the --trigger-sel option:\n\
 341 \n\
 342 min | default \n\
 343 + Consider only minimal subterms that meet criteria for triggers.\n\
 344 \n\
 345 max \n\
 346 + Consider only maximal subterms that meet criteria for triggers. \n\
 347 \n\
 348 all \n\
 349 + Consider all subterms that meet criteria for triggers. \n\
 350 \n\
 351 min-s-max \n\
 352 + Consider only minimal subterms that meet criteria for single triggers, maximal otherwise. \n\
 353 \n\
 354 min-s-all \n\
 355 + Consider only minimal subterms that meet criteria for single triggers, all otherwise. \n\
 356 \n\
 357 ";
 358 const std::string OptionsHandler::s_triggerActiveSelModeHelp = "\
 359 Trigger active selection modes currently supported by the --trigger-sel option:\n\
 360 \n\
 361 all \n\
 362 + Make all triggers active. \n\
 363 \n\
 364 min \n\
 365 + Activate triggers with minimal ground terms.\n\
 366 \n\
 367 max \n\
 368 + Activate triggers with maximal ground terms. \n\
 369 \n\
 370 ";
 371 const std::string OptionsHandler::s_prenexQuantModeHelp = "\
 372 Prenex quantifiers modes currently supported by the --prenex-quant option:\n\
 373 \n\
 374 none \n\
 375 + Do no prenex nested quantifiers. \n\
 376 \n\
 377 default | simple \n\
 378 + Default, do simple prenexing of same sign quantifiers.\n\
 379 \n\
 380 dnorm \n\
 381 + Prenex to disjunctive prenex normal form.\n\
 382 \n\
 383 norm \n\
 384 + Prenex to prenex normal form.\n\
 385 \n\
 386 ";
 387
 388 const std::string OptionsHandler::s_cegqiFairModeHelp = "\
 389 Modes for enforcing fairness for counterexample guided quantifier instantion, supported by --sygus-fair:\n\
 390 \n\
 391 uf-dt-size \n\
 392 + Enforce fairness using an uninterpreted function for datatypes size.\n\
 393 \n\
 394 direct \n\
 395 + Enforce fairness using direct conflict lemmas.\n\
 396 \n\
 397 default | dt-size \n\
 398 + Default, enforce fairness using size operator.\n\
 399 \n\
 400 dt-height-bound \n\
 401 + Enforce fairness by height bound predicate.\n\
 402 \n\
 403 none \n\
 404 + Do not enforce fairness. \n\
 405 \n\
 406 ";
 407
 408 const std::string OptionsHandler::s_termDbModeHelp = "\
 409 Modes for term database, supported by --term-db-mode:\n\
 410 \n\
 411 all  \n\
 412 + Quantifiers module considers all ground terms.\n\
 413 \n\
 414 relevant \n\
 415 + Quantifiers module considers only ground terms connected to current assertions. \n\
 416 \n\
 417 ";
 418
 419 const std::string OptionsHandler::s_iteLiftQuantHelp = "\
 420 Modes for term database, supported by --ite-lift-quant:\n\
 421 \n\
 422 none  \n\
 423 + Do not lift if-then-else in quantified formulas.\n\
 424 \n\
 425 simple  \n\
 426 + Lift if-then-else in quantified formulas if results in smaller term size.\n\
 427 \n\
 428 all \n\
 429 + Lift if-then-else in quantified formulas. \n\
 430 \n\
 431 ";
 432
 433 const std::string OptionsHandler::s_cbqiBvIneqModeHelp =
 434     "\
 435 Modes for single invocation techniques, supported by --cbqi-bv-ineq:\n\
 436 \n\
 437 eq-slack (default)  \n\
 438 + Solve for the inequality using the slack value in the model, e.g.,\
 439   t > s becomes t = s + ( t-s )^M.\n\
 440 \n\
 441 eq-boundary \n\
 442 + Solve for the boundary point of the inequality, e.g.,\
 443   t > s becomes t = s+1.\n\
 444 \n\
 445 keep  \n\
 446 + Solve for the inequality directly using side conditions for invertibility.\n\
 447 \n\
 448 ";
 449
 450 const std::string OptionsHandler::s_cegqiSingleInvHelp = "\
 451 Modes for single invocation techniques, supported by --cegqi-si:\n\
 452 \n\
 453 none  \n\
 454 + Do not use single invocation techniques.\n\
 455 \n\
 456 use (default) \n\
 457 + Use single invocation techniques only if grammar is not restrictive.\n\
 458 \n\
 459 all-abort  \n\
 460 + Always use single invocation techniques, abort if solution reconstruction will likely fail,\
 461   for instance, when the grammar does not have ITE and solution requires it.\n\
 462 \n\
 463 all \n\
 464 + Always use single invocation techniques. \n\
 465 \n\
 466 ";
 467
 468 const std::string OptionsHandler::s_cegqiSingleInvRconsHelp =
 469     "\
 470 Modes for reconstruction solutions while using single invocation techniques,\
 471 supported by --cegqi-si-rcons:\n\
 472 \n\
 473 none \n\
 474 + Do not try to reconstruct solutions in the original (user-provided) grammar\
 475   when using single invocation techniques. In this mode, solutions produced by\
 476   CVC4 may violate grammar restrictions.\n\
 477 \n\
 478 try \n\
 479 + Try to reconstruct solutions in the original grammar when using single\
 480   invocation techniques in an incomplete (fail-fast) manner.\n\
 481 \n\
 482 all-limit \n\
 483 + Try to reconstruct solutions in the original grammar, but termintate if a\
 484   maximum number of rounds for reconstruction is exceeded.\n\
 485 \n\
 486 all \n\
 487 + Try to reconstruct solutions in the original grammar. In this mode,\
 488   we do not terminate until a solution is successfully reconstructed. \n\
 489 \n\
 490 ";
 491
 492 const std::string OptionsHandler::s_cegisSampleHelp =
 493     "\
 494 Modes for sampling with counterexample-guided inductive synthesis (CEGIS),\
 495 supported by --cegis-sample:\n\
 496 \n\
 497 none (default) \n\
 498 + Do not use sampling with CEGIS.\n\
 499 \n\
 500 use \n\
 501 + Use sampling to accelerate CEGIS. This will rule out solutions for a\
 502   conjecture when they are not satisfied by a sample point.\n\
 503 \n\
 504 trust  \n\
 505 + Trust that when a solution for a conjecture is always true under sampling,\
 506   then it is indeed a solution. Note this option may print out spurious\
 507   solutions for synthesis conjectures.\n\
 508 \n\
 509 ";
 510
 511 const std::string OptionsHandler::s_sygusFilterSolHelp =
 512     "\
 513 Modes for filtering sygus solutions supported by --sygus-filter-sol:\n\
 514 \n\
 515 none (default) \n\
 516 + Do not filter sygus solutions.\n\
 517 \n\
 518 strong \n\
 519 + Filter solutions that are logically stronger than others.\n\
 520 \n\
 521 weak \n\
 522 + Filter solutions that are logically weaker than others.\n\
 523 \n\
 524 ";
 525
 526 const std::string OptionsHandler::s_sygusInvTemplHelp = "\
 527 Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\
 528 \n\
 529 none  \n\
 530 + Synthesize invariant directly.\n\
 531 \n\
 532 pre  \n\
 533 + Synthesize invariant based on weakening of precondition .\n\
 534 \n\
 535 post \n\
 536 + Synthesize invariant based on strengthening of postcondition. \n\
 537 \n\
 538 ";
 539
 540 const std::string OptionsHandler::s_sygusActiveGenHelp =
 541     "\
 542 Modes for actively-generated sygus enumerators, supported by --sygus-active-gen:\n\
 543 \n\
 544 none  \n\
 545 + Do not use actively-generated sygus enumerators.\n\
 546 \n\
 547 basic  \n\
 548 + Use basic type enumerator for actively-generated sygus enumerators.\n\
 549 \n\
 550 enum  \n\
 551 + Use optimized enumerator for actively-generated sygus enumerators.\n\
 552 \n\
 553 var-agnostic \n\
 554 + Use sygus solver to enumerate terms that are agnostic to variables. \n\
 555 \n\
 556 auto (default) \n\
 557 + Internally decide the best policy for each enumerator. \n\
 558 \n\
 559 ";
 560
 561 const std::string OptionsHandler::s_macrosQuantHelp = "\
 562 Modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\
 563 \n\
 564 all \n\
 565 + Infer definitions for functions, including those containing quantified formulas.\n\
 566 \n\
 567 ground (default) \n\
 568 + Only infer ground definitions for functions.\n\
 569 \n\
 570 ground-uf \n\
 571 + Only infer ground definitions for functions that result in triggers for all free variables.\n\
 572 \n\
 573 ";
 574
 575 const std::string OptionsHandler::s_quantDSplitHelp = "\
 576 Modes for quantifiers splitting, supported by --quant-dsplit-mode:\n\
 577 \n\
 578 none \n\
 579 + Never split quantified formulas.\n\
 580 \n\
 581 default \n\
 582 + Split quantified formulas over some finite datatypes when finite model finding is enabled.\n\
 583 \n\
 584 agg \n\
 585 + Aggressively split quantified formulas.\n\
 586 \n\
 587 ";
 588
 589 const std::string OptionsHandler::s_quantRepHelp = "\
 590 Modes for quantifiers representative selection, supported by --quant-rep-mode:\n\
 591 \n\
 592 ee \n\
 593 + Let equality engine choose representatives.\n\
 594 \n\
 595 first (default) \n\
 596 + Choose terms that appear first.\n\
 597 \n\
 598 depth \n\
 599 + Choose terms that are of minimal depth.\n\
 600 \n\
 601 ";
 602
 603 theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(
 604     std::string option, std::string optarg)
 605 {
 606   if(optarg == "pre-full") {
 607     return theory::quantifiers::INST_WHEN_PRE_FULL;
 608   } else if(optarg == "full") {
 609     return theory::quantifiers::INST_WHEN_FULL;
 610   } else if(optarg == "full-delay") {
 611     return theory::quantifiers::INST_WHEN_FULL_DELAY;
 612   } else if(optarg == "full-last-call") {
 613     return theory::quantifiers::INST_WHEN_FULL_LAST_CALL;
 614   } else if(optarg == "full-delay-last-call") {
 615     return theory::quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL;
 616   } else if(optarg == "last-call") {
 617     return theory::quantifiers::INST_WHEN_LAST_CALL;
 618   } else if(optarg == "help") {
 619     puts(s_instWhenHelp.c_str());
 620     exit(1);
 621   } else {
 622     throw OptionException(std::string("unknown option for --inst-when: `") +
 623                           optarg + "'.  Try --inst-when help.");
 624   }
 625 }
 626
 627 void OptionsHandler::checkInstWhenMode(std::string option,
 628                                        theory::quantifiers::InstWhenMode mode)
 629 {
 630   if(mode == theory::quantifiers::INST_WHEN_PRE_FULL) {
 631     throw OptionException(std::string("Mode pre-full for ") + option + " is not supported in this release.");
 632   }
 633 }
 634
 635 theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(
 636     std::string option, std::string optarg)
 637 {
 638   if(optarg ==  "none") {
 639     return theory::quantifiers::LITERAL_MATCH_NONE;
 640   } else if(optarg ==  "use") {
 641     return theory::quantifiers::LITERAL_MATCH_USE;
 642   } else if(optarg ==  "agg-predicate") {
 643     return theory::quantifiers::LITERAL_MATCH_AGG_PREDICATE;
 644   } else if(optarg ==  "agg") {
 645     return theory::quantifiers::LITERAL_MATCH_AGG;
 646   } else if(optarg ==  "help") {
 647     puts(s_literalMatchHelp.c_str());
 648     exit(1);
 649   } else {
 650     throw OptionException(std::string("unknown option for --literal-matching: `") +
 651                           optarg + "'.  Try --literal-matching help.");
 652   }
 653 }
 654
 655 void OptionsHandler::checkLiteralMatchMode(
 656     std::string option, theory::quantifiers::LiteralMatchMode mode)
 657 {
 658 }
 659
 660 theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode(
 661     std::string option, std::string optarg)
 662 {
 663   if(optarg == "gen-ev") {
 664     return theory::quantifiers::MBQI_GEN_EVAL;
 665   } else if(optarg == "none") {
 666     return theory::quantifiers::MBQI_NONE;
 667   } else if(optarg == "default" || optarg ==  "fmc") {
 668     return theory::quantifiers::MBQI_FMC;
 669   } else if(optarg == "abs") {
 670     return theory::quantifiers::MBQI_ABS;
 671   } else if(optarg == "trust") {
 672     return theory::quantifiers::MBQI_TRUST;
 673   } else if(optarg == "help") {
 674     puts(s_mbqiModeHelp.c_str());
 675     exit(1);
 676   } else {
 677     throw OptionException(std::string("unknown option for --mbqi: `") +
 678                           optarg + "'.  Try --mbqi help.");
 679   }
 680 }
 681
 682 void OptionsHandler::checkMbqiMode(std::string option,
 683                                    theory::quantifiers::MbqiMode mode)
 684 {
 685 }
 686
 687 theory::quantifiers::QcfWhenMode OptionsHandler::stringToQcfWhenMode(
 688     std::string option, std::string optarg)
 689 {
 690   if(optarg ==  "default") {
 691     return theory::quantifiers::QCF_WHEN_MODE_DEFAULT;
 692   } else if(optarg ==  "last-call") {
 693     return theory::quantifiers::QCF_WHEN_MODE_LAST_CALL;
 694   } else if(optarg ==  "std") {
 695     return theory::quantifiers::QCF_WHEN_MODE_STD;
 696   } else if(optarg ==  "std-h") {
 697     return theory::quantifiers::QCF_WHEN_MODE_STD_H;
 698   } else if(optarg ==  "help") {
 699     puts(s_qcfWhenModeHelp.c_str());
 700     exit(1);
 701   } else {
 702     throw OptionException(std::string("unknown option for --quant-cf-when: `") +
 703                           optarg + "'.  Try --quant-cf-when help.");
 704   }
 705 }
 706
 707 theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option,
 708                                                              std::string optarg)
 709 {
 710   if(optarg ==  "conflict") {
 711     return theory::quantifiers::QCF_CONFLICT_ONLY;
 712   } else if(optarg ==  "default" || optarg == "prop-eq") {
 713     return theory::quantifiers::QCF_PROP_EQ;
 714   } else if(optarg ==  "help") {
 715     puts(s_qcfModeHelp.c_str());
 716     exit(1);
 717   } else {
 718     throw OptionException(std::string("unknown option for --quant-cf-mode: `") +
 719                           optarg + "'.  Try --quant-cf-mode help.");
 720   }
 721 }
 722
 723 theory::quantifiers::UserPatMode OptionsHandler::stringToUserPatMode(
 724     std::string option, std::string optarg)
 725 {
 726   if(optarg == "use") {
 727     return theory::quantifiers::USER_PAT_MODE_USE;
 728   } else if(optarg ==  "default" || optarg == "trust") {
 729     return theory::quantifiers::USER_PAT_MODE_TRUST;
 730   } else if(optarg == "resort") {
 731     return theory::quantifiers::USER_PAT_MODE_RESORT;
 732   } else if(optarg == "ignore") {
 733     return theory::quantifiers::USER_PAT_MODE_IGNORE;
 734   } else if(optarg == "interleave") {
 735     return theory::quantifiers::USER_PAT_MODE_INTERLEAVE;
 736   } else if(optarg ==  "help") {
 737     puts(s_userPatModeHelp.c_str());
 738     exit(1);
 739   } else {
 740     throw OptionException(std::string("unknown option for --user-pat: `") +
 741                           optarg + "'.  Try --user-pat help.");
 742   }
 743 }
 744
 745 theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(
 746     std::string option, std::string optarg)
 747 {
 748   if(optarg ==  "default" || optarg == "min") {
 749     return theory::quantifiers::TRIGGER_SEL_MIN;
 750   } else if(optarg == "max") {
 751     return theory::quantifiers::TRIGGER_SEL_MAX;
 752   } else if(optarg == "min-s-max") {
 753     return theory::quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX;
 754   } else if(optarg == "min-s-all") {
 755     return theory::quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL;
 756   } else if(optarg == "all") {
 757     return theory::quantifiers::TRIGGER_SEL_ALL;
 758   } else if(optarg ==  "help") {
 759     puts(s_triggerSelModeHelp.c_str());
 760     exit(1);
 761   } else {
 762     throw OptionException(std::string("unknown option for --trigger-sel: `") +
 763                           optarg + "'.  Try --trigger-sel help.");
 764   }
 765 }
 766
 767 theory::quantifiers::TriggerActiveSelMode
 768 OptionsHandler::stringToTriggerActiveSelMode(std::string option,
 769                                              std::string optarg)
 770 {
 771   if(optarg ==  "default" || optarg == "all") {
 772     return theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL;
 773   } else if(optarg == "min") {
 774     return theory::quantifiers::TRIGGER_ACTIVE_SEL_MIN;
 775   } else if(optarg == "max") {
 776     return theory::quantifiers::TRIGGER_ACTIVE_SEL_MAX;
 777   } else if(optarg ==  "help") {
 778     puts(s_triggerActiveSelModeHelp.c_str());
 779     exit(1);
 780   } else {
 781     throw OptionException(std::string("unknown option for --trigger-active-sel: `") +
 782                           optarg + "'.  Try --trigger-active-sel help.");
 783   }
 784 }
 785
 786 theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode(
 787     std::string option, std::string optarg)
 788 {
 789   if(optarg== "default" || optarg== "simple" ) {
 790     return theory::quantifiers::PRENEX_QUANT_SIMPLE;
 791   } else if(optarg == "none") {
 792     return theory::quantifiers::PRENEX_QUANT_NONE;
 793   } else if(optarg == "dnorm") {
 794     return theory::quantifiers::PRENEX_QUANT_DISJ_NORMAL;
 795   } else if(optarg == "norm") {
 796     return theory::quantifiers::PRENEX_QUANT_NORMAL;
 797   } else if(optarg ==  "help") {
 798     puts(s_prenexQuantModeHelp.c_str());
 799     exit(1);
 800   } else {
 801     throw OptionException(std::string("unknown option for --prenex-quant: `") +
 802                           optarg + "'.  Try --prenex-quant help.");
 803   }
 804 }
 805
 806 theory::SygusFairMode OptionsHandler::stringToSygusFairMode(std::string option,
 807                                                             std::string optarg)
 808 {
 809   if(optarg == "direct") {
 810     return theory::SYGUS_FAIR_DIRECT;
 811   } else if(optarg == "default" || optarg == "dt-size") {
 812     return theory::SYGUS_FAIR_DT_SIZE;
 813   } else if(optarg == "dt-height-bound" ){
 814     return theory::SYGUS_FAIR_DT_HEIGHT_PRED;
 815   } else if(optarg == "dt-size-bound" ){
 816     return theory::SYGUS_FAIR_DT_SIZE_PRED;
 817   } else if(optarg == "none") {
 818     return theory::SYGUS_FAIR_NONE;
 819   } else if(optarg ==  "help") {
 820     puts(s_cegqiFairModeHelp.c_str());
 821     exit(1);
 822   } else {
 823     throw OptionException(std::string("unknown option for --cegqi-fair: `") +
 824                           optarg + "'.  Try --cegqi-fair help.");
 825   }
 826 }
 827
 828 theory::quantifiers::TermDbMode OptionsHandler::stringToTermDbMode(
 829     std::string option, std::string optarg)
 830 {
 831   if(optarg == "all" ) {
 832     return theory::quantifiers::TERM_DB_ALL;
 833   } else if(optarg == "relevant") {
 834     return theory::quantifiers::TERM_DB_RELEVANT;
 835   } else if(optarg ==  "help") {
 836     puts(s_termDbModeHelp.c_str());
 837     exit(1);
 838   } else {
 839     throw OptionException(std::string("unknown option for --term-db-mode: `") +
 840                           optarg + "'.  Try --term-db-mode help.");
 841   }
 842 }
 843
 844 theory::quantifiers::IteLiftQuantMode OptionsHandler::stringToIteLiftQuantMode(
 845     std::string option, std::string optarg)
 846 {
 847   if(optarg == "all" ) {
 848     return theory::quantifiers::ITE_LIFT_QUANT_MODE_ALL;
 849   } else if(optarg == "simple") {
 850     return theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE;
 851   } else if(optarg == "none") {
 852     return theory::quantifiers::ITE_LIFT_QUANT_MODE_NONE;
 853   } else if(optarg ==  "help") {
 854     puts(s_iteLiftQuantHelp.c_str());
 855     exit(1);
 856   } else {
 857     throw OptionException(std::string("unknown option for --ite-lift-quant: `") +
 858                           optarg + "'.  Try --ite-lift-quant help.");
 859   }
 860 }
 861
 862 theory::quantifiers::CbqiBvIneqMode OptionsHandler::stringToCbqiBvIneqMode(
 863     std::string option, std::string optarg)
 864 {
 865   if (optarg == "eq-slack")
 866   {
 867     return theory::quantifiers::CBQI_BV_INEQ_EQ_SLACK;
 868   }
 869   else if (optarg == "eq-boundary")
 870   {
 871     return theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY;
 872   }
 873   else if (optarg == "keep")
 874   {
 875     return theory::quantifiers::CBQI_BV_INEQ_KEEP;
 876   }
 877   else if (optarg == "help")
 878   {
 879     puts(s_cbqiBvIneqModeHelp.c_str());
 880     exit(1);
 881   }
 882   else
 883   {
 884     throw OptionException(std::string("unknown option for --cbqi-bv-ineq: `")
 885                           + optarg
 886                           + "'.  Try --cbqi-bv-ineq help.");
 887   }
 888 }
 889
 890 theory::quantifiers::CegqiSingleInvMode
 891 OptionsHandler::stringToCegqiSingleInvMode(std::string option,
 892                                            std::string optarg)
 893 {
 894   if(optarg == "none" ) {
 895     return theory::quantifiers::CEGQI_SI_MODE_NONE;
 896   } else if(optarg == "use" || optarg == "default") {
 897     return theory::quantifiers::CEGQI_SI_MODE_USE;
 898   } else if(optarg == "all") {
 899     return theory::quantifiers::CEGQI_SI_MODE_ALL;
 900   } else if(optarg ==  "help") {
 901     puts(s_cegqiSingleInvHelp.c_str());
 902     exit(1);
 903   } else {
 904     throw OptionException(std::string("unknown option for --cegqi-si: `") +
 905                           optarg + "'.  Try --cegqi-si help.");
 906   }
 907 }
 908
 909 theory::quantifiers::CegqiSingleInvRconsMode
 910 OptionsHandler::stringToCegqiSingleInvRconsMode(std::string option,
 911                                                 std::string optarg)
 912 {
 913   if (optarg == "none")
 914   {
 915     return theory::quantifiers::CEGQI_SI_RCONS_MODE_NONE;
 916   }
 917   else if (optarg == "try")
 918   {
 919     return theory::quantifiers::CEGQI_SI_RCONS_MODE_TRY;
 920   }
 921   else if (optarg == "all")
 922   {
 923     return theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL;
 924   }
 925   else if (optarg == "all-limit")
 926   {
 927     return theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL_LIMIT;
 928   }
 929   else if (optarg == "help")
 930   {
 931     puts(s_cegqiSingleInvRconsHelp.c_str());
 932     exit(1);
 933   }
 934   else
 935   {
 936     throw OptionException(std::string("unknown option for --cegqi-si-rcons: `")
 937                           + optarg + "'.  Try --cegqi-si-rcons help.");
 938   }
 939 }
 940
 941 theory::quantifiers::CegisSampleMode OptionsHandler::stringToCegisSampleMode(
 942     std::string option, std::string optarg)
 943 {
 944   if (optarg == "none")
 945   {
 946     return theory::quantifiers::CEGIS_SAMPLE_NONE;
 947   }
 948   else if (optarg == "use")
 949   {
 950     return theory::quantifiers::CEGIS_SAMPLE_USE;
 951   }
 952   else if (optarg == "trust")
 953   {
 954     return theory::quantifiers::CEGIS_SAMPLE_TRUST;
 955   }
 956   else if (optarg == "help")
 957   {
 958     puts(s_cegisSampleHelp.c_str());
 959     exit(1);
 960   }
 961   else
 962   {
 963     throw OptionException(std::string("unknown option for --cegis-sample: `")
 964                           + optarg
 965                           + "'.  Try --cegis-sample help.");
 966   }
 967 }
 968
 969 theory::quantifiers::SygusFilterSolMode
 970 OptionsHandler::stringToSygusFilterSolMode(std::string option,
 971                                            std::string optarg)
 972 {
 973   if (optarg == "none")
 974   {
 975     return theory::quantifiers::SYGUS_FILTER_SOL_NONE;
 976   }
 977   else if (optarg == "strong")
 978   {
 979     return theory::quantifiers::SYGUS_FILTER_SOL_STRONG;
 980   }
 981   else if (optarg == "weak")
 982   {
 983     return theory::quantifiers::SYGUS_FILTER_SOL_WEAK;
 984   }
 985   else if (optarg == "help")
 986   {
 987     puts(s_cegisSampleHelp.c_str());
 988     exit(1);
 989   }
 990   else
 991   {
 992     throw OptionException(
 993         std::string("unknown option for --sygus-filter-sol: `") + optarg
 994         + "'.  Try --sygus-filter-sol help.");
 995   }
 996 }
 997
 998 theory::quantifiers::SygusInvTemplMode
 999 OptionsHandler::stringToSygusInvTemplMode(std::string option,
1000                                           std::string optarg)
1001 {
1002   if(optarg == "none" ) {
1003     return theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE;
1004   } else if(optarg == "pre") {
1005     return theory::quantifiers::SYGUS_INV_TEMPL_MODE_PRE;
1006   } else if(optarg == "post") {
1007     return theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST;
1008   } else if(optarg ==  "help") {
1009     puts(s_sygusInvTemplHelp.c_str());
1010     exit(1);
1011   } else {
1012     throw OptionException(std::string("unknown option for --sygus-inv-templ: `") +
1013                           optarg + "'.  Try --sygus-inv-templ help.");
1014   }
1015 }
1016
1017 theory::quantifiers::SygusActiveGenMode
1018 OptionsHandler::stringToSygusActiveGenMode(std::string option,
1019                                            std::string optarg)
1020 {
1021   if (optarg == "none")
1022   {
1023     return theory::quantifiers::SYGUS_ACTIVE_GEN_NONE;
1024   }
1025   else if (optarg == "basic")
1026   {
1027     return theory::quantifiers::SYGUS_ACTIVE_GEN_ENUM_BASIC;
1028   }
1029   else if (optarg == "enum")
1030   {
1031     return theory::quantifiers::SYGUS_ACTIVE_GEN_ENUM;
1032   }
1033   else if (optarg == "var-agnostic")
1034   {
1035     return theory::quantifiers::SYGUS_ACTIVE_GEN_VAR_AGNOSTIC;
1036   }
1037   else if (optarg == "auto")
1038   {
1039     return theory::quantifiers::SYGUS_ACTIVE_GEN_AUTO;
1040   }
1041   else if (optarg == "help")
1042   {
1043     puts(s_sygusActiveGenHelp.c_str());
1044     exit(1);
1045   }
1046   else
1047   {
1048     throw OptionException(std::string("unknown option for --sygus-inv-templ: `")
1049                           + optarg + "'.  Try --sygus-inv-templ help.");
1050   }
1051 }
1052
1053 theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode(
1054     std::string option, std::string optarg)
1055 {
1056   if(optarg == "all" ) {
1057     return theory::quantifiers::MACROS_QUANT_MODE_ALL;
1058   } else if(optarg == "ground") {
1059     return theory::quantifiers::MACROS_QUANT_MODE_GROUND;
1060   } else if(optarg == "ground-uf") {
1061     return theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF;
1062   } else if(optarg ==  "help") {
1063     puts(s_macrosQuantHelp.c_str());
1064     exit(1);
1065   } else {
1066     throw OptionException(std::string("unknown option for --macros-quant-mode: `") +
1067                           optarg + "'.  Try --macros-quant-mode help.");
1068   }
1069 }
1070
1071 theory::quantifiers::QuantDSplitMode OptionsHandler::stringToQuantDSplitMode(
1072     std::string option, std::string optarg)
1073 {
1074   if(optarg == "none" ) {
1075     return theory::quantifiers::QUANT_DSPLIT_MODE_NONE;
1076   } else if(optarg == "default") {
1077     return theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT;
1078   } else if(optarg == "agg") {
1079     return theory::quantifiers::QUANT_DSPLIT_MODE_AGG;
1080   } else if(optarg ==  "help") {
1081     puts(s_quantDSplitHelp.c_str());
1082     exit(1);
1083   } else {
1084     throw OptionException(std::string("unknown option for --quant-dsplit-mode: `") +
1085                           optarg + "'.  Try --quant-dsplit-mode help.");
1086   }
1087 }
1088
1089 theory::quantifiers::QuantRepMode OptionsHandler::stringToQuantRepMode(
1090     std::string option, std::string optarg)
1091 {
1092   if(optarg == "none" ) {
1093     return theory::quantifiers::QUANT_REP_MODE_EE;
1094   } else if(optarg == "first" || optarg == "default") {
1095     return theory::quantifiers::QUANT_REP_MODE_FIRST;
1096   } else if(optarg == "depth") {
1097     return theory::quantifiers::QUANT_REP_MODE_DEPTH;
1098   } else if(optarg ==  "help") {
1099     puts(s_quantRepHelp.c_str());
1100     exit(1);
1101   } else {
1102     throw OptionException(std::string("unknown option for --quant-rep-mode: `") +
1103                           optarg + "'.  Try --quant-rep-mode help.");
1104   }
1105 }
1106
1107 // theory/bv/options_handlers.h
1108 void OptionsHandler::abcEnabledBuild(std::string option, bool value)
1109 {
1110 #ifndef CVC4_USE_ABC
1111   if(value) {
1112     std::stringstream ss;
1113     ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
1114     throw OptionException(ss.str());
1115   }
1116 #endif /* CVC4_USE_ABC */
1117 }
1118
1119 void OptionsHandler::abcEnabledBuild(std::string option, std::string value)
1120 {
1121 #ifndef CVC4_USE_ABC
1122   if(!value.empty()) {
1123     std::stringstream ss;
1124     ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
1125     throw OptionException(ss.str());
1126   }
1127 #endif /* CVC4_USE_ABC */
1128 }
1129
1130 void OptionsHandler::satSolverEnabledBuild(std::string option, bool value)
1131 {
1132 #if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL)
1133   if (value)
1134   {
1135     std::stringstream ss;
1136     ss << "option `" << option
1137        << "' requires a CVC4 to be built with CryptoMiniSat or CaDiCaL";
1138     throw OptionException(ss.str());
1139   }
1140 #endif
1141 }
1142
1143 void OptionsHandler::satSolverEnabledBuild(std::string option,
1144                                            std::string value)
1145 {
1146 #if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL)
1147   if (!value.empty())
1148   {
1149     std::stringstream ss;
1150     ss << "option `" << option
1151        << "' requires a CVC4 to be built with CryptoMiniSat or CaDiCaL";
1152     throw OptionException(ss.str());
1153   }
1154 #endif
1155 }
1156
1157 const std::string OptionsHandler::s_bvSatSolverHelp = "\
1158 Sat solvers currently supported by the --bv-sat-solver option:\n\
1159 \n\
1160 minisat (default)\n\
1161 \n\
1162 cadical\n\
1163 \n\
1164 cryptominisat\n\
1165 ";
1166
1167 theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option,
1168                                                             std::string optarg)
1169 {
1170   if(optarg == "minisat") {
1171     return theory::bv::SAT_SOLVER_MINISAT;
1172   } else if(optarg == "cryptominisat") {
1173     if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY &&
1174         options::bitblastMode.wasSetByUser()) {
1175       throwLazyBBUnsupported(theory::bv::SAT_SOLVER_CRYPTOMINISAT);
1176     }
1177     if (!options::bitvectorToBool.wasSetByUser()) {
1178       options::bitvectorToBool.set(true);
1179     }
1180     return theory::bv::SAT_SOLVER_CRYPTOMINISAT;
1181   }
1182   else if (optarg == "cadical")
1183   {
1184     if (options::incrementalSolving()
1185         && options::incrementalSolving.wasSetByUser())
1186     {
1187       throw OptionException(
1188           std::string("CaDiCaL does not support incremental mode. \n\
1189                          Try --bv-sat-solver=cryptominisat or "
1190                       "--bv-sat-solver=minisat"));
1191     }
1192
1193     if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY
1194         && options::bitblastMode.wasSetByUser())
1195     {
1196       throwLazyBBUnsupported(theory::bv::SAT_SOLVER_CADICAL);
1197     }
1198     if (!options::bitvectorToBool.wasSetByUser())
1199     {
1200       options::bitvectorToBool.set(true);
1201     }
1202     return theory::bv::SAT_SOLVER_CADICAL;
1203   } else if(optarg == "help") {
1204     puts(s_bvSatSolverHelp.c_str());
1205     exit(1);
1206   } else {
1207     throw OptionException(std::string("unknown option for --bv-sat-solver: `") +
1208                           optarg + "'.  Try --bv-sat-solver=help.");
1209   }
1210 }
1211
1212 const std::string OptionsHandler::s_bitblastingModeHelp = "\
1213 Bit-blasting modes currently supported by the --bitblast option:\n\
1214 \n\
1215 lazy (default)\n\
1216 + Separate boolean structure and term reasoning between the core\n\
1217   SAT solver and the bv SAT solver\n\
1218 \n\
1219 eager\n\
1220 + Bitblast eagerly to bv SAT solver\n\
1221 ";
1222
1223 theory::bv::BitblastMode OptionsHandler::stringToBitblastMode(
1224     std::string option, std::string optarg)
1225 {
1226   if(optarg == "lazy") {
1227     if (!options::bitvectorPropagate.wasSetByUser()) {
1228       options::bitvectorPropagate.set(true);
1229     }
1230     if (!options::bitvectorEqualitySolver.wasSetByUser()) {
1231       options::bitvectorEqualitySolver.set(true);
1232     }
1233     if (!options::bitvectorEqualitySlicer.wasSetByUser()) {
1234       if (options::incrementalSolving() ||
1235           options::produceModels()) {
1236         options::bitvectorEqualitySlicer.set(theory::bv::BITVECTOR_SLICER_OFF);
1237       } else {
1238         options::bitvectorEqualitySlicer.set(theory::bv::BITVECTOR_SLICER_AUTO);
1239       }
1240     }
1241
1242     if (!options::bitvectorInequalitySolver.wasSetByUser()) {
1243       options::bitvectorInequalitySolver.set(true);
1244     }
1245     if (!options::bitvectorAlgebraicSolver.wasSetByUser()) {
1246       options::bitvectorAlgebraicSolver.set(true);
1247     }
1248     if (options::bvSatSolver() != theory::bv::SAT_SOLVER_MINISAT)
1249     {
1250       throwLazyBBUnsupported(options::bvSatSolver());
1251     }
1252     return theory::bv::BITBLAST_MODE_LAZY;
1253   } else if(optarg == "eager") {
1254     if (!options::bitvectorToBool.wasSetByUser()) {
1255       options::bitvectorToBool.set(true);
1256     }
1257
1258     if (!options::bvAbstraction.wasSetByUser() &&
1259         !options::skolemizeArguments.wasSetByUser()) {
1260       options::bvAbstraction.set(true);
1261       options::skolemizeArguments.set(true);
1262     }
1263     return theory::bv::BITBLAST_MODE_EAGER;
1264   } else if(optarg == "help") {
1265     puts(s_bitblastingModeHelp.c_str());
1266     exit(1);
1267   } else {
1268     throw OptionException(std::string("unknown option for --bitblast: `") +
1269                           optarg + "'.  Try --bitblast=help.");
1270   }
1271 }
1272
1273 const std::string OptionsHandler::s_bvSlicerModeHelp = "\
1274 Bit-vector equality slicer modes supported by the --bv-eq-slicer option:\n\
1275 \n\
1276 auto (default)\n\
1277 + Turn slicer on if input has only equalities over core symbols\n\
1278 \n\
1279 on\n\
1280 + Turn slicer on\n\
1281 \n\
1282 off\n\
1283 + Turn slicer off\n\
1284 ";
1285
1286 theory::bv::BvSlicerMode OptionsHandler::stringToBvSlicerMode(
1287     std::string option, std::string optarg)
1288 {
1289   if(optarg == "auto") {
1290     return theory::bv::BITVECTOR_SLICER_AUTO;
1291   } else if(optarg == "on") {
1292     return theory::bv::BITVECTOR_SLICER_ON;
1293   } else if(optarg == "off") {
1294     return theory::bv::BITVECTOR_SLICER_OFF;
1295   } else if(optarg == "help") {
1296     puts(s_bvSlicerModeHelp.c_str());
1297     exit(1);
1298   } else {
1299     throw OptionException(std::string("unknown option for --bv-eq-slicer: `") +
1300                           optarg + "'.  Try --bv-eq-slicer=help.");
1301   }
1302 }
1303
1304 const std::string OptionsHandler::s_boolToBVModeHelp =
1305     "\
1306 BoolToBV pass modes supported by the --bool-to-bv option:\n\
1307 \n\
1308 off (default)\n\
1309 + Don't push any booleans to width one bit-vectors\n\
1310 \n\
1311 ite\n\
1312 + Try to turn ITEs into BITVECTOR_ITE when possible. It can fail per-formula \n\
1313   if not all sub-formulas can be turned to bit-vectors\n\
1314 \n\
1315 all\n\
1316 + Force all booleans to be bit-vectors of width one except at the top level.\n\
1317   Most aggressive mode\n\
1318 ";
1319
1320 preprocessing::passes::BoolToBVMode OptionsHandler::stringToBoolToBVMode(
1321     std::string option, std::string optarg)
1322 {
1323   if (optarg == "off")
1324   {
1325     return preprocessing::passes::BOOL_TO_BV_OFF;
1326   }
1327   else if (optarg == "ite")
1328   {
1329     return preprocessing::passes::BOOL_TO_BV_ITE;
1330   }
1331   else if (optarg == "all")
1332   {
1333     return preprocessing::passes::BOOL_TO_BV_ALL;
1334   }
1335   else if (optarg == "help")
1336   {
1337     puts(s_boolToBVModeHelp.c_str());
1338     exit(1);
1339   }
1340   else
1341   {
1342     throw OptionException(std::string("unknown option for --bool-to-bv: `")
1343                           + optarg
1344                           + "'. Try --bool-to-bv=help");
1345   }
1346 }
1347
1348 void OptionsHandler::setBitblastAig(std::string option, bool arg)
1349 {
1350   if(arg) {
1351     if(options::bitblastMode.wasSetByUser()) {
1352       if(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER) {
1353         throw OptionException("bitblast-aig must be used with eager bitblaster");
1354       }
1355     } else {
1356       theory::bv::BitblastMode mode = stringToBitblastMode("", "eager");
1357       options::bitblastMode.set(mode);
1358     }
1359     if(!options::bitvectorAigSimplifications.wasSetByUser()) {
1360       options::bitvectorAigSimplifications.set("balance;drw");
1361     }
1362   }
1363 }
1364
1365 // theory/uf/options_handlers.h
1366 const std::string OptionsHandler::s_ufssModeHelp = "\
1367 UF strong solver options currently supported by the --uf-ss option:\n\
1368 \n\
1369 full \n\
1370 + Default, use uf strong solver to find minimal models for uninterpreted sorts.\n\
1371 \n\
1372 no-minimal \n\
1373 + Use uf strong solver to shrink model sizes, but do no enforce minimality.\n\
1374 \n\
1375 none \n\
1376 + Do not use uf strong solver to shrink model sizes. \n\
1377 \n\
1378 ";
1379
1380 theory::uf::UfssMode OptionsHandler::stringToUfssMode(std::string option,
1381                                                       std::string optarg)
1382 {
1383   if(optarg ==  "default" || optarg == "full" ) {
1384     return theory::uf::UF_SS_FULL;
1385   } else if(optarg == "no-minimal") {
1386     return theory::uf::UF_SS_NO_MINIMAL;
1387   } else if(optarg == "none") {
1388     return theory::uf::UF_SS_NONE;
1389   } else if(optarg ==  "help") {
1390     puts(s_ufssModeHelp.c_str());
1391     exit(1);
1392   } else {
1393     throw OptionException(std::string("unknown option for --uf-ss: `") +
1394                           optarg + "'.  Try --uf-ss help.");
1395   }
1396 }
1397
1398
1399
1400 // theory/options_handlers.h
1401 const std::string OptionsHandler::s_theoryOfModeHelp = "\
1402 TheoryOf modes currently supported by the --theoryof-mode option:\n\
1403 \n\
1404 type (default) \n\
1405 + type variables, constants and equalities by type\n\
1406 \n\
1407 term \n\
1408 + type variables as uninterpreted, equalities by the parametric theory\n\
1409 ";
1410
1411 theory::TheoryOfMode OptionsHandler::stringToTheoryOfMode(std::string option, std::string optarg) {
1412   if(optarg == "type") {
1413     return theory::THEORY_OF_TYPE_BASED;
1414   } else if(optarg == "term") {
1415     return theory::THEORY_OF_TERM_BASED;
1416   } else if(optarg == "help") {
1417     puts(s_theoryOfModeHelp.c_str());
1418     exit(1);
1419   } else {
1420     throw OptionException(std::string("unknown option for --theoryof-mode: `") +
1421                           optarg + "'.  Try --theoryof-mode help.");
1422   }
1423 }
1424
1425 // theory/options_handlers.h
1426 std::string OptionsHandler::handleUseTheoryList(std::string option, std::string optarg) {
1427   std::string currentList = options::useTheoryList();
1428   if(currentList.empty()){
1429     return optarg;
1430   } else {
1431     return currentList +','+ optarg;
1432   }
1433 }
1434
1435 void OptionsHandler::notifyUseTheoryList(std::string option) {
1436   d_options->d_useTheoryListListeners.notify();
1437 }
1438
1439
1440
1441 // printer/options_handlers.h
1442 const std::string OptionsHandler::s_modelFormatHelp = "\
1443 Model format modes currently supported by the --model-format option:\n\
1444 \n\
1445 default \n\
1446 + Print model as expressions in the output language format.\n\
1447 \n\
1448 table\n\
1449 + Print functional expressions over finite domains in a table format.\n\
1450 ";
1451
1452 const std::string OptionsHandler::s_instFormatHelp = "\
1453 Inst format modes currently supported by the --model-format option:\n\
1454 \n\
1455 default \n\
1456 + Print instantiations as a list in the output language format.\n\
1457 \n\
1458 szs\n\
1459 + Print instantiations as SZS compliant proof.\n\
1460 ";
1461
1462 ModelFormatMode OptionsHandler::stringToModelFormatMode(std::string option,
1463                                                         std::string optarg)
1464 {
1465   if(optarg == "default") {
1466     return MODEL_FORMAT_MODE_DEFAULT;
1467   } else if(optarg == "table") {
1468     return MODEL_FORMAT_MODE_TABLE;
1469   } else if(optarg == "help") {
1470     puts(s_modelFormatHelp.c_str());
1471     exit(1);
1472   } else {
1473     throw OptionException(std::string("unknown option for --model-format: `") +
1474                           optarg + "'.  Try --model-format help.");
1475   }
1476 }
1477
1478 InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option,
1479                                                       std::string optarg)
1480 {
1481   if(optarg == "default") {
1482     return INST_FORMAT_MODE_DEFAULT;
1483   } else if(optarg == "szs") {
1484     return INST_FORMAT_MODE_SZS;
1485   } else if(optarg == "help") {
1486     puts(s_instFormatHelp.c_str());
1487     exit(1);
1488   } else {
1489     throw OptionException(std::string("unknown option for --inst-format: `") +
1490                           optarg + "'.  Try --inst-format help.");
1491   }
1492 }
1493
1494
1495 // decision/options_handlers.h
1496 const std::string OptionsHandler::s_decisionModeHelp = "\
1497 Decision modes currently supported by the --decision option:\n\
1498 \n\
1499 internal (default)\n\
1500 + Use the internal decision heuristics of the SAT solver\n\
1501 \n\
1502 justification\n\
1503 + An ATGP-inspired justification heuristic\n\
1504 \n\
1505 justification-stoponly\n\
1506 + Use the justification heuristic only to stop early, not for decisions\n\
1507 ";
1508
1509 decision::DecisionMode OptionsHandler::stringToDecisionMode(std::string option,
1510                                                             std::string optarg)
1511 {
1512   options::decisionStopOnly.set(false);
1513
1514   if(optarg == "internal") {
1515     return decision::DECISION_STRATEGY_INTERNAL;
1516   } else if(optarg == "justification") {
1517     return decision::DECISION_STRATEGY_JUSTIFICATION;
1518   } else if(optarg == "justification-stoponly") {
1519     options::decisionStopOnly.set(true);
1520     return decision::DECISION_STRATEGY_JUSTIFICATION;
1521   } else if(optarg == "help") {
1522     puts(s_decisionModeHelp.c_str());
1523     exit(1);
1524   } else {
1525     throw OptionException(std::string("unknown option for --decision: `") +
1526                           optarg + "'.  Try --decision help.");
1527   }
1528 }
1529
1530 decision::DecisionWeightInternal OptionsHandler::stringToDecisionWeightInternal(
1531     std::string option, std::string optarg)
1532 {
1533   if(optarg == "off")
1534     return decision::DECISION_WEIGHT_INTERNAL_OFF;
1535   else if(optarg == "max")
1536     return decision::DECISION_WEIGHT_INTERNAL_MAX;
1537   else if(optarg == "sum")
1538     return decision::DECISION_WEIGHT_INTERNAL_SUM;
1539   else if(optarg == "usr1")
1540     return decision::DECISION_WEIGHT_INTERNAL_USR1;
1541   else
1542     throw OptionException(std::string("--decision-weight-internal must be off, max or sum."));
1543 }
1544
1545
1546 // smt/options_handlers.h
1547 const std::string OptionsHandler::s_simplificationHelp = "\
1548 Simplification modes currently supported by the --simplification option:\n\
1549 \n\
1550 batch (default) \n\
1551 + save up all ASSERTions; run nonclausal simplification and clausal\n\
1552   (MiniSat) propagation for all of them only after reaching a querying command\n\
1553   (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\
1554 \n\
1555 none\n\
1556 + do not perform nonclausal simplification\n\
1557 ";
1558
1559 SimplificationMode OptionsHandler::stringToSimplificationMode(
1560     std::string option, std::string optarg)
1561 {
1562   if(optarg == "batch") {
1563     return SIMPLIFICATION_MODE_BATCH;
1564   } else if(optarg == "none") {
1565     return SIMPLIFICATION_MODE_NONE;
1566   } else if(optarg == "help") {
1567     puts(s_simplificationHelp.c_str());
1568     exit(1);
1569   } else {
1570     throw OptionException(std::string("unknown option for --simplification: `") +
1571                           optarg + "'.  Try --simplification help.");
1572   }
1573 }
1574
1575 const std::string OptionsHandler::s_modelCoresHelp =
1576     "\
1577 Model cores modes currently supported by the --simplification option:\n\
1578 \n\
1579 none (default) \n\
1580 + do not compute model cores\n\
1581 \n\
1582 simple\n\
1583 + only include a subset of variables whose values are sufficient to show the\n\
1584 input formula is satisfied by the given model\n\
1585 \n\
1586 non-implied\n\
1587 + only include a subset of variables whose values, in addition to the values\n\
1588 of variables whose values are implied, are sufficient to show the input\n\
1589 formula is satisfied by the given model\n\
1590 \n\
1591 ";
1592
1593 ModelCoresMode OptionsHandler::stringToModelCoresMode(std::string option,
1594                                                       std::string optarg)
1595 {
1596   if (optarg == "none")
1597   {
1598     return MODEL_CORES_NONE;
1599   }
1600   else if (optarg == "simple")
1601   {
1602     return MODEL_CORES_SIMPLE;
1603   }
1604   else if (optarg == "non-implied")
1605   {
1606     return MODEL_CORES_NON_IMPLIED;
1607   }
1608   else if (optarg == "help")
1609   {
1610     puts(s_modelCoresHelp.c_str());
1611     exit(1);
1612   }
1613   else
1614   {
1615     throw OptionException(std::string("unknown option for --model-cores: `")
1616                           + optarg + "'.  Try --model-cores help.");
1617   }
1618 }
1619
1620 const std::string OptionsHandler::s_sygusSolutionOutModeHelp =
1621     "\
1622 Modes for finite model finding bound minimization, supported by --sygus-out:\n\
1623 \n\
1624 status \n\
1625 + Print only status for check-synth calls.\n\
1626 \n\
1627 status-and-def (default) \n\
1628 + Print status followed by definition corresponding to solution.\n\
1629 \n\
1630 status-or-def \n\
1631 + Print status if infeasible, or definition corresponding to\n\
1632   solution if feasible.\n\
1633 \n\
1634 sygus-standard \n\
1635 + Print based on SyGuS standard.\n\
1636 \n\
1637 ";
1638
1639 SygusSolutionOutMode OptionsHandler::stringToSygusSolutionOutMode(
1640     std::string option, std::string optarg)
1641 {
1642   if (optarg == "status")
1643   {
1644     return SYGUS_SOL_OUT_STATUS;
1645   }
1646   else if (optarg == "status-and-def")
1647   {
1648     return SYGUS_SOL_OUT_STATUS_AND_DEF;
1649   }
1650   else if (optarg == "status-or-def")
1651   {
1652     return SYGUS_SOL_OUT_STATUS_OR_DEF;
1653   }
1654   else if (optarg == "sygus-standard")
1655   {
1656     return SYGUS_SOL_OUT_STANDARD;
1657   }
1658   else if (optarg == "help")
1659   {
1660     puts(s_sygusSolutionOutModeHelp.c_str());
1661     exit(1);
1662   }
1663   else
1664   {
1665     throw OptionException(std::string("unknown option for --sygus-out: `")
1666                           + optarg
1667                           + "'.  Try --sygus-out help.");
1668   }
1669 }
1670
1671 void OptionsHandler::setProduceAssertions(std::string option, bool value)
1672 {
1673   options::produceAssertions.set(value);
1674   options::interactiveMode.set(value);
1675 }
1676
1677 void OptionsHandler::proofEnabledBuild(std::string option, bool value)
1678 {
1679 #ifdef CVC4_PROOF
1680   if (value && options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
1681       && options::bvSatSolver() != theory::bv::SAT_SOLVER_MINISAT)
1682   {
1683     throw OptionException(
1684         "Eager BV proofs only supported when minisat is used");
1685   }
1686 #else
1687   if(value) {
1688     std::stringstream ss;
1689     ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support";
1690     throw OptionException(ss.str());
1691   }
1692 #endif /* CVC4_PROOF */
1693 }
1694
1695 void OptionsHandler::LFSCEnabledBuild(std::string option, bool value) {
1696 #ifndef CVC4_USE_LFSC
1697   if (value) {
1698     std::stringstream ss;
1699     ss << "option `" << option << "' requires a build of CVC4 with integrated "
1700                                   "LFSC; this binary was not built with LFSC";
1701     throw OptionException(ss.str());
1702   }
1703 #endif /* CVC4_USE_LFSC */
1704 }
1705
1706 void OptionsHandler::notifyDumpToFile(std::string option) {
1707   d_options->d_dumpToFileListeners.notify();
1708 }
1709
1710
1711 void OptionsHandler::notifySetRegularOutputChannel(std::string option) {
1712   d_options->d_setRegularChannelListeners.notify();
1713 }
1714
1715 void OptionsHandler::notifySetDiagnosticOutputChannel(std::string option) {
1716   d_options->d_setDiagnosticChannelListeners.notify();
1717 }
1718
1719
1720 std::string OptionsHandler::checkReplayFilename(std::string option, std::string optarg) {
1721 #ifdef CVC4_REPLAY
1722   if(optarg == "") {
1723     throw OptionException (std::string("Bad file name for --replay"));
1724   } else {
1725     return optarg;
1726   }
1727 #else /* CVC4_REPLAY */
1728   throw OptionException("The replay feature was disabled in this build of CVC4.");
1729 #endif /* CVC4_REPLAY */
1730 }
1731
1732 void OptionsHandler::notifySetReplayLogFilename(std::string option) {
1733   d_options->d_setReplayFilenameListeners.notify();
1734 }
1735
1736 void OptionsHandler::statsEnabledBuild(std::string option, bool value)
1737 {
1738 #ifndef CVC4_STATISTICS_ON
1739   if(value) {
1740     std::stringstream ss;
1741     ss << "option `" << option << "' requires a statistics-enabled build of CVC4; this binary was not built with statistics support";
1742     throw OptionException(ss.str());
1743   }
1744 #endif /* CVC4_STATISTICS_ON */
1745 }
1746
1747 void OptionsHandler::threadN(std::string option) {
1748   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\"");
1749 }
1750
1751 void OptionsHandler::notifyDumpMode(std::string option)
1752 {
1753   d_options->d_setDumpModeListeners.notify();
1754 }
1755
1756
1757 // expr/options_handlers.h
1758 void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) {
1759   if(depth < -1) {
1760     throw OptionException("--default-expr-depth requires a positive argument, or -1.");
1761   }
1762 }
1763
1764 void OptionsHandler::setDefaultDagThreshPredicate(std::string option, int dag) {
1765   if(dag < 0) {
1766     throw OptionException("--default-dag-thresh requires a nonnegative argument.");
1767   }
1768 }
1769
1770 void OptionsHandler::notifySetDefaultExprDepth(std::string option) {
1771   d_options->d_setDefaultExprDepthListeners.notify();
1772 }
1773
1774 void OptionsHandler::notifySetDefaultDagThresh(std::string option) {
1775   d_options->d_setDefaultDagThreshListeners.notify();
1776 }
1777
1778 void OptionsHandler::notifySetPrintExprTypes(std::string option) {
1779   d_options->d_setPrintExprTypesListeners.notify();
1780 }
1781
1782
1783 // main/options_handlers.h
1784
1785 static void print_config (const char * str, std::string config) {
1786   std::string s(str);
1787   unsigned sz = 14;
1788   if (s.size() < sz) s.resize(sz, ' ');
1789   std::cout << s << ": " << config << std::endl;
1790 }
1791
1792 static void print_config_cond (const char * str, bool cond = false) {
1793   print_config(str, cond ? "yes" : "no");
1794 }
1795
1796 void OptionsHandler::copyright(std::string option) {
1797   std::cout << Configuration::copyright() << std::endl;
1798   exit(0);
1799 }
1800
1801 void OptionsHandler::showConfiguration(std::string option) {
1802   std::cout << Configuration::about() << std::endl;
1803
1804   print_config ("version", Configuration::getVersionString());
1805
1806   if(Configuration::isGitBuild()) {
1807     const char* branchName = Configuration::getGitBranchName();
1808     if(*branchName == '\0')  { branchName = "-"; }
1809     std::stringstream ss;
1810     ss << "git ["
1811        << branchName << " "
1812        << std::string(Configuration::getGitCommit()).substr(0, 8)
1813        << (Configuration::hasGitModifications() ? " (with modifications)" : "")
1814        << "]";
1815     print_config("scm", ss.str());
1816   } else {
1817     print_config_cond("scm", false);
1818   }
1819
1820   std::cout << std::endl;
1821
1822   std::stringstream ss;
1823   ss << Configuration::getVersionMajor() << "."
1824      << Configuration::getVersionMinor() << "."
1825      << Configuration::getVersionRelease();
1826   print_config("library", ss.str());
1827
1828   std::cout << std::endl;
1829
1830   print_config_cond("debug code", Configuration::isDebugBuild());
1831   print_config_cond("statistics", Configuration::isStatisticsBuild());
1832   print_config_cond("replay", Configuration::isReplayBuild());
1833   print_config_cond("tracing", Configuration::isTracingBuild());
1834   print_config_cond("dumping", Configuration::isDumpingBuild());
1835   print_config_cond("muzzled", Configuration::isMuzzledBuild());
1836   print_config_cond("assertions", Configuration::isAssertionBuild());
1837   print_config_cond("proof", Configuration::isProofBuild());
1838   print_config_cond("coverage", Configuration::isCoverageBuild());
1839   print_config_cond("profiling", Configuration::isProfilingBuild());
1840   print_config_cond("asan", Configuration::isAsanBuild());
1841   print_config_cond("competition", Configuration::isCompetitionBuild());
1842
1843   std::cout << std::endl;
1844
1845   print_config_cond("abc", Configuration::isBuiltWithAbc());
1846   print_config_cond("cln", Configuration::isBuiltWithCln());
1847   print_config_cond("glpk", Configuration::isBuiltWithGlpk());
1848   print_config_cond("cadical", Configuration::isBuiltWithCadical());
1849   print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
1850   print_config_cond("gmp", Configuration::isBuiltWithGmp());
1851   print_config_cond("lfsc", Configuration::isBuiltWithLfsc());
1852   print_config_cond("readline", Configuration::isBuiltWithReadline());
1853   print_config_cond("symfpu", Configuration::isBuiltWithSymFPU());
1854
1855   exit(0);
1856 }
1857
1858 static void printTags(unsigned ntags, char const* const* tags)
1859 {
1860   std::cout << "available tags:";
1861   for (unsigned i = 0; i < ntags; ++ i)
1862   {
1863     std::cout << "  " << tags[i] << std::endl;
1864   }
1865   std::cout << std::endl;
1866 }
1867
1868 void OptionsHandler::showDebugTags(std::string option)
1869 {
1870   if (!Configuration::isDebugBuild())
1871   {
1872     throw OptionException("debug tags not available in non-debug builds");
1873   }
1874   else if (!Configuration::isTracingBuild())
1875   {
1876     throw OptionException("debug tags not available in non-tracing builds");
1877   }
1878   printTags(Configuration::getNumDebugTags(),Configuration::getDebugTags());
1879   exit(0);
1880 }
1881
1882 void OptionsHandler::showTraceTags(std::string option)
1883 {
1884   if (!Configuration::isTracingBuild())
1885   {
1886     throw OptionException("trace tags not available in non-tracing build");
1887   }
1888   printTags(Configuration::getNumTraceTags(), Configuration::getTraceTags());
1889   exit(0);
1890 }
1891
1892 static std::string suggestTags(char const* const* validTags,
1893                                std::string inputTag,
1894                                char const* const* additionalTags)
1895 {
1896   DidYouMean didYouMean;
1897
1898   const char* opt;
1899   for (size_t i = 0; (opt = validTags[i]) != nullptr; ++i)
1900   {
1901     didYouMean.addWord(validTags[i]);
1902   }
1903   if (additionalTags != nullptr)
1904   {
1905     for (size_t i = 0; (opt = additionalTags[i]) != nullptr; ++i)
1906     {
1907       didYouMean.addWord(additionalTags[i]);
1908     }
1909   }
1910
1911   return didYouMean.getMatchAsString(inputTag);
1912 }
1913
1914 void OptionsHandler::enableTraceTag(std::string option, std::string optarg)
1915 {
1916   if(!Configuration::isTracingBuild())
1917   {
1918     throw OptionException("trace tags not available in non-tracing builds");
1919   }
1920   else if(!Configuration::isTraceTag(optarg.c_str()))
1921   {
1922     if (optarg == "help")
1923     {
1924       printTags(
1925           Configuration::getNumTraceTags(), Configuration::getTraceTags());
1926       exit(0);
1927     }
1928
1929     throw OptionException(
1930         std::string("trace tag ") + optarg + std::string(" not available.")
1931         + suggestTags(Configuration::getTraceTags(), optarg, nullptr));
1932   }
1933   Trace.on(optarg);
1934 }
1935
1936 void OptionsHandler::enableDebugTag(std::string option, std::string optarg)
1937 {
1938   if (!Configuration::isDebugBuild())
1939   {
1940     throw OptionException("debug tags not available in non-debug builds");
1941   }
1942   else if (!Configuration::isTracingBuild())
1943   {
1944     throw OptionException("debug tags not available in non-tracing builds");
1945   }
1946
1947   if (!Configuration::isDebugTag(optarg.c_str())
1948       && !Configuration::isTraceTag(optarg.c_str()))
1949   {
1950     if (optarg == "help")
1951     {
1952       printTags(
1953           Configuration::getNumDebugTags(), Configuration::getDebugTags());
1954       exit(0);
1955     }
1956
1957     throw OptionException(std::string("debug tag ") + optarg
1958                           + std::string(" not available.")
1959                           + suggestTags(Configuration::getDebugTags(),
1960                                         optarg,
1961                                         Configuration::getTraceTags()));
1962   }
1963   Debug.on(optarg);
1964   Trace.on(optarg);
1965 }
1966
1967 OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option,
1968                                                       std::string optarg)
1969 {
1970   if(optarg == "help") {
1971     options::languageHelp.set(true);
1972     return language::output::LANG_AUTO;
1973   }
1974
1975   try {
1976     return language::toOutputLanguage(optarg);
1977   } catch(OptionException& oe) {
1978     throw OptionException("Error in " + option + ": " + oe.getMessage() +
1979                           "\nTry --output-language help");
1980   }
1981
1982   Unreachable();
1983 }
1984
1985 InputLanguage OptionsHandler::stringToInputLanguage(std::string option,
1986                                                     std::string optarg)
1987 {
1988   if(optarg == "help") {
1989     options::languageHelp.set(true);
1990     return language::input::LANG_AUTO;
1991   }
1992
1993   try {
1994     return language::toInputLanguage(optarg);
1995   } catch(OptionException& oe) {
1996     throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --language help");
1997   }
1998
1999   Unreachable();
2000 }
2001
2002 /* options/base_options_handlers.h */
2003 void OptionsHandler::setVerbosity(std::string option, int value)
2004 {
2005   if(Configuration::isMuzzledBuild()) {
2006     DebugChannel.setStream(&CVC4::null_os);
2007     TraceChannel.setStream(&CVC4::null_os);
2008     NoticeChannel.setStream(&CVC4::null_os);
2009     ChatChannel.setStream(&CVC4::null_os);
2010     MessageChannel.setStream(&CVC4::null_os);
2011     WarningChannel.setStream(&CVC4::null_os);
2012   } else {
2013     if(value < 2) {
2014       ChatChannel.setStream(&CVC4::null_os);
2015     } else {
2016       ChatChannel.setStream(&std::cout);
2017     }
2018     if(value < 1) {
2019       NoticeChannel.setStream(&CVC4::null_os);
2020     } else {
2021       NoticeChannel.setStream(&std::cout);
2022     }
2023     if(value < 0) {
2024       MessageChannel.setStream(&CVC4::null_os);
2025       WarningChannel.setStream(&CVC4::null_os);
2026     } else {
2027       MessageChannel.setStream(&std::cout);
2028       WarningChannel.setStream(&std::cerr);
2029     }
2030   }
2031 }
2032
2033 void OptionsHandler::increaseVerbosity(std::string option) {
2034   options::verbosity.set(options::verbosity() + 1);
2035   setVerbosity(option, options::verbosity());
2036 }
2037
2038 void OptionsHandler::decreaseVerbosity(std::string option) {
2039   options::verbosity.set(options::verbosity() - 1);
2040   setVerbosity(option, options::verbosity());
2041 }
2042
2043
2044 }/* CVC4::options namespace */
2045 }/* CVC4 namespace */