diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-17 12:07:00 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-17 17:07:00 +0000 |
| commit | cf5376c18d8e4d6b3ed2d7b341279cf65fc16418 (patch) | |
| tree | afbfb5162c6ccc3111827f4080b968108be83152 /src/options | |
| parent | d39e1b906b47ef8e953dac297fa0fb565dd040a4 (diff) | |
Fix policy for eliminating quantified formulas (#7017)
This also consolidates the option strictTriggers into userPatMode.
Fixes #6996.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options.toml | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 58632aafc..ad74e4ab9 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -227,14 +227,6 @@ name = "Quantifiers" help = "consider ground terms within bodies of quantified formulas for matching" [[option]] - name = "strictTriggers" - category = "regular" - long = "strict-triggers" - type = "bool" - default = "false" - help = "only instantiate quantifiers with user patterns based on triggers" - -[[option]] name = "relevantTriggers" category = "regular" long = "relevant-triggers" @@ -388,6 +380,9 @@ name = "Quantifiers" [[option.mode.TRUST]] name = "trust" help = "When provided, use only user-provided patterns for a quantified formula." +[[option.mode.STRICT]] + name = "trust" + help = "When provided, use only user-provided patterns for a quantified formula, and do not use any other instantiation techniques." [[option.mode.RESORT]] name = "resort" help = "Use user-provided patterns only after auto-generated patterns saturate." |