1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207
|
id = "STRINGS"
name = "Strings theory"
header = "options/strings_options.h"
[[option]]
name = "stringExp"
category = "regular"
long = "strings-exp"
type = "bool"
default = "false"
help = "experimental features in the theory of strings"
[[option]]
name = "stdPrintASCII"
category = "regular"
long = "strings-print-ascii"
type = "bool"
default = "false"
read_only = true
help = "the alphabet contains only printable characters from the standard extended ASCII"
[[option]]
name = "stringFMF"
category = "regular"
long = "strings-fmf"
type = "bool"
default = "false"
help = "the finite model finding used by the theory of strings"
[[option]]
name = "stringEager"
category = "regular"
long = "strings-eager"
type = "bool"
default = "false"
read_only = true
help = "strings eager check"
[[option]]
name = "stringIgnNegMembership"
category = "regular"
long = "strings-inm"
type = "bool"
default = "false"
read_only = true
help = "internal for strings: ignore negative membership constraints (fragment checking is needed, left to users for now)"
[[option]]
name = "stringLazyPreproc"
category = "regular"
long = "strings-lazy-pp"
type = "bool"
default = "true"
read_only = true
help = "perform string preprocessing lazily"
[[option]]
name = "stringLenNorm"
category = "regular"
long = "strings-len-norm"
type = "bool"
default = "true"
read_only = true
help = "strings length normalization lemma"
[[option]]
name = "stringInferSym"
category = "regular"
long = "strings-infer-sym"
type = "bool"
default = "true"
read_only = true
help = "strings split on empty string"
[[option]]
name = "stringEagerLen"
category = "regular"
long = "strings-eager-len"
type = "bool"
default = "true"
read_only = true
help = "strings eager length lemmas"
[[option]]
name = "stringCheckEntailLen"
category = "regular"
long = "strings-check-entail-len"
type = "bool"
default = "true"
read_only = true
help = "check entailment between length terms to reduce splitting"
[[option]]
name = "stringProcessLoopMode"
category = "expert"
long = "strings-process-loop-mode=MODE"
type = "ProcessLoopMode"
default = "FULL"
help = "determines how to process looping string equations"
help_mode = "Loop processing modes."
[[option.mode.FULL]]
name = "full"
help = "Perform full processing of looping word equations."
[[option.mode.SIMPLE]]
name = "simple"
help = "Omit normal loop breaking (default with --strings-fmf)."
[[option.mode.SIMPLE_ABORT]]
name = "simple-abort"
help = "Abort when normal loop breaking is required."
[[option.mode.NONE]]
name = "none"
help = "Omit loop processing."
[[option.mode.ABORT]]
name = "abort"
help = "Abort if looping word equations are encountered."
[[option]]
name = "stringInferAsLemmas"
category = "regular"
long = "strings-infer-as-lemmas"
type = "bool"
default = "false"
read_only = true
help = "always send lemmas out instead of making internal inferences"
[[option]]
name = "stringRExplainLemmas"
category = "regular"
long = "strings-rexplain-lemmas"
type = "bool"
default = "true"
read_only = true
help = "regression explanations for string lemmas"
[[option]]
name = "stringMinPrefixExplain"
category = "regular"
long = "strings-min-prefix-explain"
type = "bool"
default = "true"
read_only = true
help = "minimize explanations for prefix of normal forms in strings"
[[option]]
name = "stringGuessModel"
category = "regular"
long = "strings-guess-model"
type = "bool"
default = "false"
read_only = true
help = "use model guessing to avoid string extended function reductions"
[[option]]
name = "stringLenPropCsp"
category = "regular"
long = "strings-lprop-csp"
type = "bool"
default = "false"
read_only = true
help = "do length propagation based on constant splits"
[[option]]
name = "regExpElim"
category = "regular"
long = "re-elim"
type = "bool"
default = "false"
help = "elimination techniques for regular expressions"
[[option]]
name = "regExpElimAgg"
category = "regular"
long = "re-elim-agg"
type = "bool"
default = "false"
help = "aggressive elimination techniques for regular expressions"
[[option]]
name = "stringFlatForms"
category = "regular"
long = "strings-ff"
type = "bool"
default = "true"
read_only = true
help = "do flat form inferences"
[[option]]
name = "stringRegExpInterMode"
category = "expert"
long = "re-inter-mode=MODE"
type = "RegExpInterMode"
default = "CONSTANT"
help = "determines which regular expressions intersections to compute"
help_mode = "Regular expression intersection modes."
[[option.mode.ALL]]
name = "all"
help = "Compute intersections for all regular expressions."
[[option.mode.CONSTANT]]
name = "constant"
help = "Compute intersections only between regular expressions that do not contain re.allchar or re.range."
[[option.mode.ONE_CONSTANT]]
name = "one-constant"
help = "Compute intersections only between regular expressions such that at least one side does not contain re.allchar or re.range."
[[option.mode.NONE]]
name = "none"
help = "Do not compute intersections for regular expressions."
|