diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-18 22:50:05 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-18 22:50:05 -0600 |
| commit | f47f24528f5d19ac0affd572f3d34c090e97f9f9 (patch) | |
| tree | 6a21c1964d862f99d9137f968881a0da33c59d1d /src/options/quantifiers_modes.h | |
| parent | 793361d81f0766c6a28ff699ed5447d9b8f8c123 (diff) | |
Implement dynamic splitting for quantified formulas. Minor refactoring of reductions in quantifiers engine.
Diffstat (limited to 'src/options/quantifiers_modes.h')
| -rw-r--r-- | src/options/quantifiers_modes.h | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 540db38ec..7395a9a30 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -163,6 +163,16 @@ enum MacrosQuantMode { MACROS_QUANT_MODE_GROUND_UF, }; +enum QuantDSplitMode { + /** never do quantifiers splitting */ + QUANT_DSPLIT_MODE_NONE, + /** default */ + QUANT_DSPLIT_MODE_DEFAULT, + /** do quantifiers splitting aggressively */ + QUANT_DSPLIT_MODE_AGG, +}; + + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ |