/*********************                                                        */
/*! \file options.cpp
 ** \verbatim
 ** Original author: mdeters
 ** Major contributors: cconway, taking
 ** Minor contributors (to current version): barrett, dejan
 ** This file is part of the CVC4 prototype.
 ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
 ** Courant Institute of Mathematical Sciences
 ** New York University
 ** See the file COPYING in the top-level source directory for licensing
 ** information.\endverbatim
 **
 ** \brief Contains code for handling command-line options.
 **
 ** Contains code for handling command-line options
 **/

#include <cstdio>
#include <cstdlib>
#include <new>
#include <unistd.h>
#include <string.h>
#include <stdint.h>
#include <time.h>
#include <sstream>

#include <getopt.h>

#include "expr/expr.h"
#include "expr/command.h"
#include "util/configuration.h"
#include "util/exception.h"
#include "util/language.h"
#include "util/options.h"
#include "util/output.h"
#include "util/dump.h"
#include "prop/sat_solver_factory.h"

#include "cvc4autoconfig.h"

using namespace std;
using namespace CVC4;

namespace CVC4 {

CVC4_THREADLOCAL(const Options*) Options::s_current = NULL;

#ifdef CVC4_DEBUG
#  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
#else /* CVC4_DEBUG */
#  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false
#endif /* CVC4_DEBUG */

#if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE)
#  define DO_SEMANTIC_CHECKS_BY_DEFAULT false
#else /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
#  define DO_SEMANTIC_CHECKS_BY_DEFAULT true
#endif /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */

/** default decision options */
const Options::DecisionOptions defaultDecOpt = {
  false,                        // relevancyLeaves
  1000,                         // maxRelTimeAsPermille
  true,                         // computeRelevancy
  false,                        // mustRelevancy
  false,                        // stopOnly
};

Options::Options() :
  binary_name(),
  statistics(false),
  in(&std::cin),
  out(&std::cout),
  err(&std::cerr),
  verbosity(0),
  inputLanguage(language::input::LANG_AUTO),
  outputLanguage(language::output::LANG_AUTO),
  help(false),
  version(false),
  languageHelp(false),
  parseOnly(false),
  preprocessOnly(false),
  semanticChecks(DO_SEMANTIC_CHECKS_BY_DEFAULT),
  theoryRegistration(true),
  memoryMap(false),
  strictParsing(false),
  lazyDefinitionExpansion(false),
  printWinner(false),
  defaultExprDepth(0),
  simplificationMode(SIMPLIFICATION_MODE_BATCH),
  simplificationModeSetByUser(false),
  decisionMode(DECISION_STRATEGY_INTERNAL),
  decisionModeSetByUser(false),
  decisionOptions(DecisionOptions(defaultDecOpt)),
  doStaticLearning(true),
  doITESimp(false),
  doITESimpSetByUser(false),
  unconstrainedSimp(false),
  unconstrainedSimpSetByUser(false),
  repeatSimp(false),
  repeatSimpSetByUser(false),
  interactive(false),
  interactiveSetByUser(false),
  perCallResourceLimit(0),
  cumulativeResourceLimit(0),
  perCallMillisecondLimit(0),
  cumulativeMillisecondLimit(0),
  segvNoSpin(false),
  produceModels(false),
  proof(false),
  produceAssignments(false),
  typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT),
  earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT),
  incrementalSolving(false),
  replayFilename(""),
  replayStream(NULL),
  replayLog(NULL),
  satRandomFreq(0.0),
  satRandomSeed(91648253),// Minisat's default value
  satVarDecay(0.95),
  satClauseDecay(0.999),
  satRestartFirst(25),
  satRestartInc(3.0),
  arithUnateLemmaMode(ALL_PRESOLVE_LEMMAS),
  arithPropagationMode(BOTH_PROP),
  arithHeuristicPivots(0),
  arithHeuristicPivotsSetByUser(false),
  arithStandardCheckVarOrderPivots(-1),
  arithStandardCheckVarOrderPivotsSetByUser(false),
  arithHeuristicPivotRule(MINIMUM),
  arithSimplexCheckPeriod(200),
  arithPivotThreshold(2),
  arithPivotThresholdSetByUser(false),
  arithPropagateMaxLength(16),
  arithDioSolver(true),
  arithRewriteEq(false),
  arithRewriteEqSetByUser(false),
  ufSymmetryBreaker(false),
  ufSymmetryBreakerSetByUser(false),
  miniscopeQuant(true),
  miniscopeQuantFreeVar(true),
  prenexQuant(true),
  varElimQuant(false),
  cnfQuant(false),
  preSkolemQuant(false),
  smartTriggers(true),
  registerQuantBodyTerms(false),
  instWhenMode(INST_WHEN_FULL_LAST_CALL),
  eagerInstQuant(false),
  finiteModelFind(false),
  ufssEagerSplits(false),
  ufssRegions(true),
  ufssColoringSat(false),
  fmfModelBasedInst(true),
  fmfInstGen(true),
  fmfOneInstPerRound(false),
  fmfInstEngine(false),
  fmfRelevantDomain(false),
  efficientEMatching(false),
  literalMatchMode(LITERAL_MATCH_NONE),
  cbqi(false),
  cbqiSetByUser(false),
  rewriteRulesAsAxioms(false),
  userPatternsQuant(true),
  flipDecision(false),
  printInstEngine(false),
  printModelEngine(false),
  lemmaOutputChannel(NULL),
  lemmaInputChannel(NULL),
  threads(2),// default should be 1 probably, but say 2 for now
  threadArgv(),
  thread_id(-1),
  separateOutput(false),
  sharingFilterByLength(-1),
  bitvectorEagerBitblast(false),
  bitvectorEagerFullcheck(false),
  bitvectorShareLemmas(false),
  sat_refine_conflicts(false),
  theoryOfModeSetByUser(false),
  theoryOfMode(theory::THEORY_OF_TYPE_BASED)
{
}


static const string mostCommonOptionsDescription = "\
Most commonly-used CVC4 options:\n\
   --version | -V         identify this CVC4 binary\n\
   --help | -h            full command line reference\n\
   --lang | -L            force input language\n\
                          (default is `auto'; see --lang help)\n\
   --output-lang          force output language\n\
                          (default is `auto'; see --lang help)\n\
   --verbose | -v         increase verbosity (may be repeated)\n\
   --quiet | -q           decrease verbosity (may be repeated)\n\
   --stats                give statistics on exit\n\
   --parse-only           exit after parsing input\n\
   --preprocess-only      exit after preproc (useful with --stats or --dump)\n\
   --dump=MODE            dump preprocessed assertions, etc., see --dump=help\n\
   --dump-to=FILE         all dumping goes to FILE (instead of stdout)\n\
   --show-config          show CVC4 static configuration\n\
   --strict-parsing       be less tolerant of non-conforming inputs\n\
   --interactive          force interactive mode\n\
   --no-interactive       force non-interactive mode\n\
   --produce-models | -m  support the get-value command\n\
   --produce-assignments  support the get-assignment command\n\
   --print-success        print the \"success\" output required of SMT-LIBv2\n\
   --smtlib2              SMT-LIBv2 conformance mode (implies other options)\n\
   --proof                turn on proof generation\n\
   --incremental | -i     enable incremental solving\n\
   --tlimit=MS            enable time limiting (give milliseconds)\n\
   --tlimit-per=MS        enable time limiting per query (give milliseconds)\n\
   --rlimit=N             enable resource limiting\n\
   --rlimit-per=N         enable resource limiting per query\n\
";

static const string optionsDescription = mostCommonOptionsDescription + "\
\n\
Additional CVC4 options:\n\
   --mmap                 memory map file input\n\
   --segv-nospin          don't spin on segfault waiting for gdb\n\
   --lazy-type-checking   type check expressions only when necessary (default)\n\
   --eager-type-checking  type check expressions immediately on creation\n\
                          (debug builds only)\n\
   --no-type-checking     never type check expressions\n\
   --no-checking          disable ALL semantic checks, including type checks\n\
   --no-theory-registration disable theory reg (not safe for some theories)\n\
   --print-winner         enable printing the winning thread (pcvc4 only)\n\
   --trace | -t           trace something (e.g. -t pushpop), can repeat\n\
   --debug | -d           debug something (e.g. -d arith), can repeat\n\
   --show-debug-tags      show all available tags for debugging\n\
   --show-trace-tags      show all available tags for tracing\n\
   --show-sat-solvers     show all available SAT solvers\n\
   --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\
   --default-dag-thresh=N dagify common subexprs appearing > N times\n\
                          (1 == default, 0 == don't dagify)\n\
   --print-expr-types     print types with variables when printing exprs\n\
   --lazy-definition-expansion expand define-funs/LAMBDAs lazily\n\
   --simplification=MODE  choose simplification mode, see --simplification=help\n\
   --decision=MODE        choose decision mode, see --decision=help\n\
   --decision-budget=N    impose a budget for relevancy heuristic which increases linearly with\n\
                          each decision. N between 0 and 1000. (default: 1000, no budget)\n\
   --no-static-learning   turn off static learning (e.g. diamond-breaking)\n\
   --ite-simp             turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\
   --no-ite-simp          turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\
   --unconstrained-simp   turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)\n\
   --no-unconstrained-simp turn off unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)\n\
   --repeat-simp          make multiple passes with nonclausal simplifier\n\
   --no-repeat-simp       do not make multiple passes with nonclausal simplifier\n\
   --replay=file          replay decisions from file\n\
   --replay-log=file      log decisions and propagations to file\n\
   --theoryof-mode=mode   mode for theoryof\n\
  SAT:\n\
   --random-freq=P        frequency of random decisions in the sat solver\n\
                          (P=0.0 by default)\n\
   --random-seed=S        sets the random seed for the sat solver\n\
   --restart-int-base=I   sets the base restart interval for the sat solver\n\
                          (I=25 by default)\n\
   --restart-int-inc=F    restart interval increase factor for the sat solver\n\
                          (F=3.0 by default)\n\
  ARITHMETIC:\n\
   --unate-lemmas=MODE   determines which lemmas to add before solving\n\
                          (default is 'all', see --unate-lemmas=help)\n\
   --arith-prop=MODE      turns on arithmetic propagation\n\
                          (default is 'old', see --arith-prop=help)\n\
   --heuristic-pivot-rule=RULE change the pivot rule for the basic variable\n\
                          (default is 'min', see --heuristic-pivot-rule help)\n\
   --heuristic-pivots=N   the number of times to apply the heuristic pivot rule.\n\
                          If N < 0, this defaults to the number of variables\n\
                          If this is unset, this is tuned by the logic selection.\n\
   --simplex-check-period=N The number of pivots to do in simplex before rechecking for\n\
                          a conflict on all variables.\n\
   --pivot-threshold=N    sets the number of pivots using --pivot-rule\n\
                          per basic variable per simplex instance before\n\
                          using variable order\n\
   --prop-row-length=N    sets the maximum row length to be used in propagation\n\
   --disable-dio-solver   turns off Linear Diophantine Equation solver \n\
                          (Griggio, JSAT 2012)\n\
   --enable-arith-rewrite-equalities   turns on the preprocessing rewrite\n\
                          turning equalities into a conjunction of inequalities.\n \
   --disable-arith-rewrite-equalities   turns off the preprocessing rewrite\n\
                          turning equalities into a conjunction of inequalities.\n \
 UF:\n\
   --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al.,\n\
                          CADE 2011) [on by default only for QF_UF]\n\
   --disable-symmetry-breaker turns off UF symmetry breaker\n\
 QUANTIFIERS:\n\
   --disable-miniscope-quant     disable miniscope quantifiers\n\
   --disable-miniscope-quant-fv  disable miniscope quantifiers for ground subformulas\n\
   --disable-prenex-quant disable prenexing of quantified formulas\n\
   --var-elim-quant       enable variable elimination of quantified formulas\n\
   --cnf-quant            apply CNF conversion to quantified formulas\n\
   --pre-skolem-quant     apply skolemization eagerly to bodies of quantified formulas\n\
   --disable-smart-triggers   disable smart triggers\n\
   --register-quant-body-terms  consider ground terms within bodies of quantified formulas for matching\n\
   --inst-when=MODE       when to apply instantiation\n\
   --eager-inst-quant     apply quantifier instantiation eagerly\n\
   --literal-matching=MODE  choose literal matching mode\n\
   --enable-cbqi          turns on counterexample-based quantifier instantiation [off by default]\n\
   --disable-cbqi         turns off counterexample-based quantifier instantiation\n\
   --ignore-user-patterns ignore user-provided patterns for quantifier instantiation\n\
   --enable-flip-decision turns on flip decision heuristic\n\
 REWRITERULES:\n\
   --efficient-e-matching use efficient E-matching (only for rewrite rules)\n\
   --rewrite-rules-as-axioms convert rewrite rules into usual axioms (for debugging only)\n\
 FINITE_MODEL_FINDING:\n\
   --finite-model-find      use finite model finding heuristic for quantifier instantiation\n\
   --disable-uf-ss-regions  disable region-based method for discovering cliques and splits in uf strong solver\n\
   --uf-ss-eager-split      add splits eagerly for uf strong solver\n\
   --uf-ss-coloring-sat     use coloring-based SAT heuristic for uf strong solver\n\
   --disable-fmf-mbqi       disable model-based quantifier instantiation for finite model finding\n\
   --disable-fmf-inst-gen   disable Inst-Gen instantiation techniques for finite model finding\n\
   --fmf-one-inst-per-round  only add one instantiation per quantifier per round for fmf\n\
   --fmf-inst-engine        use instantiation engine in conjunction with finite model finding\n\
   --fmf-relevant-domain    use relevant domain computation, similar to complete instantiation (Ge, deMoura 09)\n\
 OTHER:\n\
   --disable-dio-solver   turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\
   --disable-arith-rewrite-equalities   turns off the preprocessing rewrite turning equalities into a conjunction of inequalities.\n\
   --threads=N            sets the number of solver threads\n\
   --threadN=string       configures thread N (0..#threads-1)\n\
   --filter-lemma-length=N don't share lemmas strictly longer than N\n\
   --bitblast-eager       eagerly bitblast the bitvectors to the main SAT solver\n\
   --bitblast-share-lemmas share lemmas from the bitblasting solver with the main solver\n\
   --bitblast-eager-fullcheck check the bitblasting eagerly\n\
   --refine-conflicts     refine theory conflict clauses\n\
";



static const string languageDescription = "\
Languages currently supported as arguments to the -L / --lang option:\n\
  auto           attempt to automatically determine the input language\n\
  pl | cvc4      CVC4 presentation language\n\
  smt | smtlib   SMT-LIB format 1.2\n\
  smt2 | smtlib2 SMT-LIB format 2.0\n\
  tptp           TPTP format (cnf and fof)\n\
\n\
Languages currently supported as arguments to the --output-lang option:\n\
  auto           match the output language to the input language\n\
  pl | cvc4      CVC4 presentation language\n\
  smt | smtlib   SMT-LIB format 1.2\n\
  smt2 | smtlib2 SMT-LIB format 2.0\n\
  tptp           TPTP format\n\
  ast            internal format (simple syntax-tree language)\n\
";

static const string simplificationHelp = "\
Simplification modes currently supported by the --simplification option:\n\
\n\
batch (default) \n\
+ save up all ASSERTions; run nonclausal simplification and clausal\n\
  (MiniSat) propagation for all of them only after reaching a querying command\n\
  (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\
\n\
incremental\n\
+ run nonclausal simplification and clausal propagation at each ASSERT\n\
  (and at CHECKSAT/QUERY/SUBTYPE)\n\
\n\
none\n\
+ do not perform nonclausal simplification\n\
";

static const string theoryofHelp = "\
TheoryOf modes currently supported by the --theoryof-mode option:\n\
\n\
type (default) \n\
+ type variables, constants and equalities by type\n\
\n\
term \n\
+ type variables as uninterpreted, equalities by the parametric theory\n\
";

static const string decisionHelp = "\
Decision modes currently supported by the --decision option:\n\
\n\
internal (default)\n\
+ Use the internal decision heuristics of the SAT solver\n\
\n\
justification\n\
+ An ATGP-inspired justification heuristic\n\
\n\
justification-stoponly\n\
+ Use the justification heuristic only to stop early, not for decisions\n\
\n\
relevancy\n\
+ Under development may-relevancy\n\
\n\
relevancy-leaves\n\
+ May-relevancy, but decide only on leaves\n\
\n\
Developer modes:\n\
\n\
justification-rel\n\
+ Use the relevancy code to do the justification stuff\n\
+ (This should do exact same thing as justification)\n\
\n\
justification-must\n\
+ Start deciding on literals close to root instead of those\n\
+ near leaves (don't expect it to work well) [Unimplemented]\n\
";

static const string instWhenHelp = "\
Modes currently supported by the --inst-when option:\n\
\n\
full\n\
+ Run instantiation round at full effort, before theory combination.\n\
\n\
full-last-call (default)\n\
+ Alternate running instantiation rounds at full effort and last\n\
  call.  In other words, interleave instantiation and theory combination.\n\
\n\
last-call\n\
+ Run instantiation at last call effort, after theory combination.\n\
\n\
";

static const string literalMatchHelp = "\
Literal match modes currently supported by the --literal-match option:\n\
\n\
none (default)\n\
+ Do not use literal matching.\n\
\n\
predicate\n\
+ Consider the phase requirements of predicate literals when applying heuristic\n\
  quantifier instantiation.  For example, the trigger P( x ) in the quantified \n\
  formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\
  terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\
  Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\
\n\
";

static const string dumpHelp = "\
Dump modes currently supported by the --dump option:\n\
\n\
benchmark\n\
+ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
  does not include any declarations or assertions.  Implied by all following\n\
  modes.\n\
\n\
declarations\n\
+ Dump declarations.  Implied by all following modes.\n\
\n\
assertions\n\
+ Output the assertions after non-clausal simplification and static\n\
  learning phases, but before presolve-time T-lemmas arrive.  If\n\
  non-clausal simplification and static learning are off\n\
  (--simplification=none --no-static-learning), the output\n\
  will closely resemble the input (with term-level ITEs removed).\n\
\n\
learned\n\
+ Output the assertions after non-clausal simplification, static\n\
  learning, and presolve-time T-lemmas.  This should include all eager\n\
  T-lemmas (in the form provided by the theory, which my or may not be\n\
  clausal).  Also includes level-0 BCP done by Minisat.\n\
\n\
clauses\n\
+ Do all the preprocessing outlined above, and dump the CNF-converted\n\
  output\n\
\n\
state\n\
+ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\
  Implied by all \"stateful\" modes below and conflicts with all\n\
  non-stateful modes below.\n\
\n\
t-conflicts [non-stateful]\n\
+ Output correctness queries for all theory conflicts\n\
\n\
missed-t-conflicts [stateful]\n\
+ Output completeness queries for theory conflicts\n\
\n\
t-propagations [stateful]\n\
+ Output correctness queries for all theory propagations\n\
\n\
missed-t-propagations [stateful]\n\
+ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\
\n\
t-lemmas [non-stateful]\n\
+ Output correctness queries for all theory lemmas\n\
\n\
t-explanations [non-stateful]\n\
+ Output correctness queries for all theory explanations\n\
\n\
Dump modes can be combined with multiple uses of --dump.  Generally you want\n\
one from the assertions category (either assertions, learned, or clauses), and\n\
perhaps one or more stateful or non-stateful modes for checking correctness\n\
and completeness of decision procedure implementations.  Stateful modes dump\n\
the contextual assertions made by the core solver (all decisions and\n\
propagations as assertions; that affects the validity of the resulting\n\
correctness and completeness queries, so of course stateful and non-stateful\n\
modes cannot be mixed in the same run.\n\
\n\
The --output-language option controls the language used for dumping, and\n\
this allows you to connect CVC4 to another solver implementation via a UNIX\n\
pipe to perform on-line checking.  The --dump-to option can be used to dump\n\
to a file.\n\
";

static const string arithUnateLemmasHelp = "\
Presolve lemmas are generated before SAT search begins using the relationship\n\
of constant terms and polynomials.\n\
Modes currently supported by the --unate-lemmas option:\n\
+ none \n\
+ ineqs \n\
  Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n\
+ eqs \n\
  Outputs lemmas of the general forms\n\
  (= p c) implies (<= p d) for c < d, or\n\
  (= p c) implies (not (= p d)) for c != d.\n\
+ all \n\
  A combination of inequalities and equalities.\n\
";

static const string propagationModeHelp = "\
This decides on kind of propagation arithmetic attempts to do during the search.\n\
+ none\n\
+ unate\n\
 use constraints to do unate propagation\n\
+ bi (Bounds Inference)\n\
  infers bounds on basic variables using the upper and lower bounds of the\n\
  non-basic variables in the tableau.\n\
+both\n\
";

static const string pivotRulesHelp = "\
This decides on the rule used by simplex during heuristic rounds\n\
for deciding the next basic variable to select.\n\
Pivot rules available:\n\
+min\n\
  The minimum abs() value of the variable's violation of its bound. (default)\n\
+min-break-ties\n\
  The minimum violation with ties broken by variable order (total)\n\
+max\n\
  The maximum violation the bound\n\
";

string Options::getDescription() const {
  return optionsDescription;
}

void Options::printUsage(const std::string msg, std::ostream& out) {
  out << msg << optionsDescription << endl << flush;
}

void Options::printShortUsage(const std::string msg, std::ostream& out) {
  out << msg << mostCommonOptionsDescription << endl
      << "For full usage, please use --help." << endl << flush;
}

void Options::printLanguageHelp(std::ostream& out) {
  out << languageDescription << flush;
}

/**
 * For the main getopt() routine, we need ways to switch on long
 * options without clashing with short option characters.  This is an
 * enum of those long options.  For long options (e.g. "--verbose")
 * with a short option equivalent ("-v"), we use the single-letter
 * short option; therefore, this enumeration starts at 256 to avoid
 * any collision.
 */
enum OptionValue {
  OPTION_VALUE_BEGIN = 256, /* avoid clashing with char options */
  SMTCOMP,
  STATS,
  SEGV_NOSPIN,
  OUTPUT_LANGUAGE,
  PARSE_ONLY,
  PREPROCESS_ONLY,
  DUMP,
  DUMP_TO,
  NO_CHECKING,
  NO_THEORY_REGISTRATION,
  USE_MMAP,
  SHOW_DEBUG_TAGS,
  SHOW_TRACE_TAGS,
  SHOW_SAT_SOLVERS,
  SHOW_CONFIG,
  STRICT_PARSING,
  DEFAULT_EXPR_DEPTH,
  DEFAULT_DAG_THRESH,
  PRINT_EXPR_TYPES,
  UF_THEORY,
  LAZY_DEFINITION_EXPANSION,
  SIMPLIFICATION_MODE,
  DECISION_MODE,
  DECISION_BUDGET,
  NO_STATIC_LEARNING,
  ITE_SIMP,
  NO_ITE_SIMP,
  UNCONSTRAINED_SIMP,
  NO_UNCONSTRAINED_SIMP,
  REPEAT_SIMP,
  NO_REPEAT_SIMP,
  INTERACTIVE,
  NO_INTERACTIVE,
  PRODUCE_ASSIGNMENTS,
  PRINT_SUCCESS,
  SMTLIB2,
  PROOF,
  NO_TYPE_CHECKING,
  LAZY_TYPE_CHECKING,
  EAGER_TYPE_CHECKING,
  REPLAY,
  REPLAY_LOG,
  PRINT_WINNER,
  RANDOM_FREQUENCY,
  RANDOM_SEED,
  SAT_RESTART_FIRST,
  SAT_RESTART_INC,
  ARITHMETIC_UNATE_LEMMA_MODE,
  ARITHMETIC_PROPAGATION_MODE,
  ARITHMETIC_HEURISTIC_PIVOTS,
  ARITHMETIC_VAR_ORDER_PIVOTS,
  ARITHMETIC_PIVOT_RULE,
  ARITHMETIC_CHECK_PERIOD,
  ARITHMETIC_PIVOT_THRESHOLD,
  ARITHMETIC_PROP_MAX_LENGTH,
  ARITHMETIC_DIO_SOLVER,
  ENABLE_ARITHMETIC_REWRITE_EQUALITIES,
  DISABLE_ARITHMETIC_REWRITE_EQUALITIES,
  ENABLE_SYMMETRY_BREAKER,
  DISABLE_SYMMETRY_BREAKER,
  DISABLE_MINISCOPE_QUANT,
  DISABLE_MINISCOPE_QUANT_FV,
  DISABLE_PRENEX_QUANT,
  VAR_ELIM_QUANT,
  CNF_QUANT,
  PRE_SKOLEM_QUANT,
  DISABLE_SMART_TRIGGERS,
  REGISTER_QUANT_BODY_TERMS,
  INST_WHEN,
  EAGER_INST_QUANT,
  FINITE_MODEL_FIND,
  DISABLE_UF_SS_REGIONS,
  UF_SS_EAGER_SPLIT,
  UF_SS_COLORING_SAT,
  DISABLE_FMF_MODEL_BASED_INST,
  DISABLE_FMF_INST_GEN,
  FMF_ONE_INST_PER_ROUND,
  FMF_INST_ENGINE,
  FMF_RELEVANT_DOMAIN,
  EFFICIENT_E_MATCHING,
  LITERAL_MATCHING,
  ENABLE_CBQI,
  DISABLE_CBQI,
  IGNORE_USER_PATTERNS,
  ENABLE_FLIP_DECISION,
  REWRITE_RULES_AS_AXIOMS,
  PRINT_MODEL_ENGINE,
  PRINT_INST_ENGINE,
  PARALLEL_THREADS,
  PARALLEL_SEPARATE_OUTPUT,
  PORTFOLIO_FILTER_LENGTH,
  TIME_LIMIT,
  TIME_LIMIT_PER,
  RESOURCE_LIMIT,
  RESOURCE_LIMIT_PER,
  BITVECTOR_EAGER_BITBLAST,
  BITVECTOR_SHARE_LEMMAS,
  BITVECTOR_EAGER_FULLCHECK,
  SAT_REFINE_CONFLICTS,
  THEORYOF_MODE,
  OPTION_VALUE_END
};/* enum OptionValue */

/**
 * This is a table of long options.  By policy, each short option
 * should have an equivalent long option (but the reverse isn't the
 * case), so this table should thus contain all command-line options.
 *
 * Each option in this array has four elements:
 *
 * 1. the long option string
 * 2. argument behavior for the option:
 *    no_argument - no argument permitted
 *    required_argument - an argument is expected
 *    optional_argument - an argument is permitted but not required
 * 3. this is a pointer to an int which is set to the 4th entry of the
 *    array if the option is present; or NULL, in which case
 *    getopt_long() returns the 4th entry
 * 4. the return value for getopt_long() when this long option (or the
 *    value to set the 3rd entry to; see #3)
 *
 * If you add something here, you should add it in src/main/usage.h
 * also, to document it.
 *
 * If you add something that has a short option equivalent, you should
 * add it to the getopt_long() call in parseOptions().
 */
static struct option cmdlineOptions[] = {
  // name, has_arg, *flag, val
  { "verbose"    , no_argument      , NULL, 'v'         },
  { "quiet"      , no_argument      , NULL, 'q'         },
  { "debug"      , required_argument, NULL, 'd'         },
  { "trace"      , required_argument, NULL, 't'         },
  { "stats"      , no_argument      , NULL, STATS       },
  { "no-checking", no_argument      , NULL, NO_CHECKING },
  { "no-theory-registration", no_argument, NULL, NO_THEORY_REGISTRATION },
  { "show-debug-tags", no_argument  , NULL, SHOW_DEBUG_TAGS },
  { "show-trace-tags", no_argument  , NULL, SHOW_TRACE_TAGS },
  { "show-sat-solvers", no_argument  , NULL, SHOW_SAT_SOLVERS },
  { "show-config", no_argument      , NULL, SHOW_CONFIG },
  { "segv-nospin", no_argument      , NULL, SEGV_NOSPIN },
  { "help"       , no_argument      , NULL, 'h'         },
  { "version"    , no_argument      , NULL, 'V'         },
  { "about"      , no_argument      , NULL, 'V'         },
  { "lang"       , required_argument, NULL, 'L'         },
  { "output-lang", required_argument, NULL, OUTPUT_LANGUAGE },
  { "parse-only" , no_argument      , NULL, PARSE_ONLY  },
  { "preprocess-only", no_argument      , NULL, PREPROCESS_ONLY },
  { "dump"       , required_argument, NULL, DUMP        },
  { "dump-to"    , required_argument, NULL, DUMP_TO     },
  { "mmap"       , no_argument      , NULL, USE_MMAP    },
  { "strict-parsing", no_argument   , NULL, STRICT_PARSING },
  { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
  { "default-dag-thresh", required_argument, NULL, DEFAULT_DAG_THRESH },
  { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES },
  { "uf"         , required_argument, NULL, UF_THEORY   },
  { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION },
  { "simplification", required_argument, NULL, SIMPLIFICATION_MODE },
  { "decision", required_argument, NULL, DECISION_MODE },
  { "decision-budget", required_argument, NULL, DECISION_BUDGET },
  { "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING },
  { "ite-simp", no_argument, NULL, ITE_SIMP },
  { "no-ite-simp", no_argument, NULL, NO_ITE_SIMP },
  { "unconstrained-simp", no_argument, NULL, UNCONSTRAINED_SIMP },
  { "no-unconstrained-simp", no_argument, NULL, NO_UNCONSTRAINED_SIMP },
  { "repeat-simp", no_argument, NULL, REPEAT_SIMP },
  { "no-repeat-simp", no_argument, NULL, NO_REPEAT_SIMP },
  { "interactive", no_argument      , NULL, INTERACTIVE },
  { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
  { "produce-models", no_argument   , NULL, 'm' },
  { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS },
  { "print-success", no_argument, NULL, PRINT_SUCCESS },
  { "smtlib2", no_argument, NULL, SMTLIB2 },
  { "proof", no_argument, NULL, PROOF },
  { "no-type-checking", no_argument , NULL, NO_TYPE_CHECKING },
  { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING },
  { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING },
  { "incremental", no_argument      , NULL, 'i' },
  { "replay"     , required_argument, NULL, REPLAY      },
  { "replay-log" , required_argument, NULL, REPLAY_LOG  },
  { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY  },
  { "random-seed" , required_argument, NULL, RANDOM_SEED  },
  { "restart-int-base", required_argument, NULL, SAT_RESTART_FIRST },
  { "restart-int-inc", required_argument, NULL, SAT_RESTART_INC },
  { "print-winner", no_argument     , NULL, PRINT_WINNER  },
  { "unate-lemmas", required_argument, NULL, ARITHMETIC_UNATE_LEMMA_MODE },
  { "arith-prop", required_argument, NULL, ARITHMETIC_PROPAGATION_MODE },
  { "heuristic-pivots", required_argument, NULL, ARITHMETIC_HEURISTIC_PIVOTS },
  { "heuristic-pivot-rule" , required_argument, NULL, ARITHMETIC_PIVOT_RULE  },
  { "standard-effort-variable-order-pivots", required_argument, NULL, ARITHMETIC_VAR_ORDER_PIVOTS },
  { "simplex-check-period" , required_argument, NULL, ARITHMETIC_CHECK_PERIOD  },
  { "pivot-threshold" , required_argument, NULL, ARITHMETIC_PIVOT_THRESHOLD  },
  { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH  },
  { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER },
  { "enable-arith-rewrite-equalities", no_argument, NULL, ENABLE_ARITHMETIC_REWRITE_EQUALITIES },
  { "disable-arith-rewrite-equalities", no_argument, NULL, DISABLE_ARITHMETIC_REWRITE_EQUALITIES },
  { "enable-symmetry-breaker", no_argument, NULL, ENABLE_SYMMETRY_BREAKER },
  { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER },
  { "disable-miniscope-quant", no_argument, NULL, DISABLE_MINISCOPE_QUANT },
  { "disable-miniscope-quant-fv", no_argument, NULL, DISABLE_MINISCOPE_QUANT_FV },
  { "disable-prenex-quant", no_argument, NULL, DISABLE_PRENEX_QUANT },
  { "var-elim-quant", no_argument, NULL, VAR_ELIM_QUANT },
  { "cnf-quant", no_argument, NULL, CNF_QUANT },
  { "pre-skolem-quant", no_argument, NULL, PRE_SKOLEM_QUANT },
  { "disable-smart-triggers", no_argument, NULL, DISABLE_SMART_TRIGGERS },
  { "register-quant-body-terms", no_argument, NULL, REGISTER_QUANT_BODY_TERMS },
  { "inst-when", required_argument, NULL, INST_WHEN },
  { "eager-inst-quant", no_argument, NULL, EAGER_INST_QUANT },
  { "finite-model-find", no_argument, NULL, FINITE_MODEL_FIND },
  { "disable-uf-ss-regions", no_argument, NULL, DISABLE_UF_SS_REGIONS },
  { "uf-ss-eager-split", no_argument, NULL, UF_SS_EAGER_SPLIT },
  { "uf-ss-coloring-sat", no_argument, NULL, UF_SS_COLORING_SAT },
  { "disable-fmf-mbqi", no_argument, NULL, DISABLE_FMF_MODEL_BASED_INST },
  { "disable-fmf-inst-gen", no_argument, NULL, DISABLE_FMF_INST_GEN },
  { "fmf-one-inst-per-round", no_argument, NULL, FMF_ONE_INST_PER_ROUND },
  { "fmf-inst-engine", no_argument, NULL, FMF_INST_ENGINE },
  { "fmf-relevant-domain", no_argument, NULL, FMF_RELEVANT_DOMAIN },
  { "efficient-e-matching", no_argument, NULL, EFFICIENT_E_MATCHING },
  { "literal-matching", required_argument, NULL, LITERAL_MATCHING },
  { "enable-cbqi", no_argument, NULL, ENABLE_CBQI },
  { "disable-cbqi", no_argument, NULL, DISABLE_CBQI },
  { "ignore-user-patterns", no_argument, NULL, IGNORE_USER_PATTERNS },
  { "enable-flip-decision", no_argument, NULL, ENABLE_FLIP_DECISION },
  { "rewrite-rules-as-axioms", no_argument, NULL, REWRITE_RULES_AS_AXIOMS },
  { "print-m-e", no_argument, NULL, PRINT_MODEL_ENGINE },
  { "print-i-e", no_argument, NULL, PRINT_INST_ENGINE },
  { "threads", required_argument, NULL, PARALLEL_THREADS },
  { "separate-output", no_argument, NULL, PARALLEL_SEPARATE_OUTPUT },
  { "filter-lemma-length", required_argument, NULL, PORTFOLIO_FILTER_LENGTH },
  { "tlimit"     , required_argument, NULL, TIME_LIMIT  },
  { "tlimit-per" , required_argument, NULL, TIME_LIMIT_PER },
  { "rlimit"     , required_argument, NULL, RESOURCE_LIMIT       },
  { "rlimit-per" , required_argument, NULL, RESOURCE_LIMIT_PER   },
  { "bitblast-eager", no_argument, NULL, BITVECTOR_EAGER_BITBLAST },
  { "bitblast-share-lemmas", no_argument, NULL, BITVECTOR_SHARE_LEMMAS },
  { "bitblast-eager-fullcheck", no_argument, NULL, BITVECTOR_EAGER_FULLCHECK },
  { "refine-conflicts", no_argument, NULL, SAT_REFINE_CONFLICTS },
  { "theoryof-mode", required_argument, NULL, THEORYOF_MODE },
  { NULL         , no_argument      , NULL, '\0'        }
};/* if you add things to the above, please remember to update usage.h! */


/** Parse argc/argv and put the result into a CVC4::Options struct. */
int Options::parseOptions(int argc, char* argv[])
throw(OptionException) {
  const char *progName = argv[0];
  int c;

  // Reset getopt(), in the case of multiple calls.
  // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
  optind = 0;
#if HAVE_DECL_OPTRESET
  optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this
#endif /* HAVE_DECL_OPTRESET */

  // find the base name of the program
  const char *x = strrchr(progName, '/');
  if(x != NULL) {
    progName = x + 1;
  }
  binary_name = string(progName);

  // The strange string in this call is the short option string.  An
  // initial '+' means that option processing stops as soon as a
  // non-option argument is encountered (it is not present, by design).
  // The initial ':' indicates that getopt_long() should return ':'
  // instead of '?' for a missing option argument.  Then, each letter
  // is a valid short option for getopt_long(), and if it's encountered,
  // getopt_long() returns that character.  A ':' after an option
  // character means an argument is required; two colons indicates an
  // argument is optional; no colons indicate an argument is not
  // permitted.  cmdlineOptions specifies all the long-options and the
  // return value for getopt_long() should they be encountered.
  while((c = getopt_long(argc, argv,
                         ":himVvqL:d:t:",
                         cmdlineOptions, NULL)) != -1) {
    switch(c) {

    case 'h':
      help = true;
      break;

    case 'V':
      version = true;
      break;

    case 'v':
      ++verbosity;
      break;

    case 'q':
      --verbosity;
      break;

    case 'L':
      setInputLanguage(optarg);
      break;

    case OUTPUT_LANGUAGE:
      setOutputLanguage(optarg);
      break;

    case 't':
      if(Configuration::isTracingBuild()) {
        if(!Configuration::isTraceTag(optarg))
          throw OptionException(string("trace tag ") + optarg +
                                string(" not available"));
      } else {
        throw OptionException("trace tags not available in non-tracing builds");
      }
      Trace.on(optarg);
      break;

    case 'd':
      if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
        if(!Configuration::isDebugTag(optarg) && !Configuration::isTraceTag(optarg)) {
          throw OptionException(string("debug tag ") + optarg +
                                string(" not available"));
        }
      } else if(! Configuration::isDebugBuild()) {
        throw OptionException("debug tags not available in non-debug builds");
      } else {
        throw OptionException("debug tags not available in non-tracing builds");
      }
      Debug.on(optarg);
      Trace.on(optarg);
      break;

    case STATS:
      statistics = true;
      break;

    case SEGV_NOSPIN:
      segvNoSpin = true;
      break;

    case PARSE_ONLY:
      parseOnly = true;
      break;

    case PREPROCESS_ONLY:
      preprocessOnly = true;
      break;

    case DUMP: {
#ifdef CVC4_DUMPING
      char* tokstr = optarg;
      char* toksave;
      while((optarg = strtok_r(tokstr, ",", &toksave)) != NULL) {
        tokstr = NULL;
        if(!strcmp(optarg, "benchmark")) {
        } else if(!strcmp(optarg, "declarations")) {
        } else if(!strcmp(optarg, "assertions")) {
        } else if(!strcmp(optarg, "learned")) {
        } else if(!strcmp(optarg, "clauses")) {
        } else if(!strcmp(optarg, "t-conflicts") ||
                  !strcmp(optarg, "t-lemmas") ||
                  !strcmp(optarg, "t-explanations") ||
                  !strcmp(optarg, "bv-rewrites") ||
                  !strcmp(optarg, "theory::fullcheck")) {
          // These are "non-state-dumping" modes.  If state (SAT decisions,
          // propagations, etc.) is dumped, it will interfere with the validity
          // of these generated queries.
          if(Dump.isOn("state")) {
            throw OptionException(string("dump option `") + optarg +
                                  "' conflicts with a previous, "
                                  "state-dumping dump option.  You cannot "
                                  "mix stateful and non-stateful dumping modes; "
                                  "see --dump help.");
          } else {
            Dump.on("no-permit-state");
          }
        } else if(!strcmp(optarg, "state") ||
                  !strcmp(optarg, "missed-t-conflicts") ||
                  !strcmp(optarg, "t-propagations") ||
                  !strcmp(optarg, "missed-t-propagations")) {
          // These are "state-dumping" modes.  If state (SAT decisions,
          // propagations, etc.) is not dumped, it will interfere with the
          // validity of these generated queries.
          if(Dump.isOn("no-permit-state")) {
            throw OptionException(string("dump option `") + optarg +
                                  "' conflicts with a previous, "
                                  "non-state-dumping dump option.  You cannot "
                                  "mix stateful and non-stateful dumping modes; "
                                  "see --dump help.");
          } else {
            Dump.on("state");
          }
        } else if(!strcmp(optarg, "help")) {
          puts(dumpHelp.c_str());
          exit(1);
        } else {
          throw OptionException(string("unknown option for --dump: `") +
                                optarg + "'.  Try --dump help.");
        }

        Dump.on(optarg);
        Dump.on("benchmark");
        if(strcmp(optarg, "benchmark")) {
          Dump.on("declarations");
        }
      }
#else /* CVC4_DUMPING */
      throw OptionException("The dumping feature was disabled in this build of CVC4.");
#endif /* CVC4_DUMPING */
      break;
    }

    case DUMP_TO: {
#ifdef CVC4_DUMPING
      size_t dagSetting = expr::ExprDag::getDag(Dump.getStream());
      if(optarg == NULL || *optarg == '\0') {
        throw OptionException(string("Bad file name for --dump-to"));
      } else if(!strcmp(optarg, "-")) {
        Dump.setStream(DumpOutC::dump_cout);
      } else {
        ostream* dumpTo = new ofstream(optarg, ofstream::out | ofstream::trunc);
        if(!*dumpTo) {
          throw OptionException(string("Cannot open dump-to file (maybe it exists): `") + optarg + "'");
        }
        Dump.setStream(*dumpTo);
      }
      expr::ExprDag::setDag(Dump.getStream(), dagSetting);
#else /* CVC4_DUMPING */
      throw OptionException("The dumping feature was disabled in this build of CVC4.");
#endif /* CVC4_DUMPING */
    }
      break;

    case NO_THEORY_REGISTRATION:
      theoryRegistration = false;
      break;

    case NO_CHECKING:
      semanticChecks = false;
      typeChecking = false;
      earlyTypeChecking = false;
      break;

    case USE_MMAP:
      memoryMap = true;
      break;

    case PRINT_WINNER:
      printWinner = true;
      break;

    case STRICT_PARSING:
      strictParsing = true;
      break;

    case DEFAULT_EXPR_DEPTH:
      {
        int depth = atoi(optarg);
        Debug.getStream() << Expr::setdepth(depth);
        Trace.getStream() << Expr::setdepth(depth);
        Notice.getStream() << Expr::setdepth(depth);
        Chat.getStream() << Expr::setdepth(depth);
        Message.getStream() << Expr::setdepth(depth);
        Warning.getStream() << Expr::setdepth(depth);
        defaultExprDepth = depth;
      }
      break;

    case DEFAULT_DAG_THRESH:
      {
        int dag = atoi(optarg);
        if(dag < 0) {
          throw OptionException("--default-dag-thresh requires a nonnegative argument.");
        }
        Debug.getStream() << Expr::dag(dag);
        Trace.getStream() << Expr::dag(dag);
        Notice.getStream() << Expr::dag(dag);
        Chat.getStream() << Expr::dag(dag);
        Message.getStream() << Expr::dag(dag);
        Warning.getStream() << Expr::dag(dag);
        Dump.getStream() << Expr::dag(dag);
      }
      break;

    case PRINT_EXPR_TYPES:
      Debug.getStream() << Expr::printtypes(true);
      Trace.getStream() << Expr::printtypes(true);
      Notice.getStream() << Expr::printtypes(true);
      Chat.getStream() << Expr::printtypes(true);
      Message.getStream() << Expr::printtypes(true);
      Warning.getStream() << Expr::printtypes(true);
      break;

    case LAZY_DEFINITION_EXPANSION:
      lazyDefinitionExpansion = true;
      break;

    case SIMPLIFICATION_MODE:
      if(!strcmp(optarg, "batch")) {
        simplificationMode = SIMPLIFICATION_MODE_BATCH;
        simplificationModeSetByUser = true;
      } else if(!strcmp(optarg, "incremental")) {
        simplificationMode = SIMPLIFICATION_MODE_INCREMENTAL;
        simplificationModeSetByUser = true;
      } else if(!strcmp(optarg, "none")) {
        simplificationMode = SIMPLIFICATION_MODE_NONE;
        simplificationModeSetByUser = true;
      } else if(!strcmp(optarg, "help")) {
        puts(simplificationHelp.c_str());
        exit(1);
      } else {
        throw OptionException(string("unknown option for --simplification: `") +
                              optarg + "'.  Try --simplification help.");
      }
      break;

    case THEORYOF_MODE:
      if (!strcmp(optarg, "type")) {
        theoryOfModeSetByUser = true;
        theoryOfMode = theory::THEORY_OF_TYPE_BASED;
      } else if (!strcmp(optarg, "term")) {
        theoryOfModeSetByUser = true;
        theoryOfMode = theory::THEORY_OF_TERM_BASED;
      } else if (!strcmp(optarg, "help")) {
        puts(theoryofHelp.c_str());
        exit(1);
      } else {
        throw OptionException(string("unknown option for --theoryof-mode: `") +
                              optarg + "'.  Try --theoryof-mode help.");
      }
      break;
    case DECISION_MODE:
      decisionOptions = defaultDecOpt;  // reset all options
      if(!strcmp(optarg, "internal")) {
        decisionMode = DECISION_STRATEGY_INTERNAL;
        decisionModeSetByUser = true;
      } else if(!strcmp(optarg, "justification")) {
        decisionMode = DECISION_STRATEGY_JUSTIFICATION;
        decisionModeSetByUser = true;
      } else if(!strcmp(optarg, "justification-stoponly")) {
        decisionMode = DECISION_STRATEGY_JUSTIFICATION;
        decisionModeSetByUser = true;
        decisionOptions.stopOnly = true;
      } else if(!strcmp(optarg, "relevancy")) {
        decisionMode = DECISION_STRATEGY_RELEVANCY;
        decisionModeSetByUser = true;
        decisionOptions.relevancyLeaves = false;
      } else if(!strcmp(optarg, "relevancy-leaves")) {
        decisionMode = DECISION_STRATEGY_RELEVANCY;
        decisionModeSetByUser = true;
        decisionOptions.relevancyLeaves = true;
      } else if(!strcmp(optarg, "justification-rel")) {
        decisionMode = DECISION_STRATEGY_RELEVANCY;
        decisionModeSetByUser = true;
        // relevancyLeaves : irrelevant
        // maxRelTimeAsPermille : irrelevant
        decisionOptions.computeRelevancy = false;
        decisionOptions.mustRelevancy = false;
      } else if(!strcmp(optarg, "justification-must")) {
        decisionMode = DECISION_STRATEGY_RELEVANCY;
        decisionModeSetByUser = true;
        // relevancyLeaves : irrelevant
        // maxRelTimeAsPermille : irrelevant
        decisionOptions.computeRelevancy = false;
        decisionOptions.mustRelevancy = true;
      } else if(!strcmp(optarg, "help")) {
        puts(decisionHelp.c_str());
        exit(1);
      } else {
        throw OptionException(string("unknown option for --decision: `") +
                              optarg + "'.  Try --decision help.");
      }
      break;

    case DECISION_BUDGET: {
      int i = atoi(optarg);
      if(i < 0 || i > 1000) {
        throw OptionException(string("invalid value for --decision-budget: `") +
                              optarg + "'. Must be between 0 and 1000.");
      }
      if(i == 0) {
        Warning() << "Decision budget is 0. Consider using internal decision heuristic and "
                  << std::endl << " removing this option." << std::endl;

      }
      decisionOptions.maxRelTimeAsPermille = (unsigned short)i;
    }
      break;

    case NO_STATIC_LEARNING:
      doStaticLearning = false;
      break;

    case ITE_SIMP:
      doITESimp = true;
      doITESimpSetByUser = true;
      break;

    case NO_ITE_SIMP:
      doITESimp = false;
      doITESimpSetByUser = true;
      break;

    case UNCONSTRAINED_SIMP:
      unconstrainedSimp = true;
      unconstrainedSimpSetByUser = true;
      break;

    case NO_UNCONSTRAINED_SIMP:
      unconstrainedSimp = false;
      unconstrainedSimpSetByUser = true;
      break;

    case REPEAT_SIMP:
      repeatSimp = true;
      repeatSimpSetByUser = true;
      break;

    case NO_REPEAT_SIMP:
      repeatSimp = false;
      repeatSimpSetByUser = true;
      break;

    case INTERACTIVE:
      interactive = true;
      interactiveSetByUser = true;
      break;

    case NO_INTERACTIVE:
      interactive = false;
      interactiveSetByUser = true;
      break;

    case 'm':
      produceModels = true;
      break;

    case PRODUCE_ASSIGNMENTS:
      produceAssignments = true;
      break;

    case SMTLIB2: // smtlib v2 compliance mode
      inputLanguage = language::input::LANG_SMTLIB_V2;
      outputLanguage = language::output::LANG_SMTLIB_V2;
      strictParsing = true;
      // make sure entire expressions are printed on all the non-debug, non-trace streams
      Notice.getStream() << Expr::setdepth(-1);
      Chat.getStream() << Expr::setdepth(-1);
      Message.getStream() << Expr::setdepth(-1);
      Warning.getStream() << Expr::setdepth(-1);
      /* intentionally fall through */

    case PRINT_SUCCESS:
      Debug.getStream() << Command::printsuccess(true);
      Trace.getStream() << Command::printsuccess(true);
      Notice.getStream() << Command::printsuccess(true);
      Chat.getStream() << Command::printsuccess(true);
      Message.getStream() << Command::printsuccess(true);
      Warning.getStream() << Command::printsuccess(true);
      break;

    case PROOF:
#ifdef CVC4_PROOF
      proof = true;
#else /* CVC4_PROOF */
      throw OptionException("This is not a proof-enabled build of CVC4; --proof cannot be used");
#endif /* CVC4_PROOF */
      break;

    case NO_TYPE_CHECKING:
      typeChecking = false;
      earlyTypeChecking = false;
      break;

    case LAZY_TYPE_CHECKING:
      typeChecking = true;
      earlyTypeChecking = false;
      break;

    case EAGER_TYPE_CHECKING:
      typeChecking = true;
      earlyTypeChecking = true;
      break;

    case 'i':
      incrementalSolving = true;
      break;

    case REPLAY:
#ifdef CVC4_REPLAY
      if(optarg == NULL || *optarg == '\0') {
        throw OptionException(string("Bad file name for --replay"));
      } else {
        replayFilename = optarg;
      }
#else /* CVC4_REPLAY */
      throw OptionException("The replay feature was disabled in this build of CVC4.");
#endif /* CVC4_REPLAY */
      break;

    case REPLAY_LOG:
#ifdef CVC4_REPLAY
      if(optarg == NULL || *optarg == '\0') {
        throw OptionException(string("Bad file name for --replay-log"));
      } else if(!strcmp(optarg, "-")) {
        replayLog = &cout;
      } else {
        replayLog = new ofstream(optarg, ofstream::out | ofstream::trunc);
        if(!*replayLog) {
          throw OptionException(string("Cannot open replay-log file: `") + optarg + "'");
        }
      }
#else /* CVC4_REPLAY */
      throw OptionException("The replay feature was disabled in this build of CVC4.");
#endif /* CVC4_REPLAY */
      break;

    case ENABLE_SYMMETRY_BREAKER:
      ufSymmetryBreaker = true;
      ufSymmetryBreakerSetByUser = true;
      break;
    case DISABLE_SYMMETRY_BREAKER:
      ufSymmetryBreaker = false;
      ufSymmetryBreakerSetByUser = true;
      break;
    case DISABLE_MINISCOPE_QUANT:
      miniscopeQuant = false;
      break;
    case DISABLE_MINISCOPE_QUANT_FV:
      miniscopeQuantFreeVar = false;
      break;
    case DISABLE_PRENEX_QUANT:
      prenexQuant = false;
      break;
    case VAR_ELIM_QUANT:
      varElimQuant = true;
      break;
    case CNF_QUANT:
      cnfQuant = true;
      break;
    case PRE_SKOLEM_QUANT:
      preSkolemQuant = true;
      break;
    case DISABLE_SMART_TRIGGERS:
      smartTriggers = false;
      break;
    case REGISTER_QUANT_BODY_TERMS:
      registerQuantBodyTerms = true;
      break;
    case INST_WHEN:
      if(!strcmp(optarg, "pre-full")) {
        instWhenMode = INST_WHEN_PRE_FULL;
      } else if(!strcmp(optarg, "full")) {
        instWhenMode = INST_WHEN_FULL;
      } else if(!strcmp(optarg, "full-last-call")) {
        instWhenMode = INST_WHEN_FULL_LAST_CALL;
      } else if(!strcmp(optarg, "last-call")) {
        instWhenMode = INST_WHEN_LAST_CALL;
      } else if(!strcmp(optarg, "help")) {
        puts(instWhenHelp.c_str());
        exit(1);
      } else {
        throw OptionException(string("unknown option for --inst-when: `") +
                              optarg + "'.  Try --inst-when help.");
      }
      break;
    case EAGER_INST_QUANT:
      eagerInstQuant = true;
      break;
    case FINITE_MODEL_FIND:
      finiteModelFind = true;
      break;
    case DISABLE_UF_SS_REGIONS:
      ufssRegions = false;
      break;
    case UF_SS_EAGER_SPLIT:
      ufssEagerSplits = true;
      break;
    case UF_SS_COLORING_SAT:
      ufssColoringSat = true;
      break;
    case DISABLE_FMF_MODEL_BASED_INST:
      fmfModelBasedInst = false;
      break;
    case DISABLE_FMF_INST_GEN:
      fmfInstGen = false;
      break;
    case FMF_ONE_INST_PER_ROUND:
      fmfOneInstPerRound = true;
      break;
    case FMF_INST_ENGINE:
      fmfInstEngine = true;
      break;
    case FMF_RELEVANT_DOMAIN:
      fmfRelevantDomain = true;
      break;
    case EFFICIENT_E_MATCHING:
      efficientEMatching = true;
      break;
    case LITERAL_MATCHING:
      if(!strcmp(optarg, "none")) {
        literalMatchMode = LITERAL_MATCH_NONE;
      } else if(!strcmp(optarg, "predicate")) {
        literalMatchMode = LITERAL_MATCH_PREDICATE;
      } else if(!strcmp(optarg, "equality")) {
        literalMatchMode = LITERAL_MATCH_EQUALITY;
      } else if(!strcmp(optarg, "help")) {
        puts(literalMatchHelp.c_str());
        exit(1);
      } else {
        throw OptionException(string("unknown option for --literal-matching: `") +
                              optarg + "'.  Try --literal-matching help.");
      }
      break;
    case ENABLE_CBQI:
      cbqi = true;
      cbqiSetByUser = true;
      break;
    case DISABLE_CBQI:
      cbqi = false;
      cbqiSetByUser = true;
      break;
    case IGNORE_USER_PATTERNS:
      userPatternsQuant = false;
      break;
    case ENABLE_FLIP_DECISION:
      flipDecision = true;
      break;
    case REWRITE_RULES_AS_AXIOMS:
      rewriteRulesAsAxioms = true;
      break;
    case PRINT_MODEL_ENGINE:
      printModelEngine = true;
      break;
    case PRINT_INST_ENGINE:
      printInstEngine = true;
      break;
    case TIME_LIMIT:
      {
        int i = atoi(optarg);
        if(i < 0) {
          throw OptionException("--time-limit requires a nonnegative argument.");
        }
        cumulativeMillisecondLimit = (unsigned long) i;
      }
      break;
    case TIME_LIMIT_PER:
      {
        int i = atoi(optarg);
        if(i < 0) {
          throw OptionException("--time-limit-per requires a nonnegative argument.");
        }
        perCallMillisecondLimit = (unsigned long) i;
      }
      break;
    case RESOURCE_LIMIT:
      {
        int i = atoi(optarg);
        if(i < 0) {
          throw OptionException("--limit requires a nonnegative argument.");
        }
        cumulativeResourceLimit = (unsigned long) i;
      }
      break;
    case RESOURCE_LIMIT_PER:
      {
        int i = atoi(optarg);
        if(i < 0) {
          throw OptionException("--limit-per requires a nonnegative argument.");
        }
        perCallResourceLimit = (unsigned long) i;
        break;
      }
    case BITVECTOR_EAGER_BITBLAST:
      {
        bitvectorEagerBitblast = true;
        break;
      }
    case BITVECTOR_EAGER_FULLCHECK:
      {
        bitvectorEagerFullcheck = true;
        break;
      }
    case BITVECTOR_SHARE_LEMMAS:
      {
        bitvectorShareLemmas = true;
        break;
      }
    case SAT_REFINE_CONFLICTS:
      {
        sat_refine_conflicts = true;
        break;
      }
    case RANDOM_SEED:
      satRandomSeed = atof(optarg);
      break;

    case RANDOM_FREQUENCY:
      satRandomFreq = atof(optarg);
      if(! (0.0 <= satRandomFreq && satRandomFreq <= 1.0)){
        throw OptionException(string("--random-freq: `") +
                              optarg + "' is not between 0.0 and 1.0.");
      }
      break;

    case SAT_RESTART_FIRST:
      {
        int i = atoi(optarg);
        if(i < 1) {
          throw OptionException("--restart-int-base requires a number bigger than 1");
        }
        satRestartFirst = i;
        break;
      }

    case SAT_RESTART_INC:
      {
        int i = atoi(optarg);
        if(i < 1) {
          throw OptionException("--restart-int-inc requires a number bigger than 1.0");
        }
        satRestartInc = i;
      }
      break;

    case ARITHMETIC_UNATE_LEMMA_MODE:
      if(!strcmp(optarg, "all")) {
        arithUnateLemmaMode = ALL_PRESOLVE_LEMMAS;
        break;
      } else if(!strcmp(optarg, "none")) {
        arithUnateLemmaMode = NO_PRESOLVE_LEMMAS;
        break;
      } else if(!strcmp(optarg, "ineqs")) {
        arithUnateLemmaMode = INEQUALITY_PRESOLVE_LEMMAS;
        break;
      } else if(!strcmp(optarg, "eqs")) {
        arithUnateLemmaMode = EQUALITY_PRESOLVE_LEMMAS;
        break;
      } else if(!strcmp(optarg, "help")) {
        puts(arithUnateLemmasHelp.c_str());
        exit(1);
      } else {
        throw OptionException(string("unknown option for --unate-lemmas: `") +
                              optarg + "'.  Try --unate-lemmas=help.");
      }
      break;

    case ARITHMETIC_PROPAGATION_MODE:
      if(!strcmp(optarg, "none")) {
        arithPropagationMode = NO_PROP;
        break;
      } else if(!strcmp(optarg, "unate")) {
        arithPropagationMode = UNATE_PROP;
        break;
      } else if(!strcmp(optarg, "bi")) {
        arithPropagationMode = BOUND_INFERENCE_PROP;
        break;
      } else if(!strcmp(optarg, "both")) {
        arithPropagationMode = BOTH_PROP;
        break;
      } else if(!strcmp(optarg, "help")) {
        puts(propagationModeHelp.c_str());
        exit(1);
      } else {
        throw OptionException(string("unknown option for --arith-prop: `") +
                              optarg + "'.  Try --arith-prop help.");
      }
      break;

    case ARITHMETIC_HEURISTIC_PIVOTS:
      arithHeuristicPivots = atoi(optarg);
      arithHeuristicPivotsSetByUser = true;
      break;

    case ARITHMETIC_VAR_ORDER_PIVOTS:
      arithStandardCheckVarOrderPivots = atoi(optarg);
      arithStandardCheckVarOrderPivotsSetByUser = true;
      break;

    case ARITHMETIC_PIVOT_RULE:
      if(!strcmp(optarg, "min")) {
        arithHeuristicPivotRule = MINIMUM;
        break;
      } else if(!strcmp(optarg, "min-break-ties")) {
        arithHeuristicPivotRule = BREAK_TIES;
        break;
      } else if(!strcmp(optarg, "max")) {
        arithHeuristicPivotRule = MAXIMUM;
        break;
      } else if(!strcmp(optarg, "help")) {
        puts(pivotRulesHelp.c_str());
        exit(1);
      } else {
        throw OptionException(string("unknown option for --heuristic-pivot-rule: `") +
                              optarg + "'.  Try --heuristic-pivot-rule help.");
      }
      break;

    case ARITHMETIC_CHECK_PERIOD:
      arithSimplexCheckPeriod = atoi(optarg);
      break;

    case ARITHMETIC_PIVOT_THRESHOLD:
      arithPivotThreshold = atoi(optarg);
      arithPivotThresholdSetByUser = true;
      break;

    case ARITHMETIC_PROP_MAX_LENGTH:
      arithPropagateMaxLength = atoi(optarg);
      break;

    case ARITHMETIC_DIO_SOLVER:
      arithDioSolver = false;
      break;

    case ENABLE_ARITHMETIC_REWRITE_EQUALITIES:
      arithRewriteEq = true;
      arithRewriteEqSetByUser = true;
      break;

    case DISABLE_ARITHMETIC_REWRITE_EQUALITIES:
      arithRewriteEq = false;
      arithRewriteEqSetByUser = true;
      break;

    case SHOW_DEBUG_TAGS:
      if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
        printf("available tags:");
        unsigned ntags = Configuration::getNumDebugTags();
        char const* const* tags = Configuration::getDebugTags();
        for(unsigned i = 0; i < ntags; ++ i) {
          printf(" %s", tags[i]);
        }
        printf("\n");
      } else if(! Configuration::isDebugBuild()) {
        throw OptionException("debug tags not available in non-debug builds");
      } else {
        throw OptionException("debug tags not available in non-tracing builds");
      }
      exit(0);
      break;

    case SHOW_TRACE_TAGS:
      if(Configuration::isTracingBuild()) {
        printf("available tags:");
        unsigned ntags = Configuration::getNumTraceTags();
        char const* const* tags = Configuration::getTraceTags();
        for (unsigned i = 0; i < ntags; ++ i) {
          printf(" %s", tags[i]);
        }
        printf("\n");
      } else {
        throw OptionException("trace tags not available in non-tracing builds");
      }
      exit(0);
      break;

    case SHOW_SAT_SOLVERS:
    {
      vector<string> solvers;
      prop::SatSolverFactory::getSolverIds(solvers);
      printf("Available SAT solvers: ");
      for (unsigned i = 0; i < solvers.size(); ++ i) {
        if (i > 0) {
          printf(", ");
        }
        printf("%s", solvers[i].c_str());
      }
      printf("\n");
      exit(0);
      break;
    }
    case SHOW_CONFIG:
      fputs(Configuration::about().c_str(), stdout);
      printf("\n");
      printf("version    : %s\n", Configuration::getVersionString().c_str());
      if(Configuration::isSubversionBuild()) {
        printf("subversion : yes [%s r%u%s]\n",
               Configuration::getSubversionBranchName(),
               Configuration::getSubversionRevision(),
               Configuration::hasSubversionModifications() ?
                 " (with modifications)" : "");
      } else {
        printf("subversion : %s\n", Configuration::isSubversionBuild() ? "yes" : "no");
      }
      printf("\n");
      printf("library    : %u.%u.%u\n",
             Configuration::getVersionMajor(),
             Configuration::getVersionMinor(),
             Configuration::getVersionRelease());
      printf("\n");
      printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no");
      printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no");
      printf("replay     : %s\n", Configuration::isReplayBuild() ? "yes" : "no");
      printf("tracing    : %s\n", Configuration::isTracingBuild() ? "yes" : "no");
      printf("dumping    : %s\n", Configuration::isDumpingBuild() ? "yes" : "no");
      printf("muzzled    : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no");
      printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no");
      printf("proof      : %s\n", Configuration::isProofBuild() ? "yes" : "no");
      printf("coverage   : %s\n", Configuration::isCoverageBuild() ? "yes" : "no");
      printf("profiling  : %s\n", Configuration::isProfilingBuild() ? "yes" : "no");
      printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no");
      printf("\n");
      printf("cudd       : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no");
      printf("cln        : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no");
      printf("gmp        : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no");
      printf("tls        : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no");
      exit(0);

    case PARALLEL_THREADS:
      threads = atoi(optarg);
      break;

    case PARALLEL_SEPARATE_OUTPUT:
      separateOutput = true;
      break;

    case PORTFOLIO_FILTER_LENGTH:
      sharingFilterByLength = atoi(optarg);
      break;

    case ':':
      // This can be a long or short option, and the way to get at the name of it is different.
      if(optopt == 0 ||  // was a long option
         (optopt >= OPTION_VALUE_BEGIN && optopt <= OPTION_VALUE_END)) { // OptionValue option
        throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument");
      } else { // was a short option
        throw OptionException(string("option `-") + char(optopt) + "' missing its required argument");
      }

    case '?':
    default:
      if(optopt == 0 &&
         !strncmp(argv[optind - 1], "--thread", 8) &&
         strlen(argv[optind - 1]) > 8 &&
         isdigit(argv[optind - 1][8])) {
        int tnum = atoi(argv[optind - 1] + 8);
        threadArgv.resize(tnum + 1);
        if(threadArgv[tnum] != "") {
          threadArgv[tnum] += " ";
        }
        const char* p = strchr(argv[optind - 1] + 9, '=');
        if(p == NULL) { // e.g., we have --thread0 "foo"
          threadArgv[tnum] += argv[optind++];
        } else { // e.g., we have --thread0="foo"
          threadArgv[tnum] += p + 1;
        }
        break;
      }

      // This can be a long or short option, and the way to get at the name of it is different.
      if(optopt == 0) { // was a long option
        throw OptionException(string("can't understand option `") + argv[optind - 1] + "'");
      } else { // was a short option
        throw OptionException(string("can't understand option `-") + char(optopt) + "'");
      }
    }
  }

  if(incrementalSolving && proof) {
    throw OptionException(string("The use of --incremental with --proof is not yet supported"));
  }

  return optind;
}

void Options::setOutputLanguage(const char* str) throw(OptionException) {
  if(!strcmp(str, "cvc4") || !strcmp(str, "pl")) {
    outputLanguage = language::output::LANG_CVC4;
    return;
  } else if(!strcmp(str, "smtlib") || !strcmp(str, "smt")) {
    outputLanguage = language::output::LANG_SMTLIB;
    return;
  } else if(!strcmp(str, "smtlib2") || !strcmp(str, "smt2")) {
    outputLanguage = language::output::LANG_SMTLIB_V2;
    return;
  } else if(!strcmp(str, "tptp")) {
    outputLanguage = language::output::LANG_TPTP;
    return;
  } else if(!strcmp(str, "ast")) {
    outputLanguage = language::output::LANG_AST;
    return;
  } else if(!strcmp(str, "auto")) {
    outputLanguage = language::output::LANG_AUTO;
    return;
  }

  if(strcmp(str, "help")) {
    throw OptionException(string("unknown language for --output-lang: `") +
                          str + "'.  Try --output-lang help.");
  }

  languageHelp = true;
}

void Options::setInputLanguage(const char* str) throw(OptionException) {
  if(!strcmp(str, "cvc4") || !strcmp(str, "pl") || !strcmp(str, "presentation")) {
    inputLanguage = language::input::LANG_CVC4;
    return;
  } else if(!strcmp(str, "smtlib") || !strcmp(str, "smt")) {
    inputLanguage = language::input::LANG_SMTLIB;
    return;
  } else if(!strcmp(str, "smtlib2") || !strcmp(str, "smt2")) {
    inputLanguage = language::input::LANG_SMTLIB_V2;
    return;
  } else if(!strcmp(str, "tptp")) {
    inputLanguage = language::input::LANG_TPTP;
    return;
  } else if(!strcmp(str, "auto")) {
    inputLanguage = language::input::LANG_AUTO;
    return;
  }

  if(strcmp(str, "help")) {
    throw OptionException(string("unknown language for --lang: `") +
                          str + "'.  Try --lang help.");
  }

  languageHelp = true;
}

std::ostream& operator<<(std::ostream& out, Options::ArithHeuristicPivotRule rule) {
  switch(rule) {
  case Options::MINIMUM:
    out << "MINIMUM";
    break;
  case Options::BREAK_TIES:
    out << "BREAK_TIES";
    break;
  case Options::MAXIMUM:
    out << "MAXIMUM";
    break;
  default:
    out << "ArithPivotRule!UNKNOWN";
  }

  return out;
}

#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
#undef DO_SEMANTIC_CHECKS_BY_DEFAULT

}/* CVC4 namespace */