diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-13 00:12:02 -0500 |
|---|---|---|
| committer | Mathias Preiner <mathias.preiner@gmail.com> | 2017-10-12 22:12:02 -0700 |
| commit | 39a85cc99f3b9f3d203490f5918ebe56bd916d64 (patch) | |
| tree | 1962850621944d07af786ff491463e043aefcff1 /src/options/quantifiers_options | |
| parent | 5031c6d9a08c84a6e8fe5019c6e278b8b2d7a238 (diff) | |
CBQI BV quick heuristics (#1239)
Adds two heuristics for cbqi-bv, both disabled by default.
The first optimistically solves for boundary points of inequalities.
The second randomly interleaves inversion and value instantiations.
Adds some newly solved regressions from SMT LIB.
Diffstat (limited to 'src/options/quantifiers_options')
| -rw-r--r-- | src/options/quantifiers_options | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 2e765ce6b..d3f8c9f6a 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -334,7 +334,11 @@ option quantEprMatching --quant-epr-match bool :default true # CEGQI for BV option cbqiBv --cbqi-bv bool :read-write :default false - use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors + 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 cbqiBvSlackIneq --cbqi-bv-slack-ineq bool :read-write :default true + use model slack values when solving inequalities with word-level inversion approach ### local theory extensions options |