src/options/datatypes_options.toml

   1 id     = "DATATYPES"
   2 name   = "Datatypes theory"
   3 header = "options/datatypes_options.h"
   4
   5 # How to handle selectors applied to incorrect constructors.  If this option is set,
   6 # then we do not rewrite such a selector term to an arbitrary ground term.
   7 # For example, by default cvc5 considers cdr( nil ) = nil.  If this option is set, then
   8 # cdr( nil ) has no set value.
   9 [[option]]
  10   name       = "dtRewriteErrorSel"
  11   category   = "expert"
  12   long       = "dt-rewrite-error-sel"
  13   type       = "bool"
  14   default    = "false"
  15   help       = "rewrite incorrectly applied selectors to arbitrary ground term"
  16
  17 [[option]]
  18   name       = "dtForceAssignment"
  19   category   = "regular"
  20   long       = "dt-force-assignment"
  21   type       = "bool"
  22   default    = "false"
  23   help       = "force the datatypes solver to give specific values to all datatypes terms before answering sat"
  24
  25 [[option]]
  26   name       = "dtPoliteOptimize"
  27   smt_name   = "dt-polite-optimize"
  28   category   = "experimental"
  29   long       = "dt-polite-optimize"
  30   type       = "bool"
  31   default    = "true"
  32   help       = "turn on optimization for polite combination"
  33
  34 [[option]]
  35   name       = "dtBinarySplit"
  36   category   = "regular"
  37   long       = "dt-binary-split"
  38   type       = "bool"
  39   default    = "false"
  40   help       = "do binary splits for datatype constructor types"
  41
  42 [[option]]
  43   name       = "cdtBisimilar"
  44   category   = "regular"
  45   long       = "cdt-bisimilar"
  46   type       = "bool"
  47   default    = "true"
  48   help       = "do bisimilarity check for co-datatypes"
  49
  50 [[option]]
  51   name       = "dtCyclic"
  52   category   = "regular"
  53   long       = "dt-cyclic"
  54   type       = "bool"
  55   default    = "true"
  56   help       = "do cyclicity check for datatypes"
  57
  58 [[option]]
  59   name       = "dtInferAsLemmas"
  60   category   = "regular"
  61   long       = "dt-infer-as-lemmas"
  62   type       = "bool"
  63   default    = "false"
  64   help       = "always send lemmas out instead of making internal inferences"
  65
  66 [[option]]
  67   name       = "dtBlastSplits"
  68   category   = "regular"
  69   long       = "dt-blast-splits"
  70   type       = "bool"
  71   default    = "false"
  72   help       = "when applicable, blast splitting lemmas for all variables at once"
  73
  74 [[option]]
  75   name       = "dtNestedRec"
  76   category   = "regular"
  77   long       = "dt-nested-rec"
  78   type       = "bool"
  79   default    = "false"
  80   help       = "allow nested recursion in datatype definitions"
  81
  82 [[option]]
  83   name       = "dtSharedSelectors"
  84   category   = "regular"
  85   long       = "dt-share-sel"
  86   type       = "bool"
  87   default    = "true"
  88   help       = "internally use shared selectors across multiple constructors"
  89
  90 [[option]]
  91   name       = "sygusSymBreak"
  92   category   = "regular"
  93   long       = "sygus-sym-break"
  94   type       = "bool"
  95   default    = "true"
  96   help       = "simple sygus symmetry breaking lemmas"
  97
  98 [[option]]
  99   name       = "sygusSymBreakAgg"
 100   category   = "regular"
 101   long       = "sygus-sym-break-agg"
 102   type       = "bool"
 103   default    = "true"
 104   help       = "use aggressive checks for simple sygus symmetry breaking lemmas"
 105
 106 [[option]]
 107   name       = "sygusSymBreakDynamic"
 108   category   = "regular"
 109   long       = "sygus-sym-break-dynamic"
 110   type       = "bool"
 111   default    = "true"
 112   help       = "dynamic sygus symmetry breaking lemmas"
 113
 114 [[option]]
 115   name       = "sygusSymBreakPbe"
 116   category   = "regular"
 117   long       = "sygus-sym-break-pbe"
 118   type       = "bool"
 119   default    = "true"
 120   help       = "sygus symmetry breaking lemmas based on pbe conjectures"
 121
 122 [[option]]
 123   name       = "sygusSymBreakLazy"
 124   category   = "regular"
 125   long       = "sygus-sym-break-lazy"
 126   type       = "bool"
 127   default    = "true"
 128   help       = "lazily add symmetry breaking lemmas for terms"
 129
 130 [[option]]
 131   name       = "sygusSymBreakRlv"
 132   category   = "regular"
 133   long       = "sygus-sym-break-rlv"
 134   type       = "bool"
 135   default    = "true"
 136   help       = "add relevancy conditions to symmetry breaking lemmas"
 137
 138 [[option]]
 139   name       = "sygusFair"
 140   category   = "regular"
 141   long       = "sygus-fair=MODE"
 142   type       = "SygusFairMode"
 143   default    = "DT_SIZE"
 144   help       = "if and how to apply fairness for sygus"
 145   help_mode  = "Modes for enforcing fairness for counterexample guided quantifier instantion."
 146 [[option.mode.DIRECT]]
 147   name = "direct"
 148   help = "Enforce fairness using direct conflict lemmas."
 149 [[option.mode.DT_SIZE]]
 150   name = "dt-size"
 151   help = "Enforce fairness using size operator."
 152 [[option.mode.DT_HEIGHT_PRED]]
 153   name = "dt-height-bound"
 154   help = "Enforce fairness by height bound predicate."
 155 [[option.mode.DT_SIZE_PRED]]
 156   name = "dt-size-bound"
 157   help = "Enforce fairness by size bound predicate."
 158 [[option.mode.NONE]]
 159   name = "none"
 160   help = "Do not enforce fairness."
 161
 162 [[option]]
 163   name       = "sygusFairMax"
 164   category   = "regular"
 165   long       = "sygus-fair-max"
 166   type       = "bool"
 167   default    = "true"
 168   help       = "use max instead of sum for multi-function sygus conjectures"
 169
 170 [[option]]
 171   name       = "sygusAbortSize"
 172   category   = "regular"
 173   long       = "sygus-abort-size=N"
 174   type       = "int"
 175   default    = "-1"
 176   help       = "tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)"