diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-15 16:10:20 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-15 16:10:20 -0500 |
| commit | 1cb5f852ba17c13cc39a9c75e5bc0019c80223e8 (patch) | |
| tree | 087879d07b352dd644009ecef24fe0392a90f3d7 /src/options | |
| parent | 60687e672ea8f485b4071e485b7b0cabc034fd00 (diff) | |
Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by default in EPR mode.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 04b918afc..9e704691a 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -47,7 +47,7 @@ option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default fal option preSkolemQuant --pre-skolem-quant bool :read-write :default false apply skolemization eagerly to bodies of quantified formulas option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default true - apply skolemization to nested quantified formulass + apply skolemization to nested quantified formulas option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true apply skolemization to quantified formulas aggressively option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false @@ -118,10 +118,6 @@ option quantRepMode --quant-rep-mode=MODE CVC4::theory::quantifiers::QuantRepMo option instRelevantCond --inst-rlv-cond bool :default false add relevancy conditions for instantiations - -option eagerInstQuant --eager-inst-quant bool :default false - apply quantifier instantiation eagerly - option fullSaturateQuant --full-saturate-quant bool :default false :read-write when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown option fullSaturateQuantRd --full-saturate-quant-rd bool :default true @@ -293,8 +289,6 @@ option cbqiPreRegInst --cbqi-prereg-inst bool :read-write :default false preregister ground instantiations in counterexample-based quantifier instantiation option cbqiMinBounds --cbqi-min-bounds bool :default false use minimally constrained lower/upper bound for counterexample-based quantifier instantiation -option cbqiSymLia --cbqi-sym-lia bool :default false - use symbolic integer division in substitutions for counterexample-based quantifier instantiation option cbqiRoundUpLowerLia --cbqi-round-up-lia bool :default false round up integer lower bounds in substitutions for counterexample-based quantifier instantiation option cbqiMidpoint --cbqi-midpoint bool :default false |