src/options/arrays_options.toml

   1 id     = "ARRAYS"
   2 name   = "Arrays theory"
   3 header = "options/arrays_options.h"
   4
   5 [[option]]
   6   name       = "arraysOptimizeLinear"
   7   category   = "regular"
   8   long       = "arrays-optimize-linear"
   9   type       = "bool"
  10   default    = "true"
  11   help       = "turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper)"
  12
  13 [[option]]
  14   name       = "arraysLazyRIntro1"
  15   category   = "regular"
  16   long       = "arrays-lazy-rintro1"
  17   type       = "bool"
  18   default    = "true"
  19   help       = "turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination)"
  20
  21 [[option]]
  22   name       = "arraysWeakEquivalence"
  23   category   = "regular"
  24   long       = "arrays-weak-equiv"
  25   type       = "bool"
  26   default    = "false"
  27   help       = "use algorithm from Christ/Hoenicke (SMT 2014)"
  28
  29 [[option]]
  30   name       = "arraysModelBased"
  31   category   = "regular"
  32   long       = "arrays-model-based"
  33   type       = "bool"
  34   default    = "false"
  35   help       = "turn on model-based array solver"
  36
  37 [[option]]
  38   name       = "arraysEagerIndexSplitting"
  39   category   = "regular"
  40   long       = "arrays-eager-index"
  41   type       = "bool"
  42   default    = "true"
  43   help       = "turn on eager index splitting for generated array lemmas"
  44
  45 [[option]]
  46   name       = "arraysEagerLemmas"
  47   category   = "regular"
  48   long       = "arrays-eager-lemmas"
  49   type       = "bool"
  50   default    = "false"
  51   help       = "turn on eager lemma generation for arrays"
  52
  53 [[option]]
  54   name       = "arraysConfig"
  55   category   = "regular"
  56   long       = "arrays-config=N"
  57   type       = "int"
  58   default    = "0"
  59   help       = "set different array option configurations - for developers only"
  60
  61 [[option]]
  62   name       = "arraysReduceSharing"
  63   category   = "regular"
  64   long       = "arrays-reduce-sharing"
  65   type       = "bool"
  66   default    = "false"
  67   help       = "use model information to reduce size of care graph for arrays"
  68
  69 [[option]]
  70   name       = "arraysPropagate"
  71   category   = "regular"
  72   long       = "arrays-prop=N"
  73   type       = "int"
  74   default    = "2"
  75   help       = "propagation effort for arrays: 0 is none, 1 is some, 2 is full"
  76
  77 [[option]]
  78   name       = "arraysExp"
  79   category   = "experimental"
  80   long       = "arrays-exp"
  81   type       = "bool"
  82   default    = "false"
  83   help       = "enable experimental features in the theory of arrays"
  84