id     = "THEORY"
name   = "Theory layer"
header = "options/theory_options.h"

[[option]]
  name       = "theoryOfMode"
  smt_name   = "theoryof-mode"
  category   = "expert"
  long       = "theoryof-mode=MODE"
  type       = "CVC4::theory::TheoryOfMode"
  default    = "CVC4::theory::THEORY_OF_TYPE_BASED"
  handler    = "stringToTheoryOfMode"
  includes   = ["options/theoryof_mode.h"]
  help       = "mode for Theory::theoryof()"

[[option]]
  name       = "useTheoryList"
  smt_name   = "use-theory"
  category   = "regular"
  long       = "use-theory=NAME"
  type       = "std::string"
  handler    = "handleUseTheoryList"
  notifies   = ["notifyUseTheoryList"]
  read_only  = true
  help       = "use alternate theory implementation NAME (--use-theory=help for a list). This option may be repeated or a comma separated list."

[[option]]
  name       = "assignFunctionValues"
  category   = "regular"
  long       = "assign-function-values"
  type       = "bool"
  default    = "true"
  help       = "assign values for uninterpreted functions in models"

[[option]]
  name       = "condenseFunctionValues"
  category   = "regular"
  long       = "condense-function-values"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "condense values for functions in models rather than explicitly representing them"