projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 06ca7e3) | patch
Add side conditions for inequalities over BITVECTOR_UDIV for CBQI BV. (#1464)
authorAina Niemetz <aina.niemetz@gmail.com>
Wed, 3 Jan 2018 04:30:04 +0000 (20:30 -0800)
committerGitHub <noreply@github.com>
Wed, 3 Jan 2018 04:30:04 +0000 (20:30 -0800)
commit54fa2b48723ace784f2fa5e710aef6c2a38a7bd2
tree8a1ed8319083521dda0c0e55ab369dbdd1988a4atree
parent06ca7e3709fefbbec5d20f9c99e4a630a391dc28commit | diff
Add side conditions for inequalities over BITVECTOR_UDIV for CBQI BV. (#1464)

We now can handle all cases of (in|dis)equality over BITVECTOR_UREM. This also simplifies some
of the side conditions for equality.
src/theory/quantifiers/bv_inverter.cpp diff | blob | history
test/unit/theory/theory_quantifiers_bv_inverter_white.h diff | blob | history