diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-01 09:08:46 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-01 09:08:46 -0500 |
| commit | 79881c196e29ef341166e7a31c1183e8b537d069 (patch) | |
| tree | 25466cceb67c54895bf012fd745dd864d356b153 /src/options/strings_options.toml | |
| parent | 7537ff075dbb2d814d722d2d72586ce78235467c (diff) | |
Regular expression intersection modes (#3134)
Diffstat (limited to 'src/options/strings_options.toml')
| -rw-r--r-- | src/options/strings_options.toml | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index fd00b8917..2d8411256 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -135,8 +135,8 @@ header = "options/strings_options.h" type = "CVC4::theory::strings::ProcessLoopMode" default = "CVC4::theory::strings::ProcessLoopMode::FULL" handler = "stringToStringsProcessLoopMode" - includes = ["options/strings_process_loop_mode.h"] - help = "choose how to process looping string equations, see --strings-process-loop-mode=help for details" + includes = ["options/strings_modes.h"] + help = "determines how to process looping string equations" [[option]] name = "stringInferAsLemmas" @@ -216,3 +216,13 @@ header = "options/strings_options.h" default = "true" read_only = true help = "do flat form inferences" + +[[option]] + name = "stringRegExpInterMode" + category = "expert" + long = "re-inter-mode=MODE" + type = "CVC4::theory::strings::RegExpInterMode" + default = "CVC4::theory::strings::RE_INTER_CONSTANT" + handler = "stringToRegExpInterMode" + includes = ["options/strings_modes.h"] + help = "determines which regular expressions intersections to compute" |