diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-12-17 13:43:44 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-12-17 13:43:44 -0800 |
| commit | e9499c41f405df8b42fd9ae10004b1b91a869106 (patch) | |
| tree | fa1475f43a3e61b8f6ffdcb903b65919eba28661 /src/options/strings_options.toml | |
| parent | 9b2914ed9f7b14ecf535ffe9e1328d0fa042e072 (diff) | |
Generate code for options with modes. (#3561)
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
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." |