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