diff options
Diffstat (limited to 'src/options/quantifiers_modes.h')
| -rw-r--r-- | src/options/quantifiers_modes.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 42ab7bc06..392393a91 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -266,8 +266,10 @@ enum SygusActiveGenMode { /** do not use actively-generated enumerators */ SYGUS_ACTIVE_GEN_NONE, - /** use basic actively-generated enumerators */ - SYGUS_ACTIVE_GEN_BASIC, + /** use basic enumeration for actively-generated enumerators */ + SYGUS_ACTIVE_GEN_ENUM_BASIC, + /** use optimized enumeration actively-generated enumerators */ + SYGUS_ACTIVE_GEN_ENUM, /** use variable-agnostic enumerators */ SYGUS_ACTIVE_GEN_VAR_AGNOSTIC, }; |