diff options
Diffstat (limited to 'src/options/strings_options.toml')
-rw-r--r-- | src/options/strings_options.toml | 42 |
1 files changed, 34 insertions, 8 deletions
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 2d8411256..3916c68f3 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -132,11 +132,26 @@ header = "options/strings_options.h" name = "stringProcessLoopMode" category = "expert" long = "strings-process-loop-mode=MODE" - type = "CVC4::theory::strings::ProcessLoopMode" - default = "CVC4::theory::strings::ProcessLoopMode::FULL" - handler = "stringToStringsProcessLoopMode" - includes = ["options/strings_modes.h"] + 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" @@ -221,8 +236,19 @@ header = "options/strings_options.h" 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"] + 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." |