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