projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b40e264) | patch
bv2int module: translation of more cases (#7653)
authoryoni206 <yoni206@users.noreply.github.com>
Sat, 20 Nov 2021 00:05:03 +0000 (02:05 +0200)
committerGitHub <noreply@github.com>
Sat, 20 Nov 2021 00:05:03 +0000 (00:05 +0000)
commitb984eae6a8608993b8ec13fa8b56ca1d67332e9a
treef18dece878f55314c20e4e5fed2bc3b6d34bde28tree
parentb40e264448e55e48fcc62d92da13332d6d89459dcommit | diff
bv2int module: translation of more cases (#7653)

This commit adds the implementation of the translation from BV to Int for the remaining operators. Some cases are left for the next PR. Corresponding unit tests are added. Notice that in the new module, the following issues do not occur. They will be added as tests in the following PRs:

https://github.com/cvc5/cvc5-projects/issues/345
https://github.com/cvc5/cvc5-projects/issues/344
https://github.com/cvc5/cvc5-projects/issues/343
src/theory/bv/int_blaster.cpp diff | blob | history
test/unit/theory/theory_bv_int_blaster_white.cpp diff | blob | history