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

[[option]]
  name       = "theoryOfMode"
  smt_name   = "theoryof-mode"
  category   = "expert"
  long       = "theoryof-mode=MODE"
  type       = "TheoryOfMode"
  default    = "THEORY_OF_TYPE_BASED"
  help       = "mode for Theory::theoryof()"
  help_mode  = "Defines how we associate theories with terms."
[[option.mode.THEORY_OF_TYPE_BASED]]
  name = "type"
  help = "Type variables, constants and equalities by type."
[[option.mode.THEORY_OF_TERM_BASED]]
  name = "term"
  help = "Type variables as uninterpreted, type constants by theory, equalities by the parametric theory."

[[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"