projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: be9484d) | patch
Refactor and fix solveBvLit for CBQI BV. (#1526)
authorAina Niemetz <aina.niemetz@gmail.com>
Mon, 22 Jan 2018 04:41:39 +0000 (20:41 -0800)
committerGitHub <noreply@github.com>
Mon, 22 Jan 2018 04:41:39 +0000 (20:41 -0800)
commit6c9a210e2ca3e6dc56217f186cb632beb82ae0fa
treee0f7f4bf3d86cb7f6f7ddaa6f336315c026b9acdtree
parentbe9484dc7f7db5e4301142ccfe493871d9f7eac8commit | diff
Refactor and fix solveBvLit for CBQI BV. (#1526)

This refactors and simplifies solveBvLit() and fixes the following:

- generate side conditions for BITVECTOR_NEG, BITVECTOR_NOT, BITVECTOR_PLUS,
BITVECTOR_XOR over inequalities and disequality
- fix CONCAT handling (generate side conditions rather then computing an inverse which was incorrect)
- fix SIGN_EXTEND handling (same as with CONCATs)
src/options/quantifiers_options diff | blob | history
src/theory/quantifiers/bv_inverter.cpp diff | blob | history
test/regress/regress0/sygus/Makefile.am diff | blob | history
test/unit/theory/theory_quantifiers_bv_inverter_white.h diff | blob | history