diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-29 18:17:16 -0600 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2017-11-29 16:17:16 -0800 |
| commit | 0524281144b562fea63adf10bc3f5d6f75883296 (patch) | |
| tree | fb812221b635a2e5f9ffef6b586008ad53cfa251 /src/options | |
| parent | dd31916953ecc29514499e5c1cb96e3ae33ff3b8 (diff) | |
Minor improvements and changes to defaults for cbqi bv (#1406)
This
makes it so that --cbqi-bv tries at most 2 instantiations per quantified formula (one based on inversions when applicable, one based on model values). This makes it so that we do not have exponential run time in the worst case. This helps significantly for psyco benchmarks which have many quantified variables.
Enables --cbqi-bv by default and changes the default inequality mode to eq-boundary (which is the best performer overall), also enables extract removal by default
Allows cbqiNestedQE to be used in the BV logic.
Adds an option --cbqi-full which indicates whether we should try model value instantiations for bit-vectors (by default, this is done only for the pure BV logic).
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 1a4275d77..4a7a9e8a7 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -299,6 +299,8 @@ option sygusStream --sygus-stream bool :default false # CEGQI applied to general quantified formulas option cbqi --cbqi bool :read-write :default false turns on counterexample-based quantifier instantiation +option cbqiFullEffort --cbqi-full bool :read-write :default false + turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation option recurseCbqi --cbqi-recurse bool :default true turns on recursive counterexample-based quantifier instantiation option cbqiSat --cbqi-sat bool :read-write :default true @@ -339,13 +341,13 @@ option quantEprMatching --quant-epr-match bool :default true use matching heuristics for EPR instantiation # CEGQI for BV -option cbqiBv --cbqi-bv bool :read-write :default false +option cbqiBv --cbqi-bv bool :read-write :default true use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors option cbqiBvInterleaveValue --cbqi-bv-interleave-value bool :read-write :default false interleave model value instantiation with word-level inversion approach -option cbqiBvIneqMode --cbqi-bv-ineq=MODE CVC4::theory::quantifiers::CbqiBvIneqMode :read-write :default CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_SLACK :include "options/quantifiers_modes.h" :handler stringToCbqiBvIneqMode +option cbqiBvIneqMode --cbqi-bv-ineq=MODE CVC4::theory::quantifiers::CbqiBvIneqMode :read-write :default CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY :include "options/quantifiers_modes.h" :handler stringToCbqiBvIneqMode choose mode for handling bit-vector inequalities with counterexample-guided instantiation -option cbqiBvRmExtract --cbqi-bv-rm-extract bool :read-write :default false +option cbqiBvRmExtract --cbqi-bv-rm-extract bool :read-write :default true replaces extract terms with variables for counterexample-guided instantiation for bit-vectors ### local theory extensions options |