diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 12:43:15 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 12:43:31 -0600 |
| commit | e8c09abb9165278b13491c83bdcbe17ae535126e (patch) | |
| tree | 1101d3e878bcfd9e12cd64aaad3017aa320c896b /src/options/quantifiers_options | |
| parent | 0e956da9b32ce8a8fcf20ec65e5a2820b4e31324 (diff) | |
Refactoring, generalization of bounded inference module. Simplification of rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.
Diffstat (limited to 'src/options/quantifiers_options')
| -rw-r--r-- | src/options/quantifiers_options | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index f6b6e2177..856de103e 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -325,7 +325,7 @@ option macrosQuant --macros-quant bool :read-write :default false perform quantifiers macro expansion option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF :include "options/quantifiers_modes.h" :handler stringToMacrosQuantMode mode for quantifiers macro expansion -option quantDynamicSplit --quant-dsplit-mode=MODE CVC4::theory::quantifiers::QuantDSplitMode :read-write :default CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT :include "options/quantifiers_modes.h" :handler stringToQuantDSplitMode +option quantDynamicSplit --quant-dsplit-mode=MODE CVC4::theory::quantifiers::QuantDSplitMode :read-write :default CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToQuantDSplitMode mode for dynamic quantifiers splitting option quantAntiSkolem --quant-anti-skolem bool :read-write :default false perform anti-skolemization for quantified formulas |