diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-19 10:32:37 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-19 10:32:37 -0500 |
| commit | 06d91e9121ecdadfc96d6175792992395833329f (patch) | |
| tree | 15a969c7c044279c3677ded69465add67ea96fad /src/options/quantifiers_options | |
| parent | f70674c2f0c6c1c55e3d7c5fed916fc1e7721ffe (diff) | |
Add infrastructure for tracking instantiation lemmas (for proofs, and minimization of --dump-instantiations, qe and synthesis solutions). Eliminate quantified arithmetic variables that only have lower/upper bounds. Cleanup strings preprocess, minor fix for str.replace semantics. Reorder cegqi before fmf. Minor cleanup.
Diffstat (limited to 'src/options/quantifiers_options')
| -rw-r--r-- | src/options/quantifiers_options | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 0b5474959..0a94ad890 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -26,6 +26,8 @@ option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMod # forall y. P( c, y ) option varElimQuant --var-elim-quant bool :default true enable simple variable elimination for quantified formulas +option varIneqElimQuant --var-ineq-elim-quant bool :default true + enable variable elimination based on infinite projection of unbound arithmetic variables option dtVarExpandQuant --dt-var-exp-quant bool :default true expand datatype variables bound to one constructor in quantifiers #ite lift mode for quantified formulas @@ -50,8 +52,6 @@ option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false perform aggressive miniscoping for quantifiers 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 option condRewriteQuant --cond-rewrite-quant bool :default true @@ -328,4 +328,9 @@ option quantAntiSkolem --quant-anti-skolem bool :read-write :default false option quantEqualityEngine --quant-ee bool :default false maintain congrunce closure over universal equalities +### proof options + +option trackInstLemmas --track-inst-lemmas bool :default true + when proof is enabled, track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization) + endmodule |