diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-26 13:39:06 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-26 13:39:06 -0600 |
commit | 135f99f365920097ce48be87cb77fb1144d446a3 (patch) | |
tree | 9a83a6c90aafca0de217a1fee3fd943199926ee2 /src/options/strings_options | |
parent | a1135ca591276f6d02b3632bc77a3934ded2d2af (diff) |
Refactoring of inferences in strings. Add several options.
Diffstat (limited to 'src/options/strings_options')
-rw-r--r-- | src/options/strings_options | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/options/strings_options b/src/options/strings_options index 1b64af83f..dee379878 100644 --- a/src/options/strings_options +++ b/src/options/strings_options @@ -55,6 +55,14 @@ option stringEagerLen strings-eager-len --strings-eager-len bool :default true strings eager length lemmas option stringCheckEntailLen strings-check-entail-len --strings-check-entail-len bool :default true check entailment between length terms to reduce splitting +option stringProcessLoop strings-process-loop --strings-process-loop bool :default true + reduce looping word equations to regular expressions +option stringAbortLoop strings-abort-loop --strings-abort-loop bool :default false + abort when a looping word equation is encountered +option stringInferAsLemmas strings-infer-as-lemmas --strings-infer-as-lemmas bool :default false + always send lemmas out instead of making internal inferences +option stringRExplainLemmas strings-rexplain-lemmas --strings-rexplain-lemmas bool :default true + regression explanations for string lemmas endmodule |