id     = "BASE"
name   = "Base"

[[option]]
  name       = "binary_name"
  category   = "undocumented"
  type       = "std::string"

[[option]]
  name       = "in"
  category   = "undocumented"
  type       = "std::istream*"
  default    = "&std::cin"
  includes   = ["<iosfwd>"]

[[option]]
  name       = "out"
  category   = "undocumented"
  type       = "std::ostream*"
  default    = "&std::cout"
  includes   = ["<iosfwd>"]

[[option]]
  name       = "err"
  category   = "undocumented"
  type       = "std::ostream*"
  default    = "&std::cerr"
  includes   = ["<iosfwd>"]

[[option]]
  name       = "inputLanguage"
  alias      = ["input-language"]
  category   = "common"
  short      = "L"
  long       = "lang=LANG"
  type       = "InputLanguage"
  default    = "language::input::LANG_AUTO"
  handler    = "stringToInputLanguage"
  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       = "OutputLanguage"
  default    = "language::output::LANG_AUTO"
  handler    = "stringToOutputLanguage"
  includes   = ["options/language.h"]
  help       = "force output language (default is \"auto\"; see --output-lang help)"

[[option]]
  name       = "languageHelp"
  category   = "undocumented"
  type       = "bool"

[[option]]
  name       = "verbosity"
  long       = "verbosity=N"
  category   = "regular"
  type       = "int"
  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       = "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 = ["setStats"]
  help       = "print unchanged (defaulted) statistics as well"

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

[[option]]
  name       = "statisticsEveryQuery"
  long       = "stats-every-query"
  category   = "regular"
  type       = "bool"
  predicates = ["setStats"]
  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       = "printSuccess"
  category   = "regular"
  long       = "print-success"
  type       = "bool"
  help       = "print the \"success\" output required of SMT-LIBv2"