id     = "BASE"
name   = "Base"

[[option]]
  name       = "err"
  category   = "undocumented"
  long       = "err=erroutput"
  type       = "ManagedErr"
  alias      = ["diagnostic-output-channel"]
  predicates = ["setErrStream"]
  includes   = ["<iostream>", "options/managed_streams.h"]

[[option]]
  name       = "in"
  category   = "undocumented"
  long       = "in=input"
  type       = "ManagedIn"
  includes   = ["<iostream>", "options/managed_streams.h"]

[[option]]
  name       = "out"
  category   = "undocumented"
  long       = "out=output"
  type       = "ManagedOut"
  alias      = ["regular-output-channel"]
  includes   = ["<iostream>", "options/managed_streams.h"]

[[option]]
  name       = "inputLanguage"
  alias      = ["input-language"]
  category   = "common"
  short      = "L"
  long       = "lang=LANG"
  type       = "Language"
  default    = "Language::LANG_AUTO"
  handler    = "stringToLanguage"
  predicates = ["languageIsNotAST"]
  includes   = ["options/language.h"]
  help       = "force input language (default is \"auto\"; see --lang help)"

[[option]]
  name       = "outputLanguage"
  alias      = ["output-language"]
  category   = "common"
  long       = "output-lang=LANG"
  type       = "Language"
  default    = "Language::LANG_AUTO"
  handler    = "stringToLanguage"
  predicates = ["applyOutputLanguage"]
  includes   = ["options/language.h"]
  help       = "force output language (default is \"auto\"; see --output-lang help)"

[[option]]
  name       = "verbosity"
  long       = "verbosity=N"
  category   = "regular"
  type       = "int64_t"
  default    = "0"
  predicates = ["setVerbosity"]
  help       = "the verbosity level of cvc5"

[[option]]
  category   = "common"
  short      = "v"
  long       = "verbose"
  type       = "void"
  handler    = "increaseVerbosity"
  help       = "increase verbosity (may be repeated)"

[[option]]
  category   = "common"
  short      = "q"
  long       = "quiet"
  type       = "void"
  handler    = "decreaseVerbosity"
  help       = "decrease verbosity (may be repeated)"

[[option]]
  name       = "incrementalSolving"
  category   = "common"
  short      = "i"
  long       = "incremental"
  type       = "bool"
  default    = "true"
  help       = "enable incremental solving"

[[option]]
  name       = "statistics"
  long       = "stats"
  category   = "common"
  type       = "bool"
  predicates = ["setStats"]
  help       = "give statistics on exit"

[[option]]
  name       = "statisticsAll"
  long       = "stats-all"
  category   = "expert"
  type       = "bool"
  predicates = ["setStatsDetail"]
  help       = "print unchanged (defaulted) statistics as well"

[[option]]
  name       = "statisticsExpert"
  long       = "stats-expert"
  category   = "expert"
  type       = "bool"
  predicates = ["setStatsDetail"]
  help       = "print expert (non-public) statistics as well"

[[option]]
  name       = "statisticsEveryQuery"
  long       = "stats-every-query"
  category   = "regular"
  type       = "bool"
  predicates = ["setStatsDetail"]
  default    = "false"
  help       = "in incremental mode, print stats after every satisfiability or validity query"

[[option]]
  name       = "parseOnly"
  category   = "regular"
  long       = "parse-only"
  type       = "bool"
  help       = "exit after parsing input"

[[option]]
  name       = "preprocessOnly"
  category   = "regular"
  long       = "preprocess-only"
  type       = "bool"
  help       = "exit after preprocessing input"

[[option]]
  category   = "regular"
  short      = "t"
  long       = "trace=TAG"
  type       = "std::string"
  handler    = "enableTraceTag"
  help       = "trace something (e.g. -t pushpop), can repeat"

[[option]]
  category   = "regular"
  short      = "d"
  long       = "debug=TAG"
  type       = "std::string"
  handler    = "enableDebugTag"
  help       = "debug something (e.g. -d arith), can repeat"

[[option]]
  name       = "outputTag"
  short      = "o"
  long       = "output=TAG"
  type       = "OutputTag"
  default    = "NONE"
  handler    = "enableOutputTag"
  category   = "regular"
  help       = "Enable output tag."
  help_mode  = "Output tags."
[[option.mode.NONE]]
  name = "none"
[[option.mode.INST]]
  name = "inst"
  help = "print instantiations during solving"
  description = "With ``-o inst``, cvc5 prints information about quantifier instantions for individual quantifers."
  example-file = "regress1/quantifiers/qid-debug-inst.smt2"
[[option.mode.SYGUS]]
  name = "sygus"
  help = "print enumerated terms and candidates generated by the sygus solver"
  description = "With ``-o sygus``, cvc5 prints information about the internal SyGuS solver including enumerated terms and generated candidates."
  example-file = "regress0/sygus/print-debug.sy"
[[option.mode.SYGUS_GRAMMAR]]
  name = "sygus-grammar"
  help = "print grammars automatically generated by the sygus solver"
  description = "With ``-o sygus-grammar``, cvc5 prints the grammar it generates for a function-to-synthesize when no grammar was provided."
  example-file = "regress0/sygus/print-grammar.sy"
[[option.mode.TRIGGER]]
  name = "trigger"
  help = "print selected triggers for quantified formulas"
  description = "With ``-o trigger``, cvc5 prints the selected triggers when solving a quantified formula."
  example-file = "regress1/quantifiers/qid-debug-inst.smt2"
[[option.mode.RAW_BENCHMARK]]
  name = "raw-benchmark"
  help = "print the benchmark back on the output verbatim as it is processed"
  description = "With ``-o raw_benchmark``, cvc5 prints the benchmark back just as it has been parsed."
  example-file = "regress0/datatypes/datatype-dump.cvc.smt2"

# Stores then enabled output tags.
[[option]]
  name       = "outputTagHolder"
  category   = "undocumented"
  includes   = ["<bitset>"]
  type       = "std::bitset<static_cast<size_t>(OutputTag::__MAX_VALUE)+1>"

[[option]]
  name       = "printSuccess"
  category   = "regular"
  long       = "print-success"
  type       = "bool"
  predicates = ["setPrintSuccess"]
  help       = "print the \"success\" output required of SMT-LIBv2"

[[option]]
  name       = "cumulativeMillisecondLimit"
  category   = "common"
  long       = "tlimit=MS"
  type       = "uint64_t"
  help       = "set time limit in milliseconds of wall clock time"

[[option]]
  name       = "perCallMillisecondLimit"
  category   = "common"
  long       = "tlimit-per=MS"
  type       = "uint64_t"
  help       = "set time limit per query in milliseconds"

[[option]]
  name       = "cumulativeResourceLimit"
  category   = "common"
  long       = "rlimit=N"
  type       = "uint64_t"
  help       = "set resource limit"

[[option]]
  name       = "perCallResourceLimit"
  alias      = ["reproducible-resource-limit"]
  category   = "common"
  long       = "rlimit-per=N"
  type       = "uint64_t"
  help       = "set resource limit per query"

# --rweight is used to override the default of one particular resource weight.
# It can be given multiple times to override multiple weights. When options are
# parsed, the resource manager might now be created yet, and it is not clear
# how an option handler would access it in a reasonable way. The option handler
# thus merely puts the data in another option that holds a vector of strings.
# This other option "resourceWeightHolder" has the sole purpose of storing
# this data in a way so that the resource manager can access it in its
# constructor.
[[option]]
  category   = "expert"
  long       = "rweight=VAL=N"
  type       = "std::string"
  handler    = "setResourceWeight"
  help       = "set a single resource weight"

[[option]]
  name       = "resourceWeightHolder"
  category   = "undocumented"
  type       = "std::vector<std::string>"