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 cvc4 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       = "dtBinarySplit"
  27   category   = "regular"
  28   long       = "dt-binary-split"
  29   type       = "bool"
  30   default    = "false"
  31   read_only  = true
  32   help       = "do binary splits for datatype constructor types"
  33
  34 [[option]]
  35   name       = "dtRefIntro"
  36   category   = "regular"
  37   long       = "dt-ref-sk-intro"
  38   type       = "bool"
  39   default    = "false"
  40   read_only  = true
  41   help       = "introduce reference skolems for shorter explanations"
  42
  43 [[option]]
  44   name       = "cdtBisimilar"
  45   category   = "regular"
  46   long       = "cdt-bisimilar"
  47   type       = "bool"
  48   default    = "true"
  49   read_only  = true
  50   help       = "do bisimilarity check for co-datatypes"
  51
  52 [[option]]
  53   name       = "dtCyclic"
  54   category   = "regular"
  55   long       = "dt-cyclic"
  56   type       = "bool"
  57   default    = "true"
  58   read_only  = true
  59   help       = "do cyclicity check for datatypes"
  60
  61 [[option]]
  62   name       = "dtInferAsLemmas"
  63   category   = "regular"
  64   long       = "dt-infer-as-lemmas"
  65   type       = "bool"
  66   default    = "false"
  67   read_only  = true
  68   help       = "always send lemmas out instead of making internal inferences"
  69
  70 [[option]]
  71   name       = "dtBlastSplits"
  72   category   = "regular"
  73   long       = "dt-blast-splits"
  74   type       = "bool"
  75   default    = "false"
  76   read_only  = true
  77   help       = "when applicable, blast splitting lemmas for all variables at once"
  78
  79 [[option]]
  80   name       = "dtSharedSelectors"
  81   category   = "regular"
  82   long       = "dt-share-sel"
  83   type       = "bool"
  84   default    = "true"
  85   read_only  = true
  86   help       = "internally use shared selectors across multiple constructors"
  87
  88 [[option]]
  89   name       = "sygusSymBreak"
  90   category   = "regular"
  91   long       = "sygus-sym-break"
  92   type       = "bool"
  93   default    = "true"
  94   read_only  = true
  95   help       = "simple sygus symmetry breaking lemmas"
  96
  97 [[option]]
  98   name       = "sygusSymBreakAgg"
  99   category   = "regular"
 100   long       = "sygus-sym-break-agg"
 101   type       = "bool"
 102   default    = "true"
 103   read_only  = 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   read_only  = true
 113   help       = "dynamic sygus symmetry breaking lemmas"
 114
 115 [[option]]
 116   name       = "sygusSymBreakPbe"
 117   category   = "regular"
 118   long       = "sygus-sym-break-pbe"
 119   type       = "bool"
 120   default    = "true"
 121   help       = "sygus symmetry breaking lemmas based on pbe conjectures"
 122
 123 [[option]]
 124   name       = "sygusSymBreakLazy"
 125   category   = "regular"
 126   long       = "sygus-sym-break-lazy"
 127   type       = "bool"
 128   default    = "true"
 129   read_only  = true
 130   help       = "lazily add symmetry breaking lemmas for terms"
 131
 132 [[option]]
 133   name       = "sygusSymBreakRlv"
 134   category   = "regular"
 135   long       = "sygus-sym-break-rlv"
 136   type       = "bool"
 137   default    = "true"
 138   read_only  = true
 139   help       = "add relevancy conditions to symmetry breaking lemmas"
 140
 141 [[option]]
 142   name       = "sygusFair"
 143   category   = "regular"
 144   long       = "sygus-fair=MODE"
 145   type       = "SygusFairMode"
 146   default    = "DT_SIZE"
 147   read_only  = true
 148   help       = "if and how to apply fairness for sygus"
 149   help_mode  = "Modes for enforcing fairness for counterexample guided quantifier instantion."
 150 [[option.mode.DIRECT]]
 151   name = "direct"
 152   help = "Enforce fairness using direct conflict lemmas."
 153 [[option.mode.DT_SIZE]]
 154   name = "dt-size"
 155   help = "Enforce fairness using size operator."
 156 [[option.mode.DT_HEIGHT_PRED]]
 157   name = "dt-height-bound"
 158   help = "Enforce fairness by height bound predicate."
 159 [[option.mode.DT_SIZE_PRED]]
 160   name = "dt-size-bound"
 161   help = "Enforce fairness by size bound predicate."
 162 [[option.mode.NONE]]
 163   name = "none"
 164   help = "Do not enforce fairness."
 165
 166 [[option]]
 167   name       = "sygusFairMax"
 168   category   = "regular"
 169   long       = "sygus-fair-max"
 170   type       = "bool"
 171   default    = "true"
 172   read_only  = true
 173   help       = "use max instead of sum for multi-function sygus conjectures"
 174
 175 [[option]]
 176   name       = "sygusAbortSize"
 177   category   = "regular"
 178   long       = "sygus-abort-size=N"
 179   type       = "int"
 180   default    = "-1"
 181   read_only  = true
 182   help       = "tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)"