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_sygusInvTemplHelp = "\
 512 Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\
 513 \n\
 514 none  \n\
 515 + Synthesize invariant directly.\n\
 516 \n\
 517 pre  \n\
 518 + Synthesize invariant based on weakening of precondition .\n\
 519 \n\
 520 post \n\
 521 + Synthesize invariant based on strengthening of postcondition. \n\
 522 \n\
 523 ";
 524
 525 const std::string OptionsHandler::s_sygusActiveGenHelp =
 526     "\
 527 Modes for actively-generated sygus enumerators, supported by --sygus-active-gen:\n\
 528 \n\
 529 none  \n\
 530 + Do not use actively-generated sygus enumerators.\n\
 531 \n\
 532 basic  \n\
 533 + Use basic type enumerator as sygus enumerator.\n\
 534 \n\
 535 var-agnostic \n\
 536 + Use sygus solver to enumerate terms that are agnostic to variables. \n\
 537 \n\
 538 ";
 539
 540 const std::string OptionsHandler::s_macrosQuantHelp = "\
 541 Modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\
 542 \n\
 543 all \n\
 544 + Infer definitions for functions, including those containing quantified formulas.\n\
 545 \n\
 546 ground (default) \n\
 547 + Only infer ground definitions for functions.\n\
 548 \n\
 549 ground-uf \n\
 550 + Only infer ground definitions for functions that result in triggers for all free variables.\n\
 551 \n\
 552 ";
 553
 554 const std::string OptionsHandler::s_quantDSplitHelp = "\
 555 Modes for quantifiers splitting, supported by --quant-dsplit-mode:\n\
 556 \n\
 557 none \n\
 558 + Never split quantified formulas.\n\
 559 \n\
 560 default \n\
 561 + Split quantified formulas over some finite datatypes when finite model finding is enabled.\n\
 562 \n\
 563 agg \n\
 564 + Aggressively split quantified formulas.\n\
 565 \n\
 566 ";
 567
 568 const std::string OptionsHandler::s_quantRepHelp = "\
 569 Modes for quantifiers representative selection, supported by --quant-rep-mode:\n\
 570 \n\
 571 ee \n\
 572 + Let equality engine choose representatives.\n\
 573 \n\
 574 first (default) \n\
 575 + Choose terms that appear first.\n\
 576 \n\
 577 depth \n\
 578 + Choose terms that are of minimal depth.\n\
 579 \n\
 580 ";
 581
 582 theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(
 583     std::string option, std::string optarg)
 584 {
 585   if(optarg == "pre-full") {
 586     return theory::quantifiers::INST_WHEN_PRE_FULL;
 587   } else if(optarg == "full") {
 588     return theory::quantifiers::INST_WHEN_FULL;
 589   } else if(optarg == "full-delay") {
 590     return theory::quantifiers::INST_WHEN_FULL_DELAY;
 591   } else if(optarg == "full-last-call") {
 592     return theory::quantifiers::INST_WHEN_FULL_LAST_CALL;
 593   } else if(optarg == "full-delay-last-call") {
 594     return theory::quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL;
 595   } else if(optarg == "last-call") {
 596     return theory::quantifiers::INST_WHEN_LAST_CALL;
 597   } else if(optarg == "help") {
 598     puts(s_instWhenHelp.c_str());
 599     exit(1);
 600   } else {
 601     throw OptionException(std::string("unknown option for --inst-when: `") +
 602                           optarg + "'.  Try --inst-when help.");
 603   }
 604 }
 605
 606 void OptionsHandler::checkInstWhenMode(std::string option,
 607                                        theory::quantifiers::InstWhenMode mode)
 608 {
 609   if(mode == theory::quantifiers::INST_WHEN_PRE_FULL) {
 610     throw OptionException(std::string("Mode pre-full for ") + option + " is not supported in this release.");
 611   }
 612 }
 613
 614 theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(
 615     std::string option, std::string optarg)
 616 {
 617   if(optarg ==  "none") {
 618     return theory::quantifiers::LITERAL_MATCH_NONE;
 619   } else if(optarg ==  "use") {
 620     return theory::quantifiers::LITERAL_MATCH_USE;
 621   } else if(optarg ==  "agg-predicate") {
 622     return theory::quantifiers::LITERAL_MATCH_AGG_PREDICATE;
 623   } else if(optarg ==  "agg") {
 624     return theory::quantifiers::LITERAL_MATCH_AGG;
 625   } else if(optarg ==  "help") {
 626     puts(s_literalMatchHelp.c_str());
 627     exit(1);
 628   } else {
 629     throw OptionException(std::string("unknown option for --literal-matching: `") +
 630                           optarg + "'.  Try --literal-matching help.");
 631   }
 632 }
 633
 634 void OptionsHandler::checkLiteralMatchMode(
 635     std::string option, theory::quantifiers::LiteralMatchMode mode)
 636 {
 637 }
 638
 639 theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode(
 640     std::string option, std::string optarg)
 641 {
 642   if(optarg == "gen-ev") {
 643     return theory::quantifiers::MBQI_GEN_EVAL;
 644   } else if(optarg == "none") {
 645     return theory::quantifiers::MBQI_NONE;
 646   } else if(optarg == "default" || optarg ==  "fmc") {
 647     return theory::quantifiers::MBQI_FMC;
 648   } else if(optarg == "abs") {
 649     return theory::quantifiers::MBQI_ABS;
 650   } else if(optarg == "trust") {
 651     return theory::quantifiers::MBQI_TRUST;
 652   } else if(optarg == "help") {
 653     puts(s_mbqiModeHelp.c_str());
 654     exit(1);
 655   } else {
 656     throw OptionException(std::string("unknown option for --mbqi: `") +
 657                           optarg + "'.  Try --mbqi help.");
 658   }
 659 }
 660
 661 void OptionsHandler::checkMbqiMode(std::string option,
 662                                    theory::quantifiers::MbqiMode mode)
 663 {
 664 }
 665
 666 theory::quantifiers::QcfWhenMode OptionsHandler::stringToQcfWhenMode(
 667     std::string option, std::string optarg)
 668 {
 669   if(optarg ==  "default") {
 670     return theory::quantifiers::QCF_WHEN_MODE_DEFAULT;
 671   } else if(optarg ==  "last-call") {
 672     return theory::quantifiers::QCF_WHEN_MODE_LAST_CALL;
 673   } else if(optarg ==  "std") {
 674     return theory::quantifiers::QCF_WHEN_MODE_STD;
 675   } else if(optarg ==  "std-h") {
 676     return theory::quantifiers::QCF_WHEN_MODE_STD_H;
 677   } else if(optarg ==  "help") {
 678     puts(s_qcfWhenModeHelp.c_str());
 679     exit(1);
 680   } else {
 681     throw OptionException(std::string("unknown option for --quant-cf-when: `") +
 682                           optarg + "'.  Try --quant-cf-when help.");
 683   }
 684 }
 685
 686 theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option,
 687                                                              std::string optarg)
 688 {
 689   if(optarg ==  "conflict") {
 690     return theory::quantifiers::QCF_CONFLICT_ONLY;
 691   } else if(optarg ==  "default" || optarg == "prop-eq") {
 692     return theory::quantifiers::QCF_PROP_EQ;
 693   } else if(optarg ==  "help") {
 694     puts(s_qcfModeHelp.c_str());
 695     exit(1);
 696   } else {
 697     throw OptionException(std::string("unknown option for --quant-cf-mode: `") +
 698                           optarg + "'.  Try --quant-cf-mode help.");
 699   }
 700 }
 701
 702 theory::quantifiers::UserPatMode OptionsHandler::stringToUserPatMode(
 703     std::string option, std::string optarg)
 704 {
 705   if(optarg == "use") {
 706     return theory::quantifiers::USER_PAT_MODE_USE;
 707   } else if(optarg ==  "default" || optarg == "trust") {
 708     return theory::quantifiers::USER_PAT_MODE_TRUST;
 709   } else if(optarg == "resort") {
 710     return theory::quantifiers::USER_PAT_MODE_RESORT;
 711   } else if(optarg == "ignore") {
 712     return theory::quantifiers::USER_PAT_MODE_IGNORE;
 713   } else if(optarg == "interleave") {
 714     return theory::quantifiers::USER_PAT_MODE_INTERLEAVE;
 715   } else if(optarg ==  "help") {
 716     puts(s_userPatModeHelp.c_str());
 717     exit(1);
 718   } else {
 719     throw OptionException(std::string("unknown option for --user-pat: `") +
 720                           optarg + "'.  Try --user-pat help.");
 721   }
 722 }
 723
 724 theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(
 725     std::string option, std::string optarg)
 726 {
 727   if(optarg ==  "default" || optarg == "min") {
 728     return theory::quantifiers::TRIGGER_SEL_MIN;
 729   } else if(optarg == "max") {
 730     return theory::quantifiers::TRIGGER_SEL_MAX;
 731   } else if(optarg == "min-s-max") {
 732     return theory::quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX;
 733   } else if(optarg == "min-s-all") {
 734     return theory::quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL;
 735   } else if(optarg == "all") {
 736     return theory::quantifiers::TRIGGER_SEL_ALL;
 737   } else if(optarg ==  "help") {
 738     puts(s_triggerSelModeHelp.c_str());
 739     exit(1);
 740   } else {
 741     throw OptionException(std::string("unknown option for --trigger-sel: `") +
 742                           optarg + "'.  Try --trigger-sel help.");
 743   }
 744 }
 745
 746 theory::quantifiers::TriggerActiveSelMode
 747 OptionsHandler::stringToTriggerActiveSelMode(std::string option,
 748                                              std::string optarg)
 749 {
 750   if(optarg ==  "default" || optarg == "all") {
 751     return theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL;
 752   } else if(optarg == "min") {
 753     return theory::quantifiers::TRIGGER_ACTIVE_SEL_MIN;
 754   } else if(optarg == "max") {
 755     return theory::quantifiers::TRIGGER_ACTIVE_SEL_MAX;
 756   } else if(optarg ==  "help") {
 757     puts(s_triggerActiveSelModeHelp.c_str());
 758     exit(1);
 759   } else {
 760     throw OptionException(std::string("unknown option for --trigger-active-sel: `") +
 761                           optarg + "'.  Try --trigger-active-sel help.");
 762   }
 763 }
 764
 765 theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode(
 766     std::string option, std::string optarg)
 767 {
 768   if(optarg== "default" || optarg== "simple" ) {
 769     return theory::quantifiers::PRENEX_QUANT_SIMPLE;
 770   } else if(optarg == "none") {
 771     return theory::quantifiers::PRENEX_QUANT_NONE;
 772   } else if(optarg == "dnorm") {
 773     return theory::quantifiers::PRENEX_QUANT_DISJ_NORMAL;
 774   } else if(optarg == "norm") {
 775     return theory::quantifiers::PRENEX_QUANT_NORMAL;
 776   } else if(optarg ==  "help") {
 777     puts(s_prenexQuantModeHelp.c_str());
 778     exit(1);
 779   } else {
 780     throw OptionException(std::string("unknown option for --prenex-quant: `") +
 781                           optarg + "'.  Try --prenex-quant help.");
 782   }
 783 }
 784
 785 theory::SygusFairMode OptionsHandler::stringToSygusFairMode(std::string option,
 786                                                             std::string optarg)
 787 {
 788   if(optarg == "direct") {
 789     return theory::SYGUS_FAIR_DIRECT;
 790   } else if(optarg == "default" || optarg == "dt-size") {
 791     return theory::SYGUS_FAIR_DT_SIZE;
 792   } else if(optarg == "dt-height-bound" ){
 793     return theory::SYGUS_FAIR_DT_HEIGHT_PRED;
 794   } else if(optarg == "dt-size-bound" ){
 795     return theory::SYGUS_FAIR_DT_SIZE_PRED;
 796   } else if(optarg == "none") {
 797     return theory::SYGUS_FAIR_NONE;
 798   } else if(optarg ==  "help") {
 799     puts(s_cegqiFairModeHelp.c_str());
 800     exit(1);
 801   } else {
 802     throw OptionException(std::string("unknown option for --cegqi-fair: `") +
 803                           optarg + "'.  Try --cegqi-fair help.");
 804   }
 805 }
 806
 807 theory::quantifiers::TermDbMode OptionsHandler::stringToTermDbMode(
 808     std::string option, std::string optarg)
 809 {
 810   if(optarg == "all" ) {
 811     return theory::quantifiers::TERM_DB_ALL;
 812   } else if(optarg == "relevant") {
 813     return theory::quantifiers::TERM_DB_RELEVANT;
 814   } else if(optarg ==  "help") {
 815     puts(s_termDbModeHelp.c_str());
 816     exit(1);
 817   } else {
 818     throw OptionException(std::string("unknown option for --term-db-mode: `") +
 819                           optarg + "'.  Try --term-db-mode help.");
 820   }
 821 }
 822
 823 theory::quantifiers::IteLiftQuantMode OptionsHandler::stringToIteLiftQuantMode(
 824     std::string option, std::string optarg)
 825 {
 826   if(optarg == "all" ) {
 827     return theory::quantifiers::ITE_LIFT_QUANT_MODE_ALL;
 828   } else if(optarg == "simple") {
 829     return theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE;
 830   } else if(optarg == "none") {
 831     return theory::quantifiers::ITE_LIFT_QUANT_MODE_NONE;
 832   } else if(optarg ==  "help") {
 833     puts(s_iteLiftQuantHelp.c_str());
 834     exit(1);
 835   } else {
 836     throw OptionException(std::string("unknown option for --ite-lift-quant: `") +
 837                           optarg + "'.  Try --ite-lift-quant help.");
 838   }
 839 }
 840
 841 theory::quantifiers::CbqiBvIneqMode OptionsHandler::stringToCbqiBvIneqMode(
 842     std::string option, std::string optarg)
 843 {
 844   if (optarg == "eq-slack")
 845   {
 846     return theory::quantifiers::CBQI_BV_INEQ_EQ_SLACK;
 847   }
 848   else if (optarg == "eq-boundary")
 849   {
 850     return theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY;
 851   }
 852   else if (optarg == "keep")
 853   {
 854     return theory::quantifiers::CBQI_BV_INEQ_KEEP;
 855   }
 856   else if (optarg == "help")
 857   {
 858     puts(s_cbqiBvIneqModeHelp.c_str());
 859     exit(1);
 860   }
 861   else
 862   {
 863     throw OptionException(std::string("unknown option for --cbqi-bv-ineq: `")
 864                           + optarg
 865                           + "'.  Try --cbqi-bv-ineq help.");
 866   }
 867 }
 868
 869 theory::quantifiers::CegqiSingleInvMode
 870 OptionsHandler::stringToCegqiSingleInvMode(std::string option,
 871                                            std::string optarg)
 872 {
 873   if(optarg == "none" ) {
 874     return theory::quantifiers::CEGQI_SI_MODE_NONE;
 875   } else if(optarg == "use" || optarg == "default") {
 876     return theory::quantifiers::CEGQI_SI_MODE_USE;
 877   } else if(optarg == "all") {
 878     return theory::quantifiers::CEGQI_SI_MODE_ALL;
 879   } else if(optarg ==  "help") {
 880     puts(s_cegqiSingleInvHelp.c_str());
 881     exit(1);
 882   } else {
 883     throw OptionException(std::string("unknown option for --cegqi-si: `") +
 884                           optarg + "'.  Try --cegqi-si help.");
 885   }
 886 }
 887
 888 theory::quantifiers::CegqiSingleInvRconsMode
 889 OptionsHandler::stringToCegqiSingleInvRconsMode(std::string option,
 890                                                 std::string optarg)
 891 {
 892   if (optarg == "none")
 893   {
 894     return theory::quantifiers::CEGQI_SI_RCONS_MODE_NONE;
 895   }
 896   else if (optarg == "try")
 897   {
 898     return theory::quantifiers::CEGQI_SI_RCONS_MODE_TRY;
 899   }
 900   else if (optarg == "all")
 901   {
 902     return theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL;
 903   }
 904   else if (optarg == "all-limit")
 905   {
 906     return theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL_LIMIT;
 907   }
 908   else if (optarg == "help")
 909   {
 910     puts(s_cegqiSingleInvRconsHelp.c_str());
 911     exit(1);
 912   }
 913   else
 914   {
 915     throw OptionException(std::string("unknown option for --cegqi-si-rcons: `")
 916                           + optarg + "'.  Try --cegqi-si-rcons help.");
 917   }
 918 }
 919
 920 theory::quantifiers::CegisSampleMode OptionsHandler::stringToCegisSampleMode(
 921     std::string option, std::string optarg)
 922 {
 923   if (optarg == "none")
 924   {
 925     return theory::quantifiers::CEGIS_SAMPLE_NONE;
 926   }
 927   else if (optarg == "use")
 928   {
 929     return theory::quantifiers::CEGIS_SAMPLE_USE;
 930   }
 931   else if (optarg == "trust")
 932   {
 933     return theory::quantifiers::CEGIS_SAMPLE_TRUST;
 934   }
 935   else if (optarg == "help")
 936   {
 937     puts(s_cegisSampleHelp.c_str());
 938     exit(1);
 939   }
 940   else
 941   {
 942     throw OptionException(std::string("unknown option for --cegis-sample: `")
 943                           + optarg
 944                           + "'.  Try --cegis-sample help.");
 945   }
 946 }
 947
 948 theory::quantifiers::SygusInvTemplMode
 949 OptionsHandler::stringToSygusInvTemplMode(std::string option,
 950                                           std::string optarg)
 951 {
 952   if(optarg == "none" ) {
 953     return theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE;
 954   } else if(optarg == "pre") {
 955     return theory::quantifiers::SYGUS_INV_TEMPL_MODE_PRE;
 956   } else if(optarg == "post") {
 957     return theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST;
 958   } else if(optarg ==  "help") {
 959     puts(s_sygusInvTemplHelp.c_str());
 960     exit(1);
 961   } else {
 962     throw OptionException(std::string("unknown option for --sygus-inv-templ: `") +
 963                           optarg + "'.  Try --sygus-inv-templ help.");
 964   }
 965 }
 966
 967 theory::quantifiers::SygusActiveGenMode
 968 OptionsHandler::stringToSygusActiveGenMode(std::string option,
 969                                            std::string optarg)
 970 {
 971   if (optarg == "none")
 972   {
 973     return theory::quantifiers::SYGUS_ACTIVE_GEN_NONE;
 974   }
 975   else if (optarg == "basic")
 976   {
 977     return theory::quantifiers::SYGUS_ACTIVE_GEN_BASIC;
 978   }
 979   else if (optarg == "var-agnostic")
 980   {
 981     return theory::quantifiers::SYGUS_ACTIVE_GEN_VAR_AGNOSTIC;
 982   }
 983   else if (optarg == "help")
 984   {
 985     puts(s_sygusActiveGenHelp.c_str());
 986     exit(1);
 987   }
 988   else
 989   {
 990     throw OptionException(std::string("unknown option for --sygus-inv-templ: `")
 991                           + optarg + "'.  Try --sygus-inv-templ help.");
 992   }
 993 }
 994
 995 theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode(
 996     std::string option, std::string optarg)
 997 {
 998   if(optarg == "all" ) {
 999     return theory::quantifiers::MACROS_QUANT_MODE_ALL;
1000   } else if(optarg == "ground") {
1001     return theory::quantifiers::MACROS_QUANT_MODE_GROUND;
1002   } else if(optarg == "ground-uf") {
1003     return theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF;
1004   } else if(optarg ==  "help") {
1005     puts(s_macrosQuantHelp.c_str());
1006     exit(1);
1007   } else {
1008     throw OptionException(std::string("unknown option for --macros-quant-mode: `") +
1009                           optarg + "'.  Try --macros-quant-mode help.");
1010   }
1011 }
1012
1013 theory::quantifiers::QuantDSplitMode OptionsHandler::stringToQuantDSplitMode(
1014     std::string option, std::string optarg)
1015 {
1016   if(optarg == "none" ) {
1017     return theory::quantifiers::QUANT_DSPLIT_MODE_NONE;
1018   } else if(optarg == "default") {
1019     return theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT;
1020   } else if(optarg == "agg") {
1021     return theory::quantifiers::QUANT_DSPLIT_MODE_AGG;
1022   } else if(optarg ==  "help") {
1023     puts(s_quantDSplitHelp.c_str());
1024     exit(1);
1025   } else {
1026     throw OptionException(std::string("unknown option for --quant-dsplit-mode: `") +
1027                           optarg + "'.  Try --quant-dsplit-mode help.");
1028   }
1029 }
1030
1031 theory::quantifiers::QuantRepMode OptionsHandler::stringToQuantRepMode(
1032     std::string option, std::string optarg)
1033 {
1034   if(optarg == "none" ) {
1035     return theory::quantifiers::QUANT_REP_MODE_EE;
1036   } else if(optarg == "first" || optarg == "default") {
1037     return theory::quantifiers::QUANT_REP_MODE_FIRST;
1038   } else if(optarg == "depth") {
1039     return theory::quantifiers::QUANT_REP_MODE_DEPTH;
1040   } else if(optarg ==  "help") {
1041     puts(s_quantRepHelp.c_str());
1042     exit(1);
1043   } else {
1044     throw OptionException(std::string("unknown option for --quant-rep-mode: `") +
1045                           optarg + "'.  Try --quant-rep-mode help.");
1046   }
1047 }
1048
1049 // theory/bv/options_handlers.h
1050 void OptionsHandler::abcEnabledBuild(std::string option, bool value)
1051 {
1052 #ifndef CVC4_USE_ABC
1053   if(value) {
1054     std::stringstream ss;
1055     ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
1056     throw OptionException(ss.str());
1057   }
1058 #endif /* CVC4_USE_ABC */
1059 }
1060
1061 void OptionsHandler::abcEnabledBuild(std::string option, std::string value)
1062 {
1063 #ifndef CVC4_USE_ABC
1064   if(!value.empty()) {
1065     std::stringstream ss;
1066     ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
1067     throw OptionException(ss.str());
1068   }
1069 #endif /* CVC4_USE_ABC */
1070 }
1071
1072 void OptionsHandler::satSolverEnabledBuild(std::string option, bool value)
1073 {
1074 #if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL)
1075   if (value)
1076   {
1077     std::stringstream ss;
1078     ss << "option `" << option
1079        << "' requires a CVC4 to be built with CryptoMiniSat or CaDiCaL";
1080     throw OptionException(ss.str());
1081   }
1082 #endif
1083 }
1084
1085 void OptionsHandler::satSolverEnabledBuild(std::string option,
1086                                            std::string value)
1087 {
1088 #if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL)
1089   if (!value.empty())
1090   {
1091     std::stringstream ss;
1092     ss << "option `" << option
1093        << "' requires a CVC4 to be built with CryptoMiniSat or CaDiCaL";
1094     throw OptionException(ss.str());
1095   }
1096 #endif
1097 }
1098
1099 const std::string OptionsHandler::s_bvSatSolverHelp = "\
1100 Sat solvers currently supported by the --bv-sat-solver option:\n\
1101 \n\
1102 minisat (default)\n\
1103 \n\
1104 cadical\n\
1105 \n\
1106 cryptominisat\n\
1107 ";
1108
1109 theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option,
1110                                                             std::string optarg)
1111 {
1112   if(optarg == "minisat") {
1113     return theory::bv::SAT_SOLVER_MINISAT;
1114   } else if(optarg == "cryptominisat") {
1115     if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY &&
1116         options::bitblastMode.wasSetByUser()) {
1117       throwLazyBBUnsupported(theory::bv::SAT_SOLVER_CRYPTOMINISAT);
1118     }
1119     if (!options::bitvectorToBool.wasSetByUser()) {
1120       options::bitvectorToBool.set(true);
1121     }
1122     return theory::bv::SAT_SOLVER_CRYPTOMINISAT;
1123   }
1124   else if (optarg == "cadical")
1125   {
1126     if (options::incrementalSolving()
1127         && options::incrementalSolving.wasSetByUser())
1128     {
1129       throw OptionException(
1130           std::string("CaDiCaL does not support incremental mode. \n\
1131                          Try --bv-sat-solver=cryptominisat or "
1132                       "--bv-sat-solver=minisat"));
1133     }
1134
1135     if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY
1136         && options::bitblastMode.wasSetByUser())
1137     {
1138       throwLazyBBUnsupported(theory::bv::SAT_SOLVER_CADICAL);
1139     }
1140     if (!options::bitvectorToBool.wasSetByUser())
1141     {
1142       options::bitvectorToBool.set(true);
1143     }
1144     return theory::bv::SAT_SOLVER_CADICAL;
1145   } else if(optarg == "help") {
1146     puts(s_bvSatSolverHelp.c_str());
1147     exit(1);
1148   } else {
1149     throw OptionException(std::string("unknown option for --bv-sat-solver: `") +
1150                           optarg + "'.  Try --bv-sat-solver=help.");
1151   }
1152 }
1153
1154 const std::string OptionsHandler::s_bitblastingModeHelp = "\
1155 Bit-blasting modes currently supported by the --bitblast option:\n\
1156 \n\
1157 lazy (default)\n\
1158 + Separate boolean structure and term reasoning between the core\n\
1159   SAT solver and the bv SAT solver\n\
1160 \n\
1161 eager\n\
1162 + Bitblast eagerly to bv SAT solver\n\
1163 ";
1164
1165 theory::bv::BitblastMode OptionsHandler::stringToBitblastMode(
1166     std::string option, std::string optarg)
1167 {
1168   if(optarg == "lazy") {
1169     if (!options::bitvectorPropagate.wasSetByUser()) {
1170       options::bitvectorPropagate.set(true);
1171     }
1172     if (!options::bitvectorEqualitySolver.wasSetByUser()) {
1173       options::bitvectorEqualitySolver.set(true);
1174     }
1175     if (!options::bitvectorEqualitySlicer.wasSetByUser()) {
1176       if (options::incrementalSolving() ||
1177           options::produceModels()) {
1178         options::bitvectorEqualitySlicer.set(theory::bv::BITVECTOR_SLICER_OFF);
1179       } else {
1180         options::bitvectorEqualitySlicer.set(theory::bv::BITVECTOR_SLICER_AUTO);
1181       }
1182     }
1183
1184     if (!options::bitvectorInequalitySolver.wasSetByUser()) {
1185       options::bitvectorInequalitySolver.set(true);
1186     }
1187     if (!options::bitvectorAlgebraicSolver.wasSetByUser()) {
1188       options::bitvectorAlgebraicSolver.set(true);
1189     }
1190     if (options::bvSatSolver() != theory::bv::SAT_SOLVER_MINISAT)
1191     {
1192       throwLazyBBUnsupported(options::bvSatSolver());
1193     }
1194     return theory::bv::BITBLAST_MODE_LAZY;
1195   } else if(optarg == "eager") {
1196     if (!options::bitvectorToBool.wasSetByUser()) {
1197       options::bitvectorToBool.set(true);
1198     }
1199
1200     if (!options::bvAbstraction.wasSetByUser() &&
1201         !options::skolemizeArguments.wasSetByUser()) {
1202       options::bvAbstraction.set(true);
1203       options::skolemizeArguments.set(true);
1204     }
1205     return theory::bv::BITBLAST_MODE_EAGER;
1206   } else if(optarg == "help") {
1207     puts(s_bitblastingModeHelp.c_str());
1208     exit(1);
1209   } else {
1210     throw OptionException(std::string("unknown option for --bitblast: `") +
1211                           optarg + "'.  Try --bitblast=help.");
1212   }
1213 }
1214
1215 const std::string OptionsHandler::s_bvSlicerModeHelp = "\
1216 Bit-vector equality slicer modes supported by the --bv-eq-slicer option:\n\
1217 \n\
1218 auto (default)\n\
1219 + Turn slicer on if input has only equalities over core symbols\n\
1220 \n\
1221 on\n\
1222 + Turn slicer on\n\
1223 \n\
1224 off\n\
1225 + Turn slicer off\n\
1226 ";
1227
1228 theory::bv::BvSlicerMode OptionsHandler::stringToBvSlicerMode(
1229     std::string option, std::string optarg)
1230 {
1231   if(optarg == "auto") {
1232     return theory::bv::BITVECTOR_SLICER_AUTO;
1233   } else if(optarg == "on") {
1234     return theory::bv::BITVECTOR_SLICER_ON;
1235   } else if(optarg == "off") {
1236     return theory::bv::BITVECTOR_SLICER_OFF;
1237   } else if(optarg == "help") {
1238     puts(s_bvSlicerModeHelp.c_str());
1239     exit(1);
1240   } else {
1241     throw OptionException(std::string("unknown option for --bv-eq-slicer: `") +
1242                           optarg + "'.  Try --bv-eq-slicer=help.");
1243   }
1244 }
1245
1246 void OptionsHandler::setBitblastAig(std::string option, bool arg)
1247 {
1248   if(arg) {
1249     if(options::bitblastMode.wasSetByUser()) {
1250       if(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER) {
1251         throw OptionException("bitblast-aig must be used with eager bitblaster");
1252       }
1253     } else {
1254       theory::bv::BitblastMode mode = stringToBitblastMode("", "eager");
1255       options::bitblastMode.set(mode);
1256     }
1257     if(!options::bitvectorAigSimplifications.wasSetByUser()) {
1258       options::bitvectorAigSimplifications.set("balance;drw");
1259     }
1260   }
1261 }
1262
1263 // theory/uf/options_handlers.h
1264 const std::string OptionsHandler::s_ufssModeHelp = "\
1265 UF strong solver options currently supported by the --uf-ss option:\n\
1266 \n\
1267 full \n\
1268 + Default, use uf strong solver to find minimal models for uninterpreted sorts.\n\
1269 \n\
1270 no-minimal \n\
1271 + Use uf strong solver to shrink model sizes, but do no enforce minimality.\n\
1272 \n\
1273 none \n\
1274 + Do not use uf strong solver to shrink model sizes. \n\
1275 \n\
1276 ";
1277
1278 theory::uf::UfssMode OptionsHandler::stringToUfssMode(std::string option,
1279                                                       std::string optarg)
1280 {
1281   if(optarg ==  "default" || optarg == "full" ) {
1282     return theory::uf::UF_SS_FULL;
1283   } else if(optarg == "no-minimal") {
1284     return theory::uf::UF_SS_NO_MINIMAL;
1285   } else if(optarg == "none") {
1286     return theory::uf::UF_SS_NONE;
1287   } else if(optarg ==  "help") {
1288     puts(s_ufssModeHelp.c_str());
1289     exit(1);
1290   } else {
1291     throw OptionException(std::string("unknown option for --uf-ss: `") +
1292                           optarg + "'.  Try --uf-ss help.");
1293   }
1294 }
1295
1296
1297
1298 // theory/options_handlers.h
1299 const std::string OptionsHandler::s_theoryOfModeHelp = "\
1300 TheoryOf modes currently supported by the --theoryof-mode option:\n\
1301 \n\
1302 type (default) \n\
1303 + type variables, constants and equalities by type\n\
1304 \n\
1305 term \n\
1306 + type variables as uninterpreted, equalities by the parametric theory\n\
1307 ";
1308
1309 theory::TheoryOfMode OptionsHandler::stringToTheoryOfMode(std::string option, std::string optarg) {
1310   if(optarg == "type") {
1311     return theory::THEORY_OF_TYPE_BASED;
1312   } else if(optarg == "term") {
1313     return theory::THEORY_OF_TERM_BASED;
1314   } else if(optarg == "help") {
1315     puts(s_theoryOfModeHelp.c_str());
1316     exit(1);
1317   } else {
1318     throw OptionException(std::string("unknown option for --theoryof-mode: `") +
1319                           optarg + "'.  Try --theoryof-mode help.");
1320   }
1321 }
1322
1323 // theory/options_handlers.h
1324 std::string OptionsHandler::handleUseTheoryList(std::string option, std::string optarg) {
1325   std::string currentList = options::useTheoryList();
1326   if(currentList.empty()){
1327     return optarg;
1328   } else {
1329     return currentList +','+ optarg;
1330   }
1331 }
1332
1333 void OptionsHandler::notifyUseTheoryList(std::string option) {
1334   d_options->d_useTheoryListListeners.notify();
1335 }
1336
1337
1338
1339 // printer/options_handlers.h
1340 const std::string OptionsHandler::s_modelFormatHelp = "\
1341 Model format modes currently supported by the --model-format option:\n\
1342 \n\
1343 default \n\
1344 + Print model as expressions in the output language format.\n\
1345 \n\
1346 table\n\
1347 + Print functional expressions over finite domains in a table format.\n\
1348 ";
1349
1350 const std::string OptionsHandler::s_instFormatHelp = "\
1351 Inst format modes currently supported by the --model-format option:\n\
1352 \n\
1353 default \n\
1354 + Print instantiations as a list in the output language format.\n\
1355 \n\
1356 szs\n\
1357 + Print instantiations as SZS compliant proof.\n\
1358 ";
1359
1360 ModelFormatMode OptionsHandler::stringToModelFormatMode(std::string option,
1361                                                         std::string optarg)
1362 {
1363   if(optarg == "default") {
1364     return MODEL_FORMAT_MODE_DEFAULT;
1365   } else if(optarg == "table") {
1366     return MODEL_FORMAT_MODE_TABLE;
1367   } else if(optarg == "help") {
1368     puts(s_modelFormatHelp.c_str());
1369     exit(1);
1370   } else {
1371     throw OptionException(std::string("unknown option for --model-format: `") +
1372                           optarg + "'.  Try --model-format help.");
1373   }
1374 }
1375
1376 InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option,
1377                                                       std::string optarg)
1378 {
1379   if(optarg == "default") {
1380     return INST_FORMAT_MODE_DEFAULT;
1381   } else if(optarg == "szs") {
1382     return INST_FORMAT_MODE_SZS;
1383   } else if(optarg == "help") {
1384     puts(s_instFormatHelp.c_str());
1385     exit(1);
1386   } else {
1387     throw OptionException(std::string("unknown option for --inst-format: `") +
1388                           optarg + "'.  Try --inst-format help.");
1389   }
1390 }
1391
1392
1393 // decision/options_handlers.h
1394 const std::string OptionsHandler::s_decisionModeHelp = "\
1395 Decision modes currently supported by the --decision option:\n\
1396 \n\
1397 internal (default)\n\
1398 + Use the internal decision heuristics of the SAT solver\n\
1399 \n\
1400 justification\n\
1401 + An ATGP-inspired justification heuristic\n\
1402 \n\
1403 justification-stoponly\n\
1404 + Use the justification heuristic only to stop early, not for decisions\n\
1405 ";
1406
1407 decision::DecisionMode OptionsHandler::stringToDecisionMode(std::string option,
1408                                                             std::string optarg)
1409 {
1410   options::decisionStopOnly.set(false);
1411
1412   if(optarg == "internal") {
1413     return decision::DECISION_STRATEGY_INTERNAL;
1414   } else if(optarg == "justification") {
1415     return decision::DECISION_STRATEGY_JUSTIFICATION;
1416   } else if(optarg == "justification-stoponly") {
1417     options::decisionStopOnly.set(true);
1418     return decision::DECISION_STRATEGY_JUSTIFICATION;
1419   } else if(optarg == "help") {
1420     puts(s_decisionModeHelp.c_str());
1421     exit(1);
1422   } else {
1423     throw OptionException(std::string("unknown option for --decision: `") +
1424                           optarg + "'.  Try --decision help.");
1425   }
1426 }
1427
1428 decision::DecisionWeightInternal OptionsHandler::stringToDecisionWeightInternal(
1429     std::string option, std::string optarg)
1430 {
1431   if(optarg == "off")
1432     return decision::DECISION_WEIGHT_INTERNAL_OFF;
1433   else if(optarg == "max")
1434     return decision::DECISION_WEIGHT_INTERNAL_MAX;
1435   else if(optarg == "sum")
1436     return decision::DECISION_WEIGHT_INTERNAL_SUM;
1437   else if(optarg == "usr1")
1438     return decision::DECISION_WEIGHT_INTERNAL_USR1;
1439   else
1440     throw OptionException(std::string("--decision-weight-internal must be off, max or sum."));
1441 }
1442
1443
1444 // smt/options_handlers.h
1445 const std::string OptionsHandler::s_simplificationHelp = "\
1446 Simplification modes currently supported by the --simplification option:\n\
1447 \n\
1448 batch (default) \n\
1449 + save up all ASSERTions; run nonclausal simplification and clausal\n\
1450   (MiniSat) propagation for all of them only after reaching a querying command\n\
1451   (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\
1452 \n\
1453 none\n\
1454 + do not perform nonclausal simplification\n\
1455 ";
1456
1457 SimplificationMode OptionsHandler::stringToSimplificationMode(
1458     std::string option, std::string optarg)
1459 {
1460   if(optarg == "batch") {
1461     return SIMPLIFICATION_MODE_BATCH;
1462   } else if(optarg == "none") {
1463     return SIMPLIFICATION_MODE_NONE;
1464   } else if(optarg == "help") {
1465     puts(s_simplificationHelp.c_str());
1466     exit(1);
1467   } else {
1468     throw OptionException(std::string("unknown option for --simplification: `") +
1469                           optarg + "'.  Try --simplification help.");
1470   }
1471 }
1472
1473 const std::string OptionsHandler::s_modelCoresHelp =
1474     "\
1475 Model cores modes currently supported by the --simplification option:\n\
1476 \n\
1477 none (default) \n\
1478 + do not compute model cores\n\
1479 \n\
1480 simple\n\
1481 + only include a subset of variables whose values are sufficient to show the\n\
1482 input formula is satisfied by the given model\n\
1483 \n\
1484 non-implied\n\
1485 + only include a subset of variables whose values, in addition to the values\n\
1486 of variables whose values are implied, are sufficient to show the input\n\
1487 formula is satisfied by the given model\n\
1488 \n\
1489 ";
1490
1491 ModelCoresMode OptionsHandler::stringToModelCoresMode(std::string option,
1492                                                       std::string optarg)
1493 {
1494   if (optarg == "none")
1495   {
1496     return MODEL_CORES_NONE;
1497   }
1498   else if (optarg == "simple")
1499   {
1500     return MODEL_CORES_SIMPLE;
1501   }
1502   else if (optarg == "non-implied")
1503   {
1504     return MODEL_CORES_NON_IMPLIED;
1505   }
1506   else if (optarg == "help")
1507   {
1508     puts(s_modelCoresHelp.c_str());
1509     exit(1);
1510   }
1511   else
1512   {
1513     throw OptionException(std::string("unknown option for --model-cores: `")
1514                           + optarg + "'.  Try --model-cores help.");
1515   }
1516 }
1517
1518 const std::string OptionsHandler::s_sygusSolutionOutModeHelp =
1519     "\
1520 Modes for finite model finding bound minimization, supported by --sygus-out:\n\
1521 \n\
1522 status \n\
1523 + Print only status for check-synth calls.\n\
1524 \n\
1525 status-and-def (default) \n\
1526 + Print status followed by definition corresponding to solution.\n\
1527 \n\
1528 status-or-def \n\
1529 + Print status if infeasible, or definition corresponding to\n\
1530   solution if feasible.\n\
1531 \n\
1532 sygus-standard \n\
1533 + Print based on SyGuS standard.\n\
1534 \n\
1535 ";
1536
1537 SygusSolutionOutMode OptionsHandler::stringToSygusSolutionOutMode(
1538     std::string option, std::string optarg)
1539 {
1540   if (optarg == "status")
1541   {
1542     return SYGUS_SOL_OUT_STATUS;
1543   }
1544   else if (optarg == "status-and-def")
1545   {
1546     return SYGUS_SOL_OUT_STATUS_AND_DEF;
1547   }
1548   else if (optarg == "status-or-def")
1549   {
1550     return SYGUS_SOL_OUT_STATUS_OR_DEF;
1551   }
1552   else if (optarg == "sygus-standard")
1553   {
1554     return SYGUS_SOL_OUT_STANDARD;
1555   }
1556   else if (optarg == "help")
1557   {
1558     puts(s_sygusSolutionOutModeHelp.c_str());
1559     exit(1);
1560   }
1561   else
1562   {
1563     throw OptionException(std::string("unknown option for --sygus-out: `")
1564                           + optarg
1565                           + "'.  Try --sygus-out help.");
1566   }
1567 }
1568
1569 void OptionsHandler::setProduceAssertions(std::string option, bool value)
1570 {
1571   options::produceAssertions.set(value);
1572   options::interactiveMode.set(value);
1573 }
1574
1575 void OptionsHandler::proofEnabledBuild(std::string option, bool value)
1576 {
1577 #ifndef CVC4_PROOF
1578   if(value) {
1579     std::stringstream ss;
1580     ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support";
1581     throw OptionException(ss.str());
1582   }
1583 #endif /* CVC4_PROOF */
1584 }
1585
1586 void OptionsHandler::LFSCEnabledBuild(std::string option, bool value) {
1587 #ifndef CVC4_USE_LFSC
1588   if (value) {
1589     std::stringstream ss;
1590     ss << "option `" << option << "' requires a build of CVC4 with integrated "
1591                                   "LFSC; this binary was not built with LFSC";
1592     throw OptionException(ss.str());
1593   }
1594 #endif /* CVC4_USE_LFSC */
1595 }
1596
1597 void OptionsHandler::notifyDumpToFile(std::string option) {
1598   d_options->d_dumpToFileListeners.notify();
1599 }
1600
1601
1602 void OptionsHandler::notifySetRegularOutputChannel(std::string option) {
1603   d_options->d_setRegularChannelListeners.notify();
1604 }
1605
1606 void OptionsHandler::notifySetDiagnosticOutputChannel(std::string option) {
1607   d_options->d_setDiagnosticChannelListeners.notify();
1608 }
1609
1610
1611 std::string OptionsHandler::checkReplayFilename(std::string option, std::string optarg) {
1612 #ifdef CVC4_REPLAY
1613   if(optarg == "") {
1614     throw OptionException (std::string("Bad file name for --replay"));
1615   } else {
1616     return optarg;
1617   }
1618 #else /* CVC4_REPLAY */
1619   throw OptionException("The replay feature was disabled in this build of CVC4.");
1620 #endif /* CVC4_REPLAY */
1621 }
1622
1623 void OptionsHandler::notifySetReplayLogFilename(std::string option) {
1624   d_options->d_setReplayFilenameListeners.notify();
1625 }
1626
1627 void OptionsHandler::statsEnabledBuild(std::string option, bool value)
1628 {
1629 #ifndef CVC4_STATISTICS_ON
1630   if(value) {
1631     std::stringstream ss;
1632     ss << "option `" << option << "' requires a statistics-enabled build of CVC4; this binary was not built with statistics support";
1633     throw OptionException(ss.str());
1634   }
1635 #endif /* CVC4_STATISTICS_ON */
1636 }
1637
1638 void OptionsHandler::threadN(std::string option) {
1639   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\"");
1640 }
1641
1642 void OptionsHandler::notifyDumpMode(std::string option)
1643 {
1644   d_options->d_setDumpModeListeners.notify();
1645 }
1646
1647
1648 // expr/options_handlers.h
1649 void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) {
1650   if(depth < -1) {
1651     throw OptionException("--default-expr-depth requires a positive argument, or -1.");
1652   }
1653 }
1654
1655 void OptionsHandler::setDefaultDagThreshPredicate(std::string option, int dag) {
1656   if(dag < 0) {
1657     throw OptionException("--default-dag-thresh requires a nonnegative argument.");
1658   }
1659 }
1660
1661 void OptionsHandler::notifySetDefaultExprDepth(std::string option) {
1662   d_options->d_setDefaultExprDepthListeners.notify();
1663 }
1664
1665 void OptionsHandler::notifySetDefaultDagThresh(std::string option) {
1666   d_options->d_setDefaultDagThreshListeners.notify();
1667 }
1668
1669 void OptionsHandler::notifySetPrintExprTypes(std::string option) {
1670   d_options->d_setPrintExprTypesListeners.notify();
1671 }
1672
1673
1674 // main/options_handlers.h
1675
1676 static void print_config (const char * str, std::string config) {
1677   std::string s(str);
1678   unsigned sz = 14;
1679   if (s.size() < sz) s.resize(sz, ' ');
1680   std::cout << s << ": " << config << std::endl;
1681 }
1682
1683 static void print_config_cond (const char * str, bool cond = false) {
1684   print_config(str, cond ? "yes" : "no");
1685 }
1686
1687 void OptionsHandler::copyright(std::string option) {
1688   std::cout << Configuration::copyright() << std::endl;
1689   exit(0);
1690 }
1691
1692 void OptionsHandler::showConfiguration(std::string option) {
1693   std::cout << Configuration::about() << std::endl;
1694
1695   print_config ("version", Configuration::getVersionString());
1696
1697   if(Configuration::isGitBuild()) {
1698     const char* branchName = Configuration::getGitBranchName();
1699     if(*branchName == '\0')  { branchName = "-"; }
1700     std::stringstream ss;
1701     ss << "git ["
1702        << branchName << " "
1703        << std::string(Configuration::getGitCommit()).substr(0, 8)
1704        << (Configuration::hasGitModifications() ? " (with modifications)" : "")
1705        << "]";
1706     print_config("scm", ss.str());
1707   } else {
1708     print_config_cond("scm", false);
1709   }
1710
1711   std::cout << std::endl;
1712
1713   std::stringstream ss;
1714   ss << Configuration::getVersionMajor() << "."
1715      << Configuration::getVersionMinor() << "."
1716      << Configuration::getVersionRelease();
1717   print_config("library", ss.str());
1718
1719   std::cout << std::endl;
1720
1721   print_config_cond("debug code", Configuration::isDebugBuild());
1722   print_config_cond("statistics", Configuration::isStatisticsBuild());
1723   print_config_cond("replay", Configuration::isReplayBuild());
1724   print_config_cond("tracing", Configuration::isTracingBuild());
1725   print_config_cond("dumping", Configuration::isDumpingBuild());
1726   print_config_cond("muzzled", Configuration::isMuzzledBuild());
1727   print_config_cond("assertions", Configuration::isAssertionBuild());
1728   print_config_cond("proof", Configuration::isProofBuild());
1729   print_config_cond("coverage", Configuration::isCoverageBuild());
1730   print_config_cond("profiling", Configuration::isProfilingBuild());
1731   print_config_cond("asan", Configuration::isAsanBuild());
1732   print_config_cond("competition", Configuration::isCompetitionBuild());
1733
1734   std::cout << std::endl;
1735
1736   print_config_cond("abc", Configuration::isBuiltWithAbc());
1737   print_config_cond("cln", Configuration::isBuiltWithCln());
1738   print_config_cond("glpk", Configuration::isBuiltWithGlpk());
1739   print_config_cond("cadical", Configuration::isBuiltWithCadical());
1740   print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
1741   print_config_cond("gmp", Configuration::isBuiltWithGmp());
1742   print_config_cond("lfsc", Configuration::isBuiltWithLfsc());
1743   print_config_cond("readline", Configuration::isBuiltWithReadline());
1744   print_config_cond("symfpu", Configuration::isBuiltWithSymFPU());
1745
1746   exit(0);
1747 }
1748
1749 static void printTags(unsigned ntags, char const* const* tags)
1750 {
1751   std::cout << "available tags:";
1752   for (unsigned i = 0; i < ntags; ++ i)
1753   {
1754     std::cout << "  " << tags[i] << std::endl;
1755   }
1756   std::cout << std::endl;
1757 }
1758
1759 void OptionsHandler::showDebugTags(std::string option)
1760 {
1761   if (!Configuration::isDebugBuild())
1762   {
1763     throw OptionException("debug tags not available in non-debug builds");
1764   }
1765   else if (!Configuration::isTracingBuild())
1766   {
1767     throw OptionException("debug tags not available in non-tracing builds");
1768   }
1769   printTags(Configuration::getNumDebugTags(),Configuration::getDebugTags());
1770   exit(0);
1771 }
1772
1773 void OptionsHandler::showTraceTags(std::string option)
1774 {
1775   if (!Configuration::isTracingBuild())
1776   {
1777     throw OptionException("trace tags not available in non-tracing build");
1778   }
1779   printTags(Configuration::getNumTraceTags(), Configuration::getTraceTags());
1780   exit(0);
1781 }
1782
1783 static std::string suggestTags(char const* const* validTags,
1784                                std::string inputTag,
1785                                char const* const* additionalTags)
1786 {
1787   DidYouMean didYouMean;
1788
1789   const char* opt;
1790   for (size_t i = 0; (opt = validTags[i]) != nullptr; ++i)
1791   {
1792     didYouMean.addWord(validTags[i]);
1793   }
1794   if (additionalTags != nullptr)
1795   {
1796     for (size_t i = 0; (opt = additionalTags[i]) != nullptr; ++i)
1797     {
1798       didYouMean.addWord(additionalTags[i]);
1799     }
1800   }
1801
1802   return didYouMean.getMatchAsString(inputTag);
1803 }
1804
1805 void OptionsHandler::enableTraceTag(std::string option, std::string optarg)
1806 {
1807   if(!Configuration::isTracingBuild())
1808   {
1809     throw OptionException("trace tags not available in non-tracing builds");
1810   }
1811   else if(!Configuration::isTraceTag(optarg.c_str()))
1812   {
1813     if (optarg == "help")
1814     {
1815       printTags(
1816           Configuration::getNumTraceTags(), Configuration::getTraceTags());
1817       exit(0);
1818     }
1819
1820     throw OptionException(
1821         std::string("trace tag ") + optarg + std::string(" not available.")
1822         + suggestTags(Configuration::getTraceTags(), optarg, nullptr));
1823   }
1824   Trace.on(optarg);
1825 }
1826
1827 void OptionsHandler::enableDebugTag(std::string option, std::string optarg)
1828 {
1829   if (!Configuration::isDebugBuild())
1830   {
1831     throw OptionException("debug tags not available in non-debug builds");
1832   }
1833   else if (!Configuration::isTracingBuild())
1834   {
1835     throw OptionException("debug tags not available in non-tracing builds");
1836   }
1837
1838   if (!Configuration::isDebugTag(optarg.c_str())
1839       && !Configuration::isTraceTag(optarg.c_str()))
1840   {
1841     if (optarg == "help")
1842     {
1843       printTags(
1844           Configuration::getNumDebugTags(), Configuration::getDebugTags());
1845       exit(0);
1846     }
1847
1848     throw OptionException(std::string("debug tag ") + optarg
1849                           + std::string(" not available.")
1850                           + suggestTags(Configuration::getDebugTags(),
1851                                         optarg,
1852                                         Configuration::getTraceTags()));
1853   }
1854   Debug.on(optarg);
1855   Trace.on(optarg);
1856 }
1857
1858 OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option,
1859                                                       std::string optarg)
1860 {
1861   if(optarg == "help") {
1862     options::languageHelp.set(true);
1863     return language::output::LANG_AUTO;
1864   }
1865
1866   try {
1867     return language::toOutputLanguage(optarg);
1868   } catch(OptionException& oe) {
1869     throw OptionException("Error in " + option + ": " + oe.getMessage() +
1870                           "\nTry --output-language help");
1871   }
1872
1873   Unreachable();
1874 }
1875
1876 InputLanguage OptionsHandler::stringToInputLanguage(std::string option,
1877                                                     std::string optarg)
1878 {
1879   if(optarg == "help") {
1880     options::languageHelp.set(true);
1881     return language::input::LANG_AUTO;
1882   }
1883
1884   try {
1885     return language::toInputLanguage(optarg);
1886   } catch(OptionException& oe) {
1887     throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --language help");
1888   }
1889
1890   Unreachable();
1891 }
1892
1893 /* options/base_options_handlers.h */
1894 void OptionsHandler::setVerbosity(std::string option, int value)
1895 {
1896   if(Configuration::isMuzzledBuild()) {
1897     DebugChannel.setStream(&CVC4::null_os);
1898     TraceChannel.setStream(&CVC4::null_os);
1899     NoticeChannel.setStream(&CVC4::null_os);
1900     ChatChannel.setStream(&CVC4::null_os);
1901     MessageChannel.setStream(&CVC4::null_os);
1902     WarningChannel.setStream(&CVC4::null_os);
1903   } else {
1904     if(value < 2) {
1905       ChatChannel.setStream(&CVC4::null_os);
1906     } else {
1907       ChatChannel.setStream(&std::cout);
1908     }
1909     if(value < 1) {
1910       NoticeChannel.setStream(&CVC4::null_os);
1911     } else {
1912       NoticeChannel.setStream(&std::cout);
1913     }
1914     if(value < 0) {
1915       MessageChannel.setStream(&CVC4::null_os);
1916       WarningChannel.setStream(&CVC4::null_os);
1917     } else {
1918       MessageChannel.setStream(&std::cout);
1919       WarningChannel.setStream(&std::cerr);
1920     }
1921   }
1922 }
1923
1924 void OptionsHandler::increaseVerbosity(std::string option) {
1925   options::verbosity.set(options::verbosity() + 1);
1926   setVerbosity(option, options::verbosity());
1927 }
1928
1929 void OptionsHandler::decreaseVerbosity(std::string option) {
1930   options::verbosity.set(options::verbosity() - 1);
1931   setVerbosity(option, options::verbosity());
1932 }
1933
1934
1935 }/* CVC4::options namespace */
1936 }/* CVC4 namespace */