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