diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-24 15:12:26 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-24 15:12:26 +0200 |
| commit | 821681f181ef9cdced728ba585bec83b3fab16c0 (patch) | |
| tree | 17363d145f5316c1535d60a76aa83ed055575f4b /src/theory/quantifiers/modes.h | |
| parent | c6436566dec99c0ed6794fa34b9b67a7e47918b0 (diff) | |
Add --user-pat=resort. Minor cleanup of options.
Diffstat (limited to 'src/theory/quantifiers/modes.h')
| -rw-r--r-- | src/theory/quantifiers/modes.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 53842b373..acc883f2a 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -103,6 +103,8 @@ typedef enum { USER_PAT_MODE_USE, /** default, if patterns are supplied for a quantifier, use only those */ USER_PAT_MODE_TRUST, + /** resort to user patterns only when necessary */ + USER_PAT_MODE_RESORT, /** ignore user patterns */ USER_PAT_MODE_IGNORE, } UserPatMode; |