projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 83d2279) | patch
Add missing side conditions for SHL, LSHR, ASHR for CBQI BV. (#1441)
authorAina Niemetz <aina.niemetz@gmail.com>
Thu, 14 Dec 2017 03:10:16 +0000 (19:10 -0800)
committerGitHub <noreply@github.com>
Thu, 14 Dec 2017 03:10:16 +0000 (19:10 -0800)
commit26214b7b02e90fca270e6bac7d6b64ea1a6d723a
treee27be86f2fd70c677ed7edaa7527d6ab43e6e21dtree
parent83d2279aaa79ce04aa35b394b5063c6d59ff3ac1commit | diff
Add missing side conditions for SHL, LSHR, ASHR for CBQI BV. (#1441)

This adds side conditions for operators BITVECTOR_SHL, BITVECTOR_LSHR and
BITVECTOR_ASHR for index = 1, i.e., s << x = t and s >> x = t. Previously, we treated
 these cases as non-invertible.
src/theory/quantifiers/bv_inverter.cpp diff | blob | history
test/unit/theory/theory_quantifiers_bv_inverter_white.h diff | blob | history