/******************************************************************************

 * Top contributors (to current version):

 *   Tim King, Gereon Kremer, Andrew Reynolds

 *

 * This file is part of the cvc5 project.

 *

 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS

 * in the top-level source directory and their institutional affiliations.

 * All rights reserved.  See the file COPYING in the top-level source

 * directory for licensing information.

 * ****************************************************************************

 *

 * Global (command-line, set-option, ...) parameters for SMT.

 */

#include "options/options_public.h"

#if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__)

// force use of optreset; mingw32 croaks on argv-switching otherwise

#include "base/cvc5config.h"

#define _BSD_SOURCE

#undef HAVE_DECL_OPTRESET

#define HAVE_DECL_OPTRESET 1

#define CVC5_IS_NOT_REALLY_BSD

#endif /* !_BSD_SOURCE && __MINGW32__ && !__MINGW64__ */

#ifdef __MINGW64__

extern int optreset;

#endif /* __MINGW64__ */

#include <getopt.h>

// clean up

#ifdef CVC5_IS_NOT_REALLY_BSD

#  undef _BSD_SOURCE

#endif /* CVC5_IS_NOT_REALLY_BSD */

#include "base/check.h"

#include "base/output.h"

#include "options/didyoumean.h"

#include "options/options_handler.h"

#include "options/options_listener.h"

#include "options/options.h"

#include "options/uf_options.h"

#include "options/arith_options.h"

#include "options/arrays_options.h"

#include "options/base_options.h"

#include "options/booleans_options.h"

#include "options/builtin_options.h"

#include "options/bv_options.h"

#include "options/datatypes_options.h"

#include "options/decision_options.h"

#include "options/expr_options.h"

#include "options/fp_options.h"

#include "options/main_options.h"

#include "options/parser_options.h"

#include "options/printer_options.h"

#include "options/proof_options.h"

#include "options/prop_options.h"

#include "options/quantifiers_options.h"

#include "options/sep_options.h"

#include "options/sets_options.h"

#include "options/smt_options.h"

#include "options/strings_options.h"

#include "options/theory_options.h"

#include "options/uf_options.h"

#include <cstring>

#include <iostream>

#include <limits>

namespace cvc5::options {

// clang-format off

    "\

Most commonly-used cvc5 options:\n"

"  --incremental | -i     enable incremental solving [*]\n"

"  --lang=LANG | --input-language=LANG | -L LANG\n"

"                         force input language (default is \"auto\"; see --lang\n"

"                         help)\n"

"  --output-lang=LANG | --output-language=LANG\n"

"                         force output language (default is \"auto\"; see\n"

"                         --output-lang help)\n"

"  --quiet | -q           decrease verbosity (may be repeated)\n"

"  --rlimit-per=N | --reproducible-resource-limit=N\n"

"                         set resource limit per query\n"

"  --rlimit=N             set resource limit\n"

"  --stats                give statistics on exit [*]\n"

"  --tlimit-per=MS        set time limit per query in milliseconds\n"

"  --tlimit=MS            set time limit in milliseconds of wall clock time\n"

"  --verbose | -v         increase verbosity (may be repeated)\n"

"  --copyright            show cvc5 copyright information\n"

"  --help | -h            full command line reference\n"

"  --seed=N | -s N        seed for random number generator\n"

"  --show-config          show cvc5 static configuration\n"

"  --version | -V         identify this cvc5 binary\n"

"  --strict-parsing       be less tolerant of non-conforming inputs [*]\n"

"  --dump-to=FILE         all dumping goes to FILE (instead of stdout)\n"

"  --dump=MODE            dump preprocessed assertions, etc., see --dump=help\n"

"  --produce-assertions   keep an assertions list (enables get-assertions\n"

"                         command) [*]\n"

"  --produce-models | -m  support the get-value and get-model commands [*]\n"

    ;

    mostCommonOptionsDescription + "\n\nAdditional cvc5 options:\n"

"\nFrom the Arithmetic Theory module:\n"

"  --approx-branch-depth=N\n"

"                         maximum branch depth the approximate solver is allowed\n"

"                         to take\n"

"  --arith-brab           whether to use simple rounding, similar to a unit-cube\n"

"                         test, for integers [*]\n"

"  --arith-cong-man       (experimental) whether to use the congruence manager\n"

"                         when the equality solver is enabled [*]\n"

"  --arith-eq-solver      whether to use the equality solver in the theory of\n"

"                         arithmetic [*]\n"

"  --arith-no-partial-fun do not use partial function semantics for arithmetic\n"

"                         (not SMT LIB compliant) [*]\n"

"  --arith-prop-clauses=N rows shorter than this are propagated as clauses\n"

"  --arith-prop=MODE      turns on arithmetic propagation (default is 'old', see\n"

"                         --arith-prop=help)\n"

"  --arith-rewrite-equalities\n"

"                         turns on the preprocessing rewrite turning equalities\n"

"                         into a conjunction of inequalities [*]\n"

"  --collect-pivot-stats  collect the pivot history [*]\n"

"  --cut-all-bounded      turns on the integer solving step of periodically\n"

"                         cutting all integer variables that have both upper and\n"

"                         lower bounds [*]\n"

"  --dio-decomps          let skolem variables for integer divisibility\n"

"                         constraints leak from the dio solver [*]\n"

"  --dio-repeat           handle dio solver constraints in mass or one at a time\n"

"                         [*]\n"

"  --dio-solver           turns on Linear Diophantine Equation solver (Griggio,\n"

"                         JSAT 2012) [*]\n"

"  --dio-turns=N          turns in a row dio solver cutting gets\n"

"  --error-selection-rule=RULE\n"

"                         change the pivot rule for the basic variable (default\n"

"                         is 'min', see --pivot-rule help)\n"

"  --fc-penalties         turns on degenerate pivot penalties [*]\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; if\n"

"                         this is unset, this is tuned by the logic selection\n"

"  --lemmas-on-replay-failure\n"

"                         attempt to use external lemmas if approximate solve\n"

"                         integer failed [*]\n"

"  --maxCutsInContext=N   maximum cuts in a given context before signalling a\n"

"                         restart\n"

"  --miplib-trick         turns on the preprocessing step of attempting to infer\n"

"                         bounds on miplib problems [*]\n"

"  --miplib-trick-subs=N  do substitution for miplib 'tmp' vars if defined in <=\n"

"                         N eliminated vars\n"

"  --new-prop             use the new row propagation system [*]\n"

"  --nl-cad               whether to use the cylindrical algebraic decomposition\n"

"                         solver for non-linear arithmetic [*]\n"

"  --nl-cad-initial       whether to use the linear model as initial guess for\n"

"                         the cylindrical algebraic decomposition solver [*]\n"

"  --nl-cad-lift=MODE     choose the CAD lifting mode (EXPERTS only)\n"

"  --nl-cad-proj=MODE     choose the CAD projection operator (EXPERTS only)\n"

"  --nl-ext-ent-conf      check for entailed conflicts in non-linear solver [*]\n"

"  --nl-ext-factor        use factoring inference in non-linear incremental\n"

"                         linearization solver [*]\n"

"  --nl-ext-inc-prec      whether to increment the precision for irrational\n"

"                         function constraints [*]\n"

"  --nl-ext-purify        purify non-linear terms at preprocess [*]\n"

"  --nl-ext-rbound        use resolution-style inference for inferring new bounds\n"

"                         in non-linear incremental linearization solver [*]\n"

"  --nl-ext-rewrite       do context-dependent simplification based on rewrites\n"

"                         in non-linear solver [*]\n"

"  --nl-ext-split-zero    initial splits on zero for all variables [*]\n"

"  --nl-ext-tf-taylor-deg=N\n"

"                         initial degree of polynomials for Taylor approximation\n"

"  --nl-ext-tf-tplanes    use non-terminating tangent plane strategy for\n"

"                         transcendental functions for non-linear incremental\n"

"                         linearization solver [*]\n"

"  --nl-ext-tplanes       use non-terminating tangent plane strategy for\n"

"                         non-linear incremental linearization solver [*]\n"

"  --nl-ext-tplanes-interleave\n"

"                         interleave tangent plane strategy for non-linear\n"

"                         incremental linearization solver [*]\n"

"  --nl-ext=MODE          incremental linearization approach to non-linear\n"

"  --nl-icp               whether to use ICP-style propagations for non-linear\n"

"                         arithmetic [*]\n"

"  --nl-rlv=MODE          choose mode for using relevance of assertions in\n"

"                         non-linear arithmetic\n"

"  --pb-rewrites          apply pseudo boolean rewrites [*]\n"

"  --pivot-threshold=N    sets the number of pivots using --pivot-rule per basic\n"

"                         variable per simplex instance before using variable\n"

"                         order\n"

"  --pp-assert-max-sub-size=N\n"

"                         threshold for substituting an equality in ppAssert\n"

"  --prop-row-length=N    sets the maximum row length to be used in propagation\n"

"  --replay-early-close-depth=N\n"

"                         multiples of the depths to try to close the approx log\n"

"                         eagerly\n"

"  --replay-failure-penalty=N\n"

"                         number of solve integer attempts to skips after a\n"

"                         numeric failure\n"

"  --replay-lemma-reject-cut=N\n"

"                         maximum complexity of any coefficient while outputting\n"

"                         replaying cut lemmas\n"

"  --replay-num-err-penalty=N\n"

"                         number of solve integer attempts to skips after a\n"

"                         numeric failure\n"

"  --replay-reject-cut=N  maximum complexity of any coefficient while replaying\n"

"                         cuts\n"

"  --replay-soi-major-threshold-pen=N\n"

"                         threshold for a major tolerance failure by the\n"

"                         approximate solver\n"

"  --replay-soi-major-threshold=T\n"

"                         threshold for a major tolerance failure by the\n"

"                         approximate solver\n"

"  --replay-soi-minor-threshold-pen=N\n"

"                         threshold for a minor tolerance failure by the\n"

"                         approximate solver\n"

"  --replay-soi-minor-threshold=T\n"

"                         threshold for a minor tolerance failure by the\n"

"                         approximate solver\n"

"  --restrict-pivots      have a pivot cap for simplex at effort levels below\n"

"                         fullEffort [*]\n"

"  --revert-arith-models-on-unsat\n"

"                         revert the arithmetic model to a known safe model on\n"

"                         unsat if one is cached [*]\n"

"  --rr-turns=N           round robin turn\n"

"  --se-solve-int         attempt to use the approximate solve integer method on\n"

"                         standard effort [*]\n"

"  --simplex-check-period=N\n"

"                         the number of pivots to do in simplex before rechecking\n"

"                         for a conflict on all variables\n"

"  --soi-qe               use quick explain to minimize the sum of infeasibility\n"

"                         conflicts [*]\n"

"  --standard-effort-variable-order-pivots=N\n"

"                         limits the number of pivots in a single invocation of\n"

"                         check() at a non-full effort level using Bland's pivot\n"

"                         rule (EXPERTS only)\n"

"  --unate-lemmas=MODE    determines which lemmas to add before solving (default\n"

"                         is 'all', see --unate-lemmas=help)\n"

"  --use-approx           attempt to use an approximate solver [*]\n"

"  --use-fcsimplex        use focusing and converging simplex (FMCAD 2013\n"

"                         submission) [*]\n"

"  --use-soi              use sum of infeasibility simplex (FMCAD 2013\n"

"                         submission) [*]\n"

"\nFrom the Arrays Theory module:\n"

"  --arrays-config=N      set different array option configurations - for\n"

"                         developers only\n"

"  --arrays-eager-index   turn on eager index splitting for generated array\n"

"                         lemmas [*]\n"

"  --arrays-eager-lemmas  turn on eager lemma generation for arrays [*]\n"

"  --arrays-exp           enable experimental features in the theory of arrays\n"

"                         [*]\n"

"  --arrays-model-based   turn on model-based array solver [*]\n"

"  --arrays-optimize-linear\n"

"                         turn on optimization for linear array terms (see de\n"

"                         Moura FMCAD 09 arrays paper) [*]\n"

"  --arrays-prop=N        propagation effort for arrays: 0 is none, 1 is some, 2\n"

"                         is full\n"

"  --arrays-reduce-sharing\n"

"                         use model information to reduce size of care graph for\n"

"                         arrays [*]\n"

"  --arrays-weak-equiv    use algorithm from Christ/Hoenicke (SMT 2014) [*]\n"

"\nFrom the Base module:\n"

"  --debug=TAG | -d TAG   debug something (e.g. -d arith), can repeat\n"

"  --output=TAG | -o TAG  Enable output tag.\n"

"  --parse-only           exit after parsing input [*]\n"

"  --preprocess-only      exit after preprocessing input [*]\n"

"  --print-success        print the \"success\" output required of SMT-LIBv2 [*]\n"

"  --rweight=VAL=N        set a single resource weight (EXPERTS only)\n"

"  --stats-all            print unchanged (defaulted) statistics as well (EXPERTS\n"

"                         only) [*]\n"

"  --stats-every-query    in incremental mode, print stats after every\n"

"                         satisfiability or validity query [*]\n"

"  --stats-expert         print expert (non-public) statistics as well (EXPERTS\n"

"                         only) [*]\n"

"  --trace=TAG | -t TAG   trace something (e.g. -t pushpop), can repeat\n"

"  --verbosity=N          the verbosity level of cvc5\n"

"\nFrom the Bitvector Theory module:\n"

"  --bitblast-aig         bitblast by first converting to AIG (implies\n"

"                         --bitblast=eager) [*]\n"

"  --bitblast=MODE        choose bitblasting mode, see --bitblast=help\n"

"  --bitwise-eq           lift equivalence with one-bit bit-vectors to be boolean\n"

"                         operations [*]\n"

"  --bool-to-bv=MODE      convert booleans to bit-vectors of size 1 at various\n"

"                         levels of aggressiveness, see --bool-to-bv=help\n"

"  --bv-aig-simp=COMMAND  abc command to run AIG simplifications (implies\n"

"                         --bitblast-aig, default is \"balance;drw\") (EXPERTS\n"

"                         only)\n"

"  --bv-alg-extf          algebraic inferences for extended functions [*]\n"

"  --bv-algebraic-budget=N\n"

"                         the budget allowed for the algebraic solver in number\n"

"                         of SAT conflicts (EXPERTS only)\n"

"  --bv-algebraic-solver  turn on experimental algebraic solver for the\n"

"                         bit-vector theory (only if --bv-solver=layered) [*]\n"

"  --bv-assert-input      assert input assertions on user-level 0 instead of\n"

"                         assuming them in the bit-vector SAT solver [*]\n"

"  --bv-eager-explanations\n"

"                         compute bit-blasting propagation explanations eagerly\n"

"                         (EXPERTS only) [*]\n"

"  --bv-eq-solver         use the equality engine for the bit-vector theory (only\n"

"                         if --bv-solver=layered) [*]\n"

"  --bv-extract-arith     enable rewrite pushing extract [i:0] over arithmetic\n"

"                         operations (can blow up) (EXPERTS only) [*]\n"

"  --bv-gauss-elim        simplify formula via Gaussian Elimination if applicable\n"

"                         (EXPERTS only) [*]\n"

"  --bv-inequality-solver turn on the inequality solver for the bit-vector theory\n"

"                         (only if --bv-solver=layered) [*]\n"

"  --bv-intro-pow2        introduce bitvector powers of two as a preprocessing\n"

"                         pass (EXPERTS only) [*]\n"

"  --bv-num-func=N        number of function symbols in conflicts that are\n"

"                         generalized (EXPERTS only)\n"

"  --bv-print-consts-as-indexed-symbols\n"

"                         print bit-vector constants in decimal (e.g. (_ bv1 4))\n"

"                         instead of binary (e.g. #b0001), applies to SMT-LIB 2.x\n"

"                         [*]\n"

"  --bv-propagate         use bit-vector propagation in the bit-blaster [*]\n"

"  --bv-quick-xplain      minimize bv conflicts using the QuickXplain algorithm\n"

"                         (EXPERTS only) [*]\n"

"  --bv-sat-solver=MODE   choose which sat solver to use, see\n"

"                         --bv-sat-solver=help (EXPERTS only)\n"

"  --bv-solver=MODE       choose bit-vector solver, see --bv-solver=help\n"

"  --bv-to-bool           lift bit-vectors of size 1 to booleans when possible\n"

"                         [*]\n"

"\nFrom the Datatypes Theory module:\n"

"  --cdt-bisimilar        do bisimilarity check for co-datatypes [*]\n"

"  --dt-binary-split      do binary splits for datatype constructor types [*]\n"

"  --dt-blast-splits      when applicable, blast splitting lemmas for all\n"

"                         variables at once [*]\n"

"  --dt-cyclic            do cyclicity check for datatypes [*]\n"

"  --dt-force-assignment  force the datatypes solver to give specific values to\n"

"                         all datatypes terms before answering sat [*]\n"

"  --dt-infer-as-lemmas   always send lemmas out instead of making internal\n"

"                         inferences [*]\n"

"  --dt-nested-rec        allow nested recursion in datatype definitions [*]\n"

"  --dt-polite-optimize   turn on optimization for polite combination [*]\n"

"  --dt-rewrite-error-sel rewrite incorrectly applied selectors to arbitrary\n"

"                         ground term (EXPERTS only) [*]\n"

"  --dt-share-sel         internally use shared selectors across multiple\n"

"                         constructors [*]\n"

"  --sygus-abort-size=N   tells enumerative sygus to only consider solutions up\n"

"                         to term size N (-1 == no limit, default)\n"

"  --sygus-fair-max       use max instead of sum for multi-function sygus\n"

"                         conjectures [*]\n"

"  --sygus-fair=MODE      if and how to apply fairness for sygus\n"

"  --sygus-sym-break      simple sygus symmetry breaking lemmas [*]\n"

"  --sygus-sym-break-agg  use aggressive checks for simple sygus symmetry\n"

"                         breaking lemmas [*]\n"

"  --sygus-sym-break-dynamic\n"

"                         dynamic sygus symmetry breaking lemmas [*]\n"

"  --sygus-sym-break-lazy lazily add symmetry breaking lemmas for terms [*]\n"

"  --sygus-sym-break-pbe  sygus symmetry breaking lemmas based on pbe conjectures\n"

"                         [*]\n"

"  --sygus-sym-break-rlv  add relevancy conditions to symmetry breaking lemmas\n"

"                         [*]\n"

"\nFrom the Decision Heuristics module:\n"

"  --decision-random-weight=N\n"

"                         assign random weights to nodes between 0 and N-1 (0:\n"

"                         disable) (EXPERTS only)\n"

"  --decision-threshold=N ignore all nodes greater than threshold in first\n"

"                         attempt to pick decision (EXPERTS only)\n"

"  --decision-use-weight  use the weight nodes (locally, by looking at children)\n"

"                         to direct recursive search (EXPERTS only) [*]\n"

"  --decision-weight-internal=HOW\n"

"                         compute weights of internal nodes using children: off,\n"

"                         max, sum, usr1 (EXPERTS only)\n"

"  --decision=MODE | --decision-mode=MODE\n"

"                         choose decision mode, see --decision=help\n"

"  --jh-rlv-order         maintain activity-based ordering for decision\n"

"                         justification heuristic (EXPERTS only) [*]\n"

"  --jh-skolem-rlv=MODE   policy for when to consider skolem definitions relevant\n"

"                         in justification heuristic (EXPERTS only)\n"

"  --jh-skolem=MODE       policy for when to satisfy skolem definitions in\n"

"                         justification heuristic (EXPERTS only)\n"

"\nFrom the Expression module:\n"

"  --dag-thresh=N         dagify common subexprs appearing > N times (1 ==\n"

"                         default, 0 == don't dagify)\n"

"  --expr-depth=N         print exprs to depth N (0 == default, -1 == no limit)\n"

"  --type-checking        type check expressions [*]\n"

"\nFrom the Floating-Point module:\n"

"  --fp-exp               Allow floating-point sorts of all sizes, rather than\n"

"                         only Float32 (8/24) or Float64 (11/53) (experimental)\n"

"                         [*]\n"

"  --fp-lazy-wb           Enable lazier word-blasting (on preNotifyFact instead\n"

"                         of registerTerm) [*]\n"

"\nFrom the Driver module:\n"

"  --dump-instantiations  output instantiations of quantified formulas after\n"

"                         every UNSAT/VALID response [*]\n"

"  --dump-instantiations-debug\n"

"                         output instantiations of quantified formulas after\n"

"                         every UNSAT/VALID response, with debug information [*]\n"

"  --dump-models          output models after every SAT/INVALID/UNKNOWN response\n"

"                         [*]\n"

"  --dump-proofs          output proofs after every UNSAT/VALID response [*]\n"

"  --dump-unsat-cores     output unsat cores after every UNSAT/VALID response [*]\n"

"  --dump-unsat-cores-full\n"

"                         dump the full unsat core, including unlabeled\n"

"                         assertions [*]\n"

"  --early-exit           do not run destructors at exit; default on except in\n"

"                         debug builds (EXPERTS only) [*]\n"

"  --force-no-limit-cpu-while-dump\n"

"                         Force no CPU limit when dumping models and proofs [*]\n"

"  --interactive          force interactive shell/non-interactive mode [*]\n"

"  --segv-spin            spin on segfault/other crash waiting for gdb [*]\n"

"  --show-debug-tags      show all available tags for debugging\n"

"  --show-trace-tags      show all available tags for tracing\n"

"\nFrom the Parser module:\n"

"  --force-logic=LOGIC    set the logic, and override all further user attempts\n"

"                         to change it (EXPERTS only)\n"

"  --global-declarations  force all declarations and definitions to be global [*]\n"

"  --mmap                 memory map file input [*]\n"

"  --semantic-checks      enable semantic checks, including type checks [*]\n"

"\nFrom the Printing module:\n"

"  --flatten-ho-chains    print (binary) application chains in a flattened way,\n"

"                         e.g. (a b c) rather than ((a b) c) [*]\n"

"  --model-format=MODE    print format mode for models, see --model-format=help\n"

"  --print-inst-full      print instantiations for formulas that do not have\n"

"                         given identifiers [*]\n"

"  --print-inst=MODE      print format for printing instantiations\n"

"\nFrom the Proof module:\n"

"  --proof-eager-checking check proofs eagerly with proof for local debugging [*]\n"

"  --proof-format-mode=MODE\n"

"                         select language of proof output\n"

"  --proof-granularity=MODE\n"

"                         modes for proof granularity\n"

"  --proof-pedantic=N     assertion failure for any incorrect rule application or\n"

"                         untrusted lemma having pedantic level <=N with proof\n"

"  --proof-print-conclusion\n"

"                         Print conclusion of proof steps when printing AST [*]\n"

"\nFrom the SAT Layer module:\n"

"  --minisat-dump-dimacs  instead of solving minisat dumps the asserted clauses\n"

"                         in Dimacs format [*]\n"

"  --minisat-elimination  use Minisat elimination [*]\n"

"  --random-freq=P | --random-frequency=P\n"

"                         sets the frequency of random decisions in the sat\n"

"                         solver (P=0.0 by default)\n"

"  --random-seed=S        sets the random seed for the sat solver\n"

"  --refine-conflicts     refine theory conflict clauses (default false) [*]\n"

"  --restart-int-base=N   sets the base restart interval for the sat solver (N=25\n"

"                         by default)\n"

"  --restart-int-inc=F    sets the restart interval increase factor for the sat\n"

"                         solver (F=3.0 by default)\n"

"\nFrom the Quantifiers module:\n"

"  --ag-miniscope-quant   perform aggressive miniscoping for quantifiers [*]\n"

"  --cegis-sample=MODE    mode for using samples in the counterexample-guided\n"

"                         inductive synthesis loop\n"

"  --cegqi                turns on counterexample-based quantifier instantiation\n"

"                         [*]\n"

"  --cegqi-all            apply counterexample-based instantiation to all\n"

"                         quantified formulas [*]\n"

"  --cegqi-bv             use word-level inversion approach for\n"

"                         counterexample-guided quantifier instantiation for\n"

"                         bit-vectors [*]\n"

"  --cegqi-bv-concat-inv  compute inverse for concat over equalities rather than\n"

"                         producing an invertibility condition [*]\n"

"  --cegqi-bv-ineq=MODE   choose mode for handling bit-vector inequalities with\n"

"                         counterexample-guided instantiation\n"

"  --cegqi-bv-interleave-value\n"

"                         interleave model value instantiation with word-level\n"

"                         inversion approach [*]\n"

"  --cegqi-bv-linear      linearize adder chains for variables [*]\n"

"  --cegqi-bv-rm-extract  replaces extract terms with variables for\n"

"                         counterexample-guided instantiation for bit-vectors [*]\n"

"  --cegqi-bv-solve-nl    try to solve non-linear bv literals using model value\n"

"                         projections [*]\n"

"  --cegqi-full           turns on full effort counterexample-based quantifier\n"

"                         instantiation, which may resort to model-value\n"

"                         instantiation [*]\n"

"  --cegqi-innermost      only process innermost quantified formulas in\n"

"                         counterexample-based quantifier instantiation [*]\n"

"  --cegqi-midpoint       choose substitutions based on midpoints of lower and\n"

"                         upper bounds for counterexample-based quantifier\n"

"                         instantiation [*]\n"

"  --cegqi-min-bounds     use minimally constrained lower/upper bound for\n"

"                         counterexample-based quantifier instantiation [*]\n"

"  --cegqi-model          guide instantiations by model values for\n"

"                         counterexample-based quantifier instantiation [*]\n"

"  --cegqi-multi-inst     when applicable, do multi instantiations per quantifier\n"

"                         per round in counterexample-based quantifier\n"

"                         instantiation [*]\n"

"  --cegqi-nested-qe      process nested quantified formulas with quantifier\n"

"                         elimination in counterexample-based quantifier\n"

"                         instantiation [*]\n"

"  --cegqi-nopt           non-optimal bounds for counterexample-based quantifier\n"

"                         instantiation [*]\n"

"  --cegqi-repeat-lit     solve literals more than once in counterexample-based\n"

"                         quantifier instantiation [*]\n"

"  --cegqi-round-up-lia   round up integer lower bounds in substitutions for\n"

"                         counterexample-based quantifier instantiation [*]\n"

"  --cegqi-sat            answer sat when quantifiers are asserted with\n"

"                         counterexample-based quantifier instantiation [*]\n"

"  --cegqi-use-inf-int    use integer infinity for vts in counterexample-based\n"

"                         quantifier instantiation [*]\n"

"  --cegqi-use-inf-real   use real infinity for vts in counterexample-based\n"

"                         quantifier instantiation [*]\n"

"  --cond-var-split-agg-quant\n"

"                         aggressive split quantified formulas that lead to\n"

"                         variable eliminations [*]\n"

"  --cond-var-split-quant split quantified formulas that lead to variable\n"

"                         eliminations [*]\n"

"  --conjecture-filter-active-terms\n"

"                         filter based on active terms [*]\n"

"  --conjecture-filter-canonical\n"

"                         filter based on canonicity [*]\n"

"  --conjecture-filter-model\n"

"                         filter based on model [*]\n"

"  --conjecture-gen       generate candidate conjectures for inductive proofs [*]\n"

"  --conjecture-gen-gt-enum=N\n"

"                         number of ground terms to generate for model filtering\n"

"  --conjecture-gen-max-depth=N\n"

"                         maximum depth of terms to consider for conjectures\n"

"  --conjecture-gen-per-round=N\n"

"                         number of conjectures to generate per instantiation\n"

"                         round\n"

"  --conjecture-gen-uee-intro\n"

"                         more aggressive merging for universal equality engine,\n"

"                         introduces terms [*]\n"

"  --conjecture-no-filter do not filter conjectures [*]\n"

"  --dt-stc-ind           apply strengthening for existential quantification over\n"

"                         datatypes based on structural induction [*]\n"

"  --dt-var-exp-quant     expand datatype variables bound to one constructor in\n"

"                         quantifiers [*]\n"

"  --e-matching           whether to do heuristic E-matching [*]\n"

"  --elim-taut-quant      eliminate tautological disjuncts of quantified formulas\n"

"                         [*]\n"

"  --ext-rewrite-quant    apply extended rewriting to bodies of quantified\n"

"                         formulas [*]\n"

"  --finite-model-find    use finite model finding heuristic for quantifier\n"

"                         instantiation [*]\n"

"  --fmf-bound            finite model finding on bounded quantification [*]\n"

"  --fmf-bound-int        finite model finding on bounded integer quantification\n"

"                         [*]\n"

"  --fmf-bound-lazy       enforce bounds for bounded quantification lazily via\n"

"                         use of proxy variables [*]\n"

"  --fmf-fmc-simple       simple models in full model check for finite model\n"

"                         finding [*]\n"

"  --fmf-fresh-dc         use fresh distinguished representative when applying\n"

"                         Inst-Gen techniques [*]\n"

"  --fmf-fun              find models for recursively defined functions, assumes\n"

"                         functions are admissible [*]\n"

"  --fmf-fun-rlv          find models for recursively defined functions, assumes\n"

"                         functions are admissible, allows empty type when\n"

"                         function is irrelevant [*]\n"

"  --fmf-inst-engine      use instantiation engine in conjunction with finite\n"

"                         model finding [*]\n"

"  --fmf-type-completion-thresh=N\n"

"                         the maximum cardinality of an interpreted type for\n"

"                         which exhaustive enumeration in finite model finding is\n"

"                         attempted\n"

"  --fs-interleave        interleave enumerative instantiation with other\n"

"                         techniques [*]\n"

"  --fs-stratify          stratify effort levels in enumerative instantiation,\n"

"                         which favors speed over fairness [*]\n"

"  --fs-sum               enumerating tuples of quantifiers by increasing the sum\n"

"                         of indices, rather than the maximum [*]\n"

"  --full-saturate-quant  enumerative instantiation: instantiate with ground\n"

"                         terms from relevant domain, then arbitrary ground terms\n"

"                         before answering unknown [*]\n"

"  --full-saturate-quant-limit=N\n"

"                         maximum number of rounds of enumerative instantiation\n"

"                         to apply (-1 means no limit)\n"

"  --full-saturate-quant-rd\n"

"                         whether to use relevant domain first for enumerative\n"

"                         instantiation strategy [*]\n"

"  --global-negate        do global negation of input formula [*]\n"

"  --ho-elim              eagerly eliminate higher-order constraints [*]\n"

"  --ho-elim-store-ax     use store axiom during ho-elim [*]\n"

"  --ho-matching          do higher-order matching algorithm for triggers with\n"

"                         variable operators [*]\n"

"  --ho-matching-var-priority\n"

"                         give priority to variable arguments over constant\n"

"                         arguments [*]\n"

"  --ho-merge-term-db     merge term indices modulo equality [*]\n"

"  --increment-triggers   generate additional triggers as needed during search\n"

"                         [*]\n"

"  --inst-level-input-only\n"

"                         only input terms are assigned instantiation level zero\n"

"                         [*]\n"

"  --inst-max-level=N     maximum inst level of terms used to instantiate\n"

"                         quantified formulas with (-1 == no limit, default)\n"

"  --inst-max-rounds=N    maximum number of instantiation rounds (-1 == no limit,\n"

"                         default)\n"

"  --inst-no-entail       do not consider instances of quantified formulas that\n"

"                         are currently entailed [*]\n"

"  --inst-when-phase=N    instantiation rounds quantifiers takes (>=1) before\n"

"                         allowing theory combination to happen\n"

"  --inst-when-strict-interleave\n"

"                         ensure theory combination and standard quantifier\n"

"                         effort strategies take turns [*]\n"

"  --inst-when-tc-first   allow theory combination to happen once initially,\n"

"                         before quantifier strategies are run [*]\n"

"  --inst-when=MODE       when to apply instantiation\n"

"  --int-wf-ind           apply strengthening for integers based on well-founded\n"

"                         induction [*]\n"

"  --ite-dtt-split-quant  split ites with dt testers as conditions [*]\n"

"  --ite-lift-quant=MODE  ite lifting mode for quantified formulas\n"

"  --literal-matching=MODE\n"

"                         choose literal matching mode\n"

"  --macros-quant         perform quantifiers macro expansion [*]\n"

"  --macros-quant-mode=MODE\n"

"                         mode for quantifiers macro expansion\n"

"  --mbqi-interleave      interleave model-based quantifier instantiation with\n"

"                         other techniques [*]\n"

"  --mbqi-one-inst-per-round\n"

"                         only add one instantiation per quantifier per round for\n"

"                         mbqi [*]\n"

"  --mbqi=MODE            choose mode for model-based quantifier instantiation\n"

"  --miniscope-quant      miniscope quantifiers [*]\n"

"  --miniscope-quant-fv   miniscope quantifiers for ground subformulas [*]\n"

"  --multi-trigger-cache  caching version of multi triggers [*]\n"

"  --multi-trigger-linear implementation of multi triggers where maximum number\n"

"                         of instantiations is linear wrt number of ground terms\n"

"                         [*]\n"

"  --multi-trigger-priority\n"

"                         only try multi triggers if single triggers give no\n"

"                         instantiations [*]\n"

"  --multi-trigger-when-single\n"

"                         select multi triggers when single triggers exist [*]\n"

"  --partial-triggers     use triggers that do not contain all free variables [*]\n"

"  --pool-inst            pool-based instantiation: instantiate with ground terms\n"

"                         occurring in user-specified pools [*]\n"

"  --pre-skolem-quant     apply skolemization eagerly to bodies of quantified\n"

"                         formulas [*]\n"

"  --pre-skolem-quant-agg apply skolemization to quantified formulas aggressively\n"

"                         [*]\n"

"  --pre-skolem-quant-nested\n"

"                         apply skolemization to nested quantified formulas [*]\n"

"  --prenex-quant-user    prenex quantified formulas with user patterns [*]\n"

"  --prenex-quant=MODE    prenex mode for quantified formulas\n"

"  --purify-triggers      purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto\n"

"                         y-1 [*]\n"

"  --qcf-all-conflict     add all available conflicting instances during\n"

"                         conflict-based instantiation [*]\n"

"  --qcf-eager-check-rd   optimization, eagerly check relevant domain of matched\n"

"                         position [*]\n"

"  --qcf-eager-test       optimization, test qcf instances eagerly [*]\n"

"  --qcf-nested-conflict  consider conflicts for nested quantifiers [*]\n"

"  --qcf-skip-rd          optimization, skip instances based on possibly\n"

"                         irrelevant portions of quantified formulas [*]\n"

"  --qcf-tconstraint      enable entailment checks for t-constraints in qcf\n"

"                         algorithm [*]\n"

"  --qcf-vo-exp           qcf experimental variable ordering [*]\n"

"  --quant-alpha-equiv    infer alpha equivalence between quantified formulas [*]\n"

"  --quant-cf             enable conflict find mechanism for quantifiers [*]\n"

"  --quant-cf-mode=MODE   what effort to apply conflict find mechanism\n"

"  --quant-cf-when=MODE   when to invoke conflict find mechanism for quantifiers\n"

"  --quant-dsplit-mode=MODE\n"

"                         mode for dynamic quantifiers splitting\n"

"  --quant-fun-wd         assume that function defined by quantifiers are well\n"

"                         defined [*]\n"

"  --quant-ind            use all available techniques for inductive reasoning\n"

"                         [*]\n"

"  --quant-rep-mode=MODE  selection mode for representatives in quantifiers\n"

"                         engine\n"

"  --quant-split          apply splitting to quantified formulas based on\n"

"                         variable disjoint disjuncts [*]\n"

"  --register-quant-body-terms\n"

"                         consider ground terms within bodies of quantified\n"

"                         formulas for matching [*]\n"

"  --relational-triggers  choose relational triggers such as x = f(y), x >= f(y)\n"

"                         [*]\n"

"  --relevant-triggers    prefer triggers that are more relevant based on SInE\n"

"                         style analysis [*]\n"

"  --sygus                use sygus solver (default is true for sygus inputs) [*]\n"

"  --sygus-active-gen-cfactor=N\n"

"                         the branching factor for the number of interpreted\n"

"                         constants to consider for each size when using\n"

"                         --sygus-active-gen=enum\n"

"  --sygus-active-gen=MODE\n"

"                         mode for actively-generated sygus enumerators\n"

"  --sygus-add-const-grammar\n"

"                         statically add constants appearing in conjecture to\n"

"                         grammars [*]\n"

"  --sygus-arg-relevant   static inference techniques for computing whether\n"

"                         arguments of functions-to-synthesize are relevant [*]\n"

"  --sygus-auto-unfold    enable approach which automatically unfolds transition\n"

"                         systems for directly solving invariant synthesis\n"

"                         problems [*]\n"

"  --sygus-bool-ite-return-const\n"

"                         Only use Boolean constants for return values in\n"

"                         unification-based function synthesis [*]\n"

"  --sygus-core-connective\n"

"                         use unsat core analysis to construct Boolean connective\n"

"                         to sygus conjectures [*]\n"

"  --sygus-crepair-abort  abort if constant repair techniques are not applicable\n"

"                         [*]\n"

"  --sygus-eval-opt       use optimized approach for evaluation in sygus [*]\n"

"  --sygus-eval-unfold    do unfolding of sygus evaluation functions [*]\n"

"  --sygus-eval-unfold-bool\n"

"                         do unfolding of Boolean evaluation functions that\n"

"                         appear in refinement lemmas [*]\n"

"  --sygus-expr-miner-check-timeout=N\n"

"                         timeout (in milliseconds) for satisfiability checks in\n"

"                         expression miners\n"

"  --sygus-ext-rew        use extended rewriter for sygus [*]\n"

"  --sygus-filter-sol-rev compute backwards filtering to compute whether previous\n"

"                         solutions are filtered based on later ones (EXPERTS\n"

"                         only) [*]\n"

"  --sygus-filter-sol=MODE\n"

"                         mode for filtering sygus solutions\n"

"  --sygus-grammar-cons=MODE\n"

"                         mode for SyGuS grammar construction\n"

"  --sygus-grammar-norm   statically normalize sygus grammars based on flattening\n"

"                         (linearization) [*]\n"

"  --sygus-inference      attempt to preprocess arbitrary inputs to sygus\n"

"                         conjectures [*]\n"

"  --sygus-inst           Enable SyGuS instantiation quantifiers module [*]\n"

"  --sygus-inst-mode=MODE select instantiation lemma mode\n"

"  --sygus-inst-scope=MODE\n"

"                         select scope of ground terms\n"

"  --sygus-inst-term-sel=MODE\n"

"                         granularity for ground terms\n"

"  --sygus-inv-templ-when-sg\n"

"                         use invariant templates (with solution reconstruction)\n"

"                         for syntax guided problems [*]\n"

"  --sygus-inv-templ=MODE template mode for sygus invariant synthesis (weaken\n"

"                         pre-condition, strengthen post-condition, or none)\n"

"  --sygus-min-grammar    statically minimize sygus grammars [*]\n"

"  --sygus-pbe            enable approach which unifies conditional solutions,\n"

"                         specialized for programming-by-examples (pbe)\n"

"                         conjectures [*]\n"

"  --sygus-pbe-multi-fair when using multiple enumerators, ensure that we only\n"

"                         register value of minimial term size [*]\n"

"  --sygus-pbe-multi-fair-diff=N\n"

"                         when using multiple enumerators, ensure that we only\n"

"                         register values of minimial term size plus this value\n"

"                         (default 0)\n"

"  --sygus-qe-preproc     use quantifier elimination as a preprocessing step for\n"

"                         sygus [*]\n"

"  --sygus-query-gen      use sygus to enumerate interesting satisfiability\n"

"                         queries [*]\n"

"  --sygus-query-gen-check\n"

"                         use interesting satisfiability queries to check\n"

"                         soundness of cvc5 [*]\n"

"  --sygus-query-gen-dump-files=MODE\n"

"                         mode for dumping external files corresponding to\n"

"                         interesting satisfiability queries with sygus-query-gen\n"

"  --sygus-query-gen-thresh=N\n"

"                         number of points that we allow to be equal for\n"

"                         enumerating satisfiable queries with sygus-query-gen\n"

"  --sygus-rec-fun        enable efficient support for recursive functions in\n"

"                         sygus grammars [*]\n"

"  --sygus-rec-fun-eval-limit=N\n"

"                         use a hard limit for how many times in a given\n"

"                         evaluator call a recursive function can be evaluated\n"

"                         (so infinite loops can be avoided)\n"

"  --sygus-repair-const   use approach to repair constants in sygus candidate\n"

"                         solutions [*]\n"

"  --sygus-repair-const-timeout=N\n"

"                         timeout (in milliseconds) for the satisfiability check\n"

"                         to repair constants in sygus candidate solutions\n"

"  --sygus-rr             use sygus to enumerate and verify correctness of\n"

"                         rewrite rules [*]\n"

"  --sygus-rr-synth       use sygus to enumerate candidate rewrite rules [*]\n"

"  --sygus-rr-synth-accel add dynamic symmetry breaking clauses based on\n"

"                         candidate rewrites [*]\n"

"  --sygus-rr-synth-check use satisfiability check to verify correctness of\n"

"                         candidate rewrites [*]\n"

"  --sygus-rr-synth-filter-cong\n"

"                         filter candidate rewrites based on congruence [*]\n"

"  --sygus-rr-synth-filter-match\n"

"                         filter candidate rewrites based on matching [*]\n"

"  --sygus-rr-synth-filter-nl\n"

"                         filter non-linear candidate rewrites [*]\n"

"  --sygus-rr-synth-filter-order\n"

"                         filter candidate rewrites based on variable ordering\n"

"                         [*]\n"

"  --sygus-rr-synth-input synthesize rewrite rules based on the input formula [*]\n"

"  --sygus-rr-synth-input-nvars=N\n"

"                         the maximum number of variables per type that appear in\n"

"                         rewrites from sygus-rr-synth-input\n"

"  --sygus-rr-synth-input-use-bool\n"

"                         synthesize Boolean rewrite rules based on the input\n"

"                         formula [*]\n"

"  --sygus-rr-synth-rec   synthesize rewrite rules over all sygus grammar types\n"

"                         recursively [*]\n"

"  --sygus-rr-verify      use sygus to verify the correctness of rewrite rules\n"

"                         via sampling [*]\n"

"  --sygus-rr-verify-abort\n"

"                         abort when sygus-rr-verify finds an instance of\n"

"                         unsoundness [*]\n"

"  --sygus-sample-fp-uniform\n"

"                         sample floating-point values uniformly instead of in a\n"

"                         biased fashion [*]\n"

"  --sygus-sample-grammar when applicable, use grammar for choosing sample points\n"

"                         [*]\n"

"  --sygus-samples=N      number of points to consider when doing sygus rewriter\n"

"                         sample testing\n"

"  --sygus-si-abort       abort if synthesis conjecture is not single invocation\n"

"                         [*]\n"

"  --sygus-si-partial     combined techniques for synthesis conjectures that are\n"

"                         partially single invocation [*]\n"

"  --sygus-si-rcons-limit=N\n"

"                         number of rounds of enumeration to use during solution\n"

"                         reconstruction (negative means unlimited)\n"

"  --sygus-si-rcons=MODE  policy for reconstructing solutions for single\n"

"                         invocation conjectures\n"

"  --sygus-si-reconstruct-const\n"

"                         include constants when reconstruct solutions for single\n"

"                         invocation conjectures in original grammar [*]\n"

"  --sygus-si=MODE        mode for processing single invocation synthesis\n"

"                         conjectures\n"

"  --sygus-stream         enumerate a stream of solutions instead of terminating\n"

"                         after the first one [*]\n"

"  --sygus-templ-embed-grammar\n"

"                         embed sygus templates into grammars [*]\n"

"  --sygus-unif-cond-independent-no-repeat-sol\n"

"                         Do not try repeated solutions when using independent\n"

"                         synthesis of conditions in unification-based function\n"

"                         synthesis [*]\n"

"  --sygus-unif-pi=MODE   mode for synthesis via piecewise-indepedent unification\n"

"  --sygus-unif-shuffle-cond\n"

"                         Shuffle condition pool when building solutions (may\n"

"                         change solutions sizes) [*]\n"

"  --sygus-verify-inst-max-rounds=N\n"

"                         maximum number of instantiation rounds for sygus\n"

"                         verification calls (-1 == no limit, default is 3)\n"

"  --term-db-cd           register terms in term database based on the SAT\n"

"                         context [*]\n"

"  --term-db-mode=MODE    which ground terms to consider for instantiation\n"

"  --trigger-active-sel=MODE\n"

"                         selection mode to activate triggers\n"

"  --trigger-sel=MODE     selection mode for triggers\n"

"  --user-pat=MODE        policy for handling user-provided patterns for\n"

"                         quantifier instantiation\n"

"  --var-elim-quant       enable simple variable elimination for quantified\n"

"                         formulas [*]\n"

"  --var-ineq-elim-quant  enable variable elimination based on infinite\n"

"                         projection of unbound arithmetic variables [*]\n"

"\nFrom the Separation Logic Theory module:\n"

"  --sep-check-neg        check negated spatial assertions [*]\n"

"  --sep-child-refine     child-specific refinements of negated star, positive\n"

"                         wand [*]\n"

"  --sep-deq-c            assume cardinality elements are distinct [*]\n"

"  --sep-exp              experimental flag for sep [*]\n"

"  --sep-min-refine       only add refinement lemmas for minimal (innermost)\n"

"                         assertions [*]\n"

"  --sep-pre-skolem-emp   eliminate emp constraint at preprocess time [*]\n"

"\nFrom the Sets Theory module:\n"

"  --sets-ext             enable extended symbols such as complement and universe\n"

"                         in theory of sets [*]\n"

"  --sets-infer-as-lemmas send inferences as lemmas [*]\n"

"  --sets-proxy-lemmas    introduce proxy variables eagerly to shorten lemmas [*]\n"

"\nFrom the SMT Layer module:\n"

"  --abstract-values      in models, output arrays (and in future, maybe others)\n"

"                         using abstract values, as required by the SMT-LIB\n"

"                         standard [*]\n"

"  --ackermann            eliminate functions by ackermannization [*]\n"

"  --block-models=MODE    mode for producing several models\n"

"  --check-abducts        checks whether produced solutions to get-abduct are\n"

"                         correct [*]\n"

"  --check-interpols      checks whether produced solutions to get-interpol are\n"

"                         correct [*]\n"

"  --check-models         after SAT/INVALID/UNKNOWN, check that the generated\n"

"                         model satisfies user assertions [*]\n"

"  --check-proofs         after UNSAT/VALID, check the generated proof (with\n"

"                         proof) [*]\n"

"  --check-synth-sol      checks whether produced solutions to\n"

"                         functions-to-synthesize satisfy the conjecture [*]\n"

"  --check-unsat-cores    after UNSAT/VALID, produce and check an unsat core\n"

"                         (expensive) [*]\n"

"  --debug-check-models   after SAT/INVALID/UNKNOWN, check that the generated\n"

"                         model satisfies user and internal assertions [*]\n"

"  --early-ite-removal    remove ITEs early in preprocessing [*]\n"

"  --expand-definitions   always expand symbol definitions in output [*]\n"

"  --ext-rew-prep         use extended rewriter as a preprocessing pass [*]\n"

"  --ext-rew-prep-agg     use aggressive extended rewriter as a preprocessing\n"

"                         pass [*]\n"

"  --foreign-theory-rewrite\n"

"                         Cross-theory rewrites [*]\n"

"  --ite-simp             turn on ite simplification (Kim (and Somenzi) et al.,\n"

"                         SAT 2009) [*]\n"

"  --learned-rewrite      rewrite the input based on learned literals [*]\n"

"  --minimal-unsat-cores  if an unsat core is produced, it is reduced to a\n"

"                         minimal unsat core [*]\n"

"  --model-cores=MODE     mode for producing model cores\n"

"  --model-u-print=MODE | --model-uninterp-print=MODE\n"

"                         determines how to print uninterpreted elements in\n"

"                         models\n"

"  --model-witness-value  in models, use a witness constant for choice functions\n"

"                         [*]\n"

"  --on-repeat-ite-simp   do the ite simplification pass again if repeating\n"

"                         simplification [*]\n"

"  --produce-assignments  support the get-assignment command [*]\n"

"  --produce-proofs       produce proofs, support check-proofs and get-proof [*]\n"

"  --produce-unsat-assumptions\n"

"                         turn on unsat assumptions generation [*]\n"

"  --produce-unsat-cores  turn on unsat core generation. Unless otherwise\n"

"                         specified, cores will be produced using SAT soving\n"

"                         under assumptions and preprocessing proofs. [*]\n"

"  --repeat-simp          make multiple passes with nonclausal simplifier [*]\n"

"  --simp-ite-compress    enables compressing ites after ite simplification [*]\n"

"  --simp-ite-hunt-zombies=N\n"

"                         post ite compression enables zombie removal while the\n"

"                         number of nodes is above this threshold\n"

"  --simp-with-care       enables simplifyWithCare in ite simplificiation [*]\n"

"  --simplification=MODE | --simplification-mode=MODE\n"

"                         choose simplification mode, see --simplification=help\n"

"  --sort-inference       calculate sort inference of input problem, convert the\n"

"                         input based on monotonic sorts [*]\n"

"  --static-learning      use static learning (on by default) [*]\n"

"  --sygus-out=MODE       output mode for sygus\n"

"  --sygus-print-callbacks\n"

"                         use sygus print callbacks to print sygus terms in the\n"

"                         user-provided form (disable for debugging) [*]\n"

"  --unconstrained-simp   turn on unconstrained simplification (see\n"

"                         Bruttomesso/Brummayer PhD thesis). Fully supported only\n"

"                         in (subsets of) the logic QF_ABV. [*]\n"

"  --unsat-cores-mode=MODE\n"

"                         choose unsat core mode, see --unsat-cores-mode=help\n"

"\nFrom the Strings Theory module:\n"

"  --re-elim              elimination techniques for regular expressions [*]\n"

"  --re-elim-agg          aggressive elimination techniques for regular\n"

"                         expressions [*]\n"

"  --re-inter-mode=MODE   determines which regular expressions intersections to\n"

"                         compute (EXPERTS only)\n"

"  --strings-check-entail-len\n"

"                         check entailment between length terms to reduce\n"

"                         splitting [*]\n"

"  --strings-eager        strings eager check [*]\n"

"  --strings-eager-eval   perform eager context-dependent evaluation for\n"

"                         applications of string kinds [*]\n"

"  --strings-eager-len    strings eager length lemmas [*]\n"

"  --strings-exp          experimental features in the theory of strings [*]\n"

"  --strings-ff           do flat form inferences [*]\n"

"  --strings-fmf          the finite model finding used by the theory of strings\n"

"                         [*]\n"

"  --strings-guess-model  use model guessing to avoid string extended function\n"

"                         reductions [*]\n"

"  --strings-infer-as-lemmas\n"

"                         always send lemmas out instead of making internal\n"

"                         inferences [*]\n"

"  --strings-infer-sym    strings split on empty string [*]\n"

"  --strings-lazy-pp      perform string preprocessing lazily [*]\n"

"  --strings-len-norm     strings length normalization lemma [*]\n"

"  --strings-lprop-csp    do length propagation based on constant splits [*]\n"

"  --strings-min-prefix-explain\n"

"                         minimize explanations for prefix of normal forms in\n"

"                         strings [*]\n"

"  --strings-process-loop-mode=MODE\n"

"                         determines how to process looping string equations\n"

"                         (EXPERTS only)\n"

"  --strings-rexplain-lemmas\n"

"                         regression explanations for string lemmas [*]\n"

"  --strings-unified-vspt use a single skolem for the variable splitting rule [*]\n"

"\nFrom the Theory Layer module:\n"

"  --assign-function-values\n"

"                         assign values for uninterpreted functions in models [*]\n"

"  --condense-function-values\n"

"                         condense values for functions in models rather than\n"

"                         explicitly representing them [*]\n"

"  --ee-mode=MODE         mode for managing equalities across theory solvers\n"

"                         (EXPERTS only)\n"

"  --relevance-filter     enable analysis of relevance of asserted literals with\n"

"                         respect to the input formula [*]\n"

"  --tc-mode=MODE         mode for theory combination (EXPERTS only)\n"

"  --theoryof-mode=MODE   mode for Theory::theoryof() (EXPERTS only)\n"

"\nFrom the Uninterpreted Functions Theory module:\n"

"  --symmetry-breaker | --uf-symmetry-breaker\n"

"                         use UF symmetry breaker (Deharbe et al., CADE 2011) [*]\n"

"  --uf-ho                enable support for higher-order reasoning [*]\n"

"  --uf-ho-ext            apply extensionality on function symbols [*]\n"

"  --uf-ss-abort-card=N   tells the uf with cardinality to only consider models\n"

"                         that interpret uninterpreted sorts of cardinality at\n"

"                         most N (-1 == no limit, default)\n"

"  --uf-ss-fair           use fair strategy for finite model finding multiple\n"

"                         sorts [*]\n"

"  --uf-ss-fair-monotone  group monotone sorts when enforcing fairness for finite\n"

"                         model finding [*]\n"

"  --uf-ss-totality-limited=N\n"

"                         apply totality axioms, but only up to cardinality N (-1\n"

"                         == do not apply totality axioms, default)\n"

"  --uf-ss-totality-sym-break\n"

"                         apply symmetry breaking for totality axioms [*]\n"

"  --uf-ss=MODE           mode of operation for uf with cardinality solver.\n";

[*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\

    sense of the option.\n\

";

    "\

Languages currently supported as arguments to the -L / --lang option:\n\

  auto                           attempt to automatically determine language\n\

  cvc | presentation | pl        CVC presentation language\n\

  smt | smtlib | smt2 |\n\

  smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard\n\

  tptp                           TPTP format (cnf, fof and tff)\n\

  sygus | sygus2                 SyGuS version 2.0\n\

\n\

Languages currently supported as arguments to the --output-lang option:\n\

  auto                           match output language to input language\n\

  cvc | presentation | pl        CVC presentation language\n\

  smt | smtlib | smt2 |\n\

  smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard\n\

  tptp                           TPTP format\n\

  ast                            internal format (simple syntax trees)\n\

";

// clang-format on

{

}

/** Set a given Options* as "current" just for a particular scope. */

class OptionsGuard {

  Options** d_field;

  Options* d_old;

public:

    d_field(field),

};/* class OptionsGuard */

/**

 * 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 parse().

 */

// clang-format off

static struct option cmdlineOptions[] = {

  { "approx-branch-depth", required_argument, nullptr, 256 },

  { "arith-brab", no_argument, nullptr, 257 },

  { "no-arith-brab", no_argument, nullptr, 258 },

  { "arith-cong-man", no_argument, nullptr, 259 },

  { "no-arith-cong-man", no_argument, nullptr, 260 },

  { "arith-eq-solver", no_argument, nullptr, 261 },

  { "no-arith-eq-solver", no_argument, nullptr, 262 },

  { "arith-no-partial-fun", no_argument, nullptr, 263 },

  { "no-arith-no-partial-fun", no_argument, nullptr, 264 },

  { "arith-prop-clauses", required_argument, nullptr, 265 },

  { "arith-prop", required_argument, nullptr, 266 },

  { "arith-rewrite-equalities", no_argument, nullptr, 267 },

  { "no-arith-rewrite-equalities", no_argument, nullptr, 268 },

  { "collect-pivot-stats", no_argument, nullptr, 269 },

  { "no-collect-pivot-stats", no_argument, nullptr, 270 },

  { "cut-all-bounded", no_argument, nullptr, 271 },

  { "no-cut-all-bounded", no_argument, nullptr, 272 },

  { "dio-decomps", no_argument, nullptr, 273 },

  { "no-dio-decomps", no_argument, nullptr, 274 },

  { "dio-repeat", no_argument, nullptr, 275 },

  { "no-dio-repeat", no_argument, nullptr, 276 },

  { "dio-solver", no_argument, nullptr, 277 },

  { "no-dio-solver", no_argument, nullptr, 278 },

  { "dio-turns", required_argument, nullptr, 279 },

  { "error-selection-rule", required_argument, nullptr, 280 },

  { "fc-penalties", no_argument, nullptr, 281 },

  { "no-fc-penalties", no_argument, nullptr, 282 },

  { "heuristic-pivots", required_argument, nullptr, 283 },

  { "lemmas-on-replay-failure", no_argument, nullptr, 284 },

  { "no-lemmas-on-replay-failure", no_argument, nullptr, 285 },

  { "maxCutsInContext", required_argument, nullptr, 286 },

  { "miplib-trick", no_argument, nullptr, 287 },

  { "no-miplib-trick", no_argument, nullptr, 288 },

  { "miplib-trick-subs", required_argument, nullptr, 289 },

  { "new-prop", no_argument, nullptr, 290 },

  { "no-new-prop", no_argument, nullptr, 291 },

  { "nl-cad", no_argument, nullptr, 292 },

  { "no-nl-cad", no_argument, nullptr, 293 },

  { "nl-cad-initial", no_argument, nullptr, 294 },

  { "no-nl-cad-initial", no_argument, nullptr, 295 },

  { "nl-cad-lift", required_argument, nullptr, 296 },

  { "nl-cad-proj", required_argument, nullptr, 297 },

  { "nl-ext-ent-conf", no_argument, nullptr, 298 },

  { "no-nl-ext-ent-conf", no_argument, nullptr, 299 },

  { "nl-ext-factor", no_argument, nullptr, 300 },

  { "no-nl-ext-factor", no_argument, nullptr, 301 },

  { "nl-ext-inc-prec", no_argument, nullptr, 302 },

  { "no-nl-ext-inc-prec", no_argument, nullptr, 303 },

  { "nl-ext-purify", no_argument, nullptr, 304 },

  { "no-nl-ext-purify", no_argument, nullptr, 305 },

  { "nl-ext-rbound", no_argument, nullptr, 306 },

  { "no-nl-ext-rbound", no_argument, nullptr, 307 },

  { "nl-ext-rewrite", no_argument, nullptr, 308 },

  { "no-nl-ext-rewrite", no_argument, nullptr, 309 },

  { "nl-ext-split-zero", no_argument, nullptr, 310 },

  { "no-nl-ext-split-zero", no_argument, nullptr, 311 },

  { "nl-ext-tf-taylor-deg", required_argument, nullptr, 312 },

  { "nl-ext-tf-tplanes", no_argument, nullptr, 313 },

  { "no-nl-ext-tf-tplanes", no_argument, nullptr, 314 },

  { "nl-ext-tplanes", no_argument, nullptr, 315 },

  { "no-nl-ext-tplanes", no_argument, nullptr, 316 },

  { "nl-ext-tplanes-interleave", no_argument, nullptr, 317 },

  { "no-nl-ext-tplanes-interleave", no_argument, nullptr, 318 },

  { "nl-ext", required_argument, nullptr, 319 },

  { "nl-icp", no_argument, nullptr, 320 },

  { "no-nl-icp", no_argument, nullptr, 321 },

  { "nl-rlv", required_argument, nullptr, 322 },

  { "pb-rewrites", no_argument, nullptr, 323 },

  { "no-pb-rewrites", no_argument, nullptr, 324 },

  { "pivot-threshold", required_argument, nullptr, 325 },

  { "pp-assert-max-sub-size", required_argument, nullptr, 326 },

  { "prop-row-length", required_argument, nullptr, 327 },

  { "replay-early-close-depth", required_argument, nullptr, 328 },