projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e03d56b) | patch
CBQI BV: Add handling for missing operators. (#1274)
authorAina Niemetz <aina.niemetz@gmail.com>
Wed, 25 Oct 2017 20:04:05 +0000 (13:04 -0700)
committerGitHub <noreply@github.com>
Wed, 25 Oct 2017 20:04:05 +0000 (13:04 -0700)
commitc49ef48588c708bfef3c7a0f9db8219415301a94
tree1664042f6a64daeaf3cee0dbbe0ebf7caa3544betree
parente03d56b6de112cae8e9234fff16b985f0765740ecommit | diff
CBQI BV: Add handling for missing operators. (#1274)

This adds inverse handling for BITVECTOR_XOR, BITVECTOR_SIGN_EXTENDS, BITVECTOR_COMP, BITVECTOR_ASHR. Function isInvertible() now corresponds to exactly the operators (plus index) for which we can determine an inverse, which avoids traversing along non-invertible paths.

This further enables a test case that I missed to enable in PR #1268.
src/theory/quantifiers/bv_inverter.cpp diff | blob | history
src/theory/quantifiers/bv_inverter.h diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 diff | blob | history
test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 diff | blob | history
test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 [new file with mode: 0644] blob