diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2020-09-03 13:28:48 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-03 15:28:48 -0500 |
commit | 31b3986ea297d54e828cd6c34e3689435ba63d7c (patch) | |
tree | b989aace00e94611c8455d76d2dbdbb548b0a23f /src/theory/quantifiers/cegqi | |
parent | 58733b382a4a956c051d06e7318afa1deed612da (diff) |
Changing the handled operators in bv2int preprocessing pass (#4970)
Some of the bit-vector operators are directly translated to integers, while others are eliminated before the translation.
This PR changes the set of operators that we eliminate (and as a consequence, also the set of operators that we handle directly):
The only bit-wise operator that is translated is bvand. The rest are now eliminated.
bvneg is now eliminated.
The various division operators are still eliminated, but using different rewrite rules.
zero-extend and sign-extend are now handled directly.
shifting is changed to favor ITEs over non-linear multiplication.
Diffstat (limited to 'src/theory/quantifiers/cegqi')
0 files changed, 0 insertions, 0 deletions