diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-05 16:50:48 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-11-05 16:50:48 -0600 |
| commit | 2ef5f132c1169cbeadd580638cbc35b6e454d6a5 (patch) | |
| tree | e52fe812aafe511293e345c494f4a389eec0f855 /src/options/quantifiers_modes.h | |
| parent | cc5ea0ed533e081ecccca57cf1c4efb63296f995 (diff) | |
Change default sygus enumeration mode to auto (#2689)
Diffstat (limited to 'src/options/quantifiers_modes.h')
| -rw-r--r-- | src/options/quantifiers_modes.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 392393a91..05388cdf6 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -272,6 +272,8 @@ enum SygusActiveGenMode SYGUS_ACTIVE_GEN_ENUM, /** use variable-agnostic enumerators */ SYGUS_ACTIVE_GEN_VAR_AGNOSTIC, + /** internally decide the best policy for each enumerator */ + SYGUS_ACTIVE_GEN_AUTO, }; enum MacrosQuantMode { |