id     = "THEORY"
name   = "Theory Layer"

[[option]]
  name       = "theoryOfMode"
  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"
  help       = "condense values for functions in models rather than explicitly representing them"

[[option]]
  name       = "relevanceFilter"
  category   = "regular"
  long       = "relevance-filter"
  type       = "bool"
  default    = "false"
  help       = "enable analysis of relevance of asserted literals with respect to the input formula"

[[option]]
  name       = "eeMode"
  category   = "expert"
  long       = "ee-mode=MODE"
  type       = "EqEngineMode"
  default    = "DISTRIBUTED"
  help       = "mode for managing equalities across theory solvers"
  help_mode  = "Defines mode for managing equalities across theory solvers."
[[option.mode.DISTRIBUTED]]
  name = "distributed"
  help = "Each theory maintains its own equality engine."
[[option.mode.CENTRAL]]
  name = "central"
  help = "All applicable theories use the central equality engine."

[[option]]
  name       = "tcMode"
  category   = "expert"
  long       = "tc-mode=MODE"
  type       = "TcMode"
  default    = "CARE_GRAPH"
  help       = "mode for theory combination"
  help_mode  = "Defines mode for theory combination."
[[option.mode.CARE_GRAPH]]
  name = "care-graph"
  help = "Use care graphs for theory combination."