projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 198e4a9) | patch
bv-to-int: more implementations (#7051)
authoryoni206 <yoni206@users.noreply.github.com>
Tue, 24 Aug 2021 01:20:56 +0000 (04:20 +0300)
committerGitHub <noreply@github.com>
Tue, 24 Aug 2021 01:20:56 +0000 (01:20 +0000)
commit2c35a4fd262a7aa1cc3b953265d327de4eae9f8e
tree0ff9aeea76a86ad8fe07a344384de37139efcfdctree
parent198e4a9b622bff260cf6b24f67f31fbff11873f2commit | diff
bv-to-int: more implementations (#7051)

This PR introduces more implementations for the bv-to-int module. Once all implementations are in, this module will be called from the bv-to-int preprocessing pass, and the code there will be deleted.

Here we focus on the translation of nodes without children.
Unit tests are included.
src/theory/bv/int_blaster.cpp diff | blob | history
src/theory/bv/int_blaster.h diff | blob | history
test/unit/theory/theory_bv_int_blaster_white.cpp diff | blob | history