diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-21 14:02:24 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-21 14:02:24 -0600 |
| commit | 60f1dd27da89be80c172e15e01c49f58e0ceb6c0 (patch) | |
| tree | b8aef41ea8e9e37d559b6309d7337109a7fd33aa /src/options | |
| parent | 4a12827561bc070fb5c7fd9baf1320a6bf154bc2 (diff) | |
Cegqi bv remove extract terms preprocess pass (#1376)
* Preprocess extract -> concat pass for cegqi bv.
* Add sygus bench
* Fixes, infrastructure.
* Minor fixes.
* Try
* Minor
* Minor
* Document
* Format
* Improving debug messages.
* Address
* Format
* Overlapping extracts.
* Format
* Minor
* Address review.
* Format
* Comment
* Format
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index c6dbe60c7..8106c5e5d 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -343,6 +343,8 @@ option cbqiBvInterleaveValue --cbqi-bv-interleave-value bool :read-write :defaul 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 choose mode for handling bit-vector inequalities with counterexample-guided instantiation +option cbqiBvRmExtract --cbqi-bv-rm-extract bool :read-write :default false + replaces extract terms with variables for counterexample-guided instantiation for bit-vectors ### local theory extensions options |