diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-13 12:17:46 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-13 12:17:46 +0100 |
| commit | 52514cada7c0c7c4fff69c85e0bd735abfdc03fd (patch) | |
| tree | 401b5ab2efae7a0d3971d07d01ff61b0ab18fbcd /src/theory/quantifiers/modes.h | |
| parent | 0e761324a33a993ae9a268bc2d2ed46f7e86b42d (diff) | |
Remove two obsolete versions of MBQI.
Diffstat (limited to 'src/theory/quantifiers/modes.h')
| -rw-r--r-- | src/theory/quantifiers/modes.h | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index acc883f2a..80dbb783e 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -62,14 +62,10 @@ typedef enum { MBQI_GEN_EVAL, /** no mbqi */ MBQI_NONE, - /** implementation that mimics inst-gen */ - MBQI_INST_GEN, /** default, mbqi from Section 5.4.2 of AJR thesis */ MBQI_FMC, /** mbqi with integer intervals */ MBQI_FMC_INTERVAL, - /** mbqi with interval abstraction of uninterpreted sorts */ - MBQI_INTERVAL, /** abstract mbqi algorithm */ MBQI_ABS, /** mbqi trust (produce no instantiations) */ |