diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-12 15:48:11 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-12 15:48:11 -0500 |
| commit | ca1b17c8bba3681643a1a3de19d32b038c38aceb (patch) | |
| tree | ff02dc2314a3c1e86d19ca9bc2bbe8a57ef1856b /src/options/quantifiers_options | |
| parent | 685b1f3769decafbff1c5b929d4ce01169ff9d81 (diff) | |
Refactor prenex modes.
Diffstat (limited to 'src/options/quantifiers_options')
| -rw-r--r-- | src/options/quantifiers_options | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 2e9aa00cc..04b918afc 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -19,10 +19,10 @@ option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write miniscope quantifiers for ground subformulas option quantSplit --quant-split bool :default true :read-write apply splitting to quantified formulas based on variable disjoint disjuncts -option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "options/quantifiers_modes.h" :read-write :handler stringToPrenexQuantMode +option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_QUANT_SIMPLE :include "options/quantifiers_modes.h" :read-write :handler stringToPrenexQuantMode prenex mode for quantified formulas -option prenexQuantAgg --prenex-quant-agg bool :default false :read-write - aggressive prenexing to ensure prenex normal form +option prenexQuantUser --prenex-quant-user bool :default false :read-write + prenex quantified formulas with user patterns # Whether to variable-eliminate quantifiers. # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to # forall y. P( c, y ) |