diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-10 17:49:13 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-10 17:49:13 -0600 |
| commit | d0df704a60696d7f824eb01781b413d91a0e4202 (patch) | |
| tree | 501058c359ff029cad024a3a715efdf33968c426 /src/options | |
| parent | 346c85d145f6938ce7dce74e7e7cb855d5a6025a (diff) | |
Faster conditional rewriting for and/or beneath quantifiers. Improvements to sort inference, related to constants. Add several quantifiers options, minor refactoring.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index e3f4e94f2..1363626c6 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -57,6 +57,8 @@ option elimTautQuant --elim-taut-quant bool :default true eliminate tautological disjuncts of quantified formulas option purifyQuant --purify-quant bool :default false purify quantified formulas +option elimExtArithQuant --elim-ext-arith-quant bool :default true + eliminate extended arithmetic symbols in quantified formulas #### E-matching options @@ -67,6 +69,8 @@ option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default which ground terms to consider for instantiation option registerQuantBodyTerms --register-quant-body-terms bool :default false consider ground terms within bodies of quantified formulas for matching +option inferArithTriggerEq --infer-arith-trigger-eq bool :default false + infer equalities for trigger terms based on solving arithmetic equalities option smartTriggers --smart-triggers bool :default true enable smart triggers @@ -95,6 +99,8 @@ option incrementTriggers --increment-triggers bool :default true option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "options/quantifiers_modes.h" :handler stringToInstWhenMode :predicate checkInstWhenMode when to apply instantiation +option instWhenDelayIncrement --inst-when-delay-increment bool :default false + delay incrementing counters for inst-when mode to ensure theory combination and standard quantifier effort strategies take turns option instMaxLevel --inst-max-level=N int :read-write :default -1 maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) |