diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-01-22 10:06:26 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-01-22 10:06:26 -0800 |
| commit | 7b12b1e8307295e68cb389eaa7692036fae6e872 (patch) | |
| tree | fca232d920668c9a05e628576d19a58caa391fff /src/options | |
| parent | 6c9a210e2ca3e6dc56217f186cb632beb82ae0fa (diff) | |
Add previous concat handling for CBQI BV as heuristic for EQ. (#1528)
Previously, we computed an inverse for s1 o x, x o s2, s1 o x o s2 while disregarding that invertibility
depends on si. This adds this handling as an optional heuristic for concats over (dis)equality since it improves performance on a considerable number of benchmarks.
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 2376409e0..c6eb1cd5e 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -355,6 +355,8 @@ option cbqiBvRmExtract --cbqi-bv-rm-extract bool :read-write :default true replaces extract terms with variables for counterexample-guided instantiation for bit-vectors option cbqiBvLinearize --cbqi-bv-linear bool :read-write :default true linearize adder chains for variables +option cbqiBvConcInv cbqi-bv-concat-inv --cbqi-bv-concat-inv bool :read-write :default true + compute inverse for concat over equalities rather than producing an invertibility condition ### local theory extensions options |