diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-15 10:28:47 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-15 10:28:47 -0800 |
| commit | 4a38be3b9ac133655602a989f1136cd24ed89bc6 (patch) | |
| tree | d8a03c6a78a822b658587cbd06af2e0c1e5bd50f /src/options/strings_options.toml | |
| parent | da504025a3a77e9a3201af33ee6f96f937802807 (diff) | |
Strings: Add option to change loop process mode (#2794)
This commit adds an option `--strings-process-loop-mode` that allows
finer-grained control over CVC4 processes looping word equation. In
particular, performing normal loop breaking sometimes leads to worse
performance. The "simple" mode disables that inference.
Diffstat (limited to 'src/options/strings_options.toml')
| -rw-r--r-- | src/options/strings_options.toml | 24 |
1 files changed, 8 insertions, 16 deletions
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 3544c37fe..fd00b8917 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -129,22 +129,14 @@ header = "options/strings_options.h" help = "check entailment between length terms to reduce splitting" [[option]] - name = "stringProcessLoop" - category = "regular" - long = "strings-process-loop" - type = "bool" - default = "true" - read_only = true - help = "reduce looping word equations to regular expressions" - -[[option]] - name = "stringAbortLoop" - category = "regular" - long = "strings-abort-loop" - type = "bool" - default = "false" - read_only = true - help = "abort when a looping word equation is encountered" + 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_process_loop_mode.h"] + help = "choose how to process looping string equations, see --strings-process-loop-mode=help for details" [[option]] name = "stringInferAsLemmas" |