projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2d147b7) | patch
Add side conditions for inequalities over BITVECTOR_UREM for CBQI BV. (#1460)
authorAina Niemetz <aina.niemetz@gmail.com>
Sat, 30 Dec 2017 04:02:38 +0000 (20:02 -0800)
committerGitHub <noreply@github.com>
Sat, 30 Dec 2017 04:02:38 +0000 (20:02 -0800)
commitdc2f9914f49076d56cdb18e14971df67fbe567bb
treea82f640d60e27525a3094efaaae110b542ffccc9tree
parent2d147b72e1339f4c281caf7786dfa9b4d79ed21ccommit | diff
Add side conditions for inequalities over BITVECTOR_UREM for CBQI BV. (#1460)

We now can handle all cases of (in|dis)equality over UREM. Previously, we could not handle equality
for index=0 and had to rewrite x % s = t to x - x / s * s. Since we can now handle this case, we do not
apply this rewriting anymore.
src/theory/quantifiers/bv_inverter.cpp diff | blob | history
src/theory/quantifiers/ceg_t_instantiator.cpp diff | blob | history
test/unit/theory/theory_quantifiers_bv_inverter_white.h diff | blob | history