projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6c9a210) | patch
Add previous concat handling for CBQI BV as heuristic for EQ. (#1528)
authorAina Niemetz <aina.niemetz@gmail.com>
Mon, 22 Jan 2018 18:06:26 +0000 (10:06 -0800)
committerGitHub <noreply@github.com>
Mon, 22 Jan 2018 18:06:26 +0000 (10:06 -0800)
commit7b12b1e8307295e68cb389eaa7692036fae6e872
treefca232d920668c9a05e628576d19a58caa391ffftree
parent6c9a210e2ca3e6dc56217f186cb632beb82ae0facommit | 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.
src/options/quantifiers_options diff | blob | history
src/theory/quantifiers/bv_inverter.cpp diff | blob | history