diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-12 15:48:11 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-12 15:48:11 -0500 |
| commit | ca1b17c8bba3681643a1a3de19d32b038c38aceb (patch) | |
| tree | ff02dc2314a3c1e86d19ca9bc2bbe8a57ef1856b /src/options/quantifiers_modes.h | |
| parent | 685b1f3769decafbff1c5b929d4ce01169ff9d81 (diff) | |
Refactor prenex modes.
Diffstat (limited to 'src/options/quantifiers_modes.h')
| -rw-r--r-- | src/options/quantifiers_modes.h | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index fe76f8798..cc6abaa8b 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -123,12 +123,14 @@ enum TriggerActiveSelMode { }; enum CVC4_PUBLIC PrenexQuantMode { - /** default : prenex quantifiers without user patterns */ - PRENEX_NO_USER_PAT, - /** prenex all */ - PRENEX_ALL, - /** prenex none */ - PRENEX_NONE, + /** do not prenex */ + PRENEX_QUANT_NONE, + /** prenex same sign quantifiers */ + PRENEX_QUANT_SIMPLE, + /** aggressive prenex, disjunctive prenex normal form */ + PRENEX_QUANT_DISJ_NORMAL, + /** prenex normal form */ + PRENEX_QUANT_NORMAL, }; enum CegqiFairMode { |