summaryrefslogtreecommitdiff
path: root/src/options/quantifiers_modes.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/quantifiers_modes.h')
-rw-r--r--src/options/quantifiers_modes.h14
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 {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback