3 header = "options/arrays_options.h"
6 name = "arraysOptimizeLinear"
8 long = "arrays-optimize-linear"
11 help = "turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper)"
14 name = "arraysLazyRIntro1"
16 long = "arrays-lazy-rintro1"
19 help = "turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination)"
22 name = "arraysWeakEquivalence"
24 long = "arrays-weak-equiv"
27 help = "use algorithm from Christ/Hoenicke (SMT 2014)"
30 name = "arraysModelBased"
32 long = "arrays-model-based"
35 help = "turn on model-based array solver"
38 name = "arraysEagerIndexSplitting"
40 long = "arrays-eager-index"
43 help = "turn on eager index splitting for generated array lemmas"
46 name = "arraysEagerLemmas"
48 long = "arrays-eager-lemmas"
51 help = "turn on eager lemma generation for arrays"
56 long = "arrays-config=N"
59 help = "set different array option configurations - for developers only"
62 name = "arraysReduceSharing"
64 long = "arrays-reduce-sharing"
67 help = "use model information to reduce size of care graph for arrays"
70 name = "arraysPropagate"
72 long = "arrays-prop=N"
75 help = "propagation effort for arrays: 0 is none, 1 is some, 2 is full"
79 category = "experimental"
83 help = "enable experimental features in the theory of arrays"