id     = "DATATYPES"
name   = "Datatypes theory"
header = "options/datatypes_options.h"

# How to handle selectors applied to incorrect constructors.  If this option is set,
# then we do not rewrite such a selector term to an arbitrary ground term.  
# For example, by default cvc5 considers cdr( nil ) = nil.  If this option is set, then
# cdr( nil ) has no set value.
[[option]]
  name       = "dtRewriteErrorSel"
  category   = "expert"
  long       = "dt-rewrite-error-sel"
  type       = "bool"
  default    = "false"
  help       = "rewrite incorrectly applied selectors to arbitrary ground term"

[[option]]
  name       = "dtForceAssignment"
  category   = "regular"
  long       = "dt-force-assignment"
  type       = "bool"
  default    = "false"
  help       = "force the datatypes solver to give specific values to all datatypes terms before answering sat"

[[option]]
  name       = "dtPoliteOptimize"
  smt_name   = "dt-polite-optimize"
  category   = "experimental"
  long       = "dt-polite-optimize"
  type       = "bool"
  default    = "true"
  help       = "turn on optimization for polite combination"

[[option]]
  name       = "dtBinarySplit"
  category   = "regular"
  long       = "dt-binary-split"
  type       = "bool"
  default    = "false"
  help       = "do binary splits for datatype constructor types"

[[option]]
  name       = "cdtBisimilar"
  category   = "regular"
  long       = "cdt-bisimilar"
  type       = "bool"
  default    = "true"
  help       = "do bisimilarity check for co-datatypes"

[[option]]
  name       = "dtCyclic"
  category   = "regular"
  long       = "dt-cyclic"
  type       = "bool"
  default    = "true"
  help       = "do cyclicity check for datatypes"

[[option]]
  name       = "dtInferAsLemmas"
  category   = "regular"
  long       = "dt-infer-as-lemmas"
  type       = "bool"
  default    = "false"
  help       = "always send lemmas out instead of making internal inferences"

[[option]]
  name       = "dtBlastSplits"
  category   = "regular"
  long       = "dt-blast-splits"
  type       = "bool"
  default    = "false"
  help       = "when applicable, blast splitting lemmas for all variables at once"

[[option]]
  name       = "dtNestedRec"
  category   = "regular"
  long       = "dt-nested-rec"
  type       = "bool"
  default    = "false"
  help       = "allow nested recursion in datatype definitions"

[[option]]
  name       = "dtSharedSelectors"
  category   = "regular"
  long       = "dt-share-sel"
  type       = "bool"
  default    = "true"
  help       = "internally use shared selectors across multiple constructors"

[[option]]
  name       = "sygusSymBreak"
  category   = "regular"
  long       = "sygus-sym-break"
  type       = "bool"
  default    = "true"
  help       = "simple sygus symmetry breaking lemmas"

[[option]]
  name       = "sygusSymBreakAgg"
  category   = "regular"
  long       = "sygus-sym-break-agg"
  type       = "bool"
  default    = "true"
  help       = "use aggressive checks for simple sygus symmetry breaking lemmas"

[[option]]
  name       = "sygusSymBreakDynamic"
  category   = "regular"
  long       = "sygus-sym-break-dynamic"
  type       = "bool"
  default    = "true"
  help       = "dynamic sygus symmetry breaking lemmas"

[[option]]
  name       = "sygusSymBreakPbe"
  category   = "regular"
  long       = "sygus-sym-break-pbe"
  type       = "bool"
  default    = "true"
  help       = "sygus symmetry breaking lemmas based on pbe conjectures"

[[option]]
  name       = "sygusSymBreakLazy"
  category   = "regular"
  long       = "sygus-sym-break-lazy"
  type       = "bool"
  default    = "true"
  help       = "lazily add symmetry breaking lemmas for terms"

[[option]]
  name       = "sygusSymBreakRlv"
  category   = "regular"
  long       = "sygus-sym-break-rlv"
  type       = "bool"
  default    = "true"
  help       = "add relevancy conditions to symmetry breaking lemmas"

[[option]]
  name       = "sygusFair"
  category   = "regular"
  long       = "sygus-fair=MODE"
  type       = "SygusFairMode"
  default    = "DT_SIZE"
  help       = "if and how to apply fairness for sygus"
  help_mode  = "Modes for enforcing fairness for counterexample guided quantifier instantion."
[[option.mode.DIRECT]]
  name = "direct"
  help = "Enforce fairness using direct conflict lemmas."
[[option.mode.DT_SIZE]]
  name = "dt-size"
  help = "Enforce fairness using size operator."
[[option.mode.DT_HEIGHT_PRED]]
  name = "dt-height-bound"
  help = "Enforce fairness by height bound predicate."
[[option.mode.DT_SIZE_PRED]]
  name = "dt-size-bound"
  help = "Enforce fairness by size bound predicate."
[[option.mode.NONE]]
  name = "none"
  help = "Do not enforce fairness."

[[option]]
  name       = "sygusFairMax"
  category   = "regular"
  long       = "sygus-fair-max"
  type       = "bool"
  default    = "true"
  help       = "use max instead of sum for multi-function sygus conjectures"

[[option]]
  name       = "sygusAbortSize"
  category   = "regular"
  long       = "sygus-abort-size=N"
  type       = "int"
  default    = "-1"
  help       = "tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)"